mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Int.Linear
Int.Internal.Linear.le_of_le_cert.induct_unfolding : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Bool → Prop),
  (∀ (k : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly) (k_1 : ℤ),
      motive (Int.Internal.Linear.Poly.add k v p) (Int.Internal.Linear.Poly.num k_1) false) →
    (∀ (k k_1 : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
        motive (Int.Internal.Linear.Poly.num k) (Int.Internal.Linear.Poly.add k_1 v p) false) →
      (∀ (c₁ c₂ : ℤ), motive (Int.Internal.Linear.Poly.num c₁) (Int.Internal.Linear.Poly.num c₂) (decide (c₁ ≥ c₂))) →
        (∀ (a₁ : ℤ) (x₁ : Int.Internal.Linear.Var) (p₁ : Int.Internal.Linear.Poly) (a₂ : ℤ)
            (x₂ : Int.Internal.Linear.Var) (p₂ : Int.Internal.Linear.Poly),
            motive p₁ p₂ (Int.Internal.Linear.le_of_le_cert p₁ p₂) →
              motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂)
                (a₁ == a₂ && x₁ == x₂ && Int.Internal.Linear.le_of_le_cert p₁ p₂)) →
          ∀ (p₁ p₂ : Int.Internal.Linear.Poly), motive p₁ p₂ (Int.Internal.Linear.le_of_le_cert p₁ p₂)
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- The logarithmic derivative converts products into sums: away from a codiscrete subset of `𝕜`, the
logarithmic derivative of a product of two meromorphic functions is the sum of the logarithmic
derivatives.
 -/
Meromorphic.logDeriv_mul_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f g : 𝕜 → 𝕜'},
  Meromorphic f →
    Meromorphic g →
      (∀ (x : 𝕜), meromorphicOrderAt f x ≠ ⊤) →
        (∀ (x : 𝕜), meromorphicOrderAt g x ≠ ⊤) → logDeriv (f * g) =ᶠ[Filter.codiscrete 𝕜] logDeriv f + logDeriv g
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.isIso_iff_isIso_of_isIso : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {W X Y Z : T} {f : W ⟶ X} {g : Y ⟶ Z}
  (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) [CategoryTheory.IsIso sq],
  CategoryTheory.IsIso f ↔ CategoryTheory.IsIso g
-- Batteries.Data.List.Basic
List.dropSlice_eq_dropSliceTR : @List.dropSlice = @List.dropSliceTR
-- Init.Data.Option.Monadic
Option.forM_map : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_4} [inst : Monad m] [LawfulMonad m] (o : Option α) (g : α → β)
  (f : β → m PUnit.{u_1 + 1}), forM (Option.map g o) f = forM o fun a => f (g a)
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : a ⟶ c)
  [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g] {x : B} (h : c ⟶ x)
  [inst_2 : CategoryTheory.Bicategory.Lan.CommuteWith f g h],
  (CategoryTheory.Bicategory.Lan.CommuteWith.lanCompIso f g h).inv =
    (CategoryTheory.Bicategory.Lan.CommuteWith.isKan f g h).desc
      (CategoryTheory.Bicategory.lanLeftExtension f (CategoryTheory.CategoryStruct.comp g h))
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.ceil_ofNat : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] [IsStrictOrderedRing R] (n : ℕ)
  [inst_4 : n.AtLeastTwo], ⌈OfNat.ofNat n⌉₊ = OfNat.ofNat n
-- Init.System.FilePath
_private.Init.System.FilePath.0.System.FilePath.posOfLastSep : (p : System.FilePath) → Option p.toString.Pos
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.instNontrivial : ∀ {α : Type u_1} [inst : TopologicalSpace α] [Nontrivial α], Nontrivial (TopologicalSpace.NonemptyCompacts α)
-- Mathlib.Algebra.Order.Hom.Basic
MulRingNormClass.mk : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} [inst : NonAssocRing α] [inst_1 : Semiring β]
  [inst_2 : PartialOrder β] [inst_3 : FunLike F α β] [toMulRingSeminormClass : MulRingSeminormClass F α β],
  (∀ (f : F) {a : α}, f a = 0 → a = 0) → MulRingNormClass F α β
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.isCancelMul : ∀ {M : Type u_1} {N : Type u_2} [inst : CommMonoid M] {S : Submonoid M} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) [IsCancelMul M], IsCancelMul N
-- Mathlib.Data.Fintype.Option
/-- A recursor principle for finite types, analogous to `Nat.rec`. It effectively says
that every `Fintype` is either `Empty` or `Option α`, up to an `Equiv`.  -/
Fintype.truncRecEmptyOption : {P : Type u → Sort v} →
  ({α β : Type u} → α ≃ β → P α → P β) →
    P PEmpty.{u + 1} →
      ({α : Type u} → [Fintype α] → [DecidableEq α] → P α → P (Option α)) →
        (α : Type u) → [Fintype α] → [DecidableEq α] → Trunc (P α)
