mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.of_toList_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp}, t₁.toList.Perm t₂.toList → t₁.Equiv t₂
-- Mathlib.Order.Filter.Map
Function.Commute.filter_map : ∀ {α : Type u_1} {f g : α → α}, Function.Commute f g → Function.Commute (Filter.map f) (Filter.map g)
-- Mathlib.Data.Finset.Lattice.Basic
Finset.mem_union : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Finset α} {a : α}, a ∈ s ∪ t ↔ a ∈ s ∨ a ∈ t
-- Mathlib.Data.List.Iterate
Nat.iterate.eq_2 : ∀ {α : Sort u} (op : α → α) (x : α) (k : ℕ), op^[k.succ] x = op^[k] (op x)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_of_mem_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] {f : α → Bool} {k : α},
  t.WF → k ∈ Std.TreeSet.Raw.filter f t → k ∈ t
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.uniqueUpToIso.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {s t : CategoryTheory.Limits.Cocone F} (P : CategoryTheory.Limits.IsColimit s)
  (Q : CategoryTheory.Limits.IsColimit t),
  P.uniqueUpToIso Q = { hom := P.descCoconeMorphism t, inv := Q.descCoconeMorphism s, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.range_coprod : ∀ {R : Type u_1} {M : Type u_3} {M₁ : Type u_5} {M₂ : Type u_6} [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M₁] [inst_3 : TopologicalSpace M₂] [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  [inst_6 : ContinuousAdd M] [inst_7 : AddCommMonoid M₁] [inst_8 : Module R M₁] [inst_9 : AddCommMonoid M₂]
  [inst_10 : Module R M₂] (f₁ : M₁ →L[R] M) (f₂ : M₂ →L[R] M), (↑(f₁.coprod f₂)).range = (↑f₁).range ⊔ (↑f₂).range
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.nnrpow_nnrpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {a : A} {x y : NNReal}, (a ^ x) ^ y = a ^ (x * y)
-- Mathlib.RingTheory.Extension.Generators
IsLocalization.Away.invSelf.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Type u_2} [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (x : R)
  [inst_3 : IsLocalization.Away x S], IsLocalization.Away.invSelf x = IsLocalization.mk' S 1 ⟨x, ⋯⟩
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
ModularGroup.S_inv : ModularGroup.S⁻¹ = -ModularGroup.S
-- Mathlib.Algebra.Group.Action.Basic
IsAddUnit.vadd_bijective : ∀ {α : Type u_5} {β : Type u_6} [inst : AddMonoid α] [inst_1 : AddAction α β] {m : α},
  IsAddUnit m → Function.Bijective fun a => m +ᵥ a
-- Mathlib.Topology.Sequences
/-- Sequential compactness of sets is preserved under sequentially continuous functions.  -/
IsSeqCompact.image : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  SeqContinuous f → ∀ {K : Set X}, IsSeqCompact K → IsSeqCompact (f '' K)
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- If `t.coef = 0`, then `t.toFun` is zero.  -/
Tactic.ComputeAsymptotics.Monomial.zero_coef_toFun' : ∀ (basis : Tactic.ComputeAsymptotics.Basis) (exps : Tactic.ComputeAsymptotics.UnitMonomial),
  { coef := 0, unit := exps }.toFun basis = 0
-- Mathlib.Algebra.Lie.Weights.Chain
/-- The first weight in an `α`-chain through `β`.  -/
LieModule.chainBot : {R : Type u_1} →
  {L : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          {M : Type u_3} →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [inst_6 : LieModule R L M] →
                    [inst_7 : LieRing.IsNilpotent L] →
                      [IsAddTorsionFree R] →
                        [IsDomain R] →
                          [Module.IsTorsionFree R M] →
                            [IsNoetherian R M] → (L → R) → LieModule.Weight R L M → LieModule.Weight R L M
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instMonoidalActionTypeLinearization : (k : Type u) → (G : Type v) → [inst : CommRing k] → [inst_1 : Monoid G] → (Rep.linearization k G).Monoidal
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- When `data : FunctorialFactorizationData W₁ W₂`, this is the
morphism `(data.factorizationData f).Z ⟶ (data.factorizationData g).Z` expressing the
functoriality of the intermediate objects of the factorizations
for `φ : Arrow.mk f ⟶ Arrow.mk g`.  -/
CategoryTheory.MorphismProperty.FunctorialFactorizationData.mapZ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} →
      (data : W₁.FunctorialFactorizationData W₂) →
        {X Y X' Y' : C} →
          {f : X ⟶ Y} →
            {g : X' ⟶ Y'} →
              (CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk g) →
                ((data.factorizationData f).Z ⟶ (data.factorizationData g).Z)
-- Lean.Data.Lsp.Client
Lean.Lsp.RegistrationParams.registrations : Lean.Lsp.RegistrationParams → Array Lean.Lsp.Registration
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.mkNotCached_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (idx : ℕ) (aig : Std.Sat.AIG α) (gate : aig.Ref)
  {h : idx < aig.decls.size} {h2 : idx < (aig.mkNotCached gate).aig.decls.size},
  (aig.mkNotCached gate).aig.decls[idx] = aig.decls[idx]
-- ProofWidgets.Data.Html
/-- Interpolates an array of elements into a JSX literal  -/
ProofWidgets.Jsx.«proofWidgetsJsxChild{..._}» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Module.Defs
Pi.instSMulPosReflectLT : ∀ {α : Type u_1} {ι : Type u_3} {β : ι → Type u_4} [inst : Zero α] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : PartialOrder α] [inst_3 : (i : ι) → PartialOrder (β i)] [inst_4 : (i : ι) → SMulWithZero α (β i)]
  [∀ (i : ι), SMulPosReflectLT α (β i)], SMulPosReflectLT α ((i : ι) → β i)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instAdd : {α : Type u_1} → {x : MeasurableSpace α} → Add (MeasureTheory.Measure α)
-- Init.Data.BitVec.Lemmas
BitVec.cpop_append : ∀ {w u : ℕ} {x : BitVec w} {y : BitVec u},
  (x ++ y).cpop = BitVec.setWidth (w + u) x.cpop + BitVec.setWidth (w + u) y.cpop
-- Init.Data.BitVec.Bitblast
/-- The quotient is morally a `Bitvec wr`, and so has value less than `2^wr`.  -/
BitVec.DivModState.Lawful.hqWidth : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w},
  BitVec.DivModState.Lawful args qr → qr.q.toNat < 2 ^ qr.wr
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
/-- The morphism of locally ringed space from `Proj|D(f)` to `Spec A⁰_f` induced by the ring map
`A⁰_ f → Γ(Proj, D(f))` under the gamma spec adjunction.
 -/
AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              (f : A) →
                (AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯ ⟶
                  AlgebraicGeometry.Spec.locallyRingedSpaceObj (CommRingCat.of (HomogeneousLocalization.Away 𝒜 f))
-- Mathlib.Analysis.Fourier.ZMod
ZMod.dft_const_mul : ∀ {N : ℕ} [inst : NeZero N] {R : Type u_2} [inst_1 : Ring R] [inst_2 : Algebra ℂ R] (r : R) (Φ : ZMod N → R),
  (ZMod.dft fun j => r * Φ j) = fun k => r * ZMod.dft Φ k
-- Mathlib.Geometry.Manifold.VectorBundle.MDifferentiable
mDifferentiableOn_sub_section : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : TopologicalSpace B]
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : (x : B) → TopologicalSpace (E x)]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NontriviallyNormedField 𝕜] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : FiberBundle F E] [inst_7 : (x : B) → AddCommGroup (E x)] [inst_8 : (x : B) → Module 𝕜 (E x)]
  [VectorBundle 𝕜 F E] {HB : Type u_7} [inst_10 : TopologicalSpace HB] [inst_11 : ChartedSpace HB B] {EB : Type u_8}
  [inst_12 : NormedAddCommGroup EB] [inst_13 : NormedSpace 𝕜 EB] {I : ModelWithCorners 𝕜 EB HB} {s t : (x : B) → E x}
  {u : Set B}, MDiff[u] (T% s) → MDiff[u] (T% t) → MDiff[u] fun x => ⟨x, (s - t) x⟩
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.yonedaGrpObjRepresentableBy.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C] (G : C)
  [inst_2 : CategoryTheory.GrpObj G],
  CategoryTheory.yonedaGrpObjRepresentableBy G =
    CategoryTheory.Functor.representableByEquiv.symm (CategoryTheory.Iso.refl (CategoryTheory.yoneda.obj G))
