mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `s` is any limit kernel cone over `f` and if `i` is an isomorphism such that
`i.hom ≫ s.ι = l`, then `l` is a kernel of `f`.  -/
CategoryTheory.Limits.IsKernel.isoKernel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        (f : X ⟶ Y) →
          {Z : C} →
            (l : Z ⟶ X) →
              {s : CategoryTheory.Limits.KernelFork f} →
                CategoryTheory.Limits.IsLimit s →
                  (i : Z ≅ s.pt) →
                    (h : CategoryTheory.CategoryStruct.comp i.hom (CategoryTheory.Limits.Fork.ι s) = l) →
                      CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι l ⋯)
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.eq_of_toPoly_eq : ∀ (ctx : Nat.Internal.Linear.Context) (a b : Nat.Internal.SOM.Expr),
  (a.toPoly == b.toPoly) = true → Nat.Internal.SOM.Expr.denote ctx a = Nat.Internal.SOM.Expr.denote ctx b
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonTextEditBatch : Lean.FromJson Lean.Lsp.TextEditBatch
-- Mathlib.GroupTheory.SpecificGroups.Alternating.Simple
/-- The Iwasawa structure of `Perm α` acting on `Set.powersetCard α 2`.  -/
Equiv.Perm.iwasawaStructure_two : {α : Type u_1} →
  [Finite α] →
    [inst : DecidableEq α] →
      [(s : Set α) → DecidablePred fun x => x ∈ s] → MulAction.IwasawaStructure (Equiv.Perm α) ↑(Set.powersetCard α 2)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.cos_pos_iff_abs_toReal_lt_pi_div_two : ∀ {θ : Real.Angle}, 0 < θ.cos ↔ |θ.toReal| < Real.pi / 2
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
/-- An alternative colimit cocone in the functor category `K ⥤ C` in the case where `C` has
`J`-shaped colimits, with cocone point `F.flip ⋙ colim`.
 -/
CategoryTheory.Limits.pointwiseCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} J] →
        {K : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} K] →
            [CategoryTheory.Limits.HasColimitsOfShape J C] →
              (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) → CategoryTheory.Limits.Cocone F
-- Init.Data.Option.Lemmas
Option.join_ne_none : ∀ {α : Type u_1} {x : Option (Option α)}, x.join ≠ none ↔ ∃ z, x = some (some z)
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.symm_symm : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y), h.symm.symm = h
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
HomotopicalAlgebra.FibrantObject.instIsIsoFunctorResolutionCompToLocalizationNatTrans : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  [inst_3 : L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)],
  CategoryTheory.IsIso (HomotopicalAlgebra.FibrantObject.HoCat.resolutionCompToLocalizationNatTrans L)
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- On an open set, `f : ℂ → E` is analytic iff it is differentiable  -/
Complex.analyticOn_iff_differentiableOn : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {s : Set ℂ},
  IsOpen s → (AnalyticOn ℂ f s ↔ DifferentiableOn ℂ f s)
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.initial_fromInitialModel : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] [inst_1 : CategoryTheory.InitiallySmall J],
  (CategoryTheory.fromInitialModel J).Initial
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_ofList_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β} [inst : Inhabited β],
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l → (k, v) ∈ l → (Std.TreeMap.Raw.ofList l cmp)[k']! = v
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.normalizeIsoApp_eq : ∀ (C : Type u) (X : CategoryTheory.FreeMonoidalCategory C)
  (n : (CategoryTheory.Discrete ∘ CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject) C),
  CategoryTheory.FreeMonoidalCategory.normalizeIsoApp C X n =
    CategoryTheory.FreeMonoidalCategory.normalizeIsoApp' C X n.as
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isSome_getKey?_iff_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  (t.getKey? a).isSome = true ↔ a ∈ t
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Var.eq_of_revlex : ∀ {x₁ x₂ : Lean.Grind.CommRing.Var}, x₁.revlex x₂ = Ordering.eq → x₁ = x₂
-- Init.Internal.Order.Basic
Lean.Order.prod_sup : {α : Sort u} → {β : Sort v} → [Lean.Order.CompleteLattice α] → [Lean.Order.CompleteLattice β] → (α ×' β → Prop) → α ×' β
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Sinc
Real.sinc_le_inv_abs : ∀ {x : ℝ}, x ≠ 0 → Real.sinc x ≤ |x|⁻¹
-- Init.Data.Array.Attach
Array.flatMap_wfParam : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β},
  Array.flatMap f (wfParam xs) = Array.flatMap f xs.attach.unattach
-- Mathlib.Analysis.InnerProductSpace.Dual
InnerProductSpace.continuousLinearMapOfBilin.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : CompleteSpace E] (B : E →L⋆[𝕜] E →L[𝕜] 𝕜),
  InnerProductSpace.continuousLinearMapOfBilin B = ↑↑(InnerProductSpace.toDual 𝕜 E).symm ∘SL B
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapRange_multiset_sum : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] {F : Type u_12}
  [inst_2 : FunLike F M N] [inst_3 : AddMonoidHomClass F M N] (f : F) (m : Multiset (α →₀ M)),
  Finsupp.mapRange ⇑f ⋯ m.sum = (Multiset.map (fun x => Finsupp.mapRange ⇑f ⋯ x) m).sum
-- Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart
/-- `P` is a slightly generalized version of `Iᵢ` in
[the wikipedia proof](https://en.wikipedia.org/wiki/Lindemann%E2%80%93Weierstrass_theorem):
`Iᵢ(s) = P(fᵢ, s)`.
 -/
_private.Mathlib.NumberTheory.Transcendental.Lindemann.AnalyticalPart.0.LindemannWeierstrass.P : Polynomial ℂ → ℂ → ℂ
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.centralizer_smul_def : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] (g : Equiv.Perm α) (k : ↥(Subgroup.centralizer {g}))
  (c : ↥g.cycleFactorsFinset), k • c = ⟨↑k * ↑c * ↑k⁻¹, ⋯⟩
-- Mathlib.Data.Fin.SuccPred
/-- The `Fin.castSucc_zero` in `Lean` only applies in `Fin (n+1)`.
This one instead uses a `NeZero n` typeclass hypothesis.
 -/
Fin.castSucc_zero' : ∀ {n : ℕ} [inst : NeZero n], Fin.castSucc 0 = 0
-- Mathlib.Data.Set.Countable
/-- **Alias** of the forward direction of `Set.countable_iff_nonempty_encodable`. -/
Set.Countable.nonempty_encodable : ∀ {α : Type u} {s : Set α}, s.Countable → Nonempty (Encodable ↑s)
-- Lean.Elab.MutualDef
Lean.Elab.DefViewElabHeader.mk : Lean.Elab.DefView →
  Lean.Elab.DefViewElabHeaderData →
    Option (Lean.Language.SnapshotBundle Lean.Elab.Tactic.TacticParsedSnapshot) →
      Option (Lean.Language.SnapshotBundle (Option Lean.Elab.BodyProcessedSnapshot)) → Lean.Elab.DefViewElabHeader
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorRight_mapComp_hom_toNatTrans_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {a b c : CategoryTheory.Cat} (F : a ⟶ b) (G : b ⟶ c)
  (X : CategoryTheory.Join C ↑a),
  ((CategoryTheory.Join.pseudofunctorRight C).mapComp F G).hom.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp
      (match X with
      | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left x)
      | CategoryTheory.Join.right x =>
        CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right (G.toFunctor.obj (F.toFunctor.obj x))))
      ((CategoryTheory.Join.mapPairComp (CategoryTheory.Functor.id C) F.toFunctor (CategoryTheory.Functor.id C)
              G.toFunctor).hom.app
        X)
-- Mathlib.RingTheory.Coalgebra.TensorProduct
Coalgebra.TensorProduct.lid_symm_apply : ∀ {R : Type u_5} {P : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid P] [inst_2 : Module R P]
  [inst_3 : Coalgebra R P] (a : P), (Coalgebra.TensorProduct.lid R P).symm a = 1 ⊗ₜ[R] a
-- Mathlib.Analysis.SpecificLimits.FloorPow
/-- The sum of `1/⌊c^i⌋₊^2` above a threshold `j` is comparable to `1/j^2`, up to a multiplicative
constant.  -/
sum_div_nat_floor_pow_sq_le_div_sq : ∀ (N : ℕ) {j : ℝ},
  0 < j → ∀ {c : ℝ}, 1 < c → ∑ i ∈ Finset.range N with j < ↑⌊c ^ i⌋₊, 1 / ↑⌊c ^ i⌋₊ ^ 2 ≤ c ^ 5 * (c - 1)⁻¹ ^ 3 / j ^ 2
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.map.mk : ∀ {α : Type u} {L : List (α × Bool)} {β : Type v} {f : α → β},
  (FreeGroup.map f) (FreeGroup.mk L) = FreeGroup.mk (List.map (fun x => (f x.1, x.2)) L)
