mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.Pell
/-- The map sending an integer `n` to the `y`-coordinate of `a^n` for a fundamental
solution `a` is strictly increasing.  -/
Pell.IsFundamental.y_strictMono : ∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → StrictMono fun n => (a ^ n).y
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.exists_root_eq_sum_int : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [CharZero R] (i : ι),
  ∃ f, Function.support f ⊆ ↑b.support ∧ (0 < f ∨ f < 0) ∧ P.root i = ∑ j ∈ b.support, f j • P.root j
-- Mathlib.Topology.ContinuousMap.Bounded.Star
/-- The right-hand side of this equality can be parsed `star ∘ ⇑f` because of the
instance `Pi.instStarForAll`. Upon inspecting the goal, one sees `⊢ ↑(star f) = star ↑f`.  -/
BoundedContinuousFunction.coe_star : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β] [inst_2 : StarAddMonoid β]
  [inst_3 : NormedStarGroup β] (f : BoundedContinuousFunction α β), ⇑(star f) = star ⇑f
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.natEnd.match_1.eq_2 : ∀ (motive : Turing.PartrecToTM2.Γ' → Sort u_1) (h_1 : Unit → motive Turing.PartrecToTM2.Γ'.consₗ)
  (h_2 : Unit → motive Turing.PartrecToTM2.Γ'.cons) (h_3 : (x : Turing.PartrecToTM2.Γ') → motive x),
  (match Turing.PartrecToTM2.Γ'.cons with
    | Turing.PartrecToTM2.Γ'.consₗ => h_1 ()
    | Turing.PartrecToTM2.Γ'.cons => h_2 ()
    | x => h_3 x) =
    h_2 ()
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- A functor `F` preserves biproducts of `f` if `F` maps every bilimit bicone over `f` to a
bilimit bicone over `F.obj ∘ f`.  -/
CategoryTheory.Limits.isBilimitOfPreserves : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            {J : Type w₁} →
              {f : J → C} →
                (F : CategoryTheory.Functor C D) →
                  [inst_4 : F.PreservesZeroMorphisms] →
                    [CategoryTheory.Limits.PreservesBiproduct f F] →
                      {b : CategoryTheory.Limits.Bicone f} → b.IsBilimit → (F.mapBicone b).IsBilimit
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.length_alterKey' : ∀ {α : Type u} [inst : BEq α] {β : Type v} {k : α} {f : Option β → Option β} {l : List ((_ : α) × β)},
  (Std.Internal.List.Const.alterKey k f l).length =
    if Std.Internal.List.containsKey k l = true ∧ (f (Std.Internal.List.getValue? k l)).isNone = true then l.length - 1
    else
      if Std.Internal.List.containsKey k l = false ∧ (f (Std.Internal.List.getValue? k l)).isSome = true then
        l.length + 1
      else l.length
-- Mathlib.Topology.Order.LiminfLimsup
Filter.Tendsto.bddAbove_range_of_cofinite : ∀ {ι : Type u_1} {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedLENhdsClass α] {u : ι → α}
  {a : α} [IsDirectedOrder α], Filter.Tendsto u Filter.cofinite (nhds a) → BddAbove (Set.range u)
-- Mathlib.MeasureTheory.Integral.Layercake
/-- The standard case of the layer cake formula / Cavalieri's principle / tail probability formula:

For an integrable a.e.-nonnegative real-valued function `f`, the Bochner integral of `f` can be
written (roughly speaking) as: `∫ f ∂μ = ∫ t in 0..∞, μ {ω | f(ω) > t}`.

