mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc_X₂ : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' : κ) (i₀ i₁ i₂ i₃ i₃' : ι) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃'
        hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).X₂ =
    CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageX X data r pq' ⋯
-- Mathlib.Order.BooleanSubalgebra
/-- The inf of Boolean subalgebras is their intersection.  -/
BooleanSubalgebra.instInfSet : {α : Type u_2} → [inst : BooleanAlgebra α] → InfSet (BooleanSubalgebra α)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonLeanPrepareModuleHierarchyParams.toJson : Lean.Lsp.LeanPrepareModuleHierarchyParams → Lean.Json
-- Mathlib.Data.Set.Function
Disjoint.image : ∀ {α : Type u_1} {β : Type u_2} {s t u : Set α} {f : α → β},
  Disjoint s t → Set.InjOn f u → s ⊆ u → t ⊆ u → Disjoint (f '' s) (f '' t)
-- Mathlib.RingTheory.MvPolynomial.Tower
MvPolynomial.aeval_algebraMap_apply : ∀ {R : Type u_1} {A : Type u_2} (B : Type u_3) {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra A B] [inst_5 : Algebra R B] [IsScalarTower R A B]
  (x : σ → A) (p : MvPolynomial σ R),
  (MvPolynomial.aeval (⇑(algebraMap A B) ∘ x)) p = (algebraMap A B) ((MvPolynomial.aeval x) p)
-- Init.Data.Float.Float
instLEFloat : LE Float
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.coe_sdiff : ∀ (x y : ZFSet.{u}), ↑(x \ y) = ↑x \ ↑y
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.eq_1 : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] (f : (i : α) → E i) (p : ENNReal),
  Memℓp f p =
    if p = 0 then {i | f i ≠ 0}.Finite
    else if p = ⊤ then BddAbove (Set.range fun i => ‖f i‖) else Summable fun i => ‖f i‖ ^ p.toReal
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.counit_app_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X : C), e.counit.app (e.functor.obj X) = e.functor.map (e.unitInv.app X)
-- Mathlib.Algebra.Group.Equiv.Defs
/-- The inverse of an isomorphism is an isomorphism.  -/
MulEquiv.symm : {M : Type u_9} → {N : Type u_10} → [inst : Mul M] → [inst_1 : Mul N] → M ≃* N → N ≃* M
-- Mathlib.Probability.Kernel.Composition.MeasureCompProd
MeasureTheory.Measure.dirac_unit_compProd : ∀ {β : Type u_2} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel Unit β) [ProbabilityTheory.IsSFiniteKernel κ],
  (MeasureTheory.Measure.dirac ()).compProd κ = MeasureTheory.Measure.map (Prod.mk ()) (κ ())
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.coe_sub : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] {x y : ℚ}, ↑(x - y) = ↑x - ↑y
-- Aesop.Tree.Data
Aesop.Goal.origin : Aesop.Goal → Aesop.GoalOrigin
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.multiset_prod_X_sub_C_nextCoeff : ∀ {R : Type u} [inst : CommRing R] (t : Multiset R),
  (Multiset.map (fun x => Polynomial.X - Polynomial.C x) t).prod.nextCoeff = -t.sum
