mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.brecOn_1.go : {motive_1 : Mathlib.Tactic.Translate.ArgReorder → Sort u} →
  {motive_2 : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u} →
    {motive_3 : List (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u} →
      {motive_4 : ℕ × Mathlib.Tactic.Translate.ArgReorder → Sort u} →
        (t : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)) →
          ((t : Mathlib.Tactic.Translate.ArgReorder) → t.below → motive_1 t) →
            ((t : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)) →
                Mathlib.Tactic.Translate.ArgReorder.below_1 t → motive_2 t) →
              ((t : List (ℕ × Mathlib.Tactic.Translate.ArgReorder)) →
                  Mathlib.Tactic.Translate.ArgReorder.below_2 t → motive_3 t) →
                ((t : ℕ × Mathlib.Tactic.Translate.ArgReorder) →
                    Mathlib.Tactic.Translate.ArgReorder.below_3 t → motive_4 t) →
                  motive_2 t ×' Mathlib.Tactic.Translate.ArgReorder.below_1 t
-- Mathlib.NumberTheory.Chebyshev
Nat.lcmUpto_pos : ∀ (n : ℕ), 0 < n.lcmUpto
-- Mathlib.Algebra.Category.Grp.EquivalenceGroupAddGroup
AddCommGrpCat.toCommGrp_obj_coe : ∀ (X : AddCommGrpCat), ↑(AddCommGrpCat.toCommGrp.obj X) = Multiplicative ↑X
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstr.mk.injEq : ∀ (d : ℤ) (p : Int.Internal.Linear.Poly) (h : Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof) (d_1 : ℤ)
  (p_1 : Int.Internal.Linear.Poly) (h_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof),
  ({ d := d, p := p, h := h } = { d := d_1, p := p_1, h := h_1 }) = (d = d_1 ∧ p = p_1 ∧ h = h_1)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.instIsIsoHomOfMapForget : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} (f : A ⟶ B) [e : CategoryTheory.IsIso ((CategoryTheory.Mon.forget C).map f)],
  CategoryTheory.IsIso f.hom
-- Mathlib.Probability.Kernel.Deterministic
ProbabilityTheory.Kernel.instIsZeroOneMeasureCoeMeasureOfIsFiniteKernelOfIsDeterministic : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [ProbabilityTheory.IsFiniteKernel κ] [ProbabilityTheory.IsDeterministic κ] (a : α),
  MeasureTheory.IsZeroOneMeasure (κ a)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Iic_mul_bij : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  Set.BijOn (fun x => x * a) (Set.Iic b) (Set.Iic (b * a))
-- Mathlib.Topology.OpenPartialHomeomorph.Constructions
/-- The restriction of an open partial homeomorphism `e` to an open subset `s` of the domain type
produces an open partial homeomorphism whose domain is the subtype `s`.  -/
OpenPartialHomeomorph.subtypeRestr : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] →
        OpenPartialHomeomorph X Y → {s : TopologicalSpace.Opens X} → Nonempty ↥s → OpenPartialHomeomorph (↥s) Y
