mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instCommSemigroup.eq_1 : ∀ {α : Type u_1} [inst : CommSemigroup α],
  OrderDual.instCommSemigroup = { toSemigroup := OrderDual.instSemigroup, mul_comm := ⋯ }
-- Mathlib.Topology.Sheaves.Presheaf
/-- The pushforward functor.  -/
TopCat.Presheaf.pushforward : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : TopCat} → (X ⟶ Y) → CategoryTheory.Functor (TopCat.Presheaf C X) (TopCat.Presheaf C Y)
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.BoundedFormula.freeVarFinset.eq_5 : ∀ {L : FirstOrder.Language} {α : Type u'} [inst : DecidableEq α] (x : ℕ) (f : L.BoundedFormula α (x + 1)),
  f.all.freeVarFinset = f.freeVarFinset
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.linkAux_size : ∀ {self : Array Batteries.UFNode} {x y : Fin self.size}, (Batteries.UnionFind.linkAux self x y).size = self.size
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for the left whiskering `whiskerLeftIso f η`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂Iso.whiskerLeftM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂Iso m] →
    Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂Iso
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Mono
CategoryTheory.Limits.pullback_snd_iso_of_right_factors_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Z : C} (f : X ⟶ Z) (i : Z ⟶ W)
  [inst_1 : CategoryTheory.Mono i],
  CategoryTheory.IsIso (CategoryTheory.Limits.pullback.snd i (CategoryTheory.CategoryStruct.comp f i))
-- Mathlib.Topology.Subpath
Path.subpath.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) (t₀ t₁ : ↑unitInterval),
  γ.subpath t₀ t₁ = { toFun := ⇑γ ∘ Set.Icc.convexComb t₀ t₁, continuous_toFun := ⋯, source' := ⋯, target' := ⋯ }
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- The zero acts trivially.  -/
CategoryTheory.AddModObj.zero_vadd_assoc : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {M : C} {inst_4 : CategoryTheory.AddMonObj M} (X : D) [self : CategoryTheory.AddModObj M X] {Z : D} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft CategoryTheory.AddMonObj.zero X)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom h
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Mapping from variables to their disequalities. We say a disequality constraint `c` is a disequality for a variable `x`
if `x` is the maximal variable in `c`.
 -/
Lean.Meta.Grind.Arith.Linear.Struct.diseqs : Lean.Meta.Grind.Arith.Linear.Struct → Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Linear.DiseqCnstr)
-- Mathlib.Data.Set.Finite.Lattice
Set.map_finite_iSup : ∀ {α : Type u} {β : Type v} {F : Type u_1} {ι : Type u_2} [inst : CompleteLattice α] [inst_1 : CompleteLattice β]
  [inst_2 : FunLike F α β] [SupBotHomClass F α β] [Finite ι] (f : F) (g : ι → α), f (⨆ i, g i) = ⨆ i, f (g i)
-- Mathlib.Order.Notation
/-- The supremum/join operation: `x ⊔ y`. It is notation for `max x y`
and should be used when the type is not a linear order.


Conventions for notations in identifiers:

 * The recommended spelling of `⊔` in identifiers is `sup`. -/
«term_⊔_» : Lean.TrailingParserDescr
-- Std.Time.Format.Modifier
Std.Time.Modifier.z.injEq : ∀ (presentation presentation_1 : Std.Time.ZoneName),
  (Std.Time.Modifier.z presentation = Std.Time.Modifier.z presentation_1) = (presentation = presentation_1)
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.continuousOn_Ioc : ∀ {f : ℝ → ℝ} {y z : ℝ}, ConcaveOn ℝ (Set.Ioc y z) f → ContinuousWithinAt f (Set.Iic z) z → ContinuousOn f (Set.Ioc y z)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
/-- We say that a 1-morphism `h` commutes with the left Kan lift `f₊ g` if the whiskered left lift
for `f₊ g` by `h` is a Kan lift of `h ≫ g` along `f`.  -/
CategoryTheory.Bicategory.LanLift.CommuteWith : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} → (f : b ⟶ a) → (g : c ⟶ a) → [CategoryTheory.Bicategory.HasLeftKanLift f g] → {x : B} → (x ⟶ c) → Prop
-- Init.Data.List.Sublist
List.suffix_cons_append : ∀ {α : Type u_1} {a : α} {l₁ l₂ : List α}, l₂ <:+ a :: (l₁ ++ l₂)
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.isSubDPIdeal_sup : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} {hI : DividedPowers I} {J K : Ideal A},
  hI.IsSubDPIdeal J → hI.IsSubDPIdeal K → hI.IsSubDPIdeal (J ⊔ K)