-- Mathlib.Algebra.Module.Equiv.Defs
/-- Linear equivalences are transitive.  -/
LinearEquiv.trans : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {R₃ : Type u_4} →
      {M₁ : Type u_8} →
        {M₂ : Type u_9} →
          {M₃ : Type u_10} →
            [inst : Semiring R₁] →
              [inst_1 : Semiring R₂] →
                [inst_2 : Semiring R₃] →
                  [inst_3 : AddCommMonoid M₁] →
                    [inst_4 : AddCommMonoid M₂] →
                      [inst_5 : AddCommMonoid M₃] →
                        {module_M₁ : Module R₁ M₁} →
                          {module_M₂ : Module R₂ M₂} →
                            {module_M₃ : Module R₃ M₃} →
                              {σ₁₂ : R₁ →+* R₂} →
                                {σ₂₁ : R₂ →+* R₁} →
                                  {σ₁₃ : R₁ →+* R₃} →
                                    {σ₃₁ : R₃ →+* R₁} →
                                      {σ₂₃ : R₂ →+* R₃} →
                                        {σ₃₂ : R₃ →+* R₂} →
                                          [RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] →
                                            [RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] →
                                              {re₁₂ : RingHomInvPair σ₁₂ σ₂₁} →
                                                {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} →
                                                  [inst_8 : RingHomInvPair σ₁₃ σ₃₁] →
                                                    {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} →
                                                      {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} →
                                                        [inst_9 : RingHomInvPair σ₃₁ σ₁₃] →
                                                          (M₁ ≃ₛₗ[σ₁₂] M₂) → (M₂ ≃ₛₗ[σ₂₃] M₃) → M₁ ≃ₛₗ[σ₁₃] M₃
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.copy_eq : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (f : α →+o β) (f' : α → β) (h : f' = ⇑f), f.copy f' h = f
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.splitAt.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → ℕ → List α → Sort u_2) (x : α) (xs : List α) (n : ℕ) (acc : List α)
  (h_1 : (x : ℕ) → (x_1 : List α) → motive [] x x_1)
  (h_2 : (x : α) → (xs : List α) → (n : ℕ) → (acc : List α) → motive (x :: xs) n.succ acc)
  (h_3 : (xs : List α) → (x : ℕ) → (acc : List α) → motive xs x acc),
  (match x :: xs, n.succ, acc with
    | [], x, x_1 => h_1 x x_1
    | x :: xs, n.succ, acc => h_2 x xs n acc
    | xs, x, acc => h_3 xs x acc) =
    h_2 x xs n acc
-- Mathlib.Algebra.MvPolynomial.Rename
MvPolynomial.aeval_comp_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} {S : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (k : σ → τ) (g : τ → S) [inst_2 : Algebra R S],
  (MvPolynomial.aeval g).comp (MvPolynomial.rename k) = MvPolynomial.aeval (g ∘ k)
-- Mathlib.Topology.Order.Compact
/-- A continuous function with compact support is bounded above.  -/
Continuous.bddAbove_range_of_hasCompactMulSupport : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIciTopology α] [inst_4 : One α] {f : β → α}, Continuous f → HasCompactMulSupport f → BddAbove (Set.range f)
-- Mathlib.Topology.ClusterPt
MapClusterPt.of_comp : ∀ {X : Type u} [inst : TopologicalSpace X] {α : Type u_1} {β : Type u_2} {F : Filter α} {u : α → X} {x : X} {φ : β → α}
  {p : Filter β}, Filter.Tendsto φ p F → MapClusterPt x p (u ∘ φ) → MapClusterPt x F u
-- Mathlib.CategoryTheory.Category.Quiv
/-- The left triangle identity of `Cat.free ⊣ Quiv.forget` as a natural isomorphism  -/
CategoryTheory.Quiv.freeMapPathsOfCompPathCompositionIso : (V : Type u) →
  [inst : Quiver V] →
    (CategoryTheory.Cat.freeMap (CategoryTheory.Paths.of V)).comp
        (CategoryTheory.pathComposition (CategoryTheory.Paths V)) ≅
      CategoryTheory.Functor.id (CategoryTheory.Paths V)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.frequently_ae_ne_zero_of_integral_ne_zero : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → G}, ∫ (a : α), f a ∂μ ≠ 0 → ∃ᵐ (a : α) ∂μ, f a ≠ 0
-- Mathlib.Order.Hom.Bounded
TopHom.id_apply : ∀ {α : Type u_2} [inst : Top α] (a : α), (TopHom.id α) a = a
-- Mathlib.Data.Quot
Quot.instDecidableLiftOn₂OfDecidablePred : {α : Sort u_1} →
  {β : Sort u_2} →
    (r : α → α → Prop) →
      (s : β → β → Prop) →
        (q₁ : Quot r) →
          (q₂ : Quot s) →
            (f : α → β → Prop) →
              (ha : ∀ (a : α) (b₁ b₂ : β), s b₁ b₂ → f a b₁ = f a b₂) →
                (hb : ∀ (a₁ a₂ : α) (b : β), r a₁ a₂ → f a₁ b = f a₂ b) →
                  [(a : α) → DecidablePred (f a)] → Decidable (q₁.liftOn₂ q₂ f ha hb)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Add
