mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Nat.Factorial.Basic
Nat.descFactorial_self : ∀ (n : ℕ), n.descFactorial n = n.factorial
-- Mathlib.Topology.Homotopy.Lifting
/-- Two continuous maps from a preconnected space to the total space of a covering map
are homotopic relative to a set `S` if and only if their compositions with the covering map
are homotopic relative to `S`, assuming that they agree at a point in `S`.  -/
IsCoveringMap.homotopicRel_iff_comp : ∀ {E : Type u_1} {X : Type u_2} {A : Type u_3} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace A] {p : E → X} (cov : IsCoveringMap p) [PreconnectedSpace A] {f₀ f₁ : C(A, E)} {S : Set A},
  (∃ a ∈ S, f₀ a = f₁ a) →
    (f₀.HomotopicRel f₁ S ↔
      ({ toFun := p, continuous_toFun := ⋯ }.comp f₀).HomotopicRel ({ toFun := p, continuous_toFun := ⋯ }.comp f₁) S)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
/-- A Dirichlet character is odd if its value at -1 is -1.  -/
DirichletCharacter.Odd : {S : Type u_2} → [inst : CommRing S] → {m : ℕ} → DirichletCharacter S m → Prop
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Ici_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a : α) {c : α},
  c < 0 → (fun x => c * x) ⁻¹' Set.Ici a = Set.Iic (a / c)
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tmul_tensorComm_apply : ∀ {R : Type uR} {M₁ : Type uM₁} {M₂ : Type uM₂} [inst : CommRing R] [inst_1 : AddCommGroup M₁]
  [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] [inst_5 : Invertible 2]
  (Q₁ : QuadraticForm R M₁) (Q₂ : QuadraticForm R M₂) (x : TensorProduct R M₁ M₂),
  (Q₂.tmul Q₁) ((TensorProduct.comm R M₁ M₂) x) = (Q₁.tmul Q₂) x
-- Batteries.Tactic.HelpCmd
/-- The command `#help command` shows all commands that have been defined in the current environment.
See `#help cat` for more information.
 -/
Batteries.Tactic.«command#help_Command+____» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.forget_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.Mon C} (f : X ⟶ Y), (CategoryTheory.Mon.forget C).map f = f.hom
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.containsThenInsert_snd : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β},
  (t.containsThenInsert k v).2 = t.insert k v
