mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Subcategory
/-- [Stacks Tag 0FX1](https://stacks.math.columbia.edu/tag/0FX1) -/
CategoryTheory.ObjectProperty.extensionProduct_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P Q R : CategoryTheory.ObjectProperty C) [CategoryTheory.IsTriangulated C],
  (P.extensionProduct Q).extensionProduct R = P.extensionProduct (Q.extensionProduct R)
-- Mathlib.Order.BoundedOrder.Basic
topOrderOrNoTopOrder.eq_1 : ∀ (α : Type u_1) [inst : LE α],
  topOrderOrNoTopOrder α =
    if H : ∀ (a : α), ∃ b, ¬b ≤ a then PSum.inr ⋯ else PSum.inl { top := Classical.choose ⋯, le_top := ⋯ }
-- ProofWidgets.Data.Html
ProofWidgets.Jsx.transformTag : Lean.Syntax →
  Lean.Ident →
    Lean.Ident →
      Array (Lean.TSyntax `proofWidgetsJsxAttr) → Array (Lean.TSyntax `proofWidgetsJsxChild) → Lean.MacroM Lean.Term
-- Lean.Expr
Lean.instLTLiteral : LT Lean.Literal
-- Mathlib.Tactic.TacticAnalysis
Mathlib.TacticAnalysis.Config.mk.injEq : ∀ (run run_1 : Array Mathlib.TacticAnalysis.TacticNode → Lean.Elab.Command.CommandElabM Unit),
  ({ run := run } = { run := run_1 }) = (run = run_1)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiff.contMDiffAt : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {n : WithTop ℕ∞},
  ContMDiff I I' n f → ContMDiffAt I I' n f x
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ContInfoRef.toContInfo : Lean.Elab.Do.ContInfoRef → Lean.Elab.Do.ContInfo
-- Mathlib.Data.QPF.Multivariate.Constructions.Cofix
MvQPF.Cofix.dest.eq_1 : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n},
  MvQPF.Cofix.dest =
    Quot.lift
      (fun x => MvFunctor.map (TypeVec.id ::: Quot.mk MvQPF.Mcongr) (MvQPF.abs (MvPFunctor.M.dest (MvQPF.P F) x))) ⋯
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.isAdjMatrix_reindex_iff : ∀ {α : Type u_1} {V : Type u_2} {W : Type u_3} {A : Matrix V V α} [inst : Zero α] [inst_1 : One α] {f : V ≃ W},
  ((Matrix.reindex f f) A).IsAdjMatrix ↔ A.IsAdjMatrix
-- Mathlib.Topology.Category.Profinite.Nobeling.Basic
Profinite.NobelingProof.spanFunctorIsoIndexFunctor_inv_app : ∀ {I : Type u} {C : Set (I → Bool)} [inst : (s : Finset I) → (i : I) → Decidable (i ∈ s)] (hC : IsCompact C)
  (X : (Finset I)ᵒᵖ),
  (Profinite.NobelingProof.spanFunctorIsoIndexFunctor hC).inv.app X =
    (CompHausLike.isoOfBijective
        (CategoryTheory.ConcreteCategory.ofHom (Profinite.NobelingProof.iso_map C fun x => x ∈ Opposite.unop X)) ⋯).inv
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.fun_comp_of_injective : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {β : Type u_3} {f : β → M} {g : α → β},
  Function.Injective g → Function.HasFiniteSupport f → Function.HasFiniteSupport fun a => f (g a)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.mkPiRing_eq_zero_iff : ∀ {R : Type uR} {ι : Type uι} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂] [inst_2 : Module R M₂]
  [inst_3 : Fintype ι] (z : M₂), MultilinearMap.mkPiRing R ι z = 0 ↔ z = 0
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.uliftYonedaFunctor_preservesLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, max (max u v) w', u, max (max u (v + 1)) (w' + 1)}
    CategoryTheory.uliftYoneda.{w', v, u}
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.Rewrites.exists_parts : ∀ {T : Type u_1} {N : Type u_2} {r : ContextFreeRule T N} {u v : List (Symbol T N)},
  r.Rewrites u v → ∃ p q, u = p ++ [Symbol.nonterminal r.input] ++ q ∧ v = p ++ r.output ++ q
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.neighborFinset_boxProd : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} (x : α × β)
  [inst : Fintype ↑(G.neighborSet x.1)] [inst_1 : Fintype ↑(H.neighborSet x.2)]
  [inst_2 : Fintype ↑((G □ H).neighborSet x)],
  (G □ H).neighborFinset x = (G.neighborFinset x.1 ×ˢ {x.2}).disjUnion ({x.1} ×ˢ H.neighborFinset x.2) ⋯
