mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.SpecialFunctions.Pow.Complex
Complex.cpow_conj : ∀ (x n : ℂ), x.arg ≠ Real.pi → x ^ (starRingEnd ℂ) n = (starRingEnd ℂ) ((starRingEnd ℂ) x ^ n)
-- Init.Data.UInt.Lemmas
UInt32.ne_of_lt : ∀ {a b : UInt32}, a < b → a ≠ b
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instOrderTop : {G : Type u_1} → [inst : Group G] → [inst_1 : TopologicalSpace G] → OrderTop (OpenSubgroup G)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sup'_inv : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Inv α] [inst_2 : SemilatticeSup β] {s : Finset α}
  (hs : s⁻¹.Nonempty) (f : α → β), s⁻¹.sup' hs f = s.sup' ⋯ fun x => f x⁻¹
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.skip?_eq_matchAt? : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, pos.skip? pat = String.Slice.Pattern.Model.matchAt? pat pos
-- Mathlib.NumberTheory.NumberField.Basic
/-- Given `f : M → K` such that `∀ x, IsIntegral ℤ (f x)`, the corresponding function
`M → 𝓞 K`.  -/
NumberField.RingOfIntegers.restrict : {K : Type u_1} →
  [inst : Field K] → {M : Type u_3} → (f : M → K) → (∀ (x : M), IsIntegral ℤ (f x)) → M → NumberField.RingOfIntegers K
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxo.Iterator.instIteratorLoop.loop.wf : {α : Type u} →
  [inst : Std.PRange.UpwardEnumerable α] →
    [inst_1 : LT α] →
      [inst_2 : DecidableLT α] →
        [Std.PRange.LawfulUpwardEnumerable α] →
          [Std.PRange.LawfulUpwardEnumerableLT α] →
            {n : Type u → Type w} →
              [Monad n] →
                (γ : Type u) →
                  (Pl : α → γ → ForInStep γ → Prop) →
                    Std.IteratorLoop.WellFounded (Std.Rxo.Iterator α) Id Pl →
                      (LargeEnough : α → Prop) →
                        (∀ (a b : α), Std.PRange.UpwardEnumerable.LE a b → LargeEnough a → LargeEnough b) →
                          (upperBound : α) →
                            γ →
                              (next : α) →
                                LargeEnough next →
                                  ((out : α) → LargeEnough out → out < upperBound → (c : γ) → n { s // Pl out c s }) →
                                    n γ
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
/-- A zero cochain consists of a family of sections.  -/
CategoryTheory.PresheafOfGroups.ZeroCochain : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.Functor Cᵒᵖ GrpCat → {I : Type w'} → (I → C) → Type (max w w')
-- Batteries.Recycling.RBTree.Lemmas
/-- `IsStrictCut` upgrades the `IsCut` property to ensure that at most one element of the tree
can match the cut, and hence `find?` will return the unique such element if one exists.
 -/
RBTree.RBNode.IsStrictCut : {α : Type u_1} → (α → α → Ordering) → (α → Ordering) → Prop
-- Init.Data.Array.Monadic
_private.Init.Data.Array.Monadic.0.Array.flatMapM.eq_1 : ∀ {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (f : α → m (Array β)) (as : Array α),
  Array.flatMapM f as =
    Array.foldlM
      (fun bs a => do
        let __do_lift ← f a
        pure (bs ++ __do_lift))
      #[] as
-- Mathlib.Analysis.Normed.Group.Uniform
AddMonoidHomClass.isometry_iff_norm : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
  [inst_2 : FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕), Isometry ⇑f ↔ ∀ (x : E), ‖f x‖ = ‖x‖
-- Mathlib.Order.Filter.Cofinite
/-- If `α` is a preorder with no top element, then `atTop ≤ cofinite`.  -/
Filter.atTop_le_cofinite : ∀ {α : Type u_2} [inst : Preorder α] [NoTopOrder α], Filter.atTop ≤ Filter.cofinite
-- Init.Data.SInt.Basic
/-- The largest number that `Int32` can represent: `2^31 - 1 = 2147483647`.  -/
Int32.maxValue : Int32
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instPartialOrder : {α : Type u_1} → [inst : TopologicalSpace α] → PartialOrder (TopologicalSpace.CompactOpens α)
-- Mathlib.Order.Partition.Finpartition
Finpartition.sum_eq_sum_finpartition_subtype : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] {s : α} (P : Finpartition s) {Pr : α → Prop}
  (Prsup : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊔ t)) (Prinf : ∀ ⦃s t : α⦄, Pr s → Pr t → Pr (s ⊓ t)) (Prbot : Pr ⊥)
  (hs : Pr s) (hP : ∀ p ∈ P.parts, Pr p) {X : Type u_2} [inst_2 : AddCommMonoid X] (f : α → X),
  ∑ p ∈ P.parts, f p = ∑ p ∈ (P.toSubtype Prsup Prinf Prbot hs hP).parts, f ↑p
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.isEmpty.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Batteries.AssocList α β → Sort u_3) (x : Batteries.AssocList α β)
  (h_1 : Unit → motive Batteries.AssocList.nil) (h_2 : (x : Batteries.AssocList α β) → motive x),
  (x = Batteries.AssocList.nil → False) →
    (match x with
      | Batteries.AssocList.nil => h_1 ()
      | x => h_2 x) =
      h_2 x