MeasureTheory.lintegral_eapprox_le_lintegral : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → ∀ (n : ℕ), (MeasureTheory.SimpleFunc.eapprox f n).lintegral μ ≤ ∫⁻ (x : α), f x ∂μ
-- Init.Data.SInt.Lemmas
Int64.sub_eq_iff_eq_add : ∀ {a b c : Int64}, a - b = c ↔ a = c + b
-- Mathlib.Algebra.Group.Units.Defs
Units.instMul.eq_1 : ∀ {α : Type u} [inst : Monoid α],
  Units.instMul = { mul := fun u₁ u₂ => { val := ↑u₁ * ↑u₂, inv := u₂.inv * u₁.inv, val_inv := ⋯, inv_val := ⋯ } }
-- Mathlib.Algebra.Category.Grp.Yoneda
/-- The `AddCommGrpCat`-valued coyoneda embedding.  -/
AddCommGrpCat.coyoneda : CategoryTheory.Functor AddCommGrpCatᵒᵖ (CategoryTheory.Functor AddCommGrpCat AddCommGrpCat)
-- Mathlib.Order.Interval.Set.InitialSeg
Set.principalSegIio_top : ∀ {α : Type u_1} [inst : Preorder α] (j : α), (Set.principalSegIio j).top = j
-- Mathlib.RingTheory.Coalgebra.Hom
/-- Identity map as a `CoalgHom`.  -/
CoalgHom.id : (R : Type u_1) →
  (A : Type u_2) →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid A] → [inst_2 : Module R A] → [inst_3 : CoalgebraStruct R A] → A →ₗc[R] A
-- Mathlib.Order.Cover
transGen_wcovBy_eq_reflTransGen_covBy : ∀ {α : Type u_1} [inst : PartialOrder α],
  (Relation.TransGen fun x1 x2 => x1 ⩿ x2) = Relation.ReflTransGen fun x1 x2 => x1 ⋖ x2
-- Init.Data.Array.Basic
List.getElem?_toArray : ∀ {α : Type u} {xs : List α} {i : ℕ}, xs.toArray[i]? = xs[i]?
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
/-- **Alias** of `SimpleGraph.Walk.length_dropUntil_le_length`. -/
SimpleGraph.Walk.length_dropUntil_le : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u v w : V} (p : G.Walk v w) (h : u ∈ p.support),
  (p.dropUntil u h).length ≤ p.length
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.addHom_ext'_iff : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_5} [inst_1 : AddMonoid M] {f g : SkewPolynomial R →+ M},
  f = g ↔
    ∀ (n : ℕ), f.comp (SkewPolynomial.monomial n).toAddMonoidHom = g.comp (SkewPolynomial.monomial n).toAddMonoidHom
-- Mathlib.Data.Finset.Lattice.Fold
/-- Given nonempty finset `s` then `s.inf' H f` is the infimum of its image under `f` in (possibly
unbounded) meet-semilattice `α`, where `H` is a proof of nonemptiness. If `α` has a top element you
may instead use `Finset.inf` which does not require `s` nonempty.  -/
Finset.inf' : {α : Type u_2} → {β : Type u_3} → [SemilatticeInf α] → (s : Finset β) → s.Nonempty → (β → α) → α
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
/-- A universe-heterogeneous version of `Pure.pure`. Given `a : α`, it returns an element of `HetT m α`
with the postcondition `(a = ·)`.
 -/
