mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Antichain
isWeakAntichain_insert : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] {s : Set ((i : ι) → α i)} {a : (i : ι) → α i},
  IsWeakAntichain (insert a s) ↔
    IsWeakAntichain s ∧ ∀ ⦃b : (i : ι) → α i⦄, b ∈ s → a ≠ b → ¬StrongLT a b ∧ ¬StrongLT b a
-- Mathlib.Algebra.Group.Defs
instIsDedekindFiniteMonoidOfIsLeftCancelMul : ∀ (M : Type u_2) [inst : Monoid M] [IsLeftCancelMul M], IsDedekindFiniteMonoid M
-- Mathlib.Algebra.Group.Action.Units
AddUnits.addAction' : {G : Type u_1} →
  {M : Type u_3} →
    [inst : AddGroup G] →
      [inst_1 : AddMonoid M] →
        [inst_2 : AddAction G M] → [VAddCommClass G M M] → [VAddAssocClass G M M] → AddAction G (AddUnits M)
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- The copy of `⊥` in any simple graph that can embed its vertices.  -/
SimpleGraph.Copy.bot : {α : Type u_4} → {β : Type u_5} → {B : SimpleGraph β} → (α ↪ β) → ⊥.Copy B
-- Mathlib.Algebra.Notation.Prod
Prod.instOne.eq_1 : ∀ {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N], Prod.instOne = { one := (1, 1) }
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
mulRight_bijective₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀), a ≠ 0 → Function.Bijective fun x => x * a
-- Aesop.Search.Expansion.Simp
Aesop.simpAll : Lean.MVarId →
  Lean.Meta.Simp.Context →
    Lean.Meta.Simp.SimprocsArray → optParam Lean.Meta.Simp.Stats { } → Lean.MetaM Aesop.SimpResult
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.hom_inv_apply : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] (A B : Rep.{w, u, v} k G) (e : A ≅ B) (x : ↑B),
  (Rep.Hom.hom e.hom) ((Rep.Hom.hom e.inv) x) = x
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.ForgetEnrichment.to_of : ∀ {C : Type u₁} (W : Type v) [inst : CategoryTheory.Category.{w, v} W] [inst_1 : CategoryTheory.MonoidalCategory W]
  [inst_2 : CategoryTheory.EnrichedCategory W C] (X : C),
  CategoryTheory.ForgetEnrichment.to W (CategoryTheory.ForgetEnrichment.of W X) = X
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.inl_v_descShortComplex_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)) (i j : ℤ) (h : i + -1 = j),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.inl S.f).v i j h)
      ((CochainComplex.mappingCone.descShortComplex S).f j) =
    0
-- Mathlib.RingTheory.Adjoin.FG
is_noetherian_subring_closure : ∀ {R : Type u} [inst : CommRing R] (s : Set R), s.Finite → IsNoetherianRing ↥(Subring.closure s)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure.of_colimitPresentation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)] {X : C} {a : α}
  (pres : CategoryTheory.Limits.ColimitPresentation (J a) X),
  (∀ (j : J a), P.colimitsClosure J (pres.diag.obj j)) → P.colimitsClosure J X
-- Aesop.RuleTac.RuleTerm
Aesop.RuleTerm.term.injEq : ∀ (term term_1 : Lean.Term), (Aesop.RuleTerm.term term = Aesop.RuleTerm.term term_1) = (term = term_1)
-- Mathlib.LinearAlgebra.Matrix.Swap
/-- Swap matrices are self inverse.  -/
Matrix.swap_mul_self : ∀ {R : Type u_1} {n : Type u_2} [inst : Semiring R] [inst_1 : DecidableEq n] [inst_2 : Fintype n] (i j : n),
  Matrix.swap R i j * Matrix.swap R i j = 1
