mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.isPullback_natTrans_ι_toBase : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰)
  [inst_2 : Small.{u, u_1} 𝒰.I₀] [inst_3 : Quiver.IsThin 𝒰.I₀] (i : 𝒰.I₀),
  CategoryTheory.IsPullback (d.natTrans.app i) (CategoryTheory.Limits.colimit.ι d.functor i) (𝒰.f i) d.toBase
-- Mathlib.Computability.TuringMachine.Config
_private.Mathlib.Computability.TuringMachine.Config.0.Turing.ToPartrec.step.match_1.splitter : (motive : Turing.ToPartrec.Cfg → Sort u_1) →
  (x : Turing.ToPartrec.Cfg) →
    ((a : List ℕ) → motive (Turing.ToPartrec.Cfg.halt a)) →
      ((k : Turing.ToPartrec.Cont) → (v : List ℕ) → motive (Turing.ToPartrec.Cfg.ret k v)) → motive x
-- Init.Data.UInt.Bitwise
USize.and_eq_neg_one_iff : ∀ {a b : USize}, a &&& b = -1 ↔ a = -1 ∧ b = -1
-- Batteries.Data.Fin.Basic
/-- `find? p` returns the first `i` for which `p i = true`, or `none` if no such element is found.
The function `p` is not evaluated on further inputs after the first `i` is found.
 -/
Fin.findRev? : {n : ℕ} → (Fin n → Bool) → Option (Fin n)
-- Mathlib.Algebra.Lie.CartanSubalgebra
LieSubalgebra.IsCartanSubalgebra.self_normalizing : ∀ {R : Type u} {L : Type v} {inst : CommRing R} {inst_1 : LieRing L} {inst_2 : LieAlgebra R L} {H : LieSubalgebra R L}
  [self : H.IsCartanSubalgebra], H.normalizer = H
-- Mathlib.Data.Set.Insert
Set.insert_idem : ∀ {α : Type u_1} (a : α) (s : Set α), insert a (insert a s) = insert a s
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.SeparatingRight.toLinearMap₂' : ∀ {R : Type u_1} {n : Type u_11} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R},
  M.SeparatingRight → ((Matrix.toLinearMap₂' R) M).SeparatingRight
-- Mathlib.RingTheory.Congruence.Hom
RingCon.comapQuotientEquivRange.congr_simp : ∀ {M : Type u_1} {N : Type u_2} [inst : Ring M] [inst_1 : Ring N] (c : RingCon M) (f : N →+* M) {d : RingCon N}
  (hcd : d = c.comap f), c.comapQuotientEquivRange f hcd = c.comapQuotientEquivRange f hcd
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.foldlIdx.match_1.splitter : {β : Type u_1} →
  (motive : List β → ℕ → Sort u_2) →
    (x : List β) →
      (x_1 : ℕ) → ((x : ℕ) → motive [] x) → ((b : β) → (l : List β) → (s : ℕ) → motive (b :: l) s) → motive x x_1
-- Mathlib.Algebra.Algebra.NonUnitalHom
/-- The first projection of a product is a non-unital algebra homomorphism.  -/
NonUnitalAlgHom.fst : (R : Type u) →
  [inst : Monoid R] →
    (A : Type v) →
      (B : Type w) →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : DistribMulAction R A] →
            [inst_3 : NonUnitalNonAssocSemiring B] → [inst_4 : DistribMulAction R B] → A × B →ₙₐ[R] A
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.brecOn.go : {C : Type u} →
  {motive : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C → Sort u_1} →
    (t : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
      ((t : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
          CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.below t → motive t) →
        motive t ×' CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.below t
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get.congr_simp : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m m_1 : Std.HashSet.Raw α) (e_m : m = m_1) (a a_1 : α)
  (e_a : a = a_1) (h : a ∈ m), m.get a h = m_1.get a_1 ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
CategoryTheory.Limits.pullbackRightPullbackFstIso_inv_snd_snd_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) (f' : W ⟶ X)
  [inst_1 : CategoryTheory.Limits.HasPullback f g]
  [inst_2 : CategoryTheory.Limits.HasPullback f' (CategoryTheory.Limits.pullback.fst f g)] {Z_1 : C} (h : Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackRightPullbackFstIso f g f').inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd f' (CategoryTheory.Limits.pullback.fst f g))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f g) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd (CategoryTheory.CategoryStruct.comp f' f) g)
      h
