mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.self_trans_symm : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), e.trans e.symm = AffineEquiv.refl k P₁
-- Mathlib.FieldTheory.NormalizedTrace
/-- The normalized trace transfers via restriction to a subextension.  -/
Algebra.normalizedTrace_intermediateField : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] [inst_3 : CharZero F]
  [inst_4 : Algebra.IsIntegral F K] {E : IntermediateField F K} (a : ↥E),
  (Algebra.normalizedTrace F K) ↑a = (Algebra.normalizedTrace F ↥E) a
-- Init.Data.Option.Lemmas
Option.map_eq_none_iff : ∀ {α : Type u_1} {x : Option α} {α_1 : Type u_2} {f : α → α_1}, Option.map f x = none ↔ x = none
-- Aesop.Tree.Traversal
Aesop.TreeRef.goal.injEq : ∀ (gref gref_1 : Aesop.GoalRef), (Aesop.TreeRef.goal gref = Aesop.TreeRef.goal gref_1) = (gref = gref_1)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.piTensorHomMap₂_tprod_tprod_tprod : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} {t' : ι → Type u_12} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] [inst_5 : (i : ι) → AddCommMonoid (t' i)] [inst_6 : (i : ι) → Module R (t' i)]
  (f : (i : ι) → s i →ₗ[R] t i →ₗ[R] t' i) (a : (i : ι) → s i) (b : (i : ι) → t i),
  ((PiTensorProduct.piTensorHomMap₂ ((PiTensorProduct.tprod R) f)) ((PiTensorProduct.tprod R) a))
      ((PiTensorProduct.tprod R) b) =
    ⨂ₜ[R] (i : ι), ((f i) (a i)) (b i)
-- Std.Time.Format
/-- Formats a `DateTime` value into a simple date time with timezone string that can be parsed by the date% notation.
 -/
Std.Time.DateTime.toLeanDateTimeWithZoneString : Std.Time.DateTime → String
-- Mathlib.RingTheory.Artinian.Ring
/-- `IsArtinianRing.localization_artinian` can't be made an instance, as it would make `S` + `R`
into metavariables. However, this is safe.  -/
IsArtinianRing.instLocalization : ∀ {R : Type u_1} [inst : CommRing R] [IsArtinianRing R] (S : Submonoid R), IsArtinianRing (Localization S)
-- Lean.Elab.Quotation.Precheck
Lean.Elab.Term.Quotation.Precheck.Context.mk.injEq : ∀ (quotLCtx quotLCtx_1 : Lean.NameSet),
  ({ quotLCtx := quotLCtx } = { quotLCtx := quotLCtx_1 }) = (quotLCtx = quotLCtx_1)
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.WorkItem.indent : Std.Format.WorkItem✝ → ℤ
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- The identity copy from a simple graph to itself.  -/
SimpleGraph.Copy.id : {V : Type u_1} → (G : SimpleGraph V) → G.Copy G
-- Mathlib.Algebra.Group.Conj
IsConj.eq_1 : ∀ {α : Type u} [inst : Monoid α] (a b : α), IsConj a b = ∃ c, SemiconjBy (↑c) a b
-- Mathlib.Data.Set.Image
Set.subsingleton_range : ∀ {β : Type u_2} {α : Sort u_5} [Subsingleton α] (f : α → β), (Set.range f).Subsingleton
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
ContDiffAt.sin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {n : WithTop ℕ∞},
  ContDiffAt ℝ n f x → ContDiffAt ℝ n (fun x => Real.sin (f x)) x
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometry.mk : {𝕜 : Type u_1} →
  {V : Type u_2} →
    {V₂ : Type u_5} →
      {P : Type u_10} →
        {P₂ : Type u_11} →
          [inst : NormedField 𝕜] →
            [inst_1 : SeminormedAddCommGroup V] →
              [inst_2 : NormedSpace 𝕜 V] →
                [inst_3 : PseudoMetricSpace P] →
                  [inst_4 : NormedAddTorsor V P] →
                    [inst_5 : SeminormedAddCommGroup V₂] →
                      [inst_6 : NormedSpace 𝕜 V₂] →
                        [inst_7 : PseudoMetricSpace P₂] →
                          [inst_8 : NormedAddTorsor V₂ P₂] →
                            (toAffineMap : P →ᵃ[𝕜] P₂) → (∀ (x : V), ‖toAffineMap.linear x‖ = ‖x‖) → P →ᵃⁱ[𝕜] P₂
-- Lean.CoreM
Lean.MonadRuntimeException.mk : {m : Type → Type} → ({α : Type} → m α → (Lean.Exception → m α) → m α) → Lean.MonadRuntimeException m
-- Mathlib.RingTheory.Smooth.IntegralClosure
/-- Base changing to `MvPolynomial σ R` preserves integral closure.  -/
TensorProduct.toIntegralClosure_mvPolynomial_bijective : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing B] [inst_2 : Algebra R B] {σ : Type u_4},
  Function.Bijective ⇑(TensorProduct.toIntegralClosure R (MvPolynomial σ R) B)
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- An `AddSubgroup` of an `AddGroup` inherits a zero.  -/
AddSubgroup.zero : {G : Type u_1} → [inst : AddGroup G] → (H : AddSubgroup G) → Zero ↥H
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to0.trAux.match_1.eq_6 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (motive : Turing.TM1.Stmt Γ Λ σ → σ → Sort u_4) (v : σ)
  (h_1 : (d : Turing.Dir) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.move d q) v)
  (h_2 : (a : Γ → σ → Γ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.write a q) v)
  (h_3 : (a : Γ → σ → σ) → (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.load a q) v)
  (h_4 : (p : Γ → σ → Bool) → (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v)
  (h_5 : (l : Γ → σ → Λ) → (v : σ) → motive (Turing.TM1.Stmt.goto l) v) (h_6 : (v : σ) → motive Turing.TM1.Stmt.halt v),
  (match Turing.TM1.Stmt.halt, v with
    | Turing.TM1.Stmt.move d q, v => h_1 d q v
    | Turing.TM1.Stmt.write a q, v => h_2 a q v
    | Turing.TM1.Stmt.load a q, v => h_3 a q v
    | Turing.TM1.Stmt.branch p q₁ q₂, v => h_4 p q₁ q₂ v
    | Turing.TM1.Stmt.goto l, v => h_5 l v
    | Turing.TM1.Stmt.halt, v => h_6 v) =
    h_6 v
-- Init.Data.BitVec.Bitblast
/-- the denominator (aka, divisor) -/
BitVec.DivModArgs.d : {w : ℕ} → BitVec.DivModArgs w → BitVec w
-- Mathlib.Topology.Order
continuous_sup_rng_right : ∀ {α : Type u} {β : Type v} {f : α → β} {t₁ : TopologicalSpace α} {t₃ t₂ : TopologicalSpace β},
  Continuous f → Continuous f
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.hasCoproducts_of_opposite : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasProducts Cᵒᵖ],
  CategoryTheory.Limits.HasCoproducts C
-- Mathlib.Data.Countable.Basic
countable_prod_swap : ∀ {α : Type u} {β : Type v} [Countable (α × β)], Countable (β × α)
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
/-- A morphism property stable under left and right unitor isomorphisms.  -/
CategoryTheory.MorphismProperty.IsStableUnderUnitor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.MonoidalCategory C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.mk_base : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {X Y : CategoryTheory.CatEnrichedOrdinary C}
  {f g : X ⟶ Y} (α : f ⟶ g),
  CategoryTheory.CatEnrichedOrdinary.Hom.mk (CategoryTheory.CatEnrichedOrdinary.Hom.base α) = α
-- Mathlib.Order.Preorder.Chain
Flag.le_or_le : ∀ {α : Type u_1} [inst : Preorder α] {a b : α} (s : Flag α), a ∈ s → b ∈ s → a ≤ b ∨ b ≤ a
-- Mathlib.CategoryTheory.Triangulated.TStructure.Induced
CategoryTheory.ObjectProperty.tStructure_isLE_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) (t : CategoryTheory.Triangulated.TStructure C) [inst_6 : P.IsTriangulated]
  [h : P.HasInducedTStructure t] (X : P.FullSubcategory) (n : ℤ), (P.tStructure t).IsLE X n ↔ t.IsLE X.obj n
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.e_assoc : ∀ (V : Type v) [inst : CategoryTheory.Category.{w, v} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u₁}
  [inst_2 : CategoryTheory.EnrichedCategory V C] (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (W ⟶[V] X) (X ⟶[V] Y) (Y ⟶[V] Z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.eComp V W X Y) (Y ⟶[V] Z))
        (CategoryTheory.eComp V W Y Z)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (W ⟶[V] X) (CategoryTheory.eComp V X Y Z))
      (CategoryTheory.eComp V W X Z)
