mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.OrderIsoNat
Nat.Subtype.orderIsoOfNat_apply : ∀ {s : Set ℕ} [inst : Infinite ↑s] [dP : DecidablePred fun x => x ∈ s] {n : ℕ},
  (Nat.Subtype.orderIsoOfNat s) n = Nat.Subtype.ofNat s n
-- Init.Data.Float.Model.Unpacked.Pack.Lemmas
_private.Init.Data.Float.Model.Unpacked.Pack.Lemmas.0.Float.Model.UnpackedFloat.pack.match_1.splitter : (motive : Float.Model.UnpackedFloat → Sort u_1) →
  (x : Float.Model.UnpackedFloat) →
    (Unit → motive Float.Model.UnpackedFloat.notANumber) →
      ((s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.infinity s)) →
        ((s : Float.Model.UnpackedFloat.Sign) → motive (Float.Model.UnpackedFloat.zero s)) →
          ((s : Float.Model.UnpackedFloat.Sign) →
              (m : ℕ) →
                (e : ℤ) → (mantissa_pos : 0 < m) → motive (Float.Model.UnpackedFloat.finite s m e mantissa_pos)) →
            motive x
-- Init.Sym.Simp.SimprocDSL
/-- Evaluate ground (fully concrete) terms.  -/
Lean.Parser.Sym.Simp.ground : Lean.ParserDescr
-- Mathlib.Order.Atoms
/-- Every element is a `sSup` of a set of atoms.  -/
IsAtomistic.isLUB_atoms : ∀ {α : Type u_2} {inst : PartialOrder α} {inst_1 : OrderBot α} [self : IsAtomistic α] (b : α),
  ∃ s, IsLUB s b ∧ ∀ a ∈ s, IsAtom a
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary.faceSingletonComplIso_inv_ι_assoc : ∀ {n : ℕ} (i : Fin (n + 2)) {Z : SSet} (h : (SSet.boundary (n + 1)).toSSet ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonComplIso i).inv
      (CategoryTheory.CategoryStruct.comp (SSet.boundary.ι i) h) =
    CategoryTheory.CategoryStruct.comp (SSet.boundary.faceι i) h
-- Mathlib.Computability.StateTransition
StateTransition.EvalsToInTime.mk.sizeOf_spec : ∀ {σ : Type u_1} {f : σ → Option σ} {a : σ} {b : Option σ} {m : ℕ} [inst : SizeOf σ]
  (toEvalsTo : StateTransition.EvalsTo f a b) (steps_le_m : toEvalsTo.steps ≤ m),
  sizeOf { toEvalsTo := toEvalsTo, steps_le_m := steps_le_m } = 1 + sizeOf toEvalsTo + sizeOf steps_le_m
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.symm_mk_pow : ∀ {M : Type u_1} [inst : Monoid M] (a : Mᵈᵐᵃ) (n : ℕ), DomMulAct.mk.symm (a ^ n) = DomMulAct.mk.symm a ^ n
-- Mathlib.Topology.Algebra.MulAction
Filter.Tendsto.one_smul : ∀ {M : Type u_1} {X : Type u_2} {α : Type u_4} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : Monoid M] [inst_3 : MulAction M X] [ContinuousSMul M X] {f : α → M} {g : α → X} {l : Filter α} {a : X},
  Filter.Tendsto f l (nhds 1) → Filter.Tendsto g l (nhds a) → Filter.Tendsto (fun x => f x • g x) l (nhds a)
