mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.id_right : ∀ {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} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.ContainsIdentities]
  [inst_4 : W.ContainsIdentities] (X : CategoryTheory.MorphismProperty.Comma L R P Q W),
  X.id.right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.CategoryTheory.Limits.Opposites
/-- If `F.leftOp : Jᵒᵖ ⥤ C` has a colimit, we can construct a limit for `F : J ⥤ Cᵒᵖ`.
 -/
CategoryTheory.Limits.hasLimit_of_hasColimit_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [CategoryTheory.Limits.HasColimit F.leftOp], CategoryTheory.Limits.HasLimit F
-- Mathlib.Order.GameAdd
Prod.gameAdd_swap_swap : ∀ {α : Type u_1} {β : Type u_2} (rα : α → α → Prop) (rβ : β → β → Prop) (a b : α × β),
  Prod.GameAdd rβ rα a.swap b.swap ↔ Prod.GameAdd rα rβ a b
-- Mathlib.CategoryTheory.Presentable.Limits
CategoryTheory.Functor.IsCardinalAccessible.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F F_1 : CategoryTheory.Functor C D),
  F = F_1 →
    ∀ (κ κ_1 : Cardinal.{w}) (e_κ : κ = κ_1) [inst_2 : Fact κ.IsRegular],
      F.IsCardinalAccessible κ = F_1.IsCardinalAccessible κ_1
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- The iterated derivative commutes with subtracting a constant.  -/
iteratedFDeriv_comp_sub' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  (n : ℕ) (a : E), (iteratedFDeriv 𝕜 n fun z => f (z - a)) = fun x => iteratedFDeriv 𝕜 n f (x - a)
-- Mathlib.Algebra.MonoidAlgebra.Basic
/-- If `f : M → N` is a homomorphism between two magmas, then `MonoidAlgebra.mapDomain f`
is a non-unital algebra homomorphism between their magma algebras.  -/
MonoidAlgebra.mapDomainNonUnitalAlgHom : (R : Type u_1) →
  (A : Type u_4) →
    {M : Type u_7} →
      {N : Type u_8} →
        [inst : CommSemiring R] →
          [inst_1 : Semiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : Mul M] → [inst_4 : Mul N] → (M →ₙ* N) → MonoidAlgebra A M →ₙₐ[R] MonoidAlgebra A N
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.map_δ_μ_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 D] {C' : Type u₁'}
  [inst_4 : CategoryTheory.Category.{v₁', u₁'} C'] (F : CategoryTheory.Functor C D) [inst_5 : F.Monoidal]
  (G : CategoryTheory.Functor D C') (X Y : C) {Z : C'}
  (h : G.obj (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.OplaxMonoidal.δ F X Y))
      (CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Functor.LaxMonoidal.μ F X Y)) h) =
    h
-- Mathlib.Logic.Equiv.Defs
Equiv.symm_symm : ∀ {α : Sort u} {β : Sort v} (e : α ≃ β), e.symm.symm = e
-- Mathlib.Algebra.Order.Group.Synonym
ofLex_vadd : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : β) (a : Lex α), ofLex (b +ᵥ a) = b +ᵥ ofLex a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.comp_mul_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X Y : C} [inst_2 : CategoryTheory.MonObj M] (f : X ⟶ Y) (g₁ g₂ : Y ⟶ M) {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (g₁ * g₂) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp f g₁ * CategoryTheory.CategoryStruct.comp f g₂) h
-- Mathlib.Tactic.Widget.StringDiagram
/-- Add the variable `v` with the type `tp` to the substance program.  -/
Mathlib.Tactic.Widget.StringDiagram.addPenroseVar : String → Mathlib.Tactic.Widget.StringDiagram.PenroseVar → ProofWidgets.Penrose.DiagramBuilderM Unit
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.instInt : Lean.Elab.ConfigEval.EvalTerm ℤ
-- Mathlib.LinearAlgebra.FreeModule.Norm
LinearEquiv.coord.congr_simp : ∀ (R : Type u_1) (M : Type u_4) [inst : Ring R] [inst_1 : IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.IsTorsionFree R M] (x : M) (h : x ≠ 0), LinearEquiv.coord R M x h = LinearEquiv.coord R M x h
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.ext_iff : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {I J : FractionalIdeal S P}, I = J ↔ ∀ (x : P), x ∈ I ↔ x ∈ J
-- Mathlib.Order.Sublattice
Sublattice.prod_eq_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] {L : Sublattice α} {M : Sublattice β},
  L.prod M = ⊥ ↔ L = ⊥ ∨ M = ⊥
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonProj : Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.MeasureTheory.Function.Jacobian
MeasureTheory.addHaar_image_le_lintegral_abs_det_fderiv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasurableSet s →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → μ (f '' s) ≤ ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| ∂μ
-- Lean.DeprecatedModule
Lean.DeprecatedModuleEntry.mk : Option String → Option String → Lean.DeprecatedModuleEntry
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
/-- Variant of the interaction of `sum` and `•` assuming some scalar multiplication structure.  -/
SkewMonoidAlgebra.sum_smul_index' : ∀ {k : Type u_1} {G : Type u_2} {N : Type u_3} {R : Type u_4} [inst : AddCommMonoid k] [inst_1 : DistribSMul R k]
  [inst_2 : AddCommMonoid N] {g : SkewMonoidAlgebra k G} {b : R} {h : G → k → N},
  (∀ (i : G), h i 0 = 0) → (b • g).sum h = g.sum fun x1 x2 => h x1 (b • x2)
