mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- Given two commutative squares
```
a --φ--> b --ψ--> c
|        |        |
v        v        v
R --f--> S --g--> T
```
such that `φ ≫ ψ` and `φ` are strongly co-Cartesian, then so is `ψ`.  -/
CategoryTheory.Functor.IsStronglyCocartesian.of_comp : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S T : 𝒮} {a b c : 𝒳} {f : R ⟶ S} {g : S ⟶ T} {φ : a ⟶ b} {ψ : b ⟶ c}
  [p.IsStronglyCocartesian f φ]
  [p.IsStronglyCocartesian (CategoryTheory.CategoryStruct.comp f g) (CategoryTheory.CategoryStruct.comp φ ψ)]
  [p.IsHomLift g ψ], p.IsStronglyCocartesian g ψ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Inhabited α] {k k' : α} {f : Option β → Option β} {hc : k' ∈ Std.ExtDTreeMap.Const.alter t k f},
  (Std.ExtDTreeMap.Const.alter t k f).getKey k' hc = if heq : cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
FundamentalGroupoidFunctor.piIso_hom : ∀ {I : Type u} (X : I → TopCat), (FundamentalGroupoidFunctor.piIso X).hom = FundamentalGroupoidFunctor.piToPiTop X
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.toPresheafFiberNatTrans_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X)
  (P : CategoryTheory.Functor Cᵒᵖ A), (Φ.toPresheafFiberNatTrans X x).app P = Φ.toPresheafFiber X x P
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- If the unit and counit for the adjunction corresponding to a right adjoint functor are (pointwise)
isomorphisms, then the functor is an equivalence of categories.
 -/
CategoryTheory.Functor.isEquivalence_of_isRightAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [inst_2 : G.IsRightAdjoint]
  [∀ (X : D), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofIsRightAdjoint G).unit.app X)]
  [∀ (Y : C), CategoryTheory.IsIso ((CategoryTheory.Adjunction.ofIsRightAdjoint G).counit.app Y)], G.IsEquivalence
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.class : Lean.Lsp.SymbolKind
-- Mathlib.Algebra.Group.Prod
/-- Multiplying by the trivial monoid doesn't change the
structure.

This is the `AddEquiv` version of `Equiv.prodUnique`.  -/
AddEquiv.prodUnique : {M : Type u_3} → {N : Type u_4} → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → [Unique N] → M × N ≃+ M
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.nnnorm_seminormedAddCommGroupToProd : ∀ (p : ENNReal) [hp : Fact (1 ≤ p)] (α : Type u_4) (β : Type u_5) [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (x : α × β), ‖x‖₊ = ‖WithLp.toLp p x‖₊
-- Mathlib.Topology.MetricSpace.Bounded
/-- Extension for the `positivity` tactic: the diameter of a set is always nonnegative.  -/
Mathlib.Meta.Positivity.evalDiam : Mathlib.Meta.Positivity.PositivityExt
-- Mathlib.RingTheory.DividedPowers.Padic
_private.Mathlib.RingTheory.DividedPowers.Padic.0.PadicInt.dpow'_int : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ) {x : ℤ_[p]}, x ∈ Ideal.span {↑p} → ‖PadicInt.dpow'✝ p n ↑x‖ ≤ 1
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type with inverse that satisfies `(f⁻¹) x = (f x)⁻¹` is an involutive inversion
if `β` is an involutive inversion.  -/
FunLike.involutiveInv : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] → [inst_1 : Inv F] → [inst_2 : InvolutiveInv β] → [IsInvApply F α β] → InvolutiveInv F
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
SemiNormedGrp.Hom.Simps.hom : (M N : SemiNormedGrp) → M.Hom N → NormedAddGroupHom M.carrier N.carrier
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ContInfo.toContInfoRefImpl : Lean.Elab.Do.ContInfo → Lean.Elab.Do.ContInfoRef
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.instNormOneClass : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A], NormOneClass (Unitization 𝕜 A)
-- Init.Data.SInt.Lemmas
ISize.toISize_toInt64 : ∀ (n : ISize), n.toInt64.toISize = n
-- Mathlib.Data.Part
Part.one_mem_one : ∀ {α : Type u_1} [inst : One α], 1 ∈ 1
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Controlling the norm of `f.iteratedFDeriv` when `f` is continuous multilinear. For the same
bound on the iterated derivative of `f` in the calculus sense,
see `ContinuousMultilinearMap.norm_iteratedFDeriv_le`.  -/
ContinuousMultilinearMap.norm_iteratedFDeriv_le' : ∀ {𝕜 : Type u} {ι : Type v} {E₁ : ι → Type wE₁} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_3 : SeminormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] [inst_5 : Fintype ι]
  (f : ContinuousMultilinearMap 𝕜 E₁ G) (k : ℕ) (x : (i : ι) → E₁ i),
  ‖f.iteratedFDeriv k x‖ ≤ ↑((Fintype.card ι).descFactorial k) * ‖f‖ * ‖x‖ ^ (Fintype.card ι - k)