-- Lean.Elab.Tactic.Conv.Pattern
Lean.Elab.Tactic.Conv.evalPattern : Lean.Elab.Tactic.Tactic
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If `f` is a monotone function on a left neighborhood of `a` and the image of this neighborhood
under `f` meets every interval `(b, f a)`, `b < f a`, then `f` is continuous at `a` from the left.

The assumption `hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ioo b (f a)` cannot be replaced by the weaker
assumption `hfs : ∀ b < f a, ∃ c ∈ s, f c ∈ Ico b (f a)` we use for strictly monotone functions
because otherwise the function `floor : ℝ → ℤ` would be a counter-example at `a = 0`.  -/
continuousWithinAt_left_of_monotoneOn_of_exists_between : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] {f : α → β} {s : Set α} {a : α},
  MonotoneOn f s →
    s ∈ nhdsWithin a (Set.Iic a) → (∀ b < f a, ∃ c ∈ s, f c ∈ Set.Ioo b (f a)) → ContinuousWithinAt f (Set.Iic a) a
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Modification.ext : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F G : CategoryTheory.LaxFunctor B C} {η θ : F ⟶ G} {x y : CategoryTheory.Lax.LaxTrans.Modification η θ},
  x.app = y.app → x = y
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- Adjoining a finite subset is compact in the lattice of intermediate fields.  -/
IntermediateField.adjoin_finset_isCompactElement : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (S : Finset E),
  IsCompactElement (IntermediateField.adjoin F ↑S)