-- Mathlib.Analysis.Normed.Module.Basic
/-- Produces a `PseudoEMetricSpace E` instance from a `SeminormedSpace.Core`. Note that
if this is used to define an instance on a type, it also provides a new uniformity and
topology on the type. See note [reducible non-instances].  -/
PseudoEMetricSpace.ofSeminormedSpaceCore : {𝕜 : Type u_6} →
  {E : Type u_7} →
    [inst : NormedField 𝕜] →
      [inst_1 : AddCommGroup E] →
        [inst_2 : Norm E] → [inst_3 : Module 𝕜 E] → SeminormedSpace.Core 𝕜 E → PseudoEMetricSpace E
-- Init.Data.List.Lemmas
List.isEqv.eq_def : ∀ {α : Type u} (x x_1 : List α) (x_2 : α → α → Bool),
  x.isEqv x_1 x_2 =
    match x, x_1, x_2 with
    | [], [], x => true
    | a :: as, b :: bs, eqv => eqv a b && as.isEqv bs eqv
    | x, x_3, x_4 => false
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.equalizerSubobject_arrow_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobject f g).arrow f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizerSubobject f g).arrow g
-- Mathlib.AlgebraicGeometry.Morphisms.FiniteType
/-- **Alias** of `AlgebraicGeometry.Scheme.Hom.finiteType_appLE`.

---

**Alias** of `AlgebraicGeometry.LocallyOfFiniteType.finiteType_appLE`. -/
AlgebraicGeometry.LocallyOfFiniteType.finiteType_of_affine_subset : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.LocallyOfFiniteType f] {U : Y.Opens},
  AlgebraicGeometry.IsAffineOpen U →
    ∀ {V : X.Opens},
      AlgebraicGeometry.IsAffineOpen V →
        ∀ (e : V ≤ (TopologicalSpace.Opens.map f.base).obj U),
          (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appLE f U V e)).FiniteType
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_int_mul_pi_sub : ∀ (x : ℝ) (n : ℤ), Real.sin (↑n * Real.pi - x) = -((-1) ^ n * Real.sin x)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
one_le_tprod : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {g : ι → α}, (∀ (i : ι), 1 ≤ g i) → 1 ≤ ∏'[L] (i : ι), g i
-- Lean.Meta.Tactic.FVarSubst
Lean.Expr.applyFVarSubst : Lean.Meta.FVarSubst → Lean.Expr → Lean.Expr
-- Mathlib.Analysis.Normed.Operator.Bilinear
LinearMap.mkContinuous₂_norm_le' : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {𝕜₃ : Type u_3} {E : Type u_4} {F : Type u_6} {G : Type u_8}
  [inst : SeminormedAddCommGroup E] [inst_1 : SeminormedAddCommGroup F] [inst_2 : SeminormedAddCommGroup G]
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NontriviallyNormedField 𝕜₂] [inst_5 : NontriviallyNormedField 𝕜₃]
  [inst_6 : NormedSpace 𝕜 E] [inst_7 : NormedSpace 𝕜₂ F] [inst_8 : NormedSpace 𝕜₃ G] {σ₂₃ : 𝕜₂ →+* 𝕜₃} {σ₁₃ : 𝕜 →+* 𝕜₃}
  [inst_9 : RingHomIsometric σ₂₃] (f : E →ₛₗ[σ₁₃] F →ₛₗ[σ₂₃] G) {C : ℝ}
  (hC : ∀ (x : E) (y : F), ‖(f x) y‖ ≤ C * ‖x‖ * ‖y‖), ‖f.mkContinuous₂ C hC‖ ≤ max C 0
