mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.relabelEquiv.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (g : α ≃ β) {k : ℕ},
  FirstOrder.Language.BoundedFormula.relabelEquiv g =
    FirstOrder.Language.BoundedFormula.mapTermRelEquiv
      (fun _n => FirstOrder.Language.Term.relabelEquiv (g.sumCongr (Equiv.refl (Fin _n)))) fun _n =>
      Equiv.refl (L.Relations _n)
-- Std.Time.Date.Unit.Year
Std.Time.Year.instLTOffset : LT Std.Time.Year.Offset
-- Mathlib.Algebra.Order.ToIntervalMod
toIcoMod_ofNat_mul_add' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ) [inst_4 : m.AtLeastTwo],
  toIcoMod hp (OfNat.ofNat m * p + a) b = OfNat.ofNat m * p + toIcoMod hp a b
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extMk_comp_mk₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} {R : CategoryTheory.InjectiveResolution Y} {n : ℕ}
  (f : X ⟶ R.cocomplex.X n) (m : ℕ) (hm : n + 1 = m) (hf : CategoryTheory.CategoryStruct.comp f (R.cocomplex.d n m) = 0)
  {Y' : C} {R' : CategoryTheory.InjectiveResolution Y'} {g : Y ⟶ Y'} (φ : R.Hom R' g),
  (R.extMk f m hm hf).comp (CategoryTheory.Abelian.Ext.mk₀ g) ⋯ =
    R'.extMk (CategoryTheory.CategoryStruct.comp f (φ.hom.f n)) m hm ⋯
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.WithBot.completeLattice.eq_1 : ∀ {α : Type u_5} [inst : ConditionallyCompleteLattice α],
  WithTop.WithBot.completeLattice =
    { toLattice := WithTop.lattice, toSupSet := WithTop.instSupSet, isLUB_sSup := ⋯, toInfSet := WithTop.instInfSet,
      isGLB_sInf := ⋯, toBoundedOrder := WithTop.instBoundedOrder }
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.polar_univ : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜),
  B.SeparatingRight → B.polar Set.univ = {0}
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Construct a multifork using a collection `ι` of morphisms.  -/
CategoryTheory.Limits.Multifork.ofι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        (P : C) →
          (ι : (a : J.L) → P ⟶ I.left a) →
            (∀ (b : J.R),
                CategoryTheory.CategoryStruct.comp (ι (J.fst b)) (I.fst b) =
                  CategoryTheory.CategoryStruct.comp (ι (J.snd b)) (I.snd b)) →
              CategoryTheory.Limits.Multifork I
-- Mathlib.Order.Filter.Map
Filter.gc_map_comap : ∀ {α : Type u_1} {β : Type u_2} (m : α → β), GaloisConnection (Filter.map m) (Filter.comap m)
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.head_eval : ∀ (v : List ℕ), Turing.ToPartrec.Code.head.eval v = pure [v.headI]
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_union_add_inter' : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s →
    autoParam (μ s ≠ ⊤) MeasureTheory.measureReal_union_add_inter'._auto_1 →
      autoParam (μ t ≠ ⊤) MeasureTheory.measureReal_union_add_inter'._auto_3 →
        μ.real (s ∪ t) + μ.real (s ∩ t) = μ.real s + μ.real t
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Check whether any suggestion has been made.  -/
_private.Mathlib.Tactic.ClickSuggestions.Util.0.Mathlib.Tactic.ClickSuggestions.checkProgress : Mathlib.Tactic.ClickSuggestions.ClickSuggestionsM Unit
-- Mathlib.Tactic.ClickSuggestions.Util
/-- Whether any progress has been made at all. If all computations have been finished
and no progress has been made, then inform the user.  -/
Mathlib.Tactic.ClickSuggestions.State.progress : Mathlib.Tactic.ClickSuggestions.State → Bool
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.lift_le_ofENat : ∀ {x : Cardinal.{v}} {m : ℕ∞}, Cardinal.lift.{u, v} x ≤ ↑m ↔ x ≤ ↑m
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.isRightKanExtension_iff_of_iso₂ : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  {L : CategoryTheory.Functor C D} {F₁ F₂ : CategoryTheory.Functor C H} {F₁' F₂' : CategoryTheory.Functor D H}
  (α₁ : L.comp F₁' ⟶ F₁) (α₂ : L.comp F₂' ⟶ F₂) (e : F₁ ≅ F₂) (e' : F₁' ≅ F₂'),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft e'.hom) α₂ = CategoryTheory.CategoryStruct.comp α₁ e.hom →
    (F₁'.IsRightKanExtension α₁ ↔ F₂'.IsRightKanExtension α₂)