-- Std.Http.Protocol.H1
/-- Events that occurred during this step (e.g., headers received, control flow, errors).
 -/
Std.Http.Protocol.H1.StepResult.events : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.StepResult dir → Array (Std.Http.Protocol.H1.Event dir)
-- Init.Grind.Order
Lean.Grind.Order.lt_trans_k : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [Std.LawfulOrderLT α] [inst_3 : Std.IsPreorder α]
  [inst_4 : Lean.Grind.Ring α] [Lean.Grind.OrderedRing α] {a b c : α} {k₁ k₂ : ℤ} (k : ℤ),
  a < b + ↑k₁ → b < c + ↑k₂ → (k == k₂ + k₁) = true → a < c + ↑k
-- Mathlib.Computability.EpsilonNFA
εNFA.eval.eq_1 : ∀ {α : Type u} {σ : Type v} (M : εNFA α σ), M.eval = M.evalFrom M.start
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionList.mk.sizeOf_spec : ∀ (isIncomplete : Bool) (items : Array Lean.Lsp.CompletionItem),
  sizeOf { isIncomplete := isIncomplete, items := items } = 1 + sizeOf isIncomplete + sizeOf items
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Turan
SimpleGraph.IsTuranMaximal.congr_simp : ∀ {V : Type u_1} [inst : Fintype V] (G G_1 : SimpleGraph V),
  G = G_1 →
    ∀ {inst_1 : DecidableRel G.Adj} [inst_2 : DecidableRel G_1.Adj] (r r_1 : ℕ),
      r = r_1 → G.IsTuranMaximal r = G_1.IsTuranMaximal r_1
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Multiset.sum_count_eq_card : ∀ {ι : Type u_1} [inst : DecidableEq ι] {s : Finset ι} {m : Multiset ι},
  (∀ a ∈ m, a ∈ s) → ∑ a ∈ s, Multiset.count a m = m.card
-- Mathlib.LinearAlgebra.Complex.FiniteDimensional
rank_real_of_complex : ∀ (E : Type u_1) [inst : AddCommGroup E] [inst_1 : Module ℂ E], Module.rank ℝ E = 2 * Module.rank ℂ E
-- Mathlib.LinearAlgebra.Charpoly.Basic
LinearMap.eval_charpoly : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : Module.Free R M] [inst_4 : Module.Finite R M] (f : M →ₗ[R] M) (t : R),
  Polynomial.eval t f.charpoly = LinearMap.det ((algebraMap R (M →ₗ[R] M)) t - f)
-- Mathlib.Data.Seq.Computation
Computation.map_pure' : ∀ {α β : Type u_1} (f : α → β) (a : α), f <$> Computation.pure a = Computation.pure (f a)
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
_private.Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal.0.AugmentedSimplexCategory.tensorObj.match_1.splitter : (motive : AugmentedSimplexCategory → AugmentedSimplexCategory → Sort u_1) →
  (m n : AugmentedSimplexCategory) →
    ((m n : SimplexCategory) → motive (CategoryTheory.WithInitial.of m) (CategoryTheory.WithInitial.of n)) →
      ((x : AugmentedSimplexCategory) → motive CategoryTheory.WithInitial.star x) →
        ((x : AugmentedSimplexCategory) →
            (x = CategoryTheory.WithInitial.star → False) → motive x CategoryTheory.WithInitial.star) →
          motive m n
-- Lean.Meta.Instances
Lean.Meta.getDefaultInstances : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (List (Lean.Name × ℕ))
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.mem_star_iff : ∀ {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 : StarModule R A] (S : NonUnitalSubalgebra R A) (x : A),
  x ∈ star S ↔ star x ∈ S