-- Mathlib.Data.Set.Prod
/-- A function is `Function.const α a` for some `a` if and only if `∀ x y, f x = f y`.  -/
Set.range_const_eq_diagonal : ∀ {α : Type u_1} {β : Type u_2} [hβ : Nonempty β], Set.range (Function.const α) = {f | ∀ (x y : α), f x = f y}
-- Init.Data.Range.Polymorphic.PRange
Std.Rio.mk : {α : Type u} → α → Std.Rio α
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.Cowedge.IsColimit.π_desc : ∀ {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)} {c : CategoryTheory.Limits.Cowedge F}
  (hc : CategoryTheory.Limits.IsColimit c) {X : C} (f : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ X)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp ((F.map g.op).app i) (f i) =
        CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j))
  (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Multicofork.π c j)
      (CategoryTheory.Limits.Cowedge.IsColimit.desc hc f hf) =
    f j
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.unitsSMulGroup_snd : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (d : HNNExtension.NormalWord.TransversalPair G A B)
  (u : ℤˣ) (g : G), (HNNExtension.NormalWord.unitsSMulGroup φ d u g).2 = (⋯.equiv g).2
-- Init.Data.UInt.Lemmas
UInt64.toUSize_lt : ∀ {a b : UInt64}, a.toUSize < b.toUSize ↔ a % UInt64.ofNat USize.size < b % UInt64.ofNat USize.size
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.LocalPredicate.mk.injEq : ∀ {X : TopCat} {T : ↑X → Type u_1} (toPrelocalPredicate : TopCat.PrelocalPredicate T)
  (locality :
    ∀ {U : TopologicalSpace.Opens ↑X} (f : (x : ↥U) → T ↑x),
      (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, toPrelocalPredicate.pred fun x => f (i x)) → toPrelocalPredicate.pred f)
  (toPrelocalPredicate_1 : TopCat.PrelocalPredicate T)
  (locality_1 :
    ∀ {U : TopologicalSpace.Opens ↑X} (f : (x : ↥U) → T ↑x),
      (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, toPrelocalPredicate_1.pred fun x => f (i x)) →
        toPrelocalPredicate_1.pred f),
  ({ toPrelocalPredicate := toPrelocalPredicate, locality := locality } =
      { toPrelocalPredicate := toPrelocalPredicate_1, locality := locality_1 }) =
    (toPrelocalPredicate = toPrelocalPredicate_1)
-- Init.Data.List.Lemmas
List.foldr_reverse : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β → β} {b : β},
  List.foldr f b l.reverse = List.foldl (fun x y => f y x) b l
-- Init.Prelude
instDecidableEqNat : DecidableEq ℕ
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- The canonical projection from `AutGalois F` to the `C`-automorphism group of each
pointed Galois object.  -/
CategoryTheory.PreGaloisCategory.AutGalois.π : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      (F : CategoryTheory.Functor C FintypeCat) →
        (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) →
          CategoryTheory.PreGaloisCategory.AutGalois F →* CategoryTheory.Aut A.obj
-- Mathlib.Topology.Constructions
OrderDual.instNeBotNhdsWithinIoi : ∀ {X : Type u} [inst : TopologicalSpace X] [inst_1 : Preorder X] {x : X} [(nhdsWithin x (Set.Iio x)).NeBot],
  (nhdsWithin (OrderDual.toDual x) (Set.Ioi (OrderDual.toDual x))).NeBot