-- Std.Internal.Do.Triple.Basic
Std.Internal.Do.Triple.iff_conseq : ∀ {Pred EPred : Type u} {Prog : Type v} {Value : Type u} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] {x : Prog} {pre : Pred}
  {post : Value → Pred} {epost : EPred},
  ⦃ pre ⦄ x ⦃ post; epost ⦄ ↔
    ∀ (pre' : Pred) (post' : Value → Pred),
      Lean.Order.PartialOrder.rel pre' pre →
        Lean.Order.PartialOrder.rel post post' → Lean.Order.PartialOrder.rel pre' (Std.Internal.Do.wp x post' epost)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_mul_left_Iic : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀},
  0 < a → ∀ (b : G₀), (fun x => a * x) '' Set.Iic b = Set.Iic (a * b)
-- Batteries.Data.Fin.Lemmas
Fin.eq_true_of_find?_eq_some : ∀ {n : ℕ} {i : Fin n} {p : Fin n → Bool}, Fin.find? p = some i → p i = true
-- Mathlib.Order.UpperLower.Basic
IsUpperSet.eq_empty_or_Ici : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} [WellFoundedLT α], IsUpperSet s → s = ∅ ∨ ∃ a, s = Set.Ici a
-- Mathlib.CategoryTheory.ObjectProperty.LimitsOfShape
CategoryTheory.ObjectProperty.LimitOfShape.toStructuredArrow_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] {X : C} (p : P.LimitOfShape J X) (j : J),
  p.toStructuredArrow.obj j = CategoryTheory.StructuredArrow.mk (p.π.app j)
-- Std.Do.PredTrans
Std.Do.PredTrans.apply_dite : ∀ {α : Type u} {ps : Std.Do.PostShape} {Q : Std.Do.PostCond α ps} (c : Prop) [inst : Decidable c]
  (t : c → Std.Do.PredTrans ps α) (e : ¬c → Std.Do.PredTrans ps α),
  (if h : c then t h else e h).apply Q = if h : c then (t h).apply Q else (e h).apply Q
-- Mathlib.NumberTheory.NumberField.Discriminant.Different
NumberField.isCoprime_differentIdeal_of_isCoprime_discr : ∀ (L : Type u_3) [inst : Field L] {K₁ : Type u_4} {K₂ : Type u_5} [inst_1 : Field K₁] [inst_2 : NumberField K₁]
  [inst_3 : Field K₂] [inst_4 : NumberField K₂] [inst_5 : Algebra K₁ L] [inst_6 : Algebra K₂ L],
  IsCoprime (NumberField.discr K₁) (NumberField.discr K₂) →
    IsCoprime
      (Ideal.map (algebraMap (NumberField.RingOfIntegers K₁) (NumberField.RingOfIntegers L))
        (differentIdeal ℤ (NumberField.RingOfIntegers K₁)))
      (Ideal.map (algebraMap (NumberField.RingOfIntegers K₂) (NumberField.RingOfIntegers L))
        (differentIdeal ℤ (NumberField.RingOfIntegers K₂)))
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
TensorProduct.toDirectLimit_tmul_of : ∀ {R : Type u_1} [inst : CommSemiring R] {ι : Type u_2} [inst_1 : DecidableEq ι] [inst_2 : Preorder ι]
  {G : ι → Type u_3} [inst_3 : (i : ι) → AddCommMonoid (G i)] [inst_4 : (i : ι) → Module R (G i)]
  (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) {M : Type u_4} [inst_5 : AddCommMonoid M] [inst_6 : Module R M] {i : ι}
  (g : G i) (m : M),
  (TensorProduct.toDirectLimit f M) ((Module.DirectLimit.of R ι G f i) g ⊗ₜ[R] m) =
    (Module.DirectLimit.of R ι (fun x => TensorProduct R (G x) M) (fun i j h => LinearMap.rTensor M (f i j h)) i)
      (g ⊗ₜ[R] m)
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.ofTop_apply : ∀ (E : Type u_5) [inst : SeminormedAddCommGroup E] {R : Type u_12} [inst_1 : Ring R] [inst_2 : Module R E]
  (p : Submodule R E) (hp : p = ⊤) (self : ↥p), (LinearIsometryEquiv.ofTop E p hp) self = ↑self