See `MeasureTheory.lintegral_eq_lintegral_meas_lt` for a version with Lebesgue integral `∫⁻`
instead.  -/
MeasureTheory.Integrable.integral_eq_integral_meas_lt : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ → 0 ≤ᵐ[μ] f → ∫ (ω : α), f ω ∂μ = ∫ (t : ℝ) in Set.Ioi 0, μ.real {a | t < f a}
-- Mathlib.Data.ZMod.Basic
pow_pow_zmod_val_inv : ∀ {α : Type u_1} [inst : Group α] {n : ℕ}, (Nat.card α).gcd n = 1 → ∀ (a : α), (a ^ n) ^ (↑n)⁻¹.val = a
-- Mathlib.Data.Rel
SetRel.isTrans_iInter : ∀ {α : Type u_1} {ι : Sort u_5} {R : ι → SetRel α α} [∀ (i : ι), (R i).IsTrans], SetRel.IsTrans (⋂ i, R i)
-- Mathlib.RingTheory.MatrixAlgebra
/-- `Matrix.kroneckerTMul` as an algebra equivalence, when the two arguments are tensored.  -/
Matrix.kroneckerTMulAlgEquiv : (m : Type u_2) →
  (n : Type u_3) →
    (R : Type u_5) →
      (S : Type u_6) →
        (A : Type u_7) →
          (B : Type u_8) →
            [inst : CommSemiring R] →
              [inst_1 : Semiring A] →
                [inst_2 : Semiring B] →
                  [inst_3 : Algebra R A] →
                    [inst_4 : Algebra R B] →
                      [inst_5 : Fintype n] →
                        [inst_6 : DecidableEq n] →
                          [inst_7 : CommSemiring S] →
                            [inst_8 : Algebra R S] →
                              [inst_9 : Algebra S A] →
                                [inst_10 : IsScalarTower R S A] →
                                  [inst_11 : Fintype m] →
                                    [inst_12 : DecidableEq m] →
                                      TensorProduct R (Matrix m m A) (Matrix n n B) ≃ₐ[S]
                                        Matrix (m × n) (m × n) (TensorProduct R A B)
-- Mathlib.Data.Complex.Basic
Complex.sub_re : ∀ (z w : ℂ), (z - w).re = z.re - w.re
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.mk : {R : Type u} →
  {M : Type v} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          (toAddSubmonoid : AddSubmonoid M) →
            (∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier) → Submodule R M
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.insert_eq : ∀ (x y : ZFSet.{u_1}), insert x y = {x} ∪ y
-- Lean.LibrarySuggestions.Basic
/-- Attribute for registering library suggestions selectors.  -/
Lean.LibrarySuggestions.librarySuggestionsAttr : Lean.TagAttribute
-- Lean.Class
Lean.ClassState.outParamMap : Lean.ClassState → Lean.SMap Lean.Name (Array ℕ)
-- Mathlib.Algebra.Lie.Weights.Basic
/-- If `M` is a representation of a nilpotent Lie algebra `L`
and `χ : L → R` is a family of scalars,
then `genWeightSpace M χ` is the intersection of the maximal generalized `χ x`-eigenspaces
of the action of `x` on `M` as `x` ranges over `L`.

It is a Lie submodule because `L` is nilpotent.  -/
LieModule.genWeightSpace : {R : Type u_2} →
  {L : Type u_3} →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] →
                [inst_5 : LieRingModule L M] →
                  [LieModule R L M] → [LieRing.IsNilpotent L] → (L → R) → LieSubmodule R L M
-- Mathlib.Analysis.LocallyConvex.Separation
StrongDual.extendRCLikeₗ.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {F : Type u_2} [inst_1 : TopologicalSpace F] [inst_2 : AddCommGroup F]
  [inst_3 : Module 𝕜 F] [inst_4 : ContinuousConstSMul 𝕜 F] [inst_5 : Module ℝ F] [inst_6 : IsScalarTower ℝ 𝕜 F],
  StrongDual.extendRCLikeₗ = StrongDual.extendRCLikeₗ
-- Init.Data.String.Subslice
/-- A region or slice of a fixed slice.

Given a `Slice` `s`, the type `s.Subslice` is the type of half-open regions
in `s` delineated by a valid position on both sides.

This type is useful to track regions of interest within some larger slice that is also of interest.
In contrast, `Slice` is used to track regions of interest within some larger string that is
not or no longer relevant.

Equality on `Subslice` is somewhat better behaved than on `Slice`, but note that there
will in general be many different representations of the empty subslice of a slice.
 -/