-- Mathlib.Data.Sum.Lattice
Sum.Lex.instSemilatticeSup : {α : Type u_1} → {β : Type u_2} → [SemilatticeSup α] → [SemilatticeSup β] → SemilatticeSup (α ⊕ₗ β)
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
OrderMonoidWithZeroHom.toOrderMonoidHom_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : MulZeroOneClass α]
  [inst_3 : MulZeroOneClass β], Function.Injective OrderMonoidWithZeroHom.toOrderMonoidHom
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.ofList_equiv_foldl : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {l : List (α × β)},
  (Std.DTreeMap.Const.ofList l cmp).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) ∅ l)
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.vec2_dotProduct' : ∀ {α : Type u} [inst : AddCommMonoid α] [inst_1 : Mul α] {a₀ a₁ b₀ b₁ : α}, ![a₀, a₁] ⬝ᵥ ![b₀, b₁] = a₀ * b₀ + a₁ * b₁
-- Mathlib.Algebra.Homology.BifunctorHomotopy
/-- Auxiliary definition for `mapBifunctorMapHomotopy₁`.  -/
HomologicalComplex.mapBifunctorMapHomotopy.hom₁ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D : Type u_3} →
      {I₁ : Type u_4} →
        {I₂ : Type u_5} →
          {J : Type u_6} →
            [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} D] →
                  [inst_3 : CategoryTheory.Preadditive C₁] →
                    [inst_4 : CategoryTheory.Preadditive C₂] →
                      [inst_5 : CategoryTheory.Preadditive D] →
                        {c₁ : ComplexShape I₁} →
                          {c₂ : ComplexShape I₂} →
                            {K₁ L₁ : HomologicalComplex C₁ c₁} →
                              {f₁ f₁' : K₁ ⟶ L₁} →
                                Homotopy f₁ f₁' →
                                  {K₂ L₂ : HomologicalComplex C₂ c₂} →
                                    (K₂ ⟶ L₂) →
                                      (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) →
                                        [inst_6 : F.Additive] →
                                          [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] →
                                            (c : ComplexShape J) →
                                              [inst_8 : DecidableEq J] →
                                                [inst_9 : TotalComplexShape c₁ c₂ c] →
                                                  [inst_10 : K₁.HasMapBifunctor K₂ F c] →
                                                    [inst_11 : L₁.HasMapBifunctor L₂ F c] →
                                                      (j j' : J) →
                                                        (K₁.mapBifunctor K₂ F c).X j ⟶ (L₁.mapBifunctor L₂ F c).X j'
-- Std.Data.DTreeMap.Internal.Model
/-- Model implementation of the `contains` function.
Internal implementation detail of the tree map
 -/
Std.DTreeMap.Internal.Impl.containsₘ : {α : Type u} → {β : α → Type v} → [Ord α] → Std.DTreeMap.Internal.Impl α β → α → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- Given a fork over `∏ᶜ I.left ⇉ ∏ᶜ I.right`, we may obtain a multifork.  -/
CategoryTheory.Limits.Multifork.ofPiFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      {I : CategoryTheory.Limits.MulticospanIndex J C} →
        {c : CategoryTheory.Limits.Fan I.left} →
          {d : CategoryTheory.Limits.Fan I.right} →
            {hd : CategoryTheory.Limits.IsLimit d} →
              CategoryTheory.Limits.Fork (I.fstPiMapOfIsLimit c hd) (I.sndPiMapOfIsLimit c hd) →
                CategoryTheory.Limits.Multifork I
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.preimage_basicOpen : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) {U : TopologicalSpace.Opens ↑Y.toTopCat}
  (s : ↑(Y.presheaf.obj (Opposite.op U))),
  (TopologicalSpace.Opens.map f.base).obj (Y.toRingedSpace.basicOpen s) =
    X.toRingedSpace.basicOpen ((CategoryTheory.ConcreteCategory.hom (f.c.app (Opposite.op U))) s)
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.replaceF_eq_replaceFTR.go : ∀ (α : Type u_1) (p : α → Option α) (acc : Array α) (xs : List α),
  List.replaceFTR.go p xs acc = acc.toList ++ List.replaceF p xs
-- Mathlib.Combinatorics.Matroid.Circuit
Matroid.Indep.mem_fundCircuit_iff : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} {e x : α},
  M.Indep I → e ∈ M.closure I → e ∉ I → (x ∈ M.fundCircuit e I ↔ M.Indep (insert e I \ {x}))
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.not_mem_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → k ∉ m₁ \ m₂
-- Lean.Elab.Binders
/-- Elaborate the given binders (i.e., `Syntax` objects for `bracketedBinder`),
update the local context, set of local instances, reset instance cache (if needed), and then
execute `k` with the updated context.
The local context will only be included inside `k`.