-- Mathlib.Order.Heyting.Hom
HeytingHomClass.mk : ∀ {F : Type u_6} {α : Type u_7} {β : Type u_8} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β]
  [inst_2 : FunLike F α β] [toLatticeHomClass : LatticeHomClass F α β],
  (∀ (f : F), f ⊥ = ⊥) → (∀ (f : F) (a b : α), f (a ⇨ b) = f a ⇨ f b) → HeytingHomClass F α β
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
AlgebraicGeometry.opensDiagram_map : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme) (i : I)
  (U : (D.obj i).Opens) {j k : CategoryTheory.Over i} (f : j ⟶ k),
  (AlgebraicGeometry.opensDiagram D i U).map f =
    AlgebraicGeometry.Scheme.Hom.resLE (D.map (CategoryTheory.Over.Hom.left f))
      ((TopologicalSpace.Opens.map (D.map k.hom).base).obj U) ((TopologicalSpace.Opens.map (D.map j.hom).base).obj U) ⋯
-- Mathlib.Data.List.Chain
List.isChain_append : ∀ {α : Type u_1} {R : α → α → Prop} {l₁ l₂ : List α},
  List.IsChain R (l₁ ++ l₂) ↔ List.IsChain R l₁ ∧ List.IsChain R l₂ ∧ ∀ x ∈ l₁.getLast?, ∀ y ∈ l₂.head?, R x y
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length'_ne_zero_iff_cons : ∀ {α : Type u} (s : Stream'.Seq α), s.length' ≠ 0 ↔ ∃ x s', s = Stream'.Seq.cons x s'
-- Mathlib.LinearAlgebra.AffineSpace.Basis
/-- The `i`th barycentric coordinate of a point.  -/
AffineBasis.coord : {ι : Type u_1} →
  {k : Type u_5} →
    {V : Type u_6} →
      {P : Type u_7} →
        [inst : AddCommGroup V] →
          [inst_1 : AddTorsor V P] → [inst_2 : Ring k] → [inst_3 : Module k V] → AffineBasis ι k P → ι → P →ᵃ[k] k
-- Mathlib.Data.Finset.Sum
Finset.disjSum_subset : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} {u : Finset (α ⊕ β)},
  s.disjSum t ⊆ u ↔ s ⊆ u.toLeft ∧ t ⊆ u.toRight