-- Mathlib.Data.Nat.Squarefree
_private.Mathlib.Data.Nat.Squarefree.0.Nat.MinSqFacProp.match_1.eq_2 : ∀ (motive : Option ℕ → Sort u_1) (d : ℕ) (h_1 : Unit → motive none) (h_2 : (d : ℕ) → motive (some d)),
  (match some d with
    | none => h_1 ()
    | some d => h_2 d) =
    h_2 d
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.Order.LiminfLimsup
Filter.limsInf_top : ∀ {α : Type u_1} [inst : CompleteLattice α], ⊤.limsInf = ⊥
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.compl_neg : ∀ {α : Type u_2} [inst : Neg α] {s : Set α}, -sᶜ = (-s)ᶜ
-- Mathlib.Topology.UniformSpace.Path
/-- Given a path `γ`, it extension to the real line `γ.extend : C(ℝ, X)`
is a uniformly continuous function.  -/
Path.uniformContinuous_extend : ∀ {X : Type u_1} [inst : UniformSpace X] {x y : X} (γ : Path x y), UniformContinuous ⇑γ.extend
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverWsWith : Array Lean.Syntax → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Equivalence
/-- The counit of an equivalence of categories.  -/
CategoryTheory.Equivalence.counit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (e : C ≌ D) → e.inverse.comp e.functor ⟶ CategoryTheory.Functor.id D
-- Mathlib.Data.Multiset.Filter
/-- Mapping a multiset through a predicate and counting the `True`s yields the cardinality of the set
filtered by the predicate. Note that this uses the notion of a multiset of `Prop`s - due to the
decidability requirements of `count`, the decidability instance on the LHS is different from the
RHS. In particular, the decidability instance on the left leaks `Classical.decEq`.
See [here](https://github.com/leanprover-community/mathlib/pull/11306#discussion_r782286812)
for more discussion.
 -/
Multiset.map_count_True_eq_filter_card : ∀ {α : Type u_1} (s : Multiset α) (p : α → Prop) [inst : DecidablePred p],
  Multiset.count True (Multiset.map p s) = (Multiset.filter p s).card
-- Mathlib.NumberTheory.Cyclotomic.Discriminant
/-- If `p` is a prime and `IsCyclotomicExtension {p ^ k} K L`, then the discriminant of
`hζ.powerBasis K` is `(-1) ^ ((p ^ k).totient / 2) * p ^ (p ^ (k - 1) * ((p - 1) * k - 1))`
if `Irreducible (cyclotomic (p ^ k) K))`. Beware that in the cases `p ^ k = 1` and `p ^ k = 2`
the formula uses `1 / 2 = 0` and `0 - 1 = 0`. It is useful only to have a uniform result.
See also `IsCyclotomicExtension.discr_prime_pow_eq_unit_mul_pow`.  -/
IsCyclotomicExtension.discr_prime_pow : ∀ {p k : ℕ} {K : Type u} {L : Type v} {ζ : L} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [hcycl : IsCyclotomicExtension {p ^ k} K L] [hp : Fact (Nat.Prime p)] (hζ : IsPrimitiveRoot ζ (p ^ k)),
  Irreducible (Polynomial.cyclotomic (p ^ k) K) →
    Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
      (-1) ^ ((p ^ k).totient / 2) * ↑p ^ (p ^ (k - 1) * ((p - 1) * k - 1))
-- Init.Data.Iterators.Combinators.Monadic.Append
Std.Iterators.Types.Append.fst : {α₁ α₂ : Type w} →
  {m : Type w → Type w'} → {β : Type w} → Std.IterM m β → Std.IterM m β → Std.Iterators.Types.Append α₁ α₂ m β
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.mem_inf : ∀ {μ ν : YoungDiagram} {x : ℕ × ℕ}, x ∈ μ ⊓ ν ↔ x ∈ μ ∧ x ∈ ν
-- Mathlib.Algebra.Module.Bimodule
Subbimodule.smul_mem : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {M : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring A] [inst_4 : Semiring B] [inst_5 : Module A M] [inst_6 : Module B M]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M]
  [inst_11 : SMulCommClass A B M] (p : Submodule (TensorProduct R A B) M) (a : A) {m : M}, m ∈ p → a • m ∈ p
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.retractClosure_retractClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C),
  P.retractClosure.retractClosure = P.retractClosure