-- Init.Data.Int.Gcd
Int.lcm_eq_iff : ∀ {n m : ℤ} {l : ℕ}, n.lcm m = l ↔ n ∣ ↑l ∧ m ∣ ↑l ∧ ∀ (c : ℤ), n ∣ c → m ∣ c → ↑l ∣ c
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.Ψ₃_ne_zero : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), 3 ≠ 0 → W.Ψ₃ ≠ 0
-- Mathlib.CategoryTheory.Monoidal.Limits.Shapes.Pullback
CategoryTheory.MonoidalCategory.IsPushout.whiskerLeft_inr_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {Z X Y P : C}
  {f : Z ⟶ X} {g : Z ⟶ Y} {inl : X ⟶ P} {inr : Y ⟶ P} (hP : CategoryTheory.IsPushout f g inl inr) {W : C} (h : X ⟶ W)
  (k : Y ⟶ W) (w : CategoryTheory.CategoryStruct.comp f h = CategoryTheory.CategoryStruct.comp g k) {Q : C},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q inr)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (hP.desc h k w)) =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q k
-- Init.Data.Option.Basic
Option.instOrElse : {α : Type u_1} → OrElse (Option α)
-- Mathlib.GroupTheory.Torsion
/-- For prime `p`, `g` lies in the `p`-primary component iff its order is a power of `p`.  -/
CommMonoid.mem_primaryComponent_iff_orderOf : ∀ {G : Type u_1} [inst : CommMonoid G] {p : ℕ} [Fact (Nat.Prime p)] {g : G},
  g ∈ CommMonoid.primaryComponent G p ↔ ∃ n, orderOf g = p ^ n
-- Init.Data.String.Length
Nat.repeat.eq_2 : ∀ {α : Type u} (f : α → α) (x : α) (n : ℕ), Nat.repeat f n.succ x = f (Nat.repeat f n x)
-- Mathlib.Data.List.Basic
Decidable.List.eq_or_ne_mem_of_mem : ∀ {α : Type u} [DecidableEq α] {a b : α} {l : List α}, a ∈ b :: l → a = b ∨ a ≠ b ∧ a ∈ l
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `b`, the derivative `f'` is nonnegative on `Iio b` and
nonpositive on `Ioo b c`. Then `f` attains its maximum on `Iio c` at `b`.  -/
isMaxOn_Iio_of_deriv : ∀ {f : ℝ → ℝ} {b c : ℝ},
  ContinuousAt f b →
    DifferentiableOn ℝ f (Set.Iio b) →
      DifferentiableOn ℝ f (Set.Ioo b c) →
        (∀ x ∈ Set.Iio b, 0 ≤ deriv f x) → (∀ x ∈ Set.Ioo b c, deriv f x ≤ 0) → IsMaxOn f (Set.Iio c) b
-- Mathlib.Data.Multiset.UnionInter
Multiset.inter_zero : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s ∩ 0 = 0
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.head_nil : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil.head = none
-- Mathlib.GroupTheory.MonoidLocalization.Away
/-- Given `x : M`, `invSelf` is `x⁻¹` in the Localization (as a quotient type) of `M` at the
Submonoid generated by `x`.  -/
Localization.Away.invSelf : {M : Type u_1} → [inst : CommMonoid M] → (x : M) → Localization.Away x
-- Lean.Elab.Import
Lean.Elab.HeaderSyntax.startPos : Lean.Elab.HeaderSyntax → String.Pos.Raw
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.diag_map_fst_snd_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) C]
  {X X' Y Y' : C} (g : X ⟶ Y) (g' : X' ⟶ Y'),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.diag (X ⨯ X'))
      (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst g)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd g')) =
    CategoryTheory.Limits.prod.map g g'
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.ker_completion : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  {f : NormedAddGroupHom G H} {C : ℝ},
  f.SurjectiveOnWith f.range C →
    ↑f.completion.ker = closure ↑(NormedAddCommGroup.toCompl.comp (NormedAddGroupHom.incl f.ker)).range
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.map_ofHom : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f : X ⟶ Y)
  (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) [inst_2 : W.ContainsIdentities],
  (CategoryTheory.MorphismProperty.RightFraction.ofHom W f).map L hL = L.map f
-- Mathlib.Data.Multiset.Dedup
Multiset.Nodup.le_dedup_iff_le : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s.Nodup → (s ≤ t.dedup ↔ s ≤ t)
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.verschiebungFun_coeff : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] (x : WittVector p R) (n : ℕ),
  x.verschiebungFun.coeff n = if n = 0 then 0 else x.coeff (n - 1)