-- Mathlib.Data.Finset.Card
List.toFinset_card_le : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.toFinset.card ≤ l.length
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
_private.Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic.0.MeasureTheory.simpleFuncAux.eq_def : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSingletonClass α] (f : α → β) (g : ℕ → α)
  (x_1 : ℕ),
  MeasureTheory.simpleFuncAux✝ f g x_1 =
    match x_1 with
    | 0 => MeasureTheory.SimpleFunc.const α (f (g 0))
    | n.succ =>
      MeasureTheory.SimpleFunc.piecewise {g n} ⋯ (MeasureTheory.SimpleFunc.const α (f (g n)))
        (MeasureTheory.simpleFuncAux✝ f g n)
-- Mathlib.Analysis.Complex.HasPrimitives
/-- The `wedgeIntegral` has derivative at `z` equal to `f z`.  -/
Complex.IsConservativeOn.hasDerivAt_wedgeIntegral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {c : ℂ} {r : ℝ} {f : ℂ → E} [CompleteSpace E],
  ContinuousOn f (Metric.ball c r) →
    ∀ {z : ℂ},
      z ∈ Metric.ball c r →
        Complex.IsConservativeOn f (Metric.ball c r) → HasDerivAt (fun w => c.wedgeIntegral w f) (f z) z
-- Mathlib.Data.Setoid.Basic
Setoid.quotientKerEquivOfRightInverse_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (g : β → α) (hf : Function.RightInverse g f) (a : Quotient (Setoid.ker f)),
  (Setoid.quotientKerEquivOfRightInverse f g hf) a = Setoid.kerLift f a
-- Mathlib.Topology.ContinuousMap.Compact
/-- The norm of a function is controlled by the supremum of the pointwise norms.  -/
ContinuousMap.norm_le : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] (f : C(α, E)) {C : ℝ}, 0 ≤ C → (‖f‖ ≤ C ↔ ∀ (x : α), ‖f x‖ ≤ C)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.mk.inj : ∀ {R : Type u} {S : Type v} {inst : CommSemiring R} {inst_1 : Semiring S} {inst_2 : Algebra R S} {f : Polynomial R}
  {toIsAdjoinRoot : IsAdjoinRoot S f} {monic : f.Monic} {toIsAdjoinRoot_1 : IsAdjoinRoot S f} {monic_1 : f.Monic},
  { toIsAdjoinRoot := toIsAdjoinRoot, monic := monic } = { toIsAdjoinRoot := toIsAdjoinRoot_1, monic := monic_1 } →
    toIsAdjoinRoot = toIsAdjoinRoot_1
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- Given a measurable function `g : β → γ → δ`, and almost everywhere equal functions
`[f₁] : α →ₘ β` and `[f₂] : α →ₘ γ`, return the equivalence class of the function
`fun a => g (f₁ a) (f₂ a)`, i.e., the almost everywhere equal function
`[fun a => g (f₁ a) (f₂ a)] : α →ₘ γ`. This requires `δ` to have second-countable topology.  -/
MeasureTheory.AEEqFun.comp₂Measurable : {α : Type u_1} →
  {β : Type u_2} →
    {γ : Type u_3} →
      {δ : Type u_4} →
        [inst : MeasurableSpace α] →
          {μ : MeasureTheory.Measure α} →
            [inst_1 : TopologicalSpace δ] →
              [inst_2 : TopologicalSpace β] →
                [inst_3 : TopologicalSpace γ] →
                  [inst_4 : MeasurableSpace β] →
                    [TopologicalSpace.PseudoMetrizableSpace β] →
                      [BorelSpace β] →
                        [inst_7 : MeasurableSpace γ] →
                          [TopologicalSpace.PseudoMetrizableSpace γ] →
                            [BorelSpace γ] →
                              [SecondCountableTopologyEither β γ] →
                                [inst_11 : MeasurableSpace δ] →
                                  [TopologicalSpace.PseudoMetrizableSpace δ] →
                                    [OpensMeasurableSpace δ] →
                                      [SecondCountableTopology δ] →
                                        (g : β → γ → δ) →
                                          Measurable (Function.uncurry g) → (α →ₘ[μ] β) → (α →ₘ[μ] γ) → α →ₘ[μ] δ
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_coe_toEquiv_symm : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S),
  ⇑(↑e).symm = ⇑e.symm
