mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.RelSeries
RelSeries.cons_length : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (newHead : α) (rel : (newHead, p.head) ∈ r),
  (p.cons newHead rel).length = p.length + 1
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.ofSubmodule_sSup : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] (s : Set (Submodule R E)),
  ↑(sSup s) = sSup (PointedCone.ofSubmodule '' s)
-- Init.Data.List.MapIdx
List.mapFinIdx_eq_cons_iff' : ∀ {α : Type u_1} {β : Type u_2} {l₂ : List β} {l : List α} {b : β} {f : (i : ℕ) → α → i < l.length → β},
  l.mapFinIdx f = b :: l₂ ↔
    (l.head?.pbind fun x m => some (f 0 x ⋯)) = some b ∧
      Option.map
          (fun x =>
            match x with
            | ⟨t, m⟩ => t.mapFinIdx fun i a h => f (i + 1) a ⋯)
          l.tail?.attach =
        some l₂
-- Mathlib.Order.WithBot
WithTop.untopD_eq_self_iff : ∀ {α : Type u_1} {d : α} {x : WithTop α}, WithTop.untopD d x = d ↔ x = ↑d ∨ x = ⊤
-- Mathlib.LinearAlgebra.TensorPower.Basic
TensorPower.cast_symm : ∀ (R : Type u_1) (M : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {i j : ℕ}
  (h : i = j), (TensorPower.cast R M h).symm = TensorPower.cast R M ⋯
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
algebraicIndependent_empty_type_iff : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [IsEmpty ι], AlgebraicIndependent R x ↔ Function.Injective ⇑(algebraMap R A)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne.eq_1 : ∀ {n : ℕ} (id : ℕ) (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment),
  { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }.deleteOne id =
    match clauses[id]! with
    | none => { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }
    | some { clause := [l], nodupkey := nodupkey, nodup := nodup } =>
      { clauses := clauses.set! id none, rupUnits := rupUnits, ratUnits := ratUnits,
        assignments := assignments.modify (↑l.1) (Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeAssignment l.2) }
    | some val =>
      { clauses := clauses.set! id none, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.toSubmonoid_injective : ∀ {G : Type u_1} [inst : Group G], Function.Injective Subgroup.toSubmonoid
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.all : Lean.Option Bool
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.parseTZifV1 : Std.Internal.Parsec.ByteArray.Parser Std.Time.TimeZone.TZif.TZifV1
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
/-- If `G` preserves coproducts and `C` has them,
then the cofan constructed of the mapped inclusion of a coproduct is a colimit.
 -/
CategoryTheory.Limits.isColimitOfHasCoproductOfPreservesColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          {J : Type w} →
            (f : J → C) →
              [inst_2 : CategoryTheory.Limits.HasCoproduct f] →
                [CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f) G] →
                  CategoryTheory.Limits.IsColimit
                    (CategoryTheory.Limits.Cofan.mk (G.obj (∐ f)) fun j => G.map (CategoryTheory.Limits.Sigma.ι f j))
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isTrail_of_isSubwalk : ∀ {V : Type u} {G : SimpleGraph V} {v w v' w' : V} {p₁ : G.Walk v w} {p₂ : G.Walk v' w'},
  p₁.IsSubwalk p₂ → p₂.IsTrail → p₁.IsTrail
-- Mathlib.Control.Functor
Functor.Comp.instApplicativeComp : {F : Type u → Type w} → {G : Type v → Type u} → [Applicative F] → [Applicative G] → Applicative (Functor.Comp F G)
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.IsUltra.bot : ∀ {X : Type u_1} {R : Type u_2} [inst : AddZeroClass R] [inst_1 : SemilatticeSup R], ⊥.IsUltra
-- Mathlib.RingTheory.QuasiFinite.Polynomial
Polynomial.not_weaklyQuasiFiniteAt : ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal (Polynomial R)) [inst_1 : P.IsPrime], ¬Algebra.WeaklyQuasiFiniteAt R P
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.inter : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet s μ → MeasureTheory.NullMeasurableSet t μ → MeasureTheory.NullMeasurableSet (s ∩ t) μ
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- The coefficient of `m` in the `i`-th coefficient of `finSuccEquiv R n f` equals the
coefficient of `Finsupp.cons i m` in `f`.  -/
MvPolynomial.finSuccEquiv_coeff_coeff : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ} (m : Fin n →₀ ℕ) (f : MvPolynomial (Fin (n + 1)) R) (i : ℕ),
  MvPolynomial.coeff m (((MvPolynomial.finSuccEquiv R n) f).coeff i) = MvPolynomial.coeff (Finsupp.cons i m) f
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- Formal power series of a continuous linear map `f : E →L[𝕜] F` at `x : E`:
`f y = f x + f (y - x)`.  -/
ContinuousLinearMap.fpowerSeries : {𝕜 : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : NontriviallyNormedField 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → (E →L[𝕜] F) → E → FormalMultilinearSeries 𝕜 E F
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.CategoryTheory.Monoidal.Category
/-- Naturality of the right unitor: commutativity of `X ⊗ 𝟙_ C ⟶ Y ⊗ 𝟙_ C ⟶ Y` and `X ⊗ 𝟙_ C ⟶ X ⟶ Y`
 -/
CategoryTheory.MonoidalCategory.rightUnitor_naturality_assoc : ∀ {C : Type u} {𝒞 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.MonoidalCategory C] {X Y : C} (f : X ⟶ Y)
  {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjXIso.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {D : Type u_3} [inst_4 : CategoryTheory.Category.{v_2, u_3} D]
  [inst_5 : CategoryTheory.Preadditive D] (H : CategoryTheory.Functor C D) [inst_6 : H.Additive]
  [inst_7 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)] (i : ι),
  HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjXIso φ H i =
    if hi : c.Rel i (c.next i) then
      H.mapIso (HomologicalComplex.homotopyCofiber.XIsoBiprod φ i (c.next i) hi) ≪≫
        H.mapBiprod (F.X (c.next i)) (G.X i) ≪≫
          (HomologicalComplex.homotopyCofiber.XIsoBiprod ((H.mapHomologicalComplex c).map φ) i (c.next i) hi).symm
    else
      H.mapIso (HomologicalComplex.homotopyCofiber.XIso φ i hi) ≪≫
        (HomologicalComplex.homotopyCofiber.XIso ((H.mapHomologicalComplex c).map φ) i hi).symm
-- Lean.Elab.Command
Lean.Elab.Command.MacroExpandedSnapshot.mk.inj : ∀ {toSnapshot : Lean.Language.Snapshot} {macroDecl : Lean.Name} {newStx : Lean.Syntax} {newNextMacroScope : ℕ}
  {hasTraces : Bool} {next : Array (Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot)}
  {toSnapshot_1 : Lean.Language.Snapshot} {macroDecl_1 : Lean.Name} {newStx_1 : Lean.Syntax} {newNextMacroScope_1 : ℕ}
  {hasTraces_1 : Bool} {next_1 : Array (Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot)},
  { toSnapshot := toSnapshot, macroDecl := macroDecl, newStx := newStx, newNextMacroScope := newNextMacroScope,
        hasTraces := hasTraces, next := next } =
      { toSnapshot := toSnapshot_1, macroDecl := macroDecl_1, newStx := newStx_1,
        newNextMacroScope := newNextMacroScope_1, hasTraces := hasTraces_1, next := next_1 } →
    toSnapshot = toSnapshot_1 ∧
      macroDecl = macroDecl_1 ∧
        newStx = newStx_1 ∧ newNextMacroScope = newNextMacroScope_1 ∧ hasTraces = hasTraces_1 ∧ next = next_1
-- Mathlib.Topology.Order.OrderClosed
isClosed_Ici : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIciTopology α] {a : α}, IsClosed (Set.Ici a)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The proof that it is the colimit cocone  -/
CategoryTheory.Limits.ColimitCocone.isColimit : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          (self : CategoryTheory.Limits.ColimitCocone F) → CategoryTheory.Limits.IsColimit self.cocone
-- Init.Tactics
/-- `refine e` behaves like `exact e`, except that named (`?x`) or unnamed (`?_`)
holes in `e` that are not solved by unification with the main goal's target type
are converted into new goals, using the hole's name, if any, as the goal case name.
 -/
