mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
/-- The natural isomorphism between the diagram obtained by forgetting the reflexion of
`ofIsReflexivePair f g` and the original parallel pair.  -/
CategoryTheory.Limits.inclusionWalkingReflexivePairOfIsReflexivePairIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A B : C} →
      (f g : A ⟶ B) →
        [inst_1 : CategoryTheory.IsReflexivePair f g] →
          CategoryTheory.Limits.WalkingParallelPair.inclusionWalkingReflexivePair.comp
              (CategoryTheory.Limits.ofIsReflexivePair f g) ≅
            CategoryTheory.Limits.parallelPair f g
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_insertEntry_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {k : α} {v : β},
  Std.Internal.List.getValue? k (Std.Internal.List.insertEntry k v l) = some v
-- Lean.Environment
Lean.PersistentEnvExtension.mk.inj : ∀ {α β σ : Type} {toEnvExtension : Lean.EnvExtension (Lean.PersistentEnvExtensionState α σ)} {name : Lean.Name}
  {addImportedFn : Array (Array α) → Lean.ImportM σ} {addEntryFn : σ → β → σ}
  {exportEntriesFn : Lean.Environment → σ → Lean.OLeanEntries (Array α)} {statsFn : σ → Std.Format}
  {toEnvExtension_1 : Lean.EnvExtension (Lean.PersistentEnvExtensionState α σ)} {name_1 : Lean.Name}
  {addImportedFn_1 : Array (Array α) → Lean.ImportM σ} {addEntryFn_1 : σ → β → σ}
  {exportEntriesFn_1 : Lean.Environment → σ → Lean.OLeanEntries (Array α)} {statsFn_1 : σ → Std.Format},
  { toEnvExtension := toEnvExtension, name := name, addImportedFn := addImportedFn, addEntryFn := addEntryFn,
        exportEntriesFn := exportEntriesFn, statsFn := statsFn } =
      { toEnvExtension := toEnvExtension_1, name := name_1, addImportedFn := addImportedFn_1,
        addEntryFn := addEntryFn_1, exportEntriesFn := exportEntriesFn_1, statsFn := statsFn_1 } →
    toEnvExtension = toEnvExtension_1 ∧
      name = name_1 ∧
        addImportedFn = addImportedFn_1 ∧
          addEntryFn = addEntryFn_1 ∧ exportEntriesFn = exportEntriesFn_1 ∧ statsFn = statsFn_1
-- Mathlib.Algebra.Group.Submonoid.Support
AddSubmonoid.mem_support : ∀ {G : Type u_1} [inst : AddGroup G] {M : AddSubmonoid G} {x : G}, x ∈ M.support ↔ x ∈ M ∧ -x ∈ M
-- Init.Sym.DSimp.DSimprocDSL
Lean.Parser.Category.sym_dsimp_field : Lean.Parser.Category
-- Mathlib.Computability.Primrec.Basic
Primrec.of_equiv_iff : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {β : Type u_4} (e : β ≃ α) {f : σ → β},
  (Primrec fun a => e (f a)) ↔ Primrec f
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.fderivCompContinuousLinearMap.eq_1 : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι] [inst_8 : DecidableEq ι]
  (f : ContinuousMultilinearMap 𝕜 E₁ G) (g : (i : ι) → E i →L[𝕜] E₁ i),
  f.fderivCompContinuousLinearMap g =
    (((ContinuousLinearMap.apply 𝕜 (ContinuousMultilinearMap 𝕜 E G)) f).compContinuousMultilinearMap
          (ContinuousMultilinearMap.compContinuousLinearMapContinuousMultilinear 𝕜 E E₁ G)).linearDeriv
      g
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueueEntry.unsafeRule.inj : ∀ {r r_1 : Aesop.IndexMatchResult Aesop.UnsafeRule},
  Aesop.UnsafeQueueEntry.unsafeRule r = Aesop.UnsafeQueueEntry.unsafeRule r_1 → r = r_1