-- Mathlib.Analysis.Real.Pi.Irrational
_private.Mathlib.Analysis.Real.Pi.Irrational.0.sinPoly.eq_def : ∀ (x : ℕ),
  sinPoly✝ x =
    match x with
    | 0 => Polynomial.C 2
    | 1 => Polynomial.C 4
    | n.succ.succ => (2 * (2 * ↑n + 3)) • sinPoly✝ (n + 1) + (Polynomial.monomial 2) (-4) * sinPoly✝ n
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (toPrecoverage : CategoryTheory.Precoverage C)
  (has_isos :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X) [CategoryTheory.IsIso f], CategoryTheory.Presieve.singleton f ∈ toPrecoverage.coverings X)
  (pullbacks :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
      ∀ S ∈ toPrecoverage.coverings X, CategoryTheory.Presieve.pullbackArrows f S ∈ toPrecoverage.coverings Y)
  (transitive :
    ∀ ⦃X : C⦄ (S : CategoryTheory.Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → CategoryTheory.Presieve Y),
      S ∈ toPrecoverage.coverings X →
        (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ toPrecoverage.coverings Y) → S.bind Ti ∈ toPrecoverage.coverings X)
  (toPrecoverage_1 : CategoryTheory.Precoverage C)
  (has_isos_1 :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X) [CategoryTheory.IsIso f], CategoryTheory.Presieve.singleton f ∈ toPrecoverage_1.coverings X)
  (pullbacks_1 :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X),
      ∀ S ∈ toPrecoverage_1.coverings X, CategoryTheory.Presieve.pullbackArrows f S ∈ toPrecoverage_1.coverings Y)
  (transitive_1 :
    ∀ ⦃X : C⦄ (S : CategoryTheory.Presieve X) (Ti : ⦃Y : C⦄ → (f : Y ⟶ X) → S f → CategoryTheory.Presieve Y),
      S ∈ toPrecoverage_1.coverings X →
        (∀ ⦃Y : C⦄ (f : Y ⟶ X) (H : S f), Ti f H ∈ toPrecoverage_1.coverings Y) →
          S.bind Ti ∈ toPrecoverage_1.coverings X),
  ({ toPrecoverage := toPrecoverage, has_isos := has_isos, pullbacks := pullbacks, transitive := transitive } =
      { toPrecoverage := toPrecoverage_1, has_isos := has_isos_1, pullbacks := pullbacks_1,
        transitive := transitive_1 }) =
    (toPrecoverage = toPrecoverage_1)
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.instCategoryWithWeakEquivalencesOver : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (S : C) →
      [HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        HomotopicalAlgebra.CategoryWithWeakEquivalences (CategoryTheory.Over S)
-- Batteries.Classes.Order
Std.OrientedOrd.instOn : ∀ {β : Type u_1} {α : Type u_2} [ord : Ord β] [Std.OrientedOrd β] (f : α → β), Std.OrientedOrd α
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.coe_subtype : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (L : BooleanSubalgebra α), ⇑L.subtype = Subtype.val
-- Mathlib.MeasureTheory.OuterMeasure.Defs
MeasureTheory.OuterMeasure.empty : ∀ {α : Type u_2} (self : MeasureTheory.OuterMeasure α), self.measureOf ∅ = 0
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomain_zero : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] (f : M → N), AddMonoidAlgebra.mapDomain f 0 = 0
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_roc_eq_none_iff : ∀ {m n i : ℕ}, (m<...=n).toArray[i]? = none ↔ n ≤ i + m
-- Std.Data.TreeMap.Raw.Basic
Std.TreeMap.Raw.Equiv.mk : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeMap.Raw α β cmp},
  m₁.inner.Equiv m₂.inner → m₁.Equiv m₂