Lean.Parser.Tactic.refine : Lean.ParserDescr
-- Mathlib.Combinatorics.Enumerative.Pentagonal.PowerSeries
PowerSeries.WithPiTopology.pentagonalSeries_eq_tsum_pow_pentagonal_sub : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : TopologicalSpace R] [T2Space R],
  PowerSeries.pentagonalSeries R =
    ∑' (k : ℕ), (-1) ^ k * (PowerSeries.X ^ pentagonal (-↑k) - PowerSeries.X ^ pentagonal (↑k + 1))
-- Mathlib.Computability.Primrec.Basic
Primrec.nat_rec₁ : ∀ {α : Type u_1} [inst : Primcodable α] {f : ℕ → α → α} (a : α), Primrec₂ f → Primrec fun t => Nat.rec a f t
-- Mathlib.Topology.Algebra.Module.Complement
Submodule.coe_projectionOntoL_apply : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {p q : Submodule R M} (h : Submodule.IsTopCompl p q) (x : M),
  ↑((p.projectionOntoL q h) x) = (p.projectionL q h) x
-- Mathlib.ModelTheory.Bundled
Equiv.bundledInduced_str : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] {N : Type w'} (g : M ≃ N),
  (Equiv.bundledInduced L g).str = g.inducedStructure
-- Mathlib.Data.Seq.Computation
Computation.eq_thinkN : ∀ {α : Type u} {s : Computation α} {a : α} {n : ℕ}, s.Results a n → s = (Computation.pure a).thinkN n
-- Mathlib.Topology.ContinuousMap.BoundedCompactlySupported
norm_lt_iff_of_compactlySupported : ∀ {α : Type u_1} {γ : Type u_2} [inst : TopologicalSpace α] [inst_1 : NonUnitalNormedRing γ]
  {f : BoundedContinuousFunction α γ}, f ∈ compactlySupported α γ → ∀ {M : ℝ}, 0 < M → (‖f‖ < M ↔ ∀ (x : α), ‖f x‖ < M)
-- Mathlib.Order.Hom.CompleteLattice
sInfHomClass.toInfTopHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : CompleteLattice α]
  [inst_2 : CompleteLattice β] [sInfHomClass F α β], InfTopHomClass F α β