-- Mathlib.AlgebraicTopology.SimplicialSet.Finite
SSet.Finite.finite : ∀ {X : SSet} [self : X.Finite], Finite X.N
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- The forgetful functor from `X.AffineZariskiSite` to `Scheme` is isomorphic to `Spec Γ(X, -)`.  -/
AlgebraicGeometry.Scheme.AffineZariskiSite.restrictIsoSpec : (X : AlgebraicGeometry.Scheme) →
  (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).comp
      (X.restrictFunctor.comp (CategoryTheory.Over.forget X)) ≅
    (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).comp
      ((CategoryTheory.Functor.rightOp X.presheaf).comp AlgebraicGeometry.Scheme.Spec)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_filterMap : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] {f : α → β → Option γ} {k : α} (h : t.WF)
  {h' : Std.DTreeMap.Internal.Impl.contains k (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl = true},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.filterMap f t ⋯).impl k h' =
    (f (t.getKey k ⋯) (Std.DTreeMap.Internal.Impl.Const.get t k ⋯)).get ⋯
-- Mathlib.Topology.FiberBundle.Constructions
pullbackTopology_def : ∀ {B : Type u_1} (F : Type u_2) (E : B → Type u_3) {B' : Type u_4} (f : B' → B) [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)],
  pullbackTopology F E f =
    TopologicalSpace.induced Bundle.TotalSpace.proj inst ⊓ TopologicalSpace.induced (Bundle.Pullback.lift f) inst_1
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.pullbackIsoUnopPushout_hom_inr_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPullback f g] {Z_1 : Cᵒᵖ}
  (h : Opposite.op (CategoryTheory.Limits.pullback f g) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr f.op g.op)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackIsoUnopPushout f g).hom.op h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g).op h