-- Mathlib.Topology.OpenPartialHomeomorph.Defs
OpenPartialHomeomorph.replacePartialEquiv_eq_self : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (e' : PartialEquiv X Y) (h : e.toPartialEquiv = e'), e.replacePartialEquiv e' h = e
-- Mathlib.Algebra.Divisibility.Basic
/-- Transitivity of `|` for use in `calc` blocks.  -/
instIsTransDvd : ∀ {α : Type u_1} [inst : Semigroup α], IsTrans α Dvd.dvd
-- Mathlib.Data.EReal.Inv
EReal.div_lt_div_right_of_pos : ∀ {a b c : EReal}, 0 < c → c ≠ ⊤ → a < b → a / c < b / c
-- Init.Data.Array.Range
Array.getElem?_zipIdx : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ}, (xs.zipIdx i)[j]? = Option.map (fun a => (a, i + j)) xs[j]?
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.ZPow.eq_1 : ∀ {α : Type u_2} [inst : One α] [inst_1 : Mul α] [inst_2 : Inv α], Set.ZPow = { pow := fun s n => zpowRec npowRec n s }
-- Init.System.IO
instMonadEIO : {ε : Type} → Monad (EIO ε)
-- Init.Data.Slice.List.Lemmas
ListSlice.size_mkSlice_ric : ∀ {α : Type u_1} {xs : ListSlice α} {hi : ℕ},
  Std.Slice.size (Std.Ric.Sliceable.mkSlice xs *...=hi) = min (hi + 1) (Std.Slice.size xs)
-- Mathlib.Algebra.Ring.SumsOfSquares
/-- In an additive monoid with multiplication `R`, the submonoid generated by the squares is the set of
sums of squares in `R`.
 -/
AddSubmonoid.closure_isSquare : ∀ {R : Type u_1} [inst : AddMonoid R] [inst_1 : Mul R], AddSubmonoid.closure {x | IsSquare x} = AddSubmonoid.sumSq R
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- Composition of equivalences  -/
RootPairing.Equiv.comp : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  {ι₁ : Type u_8} →
                    {M₁ : Type u_9} →
                      {N₁ : Type u_10} →
                        {ι₂ : Type u_11} →
                          {M₂ : Type u_12} →
                            {N₂ : Type u_13} →
                              [inst_5 : AddCommGroup M₁] →
                                [inst_6 : Module R M₁] →
                                  [inst_7 : AddCommGroup N₁] →
                                    [inst_8 : Module R N₁] →
                                      [inst_9 : AddCommGroup M₂] →
                                        [inst_10 : Module R M₂] →
                                          [inst_11 : AddCommGroup N₂] →
                                            [inst_12 : Module R N₂] →
                                              {P : RootPairing ι R M N} →
                                                {P₁ : RootPairing ι₁ R M₁ N₁} →
                                                  {P₂ : RootPairing ι₂ R M₂ N₂} → P₁.Equiv P₂ → P.Equiv P₁ → P.Equiv P₂
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- If `1 < k` then `(∑ i ∈ range k, ζ ^ i) = 0`.  -/
IsPrimitiveRoot.geom_sum_eq_zero : ∀ {R : Type u_4} {k : ℕ} [inst : CommRing R] [IsDomain R] {ζ : R},
  IsPrimitiveRoot ζ k → 1 < k → ∑ i ∈ Finset.range k, ζ ^ i = 0
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getD_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α] {l : List ((a : α) × β a)}
  {k k' : α} (k_beq : (k == k') = true) {v : β k} {fallback : β k'},
  List.Pairwise (fun a b => (a.fst == b.fst) = false) l →
    ⟨k, v⟩ ∈ l → (↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany l)).getD k' fallback = cast ⋯ v
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.coe_prodAssoc : ∀ (R : Type u_1) (E : Type u_5) (E₂ : Type u_6) (E₃ : Type u_7) [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : SeminormedAddCommGroup E₂] [inst_3 : SeminormedAddCommGroup E₃] [inst_4 : Module R E] [inst_5 : Module R E₂]
  [inst_6 : Module R E₃], ⇑(LinearIsometryEquiv.prodAssoc R E E₂ E₃) = ⇑(Equiv.prodAssoc E E₂ E₃)
-- Mathlib.NumberTheory.LocalField.Basic
IsNonarchimedeanLocalField.instIsDiscrete : ∀ (K : Type u_1) [inst : Field K] [inst_1 : ValuativeRel K] [inst_2 : TopologicalSpace K]
  [IsNonarchimedeanLocalField K], ValuativeRel.IsDiscrete K
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_imp : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {l : ℕ} {φ ψ : L.BoundedFormula α l}
  {v : α → M} {xs : Fin l → M}, (φ.imp ψ).Realize v xs ↔ φ.Realize v xs → ψ.Realize v xs
