mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Simple
CategoryTheory.Functor.simple_of_simple_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [F.PreservesMonomorphisms] [F.PreservesZeroMorphisms] [F.ReflectsIsomorphisms]
  [F.Faithful] (X : C) [CategoryTheory.Simple (F.obj X)], CategoryTheory.Simple X
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.Collector.M : Type → Type
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
/-- If `{ xᵢ }` spans the irrelevant ideal of `A`, then `D₊(xᵢ)` covers `Proj A`.  -/
AlgebraicGeometry.Proj.iSup_basicOpen_eq_top : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {ι : Type u_2} (f : ι → A),
  (HomogeneousIdeal.irrelevant 𝒜).toIdeal ≤ Ideal.span (Set.range f) → ⨆ i, AlgebraicGeometry.Proj.basicOpen 𝒜 (f i) = ⊤
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.exists_isBasis : ∀ {α : Type u_1} (M : Matroid α) (X : Set α), autoParam (X ⊆ M.E) Matroid.exists_isBasis._auto_1 → ∃ I, M.IsBasis I X
-- Mathlib.Data.Opposite
Opposite.op.sizeOf_spec : ∀ {α : Sort u} [inst : SizeOf α] (unop : α), sizeOf (Opposite.op unop) = 1 + sizeOf unop
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- The comparison morphism from the image of a terminal object to the terminal object in the target
category.
This is an isomorphism iff `G` preserves terminal objects, see
`CategoryTheory.Limits.PreservesTerminal.ofIsoComparison`.
 -/
CategoryTheory.Limits.terminalComparison : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          [inst_2 : CategoryTheory.Limits.HasTerminal C] →
            [inst_3 : CategoryTheory.Limits.HasTerminal D] → G.obj (⊤_ C) ⟶ ⊤_ D
-- Mathlib.Algebra.Ring.Rat
Rat.semiring : Semiring ℚ
-- Mathlib.Order.SuccPred.LinearLocallyFinite
/-- **Alias** of `toZ_lt_toZ`. -/
toZ_lt_iff : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 i j : ι}, toZ i0 i < toZ i0 j ↔ i < j
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_fun_sum : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E}
  {ι : Type u_4} {u : Finset ι} {A : ι → E → F},
  (∀ i ∈ u, DifferentiableAt 𝕜 (A i) x) → fderiv 𝕜 (fun y => ∑ i ∈ u, A i y) x = ∑ i ∈ u, fderiv 𝕜 (A i) x
-- Mathlib.Data.Matrix.Block
Matrix.fromBlocks_map : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} {β : Type u_13} (A : Matrix n l α)
  (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (f : α → β),
  (Matrix.fromBlocks A B C D).map f = Matrix.fromBlocks (A.map f) (B.map f) (C.map f) (D.map f)
-- Mathlib.GroupTheory.Torsion
AddCommGroup.comap_torsion_of_injective : ∀ {G : Type u_1} {H : Type u_2} [inst : AddCommGroup G] [inst_1 : AddCommGroup H] {f : G →+ H},
  Function.Injective ⇑f → AddSubgroup.comap f (AddCommGroup.torsion H) = AddCommGroup.torsion G
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.surj : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (z : N), ∃ x, z * f ↑x.2 = f x.1
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.prod_inf_prod : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (p p' : Submodule R M) {M' : Type u_8} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (q₁ q₁' : Submodule R M'),
  p.prod q₁ ⊓ p'.prod q₁' = (p ⊓ p').prod (q₁ ⊓ q₁')
-- Mathlib.RingTheory.Bialgebra.Convolution
AlgHom.instMonoidWithConv : {R : Type u_1} →
  {A : Type u_2} →
    {C : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Semiring C] → [inst_3 : Bialgebra R C] → [inst_4 : Algebra R A] → Monoid (WithConv (C →ₐ[R] A))
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.subsingleton_isBilimit : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} {c : CategoryTheory.Limits.Bicone f},
  Subsingleton c.IsBilimit
-- Mathlib.Tactic.Ring.RingNF
/-- The tactic `ring` evaluates expressions in *commutative* (semi)rings.
This is the conv tactic version, which rewrites a target which is a ring equality to `True`.

See also the `ring` tactic.
 -/
Mathlib.Tactic.RingNF.ringConv : Lean.ParserDescr
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
/-- The intermediate object in the definition of the morphism `toSucc W Z : Z ⟶ succ W Z`.
It is the pushout of the following square:
```lean
∐ D₁.obj₁ ⟶ ∐ D₁.obj₂
   |           |
   v           v
   Z      ⟶   step W Z
```
where the coproduct is taken over all the diagram consisting of a morphism `f : X ⟶ Y`
satisfying `W` and a morphism `X ⟶ Z`. The top map is the coproduct of all of these `f`.
 -/