-- Mathlib.Algebra.Group.Defs
DivisionMonoid.mk : {G : Type u} →
  [toDivInvMonoid : DivInvMonoid G] →
    (∀ (x : G), x⁻¹⁻¹ = x) →
      (∀ (a b : G), (a * b)⁻¹ = b⁻¹ * a⁻¹) → (∀ (a b : G), a * b = 1 → a⁻¹ = b) → DivisionMonoid G
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_ord : ∀ {ι : Sort u_3} (f : ι → Cardinal.{u_4}), (⨆ i, f i).ord = ⨆ i, (f i).ord
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.size_alter_le_size : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α} {f : Option β → Option β}, (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.size ≤ t.size + 1
-- Mathlib.Analysis.InnerProductSpace.Defs
PreInnerProductSpace.Core.toInner : {𝕜 : Type u_4} →
  {F : Type u_5} →
    [inst : RCLike 𝕜] → [inst_1 : AddCommGroup F] → [inst_2 : Module 𝕜 F] → PreInnerProductSpace.Core 𝕜 F → Inner 𝕜 F
-- Mathlib.Topology.Sets.Compacts
/-- the carrier set, i.e. the points in this set  -/
TopologicalSpace.Compacts.carrier : {α : Type u_4} → [inst : TopologicalSpace α] → TopologicalSpace.Compacts α → Set α
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndepOn.notMem_span_of_insert : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {i : ι} [Nontrivial R], LinearIndepOn R v (insert i s) → i ∉ s → v i ∉ Submodule.span R (v '' s)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.top_prod : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] (s : AddSubsemigroup N),
  ⊤.prod s = AddSubsemigroup.comap (AddHom.snd M N) s
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.mono : ∀ {G : Type u_1} [inst : Group G] {A : Set G} {K L : ℝ}, K ≤ L → IsApproximateSubgroup K A → IsApproximateSubgroup L A
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.coconePointsIsoOfNatIso_inv_desc_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F G : CategoryTheory.Functor J C} {r s : CategoryTheory.Limits.Cocone F} {t : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit s) (Q : CategoryTheory.Limits.IsColimit t) (w : F ≅ G) {Z : C} (h : r.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.coconePointsIsoOfNatIso Q w).inv
      (CategoryTheory.CategoryStruct.comp (P.desc r) h) =
    CategoryTheory.CategoryStruct.comp (Q.map r w.inv) h
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Note that this provides `IsScalarTower S R R` which is needed by `smul_mul_assoc`.  -/
Subsemiring.isScalarTower : ∀ {R' : Type u_1} {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring R'] [inst_1 : SMul α β] [inst_2 : SMul R' α]
  [inst_3 : SMul R' β] [IsScalarTower R' α β] (S : Subsemiring R'), IsScalarTower (↥S) α β
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.CongrInfo.interlaced.inj : ∀ {rewritable rewritable_1 : Array Bool},
  Lean.Meta.Sym.CongrInfo.interlaced rewritable = Lean.Meta.Sym.CongrInfo.interlaced rewritable_1 →
    rewritable = rewritable_1
-- Mathlib.Order.Filter.SmallSets
Filter.hasBasis_smallSets : ∀ {α : Type u_1} (l : Filter α), l.smallSets.HasBasis (fun t => t ∈ l) Set.powerset
-- Batteries.Data.Fin.Lemmas
Fin.eq_false_of_find?_eq_some_of_lt : ∀ {n : ℕ} {i : Fin n} {p : Fin n → Bool}, Fin.find? p = some i → ∀ j < i, p j = false
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.stationaryPoint.congr_simp : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f f_1 : PadicSeq p} (e_f : f = f_1) (hf : ¬f ≈ 0),
  PadicSeq.stationaryPoint hf = PadicSeq.stationaryPoint ⋯
-- Lean.Meta.Basic
Lean.Meta.instInhabitedExprConfigCacheKey : Inhabited Lean.Meta.ExprConfigCacheKey
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toLinearMap : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        {σ : R →+* S} →
          {M : Type u_3} →
            [inst_2 : TopologicalSpace M] →
              [inst_3 : AddCommMonoid M] →
                {M₂ : Type u_4} →
                  [inst_4 : TopologicalSpace M₂] →
                    [inst_5 : AddCommMonoid M₂] →
                      [inst_6 : Module R M] → [inst_7 : Module S M₂] → (M →SL[σ] M₂) → M →ₛₗ[σ] M₂
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.hasImageMapOfIsIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : CategoryTheory.Arrow C}
  [inst_1 : CategoryTheory.Limits.HasImage f.hom] [inst_2 : CategoryTheory.Limits.HasImage g.hom] (sq : f ⟶ g)
  [CategoryTheory.IsIso sq], CategoryTheory.Limits.HasImageMap sq
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k a : α} {h' : a ∈ t.erase k}, (t.erase k).getKey a h' = t.getKey a ⋯
-- Std.Sat.AIG.RefVec
_private.Std.Sat.AIG.RefVec.0.Std.Sat.AIG.RefVec.get.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {len : ℕ} →
          (motive : aig.RefVec len → Sort u_1) →
            (s : aig.RefVec len) →
              ((refs : Vector Std.Sat.AIG.Fanin len) →
                  (hrefs : ∀ {i : ℕ} (h : i < len), refs[i].gate < aig.decls.size) →
                    motive { refs := refs, hrefs := hrefs }) →
                motive s
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.symm_trans_self : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N), e.symm.trans e = LieModuleEquiv.refl
-- Batteries.Data.Fin.Lemmas
Fin.exists_isSome_of_isSome_findSome? : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, (Fin.findSome? f).isSome = true → ∃ i, (f i).isSome = true
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform_obj_obj_fst_obj : ∀ {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} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  (X : Type u₇) [inst_6 : CategoryTheory.Category.{v₇, u₇} X] (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (S : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X) (X_1 : X),
  (((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ).obj S).fst.obj X_1 =
    ψ.left.obj (S.fst.obj X_1)
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.card_mul_cast_mulConst : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {𝕜 : Type u_3} [inst_2 : Semifield 𝕜] [CharZero 𝕜]
  (A B : Finset G), ↑A.card * ↑(A.mulConst B) = ↑(A * B).card
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
_private.Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph.0.SimpleGraph.Walk.toSubgraph.match_1.splitter : {V : Type u_1} →
  {G : SimpleGraph V} →
    {u : V} →
      (motive : (v : V) → G.Walk u v → Sort u_2) →
        (v : V) →
          (x : G.Walk u v) →
            (Unit → motive u SimpleGraph.Walk.nil) →
              ((v v_1 : V) → (h : G.Adj u v_1) → (p : G.Walk v_1 v) → motive v (SimpleGraph.Walk.cons h p)) → motive v x
-- Mathlib.Algebra.Notation.Defs
add_dite : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Add α] (a : α) (b : P → α) (c : ¬P → α),
  (a + if h : P then b h else c h) = if h : P then a + b h else a + c h
-- Mathlib.Order.CompleteLatticeIntervals
/-- For a nonempty subset of a conditionally complete linear order to be a conditionally complete
linear order, it suffices that it contain the `sSup` of all its nonempty bounded-above subsets, and
the `sInf` of all its nonempty bounded-below subsets.
See note [reducible non-instances].  -/
subsetConditionallyCompleteLinearOrder : {α : Type u_2} →
  (s : Set α) →
    [inst : ConditionallyCompleteLinearOrder α] →
      [Inhabited ↑s] →
        (∀ {t : Set ↑s}, t.Nonempty → BddAbove t → sSup (Subtype.val '' t) ∈ s) →
          (∀ {t : Set ↑s}, t.Nonempty → BddBelow t → sInf (Subtype.val '' t) ∈ s) → ConditionallyCompleteLinearOrder ↑s
-- Mathlib.Data.Int.GCD
/-- For nonzero integers `a` and `b`, `gcd a b` is the smallest positive natural number that can be
written in the form `a * x + b * y` for some pair of integers `x` and `y`  -/
Int.gcd_least_linear : ∀ {a b : ℤ}, a ≠ 0 → IsLeast {n | 0 < n ∧ ∃ x y, ↑n = a * x + b * y} (a.gcd b)
-- Mathlib.Data.Set.Piecewise
Set.piecewise_same : ∀ {α : Type u_1} {δ : α → Sort u_7} (s : Set α) (f : (i : α) → δ i) [inst : (j : α) → Decidable (j ∈ s)],
  s.piecewise f f = f
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ (Type v)} {ℱ' : CategoryTheory.Sheaf K (Type v)}
  (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) [G.IsLocallyFull K] {X : D} (x : ℱ.obj (Opposite.op X)) {Y : C}
  (f : G.obj Y ⟶ X),
  CategoryTheory.Functor.IsCoverDense.Types.pushforwardFamily α x f ⋯ =
    (CategoryTheory.ConcreteCategory.hom (α.app (Opposite.op Y))) ((CategoryTheory.ConcreteCategory.hom (ℱ.map f.op)) x)
-- Lean.Meta.Closure
_private.Lean.Meta.Closure.0.Lean.Meta.Closure.TopoSort.newArgs : Lean.Meta.Closure.TopoSort✝ → Array Lean.Expr
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
exists_dist_eq : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] (x z : E) {a b : ℝ},
  0 ≤ a → 0 ≤ b → a + b = 1 → ∃ y, dist x y = b * dist x z ∧ dist y z = a * dist x z
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueAdd.of_addOpposite : ∀ {G : Type u_1} [inst : Add G] {A B : Finset G} {a0 b0 : G},
  UniqueAdd (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } B) (Finset.map { toFun := AddOpposite.op, inj' := ⋯ } A)
      (AddOpposite.op b0) (AddOpposite.op a0) →
    UniqueAdd A B a0 b0
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.instCoeAffineMap : {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₂] → Coe (P₁ ≃ᵃ[k] P₂) (P₁ →ᵃ[k] P₂)
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctor_map_hom₃ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (n : ℤ) {X Y : CategoryTheory.Pretriangulated.Triangle C} (f : X ⟶ Y),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctor C n).map f).hom₃ = (CategoryTheory.shiftFunctor C n).map f.hom₃
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.whiskerLeft_naturality_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.Pseudofunctor B C} (θ : G ⟶ H) {a b c : B} {a' : C} (f : a' ⟶ G.obj a) (g : a ⟶ b) (h : b ⟶ c)
  {Z : a' ⟶ H.obj c}
  (h_1 :
    CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp (θ.app a) (CategoryTheory.CategoryStruct.comp (H.map g) (H.map h))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.comp g h)).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapComp g h).hom))
        h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapComp g h).hom (θ.app c)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f
          (CategoryTheory.Bicategory.associator (G.map g) (G.map h) (θ.app c)).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft f
            (CategoryTheory.Bicategory.whiskerLeft (G.map g) (θ.naturality h).hom))
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft f
              (CategoryTheory.Bicategory.associator (G.map g) (θ.app b) (H.map h)).inv)
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Bicategory.whiskerLeft f
                (CategoryTheory.Bicategory.whiskerRight (θ.naturality g).hom (H.map h)))
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.Bicategory.whiskerLeft f
                  (CategoryTheory.Bicategory.associator (θ.app a) (H.map g) (H.map h)).hom)
                h_1)))))
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.smul_sInter_subset : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] (s : Set α) (T : Set (Set β)), s • ⋂₀ T ⊆ ⋂ t ∈ T, s • t
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- Composition of morphisms in `HomotopyCategory₂ A` is given by lifting the edge
chosen by `composeEdges`.
 -/
SSet.Truncated.HomotopyCategory₂.instCategoryStruct : {A : SSet.Truncated 2} → [A.Quasicategory₂] → CategoryTheory.CategoryStruct.{u_1, u_1} A.HomotopyCategory₂