-- Mathlib.GroupTheory.Subgroup.Center
/-- The center of an additive group `G` is the set of elements that commute with
everything in `G`  -/
AddSubgroup.center : (G : Type u_1) → [inst : AddGroup G] → AddSubgroup G
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.instSliceableImplRiiSlice : {α : Type u} →
  {β : α → Type v} → Std.Rii.Sliceable (Std.DTreeMap.Internal.Impl α β) α (Std.DTreeMap.Internal.RiiSlice α β)
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- A graph embedding induces an embedding of neighbor sets.  -/
SimpleGraph.Embedding.mapNeighborSet : {V : Type u_1} →
  {W : Type u_2} →
    {G : SimpleGraph V} → {G' : SimpleGraph W} → (f : G ↪g G') → (v : V) → ↑(G.neighborSet v) ↪ ↑(G'.neighborSet (f v))
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.T_add : ∀ {R : Type u_1} [inst : Semiring R] (m n : ℤ),
  LaurentPolynomial.T (m + n) = LaurentPolynomial.T m * LaurentPolynomial.T n
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Products
CategoryTheory.Over.prodLeftIsoPullback_hom_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (Y Z : CategoryTheory.Over X)
  [inst_1 : CategoryTheory.Limits.HasPullback Y.hom Z.hom] [inst_2 : CategoryTheory.Limits.HasBinaryProduct Y Z],
  CategoryTheory.CategoryStruct.comp (Y.prodLeftIsoPullback Z).hom (CategoryTheory.Limits.pullback.snd Y.hom Z.hom) =
    CategoryTheory.Over.Hom.left CategoryTheory.Limits.prod.snd
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `Submodule.projection_apply_of_mem_right`.

---

**Alias** of the reverse direction of `Submodule.projection_apply_eq_zero_iff`. -/
Submodule.IsCompl.projection_apply_of_mem_right : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q) {x : E}, x ∈ q → (p.projection q hpq) x = 0
-- Mathlib.Data.List.PeriodicityLemma
List.hasPeriod_zero : ∀ {α : Type u_1} (w : List α), w.HasPeriod 0
-- Mathlib.Data.Finset.Card
Finset.card_erase_le : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], (s.erase a).card ≤ s.card
-- Mathlib.CategoryTheory.ObjectProperty.Retract
CategoryTheory.ObjectProperty.IsStableUnderRetracts.instContainsZeroOfHasZeroObjectOfNonempty : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.IsStableUnderRetracts]
  [CategoryTheory.Limits.HasZeroObject C] [P.Nonempty], P.ContainsZero
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMonC_nc.eq_1 : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly) (c : ℕ),
  Lean.Grind.CommRing.Poly.mulMonC_nc k m p c =
    bif k % ↑c == 0 then Lean.Grind.CommRing.Poly.num 0
    else
      bif m == Lean.Grind.CommRing.Mon.unit then Lean.Grind.CommRing.Poly.mulConstC (k % ↑c) p c
      else Lean.Grind.CommRing.Poly.mulMonC_nc.go k m c p (Lean.Grind.CommRing.Poly.num 0)
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.equivInfinitePlace_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K]
  (w : NumberField.InfinitePlace K),
  (NumberField.IsCMField.equivInfinitePlace K) w = w.comap (algebraMap (↥(NumberField.maximalRealSubfield K)) K)
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.instAlternativeTacticM : Alternative Lean.Elab.Tactic.TacticM
-- Init.Data.Range.Polymorphic.Internal.SignedBitVec
_private.Init.Data.Range.Polymorphic.Internal.SignedBitVec.0.BitVec.Signed.instLawfulUpwardEnumerableLE : ∀ {n : ℕ}, Std.PRange.LawfulUpwardEnumerableLE (BitVec n)
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- The carrier of `H ⊔ N` is just `↑H * ↑N` (pointwise set product)
when `H` is a subgroup of the normalizer of `N` in `G`.  -/
Subgroup.coe_mul_of_left_le_normalizer_right : ∀ {G : Type u_2} [inst : Group G] (H N : Subgroup G), H ≤ Subgroup.normalizer ↑N → ↑(H ⊔ N) = ↑H * ↑N
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientAddGroup.mk'.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (N : AddSubgroup G) [nN : N.Normal],
  QuotientAddGroup.mk' N = AddMonoidHom.mk' QuotientAddGroup.mk ⋯
-- Init.Data.List.Impl
List.filterMapTR.go.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (f : α → Option β) (a : Array β), List.filterMapTR.go f [] a = a.toList
-- Init.Data.SInt.Lemmas
Int8.ofInt_toInt : ∀ (x : Int8), Int8.ofInt x.toInt = x
-- Mathlib.Order.Restriction
Preorder.frestrictLe₂_apply : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] {a b : α} (hab : a ≤ b)
  (f : (i : ↥(Finset.Iic b)) → π ↑i) (i : ↥(Finset.Iic a)), Preorder.frestrictLe₂ hab f i = f ⟨↑i, ⋯⟩
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Uniform
SimpleGraph.not_isUniform_zero : ∀ {α : Type u_1} {𝕜 : Type u_2} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {G : SimpleGraph α}
  [inst_3 : DecidableRel G.Adj] {s t : Finset α}, ¬G.IsUniform 0 s t
-- Mathlib.Data.W.Constructions
WType.NatαEquivPUnitSumPUnit_apply : ∀ (c : WType.Natα),
  WType.NatαEquivPUnitSumPUnit c =
    match c with
    | WType.Natα.zero => Sum.inl PUnit.unit
    | WType.Natα.succ => Sum.inr PUnit.unit
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_inj_iff : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂]
  {f g : NormedAddGroupHom V₁ V₂}, f = g ↔ ⇑f = ⇑g
-- Mathlib.CategoryTheory.Limits.Final
/-- We provide an induction principle for reasoning about `lift` and `homToLift`.
We want to perform some construction (usually just a proof) about
the particular choices `lift F d` and `homToLift F d`,
it suffices to perform that construction for some other pair of choices
(denoted `X₀ : C` and `k₀ : F.obj X₀ ⟶ d` below),
and to show how to transport such a construction
*both* directions along a morphism between such choices.
 -/