CategoryTheory.OrthogonalReflection.step : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (Z : C) →
        [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁] →
          [CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂] →
            [CategoryTheory.Limits.HasPushouts C] → C
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.limit_map_limitObjIsoLimitCompEvaluation_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K] [inst_3 : CategoryTheory.Limits.HasLimitsOfShape J C]
  {i j : K} (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) (f : i ⟶ j) {Z : C}
  (h : CategoryTheory.Limits.limit (F.comp ((CategoryTheory.evaluation K C).obj j)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Limits.limit F).map f)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F j).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitObjIsoLimitCompEvaluation F i).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.limMap (F.whiskerLeft ((CategoryTheory.evaluation K C).map f))) h)
-- Mathlib.Combinatorics.Additive.CovBySMul
CovBySMul.subset : ∀ {M : Type u_1} {X : Type u_3} [inst : Monoid M] [inst_1 : MulAction M X] {K : ℝ} {A₁ A₂ B₁ B₂ : Set X},
  A₁ ⊆ A₂ → B₁ ⊆ B₂ → CovBySMul M K A₂ B₁ → CovBySMul M K A₁ B₂
-- Mathlib.Topology.CWComplex.Classical.Graph
Topology.CWComplex.OneSkeletonGraph.exists_isLoopAt_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {C : Set X} [inst_1 : Topology.CWComplex C]
  (e : Topology.RelCWComplex.cell C 1),
  (∃ x, (Topology.CWComplex.OneSkeletonGraph C).IsLoopAt e x) ↔
    ∃ x, Topology.RelCWComplex.cellFrontier 1 e = Topology.RelCWComplex.closedCell 0 x
-- Std.Data.TreeSet.Basic
/-- Transforms the tree set into an array of elements in ascending order.  -/
Std.TreeSet.toArray : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet α cmp → Array α
-- Mathlib.FieldTheory.Perfect
PerfectField.mk : ∀ {K : Type u_1} [inst : Field K], (∀ {f : Polynomial K}, Irreducible f → f.Separable) → PerfectField K
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.condition : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst f g) f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd f g) g
-- Mathlib.LinearAlgebra.Determinant
LinearMap.coe_det : ∀ {M : Type u_2} [inst : AddCommGroup M] {A : Type u_5} [inst_1 : CommRing A] [inst_2 : Module A M]
  [inst_3 : DecidableEq M],
  ⇑LinearMap.det = ⇑(if H : ∃ s, Nonempty (Module.Basis (↥s) A M) then LinearMap.detAux (Trunc.mk ⋯.some) else 1)
-- Mathlib.Algebra.MonoidAlgebra.Support
AddMonoidAlgebra.support_coeff_mul_single_eq_image : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Add G] [inst_2 : DecidableEq G] (f : AddMonoidAlgebra k G)
  {r : k},
  (∀ (y : k), y * r = 0 ↔ y = 0) →
    ∀ {x : G},
      IsAddRightRegular x →
        (f * AddMonoidAlgebra.single x r).coeff.support = Finset.image (fun x_1 => x_1 + x) f.coeff.support
-- Mathlib.Order.WithBot
WithTop.decidableEq : {α : Type u_1} → [DecidableEq α] → DecidableEq (WithTop α)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ext : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, (∀ (n : ℕ), p.coeff n = q.coeff n) → p = q
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.leftHomologyFunctor_linear : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : CategoryTheory.Limits.HasKernels C] [inst_5 : CategoryTheory.Limits.HasCokernels C],
  CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.leftHomologyFunctor C)
-- Aesop.RuleSet
/-- FVars that were explicitly added as simp rules.
 -/
Aesop.LocalRuleSet.localNormSimpRules : Aesop.LocalRuleSet → Array Aesop.LocalNormSimpRule
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- The (limit) kernel fork given by the composition
`Z ⟶ I.cocomplex.X 0 ⟶ I.cocomplex.X 1` when `I : InjectiveResolution Z`.  -/
CategoryTheory.InjectiveResolution.kernelFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} → (I : CategoryTheory.InjectiveResolution Z) → CategoryTheory.Limits.KernelFork (I.cocomplex.d 0 1)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanModuleHierarchyImportsParams : Lean.FromJson Lean.Lsp.LeanModuleHierarchyImportsParams
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α} {v : β k},
  (t.insert k v).minKey! = t.minKey?.elim k fun k' => if (cmp k k').isLE = true then k else k'
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
Tactic.ComputeAsymptotics.Seq.instCompleteSpaceSeq : ∀ {α : Type u_1}, CompleteSpace (Stream'.Seq α)
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.coe_injective : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)},
  Function.Injective fun f x => f x
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.isoMk_hom_left : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (l : f.left ≅ g.left)
  (r : f.right ≅ g.right)
  (h :
    autoParam (CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom)
      CategoryTheory.Arrow.isoMk._auto_1),
  (CategoryTheory.Arrow.isoMk l r h).hom.left = l.hom