-- Mathlib.CategoryTheory.Galois.Basic
/-- Fiber functors reflect monomorphisms.  -/
CategoryTheory.PreGaloisCategory.FiberFunctor.instReflectsMonomorphismsFintypeCat : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {F : CategoryTheory.Functor C FintypeCat}
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F],
  F.ReflectsMonomorphisms
-- Mathlib.RingTheory.Multiplicity
multiplicity_eq_of_emultiplicity_eq_some : ∀ {α : Type u_1} [inst : Monoid α] {a b : α} {n : ℕ}, emultiplicity a b = ↑n → multiplicity a b = n
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.forget₂_algCat_obj : ∀ {R : Type u} [inst : CommRing R] (A : CommAlgCat R),
  (CategoryTheory.forget₂ (CommAlgCat R) (AlgCat R)).obj A = AlgCat.of R ↑A
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.unop_K : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.RightHomologyData), h.unop.K = Opposite.unop h.Q
-- Mathlib.Analysis.SpecialFunctions.Choose
/-- `n.descFactorial k` is asymptotically equivalent to `n^k`.  -/
isEquivalent_descFactorial : ∀ (k : ℕ), Asymptotics.IsEquivalent Filter.atTop (fun n => ↑(n.descFactorial k)) fun n => ↑n ^ k
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t ≠ ∅ → ∀ {km fallback : α}, t.maxKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for `Iso.inv η`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂.invM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂ m] →
    Mathlib.Tactic.BicategoryLike.Mor₂Iso → m Mathlib.Tactic.BicategoryLike.Mor₂
-- Mathlib.Tactic.NormNum.LegendreSymbol
/-- When `a` is odd and `b` is even, we can replace `b` by `b / 2`.  -/
Mathlib.Meta.NormNum.jacobiSymNat.odd_even : ∀ (a b c : ℕ) (r : ℤ),
  a % 2 = 1 →
    b % 2 = 0 → b / 2 = c → Mathlib.Meta.NormNum.jacobiSymNat a c = r → Mathlib.Meta.NormNum.jacobiSymNat a b = r
-- Init.GrindInstances.Ring.UInt
UInt8.ofInt.eq_1 : ∀ (x : ℤ), UInt8.ofInt x = UInt8.ofNat (x % 2 ^ 8).toNat
-- Mathlib.Algebra.Star.Subalgebra
StarAlgHom.adjoin_le_equalizer : ∀ {F : Type u_1} {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R]
  [inst_2 : Semiring A] [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : Semiring B] [inst_6 : Algebra R B]
  [inst_7 : StarRing B] [inst_8 : StarModule R A] [inst_9 : FunLike F A B] [inst_10 : AlgHomClass F R A B]
  [inst_11 : StarHomClass F A B] (f g : F) {s : Set A},
  Set.EqOn (⇑f) (⇑g) s → StarAlgebra.adjoin R s ≤ StarAlgHom.equalizer f g
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The matrix representation of `innerSL 𝕜 x` given by an orthonormal basis `b` and `b₂`
is equal to `vecMulVec (star b₂) (star (b.repr x))`.  -/
LinearMap.toMatrix_innerₛₗ_apply : ∀ {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {m : Type u_7} {n : Type u_8} [inst_3 : Fintype n] [inst_4 : DecidableEq n] [inst_5 : Fintype m]
  (b : OrthonormalBasis n 𝕜 E) (b₂ : OrthonormalBasis m 𝕜 𝕜) (x : E),
  (LinearMap.toMatrix b.toBasis b₂.toBasis) ((innerₛₗ 𝕜) x) = Matrix.vecMulVec (star ⇑b₂) (star (b.repr x).ofLp)
-- Std.Internal.Do.Order.Basic
/-- Binary meet (infimum)  -/
Lean.Order.«term_⊓_» : Lean.TrailingParserDescr
-- Init.Data.Float.Model.Format.Basic
/-- Specification corresponding to the IEEE `binary32` format.  -/
Float.Model.Format.binary32 : Float.Model.Format
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.addAux.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_3 ()
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ \ m₂},
  (m₁ \ m₂).get k h_mem = m₁.get k ⋯
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.instInhabited : {G : Type u_1} →
  [inst : Group G] →
    {A B : Subgroup G} → {d : HNNExtension.NormalWord.TransversalPair G A B} → Inhabited (HNNExtension.NormalWord d)
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.tensor_inv_hom_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {V W X Y Z : C}
  (f : V ≅ W) (g : X ⟶ Y) (h : Y ⟶ Z) {Z_1 : C} (h_1 : CategoryTheory.MonoidalCategoryStruct.tensorObj Z W ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f.inv)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom h f.hom) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom g (CategoryTheory.CategoryStruct.id W))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom h (CategoryTheory.CategoryStruct.id W)) h_1)