-- Mathlib.Combinatorics.Matroid.Map
Matroid.instFiniteElemERestrictSubtype : ∀ {α : Type u_1} {M : Matroid α} [M.Finite], (M.restrictSubtype M.E).Finite
-- Mathlib.Order.SupClosed
supClosure_empty : ∀ {α : Type u_3} [inst : SemilatticeSup α], supClosure ∅ = ∅
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.iSup_skeletonOfMono : ∀ {X Y : SSet} (i : X ⟶ Y), ⨆ n, (SSet.skeletonOfMono i) n = ⊤
-- Init.Data.Option.Lemmas
Option.map_or : ∀ {α : Type u_1} {o o' : Option α} {α_1 : Type u_2} {f : α → α_1},
  Option.map f (o.or o') = (Option.map f o).or (Option.map f o')
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.cosZeta.eq_1 : ∀ (a : UnitAddCircle),
  HurwitzZeta.cosZeta a = Function.update (fun s => HurwitzZeta.completedCosZeta a s / s.Gammaℝ) 0 (-1 / 2)
-- Std.Data.TreeMap.Lemmas
/-- Simpler variant of `getElem!_filter` when `LawfulEqCmp` is available.  -/
Std.TreeMap.getElem!_filter' : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  [inst : Inhabited β] {f : α → β → Bool} {k : α}, (Std.TreeMap.filter f t)[k]! = (Option.filter (f k) t[k]?).get!
-- Mathlib.Tactic.Simproc.ExistsAndEq
ExistsAndEq.instBEqGoTo.beq : ExistsAndEq.GoTo → ExistsAndEq.GoTo → Bool
-- Init.Data.List.Find
List.of_findIdx?_eq_none : ∀ {α : Type u_1} {xs : List α} {p : α → Bool},
  List.findIdx? p xs = none →
    ∀ (i : ℕ),
      match xs[i]? with
      | some a => ¬p a = true
      | none => true = true
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressKind.noConfusionType : Sort v✝ → Lean.Lsp.LeanFileProgressKind → Lean.Lsp.LeanFileProgressKind → Sort v✝
-- Mathlib.Algebra.Star.SelfAdjoint
isStarNormal_iff : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : Star R] (x : R), IsStarNormal x ↔ Commute (star x) x
-- Mathlib.Analysis.Analytic.Within
/-- `f` is analytic within `s` at `x` iff some local extension of `f` is analytic at `x`. In this
version, we make sure that the extension coincides with `f` on all of `insert x s`.  -/
analyticWithinAt_iff_exists_analyticAt' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F}
  {s : Set E} {x : E}, AnalyticWithinAt 𝕜 f s x ↔ ∃ g, f x = g x ∧ Set.EqOn f g (insert x s) ∧ AnalyticAt 𝕜 g x