-- Mathlib.Algebra.Order.Module.Defs
/-- Typeclass for reverse monotonicity of scalar multiplication by positive elements on the left,
namely `a₁ • b ≤ a₂ • b → a₁ ≤ a₂` if `0 < b`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedModule`.  -/
SMulPosReflectLE : (α : Type u_1) → (β : Type u_2) → [SMul α β] → [Preorder α] → [Preorder β] → [Zero β] → Prop
-- Lean.Compiler.IR.Basic
Lean.IR.instReprIRType.repr : Lean.IR.IRType → ℕ → Std.Format
-- Mathlib.Data.Nat.Choose.Sum
/-- **Zhu Shijie's identity** aka hockey-stick identity, version with `Icc`.  -/
Nat.sum_Icc_choose : ∀ (n k : ℕ), ∑ m ∈ Finset.Icc k n, m.choose k = (n + 1).choose (k + 1)
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.inclusionObj.eq_1 : ∀ {C : Type u},
  CategoryTheory.FreeMonoidalCategory.inclusionObj CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.unit =
    CategoryTheory.FreeMonoidalCategory.unit
-- Mathlib.CategoryTheory.Sums.Basic
/-- The sum `F.sum' G` precomposed with the right inclusion functor is isomorphic to `G`  -/
CategoryTheory.Functor.inrCompSum' : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {C : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (F : CategoryTheory.Functor A C) →
              (G : CategoryTheory.Functor B C) → (CategoryTheory.Sum.inr_ A B).comp (F.sum' G) ≅ G
-- Mathlib.Analysis.Calculus.Deriv.Pow
HasStrictDerivAt.pow : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedCommRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {f : 𝕜 → 𝔸} {f' : 𝔸} {x : 𝕜},
  HasStrictDerivAt f f' x → ∀ (n : ℕ), HasStrictDerivAt (f ^ n) (↑n * f x ^ (n - 1) * f') x
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.subLeft_toEquiv : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricVAdd G G]
  [inst_3 : IsIsometricVAdd Gᵃᵒᵖ G] (c : G), (IsometryEquiv.subLeft c).toEquiv = Equiv.subLeft c
-- Init.Data.SInt.Basic
/-- Decides whether two 8-bit signed integers are equal. Usually accessed via the `DecidableEq Int8`
instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `Int8.decEq 123 123 = .isTrue rfl`
 * `(if ((-7) : Int8) = 7 then "yes" else "no") = "no"`
 * `show (7 : Int8) = 7 by decide`
 -/
Int8.decEq : (a b : Int8) → Decidable (a = b)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.union_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : α → Type v} {m₁ m₂ m₃ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₃.WF → m₁.Equiv m₂ → (m₁ ∪ m₃).Equiv (m₂ ∪ m₃)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.endsWith_bool_eq_false_iff_get : ∀ {p : Char → Bool} {s : String},
  s.endsWith p = false ↔ ∀ (h : s.endPos ≠ s.startPos), p ((s.endPos.prev h).get ⋯) = false
-- Mathlib.Data.Fintype.EquivFin
/-- There is (noncomputably) an equivalence between `α` and `Fin (card α)`.

See `Fintype.truncEquivFin` for the computable version,
and `Fintype.truncEquivFinOfCardEq` and `Fintype.equivFinOfCardEq`
for an equiv `α ≃ Fin n` given `Fintype.card α = n`.
 -/
Fintype.equivFin : (α : Type u_4) → [inst : Fintype α] → α ≃ Fin (Fintype.card α)
-- Init.Data.Rat.Lemmas
Rat.add_mul : ∀ (a b c : ℚ), (a + b) * c = a * c + b * c
-- Mathlib.LinearAlgebra.Basis.Defs
/-- `b.reindexFinsetRange` is a basis indexed by `Finset.univ.image b`,
the finite set of basis vectors themselves.  -/
Module.Basis.reindexFinsetRange : {ι : Type u_10} →
  {R : Type u_11} →
    {M : Type u_12} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] →
            (b : Module.Basis ι R M) →
              [inst_3 : Fintype ι] → [inst_4 : DecidableEq M] → Module.Basis (↥(Finset.image (⇑b) Finset.univ)) R M
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.memP_iff_findP? : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} [Std.TransCmp cmp] [RBTree.RBNode.IsCut cmp cut]
  {t : RBTree.RBSet α cmp}, RBTree.RBSet.MemP cut t ↔ ∃ y, t.findP? cut = some y
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.instHasLimitOppositeNatCompIntCochainComplexFunctorEvalUp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] [inst_3 : CategoryTheory.Mono f]
  (n₀ : ℤ) [inst_4 : K.IsStrictlyGE (n₀ + 1)] [inst_5 : L.IsStrictlyGE (n₀ + 1)] (i : ℤ),
  CategoryTheory.Limits.HasLimit
    ((CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cochainComplexFunctor✝ f n₀).comp
      (HomologicalComplex.eval C (ComplexShape.up ℤ) i))