CategoryTheory.Functor.Initial.induction : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : F.Initial] →
            {d : D} →
              (Z : (X : C) → (F.obj X ⟶ d) → Sort u_1) →
                ((X₁ X₂ : C) →
                    (k₁ : F.obj X₁ ⟶ d) →
                      (k₂ : F.obj X₂ ⟶ d) →
                        (f : X₁ ⟶ X₂) → CategoryTheory.CategoryStruct.comp (F.map f) k₂ = k₁ → Z X₁ k₁ → Z X₂ k₂) →
                  ((X₁ X₂ : C) →
                      (k₁ : F.obj X₁ ⟶ d) →
                        (k₂ : F.obj X₂ ⟶ d) →
                          (f : X₁ ⟶ X₂) → CategoryTheory.CategoryStruct.comp (F.map f) k₂ = k₁ → Z X₂ k₂ → Z X₁ k₁) →
                    {X₀ : C} →
                      {k₀ : F.obj X₀ ⟶ d} →
                        Z X₀ k₀ →
                          Z (CategoryTheory.Functor.Initial.lift F d) (CategoryTheory.Functor.Initial.homToLift F d)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C),
  (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).obj A =
    CategoryTheory.LaxMonoidalFunctor.of (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidalObj A)
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.Builder.assertShared : Lean.Expr → Lean.Meta.Sym.Internal.AlphaShareBuilderM Unit
-- Mathlib.Algebra.MonoidAlgebra.Cardinal
/-- **Alias** of `MonoidAlgebra.cardinalMk_eq_lift_of_fintype`. -/
MonoidAlgebra.cardinalMk_lift_of_fintype : ∀ (R : Type u) (M' : Type v) [inst : Semiring R] [inst_1 : Fintype M'],
  Cardinal.mk (MonoidAlgebra R M') = Cardinal.lift.{v, u} (Cardinal.mk R) ^ Fintype.card M'
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.iUnion_spanningSets : ∀ {α : Type u_1} {m0 : MeasurableSpace α} (μ : MeasureTheory.Measure α) [inst : MeasureTheory.SigmaFinite μ],
  ⋃ i, MeasureTheory.spanningSets μ i = Set.univ
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_zero_add : ∀ (R : Type u_1) {V : Type u_2} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  (x y : V), midpoint R 0 (x + y) = midpoint R x y
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosSemidef.one : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  [inst_4 : DecidableEq n], Matrix.PosSemidef 1
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.forget₂_ringCat_map : ∀ (R : Type u) [inst : CommRing R] {X Y : AlgCat R} (f : X ⟶ Y),
  (CategoryTheory.forget₂ (AlgCat R) RingCat).map f = RingCat.ofHom ↑(AlgCat.Hom.hom f)
-- Init.Data.List.Nat.TakeDrop
List.getLast_take : ∀ {α : Type u_1} {i : ℕ} {l : List α} (h : List.take i l ≠ []), (List.take i l).getLast h = l[i - 1]?.getD (l.getLast ⋯)
-- Mathlib.Topology.Homeomorph.Lemmas
Homeomorph.finTwoArrow_apply : ∀ {X : Type u_1} [inst : TopologicalSpace X], ⇑Homeomorph.finTwoArrow = fun f => (f 0, f 1)
-- Mathlib.Order.Lattice
inf_le_right : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, a ⊓ b ≤ b
-- Mathlib.Logic.Equiv.Set
Equiv.prod_assoc_symm_preimage : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Set α} {t : Set β} {u : Set γ},
  ⇑(Equiv.prodAssoc α β γ).symm ⁻¹' (s ×ˢ t) ×ˢ u = s ×ˢ t ×ˢ u
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformly.inv` -/
TendstoUniformly.fun_inv : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f : ι → β → α} {g : β → α},
  TendstoUniformly f g l → TendstoUniformly (fun i i_1 => (f i i_1)⁻¹) (fun i => (g i)⁻¹) l
-- Mathlib.Topology.Inseparable
SeparationQuotient.map_prod_map_mk_nhds : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (x : X) (y : Y),
  Filter.map (Prod.map SeparationQuotient.mk SeparationQuotient.mk) (nhds (x, y)) =
    nhds (SeparationQuotient.mk x, SeparationQuotient.mk y)
-- Mathlib.Data.Tree.Basic
BinaryTree.brecOn.eq : ∀ {α : Type u} {motive : BinaryTree α → Sort u_1} (t : BinaryTree α)
  (F_1 : (t : BinaryTree α) → BinaryTree.below t → motive t),
  BinaryTree.brecOn t F_1 = F_1 t (BinaryTree.brecOn.go t F_1).2
-- Mathlib.Analysis.Complex.Basic
Complex.ofNat_mem_slitPlane : ∀ (n : ℕ) [inst : n.AtLeastTwo], OfNat.ofNat n ∈ Complex.slitPlane
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- A kernel of `f - g` is an equalizer of `f` and `g`.  -/
CategoryTheory.Preadditive.isLimitForkOfKernelFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {X Y : C} →
        {f g : X ⟶ Y} →
          {c : CategoryTheory.Limits.KernelFork (f - g)} →
            CategoryTheory.Limits.IsLimit c →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Preadditive.forkOfKernelFork c)
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.packingNumber_empty : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] (ε : NNReal), Metric.packingNumber ε ∅ = 0
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_greatest : ∀ {α : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {a b d : α},
  d ∣ a → d ∣ b → (∀ (e : α), e ∣ a → e ∣ b → e ∣ d) → gcd a b = normalize d
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go.eq_1 : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (best : Option (α × β)),
  Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go k best Std.DTreeMap.Internal.Impl.leaf = best
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsLimit.conePointUniqueUpToIso_hom_comp : ∀ {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.Cone F} (P : CategoryTheory.Limits.IsLimit s)
  (Q : CategoryTheory.Limits.IsLimit t) (j : J),
  CategoryTheory.CategoryStruct.comp (P.conePointUniqueUpToIso Q).hom (t.π.app j) = s.π.app j
-- Mathlib.Data.Set.Prod
Set.graphOn_eq_empty : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β}, Set.graphOn f s = ∅ ↔ s = ∅
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrix'_mul : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} [inst_1 : Fintype m] [inst_2 : DecidableEq m]
  (f g : (m → R) →ₗ[R] m → R), LinearMap.toMatrix' (f * g) = LinearMap.toMatrix' f * LinearMap.toMatrix' g
-- Mathlib.CategoryTheory.Monoidal.Ring
CategoryTheory.CommRingObjCat.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} {X : C} {commRingObj : CategoryTheory.CommRingObj X} {X_1 : C}
  {commRingObj_1 : CategoryTheory.CommRingObj X_1},
  { X := X, commRingObj := commRingObj } = { X := X_1, commRingObj := commRingObj_1 } →
    X = X_1 ∧ commRingObj ≍ commRingObj_1
-- Mathlib.RingTheory.HahnSeries.Multiplication
HahnSeries.single_zero_intCast : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero Γ] [inst_1 : PartialOrder Γ] [inst_2 : Zero R] [inst_3 : IntCast R]
  (z : ℤ), (HahnSeries.single 0) ↑z = ↑z
-- Init.Data.Iterators.Consumers.Monadic.Access
/-- Returns the step in which `it` yields its `n`-th element, or `.done` if it terminates earlier.
In contrast to `step`, this function will always return either `.yield` or `.done` but never a
`.skip` step.

For monadic iterators, the monadic effects of this operation may differ from manually iterating
to the `n`-th value because `nextAtIdx?` can take shortcuts. By the signature, the return value
is guaranteed to plausible in the sense of `IterM.IsPlausibleNthOutputStep`.

This function is only available for iterators that explicitly support it by implementing
the `IteratorAccess` typeclass.
 -/
Std.IterM.nextAtIdx? : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] →
        [Std.IteratorAccess α m] →
          (it : Std.IterM m β) → (n : ℕ) → m (Std.PlausibleIterStep (Std.IterM.IsPlausibleNthOutputStep n it))
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.toEquiv_symm : ∀ {G : Type u_1} {H : Type u_2} [inst : Add G] [inst_1 : Add H] {a : G} {b : H} (e : AddConstEquiv G H a b),
  e.symm.toEquiv = e.symm
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- For additive subgroups generated by a single element, see the simpler
`zsmul_induction_right`.  -/
AddSubgroup.closure_induction_right : ∀ {G : Type u_2} [inst : AddGroup G] {s : Set G} {p : (x : G) → x ∈ AddSubgroup.closure s → Prop},
  p 0 ⋯ →
    (∀ (x : G) (hx : x ∈ AddSubgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x + y) ⋯) →
      (∀ (x : G) (hx : x ∈ AddSubgroup.closure s) (y : G) (hy : y ∈ s), p x hx → p (x + -y) ⋯) →
        ∀ {x : G} (h : x ∈ AddSubgroup.closure s), p x h
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.rid_apply : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_4} [inst : CommSemiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] (σ : Representation A G W) (w : W) (a : A),
  (Representation.TensorProduct.rid A σ) (w ⊗ₜ[A] a) = a • w
-- Mathlib.Data.Set.Lattice
iSup_sUnion : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice β] (S : Set (Set α)) (f : α → β),
  ⨆ x ∈ ⋃₀ S, f x = ⨆ s ∈ S, ⨆ x ∈ s, f x
-- Mathlib.Analysis.PSeries
sum_Ioc_inv_sq_le_sub : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {k n : ℕ},
  k ≠ 0 → k ≤ n → ∑ i ∈ Finset.Ioc k n, (↑i ^ 2)⁻¹ ≤ (↑k)⁻¹ - (↑n)⁻¹
-- Mathlib.MeasureTheory.Function.Jacobian
/-- Change of variable formula for differentiable functions: if a function `f` is
injective and differentiable on a measurable set `s`, then the Lebesgue integral of a function
`g : E → ℝ≥0∞` on `f '' s` coincides with the integral of `|(f' x).det| * g ∘ f` on `s`.
Note that the measurability of `f '' s` is given by `measurable_image_of_fderivWithin`.  -/
MeasureTheory.lintegral_image_eq_lintegral_abs_det_fderiv_mul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasurableSet s →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) →
      Set.InjOn f s →
        ∀ (g : E → ENNReal), ∫⁻ (x : E) in f '' s, g x ∂μ = ∫⁻ (x : E) in s, ENNReal.ofReal |(f' x).det| * g (f x) ∂μ
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.intCast_def : ∀ {R : Type u_1} {M : Type u_4} [inst : Ring R] [inst_1 : MulOneClass M] (z : ℤ), ↑z = MonoidAlgebra.single 1 ↑z
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.Splits.of_eq : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ t₃ t₄ : String}, p.Splits t₁ t₂ → t₁ = t₃ → t₂ = t₄ → p.Splits t₃ t₄
-- Mathlib.Topology.Separation.CompletelyRegular
NormalSpace.instCompletelyRegularSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [NormalSpace X] [R0Space X], CompletelyRegularSpace X
-- Mathlib.MeasureTheory.Measure.Doubling
IsUnifLocDoublingMeasure.eventually_measure_le_scaling_constant_mul : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ] (K : ℝ),
  ∀ᶠ (r : ℝ) in nhdsWithin 0 (Set.Ioi 0),
    ∀ (x : α),
      μ (Metric.closedBall x (K * r)) ≤ ↑(IsUnifLocDoublingMeasure.scalingConstantOf μ K) * μ (Metric.closedBall x r)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The map `K.cycles i ⟶ L.cycles i` induced by a morphism in `HomologicalComplex`.  -/