String.Slice.Subslice : String.Slice → Type
-- Mathlib.CategoryTheory.Limits.Shapes.Grothendieck
/-- For a functor `G : Grothendieck F ⥤ H`, every cocone over `fiberwiseColimit G` induces a
cocone over `G` itself.  -/
CategoryTheory.Limits.coconeOfCoconeFiberwiseColimit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      {H : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} H] →
          {G : CategoryTheory.Functor (CategoryTheory.Grothendieck F) H} →
            [inst_2 :
                ∀ {X Y : C} (f : X ⟶ Y),
                  CategoryTheory.Limits.HasColimit
                    ((F.map f).toFunctor.comp ((CategoryTheory.Grothendieck.ι F Y).comp G))] →
              CategoryTheory.Limits.Cocone (CategoryTheory.Limits.fiberwiseColimit G) → CategoryTheory.Limits.Cocone G
-- Mathlib.Algebra.Lie.Abelian
LieIdeal.isLieAbelian_iff : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {I : LieIdeal R L},
  IsLieAbelian ↥I ↔ I ≤ LieModule.ker R L ↥I
-- Std.Data.TreeMap.Slice
Std.TreeMap.toList_ric : ∀ {α : Type u} {β : Type v} (cmp : autoParam (α → α → Ordering) Std.TreeMap.toList_ric._auto_1) [Std.TransCmp cmp]
  {t : Std.TreeMap α β cmp} {bound : α},
  Std.Slice.toList (Std.Ric.Sliceable.mkSlice t *...=bound) = List.filter (fun e => (cmp e.1 bound).isLE) t.toList
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- Given morphisms `a : W ⟶ Y` and `b : W ⟶ Z` satisfying `a ≫ f = b ≫ g`,
constructs the unique morphism `W ⟶ pullbackObj f g` which lifts `a` and `b`.  -/
CategoryTheory.ChosenPullbacksAlong.lift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Y Z X : C} →
      {f : Y ⟶ X} →
        {g : Z ⟶ X} →
          [inst_1 : CategoryTheory.ChosenPullbacksAlong g] →
            {W : C} →
              (a : W ⟶ Y) →
                (b : W ⟶ Z) →
                  autoParam (CategoryTheory.CategoryStruct.comp a f = CategoryTheory.CategoryStruct.comp b g)
                      _auto_75✝ →
                    (W ⟶ CategoryTheory.ChosenPullbacksAlong.pullbackObj f g)
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.aemeasurable_fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {f : α → γ} {g : β → γ}
  {μ : autoParam (MeasureTheory.Measure α) ProbabilityTheory.IdentDistrib._auto_1}
  {ν : autoParam (MeasureTheory.Measure β) ProbabilityTheory.IdentDistrib._auto_3},
  ProbabilityTheory.IdentDistrib f g μ ν → AEMeasurable f μ
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImportMetaKind.full.sizeOf_spec : sizeOf Lean.Lsp.LeanImportMetaKind.full = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Helper function for constructing morphisms between coequalizer coforks.
 -/
CategoryTheory.Limits.Cofork.mkHom : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {f g : X ⟶ Y} →
        {s t : CategoryTheory.Limits.Cofork f g} →
          (k : s.pt ⟶ t.pt) → CategoryTheory.CategoryStruct.comp s.π k = t.π → (s ⟶ t)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min?_erase_eq_of_not_compare_eq_min? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (∀ {km : α}, t.min? = some km → ¬cmp k km = Ordering.eq) → (t.erase k).min? = t.min?
-- Mathlib.Tactic.Widget.StringDiagram
/-- The end point of the strand in the string diagram.  -/
Mathlib.Tactic.Widget.StringDiagram.Strand.endPoint : Mathlib.Tactic.Widget.StringDiagram.Strand → Mathlib.Tactic.Widget.StringDiagram.Node
-- Mathlib.Data.PNat.Prime
PNat.coprime_one : ∀ {n : ℕ+}, n.Coprime 1
-- Mathlib.Algebra.Lie.Extension
/-- The type of all Lie extensions of `M` by `N`.  That is, short exact sequences of `R`-Lie algebra
homomorphisms `0 → N → L → M → 0` where `R`, `M`, and `N` are fixed.  -/
LieAlgebra.Extension : (R : Type u_1) →
  (N : Type u_2) →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing N] →
          [LieAlgebra R N] → [inst_3 : LieRing M] → [LieAlgebra R M] → Type (max (max (max u_1 u_2) u_4) (u_5 + 1))