-- Init.Data.List.Lemmas
/-- Variant of `any_beq` with `==` reversed.  -/
List.any_beq' : ∀ {α : Type u_1} {a : α} [inst : BEq α] [PartialEquivBEq α] {l : List α}, (l.any fun x => x == a) = l.contains a
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.opNNNorm_le_iff : ∀ {𝕜 : 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} {C : NNReal}, ‖f‖₊ ≤ C ↔ ∀ (m : (i : ι) → E i), ‖f m‖₊ ≤ C * ∏ i, ‖m i‖₊
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.instCommSemiring : {α : Type u_1} →
  [DecidableEq α] →
    [inst : CommSemiring α] →
      [inst_1 : PartialOrder α] →
        [CanonicallyOrderedAdd α] → [NoZeroDivisors α] → [Nontrivial α] → CommSemiring (WithTop α)
-- Mathlib.RingTheory.Etale.Basic
/-- Localization at an element is étale.  -/
Algebra.Etale.of_isLocalizationAway : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (r : R)
  [IsLocalization.Away r A], Algebra.Etale R A
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatIso.id_inv : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} (F : CategoryTheory.BasedFunctor 𝒳 𝒴),
  (CategoryTheory.BasedNatIso.id F).inv = CategoryTheory.CategoryStruct.id F
-- Mathlib.Algebra.Opposites
AddOpposite.instInvolutiveInv : {α : Type u_1} → [InvolutiveInv α] → InvolutiveInv αᵃᵒᵖ
-- Std.Http.Protocol.H1.Writer
Std.Http.Protocol.H1.Writer.mk.sizeOf_spec : ∀ {dir : Std.Http.Protocol.H1.Direction} (userData : Array Std.Http.Chunk)
  (outputData : Std.Http.Internal.ChunkedBuffer) (state : Std.Http.Protocol.H1.Writer.State)
  (knownSize : Option Std.Http.Body.Length) (messageHead : Std.Http.Protocol.H1.Message.Head dir.swap)
  (sentMessage userClosedBody omitBody : Bool) (userDataBytes : ℕ),
  sizeOf
      { userData := userData, outputData := outputData, state := state, knownSize := knownSize,
        messageHead := messageHead, sentMessage := sentMessage, userClosedBody := userClosedBody, omitBody := omitBody,
        userDataBytes := userDataBytes } =
    1 + sizeOf userData + sizeOf outputData + sizeOf state + sizeOf knownSize + sizeOf messageHead +
            sizeOf sentMessage +
          sizeOf userClosedBody +
        sizeOf omitBody +
      sizeOf userDataBytes
-- Mathlib.Topology.Connected.Basic
connectedComponentIn_subset : ∀ {α : Type u} [inst : TopologicalSpace α] (F : Set α) (x : α), connectedComponentIn F x ⊆ F
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.skipSuffixWhile_char_eq_skipSuffixWhile_beq : ∀ {c : Char} {s : String.Slice}, s.skipSuffixWhile c = s.skipSuffixWhile fun x => x == c
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
isLUB_csSup : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {s : Set α},
  s.Nonempty → autoParam (BddAbove s) isLUB_csSup._auto_1 → IsLUB s (sSup s)
-- Lean.Language.Basic
/-- Cancellation token that can be set by the server to cancel the task when it detects the results
are not needed anymore.
 -/