HomologicalComplex.cyclesMap : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {K L : HomologicalComplex C c} →
            (K ⟶ L) → (i : ι) → [inst_2 : K.HasHomology i] → [inst_3 : L.HasHomology i] → K.cycles i ⟶ L.cycles i
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- A refl prefunctor `V ⥤rq W` induces a functor `FreeRefl V ⥤ FreeRefl W` defined using
`freeMap` and the quotient functor.  -/
CategoryTheory.Cat.freeReflMap : {V : Type u_1} →
  [inst : CategoryTheory.ReflQuiver V] →
    {W : Type u_2} →
      [inst_1 : CategoryTheory.ReflQuiver W] →
        V ⥤rq W → CategoryTheory.Functor (CategoryTheory.Cat.FreeRefl V) (CategoryTheory.Cat.FreeRefl W)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- Applying `AffineMap.lineMap` on two `Finset.affineCombination` over the same set of points
is equivalent to applying `AffineMap.lineMap` to the weights.  -/
Finset.lineMap_affineCombination : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w₁ w₂ : ι → k) (r : k) (p : ι → P),
  (AffineMap.lineMap ((Finset.affineCombination k s p) w₁) ((Finset.affineCombination k s p) w₂)) r =
    (Finset.affineCombination k s p) ((AffineMap.lineMap w₁ w₂) r)
