mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Lie.Abelian
/-- The largest submodule of a Lie module `M` on which the Lie algebra `L` acts trivially.  -/
LieModule.maxTrivSubmodule : (R : Type u) →
  (L : Type v) →
    (M : Type w) →
      [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] → [LieModule R L M] → LieSubmodule R L M
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_map_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) {X Y : CategoryTheory.MorphismProperty.Comma L R₁ P Q W} (f : X ⟶ Y),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).functor.map f).left =
    (CategoryTheory.MorphismProperty.Comma.Hom.hom f).left
-- Mathlib.Topology.UnitInterval
unitInterval.subtype_Iio_eq_Ico : ∀ (x : ↑unitInterval), Subtype.val ⁻¹' Set.Iio ↑x = Set.Ico 0 x
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.eval_polynomialY : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P : Fin 3 → R),
  (MvPolynomial.eval P) W'.polynomialY = 2 * P 1 + W'.a₁ * P 0 * P 2 + W'.a₃ * P 2 ^ 3
-- Mathlib.Topology.Defs.Basic
/-- A set is clopen if it is both closed and open.  -/
IsClopen : {X : Type u} → [TopologicalSpace X] → Set X → Prop
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {x y : E.Hom F},
  x = y ↔
    x.s₀ = y.s₀ ∧
      x.h₀ ≍ y.h₀ ∧
        @CategoryTheory.PreOneHypercover.Hom.s₁ C inst S E F x ≍
            @CategoryTheory.PreOneHypercover.Hom.s₁ C inst S E F y ∧
          @CategoryTheory.PreOneHypercover.Hom.h₁ C inst S E F x ≍
            @CategoryTheory.PreOneHypercover.Hom.h₁ C inst S E F y
-- Std.Time.Time.Unit.Millisecond
/-- `Offset` represents a duration offset in milliseconds.
 -/
Std.Time.Millisecond.Offset : Type
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMapₛₗ₂_apply_basis : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {N₂ : Type u_10} {n : Type u_11} {m : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : AddCommMonoid N₂] [inst_6 : Module R N₂] {σ₁ : R →+* R} [inst_7 : Fintype n]
  [inst_8 : Fintype m] [inst_9 : DecidableEq m] [inst_10 : DecidableEq n] (b₁ : Module.Basis n R M₁)
  (b₂ : Module.Basis m R M₂) (M : Matrix n m N₂) (i : n) (j : m),
  (((Matrix.toLinearMapₛₗ₂ σ₁ b₁ b₂) M) (b₁ i)) (b₂ j) = M i j
-- Mathlib.LinearAlgebra.Basis.Basic
/-- If `M` is a subsingleton and `ι` is empty, this is the unique `ι`-indexed basis for `M`.  -/
Module.Basis.empty : {ι : Type u_1} →
  {R : Type u_3} →
    (M : Type u_5) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → [Subsingleton M] → [IsEmpty ι] → Module.Basis ι R M
-- Batteries.Data.AssocList
Batteries.AssocList.forM_eq : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [inst : Monad m] (f : α → β → m PUnit.{u_1 + 1})
  (l : Batteries.AssocList α β),
  Batteries.AssocList.forM f l =
    l.toList.forM fun x =>
      match x with
      | (a, b) => f a b
-- Mathlib.Probability.UniformOn
ProbabilityTheory.finite_of_uniformOn_ne_zero : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] {s t : Set Ω}, (ProbabilityTheory.uniformOn s) t ≠ 0 → s.Finite
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceRErase.eq_1 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (hrb_2 hrb_4 : Std.DTreeMap.Internal.Impl.leaf.Balanced)
  (hlr_3 :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond Std.DTreeMap.Internal.Impl.leaf.size
      Std.DTreeMap.Internal.Impl.leaf.size),
  Std.DTreeMap.Internal.Impl.balanceRErase k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf hrb_2
      hrb_4 hlr_3 =
    Std.DTreeMap.Internal.Impl.inner 1 k v Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf
-- Mathlib.FieldTheory.LinearDisjoint
/-- If there exists an `F`-basis of `L` which remains linearly independent over `A`, then
`A` and `L` are linearly disjoint.  -/
IntermediateField.LinearDisjoint.of_basis_right' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E]
  {ι : Type u_1} (b : Module.Basis ι F L), LinearIndependent (↥A) (⇑(algebraMap L E) ∘ ⇑b) → A.LinearDisjoint L
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Comon_
CategoryTheory.comonEquiv_functor : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.comonEquiv.functor = CategoryTheory.Comon.forget C
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
Commute.cfcAbs_cfcAbs : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] {a b : A},
  Commute a b → Commute a (star b) → Commute (CFC.abs a) (CFC.abs b)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getKey?_unitOfList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.ExtDHashMap.Const.unitOfList l).getKey? k' = some k
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Cardinal.lift_iSup_lt_of_lt_cof_ord : ∀ {β : Type v} {f : β → Cardinal.{u}} {a : Cardinal.{u}},
  Cardinal.lift.{u, v} (Cardinal.mk β) < (Cardinal.lift.{v, u} a).ord.cof → (∀ (i : β), f i < a) → ⨆ i, f i < a
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.ext : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} {x y : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂},
  x.h₀ = y.h₀ → x.h₁ = y.h₁ → x.h₂ = y.h₂ → x.h₃ = y.h₃ → x = y
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.Regular.comap : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α] [BorelSpace α]
  {mβ : MeasurableSpace β} [inst_3 : TopologicalSpace β] [BorelSpace β] (μ : MeasureTheory.Measure β) [μ.Regular]
  (f : α ≃ₜ β), (MeasureTheory.Measure.comap (⇑f) μ).Regular
-- Mathlib.Geometry.Manifold.GroupLieAlgebra
mdifferentiableAt_addInvariantVectorField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G]
  [inst_7 : LieAddGroup I (minSmoothness 𝕜 3) G] (v : AddGroupLieAlgebra I G) {g : G},
  (MDiffAt fun g => ⟨g, addInvariantVectorField v g⟩) g
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_hom_app_shift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X : Cᵒᵖ) (n : ℤ),
  (CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app
      ((CategoryTheory.shiftFunctor Cᵒᵖ n).obj X) =
    (CategoryTheory.shiftFunctor Cᵒᵖ n).map
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).unitIso.inv.app X)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The composition of `C^n` functions at points in domains is `C^n`,
with a weaker condition on `s` and `t`.  -/
ContDiffWithinAt.comp_of_preimage_mem_nhdsWithin_of_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : F → G}
  {f : E → F} {y : F} (x : E),
  ContDiffWithinAt 𝕜 n g t y →
    ContDiffWithinAt 𝕜 n f s x → f ⁻¹' t ∈ nhdsWithin x s → f x = y → ContDiffWithinAt 𝕜 n (g ∘ f) s x
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.weakEquivalence_toHoCat_map_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.CofibrantObject C} (f : X ⟶ Y),
  HomotopicalAlgebra.WeakEquivalence (HomotopicalAlgebra.CofibrantObject.toHoCat.map f) ↔
    HomotopicalAlgebra.WeakEquivalence f
-- Mathlib.CategoryTheory.Sites.Sheafification
/-- The canonical map from `P` to its sheafification, as a natural transformation.  -/
CategoryTheory.toSheafification : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (D : Type u_1) →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_2 : CategoryTheory.HasWeakSheafify J D] →
            CategoryTheory.Functor.id (CategoryTheory.Functor Cᵒᵖ D) ⟶ CategoryTheory.sheafification J D
-- Mathlib.Data.PNat.Basic
PNat.mul_div_exact : ∀ {m k : ℕ+}, k ∣ m → k * m.divExact k = m
-- Mathlib.Data.Setoid.Partition
/-- Interpreting an element of `Partitions α` as a set of sets.  -/
Setoid.Partitions.toSet : {α : Type u_1} → Setoid.Partitions α → Set (Set α)
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Convert the tree to a list in ascending order.  -/
RBTree.RBMap.toList : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → List (α × β)
-- Mathlib.CategoryTheory.Abelian.RightDerived
CategoryTheory.InjectiveResolution.toRightDerivedZero'_comp_iCycles : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D] [inst_1 : CategoryTheory.Abelian D] {C : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_2, u_2} C] [inst_3 : CategoryTheory.Abelian C] {X : C}
  (P : CategoryTheory.InjectiveResolution X) (F : CategoryTheory.Functor C D) [inst_4 : F.Additive],
  CategoryTheory.CategoryStruct.comp (P.toRightDerivedZero' F)
      (((F.mapHomologicalComplex (ComplexShape.up ℕ)).obj P.cocomplex).iCycles 0) =
    F.map (P.ι.f 0)
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.id₂_iso_inv : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} {x : a ⟶ b},
  (CategoryTheory.CategoryStruct.id x).iso.inv = CategoryTheory.CategoryStruct.id x.of
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.instIsRepresentableObjFunctorOppositeTypeShrinkYoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] (X : C),
  (CategoryTheory.shrinkYoneda.{w, v, u}.obj X).IsRepresentable