-- Mathlib.Data.Real.ConjExponents
NNReal.conjExponent.eq_1 : ∀ (p : NNReal), p.conjExponent = p / (p - 1)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.le_toMeasure_apply : ∀ {α : Type u_1} [ms : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α) (h : ms ≤ m.caratheodory) (s : Set α),
  m s ≤ (m.toMeasure h) s
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.str : (self : AddCommGrpCat) → AddCommGroup ↑self
-- Std.Data.HashSet.Basic
Std.HashSet.instDecidableMem : {α : Type u} → [inst : BEq α] → [inst_1 : Hashable α] → {m : Std.HashSet α} → {a : α} → Decidable (a ∈ m)
-- Mathlib.CategoryTheory.Action
/-- The canonical map `ActionCategory M X → X`. It is given by `fun x => x.snd`, but
has a more explicit type.  -/
CategoryTheory.ActionCategory.back : {M : Type u_1} → [inst : Monoid M] → {X : Type u} → [inst_1 : MulAction M X] → CategoryTheory.ActionCategory M X → X
-- Lean.Meta.Tactic.Grind.MatchCond
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go.match_1.eq_2 : ∀ (motive : Option Lean.Expr → Sort u_1) (x : Option Lean.Expr) (h_1 : (α : Lean.Expr) → motive (some α))
  (h_2 : (x : Option Lean.Expr) → motive x),
  (∀ (α : Lean.Expr), x = some α → False) →
    (match x with
      | some α => h_1 α
      | x => h_2 x) =
      h_2 x
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.mul_inv_eq_inv_mul_of_doubling_lt_two_aux : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A : Finset G}, (A * A).card < 2 * A.card → A⁻¹ * A ⊆ A * A⁻¹
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stmts₁.match_1.eq_5 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5)
  (a : σ → Bool) (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ)
  (h_1 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Γ k) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.push k a q → motive (Turing.TM2.Stmt.push k a q))
  (h_2 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.peek k a q → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.pop k a q → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.load a q → motive (Turing.TM2.Stmt.load a q))
  (h_5 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → Bool) →
        (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.branch a q₁ q₂ → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (Q : Turing.TM2.Stmt Γ Λ σ) → (a : σ → Λ) → Q = Turing.TM2.Stmt.goto a → motive (Turing.TM2.Stmt.goto a))
  (h_7 : (Q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.halt → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.branch a q₁ q₂ with
    | Q@h:(Turing.TM2.Stmt.push k a q) => h_1 Q k a q h
    | Q@h:(Turing.TM2.Stmt.peek k a q) => h_2 Q k a q h
    | Q@h:(Turing.TM2.Stmt.pop k a q) => h_3 Q k a q h
    | Q@h:(Turing.TM2.Stmt.load a q) => h_4 Q a q h
    | Q@h:(Turing.TM2.Stmt.branch a q₁ q₂) => h_5 Q a q₁ q₂ h
    | Q@h:(Turing.TM2.Stmt.goto a) => h_6 Q a h
    | Q@h:Turing.TM2.Stmt.halt => h_7 Q h) =
    h_5 (Turing.TM2.Stmt.branch a q₁ q₂) a q₁ q₂ ⋯
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.IsTheta.finsetProd : ∀ {α : Type u_1} {𝕜 : Type u_14} {𝕜' : Type u_15} [inst : NormedField 𝕜] [inst_1 : NormedField 𝕜'] {l : Filter α}
  {ι : Type u_16} {s : Finset ι} {f : ι → α → 𝕜} {g : ι → α → 𝕜'},
  (∀ i ∈ s, f i =Θ[l] g i) → (fun x => ∏ i ∈ s, f i x) =Θ[l] fun x => ∏ i ∈ s, g i x
-- Lean.Elab.Syntax
Lean.Elab.Term.ToParserDescrContext.mk.sizeOf_spec : ∀ (catName : Lean.Name) (first leftRec : Bool) (behavior : Lean.Parser.LeadingIdentBehavior),
  sizeOf { catName := catName, first := first, leftRec := leftRec, behavior := behavior } =
    1 + sizeOf catName + sizeOf first + sizeOf leftRec + sizeOf behavior
-- Mathlib.Logic.Embedding.Basic
Function.Embedding.subtype_injective : ∀ {α : Sort u_1} (p : α → Prop), Function.Injective ⇑(Function.Embedding.subtype p)
-- Aesop.Tree.AddRapp
Aesop.AddRapp.appliedRule : Aesop.AddRapp → Aesop.RegularRule
-- Mathlib.NumberTheory.GaussSum
/-- Definition of the Gauss sum associated to a multiplicative and an additive character.  -/
gaussSum : {R : Type u} →
  [inst : CommRing R] → [Fintype R] → {R' : Type v} → [inst_2 : CommRing R'] → MulChar R R' → AddChar R R' → R'
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_min?_iff_isEmpty_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.min?.isSome = true ↔ t.isEmpty = false
-- Init.Data.String.Defs
String.instInhabitedSlice : Inhabited String.Slice
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- Via `S.pOpcycles : S.X₂ ⟶ S.opcycles`, the object `S.opcycles` identifies to the
cokernel of `S.f : S.X₁ ⟶ S.X₂`.  -/
CategoryTheory.ShortComplex.opcyclesIsCokernel : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        [inst_2 : S.HasRightHomology] →
          CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ S.pOpcycles ⋯)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_max : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → ENNReal},
  Measurable f →
    Measurable g →
      ∀ (s : Set α),
        ∫⁻ (x : α) in s, max (f x) (g x) ∂μ =
          ∫⁻ (x : α) in s ∩ {x | f x ≤ g x}, g x ∂μ + ∫⁻ (x : α) in s ∩ {x | g x < f x}, f x ∂μ
