mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.DeclModifiers
Lean.Elab.Modifiers.isNonrec : Lean.Elab.Modifiers → Bool
-- Mathlib.RepresentationTheory.Character
/-- If `V` and `W` are finite-dimensional representations of a finite group, then the
scalar product of their characters is equal to the dimension of the space of
equivariant maps from `V` to `W`.
 -/
Representation.card_inv_mul_sum_char_mul_char_eq_finrank : ∀ {G : Type u_1} {k : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Group G] [inst_1 : Field k]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [FiniteDimensional k V] [inst_5 : AddCommGroup W]
  [inst_6 : Module k W] [FiniteDimensional k W] (ρ : Representation k G V) (σ : Representation k G W)
  [inst_8 : Fintype G] [Invertible ↑(Nat.card G)],
  (↑(Nat.card G))⁻¹ * ∑ g, σ.character g * ρ.character g⁻¹ = ↑(Module.finrank k (ρ.IntertwiningMap σ))
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- A copy induces an embedding of edge sets.  -/
SimpleGraph.Copy.mapEdgeSet : {α : Type u_4} → {β : Type u_5} → {A : SimpleGraph α} → {B : SimpleGraph β} → A.Copy B → ↑A.edgeSet ↪ ↑B.edgeSet
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.addMap_eq : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} (P Q : Fin 3 → R),
  W'.addMap ⟦P⟧ ⟦Q⟧ = ⟦W'.add P Q⟧
-- Lean.Parser.Tactic.Doc
/-- Gets the extensions declared for the documentation for the given canonical tactic name  -/
Lean.Parser.Tactic.Doc.getTacticExtensions : Lean.Environment → Lean.Name → Array String
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
IsEllipticNet.atomRel_abs₂ : ∀ {R : Type u_1} [inst : CommRing R] {W : ℤ → R},
  Function.Odd W → ∀ (a b c d : ℤ), IsEllipticNet.atomRel W a |b| c d = IsEllipticNet.atomRel W a b c d
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_alter_of_beq_eq_false : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β}, m.WF → (k == k') = false → (k' ∈ m.alter k f ↔ k' ∈ m)
-- Mathlib.Topology.EMetricSpace.Lipschitz
LocallyLipschitzOn.eq_1 : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (s : Set α) (f : α → β),
  LocallyLipschitzOn s f = ∀ ⦃x : α⦄, x ∈ s → ∃ K, ∃ t ∈ nhdsWithin x s, LipschitzOnWith K f t
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.count_map_roots : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : IsDomain A] [inst_3 : DecidableEq B]
  {p : Polynomial A} {f : A →+* B},
  Polynomial.map f p ≠ 0 →
    ∀ (b : B), Multiset.count b (Multiset.map (⇑f) p.roots) ≤ Polynomial.rootMultiplicity b (Polynomial.map f p)
-- Mathlib.Order.BooleanAlgebra.Basic
inf_sdiff_self_right : ∀ {α : Type u} {x y : α} [inst : GeneralizedBooleanAlgebra α], x ⊓ y \ x = ⊥
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.sub_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (x : α) [inst_2 : AddGroup β]
  [inst_3 : IsTopologicalAddGroup β] (f g : CompactlySupportedContinuousMap α β), (f - g) x = f x - g x
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.selbergTerms_apply : ∀ {s : BoundingSieve} (d : ℕ), BoundingSieve.selbergTerms d = s.nu d * ∏ p ∈ d.primeFactors, (1 - s.nu p)⁻¹
-- Lean.Compiler.IR.Basic
Lean.IR.instReprVarId.repr : Lean.IR.VarId → ℕ → Std.Format
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.relativeGluingData_functor : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰)
  [inst_5 :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.Limits.PreservesColimitsOfShape J
        (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))],
  d.relativeGluingData.functor = d.functor
-- Std.Http.Data.URI.Encoding
/-- Decodes an encoded query parameter back to a UTF-8 string.
 -/