-- Mathlib.Algebra.Order.BigOperators.Group.Multiset
Multiset.le_sum_nonempty_of_subadditive_on_pred : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β] (f : α → β) (p : α → Prop),
  (∀ (a b : α), p a → p b → f (a + b) ≤ f a + f b) →
    (∀ (a b : α), p a → p b → p (a + b)) → ∀ (s : Multiset α), s ≠ ∅ → (∀ a ∈ s, p a) → f s.sum ≤ (Multiset.map f s).sum
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.Homotopy.smul_h₃ : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C] {S₁ S₂ : CategoryTheory.ShortComplex C}
  {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) (a : R), (h.smul a).h₃ = a • h.h₃
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.sdiff_of_isLowerSet : ∀ {α : Type u_1} [inst : LE α] {s t : Set α}, IsUpperSet s → IsLowerSet t → IsUpperSet (s \ t)
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- A presheaf `P` is separated for the Grothendieck topology `J` iff for every covering sieve
`S` of `J`, the natural cone associated to `P` and `S` admits at most one morphism from every
cone in the same category.  -/
CategoryTheory.Presheaf.isSeparated_iff_subsingleton : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  (J : CategoryTheory.GrothendieckTopology C) (P : CategoryTheory.Functor Cᵒᵖ A),
  (∀ (E : A), CategoryTheory.Presieve.IsSeparated J (P.comp (CategoryTheory.coyoneda.obj (Opposite.op E)))) ↔
    ∀ ⦃X : C⦄,
      ∀ S ∈ J X,
        ∀ (c : CategoryTheory.Limits.Cone (S.arrows.diagram.op.comp P)), Subsingleton (c ⟶ P.mapCone S.arrows.cocone.op)
-- Mathlib.Analysis.Calculus.FDeriv.Congr
HasFDerivWithinAt.congr_mono : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {f' : E →L[𝕜] F} {x : E} {s t : Set E},
  HasFDerivWithinAt f f' s x → Set.EqOn f₁ f t → f₁ x = f x → t ⊆ s → HasFDerivWithinAt f₁ f' t x
-- Batteries.Recycling.RBTree.Basic
RBTree.RBSet.instInhabited : (α : Type u) → (cmp : α → α → Ordering) → Inhabited (RBTree.RBSet α cmp)
-- Lean.Meta.Constructions.RecOn
Lean.mkRecOn : Lean.Name → Lean.MetaM Unit
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- Every functor out of the walking pair is naturally isomorphic (actually, equal) to a `pair`  -/
CategoryTheory.Limits.diagramIsoPair : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C) →
      F ≅
        CategoryTheory.Limits.pair (F.obj { as := CategoryTheory.Limits.WalkingPair.left })
          (F.obj { as := CategoryTheory.Limits.WalkingPair.right })
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat
_private.Lean.Meta.Tactic.Simp.BuiltinSimprocs.Nat.0.Nat.EqResult.eq.sizeOf_spec : ∀ (x y p : Lean.Expr), sizeOf (Nat.EqResult.eq✝ x y p) = 1 + sizeOf x + sizeOf y + sizeOf p
-- Mathlib.RingTheory.IsTensorProduct
Algebra.lift_algHom_comp_right : ∀ {R : Type u_1} {S : Type v₃} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {R' : Type u_6}
  (S' : Type u_7) [inst_3 : CommSemiring R'] [inst_4 : CommSemiring S'] [inst_5 : Algebra R R'] [inst_6 : Algebra S S']
  [inst_7 : Algebra R' S'] [inst_8 : Algebra R S'] [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S']
  [inst_11 : Algebra.IsPushout R S R' S'] {A : Type u_8} [inst_12 : Semiring A] [inst_13 : Algebra R A] (f : S →ₐ[R] A)
  (g : R' →ₐ[R] A) (H : ∀ (x : S) (y : R'), f x * g y = g y * f x),
  (Algebra.pushoutDesc S' f g H).comp (IsScalarTower.toAlgHom R R' S') = g
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.qExpansion_pow : ∀ {k : ℤ} {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} [inst : Γ.HasDetPlusMinusOne],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ (f : ModularForm Γ k) (n : ℕ), UpperHalfPlane.qExpansion h ⇑(f.pow n) = UpperHalfPlane.qExpansion h ⇑f ^ n
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap.0.WeierstrassCurve.termT : Lean.ParserDescr
-- Lean.Environment
Lean.Kernel.Exception.thmTypeIsNotProp : Lean.Kernel.Environment → Lean.Name → Lean.Expr → Lean.Kernel.Exception
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_alter_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : Option β → Option β}, k ∈ t.alter k f ↔ (f t[k]?).isSome = true
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.fintypeAdd.eq_1 : ∀ {α : Type u_2} [inst : Add α] [inst_1 : DecidableEq α] (s t : Set α) [inst_2 : Fintype ↑s] [inst_3 : Fintype ↑t],
  s.fintypeAdd t = Set.fintypeImage2 (fun x1 x2 => x1 + x2) s t
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
/-- The compatibility of `HomotopyCategory.BinaryProduct.inverse`
with respect to associators.  -/
SSet.Truncated.HomotopyCategory.BinaryProduct.associativityIso : (X Y Z : SSet.Truncated 2) →
  ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X Y).prod (CategoryTheory.Functor.id Z.HomotopyCategory)).comp
      ((SSet.Truncated.HomotopyCategory.BinaryProduct.inverse (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
            Z).comp
        (SSet.Truncated.mapHomotopyCategory (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)) ≅
    (CategoryTheory.prod.associativity X.HomotopyCategory Y.HomotopyCategory Z.HomotopyCategory).functor.comp
      (((CategoryTheory.Functor.id X.HomotopyCategory).prod
            (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse Y Z)).comp
        (SSet.Truncated.HomotopyCategory.BinaryProduct.inverse X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)))
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst : AlgebraicGeometry.LocallyOfFiniteType f],
  AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus f = AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus f_1