-- Mathlib.Data.Rat.Lemmas
Rat.inv_natCast_den : ∀ (a : ℕ), (↑a)⁻¹.den = if a = 0 then 1 else a
-- Mathlib.Data.Set.Basic
SetCoe.forall : ∀ {α : Type u} {s : Set α} {p : ↑s → Prop}, (∀ (x : ↑s), p x) ↔ ∀ (x : α) (h : x ∈ s), p ⟨x, h⟩
-- Init.Data.Range.Polymorphic.PRange
Std.Roc.LawfulRcoIntersection.mk : ∀ {α : Type w} [inst : LT α] [inst_1 : LE α] [inst_2 : Std.Roc.HasRcoIntersection α],
  (∀ {a : α} {r : Std.Roc α} {s : Std.Rco α}, a ∈ Std.Roc.HasRcoIntersection.intersection r s ↔ a ∈ r ∧ a ∈ s) →
    Std.Roc.LawfulRcoIntersection α
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instMulOneClassOfContinuousMul.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : MulOneClass β]
  [inst_3 : ContinuousMul β],
  ContinuousMap.instMulOneClassOfContinuousMul =
    { toOne := ContinuousMap.instOne, toMul := ContinuousMap.instMul, one_mul := ⋯, mul_one := ⋯ }
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
/-- If a function `f` is locally integrable on a set `s` in a second countable topological space,
then there exist countably many open sets `u` covering `s` such that `f` is integrable on each
set `u ∩ s`.  -/
MeasureTheory.LocallyIntegrableOn.exists_countable_integrableOn : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} {s : Set X} [SecondCountableTopology X],
  MeasureTheory.LocallyIntegrableOn f s μ →
    ∃ T, T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, MeasureTheory.IntegrableOn f (u ∩ s) μ
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multiequalizer.hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  {I : CategoryTheory.Limits.MulticospanIndex J C} [inst_1 : CategoryTheory.Limits.HasMultiequalizer I] {W : C}
  {i j : W ⟶ CategoryTheory.Limits.multiequalizer I},
  i = j ↔
    ∀ (a : J.L),
      CategoryTheory.CategoryStruct.comp i (CategoryTheory.Limits.Multiequalizer.ι I a) =
        CategoryTheory.CategoryStruct.comp j (CategoryTheory.Limits.Multiequalizer.ι I a)