-- Init.Notation
/-- `#discr_tree_key  t` prints the discrimination tree keys for a term `t` (or, if it is a single identifier, the type of that constant).
It uses the default configuration for generating keys.

For example,
```
#discr_tree_key (∀ {a n : Nat}, bar a (OfNat.ofNat n))
-- bar _ (@OfNat.ofNat Nat _ _)

#discr_tree_simp_key Nat.add_assoc
-- @HAdd.hAdd Nat Nat Nat _ (@HAdd.hAdd Nat Nat Nat _ _ _) _
```

`#discr_tree_simp_key` is similar to `#discr_tree_key`, but treats the underlying type
as one of a simp lemma, i.e. transforms it into an equality and produces the key of the
left-hand side.
 -/
Lean.Parser.discrTreeSimpKeyCmd : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.instInhabited : Inhabited SSet
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mod
CategoryTheory.Hom.instSMulHom.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.MonObj M] {X : C} [inst_3 : CategoryTheory.ModObj M X] (Y : C),
  CategoryTheory.Hom.instSMulHom Y =
    {
      smul := fun m x =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift m x)
          CategoryTheory.ModObj.smul }
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_mul_X : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m : σ →₀ ℕ) (s : σ) (p : MvPolynomial σ R),
  MvPolynomial.coeff (m + fun₀ | s => 1) (p * MvPolynomial.X s) = MvPolynomial.coeff m p
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_toReal_zero_iff : ∀ {ι : Type u_4} {fi : Filter ι} {f : ι → ENNReal},
  autoParam (∀ (i : ι), f i ≠ ⊤) ENNReal.tendsto_toReal_zero_iff._auto_1 →
    (Filter.Tendsto (fun n => (f n).toReal) fi (nhds 0) ↔ Filter.Tendsto f fi (nhds 0))
-- Init.Data.Range.Polymorphic.IntLemmas
Int.map_add_toList_rco' : ∀ {m n k : ℤ}, List.map (fun x => k + x) (m...n).toList = ((k + m)...k + n).toList
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.mk : {α : Type u} → {β : Type v} → (Std.DHashMap.Raw α fun x => β) → Std.HashMap.Raw α β
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.toCLM_apply_single : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Fintype m] [inst_1 : NonUnitalCStarAlgebra A]
  [inst_2 : DecidableEq m] {M : CStarMatrix m n A} {i : m} (a : A),
  (CStarMatrix.toCLM M) ((WithCStarModule.equiv A (m → A)).symm (Pi.single i a)) =
    (WithCStarModule.equiv A (n → A)).symm fun j => a * M i j
-- Mathlib.Data.Seq.Computation
Computation.LiftRelAux.swap : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (a : α ⊕ Computation α)
  (b : β ⊕ Computation β),
  Computation.LiftRelAux (Function.swap R) (Function.swap C) b a = Computation.LiftRelAux R C a b
-- Batteries.Lean.EStateM
EStateM.run'_getModify : ∀ {σ ε : Type u_1} (f : σ → σ) (s : σ), (getModify f).run' s = some s
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Martingale.supermartingale : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E] [inst_4 : Preorder E],
  MeasureTheory.Martingale f ℱ μ → MeasureTheory.Supermartingale f ℱ μ
-- Lean.Meta.ArgsPacker
/-- Given type `A ⊕' B ⊕' … ⊕' D`, return `[A, B, …, D]`  -/
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Mutual.unpackType : ℕ → Lean.Expr → Lean.MetaM (List Lean.Expr)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Final
/-- A functor `L : A ⥤ T` is final if there is a final functor `R : B ⥤ T` such that for all
`b : B`, the canonical functor `CostructuredArrow L (R.obj b) ⥤ Over (R.obj b)` is final.  -/
CategoryTheory.Functor.final_of_final_costructuredArrowToOver : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [R.Final]
  [hB : ∀ (b : B), (CategoryTheory.CostructuredArrow.toOver L (R.obj b)).Final], L.Final