-- Mathlib.Order.SuccPred.Basic
Order.Icc_subset_Ico_succ_right_of_not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, ¬IsMax b → Set.Icc a b ⊆ Set.Ico a (Order.succ b)
-- Lean.Meta.Tactic.Grind.Action
/-- `x >> y`, executes `x` and then `y`
- If `x` is not applicable, then `x >> y` is not applicable.
- If `y` is not applicable, it behaves like a skip.
 -/
Lean.Meta.Grind.Action.andThen : Lean.Meta.Grind.Action → Lean.Meta.Grind.Action → Lean.Meta.Grind.Action
-- Lean.Meta.Tactic.Grind.Types
/-- Root (aka canonical representative) of the equivalence class  -/
Lean.Meta.Grind.ENode.root : Lean.Meta.Grind.ENode → Lean.Expr
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_unitOfList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α} {k : α}
  {fallback : Unit}, (Std.ExtHashMap.unitOfList l).getD k fallback = ()
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
/-- The linear isometry equivalence version of `TensorProduct.rid`.  -/
TensorProduct.ridIsometry : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → TensorProduct 𝕜 E 𝕜 ≃ₗᵢ[𝕜] E
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraQuaternion.equiv_apply : ∀ {R : Type u_1} [inst : CommRing R] {c₁ c₂ : R} (a : CliffordAlgebra (CliffordAlgebraQuaternion.Q c₁ c₂)),
  CliffordAlgebraQuaternion.equiv a = CliffordAlgebraQuaternion.toQuaternion a
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
/-- **Double counting** argument.