-- Mathlib.Algebra.Homology.ShortComplex.Basic
/-- the first morphism of a `ShortComplex`  -/
CategoryTheory.ShortComplex.f : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] → (self : CategoryTheory.ShortComplex C) → self.X₁ ⟶ self.X₂
-- Mathlib.Order.MinMax
max_eq_left_iff : ∀ {α : Type u} [inst : LinearOrder α] {a b : α}, max a b = a ↔ b ≤ a
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM.State : Type
-- Mathlib.Algebra.DirectSum.Internal
/-- The subalgebra `A 0` of `R`.  -/
SetLike.GradeZero.subalgebra : {ι : Type u_1} →
  {S : Type u_3} →
    {R : Type u_4} →
      [inst : CommSemiring S] →
        [inst_1 : Semiring R] →
          [inst_2 : Algebra S R] →
            [inst_3 : AddMonoid ι] → (A : ι → Submodule S R) → [SetLike.GradedMonoid A] → Subalgebra S R
-- Mathlib.CategoryTheory.Elements
CategoryTheory.CategoryOfElements.fromCostructuredArrow_map_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor Cᵒᵖ (Type v))
  {X Y : (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ} (f : X ⟶ Y),
  ↑((CategoryTheory.CategoryOfElements.fromCostructuredArrow F).map f) = f.unop.left.op
-- Mathlib.Probability.ConditionalProbability
/-- The conditional probability measure of any measure on any set of finite positive measure
is a probability measure.  -/
ProbabilityTheory.cond_isProbabilityMeasure_of_finite : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s : Set Ω},
  μ s ≠ 0 → μ s ≠ ⊤ → MeasureTheory.IsProbabilityMeasure μ[|s]
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Hom.of.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} {as as_1 : CategoryTheory.Oplax.OplaxTrans.Modification η θ},
  { as := as } = { as := as_1 } → as = as_1
-- Mathlib.Topology.ContinuousMap.Ordered
ContinuousMap.inf : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : SemilatticeInf β] → [ContinuousInf β] → Min C(α, β)
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- The power of a point is negative if and only if the point lies inside the sphere.  -/
EuclideanGeometry.Sphere.power_neg_iff_dist_center_lt_radius : ∀ {P : Type u_2} [inst : MetricSpace P] {s : EuclideanGeometry.Sphere P} {p : P},
  0 ≤ s.radius → (s.power p < 0 ↔ dist p s.center < s.radius)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getD_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k k' : α} {fallback : β k'} {f : Option (β k) → Option (β k)},
  (t.alter k f).getD k' fallback =
    if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).getD fallback else t.getD k' fallback