-- Mathlib.Analysis.SpecialFunctions.CompareExp
/-- If `l : Filter ℂ` is an "exponential comparison filter", then for any complex `a₁`, `a₂` and any
natural `b₁ < b₂`, we have
`(fun z ↦ z ^ a₁ * exp (b₁ * z)) =o[l] (fun z ↦ z ^ a₂ * exp (b₂ * z))`.  -/
Complex.IsExpCmpFilter.isLittleO_pow_mul_exp : ∀ {l : Filter ℂ} {b₁ b₂ : ℝ},
  Complex.IsExpCmpFilter l →
    b₁ < b₂ → ∀ (m n : ℕ), (fun z => z ^ m * Complex.exp (↑b₁ * z)) =o[l] fun z => z ^ n * Complex.exp (↑b₂ * z)
-- Init.Internal.Order.Basic
Lean.Order.admissible_const_true : ∀ {α : Sort u} [inst : Lean.Order.CCPO α], Lean.Order.admissible fun x => True
-- Mathlib.Order.UpperLower.Principal
UpperSet.coe_Ici : ∀ {α : Type u_1} [inst : Preorder α] (a : α), ↑(UpperSet.Ici a) = Set.Ici a
-- Mathlib.Topology.ContinuousMap.CocompactMap
CocompactMap.id_comp : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : CocompactMap α β),
  (CocompactMap.id β).comp f = f