Considering `r` as a bipartite graph, the LHS is a lower bound on the number of edges while the RHS
is a strict upper bound.  -/
Finset.card_nsmul_lt_card_nsmul_of_le_of_lt' : ∀ {R : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [IsStrictOrderedRing R]
  (r : α → β → Prop) {s : Finset α} {t : Finset β} {m n : R} [inst_3 : (a : α) → (b : β) → Decidable (r a b)],
  s.Nonempty →
    (∀ b ∈ t, n ≤ ↑(Finset.bipartiteBelow r s b).card) →
      (∀ a ∈ s, ↑(Finset.bipartiteAbove r t a).card < m) → t.card • n < s.card • m
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.norm_inr : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A] (a : A), ‖↑a‖ = ‖a‖
-- Mathlib.LinearAlgebra.Eigenspace.Zero
LinearMap.charpoly_eq_X_pow_iff : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [IsDomain R] [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [inst_4 : Module.Finite R M] [inst_5 : Module.Free R M] [IsNoetherian R M] (φ : Module.End R M),
  LinearMap.charpoly φ = Polynomial.X ^ Module.finrank R M ↔ ∀ (m : M), ∃ n, (φ ^ n) m = 0
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.checkLinebreakBefore.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Dyadic.Basic
Dyadic.ofOdd.congr_simp : ∀ (n n_1 : ℤ) (e_n : n = n_1) (k k_1 : ℤ), k = k_1 → ∀ (hn : n % 2 = 1), Dyadic.ofOdd n k hn = Dyadic.ofOdd n_1 k_1 ⋯
-- Mathlib.NumberTheory.Dioph
Dioph.diophPFun_comp1 : ∀ {α : Type u} {S : Set (Option α → ℕ)},
  Dioph S → ∀ {f : (α → ℕ) →. ℕ}, Dioph.DiophPFun f → Dioph {v | ∃ (h : v ∈ f.Dom), Option.elim' (f.fn v h) v ∈ S}
-- Mathlib.Algebra.Group.Embedding
mulLeftEmbedding.eq_1 : ∀ {G : Type u_1} [inst : Mul G] [inst_1 : IsLeftCancelMul G] (g : G),
  mulLeftEmbedding g = { toFun := fun h => g * h, inj' := ⋯ }
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.self_le_maxKey!_insertIfNew! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {k : α} {v : β k}, (compare k (Std.DTreeMap.Internal.Impl.insertIfNew! k v t).maxKey!).isLE = true
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.divC : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  [Lean.Grind.NoNatZeroDivisors α] (p₁ : Lean.Grind.CommRing.Poly) (k : ℤ) (p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.div_certC p₁ k p c = true →
    Lean.Grind.CommRing.Poly.denote ctx p₁ = 0 → Lean.Grind.CommRing.Poly.denote ctx p = 0
-- Mathlib.NumberTheory.NumberField.Norm
Algebra.coe_norm_int : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.RingOfIntegers K),
  ↑((Algebra.norm ℤ) x) = (Algebra.norm ℚ) ↑x
-- Mathlib.Probability.Kernel.Disintegration.Basic
MeasureTheory.Measure.IsCondKernel.isMarkovKernel : ∀ {α : Type u_1} {Ω : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω} (ρ : MeasureTheory.Measure (α × Ω))
  (ρCond : ProbabilityTheory.Kernel α Ω) [ρ.IsCondKernel ρCond] [MeasureTheory.IsFiniteMeasure ρ]
  [MeasurableSingletonClass α], (∀ (a : α), ρ.fst {a} ≠ 0) → ProbabilityTheory.IsMarkovKernel ρCond
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.coe_prodMap : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {C : Type u_4} [inst_7 : Semiring C] [inst_8 : Algebra R C] [inst_9 : TopologicalSpace C] {D : Type u_5}
  [inst_10 : Semiring D] [inst_11 : TopologicalSpace D] [inst_12 : Algebra R D] (f₁ : A →A[R] B) (f₂ : C →A[R] D),
  ↑(f₁.prodMap f₂) = (↑f₁).prodMap ↑f₂
-- Mathlib.Algebra.Module.Hom
AddMonoid.End.isCentralScalar : ∀ {R : Type u_1} {A : Type u_4} [inst : Monoid R] [inst_1 : AddCommMonoid A] [inst_2 : DistribMulAction R A]
  [inst_3 : DistribMulAction Rᵐᵒᵖ A] [IsCentralScalar R A], IsCentralScalar R (AddMonoid.End A)
-- Mathlib.RepresentationTheory.Intertwining
Representation.TensorProduct.comm_comp_lTensor : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : CommSemiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : AddCommMonoid U] [inst_5 : Module A V]
  [inst_6 : Module A W] [inst_7 : Module A U] (ρ : Representation A G V) (σ : Representation A G W)
  (τ : Representation A G U) (f : σ.IntertwiningMap τ),
  (↑(Representation.TensorProduct.comm ρ τ)).comp (Representation.IntertwiningMap.lTensor ρ f) =
    (Representation.IntertwiningMap.rTensor ρ f).comp ↑(Representation.TensorProduct.comm ρ σ)
-- Mathlib.LinearAlgebra.BilinearForm.Properties
LinearMap.BilinForm.isRefl_neg : ∀ {R₁ : Type u_3} {M₁ : Type u_4} [inst : CommRing R₁] [inst_1 : AddCommGroup M₁] [inst_2 : Module R₁ M₁]
  {B : LinearMap.BilinForm R₁ M₁}, (-B).IsRefl ↔ B.IsRefl
-- Mathlib.Algebra.Ring.Divisibility.Lemmas
associated_abs_left_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : LinearOrder R] {x y : R}, Associated |x| y ↔ Associated x y
-- Mathlib.RingTheory.Congruence.Hom
/-- The **first isomorphism theorem for algebra morphisms**.  -/
RingCon.quotientKerEquivRangeₐ : {M : Type u_1} →
  {P : Type u_3} →
    {R : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring M] →
          [inst_2 : Algebra R M] →
            [inst_3 : Semiring P] → [inst_4 : Algebra R P] → (f : M →ₐ[R] P) → (RingCon.ker ↑f).Quotient ≃ₐ[R] ↥f.range
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.homEquiv_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y : C} (m₀ : M) (hm₀ : m₀ = 0) (f : X ⟶ Y),
  (CategoryTheory.ShiftedHom.homEquiv m₀ hm₀) f = CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ f
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.isCoverDense_of_generate_singleton_functor_π_mem : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (G : CategoryTheory.Functor C D)
  (K : CategoryTheory.GrothendieckTopology D),
  (∀ (B : D), ∃ X f, CategoryTheory.Sieve.generate (CategoryTheory.Presieve.singleton f) ∈ K B) → G.IsCoverDense K