-- Mathlib.Order.Interval.Set.Basic
Set.Ici_zero_eq_univ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : Zero α] [IsBotZeroClass α], Set.Ici 0 = Set.univ
-- Lean.MetavarContext
Lean.LocalInstance.mk : Lean.Name → Lean.Expr → Lean.LocalInstance
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sub_eq_empty : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t : Finset α}, s - t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Topology.MetricSpace.UniformConvergence
UniformOnFun.lipschitzWith_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : PseudoEMetricSpace γ] {𝔖 : Set (Set α)}
  [inst_1 : PseudoEMetricSpace β] [inst_2 : Finite ↑𝔖] {f : γ → UniformOnFun α β 𝔖} {K : NNReal},
  LipschitzWith K f ↔ ∀ c ∈ ⋃₀ 𝔖, LipschitzWith K fun x => (UniformOnFun.toFun 𝔖) (f x) c
-- Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
MonoidAlgebra.instSMulForallOfIsLeftCancelSMulOfSMulWithZero.eq_1 : ∀ {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [inst : SMul G P] [inst_1 : IsLeftCancelSMul G P]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid V] [inst_4 : SMulWithZero R V],
  MonoidAlgebra.instSMulForallOfIsLeftCancelSMulOfSMulWithZero =
    { smul := fun f x p => ∑ gh ∈ Finset.SMulAntidiagonal p ⋯, f.coeff gh.1 • x gh.2 }
-- Std.Data.Iterators.Lemmas.Combinators.Monadic.DropWhile
Std.IterM.dropWhileM_eq_intermediateDropWhileM : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] [Std.Iterator α m β]
  {it : Std.IterM m β} {P : β → m (ULift.{u_1, 0} Bool)},
  Std.IterM.dropWhileM P it = Std.IterM.Intermediate.dropWhileM P true it
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.spanNorm_spanNorm : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] (T : Type u_4) [inst_9 : CommRing T] [inst_10 : IsDomain T]
  [inst_11 : IsIntegrallyClosed T] [inst_12 : Algebra R T] [inst_13 : Algebra T S] [inst_14 : Module.Finite R T]
  [inst_15 : Module.Finite T S] [inst_16 : Module.IsTorsionFree R T] [inst_17 : Module.IsTorsionFree T S]
  [IsScalarTower R T S] [IsDedekindDomain R] [IsDedekindDomain T] [IsDedekindDomain S] (I : Ideal S),
  Ideal.spanNorm R (Ideal.spanNorm T I) = Ideal.spanNorm R I
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.IsLocal.mem_jacobson_or_exists_inv : ∀ {R : Type u} [inst : CommRing R] {I : Ideal R}, I.IsLocal → ∀ (x : R), x ∈ I.jacobson ∨ ∃ y, y * x - 1 ∈ I
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.restrict : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.MutuallySingular ν → ∀ (s : Set α), (μ.restrict s).MutuallySingular ν
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_desc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain F K (-1)) (β : G ⟶ K)
  (eq :
    CochainComplex.HomComplex.δ (-1) 0 α =
      CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp φ β)),
  (CochainComplex.mappingCone.inl φ).comp
      (CochainComplex.HomComplex.Cochain.ofHom (CochainComplex.mappingCone.desc φ α β eq)) ⋯ =
    α
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.moduleEndSelf_apply_apply : ∀ (R : Type u_1) {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Aᵐᵒᵖ) (a : A),
  ((AlgEquiv.moduleEndSelf R) s) a = a * MulOpposite.unop s