-- Mathlib.Algebra.Group.Subgroup.Map
/-- The preimage of an `AddSubgroup` along an `AddMonoid` homomorphism
is an `AddSubgroup`.  -/
AddSubgroup.comap : {G : Type u_1} → [inst : AddGroup G] → {N : Type u_7} → [inst_1 : AddGroup N] → (G →+ N) → AddSubgroup N → AddSubgroup G
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
/-- The composition of two pushforward functors on categories of sheaves of modules
identify to the pushforward for the composition.  -/
SheafOfModules.pushforwardComp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {D' : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} D'] →
            {J : CategoryTheory.GrothendieckTopology C} →
              {K : CategoryTheory.GrothendieckTopology D} →
                {F : CategoryTheory.Functor C D} →
                  {S : CategoryTheory.Sheaf J RingCat} →
                    {R : CategoryTheory.Sheaf K RingCat} →
                      [inst_3 : F.IsContinuous J K] →
                        (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                          {K' : CategoryTheory.GrothendieckTopology D'} →
                            {G : CategoryTheory.Functor D D'} →
                              {R' : CategoryTheory.Sheaf K' RingCat} →
                                [inst_4 : G.IsContinuous K K'] →
                                  (ψ : R ⟶ (G.sheafPushforwardContinuous RingCat K K').obj R') →
                                    (SheafOfModules.pushforward ψ).comp (SheafOfModules.pushforward φ) ≅
                                      SheafOfModules.pushforward
                                        (CategoryTheory.CategoryStruct.comp φ
                                          ((F.sheafPushforwardContinuous RingCat J K).map ψ))
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PullbackContinuous
/-- Given a continuous functor between sites `F`, and a morphism of sheaves of rings
`S ⟶ (F.sheafPushforwardContinuous RingCat.{u} J K).obj R`, this is the adjunction
between the corresponding pullback and pushforward functors on the categories
of sheaves of modules.  -/
SheafOfModules.pullbackPushforwardAdjunction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {K : CategoryTheory.GrothendieckTopology D} →
            {F : CategoryTheory.Functor C D} →
              {S : CategoryTheory.Sheaf J RingCat} →
                {R : CategoryTheory.Sheaf K RingCat} →
                  [inst_2 : F.IsContinuous J K] →
                    (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) →
                      [inst_3 : (SheafOfModules.pushforward φ).IsRightAdjoint] →
                        SheafOfModules.pullback φ ⊣ SheafOfModules.pushforward φ
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.delayLink : Lean.StrLit → Lean.ElabInline
-- Init.Prelude
/-- Converts a natural number to an 8-bit unsigned integer. Requires a proof that the number is small
enough to be representable without overflow; it must be smaller than `2^8`.

This function is overridden at runtime with an efficient implementation.
 -/
UInt8.ofNatLT : (n : ℕ) → n < UInt8.size → UInt8
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Sum of a list of elements in a `Subsemiring` is in the `Subsemiring`.  -/
Subsemiring.list_sum_mem : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) {l : List R}, (∀ x ∈ l, x ∈ s) → l.sum ∈ s
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.compare_minKey?_modify_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k : α} {f : β → β} {km kmm : α} (hkm : t.minKey? = some km),
  (Std.DTreeMap.Raw.Const.modify t k f).minKey?.get ⋯ = kmm → cmp kmm km = Ordering.eq
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
InnerProductSpace.gramSchmidt.congr_simp : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] (f f_1 : ι → E),
  f = f_1 → ∀ (n n_1 : ι), n = n_1 → InnerProductSpace.gramSchmidt 𝕜 f n = InnerProductSpace.gramSchmidt 𝕜 f_1 n_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], (t₁ ∩ t₂)[k]! = if k ∈ t₂ then t₁[k]! else default