-- Mathlib.Order.BoundedOrder.Basic
isMax_iff_eq_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, IsMax a ↔ a = ⊤
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_obj₂ : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C),
  ((t.triangleLEGE a b h).obj j).obj₂ = j
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Fan.mk_pt : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → P ⟶ f b),
  (CategoryTheory.Limits.Fan.mk P p).pt = P
-- Mathlib.Data.Num.ZNum
ZNum.cast_to_int : ∀ {α : Type u_1} [inst : AddGroupWithOne α] (n : ZNum), ↑↑n = ↑n
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKey!_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.maxKey! ∈ t
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.equalizer.lift_ι : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g] {W : C} (k : W ⟶ X)
  (h : CategoryTheory.CategoryStruct.comp k f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.equalizer.lift k h)
      (CategoryTheory.Limits.equalizer.ι f g) =
    k
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.applyCell.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} {δ : Type u_4} [inst : Ord α] (k : α)
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      ((c : Std.DTreeMap.Internal.Cell α β (compare k)) →
          (Std.DTreeMap.Internal.Impl.contains' (compare k) l = true → c.contains = true) → δ) →
        Sort u_3)
  (size : ℕ) (k' : α) (v' : β k') (l r : Std.DTreeMap.Internal.Impl α β)
  (f :
    (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
      (Std.DTreeMap.Internal.Impl.contains' (compare k) (Std.DTreeMap.Internal.Impl.inner size k' v' l r) = true →
          c.contains = true) →
        δ)
  (h_1 :
    (f :
        (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
          (Std.DTreeMap.Internal.Impl.contains' (compare k) Std.DTreeMap.Internal.Impl.leaf = true →
              c.contains = true) →
            δ) →
      motive Std.DTreeMap.Internal.Impl.leaf f)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (f :
                (c : Std.DTreeMap.Internal.Cell α β (compare k)) →
                  (Std.DTreeMap.Internal.Impl.contains' (compare k) (Std.DTreeMap.Internal.Impl.inner size k' v' l r) =
                        true →
                      c.contains = true) →
                    δ) →
              motive (Std.DTreeMap.Internal.Impl.inner size k' v' l r) f),
  (match Std.DTreeMap.Internal.Impl.inner size k' v' l r, f with
    | Std.DTreeMap.Internal.Impl.leaf, f => h_1 f
    | Std.DTreeMap.Internal.Impl.inner size k' v' l r, f => h_2 size k' v' l r f) =
    h_2 size k' v' l r f
-- Mathlib.Data.Ineq
Mathlib.Ineq.eq : Mathlib.Ineq
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
WeierstrassCurve.integralModel.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra R K]
  (W W_1 : WeierstrassCurve K) (e_W : W = W_1) [hW : WeierstrassCurve.IsIntegral R W],
  WeierstrassCurve.integralModel R W = WeierstrassCurve.integralModel R W_1
-- Lean.Meta.InferType
/-- Returns `true` iff `type` is `Sort _` or `As → Sort _`.
 -/
Lean.Meta.isTypeFormerType : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Data.Set.Sigma
Set.sigma_mono : ∀ {ι : Type u_1} {α : ι → Type u_3} {s₁ s₂ : Set ι} {t₁ t₂ : (i : ι) → Set (α i)},
  s₁ ⊆ s₂ → (∀ (i : ι), t₁ i ⊆ t₂ i) → s₁.sigma t₁ ⊆ s₂.sigma t₂
-- Mathlib.RepresentationTheory.Rep.Basic
Representation.IntertwiningMap.id.eq_1 : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module A V] (ρ : Representation A G V),
  Representation.IntertwiningMap.id ρ = { toLinearMap := LinearMap.id, isIntertwining' := ⋯ }
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.coind₁ResMap_comp_coind₁Map_restrict : ∀ {R : Type u_1} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : TopologicalSpace V] [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] [inst_5 : AddCommGroup W]
  [inst_6 : TopologicalSpace W] [inst_7 : IsTopologicalAddGroup W] [inst_8 : Module R W] [inst_9 : AddCommGroup U]
  [inst_10 : Module R U] [inst_11 : TopologicalSpace U] [inst_12 : IsTopologicalAddGroup U] {G : Type u_7}
  {H : Type u_8} [inst_13 : Group G] [inst_14 : TopologicalSpace G] [inst_15 : TopologicalSpace R]
  [inst_16 : ContinuousSMul R V] [inst_17 : ContinuousSMul R W] [inst_18 : Group H] [inst_19 : TopologicalSpace H]
  {π : ContRepresentation R G V} [inst_20 : IsTopologicalGroup G] [inst_21 : IsTopologicalGroup H]
  [inst_22 : ContinuousSMul R U] {π' : ContRepresentation R H W} (φ : H →ₜ* G) {ρ : ContRepresentation R G U}
  (g : ContIntertwiningMap ρ π) (f : ContIntertwiningMap (π.restrict ↑φ) π'),
  (ContRepresentation.coind₁ResMap φ f).comp (ContIntertwiningMap.restrict (↑φ) (ContRepresentation.coind₁Map g)) =
    ContRepresentation.coind₁ResMap φ (f.comp (ContIntertwiningMap.restrict (↑φ) g))
-- Mathlib.Data.Fintype.Quotient
_private.Mathlib.Data.Fintype.Quotient.0.Quotient.listChoice.match_3.eq_1 : ∀ {ι : Type u_1} {α : ι → Sort u_2} {S : (i : ι) → Setoid (α i)}
  (motive : (l : List ι) → ((i : ι) → i ∈ l → Quotient (S i)) → Sort u_3) (q : (i : ι) → i ∈ [] → Quotient (S i))
  (h_1 : (q : (i : ι) → i ∈ [] → Quotient (S i)) → motive [] q)
  (h_2 : (i : ι) → (tail : List ι) → (q : (i_1 : ι) → i_1 ∈ i :: tail → Quotient (S i_1)) → motive (i :: tail) q),
  (match [], q with
    | [], q => h_1 q
    | i :: tail, q => h_2 i tail q) =
    h_1 q
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- If `V` is a preadditive category, then `RightFreyd V` is the category of arrows in `V`,
with morphisms identified when they are right homotopic.  -/
CategoryTheory.Preadditive.RightFreyd : (V : Type u_1) → [inst : CategoryTheory.Category.{v_1, u_1} V] → [CategoryTheory.Preadditive V] → Type (max u_1 v_1)
-- Mathlib.Order.WithBot
_private.Mathlib.Order.WithBot.0.WithBot.decidableLT.match_1.eq_3 : ∀ {α : Type u_1} (motive : WithBot α → WithBot α → Sort u_2) (a b : α) (h_1 : (x : WithBot α) → motive x none)
  (h_2 : (a : α) → motive none (some a)) (h_3 : (a b : α) → motive (some a) (some b)),
  (match some a, some b with
    | x, none => h_1 x
    | none, some a => h_2 a
    | some a, some b => h_3 a b) =
    h_3 a b
-- Mathlib.Topology.EMetricSpace.Weak
Option.edist_triangle' : ∀ {α : Type u} [inst : TopologicalSpace α] (m : WeakPseudoEMetricSpace α) (x y z : Option α),
  edist x z ≤ edist x y + edist y z
-- Mathlib.CategoryTheory.Monoidal.Closed.Basic
CategoryTheory.MonoidalClosed.uncurry_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {A X Y : C}
  [inst_2 : CategoryTheory.Closed A], Function.Injective CategoryTheory.MonoidalClosed.uncurry
-- Mathlib.Order.Preorder.Finite
Finset.exists_le_maximal : ∀ {α : Type u_2} [inst : Preorder α] {a : α} (s : Finset α), a ∈ s → ∃ b, a ≤ b ∧ Maximal (fun x => x ∈ s) b
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.evalEval_CC : ∀ {R : Type u_1} [inst : Semiring R] (x y p : R), Polynomial.evalEval x y (Polynomial.CC p) = p
-- Std.Time.Zoned.Database.TzIf
Std.Time.TimeZone.TZif.instInhabitedTZif.default : Std.Time.TimeZone.TZif.TZif
-- Init.Data.Range.Polymorphic.PRange
Std.Rco.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (lower upper : α), (sizeOf lower...upper) = 1 + sizeOf lower + sizeOf upper
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeAction.mk.injEq : ∀ (toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams) (toPartialResultParams : Lean.Lsp.PartialResultParams)
  (title : String) (kind? : Option Lean.Lsp.CodeActionKind) (diagnostics? : Option (Array Lean.Lsp.Diagnostic))
  (isPreferred? : Option Bool) (disabled? : Option Lean.Lsp.CodeActionDisabled) (edit? : Option Lean.Lsp.WorkspaceEdit)
  (command? : Option Lean.Lsp.Command) (data? : Option Lean.Json)
  (toWorkDoneProgressParams_1 : Lean.Lsp.WorkDoneProgressParams)
  (toPartialResultParams_1 : Lean.Lsp.PartialResultParams) (title_1 : String) (kind?_1 : Option Lean.Lsp.CodeActionKind)
  (diagnostics?_1 : Option (Array Lean.Lsp.Diagnostic)) (isPreferred?_1 : Option Bool)
  (disabled?_1 : Option Lean.Lsp.CodeActionDisabled) (edit?_1 : Option Lean.Lsp.WorkspaceEdit)
  (command?_1 : Option Lean.Lsp.Command) (data?_1 : Option Lean.Json),
  ({ toWorkDoneProgressParams := toWorkDoneProgressParams, toPartialResultParams := toPartialResultParams,
        title := title, kind? := kind?, diagnostics? := diagnostics?, isPreferred? := isPreferred?,
        disabled? := disabled?, edit? := edit?, command? := command?, data? := data? } =
      { toWorkDoneProgressParams := toWorkDoneProgressParams_1, toPartialResultParams := toPartialResultParams_1,
        title := title_1, kind? := kind?_1, diagnostics? := diagnostics?_1, isPreferred? := isPreferred?_1,
        disabled? := disabled?_1, edit? := edit?_1, command? := command?_1, data? := data?_1 }) =
    (toWorkDoneProgressParams = toWorkDoneProgressParams_1 ∧
      toPartialResultParams = toPartialResultParams_1 ∧
        title = title_1 ∧
          kind? = kind?_1 ∧
            diagnostics? = diagnostics?_1 ∧
              isPreferred? = isPreferred?_1 ∧
                disabled? = disabled?_1 ∧ edit? = edit?_1 ∧ command? = command?_1 ∧ data? = data?_1)
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.mul_coe_eq_bind : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {b : α},
  b ≠ 0 → ∀ (a : WithTop α), a * ↑b = Option.bind a fun a => some (a * b)
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.State.uPending : Lean.Meta.Sym.UnifyM.State✝ → Array (Lean.Level × Lean.Level)
-- Mathlib.Data.Finsupp.AList
AList.lookupFinsupp_eq_zero_iff : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : DecidableEq α] {l : AList fun _x => M} {a : α},
  l.lookupFinsupp a = 0 ↔ a ∉ l ∨ 0 ∈ AList.lookup a l
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_subset_iff' : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {f : ι → M} {s : Set ι}, Function.mulSupport f ⊆ s ↔ ∀ x ∉ s, f x = 1
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.χ.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (self : CategoryTheory.Subobject.Classifier C) {U X : C}
  (m m_1 : U ⟶ X) (e_m : m = m_1) [inst_1 : CategoryTheory.Mono m], self.χ m = self.χ m_1
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.epsilon_zero_eq_nfp : Ordinal.epsilon 0 = Ordinal.nfp (fun a => Ordinal.omega0 ^ a) 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTriangleLTGE_obj_obj_mor₂ : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt) (j : C),
  ((t.eTriangleLTGE.obj i).obj j).mor₂ = (t.eTruncGEπ i).app j
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
Lean.Meta.RefinedDiscrTree.Key.opaque.sizeOf_spec : sizeOf Lean.Meta.RefinedDiscrTree.Key.opaque = 1
-- Mathlib.Data.Bool.Basic
Bool.bool_eq_false : ∀ {b : Bool}, ¬b = true → b = false
-- Mathlib.Analysis.Fourier.Notation
/-- The inverse Fourier transform as a continuous linear map.  -/
FourierTransform.fourierInvCLM : (R : Type u_2) →
  (E : Type u_3) →
    {F : Type u_4} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : AddCommMonoid F] →
            [inst_3 : Module R E] →
              [inst_4 : Module R F] →
                [inst_5 : FourierTransformInv E F] →
                  [FourierInvAdd E F] →
                    [FourierInvSMul R E F] →
                      [inst_8 : TopologicalSpace E] →
                        [inst_9 : TopologicalSpace F] → [ContinuousFourierInv E F] → E →L[R] F