-- Mathlib.Algebra.Group.Units.Opposite
IsUnit.unop : ∀ {M : Type u_2} [inst : Monoid M] {m : Mᵐᵒᵖ}, IsUnit m → IsUnit (MulOpposite.unop m)
-- Mathlib.LinearAlgebra.Complex.Module
Complex.reLm_coe : ⇑Complex.reLm = Complex.re
-- Mathlib.LinearAlgebra.RootSystem.Chain
RootPairing.chainBotCoeff_reflectionPerm_right : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Finite ι] [inst_1 : CommRing R]
  [inst_2 : CharZero R] [inst_3 : IsDomain R] [inst_4 : AddCommGroup M] [inst_5 : Module R M] [inst_6 : AddCommGroup N]
  [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsCrystallographic] {i j : ι},
  RootPairing.chainBotCoeff i ((P.reflectionPerm j) j) = RootPairing.chainTopCoeff i j
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.tendsto_translationNumber_of_dist_bounded_aux : ∀ (f : CircleDeg1Lift) (x : ℕ → ℝ) (C : ℝ),
  (∀ (n : ℕ), dist ((f ^ n) 0) (x n) ≤ C) →
    Filter.Tendsto (fun n => x (2 ^ n) / 2 ^ n) Filter.atTop (nhds f.translationNumber)