-- Mathlib.Order.SuccPred.Archimedean
monotone_of_pred_le : ∀ {α : Type u_3} {β : Type u_4} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : PredOrder α]
  [IsPredArchimedean α] {f : α → β}, (∀ (a : α), ¬IsMin a → f (Order.pred a) ≤ f a) → Monotone f
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Polarization identity: The imaginary part of the inner product, in terms of the norm.  -/
im_inner_eq_norm_sub_i_smul_mul_self_sub_norm_add_i_smul_mul_self_div_four : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E),
  RCLike.im (inner 𝕜 x y) = (‖x - RCLike.I • y‖ * ‖x - RCLike.I • y‖ - ‖x + RCLike.I • y‖ * ‖x + RCLike.I • y‖) / 4
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_C_mul_X_pow_le : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (a : R), (Polynomial.C a * Polynomial.X ^ n).degree ≤ ↑n
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.contains_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (Std.ExtDHashMap.Const.alter m k f).contains k' =
    if (k == k') = true then (f (Std.ExtDHashMap.Const.get? m k)).isSome else m.contains k'
-- Lean.Meta.WHNF
Lean.Meta.whnfImp : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Analysis.Distribution.TemperedDistribution
TemperedDistribution.instFourierPair : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E]
  [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E] [inst_5 : AddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  [inst_9 : ContinuousConstSMul ℂ F], FourierPair (TemperedDistribution E F) (TemperedDistribution E F)
-- Mathlib.LinearAlgebra.TensorProduct.Tower
TensorProduct.AlgebraTensorModule.assoc_symm_tmul : ∀ (R : Type uR) (A : Type uA) (B : Type uB) {M : Type uM} {P : Type uP} {Q : Type uQ} [inst : CommSemiring R]
  [inst_1 : CommSemiring A] [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B]
  [inst_5 : AddCommMonoid M] [inst_6 : Module R M] [inst_7 : Module A M] [inst_8 : Module B M]
  [inst_9 : IsScalarTower R A M] [inst_10 : IsScalarTower R B M] [inst_11 : SMulCommClass A B M]
  [inst_12 : AddCommMonoid P] [inst_13 : Module A P] [inst_14 : AddCommMonoid Q] [inst_15 : Module R Q]
  [inst_16 : Module R P] [inst_17 : IsScalarTower R A P] [inst_18 : Algebra A B] [inst_19 : IsScalarTower A B M] (m : M)
  (p : P) (q : Q), (TensorProduct.AlgebraTensorModule.assoc R A B M P Q).symm (m ⊗ₜ[A] (p ⊗ₜ[R] q)) = m ⊗ₜ[A] p ⊗ₜ[R] q
-- Lean.Elab.Do.Basic
/-- Register the given names as that of `mut` variables.  -/
Lean.Elab.Do.declareMutVars : {α : Type} → Array Lean.Ident → Lean.Elab.Do.DoElabM α → Lean.Elab.Do.DoElabM α
-- Mathlib.Data.Finset.Basic
Finset.sdiff_insert : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (x : α), s \ insert x t = (s \ t).erase x
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel_ι : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : CategoryTheory.Limits.HasCokernel S.f]
  [inst_3 : CategoryTheory.Limits.HasKernel (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)],
  (CategoryTheory.ShortComplex.RightHomologyData.ofHasCokernelOfHasKernel S).ι =
    CategoryTheory.Limits.kernel.ι (CategoryTheory.Limits.cokernel.desc S.f S.g ⋯)