-- Mathlib.Algebra.Tropical.Basic
/-- Tropical addition is the minimum of two underlying elements of `R`.  -/
Tropical.instAdd : {R : Type u} → [LinearOrder R] → Add (Tropical R)
-- Mathlib.Algebra.Group.Pi.Units
MulEquiv.piUnits.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)],
  MulEquiv.piUnits =
    { toFun := fun f i => { val := ↑f i, inv := f.inv i, val_inv := ⋯, inv_val := ⋯ },
      invFun := fun f => { val := fun x => ↑(f x), inv := fun x => (f x).inv, val_inv := ⋯, inv_val := ⋯ },
      left_inv := ⋯, right_inv := ⋯, map_mul' := ⋯ }
-- Std.Async.Basic
/-- Runs two computations concurrently and returns both results as a pair.
 -/
Std.Async.Async.concurrently : {α β : Type} →
  Std.Async.Async α → Std.Async.Async β → optParam Task.Priority Task.Priority.default → Std.Async.Async (α × β)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.continuous : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f : NormedAddGroupHom V₁ V₂), Continuous ⇑f
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction_map : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] (data : (X : C) → F.OneHypercoverDenseData J₀ J X)
  [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] (G₀ : CategoryTheory.Sheaf J₀ A) {X : C} {X₀ : C₀}
  (f : F.obj X₀ ⟶ X) {Y₀ : C₀} (g : Y₀ ⟶ X₀) {i : (data X).I₀} (p : F.obj Y₀ ⟶ F.obj ((data X).X i)),
  CategoryTheory.CategoryStruct.comp p ((data X).f i) = CategoryTheory.CategoryStruct.comp (F.map g) f →
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction data G₀ f)
        (G₀.obj.map g.op) =
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjπ data G₀ X i)
        (CategoryTheory.Functor.IsDenseSubsite.mapPreimage J F G₀ p)