-- Mathlib.LinearAlgebra.Matrix.Stochastic
/-- The all-ones column vector multiplied with a row stochastic matrix is 1.  -/
Matrix.one_vecMul_of_mem_rowStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R] {M : Matrix n n R}, M ∈ Matrix.rowStochastic R n → M.mulVec 1 = 1
-- Mathlib.Data.Nat.Nth
Nat.le_of_nth_le_nth_of_lt_card : ∀ {p : ℕ → Prop} (hf : (Set.ofPred p).Finite) {m n : ℕ}, Nat.nth p m ≤ Nat.nth p n → m < hf.toFinset.card → m ≤ n
-- Mathlib.RingTheory.PowerSeries.Evaluation
PowerSeries.HasEval.add : ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : TopologicalSpace S] [ContinuousAdd S] [IsLinearTopology S S] {a b : S},
  PowerSeries.HasEval a → PowerSeries.HasEval b → PowerSeries.HasEval (a + b)
-- Mathlib.Topology.Instances.Matrix
Topology.IsEmbedding.matrix_map : ∀ {m : Type u_11} {n : Type u_12} {R : Type u_13} {S : Type u_14} [inst : TopologicalSpace R]
  [inst_1 : TopologicalSpace S] {f : R → S}, Topology.IsEmbedding f → Topology.IsEmbedding fun x => x.map f
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.mem_closedBall_self : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ}, 0 ≤ ε → x ∈ Metric.closedBall x ε
-- Mathlib.CategoryTheory.Action.Monoidal
_private.Mathlib.CategoryTheory.Action.Monoidal.0.Action.diagonalSuccIsoTensorTrivial.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Data.Nat.Init
_private.Mathlib.Data.Nat.Init.0.Nat.leRec.match_1.eq_2 : ∀ {n : ℕ} (motive : (x : ℕ) → n ≤ x → Sort u_1) (m : ℕ) (H : n ≤ m + 1) (h_1 : (H : n ≤ 0) → motive 0 H)
  (h_2 : (m : ℕ) → (H : n ≤ m + 1) → motive m.succ H),
  (match m.succ, H with
    | 0, H => h_1 H
    | m.succ, H => h_2 m H) =
    h_2 m H
-- Init.Data.UInt.Bitwise
UInt64.not_inj : ∀ {a b : UInt64}, ~~~a = ~~~b ↔ a = b
-- Mathlib.Logic.Function.Basic
Function.instTotalSwapProp : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Total r], Std.Total (Function.swap r)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.map_id : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), Subsemiring.map (RingHom.id R) s = s
-- Mathlib.RingTheory.WittVector.Truncated
TruncatedWittVector.truncate_surjective : ∀ {p n : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {m : ℕ} (hm : n ≤ m),
  Function.Surjective ⇑(TruncatedWittVector.truncate hm)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.MonoidalPreadditive.add_whiskerRight : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {inst_1 : CategoryTheory.Preadditive C}
  {inst_2 : CategoryTheory.MonoidalCategory C} [self : CategoryTheory.MonoidalPreadditive C] {X Y Z : C} (f g : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight (f + g) X =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight f X + CategoryTheory.MonoidalCategoryStruct.whiskerRight g X
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
ContinuousVAdd.toMeasurableVAdd : ∀ {M : Type u_7} {α : Type u_8} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace α] [inst_2 : MeasurableSpace M]
  [inst_3 : MeasurableSpace α] [OpensMeasurableSpace M] [BorelSpace α] [inst_6 : VAdd M α] [ContinuousVAdd M α],
  MeasurableVAdd M α
-- Std.Do.PostCond
Std.Do.ExceptConds.entails.eq_2 : ∀ (σ : Type u) (ps_2 : Std.Do.PostShape) (x_2 y_2 : Std.Do.ExceptConds (Std.Do.PostShape.arg σ ps_2)),
  x_2.entails y_2 = x_2.entails y_2
-- Init.Data.Array.Range
Array.count_range_1' : ∀ {a s n : ℕ}, Array.count a (Array.range' s n) = if s ≤ a ∧ a < s + n then 1 else 0
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.dblZ.eq_1 : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) (P : Fin 3 → R),
  W'.dblZ P = P 2 * (P 1 - W'.negY P) ^ 3