-- Mathlib.Algebra.BigOperators.Fin
Fin.prod_Iic_cast : ∀ {M : Type u_2} [inst : CommMonoid M] {n m : ℕ} (h : n = m) (f : Fin m → M) (a : Fin n),
  ∏ i ≤ Fin.cast h a, f i = ∏ i ≤ a, f (Fin.cast h i)
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.instBot.eq_1 : ∀ {M : Type u_1} [inst : Add M], AddSubsemigroup.instBot = { bot := { carrier := ∅, add_mem' := ⋯ } }
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_eq_univ_sdiff : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (s : Finset α), sᶜ = Finset.univ \ s
-- Mathlib.FieldTheory.SeparableDegree
/-- A random bijection between `Field.Emb F E` and `E →ₐ[F] K` when `E / F` is algebraic
and `K / F` is algebraically closed.  -/
Field.embEquivOfIsAlgClosed : (F : Type u) →
  (E : Type v) →
    [inst : Field F] →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          (K : Type w) →
            [inst_3 : Field K] →
              [inst_4 : Algebra F K] → [Algebra.IsAlgebraic F E] → [IsAlgClosed K] → Field.Emb F E ≃ (E →ₐ[F] K)
-- Init.Data.Slice.Array.Iterator
Subarray.sliceToArray_eq_toArray : ∀ {α : Type u} {s : Subarray α}, Std.Slice.toArray s = Std.Slice.toArray s
-- Mathlib.RingTheory.SimpleRing.Congr
isSimpleRing_iff_isTwoSided_imp : ∀ {R : Type u_1} [inst : Ring R], IsSimpleRing R ↔ Nontrivial R ∧ ∀ (I : Ideal R), I.IsTwoSided → I = ⊥ ∨ I = ⊤
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
/-- Extract one bit at a time from the initial vector, zero-extend it to width `w`,
and append it the result to `acc`, which eventually will have size `outWidth = w * w` -/
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtend : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {outWidth : ℕ} →
        (aig : Std.Sat.AIG α) →
          Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget aig outWidth →
            Std.Sat.AIG.RefVecEntry α outWidth
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.bijective : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N), Function.Bijective ⇑e
-- Init.Data.Int.Lemmas
Int.negOfNat_add : ∀ (m n : ℕ), Int.negOfNat m + Int.negOfNat n = Int.negOfNat (m + n)
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal_εIso : ∀ {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]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal]
  [inst_5 : CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.η F)]
  [inst_6 : ∀ (X Y : C), CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.δ F X Y)],
  (CategoryTheory.Functor.CoreMonoidal.ofOplaxMonoidal F).εIso =
    (CategoryTheory.asIso (CategoryTheory.Functor.OplaxMonoidal.η F)).symm
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_sub_iff_add_lt' : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b c : α}, b < c - a ↔ a + b < c
-- Mathlib.Analysis.InnerProductSpace.Projection.Minimal
/-- Existence of projections on complete subspaces.
Let `u` be a point in an inner product space, and let `K` be a nonempty complete subspace.
Then there exists a (unique) `v` in `K` that minimizes the distance `‖u - v‖` to `u`.
This point `v` is usually called the orthogonal projection of `u` onto `K`.
 -/
Submodule.exists_norm_eq_iInf_of_complete_subspace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E), IsComplete ↑K → ∀ (u : E), ∃ v ∈ K, ‖u - v‖ = ⨅ w, ‖u - ↑w‖
-- Mathlib.SetTheory.ZFC.PSet
PSet.Equiv.exists_left : ∀ {x : PSet.{u_1}} {y : PSet.{u_2}}, x.Equiv y → ∀ (i : x.Type), ∃ j, (x.Func i).Equiv (y.Func j)
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- `HahnEmbedding.Partial` as an `OrderedAddMonoidHom`.  -/
HahnEmbedding.Partial.toOrderAddMonoidHom : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              {seed : HahnEmbedding.Seed K M R} →
                                (f : HahnEmbedding.Partial seed) →
                                  ↥(↑f).domain →+o Lex (HahnSeries (FiniteArchimedeanClass M) R)