-- Qq.MetaM
Qq.MaybeLevelDefEq.notDefEq : {u v : Lean.Level} → Qq.MaybeLevelDefEq u v
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_union_of_not_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF →
    (↑m₂).WF →
      (∀ (a : α), m₁.contains a = true → m₂.contains a = false) → (↑(m₁.union m₂)).size = (↑m₁).size + (↑m₂).size
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∉ t₂ → (t₁ ∩ t₂)[k]! = default
-- Mathlib.Data.Finsupp.Weight
Finsupp.NonTorsionWeight.mk : ∀ {σ : Type u_1} {M : Type u_2} {R : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {w : σ → M}, (∀ {r : R} {s : σ}, r • w s = 0 → r = 0) → Finsupp.NonTorsionWeight R w
-- Mathlib.Data.Finset.Option
Option.toFinset_some : ∀ {α : Type u_1} {a : α}, (some a).toFinset = {a}
-- Init.Data.BitVec.Bitblast
BitVec.neg_toInt_neg_umod_eq_of_msb_true_msb_true : ∀ {w : ℕ} {x y : BitVec w}, x.msb = true → y.msb = true → -(-(-x % -y)).toInt = ↑(-x % -y).toNat
-- Mathlib.Topology.Algebra.InfiniteSum.Order
HasProd.one_le : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {g : ι → α} {a : α} [L.NeBot],
  (∀ (i : ι), 1 ≤ g i) → HasProd g a L → 1 ≤ a
-- Mathlib.RepresentationTheory.Intertwining
/-- Intertwining maps from `ρ` to itself are the same as `A[G]`-linear endomorphisms.  -/
Representation.IntertwiningMap.equivAlgEnd : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommSemiring A] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommMonoid V] →
            [inst_3 : Module A V] →
              (ρ : Representation A G V) → ρ.IntertwiningMap ρ ≃ₐ[A] Module.End (MonoidAlgebra A G) ρ.asModule
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, t.toList.isEmpty = t.isEmpty
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.free_obj_A : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (T : CategoryTheory.Monad C) (X : C),
  (T.free.obj X).A = T.obj X
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.seq : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] {α β : Type u}
  {x : m (α → β)} {y : m α} {Q : Std.Do.PostCond β ps},
  ⦃(Std.Do.wp x).apply (fun f => (Std.Do.wp y).apply (fun a => Q.1 (f a), Q.2), Q.2)⦄ (x <*> y) ⦃Q⦄
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insert_eq_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {p : α × β},
  insert p t = t.insert p.1 p.2
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The structure isomorphism of a `CatCommSqOver` as a natural transformation.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.e : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A B) →
              (G : CategoryTheory.Functor C B) →
                (X : Type u₄) →
                  [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                    (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.fstFunctor F G X).comp
                        ((CategoryTheory.Functor.whiskeringRight X A B).obj F) ≅
                      (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.sndFunctor F G X).comp
                        ((CategoryTheory.Functor.whiskeringRight X C B).obj G)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The short complex `A --d₀₁--> Fun(G, A) --d₁₂--> Fun(G × G, A)` is isomorphic to the 1st
short complex associated to the complex of inhomogeneous cochains of `A`.  -/
groupCohomology.isoShortComplexH1 : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        HomologicalComplex.sc (groupCohomology.inhomogeneousCochains A) 1 ≅ groupCohomology.shortComplexH1 A
-- Mathlib.Topology.Constructions
/-- The induced homeomorphism between two equal subtypes of a given topological space:
the underlying equivalence is `Equiv.subtypeEquivProp`.  -/
Homeomorph.ofEqSubtypes : {X : Type u} → [inst : TopologicalSpace X] → {p q : X → Prop} → p = q → Subtype p ≃ₜ Subtype q
-- Init.Data.UInt.Bitwise
Bool.toUInt32.eq_1 : ∀ (b : Bool), b.toUInt32 = if b = true then 1 else 0
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rco_eq_singleton_append_iff : ∀ {xs : Array ℤ} {m n a : ℤ}, (m...n).toArray = #[a] ++ xs ↔ m = a ∧ m < n ∧ ((m + 1)...n).toArray = xs
-- Mathlib.CategoryTheory.Monad.Limits
/-- (Impl)
Define the map `λ : TL ⟶ L`, which will serve as the structure of the coalgebra on `L`, and
we will show is the colimiting object. We use the cocone constructed by `c` and the fact that
`T` preserves colimits to produce this morphism.
 -/
CategoryTheory.Monad.ForgetCreatesColimits.lambda : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Monad C} →
      {J : Type u} →
        [inst_1 : CategoryTheory.Category.{v, u} J] →
          {D : CategoryTheory.Functor J T.Algebra} →
            (c : CategoryTheory.Limits.Cocone (D.comp T.forget)) →
              CategoryTheory.Limits.IsColimit c →
                [CategoryTheory.Limits.PreservesColimit (D.comp T.forget) T.toFunctor] → (T.mapCocone c).pt ⟶ c.pt