-- Mathlib.Probability.Decision.BayesEstimator
/-- The average risk of an estimator `κ` with respect to a prior `π` can be expressed as
an integral in the following way: `R_π(κ) = ((P†π × κ) ∘ P ∘ π)[(θ, y) ↦ ℓ θ y]`.  -/
ProbabilityTheory.avgRisk_eq_lintegral_posterior_prod : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [inst : StandardBorelSpace Θ] [inst_1 : Nonempty Θ],
  Measurable (Function.uncurry ℓ) →
    ∀ (P : ProbabilityTheory.Kernel Θ 𝓧) [inst_2 : ProbabilityTheory.IsFiniteKernel P]
      (κ : ProbabilityTheory.Kernel 𝓧 𝓨) [ProbabilityTheory.IsSFiniteKernel κ] (π : MeasureTheory.Measure Θ)
      [inst_4 : MeasureTheory.IsFiniteMeasure π],
      ProbabilityTheory.avgRisk ℓ P κ π =
        ∫⁻ (θy : Θ × 𝓨), ℓ θy.1 θy.2 ∂(π.bind ⇑P).bind ⇑((ProbabilityTheory.posterior P π).prod κ)
-- Mathlib.Order.Partition.Basic
/-- Noncomputably choose a representative from an equivalence class.  -/
Partition.rep : {α : Type u_1} → {u t : Set α} → (P : Partition u) → t ∈ P → α
-- Init.Data.Vector.Lemmas
Vector.getElem_cast : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {h : n = m} {i : ℕ} (hi : i < m), (Vector.cast h xs)[i] = xs[i]
-- Mathlib.AlgebraicGeometry.QuasiAffine
/-- If `f : X ⟶ Y` is an affine morphism between quasi-affine schemes, then it is the pullback of
`Spec Γ(X, ⊤) ⟶ Spec Γ(Y, ⊤)` along the open immersion `Y ⟶ Spec Γ(Y, ⊤)`.  -/
AlgebraicGeometry.Scheme.isPullback_toSpecΓ_toSpecΓ : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffineHom f] [Y.IsQuasiAffine],
  CategoryTheory.IsPullback f X.toSpecΓ Y.toSpecΓ (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.Hom.appTop f))