Std.Http.URI.EncodedQueryParam.decode : Std.Http.URI.EncodedQueryParam → Option String
-- Mathlib.Topology.MetricSpace.Snowflaking
/-- This definition makes `cases x` and `induction x` use `toSnowflaking` instead of `mk`.  -/
Metric.Snowflaking.casesOn_toSnowflaking : {X : Type u_1} →
  {α : ℝ} →
    {hα₀ : 0 < α} →
      {hα₁ : α ≤ 1} →
        {motive : Metric.Snowflaking X α hα₀ hα₁ → Sort u_2} →
          ((x : X) → motive (Metric.Snowflaking.toSnowflaking x)) → (x : Metric.Snowflaking X α hα₀ hα₁) → motive x
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
/-- Consider the contravariant functors between compact Hausdorff spaces and commutative unital
C⋆algebras `F : Cpct → CommCStarAlg := X ↦ C(X, ℂ)` and
`G : CommCStarAlg → Cpct := A → characterSpace ℂ A` whose actions on morphisms are given by
`WeakDual.CharacterSpace.compContinuousMap` and `ContinuousMap.compStarAlgHom'`, respectively.

Then `η : id → F ∘ G := gelfandStarTransform` is a natural isomorphism implementing (half of)
the duality between these categories. That is, for commutative unital C⋆-algebras `A` and `B` and
`φ : A →⋆ₐ[ℂ] B` the following diagram commutes:

```
A  --- η A ---> C(characterSpace ℂ A, ℂ)

|                     |

φ                  (F ∘ G) φ

|                     |
V                     V

B  --- η B ---> C(characterSpace ℂ B, ℂ)
```
 -/
gelfandStarTransform_naturality : ∀ {A : Type u_1} {B : Type u_2} [inst : CommCStarAlgebra A] [inst_1 : CommCStarAlgebra B] (φ : A →⋆ₐ[ℂ] B),
  (↑(gelfandStarTransform B)).comp φ =
    (ContinuousMap.compStarAlgHom' ℂ ℂ (WeakDual.CharacterSpace.compContinuousMap φ)).comp ↑(gelfandStarTransform A)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.post_map : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {X : T} (F : CategoryTheory.Functor T D) {X_1 Y : CategoryTheory.Under X} (f : X_1 ⟶ Y),
  (CategoryTheory.Under.post F).map f = CategoryTheory.Under.homMk (F.map (CategoryTheory.Under.Hom.right f)) ⋯
-- Mathlib.Probability.Kernel.MeasurableLIntegral
/-- Auxiliary lemma for `Measurable.lintegral_kernel_prod_right`.  -/
ProbabilityTheory.Kernel.measurable_lintegral_indicator_const : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {t : Set (α × β)},
  MeasurableSet t → ∀ (c : ENNReal), Measurable fun a => ∫⁻ (b : β), t.indicator (Function.const (α × β) c) (a, b) ∂κ a
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFiltered.wideSpan : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsFilteredOrEmpty C] {I : Type u_1} [Finite I]
  {i : C} {j : I → C} (f : (x : I) → i ⟶ j x),
  ∃ k fik g, ∀ (x : I), CategoryTheory.CategoryStruct.comp (f x) (g x) = fik
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get!_diff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], (m₁ \ m₂).get! k = if k ∈ m₂ then default else m₁.get! k
-- Lean.Linter.Deprecated
Lean.Linter.DeprecationEntry.mk : Option Lean.Name → Option String → Option String → Lean.Linter.DeprecationEntry
-- Mathlib.Topology.Algebra.Group.Units
Units.mapContinuousMulEquiv_apply : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Monoid M]
  [inst_3 : Monoid N] (f : M ≃ₜ* N) (a : Mˣ), (Units.mapContinuousMulEquiv f) a = (Units.map ↑↑f) a
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.setToFun_neg : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (f : α → E),
  MeasureTheory.setToFun μ T hT (-f) = -MeasureTheory.setToFun μ T hT f