Lean.Language.SnapshotTask.cancelTk? : {α : Type} → Lean.Language.SnapshotTask α → Option IO.CancelToken
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_modify : ∀ {α : Type u} {instOrd : Ord α} [inst : Std.TransOrd α] {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  (h : t.WF) {k k' : α} {f : β → β} {hc : k' ∈ Std.DTreeMap.Internal.Impl.Const.modify k f t},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.Const.modify k f t) k' hc =
    if heq : compare k k' = Ordering.eq then f (Std.DTreeMap.Internal.Impl.Const.get t k ⋯)
    else Std.DTreeMap.Internal.Impl.Const.get t k' ⋯
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.constInsertManyIfNewUnit : ∀ {α : Type u} [inst : Ord α] {ρ : Type u_1} [inst_1 : ForIn Id ρ α] {t : Std.DTreeMap.Internal.Impl α fun x => Unit}
  {l : ρ} {h : t.Balanced}, t.WF → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l h)).WF
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.instMulEquivClass : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N], MulEquivClass (M ≃ₜ* N) M N
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.id_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CoalgebraStruct R A] (x : A), (BialgHom.id R A) x = x
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.IsSFiniteKernel.snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) [ProbabilityTheory.IsSFiniteKernel κ],
  ProbabilityTheory.IsSFiniteKernel κ.snd
-- Mathlib.FieldTheory.Galois.Basic
IntermediateField.restrictNormalHom_ker : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (E : IntermediateField K L)
  [inst_3 : Normal K ↥E], (AlgEquiv.restrictNormalHom ↥E).ker = E.fixingSubgroup
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_symm_comp_lid_symm_assoc : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid P]
  [inst_6 : Module R P] (f : P →ₗ[R] TensorProduct R M N),
  ↑(TensorProduct.assoc R R M N).symm ∘ₗ ↑(TensorProduct.lid R (TensorProduct R M N)).symm ∘ₗ f =
    TensorProduct.map (↑(TensorProduct.lid R M).symm) LinearMap.id ∘ₗ f
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The cokernel of an arrow is natural.  -/
CategoryTheory.Limits.coker : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [CategoryTheory.Limits.HasCokernels C] → CategoryTheory.Functor (CategoryTheory.Arrow C) C
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivAt.comp_hasFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} (x : E),
  HasDerivAt h₂ h₂' (f x) → HasFDerivAt f f' x → HasFDerivAt (h₂ ∘ f) (h₂' • f') x
-- Mathlib.Topology.MetricSpace.Gluing
/-- The canonical map from `Y` to the space obtained by gluing isometric subsets in `X` and `Y`.  -/
Metric.toGlueR : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [inst : Nonempty Z] →
        [inst_1 : MetricSpace Z] →
          [inst_2 : MetricSpace X] →
            [inst_3 : MetricSpace Y] →
              {Φ : Z → X} → {Ψ : Z → Y} → (hΦ : Isometry Φ) → (hΨ : Isometry Ψ) → Y → Metric.GlueSpace hΦ hΨ
-- Mathlib.MeasureTheory.OuterMeasure.Operations
/-- **Alias** of `add_apply`. -/
MeasureTheory.OuterMeasure.add_apply : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : FunLike F α β} {inst_1 : Add β}
  {inst_2 : Add F} [self : IsAddApply F α β] (f g : F) (x : α), (f + g) x = f x + g x
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.Nondegenerate.toLinearMap₂ : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {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}
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂), M.Nondegenerate → ((Matrix.toLinearMap₂ b₁ b₂) M).Nondegenerate
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- We can define `esymm σ R n` by summing over a subtype instead of over `powerset_len`.  -/
MvPolynomial.esymm_eq_sum_subtype : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] (n : ℕ),
  MvPolynomial.esymm σ R n = ∑ t, ∏ i ∈ ↑t, MvPolynomial.X i