For example, suppose you have binders `[(a : α), (b : β a)]`, then the elaborator will
create two new free variables `a` and `b`, push these to the context and pass to `k #[a,b]`.
 -/
Lean.Elab.Term.elabBinders : {α : Type} → Array Lean.Syntax → (Array Lean.Expr → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Mathlib.Analysis.Meromorphic.Divisor
/-- If orders are finite, the divisor of a product of meromorphic functions is the sum of the divisors.
 -/
MeromorphicOn.divisor_fun_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {ι : Type u_3} {s : Finset ι} {f : ι → 𝕜 → 𝕜},
  (∀ i ∈ s, MeromorphicOn (f i) U) →
    (∀ i ∈ s, ∀ z ∈ U, meromorphicOrderAt (f i) z ≠ ⊤) →
      MeromorphicOn.divisor (fun x => ∏ i ∈ s, f i x) U = ∑ i ∈ s, MeromorphicOn.divisor (f i) U
-- Mathlib.GroupTheory.Nilpotent
/-- The nilpotency class of a nilpotent `G` is equal to the length of the lower
central series.  -/
AddSubgroup.lowerCentralSeries_length_eq_nilpotencyClass : ∀ {G : Type u_1} [inst : AddGroup G] [hG : AddGroup.IsNilpotent G], Nat.find ⋯ = AddGroup.nilpotencyClass G
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.const_toFun : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R] (ι : Type u_7) [inst_2 : Finite ι]
  (x : HahnSeries Γ R) (x_1 : ι), (HahnSeries.SummableFamily.const ι x) x_1 = x
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The bundled monoid giving the filtered colimit of a diagram.  -/
MonCat.FilteredColimits.colimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → CategoryTheory.Functor J MonCat → [CategoryTheory.IsFiltered J] → MonCat
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcompose₂ObjMkIso_hom_right_app : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [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]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (G : CategoryTheory.Functor H D') {F' : CategoryTheory.Functor D H} (α : F ⟶ L.comp F') (X : D),
  (CategoryTheory.Functor.LeftExtension.postcompose₂ObjMkIso G α).hom.right.app X =
    CategoryTheory.CategoryStruct.id (G.obj (F'.obj X))
-- Mathlib.LinearAlgebra.Finsupp.VectorSpace
/-- The direct sum of free modules is free.

Note that while this is stated for `DFinsupp` not `DirectSum`, the types are defeq.  -/
DFinsupp.basis : {ι : Type u_1} →
  {R : Type u_2} →
    {M : ι → Type u_3} →
      [inst : Semiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] →
            {η : ι → Type u_4} →
              ((i : ι) → Module.Basis (η i) R (M i)) → Module.Basis ((i : ι) × η i) R (Π₀ (i : ι), M i)
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.MorphismProperty.IsCardinalForSmallObjectArgument.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I I_1 : CategoryTheory.MorphismProperty C),
  I = I_1 →
    ∀ (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType],
      I.IsCardinalForSmallObjectArgument κ = I_1.IsCardinalForSmallObjectArgument κ
-- Mathlib.Algebra.Notation.Prod
Prod.smul_mk : ∀ {E : Type u_8} {α : Type u_9} {β : Type u_10} [inst : SMul E α] [inst_1 : SMul E β] (c : E) (a : α) (b : β),
  c • (a, b) = (c • a, c • b)
-- Mathlib.RingTheory.SimpleModule.Basic
IsSemisimpleModule.sup : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p q : Submodule R M},
  IsSemisimpleModule R ↥p → IsSemisimpleModule R ↥q → IsSemisimpleModule R ↥(p ⊔ q)
-- Mathlib.Data.Fintype.Inv
Fintype.leftInverse_bijInv : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] {f : α → β} (f_bij : Function.Bijective f),
  Function.LeftInverse (Fintype.bijInv f_bij) f