-- Init.Data.List.Sublist
List.singleton_prefix_iff_head?_eq_some : ∀ {α : Type u_1} {a : α} {l : List α}, [a] <+: l ↔ l.head? = some a
-- Std.Http.Data.Headers.Value
/-- A validated HTTP header value that ensures all characters conform to HTTP standards.
 -/
Std.Http.Header.Value : Type
-- Init.Data.Nat.Basic
Nat.sub_eq : ∀ {x y : ℕ}, x.sub y = x - y
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.minKey?_eq_some_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {km : α}, t.minKey? = some km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.matiyasevic : ∀ {a k x y : ℕ},
  (∃ (a1 : 1 < a), Pell.xn a1 k = x ∧ Pell.yn a1 k = y) ↔
    1 < a ∧
      k ≤ y ∧
        (x = 1 ∧ y = 0 ∨
          ∃ u v s t b,
            x * x - (a * a - 1) * y * y = 1 ∧
              u * u - (a * a - 1) * v * v = 1 ∧
                s * s - (b * b - 1) * t * t = 1 ∧
                  1 < b ∧ b ≡ 1 [MOD 4 * y] ∧ b ≡ a [MOD u] ∧ 0 < v ∧ y * y ∣ v ∧ s ≡ x [MOD u] ∧ t ≡ k [MOD 4 * y])
-- Mathlib.LinearAlgebra.FreeModule.PID
Ideal.finrank_eq_finrank : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {S : Type u_4}
  [inst_3 : CommRing S] [IsDomain S] [inst_5 : Algebra R S] [Finite ι] (b : Module.Basis ι R S) (I : Ideal S),
  I ≠ ⊥ → Module.finrank R ↥(Submodule.restrictScalars R I) = Module.finrank R S
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.associator_naturality₂_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  {X₁ X₂ X₃ Y₂ : CategoryTheory.LocalizedMonoidal L W ε} (f₂ : X₂ ⟶ Y₂) {Z : CategoryTheory.LocalizedMonoidal L W ε}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ X₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁ f₂) X₃)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₂ X₃).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₁ X₂ X₃).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁
          (CategoryTheory.MonoidalCategoryStruct.whiskerRight f₂ X₃))
        h)