-- Mathlib.Data.Set.Lattice
Set.sUnion_eq_univ_iff : ∀ {α : Type u_1} {c : Set (Set α)}, ⋃₀ c = Set.univ ↔ ∀ (a : α), ∃ b ∈ c, a ∈ b
-- Lean.Elab.DeprecatedArg
Lean.Elab.DeprecatedArgEntry.since? : Lean.Elab.DeprecatedArgEntry → Option String
-- Mathlib.Analysis.MellinTransform
/-- If `f` is `O(x ^ (-a))` as `x → +∞`, then `log • f` is `O(x ^ (-b))` for every `b < a`.  -/
isBigO_rpow_top_log_smul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E},
  b < a → (f =O[Filter.atTop] fun x => x ^ (-a)) → (fun t => Real.log t • f t) =O[Filter.atTop] fun x => x ^ (-b)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- The short root `3α + 2β`.  -/
RootPairing.EmbeddedG2.threeShortAddTwoLongRoot : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → (P : RootPairing ι R M N) → [P.EmbeddedG2] → M
-- Mathlib.Data.Setoid.Partition
IndexedPartition.mk.injEq : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (eq_of_mem : ∀ {x : α} {i j : ι}, x ∈ s i → x ∈ s j → i = j)
  (some : ι → α) (some_mem : ∀ (i : ι), some i ∈ s i) (index : α → ι) (mem_index : ∀ (x : α), x ∈ s (index x))
  (eq_of_mem_1 : ∀ {x : α} {i j : ι}, x ∈ s i → x ∈ s j → i = j) (some_1 : ι → α)
  (some_mem_1 : ∀ (i : ι), some_1 i ∈ s i) (index_1 : α → ι) (mem_index_1 : ∀ (x : α), x ∈ s (index_1 x)),
  ({ eq_of_mem := eq_of_mem, some := some, some_mem := some_mem, index := index, mem_index := mem_index } =
      { eq_of_mem := eq_of_mem_1, some := some_1, some_mem := some_mem_1, index := index_1,
        mem_index := mem_index_1 }) =
    (some = some_1 ∧ index = index_1)
-- Mathlib.Data.Vector.MapLemmas
List.Vector.mapAccumr₂_mapAccumr₂_right_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {σ₁ : Type u_6} {σ₂ : Type u_7} {φ : Type u_8} {n : ℕ} {s₁ : σ₁}
  {s₂ : σ₂} (xs : List.Vector α n) (ys : List.Vector β n) (f₁ : β → γ → σ₁ → σ₁ × φ) (f₂ : α → β → σ₂ → σ₂ × γ),
  List.Vector.mapAccumr₂ f₁ ys (List.Vector.mapAccumr₂ f₂ xs ys s₂).2 s₁ =
    have m :=
      List.Vector.mapAccumr₂
        (fun x y x_1 =>
          match x_1 with
          | (s₁, s₂) =>
            have r₂ := f₂ x y s₂;
            have r₁ := f₁ y r₂.2 s₁;
            ((r₁.1, r₂.1), r₁.2))
        xs ys (s₁, s₂);
    (m.1.1, m.2)
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.integrable_exp_mul_of_le : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ}
  (t b : ℝ),
  0 ≤ t → AEMeasurable X μ → (∀ᵐ (ω : Ω) ∂μ, X ω ≤ b) → MeasureTheory.Integrable (fun ω => Real.exp (t * X ω)) μ