-- Mathlib.Topology.Inseparable
IsClosed.not_inseparable : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X} {s : Set X}, IsClosed s → x ∈ s → y ∉ s → ¬Inseparable x y
-- Init.Data.List.Lemmas
List.intercalate_cons_of_ne_nil : ∀ {α : Type u_1} {ys l : List α} {zs : List (List α)}, zs ≠ [] → ys.intercalate (l :: zs) = l ++ ys ++ ys.intercalate zs
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.hasZeroObject : CategoryTheory.Limits.HasZeroObject SemiNormedGrp₁
-- Init.Data.Array.Range
Array.range_succ_eq_map : ∀ {n : ℕ}, Array.range (n + 1) = #[0] ++ Array.map Nat.succ (Array.range n)
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.mulRight.eq_1 : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulRightMono α] (a : α),
  OrderIso.mulRight a = { toEquiv := Equiv.mulRight a, map_rel_iff' := ⋯ }
-- Mathlib.Order.CompleteLattice.Basic
Equiv.iSup_comp : ∀ {α : Type u_1} {ι : Sort u_4} {ι' : Sort u_5} [inst : SupSet α] {g : ι' → α} (e : ι ≃ ι'), ⨆ x, g (e x) = ⨆ y, g y
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_union_right : ∀ {α : Type u_1} [inst : PartialOrder α] {a : α}, Set.Iio a ∪ {a} = Set.Iic a
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.map_ι₁_mapHomologicalComplexObjIso_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (F : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel] {D : Type u_3}
  [inst_3 : CategoryTheory.Category.{v_2, u_3} D] [inst_4 : CategoryTheory.Preadditive D]
  (H : CategoryTheory.Functor C D) [inst_5 : H.Additive]
  [inst_6 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (F.X i) (F.X i)]
  [inst_7 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F) (-CategoryTheory.CategoryStruct.id F))]
  [inst_8 :
    ∀ (i : ι),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i)
        (((H.mapHomologicalComplex c).obj F).X i)]
  [inst_9 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F))
        (-CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F)))]
  [inst_10 :
    HomologicalComplex.HasHomotopyCofiber
      ((H.mapHomologicalComplex c).map
        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F) (-CategoryTheory.CategoryStruct.id F)))]
  (hc : ∀ (j : ι), ∃ i, c.Rel i j) {Z : HomologicalComplex D c} (h : ((H.mapHomologicalComplex c).obj F).cylinder ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((H.mapHomologicalComplex c).map (HomologicalComplex.cylinder.ι₁ F))
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.mapHomologicalComplexObjIso F H hc).hom h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.cylinder.ι₁ ((H.mapHomologicalComplex c).obj F)) h
-- Mathlib.Order.Filter.CountablyGenerated
Filter.HasAntitoneBasis.hasBasis_ge : ∀ {α : Type u_1} {ι : Type u_4} [inst : Preorder ι] [IsDirectedOrder ι] {l : Filter α} {s : ι → Set α},
  l.HasAntitoneBasis s → ∀ (i : ι), l.HasBasis (fun j => i ≤ j) s
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.toSubmodule_comap : ∀ {R : Type u} {L : Type v} {M : Type w} {M' : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : Module R M] [inst_4 : LieRingModule L M] [inst_5 : AddCommGroup M']
  [inst_6 : Module R M'] [inst_7 : LieRingModule L M'] (f : M →ₗ⁅R,L⁆ M') (N' : LieSubmodule R L M'),
  ↑(LieSubmodule.comap f N') = Submodule.comap ↑f ↑N'
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.eq_zero_of_absolutelyContinuous_of_mutuallySingular : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → μ.MutuallySingular ν → μ = 0