Std.Iterators.HetT.pure : {m : Type w → Type w'} → [Pure m] → {α : Type v} → α → Std.Iterators.HetT m α
-- Mathlib.Data.Set.Image
Set.preimage_ite : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s t₁ t₂ : Set β), f ⁻¹' s.ite t₁ t₂ = (f ⁻¹' s).ite (f ⁻¹' t₁) (f ⁻¹' t₂)
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- ℤ is finitely presented  -/
Group.IsFinitelyPresented.instIsFinitelyPresentedInt : AddGroup.IsFinitelyPresented ℤ
-- Init.Data.List.Lemmas
List.isSome_head? : ∀ {α : Type u_1} {l : List α}, l.head?.isSome = true ↔ l ≠ []
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inl_snd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.snd = 0
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.idxOfAux.eq_def : ∀ {α : Type u} [inst : BEq α] (xs : Array α) (v : α) (i : ℕ),
  xs.idxOfAux v i = if h : i < xs.size then if (xs[i] == v) = true then some ⟨i, h⟩ else xs.idxOfAux v (i + 1) else none
-- Mathlib.Order.Interval.Set.SuccPred
Set.Icc_succ_left_eq_Ioc_of_not_isMax : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a : α},
  ¬IsMax a → ∀ (b : α), Set.Icc (Order.succ a) b = Set.Ioc a b
-- Mathlib.Algebra.Polynomial.OfFn
/-- `toFn n f` is the vector of the first `n` coefficients of the polynomial `f`.  -/
Polynomial.toFn : {R : Type u_1} → [inst : Semiring R] → (n : ℕ) → Polynomial R →ₗ[R] Fin n → R
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Umod.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (n d : aig.RefVec w) (wn wr : ℕ)
  (q r : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.go aig 0 n d wn wr q r = { aig := aig, q := q, r := r, hle := ⋯ }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Cache.empty : {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} → Std.Tactic.BVDecide.BVExpr.Cache aig
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_comm : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  (M N : Submodule R A), M * N = N * M
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.map_lift_kernelComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasKernel (G.map f)] {Z : C} {h : Z ⟶ X}
  (w : CategoryTheory.CategoryStruct.comp h f = 0),
  CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.kernel.lift f h w))
      (CategoryTheory.Limits.kernelComparison f G) =
    CategoryTheory.Limits.kernel.lift (G.map f) (G.map h) ⋯
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.coe_finsetSum : ∀ {α : Type u_1} {ι : Type u_5} {_m : MeasurableSpace α} (I : Finset ι) (μ : ι → MeasureTheory.Measure α),
  ⇑(∑ i ∈ I, μ i) = ∑ i ∈ I, ⇑(μ i)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.toArray_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp},
  (Std.DTreeMap.Const.toList t).toArray = Std.DTreeMap.Const.toArray t
-- Mathlib.Data.Finset.Card
Finset.length_toList : ∀ {α : Type u_1} (s : Finset α), s.toList.length = s.card
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.containsThenInsertIfNew_snd : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {k : α} {v : β k},
  (m.containsThenInsertIfNew k v).2 = m.insertIfNew k v
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.HomotopyCategory.instUniqueOfObjOppositeTruncatedOfNatNatOpMkSimplexCategoryLeLenMk : (X : SSet.Truncated 2) →
  [Unique (X.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 }))] →
    Unique X.HomotopyCategory
-- Mathlib.Algebra.Group.Opposite
AddOpposite.isDedekindFiniteAddMonoid_iff : ∀ {α : Type u_1} [inst : AddZero α], IsDedekindFiniteAddMonoid αᵃᵒᵖ ↔ IsDedekindFiniteAddMonoid α
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Flavors.zero.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (ch : Std.CloseableChannel.Zero✝ α),
  sizeOf (Std.CloseableChannel.Flavors.zero✝ ch) = 1 + sizeOf ch
-- Mathlib.RepresentationTheory.Basic
Representation.instAddCommGroupAsModuleFinsuppMonoidAlgebraFree : (k : Type u_6) →
  (G : Type u_7) →
    [inst : CommRing k] → [inst_1 : Monoid G] → (α : Type u_8) → AddCommGroup (Representation.free k G α).asModule