-- Mathlib.Analysis.CStarAlgebra.Module.Constructions
WithCStarModule.max_le_prod_norm : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] {E : Type u_2} {F : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : Module ℂ E] [inst_4 : SMul A E] [inst_5 : NormedAddCommGroup F]
  [inst_6 : Module ℂ F] [inst_7 : SMul A F] [inst_8 : CStarModule A E] [inst_9 : CStarModule A F] [StarOrderedRing A]
  (x : WithCStarModule A (E × F)), max ‖x.1‖ ‖x.2‖ ≤ ‖x‖
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k a : α} {h' : a ∈ Std.DTreeMap.Internal.Impl.erase! k t},
  (Std.DTreeMap.Internal.Impl.erase! k t).get a h' = t.get a ⋯
-- Mathlib.Data.Fin.VecNotation
Matrix.range_cons_empty : ∀ {α : Type u} (x : α) (u : Fin 0 → α), Set.range (Matrix.vecCons x u) = {x}
-- Mathlib.CategoryTheory.CopyDiscardCategory.Basic
/-- Discard distributes over tensor.  -/
CategoryTheory.CopyDiscardCategory.discard_tensor : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.CopyDiscardCategory C] (X Y : C),
  CategoryTheory.ComonObj.counit =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.counit CategoryTheory.ComonObj.counit)
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.ComonadicityInternal.unitFork_π_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) (B : C)
  (X : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Comonad.ComonadicityInternal.unitFork adj B).π.app X =
    CategoryTheory.Limits.WalkingParallelPair.rec (motive := fun t =>
      X = t →
        (B ⟶
          (CategoryTheory.Limits.parallelPair (G.map (F.map (adj.unit.app B))) (adj.unit.app (G.obj (F.obj B)))).obj X))
      (fun h => ⋯ ▸ adj.unit.app B)
      (fun h => ⋯ ▸ CategoryTheory.CategoryStruct.comp (adj.unit.app B) (adj.unit.app (G.obj (F.obj B)))) X ⋯
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
/-- A topological space `X` is compactly generated if a set `s` is open when `f ⁻¹' s` is
open for every continuous map `f : K → X`, where `K` is compact Hausdorff.  -/
compactlyGeneratedSpace_of_isOpen : ∀ {X : Type u} [inst : TopologicalSpace X],
  (∀ (s : Set X),
      (∀ (K : Type u) [inst_1 : TopologicalSpace K] [CompactSpace K] [T2Space K] (f : K → X),
          Continuous f → IsOpen (f ⁻¹' s)) →
        IsOpen s) →
    CompactlyGeneratedSpace X
-- Std.Internal.UV.System
Std.Internal.UV.System.instInhabitedCPUTimes.default : Std.Internal.UV.System.CPUTimes
-- Mathlib.Data.ENat.Basic
ENat.add_one_le_iff' : ∀ {m n : ℕ∞}, n ≠ ⊤ → (m + 1 ≤ n ↔ m < n)
-- Mathlib.Topology.PartitionOfUnity
/-- Partition of unity defined by a `BumpCovering`. We use this auxiliary definition to prove some
properties of the new family of functions before bundling it into a `PartitionOfUnity`. Do not use
this definition, use `BumpCovering.toPartitionOfUnity` instead.

The partition of unity is given by the formula `g i x = f i x * ∏ᶠ j < i, (1 - f j x)`. In other
words, `g i x = ∏ᶠ j < i, (1 - f j x) - ∏ᶠ j ≤ i, (1 - f j x)`, so
`∑ᶠ i, g i x = 1 - ∏ᶠ j, (1 - f j x)`. If `x ∈ s`, then one of `f j x` equals one, hence the product
of `1 - f j x` vanishes, and `∑ᶠ i, g i x = 1`.

In order to avoid an assumption `LinearOrder ι`, we use `WellOrderingRel` instead of `(<)`.  -/
BumpCovering.toPOUFun : {ι : Type u} → {X : Type v} → [inst : TopologicalSpace X] → {s : Set X} → BumpCovering ι X s → ι → X → ℝ