-- Lean.Linter.Init
Lean.Linter.getLinterOptions : {m : Type → Type} → [Monad m] → [Lean.MonadOptions m] → [Lean.MonadEnv m] → m Lean.Linter.LinterOptions
-- Aesop.Stats.Basic
Aesop.GoalStats.mk.sizeOf_spec : ∀ (goalId : ℕ) (goalKind : Aesop.GoalKind) (lctxSize depth : ℕ) (forwardStateStats : Aesop.ForwardStateStats),
  sizeOf
      { goalId := goalId, goalKind := goalKind, lctxSize := lctxSize, depth := depth,
        forwardStateStats := forwardStateStats } =
    1 + sizeOf goalId + sizeOf goalKind + sizeOf lctxSize + sizeOf depth + sizeOf forwardStateStats
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instBEqOfTransCmp : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [BEq β] → BEq (Std.ExtTreeMap α β cmp)
-- Mathlib.MeasureTheory.Measure.Map
/-- Even if `s` is not measurable, we can bound `map f μ s` from below.
See also `MeasurableEquiv.map_apply`.  -/
MeasureTheory.Measure.le_map_apply : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β}, AEMeasurable f μ → ∀ (s : Set β), μ (f ⁻¹' s) ≤ (MeasureTheory.Measure.map f μ) s
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- The canonical map `𝟙_ V ⟶ F.obj (𝟙_ C)` exhibits `F` as a pointwise left Kan extension
of `fromPUnit.{0} 𝟙_ V` along `fromPUnit.{0} 𝟙_ C`.  -/
CategoryTheory.MonoidalCategory.DayConvolutionUnit.isPointwiseLeftKanExtensionCan : {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} →
            {F : CategoryTheory.Functor C V} →
              [self : CategoryTheory.MonoidalCategory.DayConvolutionUnit F] →
                (CategoryTheory.Functor.LeftExtension.mk F
                    { app := fun x => CategoryTheory.MonoidalCategory.DayConvolutionUnit.can,
                      naturality := ⋯ }).IsPointwiseLeftKanExtension
-- Mathlib.Data.Set.Prod
Function.Injective.preimage_pullbackDiagonal : ∀ {X : Type u_2} {Y : Sort u_3} {Z : Type u_1} {f : X → Y} {g : Z → X},
  Function.Injective g →
    Function.mapPullback g id g ⋯ ⋯ ⁻¹' Function.pullbackDiagonal f = Function.pullbackDiagonal (f ∘ g)
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.mem_atTop : ∀ {α : Type u_3} [inst : Preorder α] (a : α), {b | a ≤ b} ∈ Filter.atTop
-- Init.Data.Array.Lemmas
Array.exists_mem_of_ne_empty : ∀ {α : Type u_1} (xs : Array α), xs ≠ #[] → ∃ x, x ∈ xs
-- Mathlib.Algebra.Quotient
/-- `HasQuotient A B` is a notation typeclass that allows us to write `A ⧸ b` for `b : B`.
This allows the usual notation for quotients of algebraic structures,
such as groups, modules and rings.

`A` is a parameter, despite being unused in the definition below, so it appears in the notation.
 -/
HasQuotient : outParam (Type u) → Type v → Type (max (u + 1) (v + 1))
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_zero : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.reverse 0 = 0
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_iInf_comap_of_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {ι : Type u_5} {f : F},
  Function.Surjective ⇑f → ∀ (S : ι → Submonoid N), Submonoid.map f (⨅ i, Submonoid.comap f (S i)) = iInf S
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.lie_comm : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (I J : LieIdeal R L),
  ⁅I, J⁆ = ⁅J, I⁆
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.eq_d₀₁_comp_inv : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.cochainsIso₀ A).inv
      ((groupCohomology.inhomogeneousCochains A).d 0 1) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.d₀₁ A) (groupCohomology.cochainsIso₁ A).inv
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- A monoid object internal to a monoidal category.

When the monoidal category is preadditive, this is also sometimes called an "algebra object".
 -/
CategoryTheory.MonObj : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → [CategoryTheory.MonoidalCategory C] → C → Type v₁
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.strictAntiOn_log : StrictAntiOn Real.log (Set.Iio 0)
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
TensorProduct.instDirectedSystemCoeLinearMapIdRTensor : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} [inst_1 : Preorder ι] {G : ι → Type u_3}
  [inst_2 : (i : ι) → AddCommMonoid (G i)] [inst_3 : (i : ι) → Module R (G i)] (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j)
  (M : Type u_4) [inst_4 : AddCommMonoid M] [inst_5 : Module R M] [DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)],
  DirectedSystem (fun x => TensorProduct R (G x) M) fun i j h => ⇑(LinearMap.rTensor M (f i j h))
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.Slice.startsWith_prop_iff_get : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String.Slice},
  s.startsWith P = true ↔ ∃ (h : s.startPos ≠ s.endPos), P (s.startPos.get h)