-- Mathlib.Algebra.Order.SuccPred
Order.Iic_two : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddMonoidWithOne α] [SuccAddOrder α] [IsBotZeroClass α] [NeZero 1]
  [NoMaxOrder α], Set.Iic 2 = {0, 1, 2}
-- Mathlib.Data.Fintype.OfMap
/-- Construct a proof of `Fintype α` from a universal list  -/
Fintype.ofList : {α : Type u_1} → [DecidableEq α] → (l : List α) → (∀ (x : α), x ∈ l) → Fintype α
-- Mathlib.NumberTheory.SumTwoSquares
ZMod.chineseRemainder.congr_simp : ∀ {m n : ℕ} (h : m.Coprime n), ZMod.chineseRemainder h = ZMod.chineseRemainder h
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.union_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ t₃ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → (t₁ ∪ t₃).Equiv (t₂ ∪ t₃)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.leadingTerm_leadingTerm : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R),
  m.leadingTerm (m.leadingTerm f) = m.leadingTerm f
-- Std.Time.Time.Unit.Basic
/-- Converts a `Millisecond.Offset` to a `Minute.Offset`.
 -/
Std.Time.Minute.Offset.ofMilliseconds : Std.Time.Millisecond.Offset → Std.Time.Minute.Offset
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarAlgebra.inf_toNonUnitalSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : NonUnitalSemiring A]
  [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : IsScalarTower R A A] [inst_6 : SMulCommClass R A A]
  [inst_7 : StarModule R A] (S T : NonUnitalStarSubalgebra R A),
  (S ⊓ T).toNonUnitalSubalgebra = S.toNonUnitalSubalgebra ⊓ T.toNonUnitalSubalgebra