-- Mathlib.RingTheory.Noetherian.Basic
/-- If `S` is disjoint from `T` and `M ⧸ T` is a noetherian module, then `S` is FG.
See also `Submodule.CoFG.fg_of_disjoint`.  -/
Submodule.FG.of_disjoint_of_isNoetherian_quotient : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S T : Submodule R M}
  [IsNoetherian R (M ⧸ T)], Disjoint S T → S.FG
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticReciprocity
legendreSym.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [inst : Fact (Nat.Prime p)] (a a_1 : ℤ), a = a_1 → legendreSym p a = legendreSym p_1 a_1
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithTop.map_add : ∀ {α : Type u} {β : Type v} [inst : Add α] {F : Type u_1} [inst_1 : Add β] [inst_2 : FunLike F α β] [AddHomClass F α β]
  (f : F) (a b : WithTop α), WithTop.map (⇑f) (a + b) = WithTop.map (⇑f) a + WithTop.map (⇑f) b
-- Mathlib.Data.Finsupp.Basic
Finsupp.support_filter : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M),
  (Finsupp.filter p f).support = {x ∈ f.support | p x}
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.immediate.inj : ∀ {names names_1 : Array Lean.Name},
  Aesop.Frontend.BuilderOption.immediate names = Aesop.Frontend.BuilderOption.immediate names_1 → names = names_1
-- Mathlib.Algebra.Module.Submodule.Pointwise
Submodule.pointwiseZero : {R : Type u_2} →
  {M : Type u_3} → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Zero (Submodule R M)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Applying a linear map to a vector is differentiable. Version in vector spaces. For a
version in nontrivial vector bundles, see `MDifferentiableAt.clm_apply_of_inCoordinates`.  -/
MDifferentiableAt.clm_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_14} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_15} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂]
  {g : M → F₁ →L[𝕜] F₂} {f : M → F₁} {x : M}, MDiffAt g x → MDiffAt f x → (MDiffAt fun x => (g x) (f x)) x
-- Std.Data.HashSet.Lemmas
Std.HashSet.isEmpty_diff_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  (m₁ \ m₂).isEmpty = true ↔ ∀ k ∈ m₁, k ∈ m₂
-- Lean.Elab.Binders
Lean.Elab.Term.elabLetFunDecl : Lean.Elab.Term.TermElab
-- Mathlib.Data.QPF.Univariate.Basic
QPF.supp_eq_of_isUniform : ∀ {F : Type u → Type u} [q : QPF F],
  QPF.IsUniform →
    ∀ {α : Type u} (a : (QPF.P F).A) (f : (QPF.P F).B a → α), Functor.supp (QPF.abs ⟨a, f⟩) = f '' Set.univ
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.add_apply : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  (f g : NormedAddGroupHom V₁ V₂) (v : V₁), (f + g) v = f v + g v
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.lt_mul_add_one_iff : ∀ {a b c : Ordinal.{u_4}}, a < b * (c + 1) ↔ ∃ d < b, a ≤ b * c + d
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- If `‖v‖^n * ‖f v‖` is integrable, then the `n`-th derivative of the Fourier transform of `f` is
the Fourier transform of `fun v ↦ (-2 * π * I) ^ n ⟪v, ⬝⟫^n f v`.  -/
Real.iteratedFDeriv_fourier : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {f : V → E} {N : ℕ∞},
  (∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ n * ‖f v‖) MeasureTheory.volume) →
    MeasureTheory.AEStronglyMeasurable f MeasureTheory.volume →
      ∀ {n : ℕ},
        ↑n ≤ N →
          iteratedFDeriv ℝ n (FourierTransform.fourier f) =
            FourierTransform.fourier fun v => VectorFourier.fourierPowSMulRight (innerSL ℝ) f v n
-- Mathlib.Probability.Kernel.MeasurableIntegral
MeasureTheory.StronglyMeasurable.integral_kernel_prod_right : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_4} [inst : NormedAddCommGroup E] [ProbabilityTheory.IsSFiniteKernel κ] [inst_2 : NormedSpace ℝ E]
  ⦃f : α → β → E⦄,
  MeasureTheory.StronglyMeasurable (Function.uncurry f) →
    MeasureTheory.StronglyMeasurable fun x => ∫ (y : β), f x y ∂κ x