-- Mathlib.RingTheory.Valuation.Basic
Valuation.toValuation_ofValuation : ∀ {R : Type u_3} {Γ₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  (v : AddValuation R (Additive Γ₀)ᵒᵈ), Valuation.toAddValuation (Valuation.ofAddValuation v) = v
-- Init.Data.Int.Lemmas
Int.neg_eq_of_add_eq_zero : ∀ {a b : ℤ}, a + b = 0 → -a = b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constModify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (k : α) (f : β → β), (Std.DTreeMap.Const.modify t₁ k f).Equiv (Std.DTreeMap.Const.modify t₂ k f)
-- Mathlib.Data.FunLike.Equiv
EquivLike.toEmbeddingLike : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [inst : EquivLike E α β], EmbeddingLike E α β
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.pairingIn_threeShortAddLong_left : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.EmbeddedG2] [CharZero R] (i : ι),
  P.pairingIn ℤ (RootPairing.EmbeddedG2.threeShortAddLong P) i =
    3 * P.pairingIn ℤ (RootPairing.EmbeddedG2.short P) i + P.pairingIn ℤ (RootPairing.EmbeddedG2.long P) i
-- Mathlib.Topology.Maps.Basic
IsClosedMap.eq_1 : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : X → Y),
  IsClosedMap f = ∀ (U : Set X), IsClosed U → IsClosed (f '' U)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instAddGroupOfIsTopologicalAddGroup.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β],
  ContinuousMap.instAddGroupOfIsTopologicalAddGroup =
    { toAddMonoid := ContinuousMap.instAddMonoidOfContinuousAdd, toNeg := ContinuousMap.instNegOfContinuousNeg,
      toSub := ContinuousMap.instSubOfContinuousSub, toZSMul := ZSMul.ofSMul, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯,
      zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Init.SizeOfLemmas
SizeOf.sizeOf.congr_simp : ∀ {α : Sort u} [self : SizeOf α] (a a_1 : α), a = a_1 → sizeOf a = sizeOf a_1
-- Mathlib.LinearAlgebra.Pi
LinearMap.lsum_piSingle : ∀ (R : Type u) {M : Type v} {ι : Type x} [inst : Semiring R] (φ : ι → Type i) [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] [inst_3 : DecidableEq ι] (S : Type u_1) [inst_4 : AddCommMonoid M]
  [inst_5 : Module R M] [inst_6 : Fintype ι] [inst_7 : Semiring S] [inst_8 : Module S M] [inst_9 : SMulCommClass R S M]
  (f : (i : ι) → φ i →ₗ[R] M) (i : ι) (x : φ i), ((LinearMap.lsum R φ S) f) (Pi.single i x) = (f i) x
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.i_self : ∀ (R : Type u_1) [inst : CommRing R] {c₁ c₂ c₃ : R},
  (QuaternionAlgebra.Basis.self R).i = { re := 0, imI := 1, imJ := 0, imK := 0 }
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- When `β` has a bottom element, `conditional β` is given by limits over finite intervals
`{y | y ≤ x}` as `x → atTop`.  -/
SummationFilter.conditional_filter_eq_map_Iic : ∀ {γ : Type u_4} [inst : PartialOrder γ] [inst_1 : LocallyFiniteOrder γ] [inst_2 : OrderBot γ],
  (SummationFilter.conditional γ).filter = Filter.map Finset.Iic Filter.atTop
-- Std.Time.Time.PlainTime
/-- Subtracts nanoseconds from a `PlainTime`.
 -/
Std.Time.PlainTime.subNanoseconds : Std.Time.PlainTime → Std.Time.Nanosecond.Offset → Std.Time.PlainTime
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.bind₁_monomial : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_3} [inst : CommSemiring R] (f : σ → MvPolynomial τ R) (d : σ →₀ ℕ) (r : R),
  (MvPolynomial.bind₁ f) ((MvPolynomial.monomial d) r) = MvPolynomial.C r * ∏ i ∈ d.support, f i ^ d i
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.instAddLeftMono : ∀ {α : Type u_2} [inst : Add α], AddLeftMono (Set α)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.essImage_yonedaAddMon : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaAddMon.essImage = fun F => (F.comp (CategoryTheory.forget AddMonCat)).IsRepresentable
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.nsmul_subset_nsmul_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s t : Finset α} {n : ℕ}, s ⊆ t → n • s ⊆ n • t