-- Mathlib.LinearAlgebra.PiTensorProduct.DFinsupp
PiTensorProduct.ofDFinsuppEquiv_symm_single_tprod : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : (i : ι) → κ i → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)] [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)]
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] [inst_5 : (i : ι) → DecidableEq (κ i)] (p : (i : ι) → κ i)
  (x : (i : ι) → M i (p i)),
  (PiTensorProduct.ofDFinsuppEquiv.symm fun₀ | p => (PiTensorProduct.tprod R) x) =
    (PiTensorProduct.tprod R) fun i => fun₀ | p i => x i
-- Aesop.Script.StructureStatic
_private.Aesop.Script.StructureStatic.0.Aesop.Script.structureStaticCore.nextStep : Aesop.Script.TacticState → Aesop.GoalWithMVars → Aesop.Script.StaticStructureM Aesop.Script.Step
-- Mathlib.Topology.UniformSpace.UniformEmbedding
isUniformEmbedding_comap : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [u : UniformSpace β], Function.Injective f → IsUniformEmbedding f
-- Mathlib.Geometry.Manifold.VectorField.Pullback
/-- The pullback of a `C^m` vector field by a `C^n` function with invertible derivative and
with `m + 1 ≤ n` is `C^m`.
Version within a set at a point, with a set used for the pullback possibly larger.  -/
ContMDiffWithinAt.mpullbackWithin_vectorField' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {H' : Type u_5} [inst_6 : TopologicalSpace H']
  {E' : Type u_6} [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M} {x₀ : M}
  {V : (x : M') → TangentSpace I' x} {m n : WithTop ℕ∞} {t : Set M'} [CompleteSpace E] [inst_12 : IsManifold I 1 M]
  [inst_13 : IsManifold I' 1 M'] {u : Set M},
  ContMDiffWithinAt I' I'.tangent m (fun x => ⟨x, V x⟩) t (f x₀) →
    ContMDiffWithinAt I I' n f u x₀ →
      (mfderiv[u] f x₀).IsInvertible →
        x₀ ∈ s →
          UniqueMDiff[s] →
            m + 1 ≤ n →
              f ⁻¹' t ∈ nhdsWithin x₀ s →
                s ⊆ u → ContMDiffWithinAt I I.tangent m (fun x => ⟨x, VectorField.mpullbackWithin I I' f V u x⟩) s x₀
-- Init.Data.SInt.Basic
/-- Truncating division for 64-bit signed integers, rounding towards zero. Usually accessed via the `/`
operator.

Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.

Examples:
* `Int64.div 10 3 = 3`
* `Int64.div 10 (-3) = (-3)`
* `Int64.div (-10) (-3) = 3`
* `Int64.div (-10) 3 = (-3)`
* `Int64.div 10 0 = 0`
 -/
Int64.div : Int64 → Int64 → Int64
-- Mathlib.GroupTheory.Finiteness
AddSubmonoid.FG.sup : ∀ {M : Type u_1} [inst : AddMonoid M] {P Q : AddSubmonoid M}, P.FG → Q.FG → (P ⊔ Q).FG
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.ν_comp_unitDesc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  [hasDayConvolution :
    ∀ (F G : CategoryTheory.Functor C V),
      (CategoryTheory.MonoidalCategory.tensor C).HasPointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F G)]
  [hasDayConvolutionUnit :
    (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).HasPointwiseLeftKanExtension
      (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit V))]
  [inst_4 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow (CategoryTheory.MonoidalCategory.tensor C) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_6 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_7 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_8 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.Functor.id C).prod
            (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)))
          d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  [inst_9 :
    ∀ (v : V) (d : C × C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          ((CategoryTheory.MonoidalCategory.tensor C).prod (CategoryTheory.Functor.id C)) d)
        (CategoryTheory.MonoidalCategory.tensorRight v)]
  {F : CategoryTheory.MonoidalCategory.DayFunctor C V}
  (φ :
    CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶
      F.functor.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.DayFunctor.ν C V)
      ((CategoryTheory.MonoidalCategory.DayFunctor.unitDesc φ).natTrans.app
        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) =
    φ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k a : α} [inst_1 : Inhabited (β a)] {v : β k},
  (t.insert k v).get! a = if h : cmp k a = Ordering.eq then cast ⋯ v else t.get! a
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instBEqMon.beq.eq_2 : ∀ (a : Lean.Grind.CommRing.Power) (a_1 : Lean.Grind.CommRing.Mon) (b : Lean.Grind.CommRing.Power)
  (b_1 : Lean.Grind.CommRing.Mon),
  Lean.Grind.CommRing.instBEqMon.beq (Lean.Grind.CommRing.Mon.mult a a_1) (Lean.Grind.CommRing.Mon.mult b b_1) =
    (a == b && Lean.Grind.CommRing.instBEqMon.beq a_1 b_1)
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_mul_ge_length_sub_length' : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w₁ w₂ : W),
  cs.length w₂ - cs.length w₁ ≤ cs.length (w₁ * w₂)