-- Mathlib.CategoryTheory.Whiskering
/-- Auxiliary definition for `whiskeringLeft₃`.  -/
CategoryTheory.Functor.whiskeringLeft₃ObjObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    (C₃ : Type u_3) →
      {D₁ : Type u_4} →
        {D₂ : Type u_5} →
          (D₃ : Type u_6) →
            [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
              [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
                [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
                  [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁] →
                    [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] →
                      [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] →
                        (E : Type u_7) →
                          [inst_6 : CategoryTheory.Category.{v_7, u_7} E] →
                            CategoryTheory.Functor C₁ D₁ →
                              CategoryTheory.Functor C₂ D₂ →
                                CategoryTheory.Functor (CategoryTheory.Functor C₃ D₃)
                                  (CategoryTheory.Functor
                                    (CategoryTheory.Functor D₁
                                      (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E)))
                                    (CategoryTheory.Functor C₁
                                      (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))))
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.finite_right : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {T : Set G} [H.FiniteIndex],
  AddSubgroup.IsComplement (↑H) T → T.Finite
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.adjoint_comp_self_eq_zero_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] {A : E →L[𝕜] F}, ContinuousLinearMap.adjoint A ∘SL A = 0 ↔ A = 0
-- Mathlib.RingTheory.GradedAlgebra.RingHom
/-- Composition of graded ring homomorphisms is a graded ring homomorphism.  -/
GradedRingHom.comp : {ι : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        {σ : Type u_6} →
          {τ : Type u_7} →
            {ψ : Type u_8} →
              [inst : Semiring A] →
                [inst_1 : Semiring B] →
                  [inst_2 : Semiring C] →
                    [inst_3 : SetLike σ A] →
                      [inst_4 : SetLike τ B] →
                        [inst_5 : SetLike ψ C] →
                          {𝒜 : ι → σ} → {ℬ : ι → τ} → {𝒞 : ι → ψ} → (ℬ →+*ᵍ 𝒞) → (𝒜 →+*ᵍ ℬ) → 𝒜 →+*ᵍ 𝒞
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.length_toList : ∀ {α : Type u} {r : Std.Roi α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.HasSize α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [inst_3 : Std.Rxi.IsAlwaysFinite α] [Std.Rxi.LawfulHasSize α],
  r.toList.length = r.size
-- Mathlib.Data.TypeVec
TypeVec.dropFun_appendFun : ∀ {n : ℕ} {α : TypeVec.{u_1} n} {α' : TypeVec.{u_2} n} {β : Type u_1} {β' : Type u_2} (f : α.Arrow α') (g : β → β'),
  TypeVec.dropFun (f ::: g) = f
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulBackwardPatternModel.skipSuffix?_eq_some_iff : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.BackwardPattern pat}
  {inst_1 : String.Slice.Pattern.Model.PatternModel pat}
  [self : String.Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String.Slice} (pos : s.Pos),
  String.Slice.Pattern.BackwardPattern.skipSuffix? pat s = some pos ↔
    String.Slice.Pattern.Model.IsLongestRevMatch pat pos
-- Mathlib.Algebra.GroupWithZero.WithZero
MulEquiv.withZero_symm_apply_symm_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : Group α] [inst_1 : Group β] (e : WithZero α ≃* WithZero β) (x : β),
  (MulEquiv.withZero.symm e).symm x = WithZero.unzero ⋯
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
/-- Rotating the triangle `mappingCocone.triangle φ` gives a triangle that is
isomorphic to `mappingCone.triangle φ`.  -/
CochainComplex.mappingCocone.rotateTriangleIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (φ : K ⟶ L) →
          [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] →
            (CochainComplex.mappingCocone.triangle φ).rotate ≅ CochainComplex.mappingCone.triangle φ
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.cancelDen.inj : ∀ {c : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr} {val : ℤ} {x n : Lean.Grind.Linarith.Var}
  {c_1 : Lean.Meta.Grind.Arith.Linear.RingIneqCnstr} {val_1 : ℤ} {x_1 n_1 : Lean.Grind.Linarith.Var},
  Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.cancelDen c val x n =
      Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof.cancelDen c_1 val_1 x_1 n_1 →
    c = c_1 ∧ val = val_1 ∧ x = x_1 ∧ n = n_1
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.OplaxFunctor.bicategory_whiskerLeft_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (η : x ⟶ x_1) (x_3 x_4 : x_1 ⟶ x_2) (Γ : x_3 ⟶ x_4) (a : B),
  (CategoryTheory.Bicategory.whiskerLeft η Γ).as.app a = CategoryTheory.Bicategory.whiskerLeft (η.app a) (Γ.as.app a)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toList_mapM_eq_toList_filterMapM : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → n γ} {it : Std.IterM m β},
  (Std.IterM.mapM f it).toList = (Std.IterM.filterMapM (fun b => some <$> f b) it).toList