-- Mathlib.Algebra.Order.CompleteField
ConditionallyCompleteLinearOrderedField.coe_inducedOrderRingIso : ∀ (β : Type u_3) (γ : Type u_4) [inst : Field β] [inst_1 : ConditionallyCompleteLinearOrder β]
  [inst_2 : IsStrictOrderedRing β] [inst_3 : Field γ] [inst_4 : ConditionallyCompleteLinearOrder γ]
  [inst_5 : IsStrictOrderedRing γ],
  ⇑(ConditionallyCompleteLinearOrderedField.inducedOrderRingIso β γ) =
    ConditionallyCompleteLinearOrderedField.inducedMap β γ
-- Mathlib.CategoryTheory.FintypeCat
FunctorToFintypeCat.naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F G : CategoryTheory.Functor C FintypeCat) {X Y : C}
  (σ : F ⟶ G) (f : X ⟶ Y) (x : (F.obj X).obj),
  (CategoryTheory.ConcreteCategory.hom (σ.app Y)) ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom (G.map f)) ((CategoryTheory.ConcreteCategory.hom (σ.app X)) x)
-- Mathlib.CategoryTheory.Sites.Canonical
/-- Construct the finest (largest) Grothendieck topology for which all the given presheaves are
sheaves.  -/
CategoryTheory.Sheaf.finestTopology : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    Set (CategoryTheory.Functor Cᵒᵖ (Type w)) → CategoryTheory.GrothendieckTopology C
-- Mathlib.Data.Setoid.Partition
/-- The equivalence classes of the equivalence relation defined by a partition of α equal
the original partition.  -/
Setoid.classes_mkClasses : ∀ {α : Type u_1} (c : Set (Set α)) (hc : Setoid.IsPartition c), (Setoid.mkClasses c ⋯).classes = c
-- Mathlib.Algebra.Order.Group.Indicator
Function.mulSupport_iInf : ∀ {ι : Sort u_1} {α : Type u_2} {M : Type u_3} [inst : One M] [inst_1 : ConditionallyCompleteLattice M] [Nonempty ι]
  (f : ι → α → M), (Function.mulSupport fun x => ⨅ i, f i x) ⊆ ⋃ i, Function.mulSupport (f i)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Consumer : Type → Type
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.snd_intCast : ∀ {q : ℕ} (n : ℤ), (↑n).2 = 0
-- Mathlib.RingTheory.Localization.Rat
Rat.isLocalizationIsInteger_iff : ∀ (q : ℚ), IsLocalization.IsInteger ℤ q ↔ q ∈ Set.range Int.cast
-- Lean.Level
Lean.Level.isIMax : Lean.Level → Bool
-- Mathlib.GroupTheory.Index
AddSubgroup.finiteIndex_normalCore : ∀ {G : Type u_3} [inst : AddGroup G] (H : AddSubgroup G) [h : H.FiniteIndex], H.normalCore.FiniteIndex
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.explore.eq_1 : ∀ {α : Type u} {β : α → Type v} {γ : Type w} [inst : Ord α] (k : α → Ordering) (init : γ)
  (inner : γ → Std.DTreeMap.Internal.Impl.ExplorationStep α β k → γ),
  Std.DTreeMap.Internal.Impl.explore k init inner Std.DTreeMap.Internal.Impl.leaf =
    inner init (Std.DTreeMap.Internal.Impl.ExplorationStep.eq [] Std.DTreeMap.Internal.Cell.empty [])
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffWithinAt_congr : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f f₁ : E → F} {x : E} {n : WithTop ℕ∞},
  (∀ y ∈ s, f₁ y = f y) → f₁ x = f x → (ContDiffWithinAt 𝕜 n f₁ s x ↔ ContDiffWithinAt 𝕜 n f s x)