-- Mathlib.Computability.Primrec.Basic
Primrec.fin_succ : ∀ {n : ℕ}, Primrec Fin.succ
-- Mathlib.Algebra.Category.Semigrp.Basic
AddSemigrp.mk : (carrier : Type u) → [str : AddSemigroup carrier] → AddSemigrp
-- Init.Data.Int.Order
Int.instTransLt : Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isLongestMatch_iff_isMatch : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.NoPrefixPatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatch pat pos ↔ String.Slice.Pattern.Model.IsMatch pat pos
-- Mathlib.CategoryTheory.Skeletal
CategoryTheory.fromSkeleton.isEquivalence : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C], (CategoryTheory.fromSkeleton C).IsEquivalence
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.isOpenEmbedding_coe : Topology.IsOpenEmbedding Real.toEReal
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn_append_aux : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] [Std.IsLinearPreorder β] {xs ys : List α}
  {f : α → β} (hxs : xs ≠ []) (hys : ys ≠ []),
  List.minIdxOn f (xs ++ ys) ⋯ = List.combineMinIdxOn✝ f (List.minIdxOn f xs hxs) (List.minIdxOn f ys hys) ⋯ ⋯
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.toContinuousLinearMap_injective : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W}, Function.Injective fun f => f.toContinuousLinearMap
-- Mathlib.Combinatorics.Quiver.Path.Vertices
/-- The end vertex of a path. A path `p : Path a b` has `p.end = b`.  -/
Quiver.Path.end : {V : Type u_1} → [inst : Quiver V] → {a b : V} → Quiver.Path a b → V
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.sub_mem_ker_iff : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M] (f : G →+ M) {x y : G},
  x - y ∈ f.ker ↔ f x = f y
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
MeasureTheory.levyProkhorovDist_triangle : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoEMetricSpace Ω] [OpensMeasurableSpace Ω]
  (μ ν κ : MeasureTheory.Measure Ω) [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [MeasureTheory.IsFiniteMeasure κ],
  MeasureTheory.levyProkhorovDist μ κ ≤ MeasureTheory.levyProkhorovDist μ ν + MeasureTheory.levyProkhorovDist ν κ
-- Mathlib.Analysis.Analytic.Composition
ContinuousMultilinearMap.compAlongComposition_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] [inst_6 : Module 𝕜 G]
  [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
  [inst_10 : IsTopologicalAddGroup E] [inst_11 : ContinuousConstSMul 𝕜 E] [inst_12 : IsTopologicalAddGroup F]
  [inst_13 : ContinuousConstSMul 𝕜 F] {n : ℕ} (p : FormalMultilinearSeries 𝕜 E F) (c : Composition n)
  (f : F [×c.length]→L[𝕜] G) (v : Fin n → E),
  (ContinuousMultilinearMap.compAlongComposition p c f) v = f (p.applyComposition c v)
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.lift_unique : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  {f : M →* P} {g : N →* P} {fg : Monoid.Coprod M N →* P},
  fg.comp Monoid.Coprod.inl = f → fg.comp Monoid.Coprod.inr = g → fg = Monoid.Coprod.lift f g
-- Mathlib.RingTheory.Lasker
/-- **Alias** of `Submodule.isPrimary_decomposition_pairwise_ne_radical`. -/
Ideal.isPrimary_decomposition_pairwise_ne_radical : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {s : Finset (Submodule R M)},
  s.inf id = N →
    (∀ ⦃J : Submodule R M⦄, J ∈ s → J.IsPrimary) →
      ∃ t,
        t.inf id = N ∧
          (∀ ⦃J : Submodule R M⦄, J ∈ t → J.IsPrimary) ∧
            (↑t).Pairwise (Function.onFun (fun x1 x2 => x1 ≠ x2) fun J => (J.colon Set.univ).radical)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- An integrability criterion for the continuous functional calculus.
For a version with stronger assumptions which in practice are often easier to verify, see
`integrableOn_cfc`.  -/
integrableOn_cfc' : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NormedRing A] [inst_3 : StarRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : ContinuousFunctionalCalculus 𝕜 A p] [inst_6 : CompleteSpace A] {s : Set X} (f : X → 𝕜 → 𝕜) (a : A),
  MeasureTheory.IntegrableOn (fun x => ContinuousMap.mkD ((spectrum 𝕜 a).domRestrict (f x)) 0) s μ →
    autoParam (p a) integrableOn_cfc'._auto_1 → MeasureTheory.IntegrableOn (fun x => cfc (f x) a) s μ
-- Mathlib.Data.Seq.Computation
Computation.eq_empty_of_not_terminates : ∀ {α : Type u} {s : Computation α}, ¬s.Terminates → s = Computation.empty α
-- Mathlib.Data.Multiset.NatAntidiagonal
Multiset.Nat.antidiagonal_succ_succ' : ∀ {n : ℕ},
  Multiset.Nat.antidiagonal (n + 2) =
    (0, n + 2) ::ₘ (n + 2, 0) ::ₘ Multiset.map (Prod.map Nat.succ Nat.succ) (Multiset.Nat.antidiagonal n)
-- Mathlib.Algebra.Order.Ring.NNRat
NNRat.instCanonicallyOrderedAdd : CanonicallyOrderedAdd ℚ≥0
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.cyclesIso₀_inv_comp_cyclesMap : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B),
  CategoryTheory.CategoryStruct.comp (groupHomology.cyclesIso₀ A).inv (groupHomology.cyclesMap f φ 0) =
    CategoryTheory.CategoryStruct.comp (Rep.Hom.toModuleCatHom φ) (groupHomology.cyclesIso₀ B).inv
-- Mathlib.RingTheory.Ideal.Maps
/-- If `f : R ≃+* S` is a ring isomorphism and `I : Ideal R`, then `map f.symm (map f I) = I`.  -/
Ideal.map_of_equiv : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal R} (f : R ≃+* S),
  Ideal.map (↑f.symm) (Ideal.map (↑f) I) = I