-- Mathlib.Algebra.Star.Subalgebra
StarAlgEquiv.restrictScalars_apply : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : MulAction R S]
  [inst_5 : Module S A] [inst_6 : Module S B] [inst_7 : Module R A] [inst_8 : Module R B] [inst_9 : IsScalarTower R S A]
  [inst_10 : IsScalarTower R S B] [inst_11 : Star A] [inst_12 : Star B] (f : A ≃⋆ₐ[S] B) (a : A),
  (StarAlgEquiv.restrictScalars R f) a = f a
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.vdecl.sizeOf_spec : ∀ (x : Lean.IR.VarId) (ty : Lean.IR.IRType) (e : Lean.IR.Expr) (b : Lean.IR.FnBody),
  sizeOf (Lean.IR.FnBody.vdecl x ty e b) = 1 + sizeOf x + sizeOf ty + sizeOf e + sizeOf b
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Affine
/-- An oriented angle is unchanged by replacing the third point by one weakly further away on the
same ray.  -/
Wbtw.oangle_eq_right : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ p₃' : P},
  Wbtw ℝ p₂ p₃ p₃' → p₃ ≠ p₂ → EuclideanGeometry.oangle p₁ p₂ p₃ = EuclideanGeometry.oangle p₁ p₂ p₃'
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.denoteSInt.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (k : ℤ),
  Lean.Grind.CommRing.denoteSInt k = bif decide (k < 0) then 0 else OfNat.ofNat k.natAbs
-- Mathlib.LinearAlgebra.RootSystem.Irreducible
RootPairing.IsIrreducible.eq_top_of_invtSubmodule_coreflection : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} {inst : CommRing R} {inst_1 : AddCommGroup M}
  {inst_2 : Module R M} {inst_3 : AddCommGroup N} {inst_4 : Module R N} {P : RootPairing ι R M N}
  [self : P.IsIrreducible] (q : Submodule R N),
  (∀ (i : ι), q ∈ Module.End.invtSubmodule ↑(P.coreflection i)) → q ≠ ⊥ → q = ⊤
-- Init.Data.Range.Basic
Std.Legacy.instMembershipNatRange : Membership ℕ Std.Legacy.Range
-- Mathlib.Topology.Algebra.ConstMulAction
/-- Eta-expanded form of `ContinuousWithinAt.const_smul` -/
ContinuousWithinAt.fun_const_smul : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : SMul M α] [ContinuousConstSMul M α]
  [inst_3 : TopologicalSpace β] {g : β → α} {b : β} {s : Set β},
  ContinuousWithinAt g s b → ∀ (c : M), ContinuousWithinAt (fun i => c • g i) s b
-- Mathlib.Algebra.Polynomial.Homogenize
Polynomial.homogenize_add : ∀ {R : Type u_1} [inst : CommSemiring R] (p q : Polynomial R) (n : ℕ),
  (p + q).homogenize n = p.homogenize n + q.homogenize n
-- Batteries.Tactic.GeneralizeProofs
/-- Context for the `MAbs` monad.  -/
Batteries.Tactic.GeneralizeProofs.AContext : Type
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.eqToHom_comp_ι_assoc : ∀ {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.HasColimit F] {j j' : J} (hj : j = j') {Z : C}
  (h : CategoryTheory.Limits.colimit F ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F j') h
-- Mathlib.Topology.Defs.Induced
/-- A topological embedding is injective.  -/
Topology.IsEmbedding.injective : ∀ {X : Type u_1} {Y : Type u_2} [tX : TopologicalSpace X] [tY : TopologicalSpace Y] {f : X → Y},
  Topology.IsEmbedding f → Function.Injective f
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.zeroLocus_sup_homogeneousIdeal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (I J : HomogeneousIdeal 𝒜),
  ProjectiveSpectrum.zeroLocus 𝒜 ↑(I ⊔ J) = ProjectiveSpectrum.zeroLocus 𝒜 ↑I ∩ ProjectiveSpectrum.zeroLocus 𝒜 ↑J
-- Init.Data.UInt.Bitwise
UInt64.toUSize_shiftLeft_mod : ∀ (a b : UInt64), (a <<< (b % UInt64.ofNat System.Platform.numBits)).toUSize = a.toUSize <<< b.toUSize
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.semiconjBy_iff : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Mul (f i)] {x y z : (i : I) → f i},
  SemiconjBy x y z ↔ ∀ (i : I), SemiconjBy (x i) (y i) (z i)
-- Mathlib.Algebra.Field.Defs
/-- `a ^ 0 = 1`  -/
Field.zpow_zero' : ∀ {K : Type u} [self : Field K] (a : K), a ^ 0 = 1
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.sizeUpTo.eq_1 : ∀ {n : ℕ} (c : Composition n) (i : ℕ), c.sizeUpTo i = (List.take i c.blocks).sum
-- Mathlib.Algebra.Group.Torsion
instNoNatZeroDivisorsOfIsAddTorsionFree : ∀ {M : Type u_1} [inst : AddCommMonoid M] [IsAddTorsionFree M], Lean.Grind.NoNatZeroDivisors M
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.subset_adjoin_of_subset_left : ∀ {E : Type u_2} [inst : Field E] (S : Set E) {F : Subfield E} {T : Set E},
  T ⊆ ↑F → T ⊆ ↑(IntermediateField.adjoin (↥F) S)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_comp_equiv : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : κ → M} (e : ι ≃ κ),
  s.prod (f ∘ ⇑e) = (Finset.map e.toEmbedding s).prod f
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.colLen_anti : ∀ (μ : YoungDiagram) (j1 j2 : ℕ), j1 ≤ j2 → μ.colLen j2 ≤ μ.colLen j1
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.addCommMonoid : {R : Type u_1} →
  [inst : CommSemiring R] →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : AddCommMonoid N] →
            [inst_3 : Module R M] → [inst_4 : Module R N] → AddCommMonoid (TensorProduct R M N)