-- Mathlib.Algebra.GCDMonoid.IntegrallyClosed
IsLocalization.surj_of_gcd_domain : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] [inst_3 : GCDMonoid R]
  (M : Submonoid R) [IsLocalization M A] (z : A), ∃ a b, IsUnit (gcd a b) ∧ z * (algebraMap R A) b = (algebraMap R A) a
-- Mathlib.Data.Rat.Cast.CharZero
NNRat.cast_mul : ∀ {α : Type u_3} [inst : DivisionSemiring α] [CharZero α] (p q : ℚ≥0), ↑(p * q) = ↑p * ↑q
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ker_residue : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsLocalRing R],
  RingHom.ker (IsLocalRing.residue R) = IsLocalRing.maximalIdeal R
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.map.congr_simp : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (S : Type u_4)
  [inst_3 : CommSemiring S] {N : Type u_5} [inst_4 : AddCommMonoid N] [inst_5 : Module R N] [inst_6 : Module S N]
  (f f_1 : M →ₗ[R] N),
  f = f_1 →
    ∀ [inst_7 : Algebra R S] [inst_8 : IsScalarTower R S N], DividedPowerAlgebra.map S f = DividedPowerAlgebra.map S f_1
-- Mathlib.Algebra.Order.Group.Equiv
toEquiv_ofLexMulEquiv : ∀ (α : Type u_1) [inst : Mul α], ↑(ofLexMulEquiv α) = ofLex
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mk_eq : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {m m' : M} {s s' : ↥S}, LocalizedModule.mk m s = LocalizedModule.mk m' s' ↔ ∃ u, u • s' • m = u • s • m'
-- Mathlib.Order.ModularLattice
/-- A generalization of the theorem that if `N` is a submodule of `M` and
`N` and `M / N` are both Noetherian, then `M` is Noetherian.  -/
wellFounded_gt_exact_sequence : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {β : Type u_2} {γ : Type u_3} [inst_2 : Preorder β]
  [inst_3 : Preorder γ] [WellFoundedGT β] [WellFoundedGT γ] (K : α) (f₁ : β → α) (f₂ : α → β) (g₁ : γ → α) (g₂ : α → γ)
  (gci : GaloisCoinsertion f₁ f₂) (gi : GaloisInsertion g₂ g₁),
  (∀ (a : α), f₁ (f₂ a) = a ⊓ K) → (∀ (a : α), g₁ (g₂ a) = a ⊔ K) → WellFoundedGT α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get?_eq_some_getD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} {fallback : β a}, a ∈ t → t.get? a = some (t.getD a fallback)
-- Mathlib.CategoryTheory.Types.Basic
/-- The concrete category instance on `Type u`.

Note: sometimes one needs to specify explicitly `(CC := fun X ↦ X)` to help typeclass inference.
 -/
instConcreteCategoryTypeFun : CategoryTheory.ConcreteCategory (Type u) TypeCat.Fun
-- Qq.Typ
Qq.instInhabitedQuoted : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-- Mathlib.Order.CompleteLattice.Basic
biInf_inf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α} {a : α},
  (∃ i, p i) → (⨅ i, ⨅ (h : p i), f i h) ⊓ a = ⨅ i, ⨅ (h : p i), f i h ⊓ a
-- Mathlib.Data.Finset.Grade
Finset.coe_wcovBy_coe : ∀ {α : Type u_1} {s t : Finset α}, ↑s ⩿ ↑t ↔ s ⩿ t
-- Lean.CoreM
/-- This ref exists to break a linking cycle that goes as follows:
- We start in `Environment.lean`, there we have functions referencing the compiler such as
  `evalConst`
- This pulls in the entire compiler transitively as well as all of its dependents
- The compiler relies on things like WHNF to inspect types
- WHNF in turn imports Environment