-- Mathlib.CategoryTheory.Localization.Construction
/-- The functor `(W.Localization ⥤ D) ⥤ (W.FunctorsInverting D)` induced by the
composition with `W.Q : C ⥤ W.Localization`.  -/
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (D : Type uD) →
        [inst_1 : CategoryTheory.Category.{uD', uD} D] →
          CategoryTheory.Functor (CategoryTheory.Functor W.Localization D) (W.FunctorsInverting D)
-- Init.Data.List.Nat.Range
/-- Variant of `mem_zipIdx` specialized at `k = 0`.  -/
List.mem_zipIdx' : ∀ {α : Type u_1} {x : α} {i : ℕ} {xs : List α} (h : (x, i) ∈ xs.zipIdx), i < xs.length ∧ x = xs[i]
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.size_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List (α × β)},
  List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
    (∀ a ∈ t, (List.map Prod.fst l).contains a = false) → (Std.DTreeMap.Const.insertMany t l).size = t.size + l.length
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_comm : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  {α : L₂ ⟶ L₁} {β : L₁ ⟶ L₂},
  CategoryTheory.CategoryStruct.comp β α = CategoryTheory.CategoryStruct.id L₁ →
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.conjugateEquiv adj₁ adj₂) α)
        ((CategoryTheory.conjugateEquiv adj₂ adj₁) β) =
      CategoryTheory.CategoryStruct.id R₁
-- Init.Data.Option.Lemmas
Option.not_comp_isSome : ∀ {α : Type u_1}, (fun x => !x) ∘ Option.isSome = Option.isNone
-- Mathlib.Analysis.Fourier.Convolution
/-- The Fourier transform of the convolution is given by the multiplication of the Fourier transform
of the individual functions.

Version for multiplication.  -/
Real.fourier_mul_convolution_eq : ∀ {R : Type u_2} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : NormedRing R]
  [inst_6 : NormedSpace ℂ R] [inst_7 : IsScalarTower ℂ R R] [inst_8 : SMulCommClass ℂ R R] [CompleteSpace R]
  {f₁ f₂ : E → R},
  MeasureTheory.Integrable f₁ MeasureTheory.volume →
    MeasureTheory.Integrable f₂ MeasureTheory.volume →
      ∀ (ξ : E),
        FourierTransform.fourier (MeasureTheory.convolution f₁ f₂ (ContinuousLinearMap.mul ℂ R) MeasureTheory.volume)
            ξ =
          FourierTransform.fourier f₁ ξ * FourierTransform.fourier f₂ ξ
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
/-- Given `S`-schemes `X` and `Y` such that `Y` is locally of finite type and
`X` is irreducible germ-injective at `x` (e.g. when `X` is integral),
any `S`-morphism `Spec 𝒪ₓ ⟶ Y` spreads out to a partial map from `X` to `Y`.
 -/
AlgebraicGeometry.Scheme.PartialMap.ofFromSpecStalk : {X Y S : AlgebraicGeometry.Scheme} →
  (sX : X ⟶ S) →
    (sY : Y ⟶ S) →
      [IrreducibleSpace ↥X] →
        [AlgebraicGeometry.LocallyOfFiniteType sY] →
          {x : ↥X} →
            [X.IsGermInjectiveAt x] →
              (φ : AlgebraicGeometry.Spec (X.presheaf.stalk x) ⟶ Y) →
                CategoryTheory.CategoryStruct.comp φ sY = CategoryTheory.CategoryStruct.comp (X.fromSpecStalk x) sX →
                  X.PartialMap Y
-- Lean.KeyedDeclsAttribute
/-- Retrieve entries tagged with `[attr key]` or `[builtinAttr key]`.  -/
Lean.KeyedDeclsAttribute.getEntries : {γ : Type} →
  Lean.KeyedDeclsAttribute γ → Lean.Environment → Lean.Name → List (Lean.KeyedDeclsAttribute.AttributeEntry γ)
-- Mathlib.FieldTheory.Differential.Liouville
/-- Transfer an `IsLiouville` instance using an equivalence `K ≃ₐ[F] K'`.
Requires an algebraic `K'` to show that the equivalence commutes with the derivative.
 -/