-- Mathlib.Logic.Equiv.Defs
Equiv.congr_arg : ∀ {α : Sort u} {β : Sort v} {f : α ≃ β} {x x' : α}, x = x' → f x = f x'
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.toPoly'.go.eq_def : ∀ (coeff : ℤ) (a : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Expr.toPoly'.go coeff a =
    match (motive := Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly) a with
    | Lean.Grind.Linarith.Expr.zero => id
    | Lean.Grind.Linarith.Expr.var v => fun x => Lean.Grind.Linarith.Poly.add coeff v x
    | a.add b => Lean.Grind.Linarith.Expr.toPoly'.go coeff a ∘ Lean.Grind.Linarith.Expr.toPoly'.go coeff b
    | a.sub b => Lean.Grind.Linarith.Expr.toPoly'.go coeff a ∘ Lean.Grind.Linarith.Expr.toPoly'.go (-coeff) b
    | Lean.Grind.Linarith.Expr.natMul k a =>
      bif k == 0 then id else Lean.Grind.Linarith.Expr.toPoly'.go (coeff.mul ↑k) a
    | Lean.Grind.Linarith.Expr.intMul k a => bif k == 0 then id else Lean.Grind.Linarith.Expr.toPoly'.go (coeff.mul k) a
    | a.neg => Lean.Grind.Linarith.Expr.toPoly'.go (-coeff) a
-- Mathlib.Topology.OpenPartialHomeomorph.IsImage
OpenPartialHomeomorph.ofSet_target : ∀ {X : Type u_1} [inst : TopologicalSpace X] (s : Set X) (hs : IsOpen s), (OpenPartialHomeomorph.ofSet s hs).target = s
-- Aesop.Builder.Basic
Aesop.RuleBuilderInput.mk.sizeOf_spec : ∀ (term : Lean.Term) (options : Aesop.RuleBuilderOptions) (phase : Aesop.PhaseSpec),
  sizeOf { term := term, options := options, phase := phase } = 1 + sizeOf term + sizeOf options + sizeOf phase
-- Mathlib.Algebra.Field.Basic
/-- Pullback a `DivisionSemiring` along an injective function.  -/
Function.Injective.divisionSemiring : {K : Type u_1} →
  {L : Type u_2} →
    [inst : Zero K] →
      [inst_1 : Add K] →
        [inst_2 : One K] →
          [inst_3 : Mul K] →
            [inst_4 : Inv K] →
              [inst_5 : Div K] →
                [inst_6 : SMul ℕ K] →
                  [inst_7 : SMul ℚ≥0 K] →
                    [inst_8 : Pow K ℕ] →
                      [inst_9 : Pow K ℤ] →
                        [inst_10 : NatCast K] →
                          [inst_11 : NNRatCast K] →
                            (f : K → L) →
                              Function.Injective f →
                                [inst_12 : DivisionSemiring L] →
                                  f 0 = 0 →
                                    f 1 = 1 →
                                      (∀ (x y : K), f (x + y) = f x + f y) →
                                        (∀ (x y : K), f (x * y) = f x * f y) →
                                          (∀ (x : K), f x⁻¹ = (f x)⁻¹) →
                                            (∀ (x y : K), f (x / y) = f x / f y) →
                                              (∀ (n : ℕ) (x : K), f (n • x) = n • f x) →
                                                (∀ (q : ℚ≥0) (x : K), f (q • x) = q • f x) →
                                                  (∀ (x : K) (n : ℕ), f (x ^ n) = f x ^ n) →
                                                    (∀ (x : K) (n : ℤ), f (x ^ n) = f x ^ n) →
                                                      (∀ (n : ℕ), f ↑n = ↑n) →
                                                        (∀ (q : ℚ≥0), f ↑q = ↑q) → DivisionSemiring K
-- Mathlib.NumberTheory.Chebyshev
/-- A weak but completely explicit upper bound on $\pi(x)$.  -/
Chebyshev.pi_le_log4_mul_div : ∀ {x : ℝ}, 1 < x → ↑⌊x⌋₊.primeCounting ≤ Real.log 4 * x / Real.log √x + √x
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instIsScalarTowerPreLp : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedRing 𝕜] [inst_2 : NormedRing 𝕜'] [inst_3 : (i : α) → Module 𝕜 (E i)]
  [inst_4 : (i : α) → Module 𝕜' (E i)] [inst_5 : SMul 𝕜' 𝕜] [∀ (i : α), IsScalarTower 𝕜' 𝕜 (E i)],
  IsScalarTower 𝕜' 𝕜 (PreLp E)
-- Mathlib.Topology.Order.LeftRightLim
ContinuousWithinAt.rightLim_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace α]
  [OrderTopology α] [T2Space β] {f : α → β} {a : α}, ContinuousWithinAt f (Set.Ici a) a → Function.rightLim f a = f a
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
/-- The projections from a family of topological modules are continuous linear maps.  -/
ContinuousLinearMap.proj : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_4} →
      {φ : ι → Type u_5} →
        [inst_1 : (i : ι) → TopologicalSpace (φ i)] →
          [inst_2 : (i : ι) → AddCommMonoid (φ i)] →
            [inst_3 : (i : ι) → Module R (φ i)] → (i : ι) → ((i : ι) → φ i) →L[R] φ i
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
MDifferentiableWithinAt.sum_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {u : Set B} {x₀ : B}
  {ι : Type u_9} {s : Finset ι} {t : ι → (x : B) → E x},
  (∀ i ∈ s, MDiffAt[u] (T% t) x₀) → (MDiffAt[u] fun x => ⟨x, ∑ i ∈ s, t i x⟩) x₀