-- Mathlib.CategoryTheory.Monad.Types
CategoryTheory.kleisliCatEquivKleisli_inverse_obj : ∀ (m : Type u → Type u) [inst : Monad m] [inst_1 : LawfulMonad m]
  (X : CategoryTheory.Kleisli (CategoryTheory.ofTypeMonad m)),
  (CategoryTheory.kleisliCatEquivKleisli m).inverse.obj X = X.of
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.le_set_normalizer_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {s : Set G},
  H ≤ AddSubgroup.normalizer s ↔ ∀ h ∈ H, ∀ g ∈ s, h + g + -h ∈ s
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwise_pair_of_symm : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α} [Std.Symm r], {a, b}.Pairwise r ↔ a ≠ b → r a b
-- Mathlib.Order.Minimal
OrderEmbedding.maximal_apply_mem_inter_range_iff : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {f : α ↪o β} {t : Set β},
  Maximal (fun x => x ∈ t ∩ Set.range ⇑f) (f x) ↔ Maximal (fun x => f x ∈ t) x
-- Mathlib.Tactic.IntervalCases
Int.le_sub_one_of_not_le : ∀ {a b : ℤ}, ¬b ≤ a → a ≤ b - 1
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Closure
SubAddAction.closure_le : ∀ {R : Type u_1} {M : Type u_2} [inst : VAdd R M] {s : Set M} {p : SubAddAction R M},
  SubAddAction.closure R s ≤ p ↔ s ⊆ ↑p
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.instIsScalarTowerCotangent : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R₁ : Type u_1} {R₂ : Type u_2} [inst_3 : CommRing R₁] [inst_4 : CommRing R₂] [inst_5 : Algebra R₁ S]
  [inst_6 : Algebra R₂ S] [inst_7 : Algebra R₁ R₂] [IsScalarTower R₁ R₂ S], IsScalarTower R₁ R₂ P.Cotangent
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isLittleO_abs_abs`. -/
Asymptotics.IsLittleO.of_abs_abs : ∀ {α : Type u_1} {l : Filter α} {u v : α → ℝ}, ((fun x => |u x|) =o[l] fun x => |v x|) → u =o[l] v
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
AlgebraicGeometry.IsIntegralHom.instUniversallyClosed : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsIntegralHom f],
  AlgebraicGeometry.UniversallyClosed f
-- Mathlib.Algebra.Field.Defs
/-- `a / b := a * b⁻¹`  -/
Field.div_eq_mul_inv : ∀ {K : Type u} [self : Field K] (a b : K), a / b = a * b⁻¹
-- Mathlib.Order.Cover
/-- **Alias** of the reverse direction of `ofDual_wcovBy_ofDual_iff`. -/
WCovBy.ofDual : ∀ {α : Type u_1} [inst : Preorder α] {a b : αᵒᵈ}, b ⩿ a → OrderDual.ofDual a ⩿ OrderDual.ofDual b
-- Mathlib.Control.Bitraversable.Instances
/-- The bitraverse function for `Const`. It throws away the second map.  -/
Const.bitraverse : {F : Type u → Type u} →
  [Applicative F] →
    {α : Type u_1} →
      {α' : Type u} →
        {β : Type u_2} → {β' : Type u} → (α → F α') → (β → F β') → Functor.Const α β → F (Functor.Const α' β')
-- Mathlib.Algebra.Category.BoolRing
BoolRing.hasForgetToCommRing : CategoryTheory.HasForget₂ BoolRing CommRingCat
-- Mathlib.Algebra.Algebra.Subalgebra.Tower
Subalgebra.restrictScalars_injective : ∀ (R : Type u) {S : Type v} {A : Type w} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A],
  Function.Injective (Subalgebra.restrictScalars R)
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- When `F ⊣ G`,
the functor associating to each `Y` the cocones over `K ⋙ F` with cone point `Y`
is naturally isomorphic to
the functor associating to each `Y` the cocones over `K` with cone point `G.obj Y`.
 -/
CategoryTheory.Adjunction.coconesIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₀, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₀, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {J : Type u} →
                [inst_2 : CategoryTheory.Category.{v, u} J] →
                  {K : CategoryTheory.Functor J C} →
                    (CategoryTheory.cocones J D).obj (Opposite.op (K.comp F)) ≅
                      G.comp ((CategoryTheory.cocones J C).obj (Opposite.op K))
-- Mathlib.Data.Int.GCD
/-- If `gcd a (m * n) = 1`, then `gcd a n = 1`.  -/
Int.gcd_eq_one_of_gcd_mul_right_eq_one_right : ∀ {a : ℤ} {m n : ℕ}, a.gcd (↑m * ↑n) = 1 → a.gcd ↑n = 1
-- Mathlib.Algebra.Algebra.Hom
AlgHom.algebraMap_eq_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B) {y : R} {x : A},
  (algebraMap R A) y = x → (algebraMap R B) y = f x
-- Lean.Elab.ConfigEval.Types
Lean.Elab.ConfigEval.throwUnsupportedExpr : {m : Type u_1 → Type u_2} → {α : Type u_1} → [MonadExceptOf Lean.Exception m] → m α
-- Mathlib.MeasureTheory.Integral.Bochner.ContinuousLinearMap
setIntegral_withDensity_eq_setIntegral_smul₀' : ∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] {f : X → NNReal} (s : Set X),
  AEMeasurable f (μ.restrict s) →
    ∀ (g : X → E), (∫ (x : X) in s, g x ∂μ.withDensity fun x => ↑(f x)) = ∫ (x : X) in s, f x • g x ∂μ
-- Lean.Meta.Constructions.CtorElim
_private.Lean.Meta.Constructions.CtorElim.0.Lean.mkPULift : Lean.Level → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.Complex.Basic
Complex.re_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], (OfNat.ofNat n).re = OfNat.ofNat n
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.Raw.toArray_keysIter : ∀ {α β : Type u} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → m.keysIter.toArray = m.keysArray
-- Mathlib.Topology.Compactness.LocallyCompact
LocallyCompactSpace.of_hasBasis : ∀ {X : Type u_1} [inst : TopologicalSpace X] {ι : X → Type u_4} {p : (x : X) → ι x → Prop} {s : (x : X) → ι x → Set X},
  (∀ (x : X), (nhds x).HasBasis (p x) (s x)) → (∀ (x : X) (i : ι x), p x i → IsCompact (s x i)) → LocallyCompactSpace X
-- Mathlib.Algebra.Regular.SMul
/-- **Alias** of the reverse direction of `isSMulRegular_iff_right_eq_zero_of_smul`. -/
IsSMulRegular.of_right_eq_zero_of_smul : ∀ {R : Type u_1} {M : Type u_3} [inst : AddGroup M] [inst_1 : DistribSMul R M] {r : R},
  (∀ (m : M), r • m = 0 → m = 0) → IsSMulRegular M r
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.hom_ofHom : ∀ (R : Type u) [inst : Ring R] [inst_1 : TopologicalSpace R] {X Y : Type v} [inst_2 : AddCommGroup X]
  [inst_3 : Module R X] [inst_4 : TopologicalSpace X] [inst_5 : ContinuousAdd X] [inst_6 : ContinuousSMul R X]
  [inst_7 : AddCommGroup Y] [inst_8 : Module R Y] [inst_9 : TopologicalSpace Y] [inst_10 : ContinuousAdd Y]
  [inst_11 : ContinuousSMul R Y] (f : X →L[R] Y), TopModuleCat.Hom.hom (TopModuleCat.ofHom f) = f
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.mk'.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] [inst_2 : SizeOf C]
  (obj₁ obj₂ obj₃ : C) (mor₁ : obj₁ ⟶ obj₂) (mor₂ : obj₂ ⟶ obj₃)
  (mor₃ : obj₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj obj₁),
  sizeOf { obj₁ := obj₁, obj₂ := obj₂, obj₃ := obj₃, mor₁ := mor₁, mor₂ := mor₂, mor₃ := mor₃ } =
    1 + sizeOf obj₁ + sizeOf obj₂ + sizeOf obj₃ + sizeOf mor₁ + sizeOf mor₂ + sizeOf mor₃
-- Mathlib.MeasureTheory.PiSystem
MeasurableSpace.DynkinSystem.GenerateHas.iUnion : ∀ {α : Type u_3} {s : Set (Set α)} {f : ℕ → Set α},
  Pairwise (Function.onFun Disjoint f) →
    (∀ (i : ℕ), MeasurableSpace.DynkinSystem.GenerateHas s (f i)) →
      MeasurableSpace.DynkinSystem.GenerateHas s (⋃ i, f i)
-- Std.Data.DHashMap.Internal.AssocList.Iterator
Std.DHashMap.Internal.AssocList.AssocListIterator.ext : ∀ {α : Type u} {β : α → Type v} {x y : Std.DHashMap.Internal.AssocList.AssocListIterator α β}, x.l = y.l → x = y
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.mdifferentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} (Φ : PartialDiffeomorph I J M N n),
  n ≠ 0 → MDiff[Φ.source] ↑Φ.toPartialEquiv
-- Mathlib.Order.Cover
CovBy.Ioo_eq_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b ⋖ a → ∀ (c : α), Set.Ioo c a = Set.Ioc c b
-- Mathlib.Topology.ContinuousMap.LocallyConstant
LocallyConstant.toContinuousMapMonoidHom.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Monoid Y]
  [inst_3 : ContinuousMul Y],
  LocallyConstant.toContinuousMapMonoidHom = { toFun := LocallyConstant.toContinuousMap, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.step.match_1.eq_2 : ∀ (motive : Turing.ToPartrec.Cfg → Sort u_1) (k : Turing.ToPartrec.Cont) (v : List ℕ)
  (h_1 : (a : List ℕ) → motive (Turing.ToPartrec.Cfg.halt a))
  (h_2 : (k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cfg.ret k v)),
  (match Turing.ToPartrec.Cfg.ret k v with
    | Turing.ToPartrec.Cfg.halt a => h_1 a
    | Turing.ToPartrec.Cfg.ret k v => h_2 k v) =
    h_2 k v
-- Mathlib.Logic.Equiv.Fin.Basic
/-- `Fin.succAbove` as a bijection between `Fin n` and `{x : Fin (n + 1) // x ≠ p}`.  -/
finSuccAboveEquiv : {n : ℕ} → (p : Fin (n + 1)) → Fin n ≃ { x // x ≠ p }
-- Mathlib.Topology.MetricSpace.PiNat
PiNat.dist_triangle_nonarch : ∀ {E : ℕ → Type u_1} (x y z : (n : ℕ) → E n), dist x z ≤ max (dist x y) (dist y z)
-- Mathlib.CategoryTheory.Category.Pointed
Pointed.instFunLikeSubtypeForallXEqPoint : (X : Pointed) → (Y : Pointed) → FunLike { f // f X.point = Y.point } X.X Y.X
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.presieve₀_empty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C},
  (CategoryTheory.PreZeroHypercover.empty S).presieve₀ = ⊥