On Windows this causes a large amount of symbols to be included in one DLL as everything that
imports the Environment instantly requires a large chunk of the Meta stack to be linked. This ref
breaks the cycle by making `compileDeclsImpl` a "dynamic" call through the ref that is not visible
to the linker. In the compiler there is a matching `builtin_initialize` to set this ref to the
actual implementation of compileDeclsRef.
 -/
Lean.compileDeclsRef : IO.Ref (Array Lean.Name → Lean.Options → Lean.CoreM Unit)
-- Mathlib.FieldTheory.IntermediateField.Basic
Subfield.le_extendScalars_iff : ∀ {L : Type u_2} [inst : Field L] {F E : Subfield L} (h : F ≤ E) (E' : IntermediateField (↥F) L),
  E' ≤ Subfield.extendScalars h ↔ E'.toSubfield ≤ E
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendRestrictScalarsAdj.Counit.map_apply_one_tmul : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {Y : ModuleCat S} (y : ↑Y),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.ExtendRestrictScalarsAdj.Counit.map f)) (1 ⊗ₜ[R] y) = y
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicatorAux_one : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α) {x : α}, x ∈ E → thickenedIndicatorAux δ E x = 1
-- Lean.Elab.Tactic.Grind.Basic
_private.Lean.Elab.Tactic.Grind.Basic.0.Lean.Elab.Tactic.Grind.evalGrindTactic.throwExs : Lean.Syntax → Array Lean.Elab.Tactic.Grind.EvalTacticFailure → Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.tensorHom_comp_tensorHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  {X₁ Y₁ Z₁ X₂ Y₂ Z₂ : CategoryTheory.Arrow C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂) (g₁ : Y₁ ⟶ Z₁) (g₂ : Y₂ ⟶ Z₂),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂)
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g₁ g₂) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.comp f₁ g₁)
      (CategoryTheory.CategoryStruct.comp f₂ g₂)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
/-- The sphere `s₁` is internally tangent to the sphere `s₂` at the point `p` (that is, `s₁` lies
inside `s₂` and is tangent to it at that point). This includes the degenerate case where the
spheres are the same.  -/
EuclideanGeometry.Sphere.IsIntTangentAt : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [NormedAddTorsor V P] → EuclideanGeometry.Sphere P → EuclideanGeometry.Sphere P → P → Prop
-- Mathlib.Algebra.Homology.ShortComplex.ShortExact
/-- A choice of splitting for a short exact short complex `S` in a balanced category
such that `S.X₁` is injective.  -/
CategoryTheory.ShortComplex.ShortExact.splittingOfInjective : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} →
        S.ShortExact → [CategoryTheory.Injective S.X₁] → [CategoryTheory.Balanced C] → S.Splitting
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.sigmaMk_apply : ∀ {α : Type u_1} {β : α → Type u_3} (a : α) (snd : β a), (Function.Embedding.sigmaMk a) snd = ⟨a, snd⟩
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U_neg_one : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.U R (-1) = 0
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
/-- Given `c = lineMap a b r`, `a < c < b`, the point `(c, f c)` is strictly below the
segment `[(a, f a), (b, f b)]` if and only if `slope f a c < slope f c b`.  -/
map_lt_lineMap_iff_slope_lt_slope : ∀ {k : Type u_1} {E : Type u_2} [inst : Field k] [inst_1 : LinearOrder k] [IsStrictOrderedRing k]
  [inst_3 : AddCommGroup E] [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E]
  [IsStrictOrderedModule k E] [PosSMulReflectLE k E] {f : k → E} {a b r : k},
  a < b →
    0 < r →
      r < 1 →
        (f ((AffineMap.lineMap a b) r) < (AffineMap.lineMap (f a) (f b)) r ↔
          slope f a ((AffineMap.lineMap a b) r) < slope f ((AffineMap.lineMap a b) r) b)