-- Mathlib.AlgebraicTopology.SimplicialObject.Coskeletal
CategoryTheory.SimplicialObject.isCoskeletal_iff_isIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ)
  [inst_1 :
    ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasRightKanExtension F],
  X.IsCoskeletal n ↔ CategoryTheory.IsIso ((CategoryTheory.SimplicialObject.coskAdj n).unit.app X)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.dvd_solve_elim_cert.match_1.splitter : (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) →
  (p₁ p₂ : Int.Internal.Linear.Poly) →
    ((a₁ : ℤ) →
        (x₁ : Int.Internal.Linear.Var) →
          (p₁ : Int.Internal.Linear.Poly) →
            (a₂ : ℤ) →
              (x₂ : Int.Internal.Linear.Var) →
                (p₂ : Int.Internal.Linear.Poly) →
                  motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂)) →
      ((x x_1 : Int.Internal.Linear.Poly) →
          (∀ (a₁ : ℤ) (x₁ : Int.Internal.Linear.Var) (p₁ : Int.Internal.Linear.Poly) (a₂ : ℤ)
              (x₂ : Int.Internal.Linear.Var) (p₂ : Int.Internal.Linear.Poly),
              x = Int.Internal.Linear.Poly.add a₁ x₁ p₁ → x_1 = Int.Internal.Linear.Poly.add a₂ x₂ p₂ → False) →
            motive x x_1) →
        motive p₁ p₂