-- Lean.MetavarContext
Lean.DependsOn.State.mk.inj : ∀ {visited : Lean.ExprSet} {mctx : Lean.MetavarContext} {visited_1 : Lean.ExprSet} {mctx_1 : Lean.MetavarContext},
  { visited := visited, mctx := mctx } = { visited := visited_1, mctx := mctx_1 } → visited = visited_1 ∧ mctx = mctx_1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaAddGrpObjIsoOfRepresentableBy_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (X : C)
  (F : CategoryTheory.Functor Cᵒᵖ AddGrpCat) (α : (F.comp (CategoryTheory.forget AddGrpCat)).RepresentableBy X),
  (CategoryTheory.yonedaAddGrpObjIsoOfRepresentableBy X F α).hom =
    { app := fun X_1 => AddGrpCat.ofHom ↑{ toEquiv := α.homEquiv, map_add' := ⋯ }, naturality := ⋯ }
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.add_apply : ∀ {p : ENNReal} {ι : Type u_2} (β : ι → Type u_4) [inst : (i : ι) → SeminormedAddCommGroup (β i)] (x y : PiLp p β)
  (i : ι), (x + y).ofLp i = x.ofLp i + y.ofLp i
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.lift_surjective_of_surjective : ∀ {R : Type u} [inst : Ring R] (I : Ideal R) {S : Type v} [inst_1 : I.IsTwoSided] [inst_2 : Semiring S] {f : R →+* S}
  (H : ∀ a ∈ I, f a = 0), Function.Surjective ⇑f → Function.Surjective ⇑(Ideal.Quotient.lift I f H)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum : ∀ {A : Type u_1} [inst : NonUnitalNormedRing A] [inst_1 : StarRing A] [inst_2 : NormedSpace ℝ A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : SMulCommClass ℝ A A] [inst_5 : PartialOrder A] [StarOrderedRing A]
  [NonUnitalIsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] (a : A),
  autoParam (0 ≤ a) NonUnitalIsometricContinuousFunctionalCalculus.isGreatest_quasispectrum._auto_1 →
    IsGreatest (quasispectrum NNReal a) ‖a‖₊
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Iic_add_bij : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  Set.BijOn (fun x => x + a) (Set.Iic b) (Set.Iic (b + a))
-- Mathlib.RingTheory.LocalProperties.Basic
/-- Let `I J : Ideal R`. If the localization of `I` at each maximal ideal `P` is equal to
the localization of `J` at `P`, then `I = J`.  -/
Ideal.eq_of_localization_maximal : ∀ {R : Type u_1} [inst : CommSemiring R] {I J : Ideal R},
  (∀ (P : Ideal R) (x : P.IsMaximal),
      Ideal.map (algebraMap R (Localization.AtPrime P)) I = Ideal.map (algebraMap R (Localization.AtPrime P)) J) →
    I = J
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Adjunction.mapAddGrp.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (a : F ⊣ G) [inst_4 : F.Monoidal]
  [inst_5 : G.Monoidal],
  a.mapAddGrp =
    {
      unit :=
        CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapAddGrpIdIso.inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapAddGrpNatTrans a.unit)
            CategoryTheory.Functor.mapAddGrpCompIso.hom),
      counit :=
        CategoryTheory.CategoryStruct.comp CategoryTheory.Functor.mapAddGrpCompIso.inv
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.mapAddGrpNatTrans a.counit)
            CategoryTheory.Functor.mapAddGrpIdIso.hom),
      left_triangle_components := ⋯, right_triangle_components := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.lipschitzWith_starProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], LipschitzWith 1 ⇑K.starProjection
-- Mathlib.MeasureTheory.Function.LpSeminorm.Indicator
MeasureTheory.eLpNorm_indicator_const_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ε : Type u_7} [inst : TopologicalSpace ε]
  [inst_1 : ESeminormedAddMonoid ε] (c : ε) {s : Set α} (p : ENNReal),
  MeasureTheory.eLpNorm (s.indicator fun x => c) p μ ≤ ‖c‖ₑ * μ s ^ (1 / p.toReal)
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.submonoidComap_apply_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] (f : M →* N) (N' : Submonoid N)
  (x : ↥(Submonoid.comap f N')), ↑((f.submonoidComap N') x) = f ↑x
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.comp_map : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C] {D : Type u₃}
  [inst_2 : CategoryTheory.Bicategory D] (F : CategoryTheory.StrictlyUnitaryPseudofunctor B C)
  (G : CategoryTheory.StrictlyUnitaryPseudofunctor C D) {X Y : B} (f : X ⟶ Y), (F.comp G).map f = G.map (F.map f)