-- Mathlib.LinearAlgebra.CliffordAlgebra.Conjugation
CliffordAlgebra.evenOdd_comap_involute : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (n : ZMod 2),
  Submodule.comap CliffordAlgebra.involute.toLinearMap (CliffordAlgebra.evenOdd Q n) = CliffordAlgebra.evenOdd Q n
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.sub_le_self : ∀ (a b : Ordinal.{u_4}), a - b ≤ a
-- Mathlib.Tactic.TermCongr
/-- A generator for an `Eq lhs rhs` or `HEq lhs rhs` proof.
If such a proof is impossible, the generator can throw an error.
The inferred type of the generated proof needs only be defeq to `Eq lhs rhs` or `HEq lhs rhs`.
This function can assign metavariables when constructing the proof.

If `pf? = none`, then `lhs` and `rhs` are defeq, and the proof is by reflexivity.  -/
Mathlib.Tactic.TermCongr.CongrResult.pf? : Mathlib.Tactic.TermCongr.CongrResult → Option (Mathlib.Tactic.TermCongr.CongrType → Lean.MetaM Lean.Expr)
-- Init.Data.UInt.Lemmas
USize.toUInt32_le : ∀ {a b : USize}, a.toUInt32 ≤ b.toUInt32 ↔ a % 4294967296 ≤ b % 4294967296
-- Mathlib.Topology.Instances.NNReal.Lemmas
Real.tendsto_toNNReal_atTop_iff : ∀ {α : Type u_2} {l : Filter α} {f : α → ℝ},
  Filter.Tendsto (fun x => (f x).toNNReal) l Filter.atTop ↔ Filter.Tendsto f l Filter.atTop
-- Init.Grind.Order
Lean.Grind.Order.le_of_offset_eq_2_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b : α} {k : ℤ}, a = b + ↑k → b ≤ a + ↑(-k)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.linearEquiv_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] (S : Type u_5) [inst_8 : Semiring S]
  [inst_9 : Module S F] [inst_10 : SMulCommClass 𝕜₂ S F] [inst_11 : ContinuousConstSMul S F]
  [inst_12 : IsTopologicalAddGroup F] (a : E →SWOT[σ] F), (ContinuousLinearMapWOT.linearEquiv S) a = a.toCLM
-- Mathlib.Data.Fin.Tuple.Reflection
FinVec.Exists.eq_1 : ∀ {α : Type u_1} (P : (Fin 0 → α) → Prop), FinVec.Exists P = P ![]
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
/-- The univariate polynomials `preΨₙ` for `n ∈ ℤ`, which are auxiliary to the bivariate polynomials
`Ψₙ` congruent to the bivariate `n`-division polynomials `ψₙ`.  -/
WeierstrassCurve.preΨ : {R : Type r} → [inst : CommRing R] → WeierstrassCurve R → ℤ → Polynomial R
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ker_eq_bot_iff : ∀ {G : Type u_1} [inst : Group G] {M : Type u_7} [inst_1 : MulOneClass M] (f : G →* M),
  f.ker = ⊥ ↔ Function.Injective ⇑f
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.withNext : {α : Type} → Lean.Expr → (Lean.Expr → Lean.Expr → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Data.Fintype.EquivFin
Sum.infinite_of_right : ∀ {α : Type u_1} {β : Type u_2} [Infinite β], Infinite (α ⊕ β)
-- Mathlib.Analysis.Convex.BetweenList
List.Wbtw.eq_1 : ∀ (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] (l : List P), List.Wbtw R l = List.Triplewise (Wbtw R) l
-- Mathlib.Data.Set.Prod
Set.InjOn.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Set α),
  Set.InjOn f s = ∀ ⦃x₁ : α⦄, x₁ ∈ s → ∀ ⦃x₂ : α⦄, x₂ ∈ s → f x₁ = f x₂ → x₁ = x₂