-- Aesop.RuleTac.Forward.Basic
/-- Check whether the given name was generated by `forwardImplDetailHypName`.
We assume that nobody else adds hyps with the `forwardImplHypDetailPrefix`
prefix.
 -/
Aesop.isForwardImplDetailHypName : Lean.Name → Bool
-- Mathlib.Order.WellFounded
WellFounded.min.congr_simp : ∀ {α : Type u_1} {r r_1 : α → α → Prop} (e_r : r = r_1) (H : WellFounded r) (s s_1 : Set α) (e_s : s = s_1)
  (h : s.Nonempty), H.min s h = ⋯.min s_1 ⋯
-- Mathlib.Order.BooleanGenerators
/-- The elements in a collection of Boolean generators satisfy an atomicity condition:
any compact element below the supremum of a finite subset `s` of generators
is equal to the supremum of a subset of `s`.  -/
IsCompactlyGenerated.BooleanGenerators.finitelyAtomistic : ∀ {α : Type u_1} [inst : CompleteLattice α] {S : Set α},
  IsCompactlyGenerated.BooleanGenerators S →
    ∀ (s : Finset α) (a : α), ↑s ⊆ S → IsCompactElement a → a ≤ s.sup id → ∃ t ⊆ s, a = t.sup id
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.model_infiniteTheory : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] [h : Infinite M], M ⊨ L.infiniteTheory
-- Mathlib.Order.Filter.Lift
Filter.lift.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : Filter α) (g : Set α → Filter β), f.lift g = ⨅ s ∈ f, g s
-- Init.Data.UInt.Lemmas
UInt16.le_trans : ∀ {a b c : UInt16}, a ≤ b → b ≤ c → a ≤ c
-- Lean.Meta.Injective
_private.Lean.Meta.Injective.0.Lean.Meta.mkInjectiveTheoremType? : Lean.ConstructorVal → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
ModelWithCorners.uniqueDiffOn_extendCoordChange_source : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} {e e' : OpenPartialHomeomorph M H},
  UniqueDiffOn 𝕜 (ModelWithCorners.extendCoordChange e e').source
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α) (m : ℤ), toIocMod hp a (b - m • p) = toIocMod hp a b
-- Init.Data.Nat.Basic
Nat.add_lt_add : ∀ {a b c d : ℕ}, a < b → c < d → a + c < b + d
-- Mathlib.Data.Real.ConjExponents
Real.holderConjugate_iff_eq_conjExponent : ∀ {p q : ℝ}, 1 < p → (p.HolderConjugate q ↔ q = p / (p - 1))
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.Monoidal.μ_of_cartesianMonoidalCategory : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Monoidal] [inst_5 : CategoryTheory.Limits.PreservesFiniteProducts F]
  (X Y : C),
  CategoryTheory.Functor.LaxMonoidal.μ F X Y = (CategoryTheory.CartesianMonoidalCategory.prodComparisonIso F X Y).inv
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_ofNatClamp_of_lt : ∀ {n : ℕ}, n < UInt32.size → (UInt32.ofNatClamp n).toUInt8 = UInt8.ofNat n
-- Mathlib.Algebra.Group.Finsupp
Finsupp.support_sub : ∀ {ι : Type u_1} {G : Type u_6} [inst : AddGroup G] [inst_1 : DecidableEq ι] {f g : ι →₀ G},
  (f - g).support ⊆ f.support ∪ g.support
-- Mathlib.Tactic.Positivity.Basic
/-- Extension for the `positivity` tactic: `Int.natAbs` is positive when its input is.
Since the output type of `Int.natAbs` is `ℕ`, the nonnegative case is handled by the default
`positivity` tactic.
 -/
Mathlib.Meta.Positivity.evalNatAbs : Mathlib.Meta.Positivity.PositivityExt
-- Init.Data.Vector.Lemmas
Vector.all_replicate : ∀ {α : Type u_1} {f : α → Bool} {n : ℕ} {a : α}, (Vector.replicate n a).all f = if n = 0 then true else f a
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.id_actionHom : ∀ {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] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) {d d' : D} (f : d ⟶ d'),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom (CategoryTheory.CategoryStruct.id c) f =
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.toMulEquiv_eq_coe : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (f : M ≃ₜ* N), f.toMulEquiv = ↑f