-- Mathlib.Algebra.Polynomial.Eval.Coeff
Polynomial.eval₂_C_X : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, Polynomial.eval₂ Polynomial.C Polynomial.X p = p
-- Mathlib.CategoryTheory.Limits.FilteredColimitCommutesProduct
CategoryTheory.Limits.colimitPointwiseProductToProductColimit_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {α : Type u_3} {I : α → Type u_4}
  [inst_2 : (i : α) → CategoryTheory.Category.{u_5, u_4} (I i)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.Discrete α) C]
  (F : (i : α) → CategoryTheory.Functor (I i) (CategoryTheory.Functor D C))
  [inst_4 : ∀ (i : α), CategoryTheory.Limits.HasColimitsOfShape (I i) C]
  [inst_5 : CategoryTheory.Limits.HasColimitsOfShape ((i : α) → I i) C] (d : D),
  (CategoryTheory.Limits.colimitPointwiseProductToProductColimit F).app d =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation (CategoryTheory.Limits.pointwiseProduct F) d).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.HasColimit.isoOfNatIso (CategoryTheory.Limits.pointwiseProductCompEvaluation F d)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.colimitPointwiseProductToProductColimit fun s =>
            (F s).comp ((CategoryTheory.evaluation D C).obj d))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.Pi.mapIso fun x =>
                (CategoryTheory.Limits.colimitObjIsoColimitCompEvaluation (F x) d).symm).hom
            (CategoryTheory.Limits.piObjIso (fun x => CategoryTheory.Limits.colimit (F x)) d).inv)))
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- The end of a functor `F : Jᵒᵖ ⥤ J ⥤ C`.  -/
CategoryTheory.Limits.end_ : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) → [CategoryTheory.Limits.HasEnd F] → C
-- Lean.Elab.InfoTree.Types
Lean.Elab.instInhabitedInfo.default : Lean.Elab.Info
-- Mathlib.Data.Nat.Hyperoperation
hyperoperation_ge_two_eq_self : ∀ (n m : ℕ), hyperoperation (n + 2) m 1 = m
-- ProofWidgets.Compat
ProofWidgets.ExprWithCtx.mk.inj : ∀ {ci : Lean.Elab.ContextInfo} {lctx : Lean.LocalContext} {linsts : Lean.LocalInstances} {expr : Lean.Expr}
  {ci_1 : Lean.Elab.ContextInfo} {lctx_1 : Lean.LocalContext} {linsts_1 : Lean.LocalInstances} {expr_1 : Lean.Expr},
  { ci := ci, lctx := lctx, linsts := linsts, expr := expr } =
      { ci := ci_1, lctx := lctx_1, linsts := linsts_1, expr := expr_1 } →
    ci = ci_1 ∧ lctx = lctx_1 ∧ linsts = linsts_1 ∧ expr = expr_1
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of `Left.one_le_inv_iff`.

---

Uses `left` co(ntra)variant.  -/
one_le_inv' : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulLeftMono α] {a : α}, 1 ≤ a⁻¹ ↔ a ≤ 1
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.anyM.match_1.eq_2 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match false with
    | true => h_1 ()
    | false => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.CStarAlgebra.Classes
NonUnitalCStarAlgebra.toStarModule : ∀ {A : Type u_1} [self : NonUnitalCStarAlgebra A], StarModule ℂ A
-- Aesop.Frontend.Basic
Aesop.Frontend.Parser.Aesop.bool_lit.quot : Lean.ParserDescr
-- Mathlib.CategoryTheory.Sites.Coherent.SheafComparison
CategoryTheory.coherentTopology.instIsCoverDense : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (F : CategoryTheory.Functor C D) [F.EffectivelyEnough]
  [inst_3 : CategoryTheory.Precoherent D], F.IsCoverDense (CategoryTheory.coherentTopology D)
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_singleton_subset_iff : ∀ {α : Type u_1} {s t : Set α} {a : α}, s \ {a} ⊆ t ↔ s ⊆ insert a t
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.LawfulUpwardEnumerable.mk : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α],
  (∀ (a b : α), Std.PRange.UpwardEnumerable.LT a b → a ≠ b) →
    (∀ (a : α), Std.PRange.succMany? 0 a = some a) →
      (∀ (n : ℕ) (a : α), Std.PRange.succMany? (n + 1) a = (Std.PRange.succMany? n a).bind Std.PRange.succ?) →
        Std.PRange.LawfulUpwardEnumerable α