-- Mathlib.Logic.Encodable.Basic
Encodable.encode_prod_val : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Encodable β] (a : α) (b : β),
  Encodable.encode (a, b) = Nat.pair (Encodable.encode a) (Encodable.encode b)
-- Mathlib.Logic.Basic
Exists.snd : ∀ {b : Prop} {p : b → Prop} (h : Exists p), p ⋯
-- Mathlib.Logic.Relator
Relator.RightTotal.rel_forall : ∀ {α : Sort u₁} {β : Sort u₂} {R : α → β → Prop},
  Relator.RightTotal R →
    Relator.LiftFun (Relator.LiftFun R fun x1 x2 => ∀ (a : x1), x2) (fun x1 x2 => ∀ (a : x1), x2)
      (fun p => (i : α) → p i) fun q => ∀ (i : β), q i
-- Mathlib.Algebra.Order.GroupWithZero.Defs
posMulMono_iff : ∀ (α : Type u_1) [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α],
  PosMulMono α ↔ ∀ ⦃a : α⦄, 0 ≤ a → ∀ ⦃b c : α⦄, b ≤ c → a * b ≤ a * c
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.range_coe : ∀ {α : Type u} {β : Type u_1} [inst : UniformSpace α] [inst_1 : UniformSpace β] (h : α ≃ᵤ β), Set.range ⇑h = Set.univ
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.prod : ∀ {α : Type u_1} {β : Type u_2} {la : Filter α} {lb : Filter β} {ι : Type u_6} {ι' : Type u_7} {pa : ι → Prop}
  {sa : ι → Set α} {pb : ι' → Prop} {sb : ι' → Set β},
  la.HasBasis pa sa → lb.HasBasis pb sb → (la ×ˢ lb).HasBasis (fun i => pa i.1 ∧ pb i.2) fun i => sa i.1 ×ˢ sb i.2
-- Mathlib.Data.Sum.Basic
Function.Injective.sumElim : ∀ {α : Type u} {β : Type v} {γ : Sort u_3} {f : α → γ} {g : β → γ},
  Function.Injective f → Function.Injective g → (∀ (a : α) (b : β), f a ≠ g b) → Function.Injective (Sum.elim f g)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM0to1.tr.eq_3 : ∀ {Γ : Type u_1} {Λ : Type u_2} [inst : Inhabited Λ] (M : Turing.TM0.Machine Γ Λ) (a : Γ) (q : Λ),
  Turing.TM0to1.tr M (Turing.TM0to1.Λ'.act (Turing.TM0.Stmt.write a) q) =
    Turing.TM1.Stmt.write (fun x x_1 => a) (Turing.TM1.Stmt.goto fun x x_1 => Turing.TM0to1.Λ'.normal q)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.toFun_eq_coe : ∀ {E : Type u_3} [inst : AddGroup E] {p : AddGroupSeminorm E}, p.toFun = ⇑p
-- Std.Time.Duration
/-- Adds a `Second.Offset` to a `Duration`
 -/
Std.Time.Duration.addSeconds : Std.Time.Duration → Std.Time.Second.Offset → Std.Time.Duration
-- Mathlib.Data.Seq.Computation
Computation.liftRelAux_inr_inl : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {C : Computation α → Computation β → Prop} {b : β} {ca : Computation α},
  Computation.LiftRelAux R C (Sum.inr ca) (Sum.inl b) = ∃ a ∈ ca, R a b
-- Mathlib.Algebra.Group.Defs
DivInvOneMonoid.inv_one : ∀ {G : Type u_2} [self : DivInvOneMonoid G], 1⁻¹ = 1
-- Mathlib.RingTheory.ClassGroup.Basic
/-- `ClassGroup.mk0` factors through the canonical quotient projection on
`(FractionalIdeal R⁰ (FractionRing R))ˣ`.  -/
ClassGroup.mk0_eq_quotientMk : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDedekindDomain R]
  (I : ↥(nonZeroDivisors (Ideal R))), ClassGroup.mk0 I = ↑((FractionalIdeal.mk0 (FractionRing R)) I)
-- Mathlib.Topology.Order.Bornology
BddAbove.isBounded_inter : ∀ {α : Type u_1} {s t : Set α} [inst : Bornology α] [inst_1 : Preorder α] [IsOrderBornology α],
  BddAbove s → BddBelow t → Bornology.IsBounded (s ∩ t)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsLEObjTruncGE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (X : C) (a b : ℤ) [t.IsLE X b],
  t.IsLE ((t.truncGE a).obj X) b
-- Mathlib.Algebra.Algebra.Hom
AlgHom.cancel_left : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type u₁} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  {g₁ g₂ : A →ₐ[R] B} {f : B →ₐ[R] C}, Function.Injective ⇑f → (f.comp g₁ = f.comp g₂ ↔ g₁ = g₂)
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The span of `x` in `M` is isomorphic to `R` quotiented by the torsion ideal of `x`.  -/
Ideal.quotTorsionOfEquivSpanSingleton : (R : Type u_1) →
  (M : Type u_2) →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (x : M) → (R ⧸ Ideal.torsionOf R M x) ≃ₗ[R] ↥(R ∙ x)
-- Aesop.Search.Queue
Aesop.LIFOQueue : Type
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.Hom.ext' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {G : CategoryTheory.Comonad C} (X Y : G.Coalgebra)
  (f g : X ⟶ Y), f.f = g.f → f = g
-- Mathlib.Order.Category.BddDistLat
BoundedLatticeHom.mk.congr_simp : ∀ {α : Type u_6} {β : Type u_7} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (toLatticeHom toLatticeHom_1 : LatticeHom α β)
  (e_toLatticeHom : toLatticeHom = toLatticeHom_1) (map_top' : toLatticeHom.toFun ⊤ = ⊤)
  (map_bot' : toLatticeHom.toFun ⊥ = ⊥),
  { toLatticeHom := toLatticeHom, map_top' := map_top', map_bot' := map_bot' } =
    { toLatticeHom := toLatticeHom_1, map_top' := ⋯, map_bot' := ⋯ }
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.isLocal_of_isIso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.IsIso f], P.isLocal f
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- An isomorphism of graphs induces an equivalence of edge sets.  -/
SimpleGraph.Iso.mapEdgeSet : {V : Type u_1} → {W : Type u_2} → {G : SimpleGraph V} → {G' : SimpleGraph W} → G ≃g G' → ↑G.edgeSet ≃ ↑G'.edgeSet
-- Mathlib.GroupTheory.NoncommCoprod
/-- Variant of `MonoidHom.noncommCoprod_apply` with the product written in the other direction.  -/
MonoidHom.noncommCoprod_apply' : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) (mn : M × N),
  (f.noncommCoprod g comm) mn = g mn.2 * f mn.1
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.inverseImage_monomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  (CategoryTheory.MorphismProperty.monomorphisms D).inverseImage L = P.monoModSerre
-- Batteries.Data.Fin.Fold
Fin.dfoldlM_succ : ∀ {m : Type u_1 → Type u_2} {n : ℕ} {α : Fin (n + 1 + 1) → Type u_1} [inst : Monad m]
  (f : (i : Fin (n + 1)) → α i.castSucc → m (α i.succ)) (x : α 0),
  Fin.dfoldlM (n + 1) α f x = do
    let x ← f 0 x
    Fin.dfoldlM n (α ∘ Fin.succ) (fun x1 x2 => f x1.succ x2) x
-- Mathlib.Data.Set.List
Set.range_list_getI : ∀ {α : Type u_1} [inst : Inhabited α] (l : List α), Set.range l.getI = insert default {x | x ∈ l}
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- The braiding isomorphism which swaps a binary product.  -/
CategoryTheory.Limits.prod.braiding : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (P Q : C) →
      [inst_1 : CategoryTheory.Limits.HasBinaryProduct P Q] →
        [inst_2 : CategoryTheory.Limits.HasBinaryProduct Q P] → P ⨯ Q ≅ Q ⨯ P
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `LE.le.sdiff_ssubset_of_nonempty`. -/
HasSubset.Subset.diff_ssubset_of_nonempty : ∀ {α : Type u_1} {s t : Set α}, s ⊆ t → s.Nonempty → t \ s ⊂ t
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.smul_apply : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} {V : Type u_4} {α : Type u_5} [inst : PartialOrder Γ]
  [inst_1 : PartialOrder Γ'] [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid R] [inst_4 : SMulWithZero R V]
  [inst_5 : VAdd Γ Γ'] [inst_6 : IsOrderedCancelVAdd Γ Γ'] {x : HahnSeries Γ R} {s : HahnSeries.SummableFamily Γ' V α}
  {a : α}, (x • s) a = (HahnModule.of R).symm (x • (HahnModule.of R) (s a))
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a normed group from a multiplication-invariant pseudodistance.  -/
NormedCommGroup.ofMulDist' : {E : Type u_5} →
  [inst : Norm E] →
    [inst_1 : CommGroup E] →
      [inst_2 : MetricSpace E] →
        (∀ (x : E), ‖x‖ = dist 1 x) → (∀ (x y z : E), dist (z * x) (z * y) ≤ dist x y) → NormedCommGroup E
-- Mathlib.GroupTheory.Focal
/-- Lemma: H* is a normal subgroup of H.  -/
Subgroup.instNormalSubtypeMemFocalSubgroupOf : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), H.focalSubgroupOf.Normal
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The natural functor from `Fintype` to `LightProfinite`, endowing a finite type with the
discrete topology.  -/
FintypeCat.toLightProfinite : CategoryTheory.Functor FintypeCat LightProfinite
-- Mathlib.Algebra.Homology.HomotopyCategory.Triangulated
CochainComplex.mappingConeCompTriangleh_comm₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {X₁ X₂ X₃ : CochainComplex C ℤ} (f : X₁ ⟶ X₂) (g : X₂ ⟶ X₃)
  {Z : HomotopyCategory C (ComplexShape.up ℤ)}
  (h :
    (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj
        (CochainComplex.mappingCone (CochainComplex.mappingConeCompTriangle f g).mor₁) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CochainComplex.mappingConeCompTriangleh f g).mor₂
      (CategoryTheory.CategoryStruct.comp
        ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map (CochainComplex.mappingConeCompHomotopyEquiv f g).hom)
        h) =
    CategoryTheory.CategoryStruct.comp
      ((HomotopyCategory.quotient C (ComplexShape.up ℤ)).map
        (CochainComplex.mappingCone.inr (CochainComplex.mappingConeCompTriangle f g).mor₁))
      h
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
/-- `IsEffective` is true for any `R`-algebra `S` having an `R`-algebra section of
`Algebra.ofId _ _ : R →ₐ[R] S`.  -/
Algebra.IsEffective.of_section : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : Ring S] [inst_2 : Algebra R S] (g : S →ₐ[R] R),
  Algebra.IsEffective R S
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Break.runK.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((a : α) → motive (some a)) → (Unit → motive none) → motive x
-- Mathlib.Data.Matrix.Basis
Matrix.liftLinear_comp_singleLinearMap : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_5} (S : Type u_6) {α : Type u_7} {β : Type u_8} [inst : DecidableEq m]
  [inst_1 : DecidableEq n] [inst_2 : Fintype m] [inst_3 : Fintype n] [inst_4 : Semiring R] [inst_5 : Semiring S]
  [inst_6 : AddCommMonoid α] [inst_7 : AddCommMonoid β] [inst_8 : Module R α] [inst_9 : Module R β]
  [inst_10 : Module S β] [inst_11 : SMulCommClass R S β] (f : m → n → α →ₗ[R] β) (i : m) (j : n),
  (Matrix.liftLinear S) f ∘ₗ Matrix.singleLinearMap R i j = f i j
-- Init.Data.SInt.Bitwise
ISize.toInt16_not : ∀ (a : ISize), (~~~a).toInt16 = ~~~a.toInt16
-- Mathlib.Order.Category.LinOrd
LinOrd.ext : ∀ {X Y : LinOrd} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.instCoeOutEquiv : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {V₁ : Type u_6} →
        {V₂ : Type u_7} →
          [inst : Ring k] →
            [inst_1 : AddCommGroup V₁] →
              [inst_2 : AddCommGroup V₂] →
                [inst_3 : Module k V₁] →
                  [inst_4 : Module k V₂] →
                    [inst_5 : AddTorsor V₁ P₁] → [inst_6 : AddTorsor V₂ P₂] → CoeOut (P₁ ≃ᵃ[k] P₂) (P₁ ≃ P₂)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCones.conePoints_map : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  {F : CategoryTheory.Functor J (CategoryTheory.Functor K C)} (D : CategoryTheory.Limits.DiagramOfCones F) {X Y : J}
  (f : X ⟶ Y), D.conePoints.map f = (D.map f).hom
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.instInhabitedColimitType : {J : Type u_1} →
  [inst : CategoryTheory.Category.{u_2, u_1} J] →
    (F : CategoryTheory.Functor J MonCat) → Inhabited (MonCat.Colimits.ColimitType F)
-- Std.Do.Triple.SpecLemmas
List.Cursor.current.eq_1 : ∀ {α : Type u_1} {l : List α} (c : l.Cursor) (h : 0 < c.suffix.length), c.current h = c.suffix[0]
-- Mathlib.LinearAlgebra.Center
/-- Over a domain `R`, an endomorphism `f` of a free module `V`
of rank ≠ 1 such that `f v` and `v` are collinear, for all `v : V`,
consists of homotheties with central ratio.

When `R` does not satisfy `StrongRankCondition`, use
`LinearMap.exists_mem_center_apply_eq_smul_of_basis`.

When `finrank R V = 1`, up to a linear equivalence `V ≃ₗ[R] R`,
then any `f` is *right*-multiplication by some `a : R`,
but not necessarily *left*-multiplication by an element of the center of `R`.  -/
LinearMap.exists_mem_center_apply_eq_smul_of_forall_notLinearIndependent : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [IsDomain R] [StrongRankCondition R] [inst_3 : AddCommGroup V]
  [inst_4 : Module R V] [Module.Free R V] {f : V →ₗ[R] V},
  Module.finrank R V ≠ 1 → (∀ (v : V), ¬LinearIndependent R ![v, f v]) → ∃ a, f = a • 1
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Limits.Cofork.IsColimit.desc'.congr_simp : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} {s : CategoryTheory.Limits.Cofork f g}
  (hs hs_1 : CategoryTheory.Limits.IsColimit s),
  hs = hs_1 →
    ∀ {W : C} (k : Y ⟶ W) (h : CategoryTheory.CategoryStruct.comp f k = CategoryTheory.CategoryStruct.comp g k),
      CategoryTheory.Limits.Cofork.IsColimit.desc' hs k h = CategoryTheory.Limits.Cofork.IsColimit.desc' hs_1 k h
-- Mathlib.Algebra.Polynomial.Div
Polynomial.modByMonic_eq_sub_mul_div : ∀ {R : Type u} [inst : Ring R] (p q : Polynomial R), p %ₘ q = p - q * (p /ₘ q)
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.MsgEmbed.brecOn_3.go : {motive_1 : Lean.Widget.MsgEmbed → Sort u} →
  {motive_2 : Lean.Widget.TaggedText Lean.Widget.MsgEmbed → Sort u} →
    {motive_3 :
        Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
            (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren) →
          Sort u} →
      {motive_4 : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u} →
        {motive_5 : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Sort u} →
          (t : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) →
            ((t : Lean.Widget.MsgEmbed) → t.below → motive_1 t) →
              ((t : Lean.Widget.TaggedText Lean.Widget.MsgEmbed) → Lean.Widget.MsgEmbed.below_1 t → motive_2 t) →
                ((t :
                      Lean.Widget.StrictOrLazy (Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed))
                        (Lean.Server.WithRpcRef Lean.Widget.LazyTraceChildren)) →
                    Lean.Widget.MsgEmbed.below_2 t → motive_3 t) →
                  ((t : Array (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) →
                      Lean.Widget.MsgEmbed.below_3 t → motive_4 t) →
                    ((t : List (Lean.Widget.TaggedText Lean.Widget.MsgEmbed)) →
                        Lean.Widget.MsgEmbed.below_4 t → motive_5 t) →
                      motive_4 t ×' Lean.Widget.MsgEmbed.below_3 t
-- Init.Data.Prod
/-- Composing a `Prod.map` with another `Prod.map` is equal to
a single `Prod.map` of composed functions.
 -/
Prod.map_comp_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {ε : Type u_5} {ζ : Type u_6} (f : α → β) (f' : γ → δ)
  (g : β → ε) (g' : δ → ζ), Prod.map g g' ∘ Prod.map f f' = Prod.map (g ∘ f) (g' ∘ f')
-- Mathlib.Data.Ineq
Mathlib.instReprIneq : Repr Mathlib.Ineq
-- Mathlib.Algebra.Group.Shrink
Shrink.instAdd : {α : Type u_2} → [inst : Small.{v, u_2} α] → [Add α] → Add (Shrink.{v, u_2} α)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabel : Type
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.coe_copy : ∀ {M : Type u_4} {N : Type u_5} {x : Zero M} {x_1 : Zero N} (f : ZeroHom M N) (f' : M → N) (h : f' = ⇑f),
  ⇑(f.copy f' h) = f'
-- Mathlib.Analysis.Fourier.FourierTransform
Real.fourier_continuousMultilinearMap_apply : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  {ι : Type u_4} [inst_7 : Fintype ι] {M : ι → Type u_5} [inst_8 : (i : ι) → NormedAddCommGroup (M i)]
  [inst_9 : (i : ι) → NormedSpace ℝ (M i)] {f : V → ContinuousMultilinearMap ℝ M E} {m : (i : ι) → M i} {v : V},
  MeasureTheory.Integrable f MeasureTheory.volume →
    (FourierTransform.fourier f v) m = FourierTransform.fourier (fun x => (f x) m) v
-- Mathlib.Data.Set.Lattice
/-- **Alias** of `Set.iUnion_ofPred`. -/
Set.iUnion_setOf : ∀ {α : Type u_1} {ι : Sort u_5} (P : ι → α → Prop), ⋃ i, {x | P i x} = {x | ∃ i, P i x}
-- Init.Data.String.Pattern.String
String.Slice.Pattern.ForwardSliceSearcher.startsWith : String.Slice → String.Slice → Bool
-- Mathlib.Geometry.Euclidean.Simplex
Affine.Simplex.Equilateral.angle_eq_pi_div_three : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} {s : Affine.Simplex ℝ P n},
  s.Equilateral →
    ∀ {i₁ i₂ i₃ : Fin (n + 1)},
      i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → EuclideanGeometry.angle (s.points i₁) (s.points i₂) (s.points i₃) = Real.pi / 3
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
summable_of_absolute_convergence_real : ∀ {f : ℕ → ℝ}, (∃ r, Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, |f i|) Filter.atTop (nhds r)) → Summable f
-- Lean.Elab.ConfigEval.DeriveEvalConfigItem
/-- The `EvalConfigItemHandlerKind.exact` handler for this trie position's key.  -/
_private.Lean.Elab.ConfigEval.DeriveEvalConfigItem.0.Lean.Elab.ConfigEval.HandlerTrie.exact? : Lean.Elab.ConfigEval.HandlerTrie✝ → Option Lean.Elab.ConfigEval.EvalConfigItemHandler
-- Mathlib.Tactic.ClickSuggestions.Util
/-- The information required for pasting a suggestion into the editor.  -/
Mathlib.Tactic.ClickSuggestions.Context : Type
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct
LinearMap.BilinForm.tmul.eq_1 : ∀ {R : Type uR} {A : Type uA} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Algebra R A] [inst_5 : Module R M₁]
  [inst_6 : Module A M₁] [inst_7 : SMulCommClass R A M₁] [inst_8 : IsScalarTower R A M₁] [inst_9 : Module R M₂]
  (B₁ : LinearMap.BilinForm A M₁) (B₂ : LinearMap.BilinMap R M₂ R),
  B₁.tmul B₂ = (LinearMap.BilinForm.tensorDistrib R A) (B₁ ⊗ₜ[R] B₂)
-- Std.Do.Triple.SpecLemmas
List.Cursor.tail.congr_simp : ∀ {α : Type u_1} {l : List α} (s s_1 : l.Cursor) (e_s : s = s_1) (h : 0 < s.suffix.length), s.tail h = s_1.tail ⋯
-- Mathlib.CategoryTheory.NatIso
/-- The functor constructed with `copyObj` is isomorphic to the given functor.  -/
CategoryTheory.Functor.isoCopyObj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → (obj : C → D) → (e : (X : C) → F.obj X ≅ obj X) → F ≅ F.copyObj obj e