-- Mathlib.Topology.Constructions
Pi.continuous_domRestrict : ∀ {ι : Type u_5} {A : ι → Type u_6} [T : (i : ι) → TopologicalSpace (A i)] (S : Set ι), Continuous S.domRestrict
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatchAt_iff : ∀ {pat : String} {s : String.Slice} {pos₁ pos₂ : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt pat pos₁ pos₂ ↔ ∃ (h : pos₁ ≤ pos₂), (s.slice pos₁ pos₂ h).copy = pat
-- Lean.Expr
Lean.mkApp7 : Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr
-- Init.Data.Array.MapIdx
Array.mapFinIdxM.map.congr_simp : ∀ {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (as : Array α)
  (f f_1 : (i : ℕ) → α → i < as.size → m β),
  f = f_1 →
    ∀ (i i_1 : ℕ) (e_i : i = i_1) (j j_1 : ℕ) (e_j : j = j_1) (inv : i + j = as.size) (bs bs_1 : Array β),
      bs = bs_1 → Array.mapFinIdxM.map as f i j inv bs = Array.mapFinIdxM.map as f_1 i_1 j_1 ⋯ bs_1
-- Mathlib.CategoryTheory.Localization.Triangulated
CategoryTheory.Functor.complete_distinguished_essImageDistTriang_morphism : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : CategoryTheory.Limits.HasZeroObject C] [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_6 : CategoryTheory.Pretriangulated C] [inst_7 : CategoryTheory.HasShift D ℤ] [inst_8 : L.CommShift ℤ],
  (∀ (T₁' T₂' : CategoryTheory.Pretriangulated.Triangle C),
      T₁' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
        T₂' ∈ CategoryTheory.Pretriangulated.distinguishedTriangles →
          ∀ (a : L.obj T₁'.obj₁ ⟶ L.obj T₂'.obj₁) (b : L.obj T₁'.obj₂ ⟶ L.obj T₂'.obj₂),
            CategoryTheory.CategoryStruct.comp (L.map T₁'.mor₁) b =
                CategoryTheory.CategoryStruct.comp a (L.map T₂'.mor₁) →
              ∃ φ, φ.hom₁ = a ∧ φ.hom₂ = b) →
    ∀ (T₁ T₂ : CategoryTheory.Pretriangulated.Triangle D),
      T₁ ∈ L.essImageDistTriang →
        T₂ ∈ L.essImageDistTriang →
          ∀ (a : T₁.obj₁ ⟶ T₂.obj₁) (b : T₁.obj₂ ⟶ T₂.obj₂),
            CategoryTheory.CategoryStruct.comp T₁.mor₁ b = CategoryTheory.CategoryStruct.comp a T₂.mor₁ →
              ∃ c,
                CategoryTheory.CategoryStruct.comp T₁.mor₂ c = CategoryTheory.CategoryStruct.comp b T₂.mor₂ ∧
                  CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor D 1).map a) =
                    CategoryTheory.CategoryStruct.comp c T₂.mor₃
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
Multiset.stronglyMeasurable_fun_prod : ∀ {α : Type u_1} {M : Type u_5} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M]
  {m : MeasurableSpace α} (s : Multiset (α → M)),
  (∀ f ∈ s, MeasureTheory.StronglyMeasurable f) →
    MeasureTheory.StronglyMeasurable fun x => (Multiset.map (fun f => f x) s).prod
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsLittleO.congr_of_sub : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {l : Filter α} {f₁ f₂ : α → E'}, (fun x => f₁ x - f₂ x) =o[l] g → (f₁ =o[l] g ↔ f₂ =o[l] g)
-- Mathlib.Tactic.CategoryTheory.Monoidal.PureCoherence
Mathlib.Tactic.Monoidal.naturality_tensorHom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {p f₁ g₁ f₂ g₂ pf₁ pf₁f₂ : C} {η : f₁ ≅ g₁} {θ : f₂ ≅ g₂}
  (η_f₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj p f₁ ≅ pf₁)
  (η_g₁ : CategoryTheory.MonoidalCategoryStruct.tensorObj p g₁ ≅ pf₁)
  (η_f₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj pf₁ f₂ ≅ pf₁f₂)
  (η_g₂ : CategoryTheory.MonoidalCategoryStruct.tensorObj pf₁ g₂ ≅ pf₁f₂),
  CategoryTheory.MonoidalCategory.whiskerLeftIso p η ≪≫ η_g₁ = η_f₁ →
    CategoryTheory.MonoidalCategory.whiskerLeftIso pf₁ θ ≪≫ η_g₂ = η_f₂ →
      CategoryTheory.MonoidalCategory.whiskerLeftIso p (CategoryTheory.MonoidalCategory.tensorIso η θ) ≪≫
          Mathlib.Tactic.Monoidal.normalizeIsoComp η_g₁ η_g₂ =
        Mathlib.Tactic.Monoidal.normalizeIsoComp η_f₁ η_f₂
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.succ.sizeOf_spec : sizeOf Nat.Partrec.Code.succ = 1
-- Mathlib.Logic.Equiv.Fin.Basic
/-- An equivalence that removes `i` and maps it to `none`.
This is a version of `Fin.predAbove` that produces `Option (Fin n)` instead of
mapping both `i.castSucc` and `i.succ` to `i`.  -/
finSuccEquiv' : {n : ℕ} → Fin (n + 1) → Fin (n + 1) ≃ Option (Fin n)