-- Mathlib.Algebra.Category.Grp.Limits
CommGrpCat.limitCommGroup.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J CommGrpCat)
  [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget CommGrpCat)).sections],
  CommGrpCat.limitCommGroup F =
    {
      mul :=
        CommGrpCat.limitCommGroup._aux_1 F
          (GrpCat.sectionsSubgroup (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat))).toCommGroup,
      mul_assoc := ⋯,
      one :=
        CommGrpCat.limitCommGroup._aux_4 F
          (GrpCat.sectionsSubgroup (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat))).toCommGroup,
      one_mul := ⋯, mul_one := ⋯,
      npow :=
        CommGrpCat.limitCommGroup._aux_8 F
          (GrpCat.sectionsSubgroup (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat))).toCommGroup,
      npow_zero := ⋯, npow_succ := ⋯,
      inv :=
        CommGrpCat.limitCommGroup._aux_12 F
          (GrpCat.sectionsSubgroup (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat))).toCommGroup,
      div :=
        CommGrpCat.limitCommGroup._aux_14 F
          (GrpCat.sectionsSubgroup (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat))).toCommGroup,
      zpow :=
        CommGrpCat.limitCommGroup._aux_16 F
          (GrpCat.sectionsSubgroup (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat))).toCommGroup,
      div_eq_mul_inv := ⋯, zpow_zero' := ⋯, zpow_succ' := ⋯, zpow_neg' := ⋯, inv_mul_cancel := ⋯, mul_comm := ⋯ }
-- Mathlib.Data.Rel
SetRel.preimage_mono : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α β}, Monotone R.preimage
-- Mathlib.Topology.EMetricSpace.Defs
EMetricSpace.toPseudoEMetricSpace : {α : Type u} → [self : EMetricSpace α] → PseudoEMetricSpace α
-- Mathlib.Data.PEquiv
PEquiv.instBotPEquiv : {α : Type u} → {β : Type v} → Bot (α ≃. β)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_map : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α}, (Std.DHashMap.map f m).get? k = Option.map (f k) (m.get? k)
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.right_U : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P), c.right.U = c.U
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.nnnorm_eq_of_L1 : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp 1 β),
  ‖x‖₊ = ∑ i, ‖x.ofLp i‖₊
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.arrowι_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J]
  [inst_2 : CategoryTheory.Limits.HasIterationOfShape J C] {i : J} (F : CategoryTheory.Functor (↑(Set.Iio i)) C)
  (hi : Order.IsSuccLimit i) (k : J) (hk : k < i),
  CategoryTheory.SmallObject.SuccStruct.arrowι F hi k hk =
    CategoryTheory.Arrow.mk (CategoryTheory.Limits.colimit.ι F ⟨k, hk⟩)
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.mutuallySingular_of_disjoint : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, Disjoint μ ν → μ.MutuallySingular ν
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Path.comp_inj : ∀ {V : Type u} [inst : Quiver V] {a b c : V} {p₁ p₂ : Quiver.Path a b} {q₁ q₂ : Quiver.Path b c},
  q₁.length = q₂.length → (p₁.comp q₁ = p₂.comp q₂ ↔ p₁ = p₂ ∧ q₁ = q₂)