-- Mathlib.Analysis.Fourier.FourierTransform
Fourier.fourierIntegral_const_smul : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] [inst_1 : MeasurableSpace 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure 𝕜) (f : 𝕜 → E) (r : ℂ),
  Fourier.fourierIntegral e μ (r • f) = r • Fourier.fourierIntegral e μ f
-- Mathlib.Analysis.Convex.Mul
ConcaveOn.mul' : ∀ {𝕜 : Type u_1} {E : Type u_2} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E] [inst_6 : AddCommGroup G] [inst_7 : Module 𝕜 G]
  [inst_8 : Module 𝕜 E] {s : Set G} [IsOrderedModule 𝕜 E] [IsScalarTower 𝕜 E E] [SMulCommClass 𝕜 E E] {f g : G → E},
  ConcaveOn 𝕜 s f →
    ConcaveOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → f x ≤ 0) → (∀ ⦃x : G⦄, x ∈ s → g x ≤ 0) → MonovaryOn f g s → ConvexOn 𝕜 s (f * g)
-- Mathlib.Topology.Hom.Open
/-- `id` as a `ContinuousOpenMap`.  -/
ContinuousOpenMap.id : (α : Type u_2) → [inst : TopologicalSpace α] → α →CO α
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- See `card_le_card_add_right` for a more convenient but less general version for types with a
right-cancellative addition.  -/
Finset.card_le_card_add_right_of_injective : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α} {a : α},
  a ∈ t → IsAddRightRegular a → s.card ≤ (s + t).card
-- Mathlib.Algebra.Category.Ring.Adjunctions
CommRingCat.coyoneda_obj_obj_carrier : ∀ (n : Type vᵒᵖ) (R : CommRingCat), ↑((CommRingCat.coyoneda.obj n).obj R) = (Opposite.unop n → ↑R)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Additive.toMul.eq_1 : ∀ {α : Type u}, Additive.toMul = Additive.ofMul.symm
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv_mem_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set F} {x : 𝕜},
  deriv f x ∈ s ↔ DifferentiableAt 𝕜 f x ∧ deriv f x ∈ s ∨ ¬DifferentiableAt 𝕜 f x ∧ 0 ∈ s
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.zpow_apply_eq_zpow_apply : ∀ {α : Type u_2} {f : Equiv.Perm α} {a : α} {s : Finset α},
  f.IsCycleOn ↑s → a ∈ s → ∀ {m n : ℤ}, (f ^ m) a = (f ^ n) a ↔ m ≡ n [ZMOD ↑s.card]
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InsertReplaceEdit.replace : Lean.Lsp.InsertReplaceEdit → Lean.Lsp.Range
-- Mathlib.Tactic.Ring.Basic
/-- Converts `ExBase sα` to `ExBase sβ`, assuming `sα` and `sβ` are defeq.  -/
Mathlib.Tactic.Ring.ExBase.cast : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      {v : Lean.Level} →
        {β : Q(Type v)} →
          {sβ : Q(CommSemiring «$β»)} →
            {a : Q(«$α»)} → Mathlib.Tactic.Ring.ExBase sα a → (a : Q(«$β»)) × Mathlib.Tactic.Ring.ExBase sβ a
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.zeroHomClass : ∀ {R : Type u_5} {S : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : PartialOrder S],
  ZeroHomClass (AbsoluteValue R S) R S
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.Approx.CofixA.brecOn.go : {F : PFunctor.{uA, uB}} →
  {motive : (a : ℕ) → PFunctor.Approx.CofixA F a → Sort u} →
    {a : ℕ} →
      (t : PFunctor.Approx.CofixA F a) →
        ((a : ℕ) → (t : PFunctor.Approx.CofixA F a) → PFunctor.Approx.CofixA.below t → motive a t) →
          motive a t ×' PFunctor.Approx.CofixA.below t