-- Mathlib.Algebra.BigOperators.Finprod
finprod_mem_def : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] (s : Set α) (f : α → M),
  ∏ᶠ (a : α) (_ : a ∈ s), f a = ∏ᶠ (a : α), s.mulIndicator f a
-- Init.Data.String.Basic
String.Pos.Raw.utf8SetAux.eq_def : ∀ (c' : Char) (x : List Char) (x_1 x_2 : String.Pos.Raw),
  String.Pos.Raw.utf8SetAux c' x x_1 x_2 =
    match x, x_1, x_2 with
    | [], x, x_3 => []
    | c :: cs, i, p => if i = p then c' :: cs else c :: String.Pos.Raw.utf8SetAux c' cs (i + c) p
-- Lean.Data.LOption
Lean.toLOptionM : {α : Type} → {m : Type → Type} → [Monad m] → m (Option α) → m (Lean.LOption α)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.triangle.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C],
  CochainComplex.mappingCocone.triangle φ =
    CategoryTheory.Pretriangulated.Triangle.mk (CochainComplex.mappingCocone.fst φ) φ
      (CategoryTheory.CategoryStruct.comp (CochainComplex.mappingCone.triangle φ).mor₂
        ((CategoryTheory.shiftFunctorCompIsoId (CochainComplex C ℤ) (-1) 1
                CochainComplex.mappingCocone.triangle._proof_2).inv.app
          (CochainComplex.mappingCone φ)))
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.rightHomologyMap_congr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  [inst_2 : S₁.HasRightHomology] [inst_3 : S₂.HasRightHomology],
  CategoryTheory.ShortComplex.rightHomologyMap φ₁ = CategoryTheory.ShortComplex.rightHomologyMap φ₂
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.sum_coe_finset : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} (s : Finset ι) (μ : ι → MeasureTheory.Measure α),
  (MeasureTheory.Measure.sum fun i => μ ↑i) = ∑ i ∈ s, μ i
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.IsNClique.erase_of_mem : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} {s : Finset α} {a : α} [inst : DecidableEq α],
  G.IsNClique n s → a ∈ s → G.IsNClique (n - 1) (s.erase a)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.foldl_eq_foldl_toList : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} {δ : Type w}
  {f : δ → (a : α) → β a → δ} {init : δ},
  Std.DTreeMap.Raw.foldl f init t = List.foldl (fun a b => f a b.fst b.snd) init t.toList
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- the first morphism in the factorizations  -/
CategoryTheory.MorphismProperty.FunctorialFactorizationData.i : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      (self : W₁.FunctorialFactorizationData W₂) → CategoryTheory.Arrow.leftFunc ⟶ self.Z
-- Mathlib.Analysis.Calculus.Deriv.Mul
/-- **Alias** of `derivWithin_fun_finsetProd`. -/
derivWithin_fun_finset_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {ι : Type u_2} [inst_1 : DecidableEq ι]
  {𝔸' : Type u_3} [inst_2 : NormedCommRing 𝔸'] [inst_3 : NormedAlgebra 𝕜 𝔸'] {u : Finset ι} {f : ι → 𝕜 → 𝔸'},
  (∀ i ∈ u, DifferentiableWithinAt 𝕜 (f i) s x) →
    derivWithin (fun x => ∏ i ∈ u, f i x) s x = ∑ i ∈ u, (∏ j ∈ u.erase i, f j x) • derivWithin (f i) s x
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.map_smulₛₗ : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂) (c : R₁) (x : M₁),
  f (c • x) = σ₁₂ c • f x
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.coyonedaEvaluation_map_down : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (P Q : C × CategoryTheory.Functor C (Type v₁)) (α : P ⟶ Q)
  (x : (CategoryTheory.coyonedaEvaluation C).obj P),
  ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.coyonedaEvaluation C).map α)) x).down =
    (CategoryTheory.ConcreteCategory.hom (α.2.app Q.1)) ((CategoryTheory.ConcreteCategory.hom (P.2.map α.1)) x.down)