-- Mathlib.Algebra.GradedMonoid
Mul.gMul_mul : ∀ (ι : Type u_1) {R : Type u_2} [inst : Add ι] [inst_1 : Mul R] {i j : ι} (x y : R), GradedMonoid.GMul.mul x y = x * y
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedValue_norm : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ : Ω → WithTop ι}
  [inst_1 : SeminormedAddCommGroup β],
  MeasureTheory.stoppedValue (fun t ω => ‖u t ω‖) τ = fun ω => ‖MeasureTheory.stoppedValue u τ ω‖
-- Mathlib.Algebra.Order.Round
round_one : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α], round 1 = 1
-- Mathlib.Analysis.Fourier.FourierTransform
/-- Fubini's theorem for the Fourier integral.

This is the main technical step in proving both Parseval's identity and self-adjointness of the
Fourier transform.  -/
VectorFourier.integral_fourierIntegral_swap : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module 𝕜 W] {E : Type u_4}
  {F : Type u_5} {G : Type u_6} [inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace ℂ E]
  [inst_8 : NormedAddCommGroup F] [inst_9 : NormedSpace ℂ F] [inst_10 : NormedAddCommGroup G]
  [inst_11 : NormedSpace ℂ G] [inst_12 : TopologicalSpace 𝕜] [IsTopologicalRing 𝕜] [inst_14 : TopologicalSpace V]
  [BorelSpace V] [inst_16 : TopologicalSpace W] [inst_17 : MeasurableSpace W] [BorelSpace W] {e : AddChar 𝕜 Circle}
  {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜} {ν : MeasureTheory.Measure W} [MeasureTheory.SigmaFinite μ]
  [MeasureTheory.SigmaFinite ν] [SecondCountableTopologyEither W V] {σ : ℂ →+* ℂ} [RingHomIsometric σ] {f : V → E}
  {g : W → F} (M : F →L[ℂ] E →SL[σ] G),
  Continuous ⇑e →
    (Continuous fun p => (L p.1) p.2) →
      MeasureTheory.Integrable f μ →
        MeasureTheory.Integrable g ν →
          ∫ (ξ : W), ∫ (x : V), (M (g ξ)) (e (-(L x) ξ) • f x) ∂μ ∂ν =
            ∫ (x : V), ∫ (ξ : W), (M (g ξ)) (e (-(L x) ξ) • f x) ∂ν ∂μ
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nullMeasurableSet_Ioo : ∀ {α : Type u_1} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α] [inst_2 : LinearOrder α]
  {a b : α} {μ : MeasureTheory.Measure α} [OrderClosedTopology α], MeasureTheory.NullMeasurableSet (Set.Ioo a b) μ
-- Mathlib.Data.Part
Part.bind_toOption : ∀ {α : Type u_1} {β : Type u_2} (f : α → Part β) (o : Part α) [inst : Decidable o.Dom]
  [inst_1 : (a : α) → Decidable (f a).Dom] [inst_2 : Decidable (o.bind f).Dom],
  (o.bind f).toOption = o.toOption.elim none fun a => (f a).toOption
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.opObjEquiv_yonedaEquiv_const : ∀ {X : SSet} {n : SimplexCategory} (x : X.op.obj (Opposite.op { len := 0 })),
  SSet.opObjEquiv (SSet.yonedaEquiv (SSet.const x)) = SSet.yonedaEquiv (SSet.const (SSet.opObjEquiv x))
-- Init.WF
/-- Strong induction on the natural numbers.

The induction hypothesis is that all numbers less than a given number satisfy the motive, which
should be demonstrated for the given number.
 -/