-- Mathlib.CategoryTheory.Profunctor.Basic
/-- A profunctor from C to D (`Profunctor.{w} C D`) is a bifunctor `C ⥤ Dᵒᵖ ⥤ Type w`.  -/
CategoryTheory.Profunctor : (C : Type u₁) →
  (D : Type u₂) →
    [CategoryTheory.Category.{v₁, u₁} C] →
      [CategoryTheory.Category.{v₂, u₂} D] → Type (max v₁ (max u₂ w) u₁ (max (max (w + 1) u₂) w) v₂)
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.id_whisker_left : ∀ {B : Type u} [inst : Quiver B] {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b}
  (η : CategoryTheory.FreeBicategory.Hom₂ f g),
  CategoryTheory.FreeBicategory.Rel
    (CategoryTheory.FreeBicategory.Hom₂.whisker_left (CategoryTheory.FreeBicategory.Hom.id a) η)
    ((CategoryTheory.FreeBicategory.Hom₂.left_unitor f).vcomp
      (η.vcomp (CategoryTheory.FreeBicategory.Hom₂.left_unitor_inv g)))
-- Mathlib.GroupTheory.OrderOfElement
Prod.orderOf_mk : ∀ {α : Type u_4} {β : Type u_5} [inst : Monoid α] [inst_1 : Monoid β] {a : α} {b : β},
  orderOf (a, b) = (orderOf a).lcm (orderOf b)
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.top_arrow_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B : C}, CategoryTheory.IsIso ⊤.arrow
-- Mathlib.MeasureTheory.Integral.IntegrableOn
integrableOn_Ioc_iff_integrableOn_Ioo : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} [inst : PartialOrder α] [MeasurableSingletonClass α]
  [inst_2 : TopologicalSpace ε'] [inst_3 : ESeminormedAddMonoid ε'] [TopologicalSpace.PseudoMetrizableSpace ε']
  {f : α → ε'} {μ : MeasureTheory.Measure α} {a b : α} [MeasureTheory.NullSingletonClass μ],
  autoParam (‖f b‖ₑ ≠ ⊤) integrableOn_Ioc_iff_integrableOn_Ioo._auto_1 →
    (MeasureTheory.IntegrableOn f (Set.Ioc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioo a b) μ)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_neg : ∀ {α : Type u_1} {F : Type u_5} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup F] (f : α → F) (p : ENNReal)
  (μ : MeasureTheory.Measure α), MeasureTheory.eLpNorm (-f) p μ = MeasureTheory.eLpNorm f p μ
-- Init.Data.Array.Lemmas
Array.setIfInBounds_append_right : ∀ {α : Type u_1} {xs ys : Array α} {i : ℕ} {x : α},
  xs.size ≤ i → (xs ++ ys).setIfInBounds i x = xs ++ ys.setIfInBounds (i - xs.size) x
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.Respects.mk : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.MorphismProperty C}
  [toRespectsLeft : P.RespectsLeft Q] [toRespectsRight : P.RespectsRight Q], P.Respects Q
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.adjoin_le_iff : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {S : StarSubalgebra R A} {s : Set A},
  StarAlgebra.adjoin R s ≤ S ↔ s ⊆ ↑S
-- Mathlib.Topology.Sheaves.Sheaf
/-- The underlying presheaf of a sheaf  -/
TopCat.Sheaf.presheaf : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X : TopCat} → TopCat.Sheaf C X → TopCat.Presheaf C X
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.instHasStrongEpiImages : CategoryTheory.Limits.HasStrongEpiImages SimplexCategory
-- Std.Data.ExtDHashMap.Basic
/-- Internal implementation detail of the hash map.  -/
Std.ExtDHashMap.lift : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        {γ : Sort w} →
          (f : Std.DHashMap α β → γ) → (∀ (a b : Std.DHashMap α β), a.Equiv b → f a = f b) → Std.ExtDHashMap α β → γ
-- Mathlib.Data.Multiset.Filter
Multiset.Nodup.filter : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] {s : Multiset α}, s.Nodup → (Multiset.filter p s).Nodup