IsLiouville.equiv : ∀ {F : Type u_1} {K : Type u_2} [inst : Field F] [inst_1 : Field K] [inst_2 : Differential F] [inst_3 : Differential K]
  [inst_4 : Algebra F K] [DifferentialAlgebra F K] [CharZero F] {K' : Type u_3} [inst_7 : Field K']
  [inst_8 : Differential K'] [inst_9 : Algebra F K'] [DifferentialAlgebra F K'] [Algebra.IsAlgebraic F K']
  [inst_12 : IsLiouville F K] (e : K ≃ₐ[F] K'), IsLiouville F K'
-- Mathlib.Data.Finsupp.Defs
Finsupp.mk.congr_simp : ∀ {α : Type u_9} {M : Type u_10} [inst : Zero M] (support support_1 : Finset α) (e_support : support = support_1)
  (toFun toFun_1 : α → M) (e_toFun : toFun = toFun_1) (mem_support_toFun : ∀ (a : α), a ∈ support ↔ toFun a ≠ 0),
  { support := support, toFun := toFun, mem_support_toFun := mem_support_toFun } =
    { support := support_1, toFun := toFun_1, mem_support_toFun := ⋯ }
-- Mathlib.MeasureTheory.Measure.Real
MeasureTheory.measureReal_restrict_apply₀ : ∀ {α : Type u_1} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasureTheory.NullMeasurableSet t (μ.restrict s) → (μ.restrict s).real t = μ.real (t ∩ s)
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleFactorsFinset_eq_list_toFinset : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {σ : Equiv.Perm α} {l : List (Equiv.Perm α)},
  l.Nodup →
    (σ.cycleFactorsFinset = l.toFinset ↔ (∀ f ∈ l, f.IsCycle) ∧ List.Pairwise Equiv.Perm.Disjoint l ∧ l.prod = σ)
-- Mathlib.Algebra.Module.SpanRank
Submodule.spanRank_range_le : ∀ {R : Type u_1} {S : Type u_2} {M N : Type u} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S}
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module S N]
  [inst_6 : RingHomSurjective σ] (f : M →ₛₗ[σ] N), f.range.spanRank ≤ ⊤.spanRank
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.contains'.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.gt with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_2 ()
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.instZeroHom : (G H : AddCommGrpCat) → Zero (G ⟶ H)
-- Init.Data.List.Basic
/-- Returns the index of the first element equal to `a`, or the length of the list if no element is
equal to `a`.

Examples:
 * `["carrot", "potato", "broccoli"].idxOf "carrot" = 0`
 * `["carrot", "potato", "broccoli"].idxOf "broccoli" = 2`
 * `["carrot", "potato", "broccoli"].idxOf "tomato" = 3`
 * `["carrot", "potato", "broccoli"].idxOf "anything else" = 3`
 -/
List.idxOf : {α : Type u} → [BEq α] → α → List α → ℕ
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.HasSubst.eventually_coeff_pow_eq_zero : ∀ {A : Type u_1} [inst : CommRing A] {f : PowerSeries A},
  PowerSeries.HasSubst f → ∀ (n : ℕ), ∀ᶠ (m : ℕ) in Filter.atTop, ∀ n' ≤ n, (PowerSeries.coeff n') (f ^ m) = 0
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.functorMap_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i)
  {S T X Y : C} {πX : X ⟶ S} {πY : Y ⟶ T} (τ : CategoryTheory.Arrow.mk πX ⟶ CategoryTheory.Arrow.mk πY)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πY))
      C]
  [inst_3 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  [inst_4 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πY)
      (CategoryTheory.SmallObject.functorObjLeft f πY)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.functorMap f τ)
      (CategoryTheory.SmallObject.πFunctorObj f πY) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πFunctorObj f πX) (CategoryTheory.Arrow.Hom.right τ)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- In a space with second countable topology, measurable implies ae strongly measurable.  -/
Measurable.aestronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f : α → β} [inst_1 : MeasurableSpace β] [TopologicalSpace.PseudoMetrizableSpace β] [SecondCountableTopology β]
  [OpensMeasurableSpace β], Measurable f → MeasureTheory.AEStronglyMeasurable f μ