-- Mathlib.Algebra.Category.MonCat.Yoneda
CommMonCat.coyonedaType_obj_map : ∀ (X : Type uᵒᵖ) {X_1 Y : CommMonCat} (f : X_1 ⟶ Y),
  (CommMonCat.coyonedaType.obj X).map f =
    CommMonCat.ofHom (MonoidHom.pi fun i => (CommMonCat.Hom.hom f).comp (Pi.evalMonoidHom (fun a => ↑X_1) i))
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.leftUnitorNatIsoCat_inv_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] (a b : B) (X : a ⟶ b),
  (CategoryTheory.Bicategory.leftUnitorNatIsoCat a b).inv.toNatTrans.app X =
    (CategoryTheory.Bicategory.leftUnitor X).inv
-- Mathlib.Tactic.Variable
Mathlib.Command.Variable.variable?.checkRedundant : Lean.Option Bool
-- Lean.Meta.Sym.Arith.Poly
Lean.Grind.CommRing.Poly.mulConst' : Lean.Grind.CommRing.Poly → ℤ → optParam (Option ℕ) none → Lean.Grind.CommRing.Poly
-- Mathlib.Data.Fin.Tuple.Finset
Finset.map_consEquiv_filter_piFinset : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_1} (S : (i : Fin (n + 1)) → Finset (α i)) (P : ((i : Fin n) → α i.succ) → Prop)
  [inst : DecidablePred P],
  Finset.map (Fin.consEquiv α).symm.toEmbedding ({r ∈ Fintype.piFinset S | P (Fin.tail r)}) =
    S 0 ×ˢ {r ∈ Fintype.piFinset (Fin.tail S) | P r}
-- Mathlib.RingTheory.RingHom.StandardSmooth
/-- Helper lemma for the `algebraize` tactic  -/
RingHom.IsStandardSmooth.toAlgebra : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S},
  f.IsStandardSmooth → Algebra.IsStandardSmooth R S
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
_private.Mathlib.NumberTheory.EllipticDivisibilitySequence.0.complEDS'.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((n : ℕ) → motive n.succ.succ) → motive x
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepFun_iff : ∀ {Ω : Type u_1} {ι : Type u_2} (m' : MeasurableSpace Ω) {mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω]
  (hm' : m' ≤ mΩ) {β : ι → Type u_3} (m : (x : ι) → MeasurableSpace (β x)) (f : (x : ι) → Ω → β x),
  (∀ (i : ι), Measurable (f i)) →
    ∀ (μ : MeasureTheory.Measure Ω) [inst_1 : MeasureTheory.IsFiniteMeasure μ],
      ProbabilityTheory.iCondIndepFun m' hm' f μ ↔
        ∀ (s : Finset ι) {g : ι → Set Ω},
          (∀ i ∈ s, MeasurableSet (g i)) →
            μ[(⋂ i ∈ s, g i).indicator fun ω => 1 | m'] =ᵐ[μ] ∏ i ∈ s, μ[(g i).indicator fun ω => 1 | m']
-- Mathlib.CategoryTheory.Iso
/-- A functor `F : C ⥤ D` sends isomorphisms `i : X ≅ Y` to isomorphisms `F.obj X ≅ F.obj Y`  -/
CategoryTheory.Functor.mapIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) → {X Y : C} → (X ≅ Y) → (F.obj X ≅ F.obj Y)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lift_succ : ∀ (a : Ordinal.{v}), Ordinal.lift.{u, v} (Order.succ a) = Order.succ (Ordinal.lift.{u, v} a)
-- Lean.Elab.MutualDef
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.ExprWithHoles.expr : Lean.Elab.Term.ExprWithHoles✝ → Lean.Expr
-- Lean.Message
/-- Wrap the given message in square brackets `[]`.  -/
Lean.MessageData.sbracket : Lean.MessageData → Lean.MessageData