-- Mathlib.Topology.Category.CompHausLike.SigmaComparison
CompHausLike.sigmaComparison_eq_comp_isos : ∀ {P : TopCat → Prop} [inst : CompHausLike.HasExplicitFiniteCoproducts P]
  (X : CategoryTheory.Functor (CompHausLike P)ᵒᵖ (Type (max u w)))
  [inst_1 : CategoryTheory.Limits.PreservesFiniteProducts X] {α : Type u} [inst_2 : Finite α] (σ : α → Type u)
  [inst_3 : (a : α) → TopologicalSpace (σ a)] [inst_4 : ∀ (a : α), CompactSpace (σ a)]
  [inst_5 : ∀ (a : α), T2Space (σ a)] [inst_6 : ∀ (a : α), CompHausLike.HasProp P (σ a)],
  CompHausLike.sigmaComparison X σ =
    CategoryTheory.CategoryStruct.comp
      (X.mapIso
          (CategoryTheory.Limits.opCoproductIsoProduct'
            (CompHausLike.finiteCoproduct.isColimit fun a => CompHausLike.of P (σ a))
            (CategoryTheory.Limits.productIsProduct fun x => Opposite.op (CompHausLike.of P (σ x))))).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.PreservesProduct.iso X fun a => Opposite.op (CompHausLike.of P (σ a))).hom
        (CategoryTheory.Limits.Types.productIso fun a => X.obj (Opposite.op (CompHausLike.of P (σ a)))).hom)
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sieves : (X : C) → Set (CategoryTheory.Sieve X))
  (top_mem' : ∀ (X : C), ⊤ ∈ sieves X)
  (pullback_stable' :
    ∀ ⦃X Y : C⦄ ⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X), S ∈ sieves X → CategoryTheory.Sieve.pullback f S ∈ sieves Y)
  (transitive' :
    ∀ ⦃X : C⦄ ⦃S : CategoryTheory.Sieve X⦄,
      S ∈ sieves X →
        ∀ (R : CategoryTheory.Sieve X),
          (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ sieves Y) → R ∈ sieves X)
  (sieves_1 : (X : C) → Set (CategoryTheory.Sieve X)) (top_mem'_1 : ∀ (X : C), ⊤ ∈ sieves_1 X)
  (pullback_stable'_1 :
    ∀ ⦃X Y : C⦄ ⦃S : CategoryTheory.Sieve X⦄ (f : Y ⟶ X),
      S ∈ sieves_1 X → CategoryTheory.Sieve.pullback f S ∈ sieves_1 Y)
  (transitive'_1 :
    ∀ ⦃X : C⦄ ⦃S : CategoryTheory.Sieve X⦄,
      S ∈ sieves_1 X →
        ∀ (R : CategoryTheory.Sieve X),
          (∀ ⦃Y : C⦄ ⦃f : Y ⟶ X⦄, S.arrows f → CategoryTheory.Sieve.pullback f R ∈ sieves_1 Y) → R ∈ sieves_1 X),
  ({ sieves := sieves, top_mem' := top_mem', pullback_stable' := pullback_stable', transitive' := transitive' } =
      { sieves := sieves_1, top_mem' := top_mem'_1, pullback_stable' := pullback_stable'_1,
        transitive' := transitive'_1 }) =
    (sieves = sieves_1)
-- Mathlib.Topology.Defs.Filter
/-- Every point of a weakly locally compact space admits a compact neighborhood.  -/
WeaklyLocallyCompactSpace.exists_compact_mem_nhds : ∀ {X : Type u_3} {inst : TopologicalSpace X} [self : WeaklyLocallyCompactSpace X] (x : X), ∃ s, IsCompact s ∧ s ∈ nhds x
-- Mathlib.FieldTheory.KummerExtension
adjoinRootXPowSubCEquiv_symm_eq_root : ∀ {K : Type u} [inst : Field K] {n : ℕ} (hζ : (primitiveRoots n K).Nonempty) {a : K}
  (H : Irreducible (Polynomial.X ^ n - Polynomial.C a)) {L : Type u_1} [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Polynomial.IsSplittingField K L (Polynomial.X ^ n - Polynomial.C a)] {α : L}
  (hα : α ^ n = (algebraMap K L) a),
  (adjoinRootXPowSubCEquiv hζ H hα).symm α = AdjoinRoot.root (Polynomial.X ^ n - Polynomial.C a)