-- Mathlib.Data.Set.Defs
Set.instUsesSetNotationForOrder : (α : Type u) → UsesSetNotationForOrder (Set α)
-- Init.Data.SInt.Lemmas
Int32.ofInt_int16ToInt : ∀ (x : Int16), Int32.ofInt x.toInt = x.toInt32
-- Mathlib.Logic.Relation
Relation.TransGen.trans_right : ∀ {α : Type u_1} {r : α → α → Prop} {a b c : α},
  Relation.ReflTransGen r a b → Relation.TransGen r b c → Relation.TransGen r a c
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.adjoint_rTensor : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] [inst_7 : CompleteSpace E] [CompleteSpace G]
  [inst_9 : CompleteSpace (TensorProduct 𝕜 E G)] [inst_10 : CompleteSpace (TensorProduct 𝕜 F G)]
  [inst_11 : CompleteSpace F] (f : E →L[𝕜] F),
  ContinuousLinearMap.adjoint (ContinuousLinearMap.rTensor G f) =
    ContinuousLinearMap.rTensor G (ContinuousLinearMap.adjoint f)
-- Lean.Environment
Lean.ModuleData.entries : Lean.ModuleData → Array (Lean.Name × Array Lean.EnvExtensionEntry)
-- Lean.Elab.Do.Basic
Lean.Elab.Do.elabDoElem : Lean.DoElem → Lean.Elab.Do.DoElemCont → optParam Bool true → Lean.Elab.Do.DoElabM Lean.Expr
-- Mathlib.Analysis.Fourier.AddCircle
fourierCoeffOn_eq_integral : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {a b : ℝ} (f : ℝ → E) (n : ℤ) (hab : a < b),
  fourierCoeffOn hab f n = (1 / (b - a)) • ∫ (x : ℝ) in a..b, (fourier (-n)) ↑x • f x
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.norm_one_sub_charFun_le_two : ∀ {E : Type u_2} {mE : MeasurableSpace E} {μ : MeasureTheory.Measure E} {t : E} [inst : SeminormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] [MeasureTheory.IsProbabilityMeasure μ], ‖1 - MeasureTheory.charFun μ t‖ ≤ 2
-- Mathlib.MeasureTheory.Measure.TightNormed
MeasureTheory.isTightMeasureSet_range_of_tendsto_limsup_measureReal_inner_of_norm_eq_one : ∀ {E : Type u_1} {mE : MeasurableSpace E} [inst : NormedAddCommGroup E] (𝕜 : Type u_2) [inst_1 : RCLike 𝕜]
  [inst_2 : InnerProductSpace 𝕜 E] [FiniteDimensional 𝕜 E] [BorelSpace E] {μ : ℕ → MeasureTheory.Measure E}
  [∀ (i : ℕ), MeasureTheory.IsFiniteMeasure (μ i)],
  (∀ (y : E),
      ‖y‖ = 1 →
        Filter.Tendsto (fun r => Filter.limsup (fun n => (μ n).real {x | r < ‖inner 𝕜 y x‖}) Filter.atTop) Filter.atTop
          (nhds 0)) →
    ∀ (C : NNReal), (∀ᶠ (n : ℕ) in Filter.atTop, (μ n) Set.univ ≤ ↑C) → MeasureTheory.IsTightMeasureSet (Set.range μ)