-- Mathlib.Algebra.Module.Basic
Function.support_const_smul_subset : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : SMulZeroClass R M] (a : R) (f : α → M),
  Function.support (a • f) ⊆ Function.support f
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.denoteAsRing_eq : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (e : Lean.Grind.CommRing.Expr),
  Lean.Grind.CommRing.Expr.denoteSAsRing ctx e = ↑(Lean.Grind.CommRing.Expr.denoteS ctx e)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.instDecidableOrderedOfTransCmp : {α : Type u_1} →
  (cmp : α → α → Ordering) → [Std.TransCmp cmp] → (t : RBTree.RBNode α) → Decidable (RBTree.RBNode.Ordered cmp t)
-- Mathlib.Order.CompleteBooleanAlgebra
/-- `(· \ a)` is left adjoint to `(· ⊔ a)`  -/
CompleteDistribLattice.sdiff_le_iff : ∀ {α : Type u_1} [self : CompleteDistribLattice α] (a b c : α), a \ b ≤ c ↔ a ≤ b ⊔ c
-- Mathlib.SetTheory.Ordinal.Basic
/-- **Alias** of `Ordinal.isEmpty_toType_iff`. -/
Ordinal.toType_empty_iff_eq_zero : ∀ {o : Ordinal.{u_1}}, IsEmpty o.ToType ↔ o = 0
-- Mathlib.GroupTheory.RegularWreathProduct
RegularWreathProduct.instFinite : ∀ {D : Type u_1} {Q : Type u_2} [Finite D] [Finite Q], Finite (D ≀ᵣ Q)
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.op_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G H : CategoryTheory.Functor C D} (α : F ⟶ G) (β : G ⟶ H),
  CategoryTheory.NatTrans.op (CategoryTheory.CategoryStruct.comp α β) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.NatTrans.op β) (CategoryTheory.NatTrans.op α)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.nnnorm_toLp_inr : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (y : β), ‖WithLp.toLp p (0, y)‖₊ = ‖y‖₊
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_ric_ne_nil : ∀ {n : ℕ}, (*...=n).toArray ≠ #[]
-- Mathlib.Data.Set.Image
/-- The image of a nontrivial set under an injective map is nontrivial.  -/
Set.Nontrivial.image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, s.Nontrivial → Function.Injective f → (f '' s).Nontrivial
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iio_inj : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, Set.Iio a = Set.Iio b ↔ a = b
-- Mathlib.Algebra.Group.Hom.Basic
/-- If `f` and `g` are monoid homomorphisms to a commutative group, then `f / g` is the homomorphism
sending `x` to `(f x) / (g x)`.  -/
MonoidHom.instDiv : {M : Type u_2} → {G : Type u_5} → [inst : MulOneClass M] → [inst_1 : CommGroup G] → Div (M →* G)
-- Mathlib.Algebra.Polynomial.Bivariate
/-- Viewing `R[X,Y,X']` as an `R[X']`-algebra, a polynomial `p : R[X',Y']` can be evaluated at
`Y : R[X,Y,X']` (substitution of `Y'` by `Y`), obtaining another polynomial in `R[X,Y,X']`.
When this polynomial is then evaluated at `X' = X`, the original polynomial `p` is recovered.  -/
Polynomial.eval_C_X_eval₂_map_C_X : ∀ {R : Type u_1} [inst : CommSemiring R] {p : Polynomial (Polynomial R)},
  Polynomial.eval (Polynomial.C Polynomial.X)
      (Polynomial.eval₂ (Polynomial.mapRingHom (algebraMap R (Polynomial (Polynomial R)))) (Polynomial.C Polynomial.X)
        p) =
    p
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_union : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {s t : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] [TopologicalSpace.PseudoMetrizableSpace ε],
  MeasureTheory.IntegrableOn f (s ∪ t) μ ↔ MeasureTheory.IntegrableOn f s μ ∧ MeasureTheory.IntegrableOn f t μ
-- Mathlib.Data.List.Chain
List.IsChain.cons_of_ne_nil : ∀ {α : Type u_1} {R : α → α → Prop} {x : α} {l : List α} (l_ne_nil : l ≠ []),
  List.IsChain R l → R x (l.head l_ne_nil) → List.IsChain R (x :: l)
-- Aesop.Tracing
Aesop.TraceOption.steps : Aesop.TraceOption