-- Mathlib.Computability.Partrec
Computable.option_some : ∀ {α : Type u_1} [inst : Primcodable α], Computable some
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropOn_of_mem_maximalAtlas : ∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {e : OpenPartialHomeomorph M H} {Q : (H → H) → Set H → H → Prop},
  G.LocalInvariantProp G Q →
    (∀ (y : H), Q id Set.univ y) → e ∈ StructureGroupoid.maximalAtlas M G → ChartedSpace.LiftPropOn Q (↑e) e.source
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.instIsEmptySubtypeMemBotOfConstants : ∀ (L : FirstOrder.Language) (M : Type w) [inst : L.Structure M] [IsEmpty L.Constants], IsEmpty ↥⊥
-- Lean.Parser.Term
Lean.Parser.Term.optSemicolon : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Topology.MetricSpace.Holder
HolderOnWith.of_le_of_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {r : NNReal} {f : X → Y}
  {C₁ C₂ s t : NNReal} {A : Set X},
  HolderOnWith C₁ r f A → HolderOnWith C₂ s f A → r ≤ t → t ≤ s → HolderOnWith (max C₁ C₂) t f A
-- Mathlib.Order.Defs.LinearOrder
le_or_gt : ∀ {α : Type u_1} [inst : LinearOrder α] (a b : α), a ≤ b ∨ b < a
-- Mathlib.Topology.Continuous
/-- A surjective map has dense range.  -/
Function.Surjective.denseRange : ∀ {X : Type u_1} [inst : TopologicalSpace X] {α : Type u_4} {f : α → X}, Function.Surjective f → DenseRange f
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
/-- Notation for `actionAssocIso`, the structural isomorphism
`- ⊙ᵣ (- ⊗ -) ≅ (- ⊙ᵣ -) ⊙ᵣ -`.  -/
CategoryTheory.MonoidalCategory.MonoidalRightAction.termαᵣ : Lean.ParserDescr
-- Mathlib.Computability.TuringDegree
/-- If a function is recursive in a constant partial function, then it is partial recursive.  -/
TuringReducible.partrec_of_const : ∀ {f : ℕ →. ℕ} {s : Part ℕ}, (TuringReducible f fun x => s) → Partrec f
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_insertIfNew_le_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {km kmi : α}, t.minKey? = some km → (t.insertIfNew k v).minKey?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Mathlib.Geometry.Convex.Cone.TensorProduct
/-- The minimal tensor product of two cones is given by all conical combinations of elementary
tensor products `x ⊗ₜ y` with `x ∈ C₁` and `y ∈ C₂`.  -/
PointedCone.minTensorProduct : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : LinearOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        {G : Type u_2} →
          [inst_3 : AddCommGroup G] →
            [inst_4 : Module R G] →
              {H : Type u_3} →
                [inst_5 : AddCommGroup H] →
                  [inst_6 : Module R H] → PointedCone R G → PointedCone R H → PointedCone R (TensorProduct R G H)
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpoly_map_eq_charpoly : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup L]
  [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] (φ : L →ₗ[R] Module.End R M)
  [inst_5 : Fintype ι] [inst_6 : DecidableEq ι] [inst_7 : Module.Free R M] [inst_8 : Module.Finite R M]
  (b : Module.Basis ι R L) (x : L),
  Polynomial.map (MvPolynomial.eval ⇑(b.repr x)) (φ.polyCharpoly b) = LinearMap.charpoly (φ x)
-- Mathlib.Data.Set.Image
Set.image_comp_image : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {g : β → γ}, Set.image g ∘ Set.image f = Set.image (g ∘ f)