-- Lean.Parser.Do
Lean.Parser.Term.doBreak.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_add_left_nhdsGT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : AddCommGroup H] [inst_2 : PartialOrder H] [IsOrderedAddMonoid H]
  [ContinuousAdd H] {c a : H},
  Filter.map (fun x => c + x) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (c + a) (Set.Ioi (c + a))
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Augment a simplicial object with an object.  -/
CategoryTheory.SimplicialObject.augment : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (X : CategoryTheory.SimplicialObject C) →
      (X₀ : C) →
        (f : X.obj (Opposite.op { len := 0 }) ⟶ X₀) →
          (∀ (i : SimplexCategory) (g₁ g₂ : { len := 0 } ⟶ i),
              CategoryTheory.CategoryStruct.comp (X.map g₁.op) f = CategoryTheory.CategoryStruct.comp (X.map g₂.op) f) →
            CategoryTheory.SimplicialObject.Augmented C
-- Mathlib.Data.Sum.Order
_private.Mathlib.Data.Sum.Order.0.Option.elim.match_1.eq_2 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Option α → β → (α → β) → Sort u_2) (y : β) (x : α → β)
  (h_1 : (x : α) → (x_1 : β) → (f : α → β) → motive (some x) x_1 f) (h_2 : (y : β) → (x : α → β) → motive none y x),
  (match none, y, x with
    | some x, x_1, f => h_1 x x_1 f
    | none, y, x => h_2 y x) =
    h_2 y x
-- Lean.Util.FindLevelMVar
Lean.FindLevelMVar.main : (Lean.LMVarId → Bool) → Lean.Expr → Lean.FindLevelMVar.Visitor
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.ExtensionState.mk.injEq : ∀ {γ : Type} (newEntries : List Lean.KeyedDeclsAttribute.OLeanEntry) (table : Lean.KeyedDeclsAttribute.Table γ)
  (declNames erased : Lean.PHashSet Lean.Name) (newEntries_1 : List Lean.KeyedDeclsAttribute.OLeanEntry)
  (table_1 : Lean.KeyedDeclsAttribute.Table γ) (declNames_1 erased_1 : Lean.PHashSet Lean.Name),
  ({ newEntries := newEntries, table := table, declNames := declNames, erased := erased } =
      { newEntries := newEntries_1, table := table_1, declNames := declNames_1, erased := erased_1 }) =
    (newEntries = newEntries_1 ∧ table = table_1 ∧ declNames = declNames_1 ∧ erased = erased_1)
-- Init.Control.Except
/-- A successful computation in the `Except ε` monad: `a` is returned, and no exception is thrown.
 -/
Except.pure : {ε : Type u} → {α : Type u_1} → α → Except ε α
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
IsLUB.ciSup_set_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLattice α] {a : α} {s : Set β} {f : β → α},
  IsLUB (f '' s) a → s.Nonempty → ⨆ i, f ↑i = a
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalSubgroup.instPartialOrder.eq_1 : ∀ {G : Type u_1} [inst : Group G],
  FiniteIndexNormalSubgroup.instPartialOrder = PartialOrder.ofSetLike (FiniteIndexNormalSubgroup G) G
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- Given a cylinder `P` for `X`, two maps `f` and `g` in `X ⟶ Y`
are homotopic relative to `P` when there is a morphism `h : P.I ⟶ Y`
such that `P.i₀ ≫ h = f` and `P.i₁ ≫ h = g`.  -/
HomotopicalAlgebra.Cylinder.LeftHomotopy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
        HomotopicalAlgebra.Cylinder X → (X ⟶ Y) → (X ⟶ Y) → Type v
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The identity between the `SubMulAction`s of `fixingSubgroup`s
of equal sets, as an equivariant map.  -/
SubMulAction.ofFixingSubgroup_of_eq : (M : Type u_1) →
  {α : Type u_2} →
    [inst : Group M] →
      [inst_1 : MulAction M α] →
        {s t : Set α} →
          (hst : s = t) →
            have φ := MulEquiv.subgroupCongr ⋯;
            ↥(SubMulAction.ofFixingSubgroup M s) →ₑ[⇑φ] ↥(SubMulAction.ofFixingSubgroup M t)
-- Mathlib.MeasureTheory.Measure.Complex
MeasureTheory.ComplexMeasure.im_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} (v : MeasureTheory.VectorMeasure α ℂ),
  MeasureTheory.ComplexMeasure.im v = v.mapRange Complex.imLm.toAddMonoidHom Complex.continuous_im