Nat.strongRecOn : {motive : ℕ → Sort u} → (n : ℕ) → ((n : ℕ) → ((m : ℕ) → m < n → motive m) → motive n) → motive n
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.sInf_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C]
  [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] [inst_3 : CategoryTheory.Limits.HasWidePullbacks C] {A : C}
  (s : Set (CategoryTheory.Subobject A)), ∀ f ∈ s, CategoryTheory.Subobject.sInf s ≤ f
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₅_app_five : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 5}
  (app₀ : f.obj' 0 _proof_449✝ ⟶ g.obj' 0 _proof_449✝) (app₁ : f.obj' 1 _proof_450✝ ⟶ g.obj' 1 _proof_450✝)
  (app₂ : f.obj' 2 _proof_451✝ ⟶ g.obj' 2 _proof_451✝) (app₃ : f.obj' 3 _proof_452✝ ⟶ g.obj' 3 _proof_452✝)
  (app₄ : f.obj' 4 _proof_453✝ ⟶ g.obj' 4 _proof_453✝) (app₅ : f.obj' 5 _proof_454✝ ⟶ g.obj' 5 _proof_454✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_450✝))
      _auto_513✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_451✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_451✝))
      _auto_515✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_452✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_452✝))
      _auto_517✝)
  (w₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_453✝) app₄ =
        CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_453✝))
      _auto_519✝)
  (w₄ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 4 5 _proof_453✝ _proof_454✝) app₅ =
        CategoryTheory.CategoryStruct.comp app₄ (g.map' 4 5 _proof_453✝ _proof_454✝))
      _auto_521✝),
  (CategoryTheory.ComposableArrows.homMk₅ app₀ app₁ app₂ app₃ app₄ app₅ w₀ w₁ w₂ w₃ w₄).app
      ⟨5, CategoryTheory.ComposableArrows.homMk₅._proof_6⟩ =
    app₅
-- Mathlib.Geometry.Euclidean.Triangle
/-- The cosine of the sum of two angles in a possibly degenerate
triangle (where two given sides are nonzero), vector angle form.  -/
_private.Mathlib.Geometry.Euclidean.Triangle.0.InnerProductGeometry.cos_angle_eq_cos_angle_add_add_angle_add : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  x ≠ 0 →
    y ≠ 0 →
      Real.cos (InnerProductGeometry.angle x y) =
        Real.cos (InnerProductGeometry.angle x (x + y) + InnerProductGeometry.angle y (y + x))
-- Mathlib.Order.Category.LinOrd
LinOrd.coe_of : ∀ (X : Type u) [inst : LinearOrder X], ↑{ carrier := X, str := inst } = X
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.coeFn_zero_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  [NeZero μ] [inst_3 : Zero β] {x : α}, ↑0 x = 0
-- Std.Http.Data.URI.Basic
/-- Adds a query parameter with a value. Both key and value will be automatically percent-encoded when
building.
 -/
Std.Http.URI.Builder.addQueryParam : Std.Http.URI.Builder → String → String → Std.Http.URI.Builder
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedContext.macroStack : Lean.Elab.Term.SavedContext → Lean.Elab.MacroStack
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasCondSubgaussianMGF.ae_condExp_le : ∀ {Ω : Type u_1} {m mΩ : MeasurableSpace Ω} {hm : m ≤ mΩ} [inst : StandardBorelSpace Ω] {μ : MeasureTheory.Measure Ω}
  [inst_1 : MeasureTheory.IsFiniteMeasure μ] {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasCondSubgaussianMGF m hm X c μ →
    ∀ (t : ℝ), ∀ᵐ (ω' : Ω) ∂μ, μ[fun ω => Real.exp (t * X ω) | m] ω' ≤ Real.exp (↑c * t ^ 2 / 2)
-- Mathlib.Data.Finset.Insert
Finset.cons_val : ∀ {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s), (Finset.cons a s h).val = a ::ₘ s.val
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyGT?.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α),
  Std.DTreeMap.Internal.Impl.getKeyGT? k = Std.DTreeMap.Internal.Impl.getKeyGT?.go k none
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
Directed.ciInf_le_of_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α] {a : α} {f : ι → α},
  Directed (fun x1 x2 => x2 ≤ x1) f → BddBelow (Set.range f) → ∀ (c : ι), f c ≤ a → iInf f ≤ a