-- Mathlib.Algebra.Module.ZLattice.Basic
ZLattice.comap_comp : ∀ (K : Type u_1) [inst : NormedField K] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace K F] (L : Submodule ℤ E)
  {G : Type u_4} [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace K G] (e : F →ₗ[K] E) (e' : G →ₗ[K] F),
  ZLattice.comap K (ZLattice.comap K L e) e' = ZLattice.comap K L (e ∘ₗ e')
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.toNonUnitalSubalgebra_le_toNonUnitalSubalgebra : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {S T : Subalgebra R A}, S.toNonUnitalSubalgebra ≤ T.toNonUnitalSubalgebra ↔ S ≤ T
-- Mathlib.LinearAlgebra.Center
LinearMap.mem_center_of_apply_eq_smul : ∀ {R : Type u_1} {V : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid V] [inst_2 : Module R V] {f : V →ₗ[R] V}
  {a : R}, (∀ (x : V), f x = a • x) → f ∈ Set.center (Module.End R V)
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` preserves colimits of shape `Jᵒᵖ`, then `F : C ⥤ Dᵒᵖ` preserves limits
of shape `J`.  -/
CategoryTheory.Limits.preservesLimitsOfShape_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (J : Type w) [inst_2 : CategoryTheory.Category.{w', w} J] (F : CategoryTheory.Functor C Dᵒᵖ)
  [CategoryTheory.Limits.PreservesColimitsOfShape Jᵒᵖ F.leftOp], CategoryTheory.Limits.PreservesLimitsOfShape J F
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_inj : ∀ {R : Type u_1} {a b : R} [inst : Zero R] {x y : R}, QuadraticAlgebra.C x = QuadraticAlgebra.C y ↔ x = y
-- Lean.Parser.Term
Lean.Parser.Term.waitForExpectedType.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.OuterMeasure.OfAddContent
MeasureTheory.AddContent.measureCaratheodory_eq : ∀ {α : Type u_1} {C : Set (Set α)} {s : Set α} (m : MeasureTheory.AddContent ENNReal C)
  (hC : MeasureTheory.IsSetSemiring C) (m_sigma_subadd : m.IsSigmaSubadditive),
  s ∈ C → (m.measureCaratheodory hC m_sigma_subadd) s = m s
-- Init.Data.String.Iterator
_private.Init.Data.String.Iterator.0.String.Legacy.Iterator.find.eq_def : ∀ (it : String.Legacy.Iterator) (p : Char → Bool),
  it.find p = if it.atEnd = true then it else if p it.curr = true then it else it.next.find p
-- Mathlib.NumberTheory.Niven
irrational_cos_rat_mul_pi : ∀ {r : ℚ}, 3 < r.den → Irrational (Real.cos (↑r * Real.pi))
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
/-- A continuous function on a compact space is automatically a continuous function vanishing at
infinity. This is not an instance to avoid type class loops.  -/
ZeroAtInftyContinuousMap.zeroAtInftyContinuousMapClass.ofCompact : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β] {G : Type u_2}
  [inst_3 : FunLike G α β] [ContinuousMapClass G α β] [CompactSpace α], ZeroAtInftyContinuousMapClass G α β
-- Mathlib.Algebra.Lie.Ideal
LieSubalgebra.ofLe.congr_simp : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  {K K_1 : LieSubalgebra R L} (e_K : K = K_1) {K' : LieSubalgebra R L} (h : K ≤ K'),
  LieSubalgebra.ofLe h = LieSubalgebra.ofLe ⋯
-- Lean.Elab.Tactic.Conv.Basic
Lean.Elab.Tactic.Conv.getLhsRhs : Lean.Elab.Tactic.TacticM (Lean.Expr × Lean.Expr)
-- Mathlib.Data.Quot
/-- Map a function `f : α → β` that sends equivalent elements to equivalent elements
to a function `Quotient sa → Quotient sb`. Useful to define unary operations on quotients.  -/
Quotient.map : {α : Sort u_1} →
  {β : Sort u_2} →
    {sa : Setoid α} → {sb : Setoid β} → (f : α → β) → (∀ ⦃a b : α⦄, a ≈ b → f a ≈ f b) → Quotient sa → Quotient sb
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.DayFunctor
CategoryTheory.MonoidalCategory.DayFunctor.isoPointwiseLeftKanExtension.eq_1 : ∀ {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 G : CategoryTheory.MonoidalCategory.DayFunctor C V),
  F.isoPointwiseLeftKanExtension G =
    (CategoryTheory.MonoidalCategoryStruct.tensorObj F G).functor.leftKanExtensionUnique (F.η G)
      ((CategoryTheory.MonoidalCategory.tensor C).pointwiseLeftKanExtension
        (CategoryTheory.MonoidalCategory.externalProduct F.functor G.functor))
      ((CategoryTheory.MonoidalCategory.tensor C).pointwiseLeftKanExtensionUnit
        (CategoryTheory.MonoidalCategory.externalProduct F.functor G.functor))
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation.coind_comp_friend_left : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {op :
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  (motive :
    (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl) →
      Prop),
  motive op →
    (∀
        (op :
          Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
            Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
        motive op →
          ∃ T,
            ∀ (s : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl),
              (op s).destruct =
                Option.map
                  (fun x =>
                    match x with
                    | (exp, coef, opf, op') => (exp, coef, ↑opf (↑op' s.tail)))
                  (T s.head)) →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperation op
-- Mathlib.Data.Finsupp.WellFounded
Finsupp.wellFoundedLT : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : Preorder N] [WellFoundedLT N],
  (∀ (n : N), ¬n < 0) → WellFoundedLT (α →₀ N)
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.subtypeVal : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsUpperSet s → ∀ {a : ↑s}, Order.IsPredLimit a → Order.IsPredLimit ↑a
-- Mathlib.RingTheory.Ideal.Finsupp
Finsupp.submodule_smul : ∀ (R : Type u_1) [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (ι : Type u_3)
  (p : ι → Submodule R M) (I : Ideal R), (Finsupp.submodule fun i => I • p i) = I • Finsupp.submodule p
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
/-- The codomain of an isomorphism.  -/
Mathlib.Tactic.Monoidal.tgtExprOfIso : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.dvd_of_mem_normalizedFactors : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {a p : α}, p ∈ UniqueFactorizationMonoid.normalizedFactors a → p ∣ a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_nat_mul_pi_sub : ∀ (x : ℝ) (n : ℕ), Real.sin (↑n * Real.pi - x) = -((-1) ^ n * Real.sin x)
-- Mathlib.Probability.Distributions.Gaussian.Fernique
ProbabilityTheory.IsGaussian.memLp_two_id : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E],
  MeasureTheory.MemLp id 2 μ
-- Mathlib.Analysis.Analytic.CPolynomial
ContinuousMultilinearMap.analyticAt_uncurry_compContinuousLinearMap : ∀ {𝕜 : Type u_1} {G : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] {ι : Type u_5} {Em : ι → Type u_6} {Fm : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (Em i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (Em i)]
  [inst_5 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_6 : (i : ι) → NormedSpace 𝕜 (Fm i)] [inst_7 : Fintype ι]
  {q : ((i : ι) → Fm i →L[𝕜] Em i) × ContinuousMultilinearMap 𝕜 Em G},
  AnalyticAt 𝕜 (fun p => p.2.compContinuousLinearMap p.1) q
-- Lean.Meta.Hint
/-- Given a `Char` diff, produces an equivalent `String` diff, joining actions of the same kind.  -/
_private.Lean.Meta.Hint.0.Lean.Meta.Hint.readableDiff.joinCharDiff : Array (Lean.Diff.Action × Char) → Array (Lean.Diff.Action × String)
-- Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite
_private.Mathlib.Analysis.Normed.Operator.Perturbation.StrictByFinite.0.step3 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} {F : Type u_3}
  [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E] [inst_9 : TopologicalSpace F]
  [IsTopologicalAddGroup F] [ContinuousSMul 𝕜 F] (u : E →L[𝕜] F) (A : Submodule 𝕜 E),
  IsClosed ↑A →
    ∀ [A.CoFG],
      Disjoint (↑u).ker A →
        IsClosed ↑(↑u).range →
          (Topology.IsStrictMap ⇑u ↔ Topology.IsStrictMap ⇑(u.domRestrict A) ∧ IsClosed ↑(↑(u.domRestrict A)).range)
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.multiset_prod : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : CommMonoid β] (m : Multiset (α → β)),
  (∀ f ∈ m, HasCompactMulSupport f) → HasCompactMulSupport m.prod
-- Mathlib.RingTheory.QuasiFinite.Basic
Ideal.exists_not_mem_forall_mem_of_ne_of_liesOver : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [p.IsPrime] (q : Ideal S) [inst_4 : q.IsPrime] [q.LiesOver p] [Algebra.EssFiniteType R S] [Algebra.QuasiFiniteAt R q],
  ∃ s ∉ q, ∀ (q' : Ideal S), q'.IsPrime → q' ≠ q → q'.LiesOver p → s ∈ q'
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.εIso_hom : ∀ {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.Monoidal],
  (CategoryTheory.Functor.Monoidal.εIso F).hom = CategoryTheory.Functor.LaxMonoidal.ε F
-- Batteries.Data.Float.Lemmas
Float32.beq_iff_ne_nan_and_eq : ∀ {f f' : Float32}, (f == f') = true ↔ f ≠ Float32.nan ∧ f' ≠ Float32.nan ∧ (f = f' ∨ f = 0 ∧ f' = -0 ∨ f = -0 ∧ f' = 0)