-- Mathlib.Analysis.Normed.Operator.Banach
/-- Associating to a linear equivalence between Banach spaces a continuous linear equivalence when
the direct map is continuous, thanks to the Banach open mapping theorem that ensures that the
inverse map is also continuous.  -/
LinearEquiv.toContinuousLinearEquivOfContinuous : {𝕜 : Type u_1} →
  {𝕜' : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NontriviallyNormedField 𝕜'] →
        {σ : 𝕜 →+* 𝕜'} →
          {E : Type u_3} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {F : Type u_4} →
                  [inst_4 : NormedAddCommGroup F] →
                    [inst_5 : NormedSpace 𝕜' F] →
                      {σ' : 𝕜' →+* 𝕜} →
                        [inst_6 : RingHomInvPair σ σ'] →
                          [RingHomIsometric σ] →
                            [RingHomIsometric σ'] →
                              [CompleteSpace F] →
                                [CompleteSpace E] →
                                  [inst_11 : RingHomInvPair σ' σ] → (e : E ≃ₛₗ[σ] F) → Continuous ⇑e → E ≃SL[σ] F
-- Mathlib.Topology.Inseparable
closure_singleton_eq_Iic : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), closure {x} = Set.Iic x
-- Mathlib.CategoryTheory.Bicategory.Span.Basic
CategoryTheory.Span.hom_ext : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Wₗ Wᵣ : CategoryTheory.MorphismProperty C} {c c' : C}
  {S S' : CategoryTheory.Span Wₗ Wᵣ c c'} {f g : S ⟶ S'}, f.hom = g.hom → f = g
-- Mathlib.Order.RelClasses
eq_empty_relation : ∀ {α : Type u} (r : α → α → Prop) [Std.Irrefl r] [Subsingleton α], r = emptyRelation
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.mem_pointwise_smul_iff_inv_smul_mem : ∀ {α : Type u_1} {M : Type u_3} [inst : Monoid M] [inst_1 : Group α] [inst_2 : MulDistribMulAction α M] {a : α}
  {S : Submonoid M} {x : M}, x ∈ a • S ↔ a⁻¹ • x ∈ S
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.coe_sInf : ∀ {α : Type u_2} [inst : TopologicalSpace α] {S : Set (TopologicalSpace.Closeds α)}, ↑(sInf S) = ⋂ i ∈ S, ↑i
-- Mathlib.Data.Fin.Tuple.Basic
Fin.insertNth_last : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (x : α (Fin.last n)) (p : (j : Fin n) → α ((Fin.last n).succAbove j)),
  (Fin.last n).insertNth x p = Fin.snoc (fun j => cast ⋯ (p j)) x
-- Init.Data.UInt.Basic
/-- Unsigned division for 64-bit unsigned integers, discarding the remainder. Usually accessed
via the `/` operator.

This operation is sometimes called “floor division.” Division by zero is defined to be zero.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.div : UInt64 → UInt64 → UInt64
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousAt_empty : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] [h : IsEmpty ι]
  (F : ι → X → α) (x₀ : X), EquicontinuousAt F x₀
-- Mathlib.Data.List.Forall2
List.forall₂_of_length_eq_of_get : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {x : List α} {y : List β},
  x.length = y.length →
    (∀ (i : ℕ) (h₁ : i < x.length) (h₂ : i < y.length), R (x.get ⟨i, h₁⟩) (y.get ⟨i, h₂⟩)) → List.Forall₂ R x y
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k a fallback : α}, (t.insert k).getD a fallback = if cmp k a = Ordering.eq ∧ k ∉ t then k else t.getD a fallback
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_sub_swap : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  (x y : R), v (x - y) = v (y - x)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.Indep.isBasis_of_forall_insert : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α}, M.Indep I → I ⊆ X → (∀ e ∈ X \ I, M.Dep (insert e I)) → M.IsBasis I X
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.tag.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (a : α) (a_1 : Lean.Widget.TaggedText α),
  sizeOf (Lean.Widget.TaggedText.tag a a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Data.Set.Disjoint
Set.disjoint_iff : ∀ {α : Type u} {s t : Set α}, Disjoint s t ↔ s ∩ t ⊆ ∅
-- Mathlib.Data.List.AList
AList.lookup_erase : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (a : α) (s : AList β), AList.lookup a (AList.erase a s) = none
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.process.processOffset : Lean.Meta.Sym.Offset → Lean.Meta.Sym.Offset → Lean.Meta.Sym.UnifyM✝ Bool
-- Init.Prelude
/-- Heterogeneous equality. `a ≍ b` asserts that `a` and `b` have the same
type, and casting `a` across the equality yields `b`, and vice versa.

You should avoid using this type if you can. Heterogeneous equality does not
have all the same properties as `Eq`, because the assumption that the types of
`a` and `b` are equal is often too weak to prove theorems of interest. One
public important non-theorem is the analogue of `congr`: If `f ≍ g` and `x ≍ y`
and `f x` and `g y` are well typed it does not follow that `f x ≍ g y`.
(This does follow if you have `f = g` instead.) However if `a` and `b` have
the same type then `a = b` and `a ≍ b` are equivalent.


Conventions for notations in identifiers:

 * The recommended spelling of `≍` in identifiers is `heq`. -/
HEq : {α : Sort u} → α → {β : Sort u} → β → Prop
-- Mathlib.SetTheory.Ordinal.FixedPointApproximants
/-- The ordinal-indexed infimum of `gfpApprox` equals `prevFixed`: the greatest fixed point
less than or equal to `x`.  -/
OrdinalApprox.prevFixed_eq_iInf_gfpApprox : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {x : α} (hx : f x ≤ x),
  ↑(f.prevFixed x hx) = ⨅ a, OrdinalApprox.gfpApprox f x a
-- Mathlib.GroupTheory.Perm.Sign
/-- Like `swap_induction_on`, but with the composition on the right of `f`.

An induction principle for permutations. If `motive` holds for the identity permutation, and
is preserved under composition with a non-trivial swap, then `motive` holds for all permutations.  -/
Equiv.Perm.swap_induction_on' : ∀ {α : Type u} [inst : DecidableEq α] [Finite α] {motive : Equiv.Perm α → Prop} (f : Equiv.Perm α),
  motive 1 → (∀ (f : Equiv.Perm α) (x y : α), x ≠ y → motive f → motive (f * Equiv.swap x y)) → motive f
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.ProfunctorCore.map_rid_comp_map_lid_assoc : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) {X X' : C} {Y Y' : D} (f : X ⟶ X') (g : Y ⟶ Y')
  {Z : Type w} (h : P.obj X' Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (P.map f (CategoryTheory.CategoryStruct.id Y'))
      (CategoryTheory.CategoryStruct.comp (P.map (CategoryTheory.CategoryStruct.id X') g) h) =
    CategoryTheory.CategoryStruct.comp (P.map f g) h
-- Mathlib.MeasureTheory.Group.Measure
/-- If a left-invariant measure gives finite mass to a set with nonempty interior, then
it gives finite mass to any compact set.  -/
MeasureTheory.measure_lt_top_of_isCompact_of_isMulLeftInvariant' : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [IsTopologicalGroup G] [μ.IsMulLeftInvariant] {U : Set G},
  (interior U).Nonempty → μ U ≠ ⊤ → ∀ {K : Set G}, IsCompact K → μ K < ⊤
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- - `∑ x, f x` is notation for `Finset.sum Finset.univ f`. It is the sum of `f x`,
  where `x` ranges over the finite domain of `f`.
- `∑ x ∈ s, f x` is notation for `Finset.sum s f`. It is the sum of `f x`,
  where `x` ranges over the finite set `s` (either a `Finset` or a `Set` with a `Fintype` instance).
- `∑ x ∈ s with p x, f x` is notation for `Finset.sum (Finset.filter p s) f`.
- `∑ x ∈ s with h : p x, f x h` is notation for `Finset.sum s fun x ↦ if h : p x then f x h else 0`.
- `∑ (x ∈ s) (y ∈ t), f x y` is notation for `Finset.sum (s ×ˢ t) (fun ⟨x, y⟩ ↦ f x y)`.

These support destructuring, for example `∑ ⟨x, y⟩ ∈ s ×ˢ t, f x y`.

Notation: `"∑" bigOpBinders* (" with" (ident ":")? term)? "," term`  -/
BigOperators.bigsum : Lean.ParserDescr
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSub₂.measurable_sub : ∀ {G : Type u_2} {inst : MeasurableSpace G} {inst_1 : Sub G} [self : MeasurableSub₂ G], Measurable fun p => p.1 - p.2
-- Mathlib.Probability.Density
/-- X `HasPDF` if there is a pdf `f` such that `map X ℙ = μ.withDensity f`.  -/
MeasureTheory.hasPDF_of_map_eq_withDensity : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {x : MeasurableSpace Ω} {X : Ω → E}
  {ℙ : MeasureTheory.Measure Ω} {μ : MeasureTheory.Measure E},
  AEMeasurable X ℙ →
    ∀ (f : E → ENNReal), AEMeasurable f μ → MeasureTheory.Measure.map X ℙ = μ.withDensity f → MeasureTheory.HasPDF X ℙ μ
-- Mathlib.Topology.Algebra.Valued.WithVal
/-- The ring of integers of `WithVal v`, when `v` is a valuation on `ℚ`, is
equivalent to `ℤ`.  -/
Rat.ringOfIntegersWithValEquiv : {Γ₀ : Type u_2} →
  [inst : LinearOrderedCommGroupWithZero Γ₀] → (v : Valuation ℚ Γ₀) → NumberField.RingOfIntegers (WithVal v) ≃+* ℤ
-- Mathlib.Order.WithBot
/-- Lift a map `f : α → β` to `WithBot α → WithBot β`. Implemented using `Option.map`.  -/
WithBot.map : {α : Type u_1} → {β : Type u_2} → (α → β) → WithBot α → WithBot β
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_const_div_Ico : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => a / x) '' Set.Ico b c = Set.Ioc (a / c) (a / b)
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.distrib : {α : Type u} → [Mul α] → Distrib (FreeAbelianGroup α)
-- Lean.Meta.Sym.Canon
/-- `withCaching` + `canonInst'`  -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonInst : Lean.Expr → optParam Bool true → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.iso_homₚ_inv_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') (i : ι)
  {Z : CategoryTheory.Functor TopCat C} (h : HP'.H i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HP.iso i).hom
      (CategoryTheory.CategoryStruct.comp (TopPair.incl.whiskerLeft (f.homₚ i))
        (CategoryTheory.CategoryStruct.comp (HP'.iso i).inv h)) =
    CategoryTheory.CategoryStruct.comp (f.hom i) h
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instInv : {α : Type u_1} → [Inv α] → Inv (Colex α)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
hasSum_zero_iff : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [CanonicallyOrderedAdd α] [inst_4 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α},
  HasSum f 0 ↔ ∀ (x : ι), f x = 0
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet_obj_obj_coe : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] {J : CategoryTheory.CardinalDirectedPoset κ} (P : Set ↑J.obj → Prop)
  [inst_1 : ∀ (S : Subtype P), CategoryTheory.IsCardinalFiltered (↑↑S) κ] (X : Subtype P),
  ↑((CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet P).obj X).obj = ↑↑X
-- Mathlib.RingTheory.Derivation.Basic
Derivation.llcomp_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] {N : Type u_5}
  [inst_6 : AddCommMonoid N] [inst_7 : Module A N] [inst_8 : Module R N] [inst_9 : IsScalarTower R A M]
  [inst_10 : IsScalarTower R A N] (f : M →ₗ[A] N), Derivation.llcomp f = f.compDer
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.μ_natural_left : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  (F : CategoryTheory.Functor C D) [self : F.LaxMonoidal] {X Y : C} (f : X ⟶ Y) (X' : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (F.map f) (F.obj X'))
      (CategoryTheory.Functor.LaxMonoidal.μ F Y X') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxMonoidal.μ F X X')
      (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerRight f X'))