mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.ColimitFunctor
PresheafOfModules.ModuleColimit.map_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.IsCofiltered C] [inst_3 : CategoryTheory.InitiallySmall C]
  {R : CategoryTheory.Functor Cᵒᵖ RingCat} {cR : CategoryTheory.Limits.Cocone R}
  (hcR : CategoryTheory.Limits.IsColimit cR) {M : PresheafOfModules R} {cM : CategoryTheory.Limits.Cocone M.presheaf}
  (hcM : CategoryTheory.Limits.IsColimit cM) {M' : PresheafOfModules R} {cM' : CategoryTheory.Limits.Cocone M'.presheaf}
  (hcM' : CategoryTheory.Limits.IsColimit cM') (f : M ⟶ M') {U : Cᵒᵖ} (m : ↑(M.obj U)),
  (PresheafOfModules.ModuleColimit.map hcR hcM hcM' f) (PresheafOfModules.ModuleColimit.ιM m) =
    PresheafOfModules.ModuleColimit.ιM ((CategoryTheory.ConcreteCategory.hom (f.app U)) m)
-- Mathlib.Analysis.InnerProductSpace.LinearMap
coe_innerSL_apply : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (v : E), ⇑((innerSL 𝕜) v) = fun w => inner 𝕜 v w
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
/-- Composition of continuous maps which map zero to zero.  -/
ContinuousMapZero.comp : {X : Type u_1} →
  {Y : Type u_2} →
    {R : Type u_3} →
      [inst : Zero X] →
        [inst_1 : Zero Y] →
          [inst_2 : Zero R] →
            [inst_3 : TopologicalSpace X] →
              [inst_4 : TopologicalSpace Y] →
                [inst_5 : TopologicalSpace R] → ContinuousMapZero Y R → ContinuousMapZero X Y → ContinuousMapZero X R
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivialization.prod.isLinear : ∀ (𝕜 : Type u_1) {B : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : TopologicalSpace B] {F₁ : Type u_3}
  [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_4}
  [inst_4 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_5} [inst_5 : NormedAddCommGroup F₂]
  [inst_6 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_6} [inst_7 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_8 : (x : B) → AddCommMonoid (E₁ x)] [inst_9 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_10 : (x : B) → AddCommMonoid (E₂ x)] [inst_11 : (x : B) → Module 𝕜 (E₂ x)]
  (e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj) (e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj)
  [Bundle.Trivialization.IsLinear 𝕜 e₁] [Bundle.Trivialization.IsLinear 𝕜 e₂],
  Bundle.Trivialization.IsLinear 𝕜 (e₁.prod e₂)
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.noMinOrder_Ioi : ∀ {α : Type u_1} {a : α} [inst : Preorder α], Order.IsPredPrelimit a → NoMinOrder ↑(Set.Ioi a)
-- Mathlib.Order.Monotone.Defs
Antitone.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β}, Antitone g → Antitone f → Monotone (g ∘ f)
-- Mathlib.Order.UpperLower.Basic
IsLowerSet.top_mem : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [inst_1 : OrderTop α], IsLowerSet s → (⊤ ∈ s ↔ s = Set.univ)
-- Mathlib.RingTheory.Finiteness.Cardinality
Module.not_finite_of_infinite_basis : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  {ι : Type u_3} [Infinite ι] (b : Module.Basis ι R M), ¬Module.Finite R M
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- The value of `χ₈ n`, for `n : ℕ`, depends only on `n % 8`.  -/
ZMod.χ₈_nat_mod_eight : ∀ (n : ℕ), ZMod.χ₈ ↑n = ZMod.χ₈ ↑(n % 8)
-- Std.Data.DTreeMap.Basic
/-- Modifies in place the value associated with a given key.

This function ensures that the value is used linearly.
 -/
Std.DTreeMap.modify : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.LawfulEqCmp cmp] → Std.DTreeMap α β cmp → (a : α) → (β a → β a) → Std.DTreeMap α β cmp
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.degreewiseEpiWithInjectiveKernel_p : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] (K L : CochainComplex C ℤ),
  CochainComplex.degreewiseEpiWithInjectiveKernel (CochainComplex.cm5b.p K L)
-- Mathlib.Data.Nat.Digits.Defs
Nat.digits_zero_succ : ∀ (n : ℕ), Nat.digits 0 n.succ = [n + 1]
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.comap_map_quotientMk : ∀ {R : Type u} [inst : Ring R] (I J : Ideal R) [inst_1 : I.IsTwoSided],
  Ideal.comap (Ideal.Quotient.mk I) (Ideal.map (Ideal.Quotient.mk I) J) = I ⊔ J
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.AddSubmonoidClass.IsHomogeneous.mem_iff : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] {P : Type u_5}
  [inst_5 : SetLike P M] [AddSubmonoidClass P M] (p : P),
  DirectSum.SetLike.IsHomogeneous ℳ p → ∀ {x : M}, x ∈ p ↔ ∀ (i : ι), ↑(((DirectSum.decompose ℳ) x) i) ∈ p
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.toIsScalarTower : ∀ {R : Type u_1} {A : Type u_2} {L : Type u_3} {inst : CommRing A} {inst_1 : LieRing L} {inst_2 : Module A L}
  {inst_3 : LieRingModule L A} {inst_4 : LieRinehartRing A L} {inst_5 : CommRing R} {inst_6 : Algebra R A}
  {inst_7 : LieAlgebra R L} [self : LieRinehartAlgebra R A L], IsScalarTower R A L
-- Mathlib.Data.List.Sublists
/-- **Alias** of the reverse direction of `List.nodup_sublists`. -/
List.Nodup.sublists : ∀ {α : Type u} {l : List α}, l.Nodup → l.sublists.Nodup
-- Mathlib.CategoryTheory.Bicategory.Kan.HasKan
CategoryTheory.Bicategory.lan.congr_simp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f f_1 : a ⟶ b) (e_f : f = f_1) (g g_1 : a ⟶ c)
  (e_g : g = g_1) [inst_1 : CategoryTheory.Bicategory.HasLeftKanExtension f g],
  CategoryTheory.Bicategory.lan f g = CategoryTheory.Bicategory.lan f_1 g_1
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.smallCategoryInitialModel : (J : Type u) →
  [inst : CategoryTheory.Category.{v, u} J] →
    [inst_1 : CategoryTheory.InitiallySmall J] → CategoryTheory.SmallCategory (CategoryTheory.InitialModel J)
-- Mathlib.Order.Hom.Bounded
/-- `TopHomClass F α β` states that `F` is a type of `⊤`-preserving morphisms.

You should extend this class when you extend `TopHom`.  -/
TopHomClass : (F : Type u_6) → (α : outParam (Type u_7)) → (β : outParam (Type u_8)) → [Top α] → [Top β] → [FunLike F α β] → Prop
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
SSet.Subcomplex.N.ext_iff : ∀ {X : SSet} {A : X.Subcomplex} (x y : A.N), x = y ↔ x.toN = y.toN
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.TriangleMorphism.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : SizeOf C] (hom₁ : T₁.obj₁ ⟶ T₂.obj₁)
  (hom₂ : T₁.obj₂ ⟶ T₂.obj₂) (hom₃ : T₁.obj₃ ⟶ T₂.obj₃)
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp T₁.mor₁ hom₂ = CategoryTheory.CategoryStruct.comp hom₁ T₂.mor₁)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₁._autoParam)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp T₁.mor₂ hom₃ = CategoryTheory.CategoryStruct.comp hom₂ T₂.mor₂)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₂._autoParam)
  (comm₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp T₁.mor₃ ((CategoryTheory.shiftFunctor C 1).map hom₁) =
        CategoryTheory.CategoryStruct.comp hom₃ T₂.mor₃)
      CategoryTheory.Pretriangulated.TriangleMorphism.comm₃._autoParam),
  sizeOf { hom₁ := hom₁, hom₂ := hom₂, hom₃ := hom₃, comm₁ := comm₁, comm₂ := comm₂, comm₃ := comm₃ } =
    1 + sizeOf hom₁ + sizeOf hom₂ + sizeOf hom₃ + sizeOf comm₁ + sizeOf comm₂ + sizeOf comm₃
-- Mathlib.Data.Complex.Basic
Complex.coe_reAddGroupHom : ⇑Complex.reAddGroupHom = Complex.re
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_iSup : ∀ {ι : Sort u_3} {f : ι → NNReal}, BddAbove (Set.range f) → ↑(iSup f) = ⨆ a, ↑(f a)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → γ} {k : α} {h' : k ∈ Std.ExtTreeMap.map f t}, (Std.ExtTreeMap.map f t).getKey k h' = t.getKey k ⋯
-- Mathlib.Analysis.Convex.Jensen
/-- **Maximum principle** for convex functions on an interval. If a function `f` is convex on the
interval `[x, y]`, then the eventual maximum of `f` on `[x, y]` is at `x` or `y`.  -/
ConvexOn.le_max_of_mem_Icc : ∀ {𝕜 : Type u_1} {β : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup β] [inst_4 : LinearOrder β] [IsOrderedAddMonoid β] [inst_6 : Module 𝕜 β]
  [IsStrictOrderedModule 𝕜 β] {s : Set 𝕜} {f : 𝕜 → β} {x y z : 𝕜},
  ConvexOn 𝕜 s f → x ∈ s → y ∈ s → z ∈ Set.Icc x y → f z ≤ max (f x) (f y)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ ∩ m₂},
  (m₁ ∩ m₂).get k h_mem = m₁.get k ⋯
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.instFaithfulCompPost : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {C : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C] (L : CategoryTheory.Functor A T) (R : CategoryTheory.Functor B T)
  (F : CategoryTheory.Functor T C), (CategoryTheory.Comma.post L R F).Faithful
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.toSubgroupEquiv_one : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B), HNNExtension.toSubgroupEquiv φ 1 = φ
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.coeff_sumAlgEquiv_apply_support : ∀ (R : Type u) (S₁ : Type v) (S₂ : Type w) [inst : CommSemiring R] (a : AddMonoidAlgebra R (S₁ ⊕ S₂ →₀ ℕ)),
  ((MvPolynomial.sumAlgEquiv R S₁ S₂) a).coeff.support =
    Finsupp.onFinsetSupport
      ((AddMonoidAlgebra.domCongr R R Finsupp.sumFinsuppAddEquivProdFinsupp) a).coeff.curry.support
      (⇑AddMonoidAlgebra.coeffAddEquiv.symm ∘
        ⇑((AddMonoidAlgebra.domCongr R R Finsupp.sumFinsuppAddEquivProdFinsupp) a).coeff.curry)
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.mk_mul_mk : ∀ {α : Type u_1} [inst : MulZeroClass α] [inst_1 : Preorder α] [inst_2 : PosMulMono α] {x y : α} (hx : 0 ≤ x)
  (hy : 0 ≤ y), ⟨x, hx⟩ * ⟨y, hy⟩ = ⟨x * y, ⋯⟩
-- Mathlib.Algebra.Module.ZLattice.Basic
/-- The fundamental domain of the ℤ-lattice spanned by `b`. See `ZSpan.isAddFundamentalDomain`
for the proof that it is a fundamental domain.  -/
ZSpan.fundamentalDomain : {E : Type u_1} →
  {ι : Type u_2} →
    {K : Type u_3} →
      [inst : NormedField K] →
        [inst_1 : NormedAddCommGroup E] → [inst_2 : NormedSpace K E] → Module.Basis ι K E → [LinearOrder K] → Set E
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic n K)` (in particular for `K = ℚ`), then the norm of
`ζ - 1` is `eval 1 (cyclotomic n ℤ)`.  -/
IsPrimitiveRoot.sub_one_norm_eq_eval_cyclotomic : ∀ {n : ℕ} [NeZero n] {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L],
  IsPrimitiveRoot ζ n →
    ∀ [IsCyclotomicExtension {n} K L],
      2 < n →
        Irreducible (Polynomial.cyclotomic n K) →
          (Algebra.norm K) (ζ - 1) = ↑(Polynomial.eval 1 (Polynomial.cyclotomic n ℤ))
-- Mathlib.Analysis.Convex.Between
Sbtw.right_mem_affineSpan : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] {x y z : P}, Sbtw R x y z → z ∈ line[R, x, y]
-- Mathlib.Algebra.Tropical.BigOperators
trop_sum : ∀ {R : Type u_1} {S : Type u_2} [inst : AddCommMonoid R] (s : Finset S) (f : S → R),
  Tropical.trop (∑ i ∈ s, f i) = ∏ i ∈ s, Tropical.trop (f i)
-- Batteries.Linter.UnreachableTactic
/-- Is this a syntax kind that contains intentionally unevaluated tactic subterms?  -/
Batteries.Linter.UnreachableTactic.isIgnoreTacticKind : Lean.NameHashSet → Lean.SyntaxNodeKind → Bool
-- Mathlib.Topology.Connected.PathConnected
/-- A set `F` is path connected if it contains a point that can be joined to all other in `F`.  -/
IsPathConnected : {X : Type u_1} → [TopologicalSpace X] → Set X → Prop
-- Batteries.Classes.Order
Std.LawfulLTCmp.compareOfLessAndEq_of_irrefl_of_trans_of_antisymm : ∀ {α : Type u_1} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : DecidableEq α],
  (∀ (x : α), ¬x < x) →
    (∀ {x y z : α}, x < y → y < z → x < z) →
      (∀ {x y : α}, ¬x < y → ¬y < x → x = y) → Std.LawfulLTCmp fun x1 x2 => compareOfLessAndEq x1 x2
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.Ici_mem_atTop : ∀ {α : Type u_3} [inst : Preorder α] (a : α), Set.Ici a ∈ Filter.atTop
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coprod_comp_inl : ∀ {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₂ ∘SL ContinuousLinearMap.inl R M₁ M₂ = f₁
-- Mathlib.NumberTheory.RamificationInertia.Basic
_private.Mathlib.NumberTheory.RamificationInertia.Basic.0.Ideal.termF : Lean.ParserDescr
-- Mathlib.GroupTheory.NoncommCoprod
/-- Variant of `AddHom.noncommCoprod_apply`, with the sum written in the other direction  -/
AddHom.noncommCoprod_apply' : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Add M] [inst_1 : Add N] [inst_2 : AddSemigroup P] (f : M →ₙ+ P)
  (g : N →ₙ+ P) (comm : ∀ (m : M) (n : N), AddCommute (f m) (g n)) (mn : M × N),
  (f.noncommCoprod g comm) mn = g mn.2 + f mn.1
-- Mathlib.Algebra.Group.Pi.Lemmas
Function.ExtendByZero.hom.eq_1 : ∀ {ι : Type u_1} {η : Type v} (R : Type w) (s : ι → η) [inst : AddZeroClass R],
  Function.ExtendByZero.hom R s = { toFun := fun f => Function.extend s f 0, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.coeFn_smul : ∀ {𝕜 : Type u_1} {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)]
  [inst_1 : NormedRing 𝕜] [inst_2 : (i : α) → Module 𝕜 (E i)] [inst_3 : ∀ (i : α), IsBoundedSMul 𝕜 (E i)] (c : 𝕜)
  (f : ↥(lp E p)), ↑(c • f) = c • ↑f
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.HasColimits
CategoryTheory.opEquiv.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (A B : Cᵒᵖ),
  CategoryTheory.opEquiv A B = { toFun := fun f => f.unop, invFun := fun g => g.op, left_inv := ⋯, right_inv := ⋯ }
-- Std.Net.Addr
Std.Net.AddressFamily.ipv6 : Std.Net.AddressFamily
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.lift.congr_simp : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f f_1 : S.LocalizationMap N),
  f = f_1 → ∀ {g g_1 : M →* P} (e_g : g = g_1) (hg : ∀ (y : ↥S), IsUnit (g ↑y)), f.lift hg = f_1.lift ⋯
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {k k' : α}, cmp k k' = Ordering.eq → t.getKey! k = t.getKey! k'
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct_apply : ∀ {R : Type uR} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Semiring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Semiring D]
  [inst_7 : Algebra R D] [inst_8 : Algebra R C] (f : TensorProduct R (TensorProduct R A B) C ≃ₗ[R] D)
  (h_mul :
    ∀ (a₁ a₂ : A) (b₁ b₂ : B) (c₁ c₂ : C),
      f ((a₁ * a₂) ⊗ₜ[R] (b₁ * b₂) ⊗ₜ[R] (c₁ * c₂)) = f (a₁ ⊗ₜ[R] b₁ ⊗ₜ[R] c₁) * f (a₂ ⊗ₜ[R] b₂ ⊗ₜ[R] c₂))
  (h_one : f (1 ⊗ₜ[R] 1 ⊗ₜ[R] 1) = 1) (x : TensorProduct R (TensorProduct R A B) C),
  (Algebra.TensorProduct.algEquivOfLinearEquivTripleTensorProduct f h_mul h_one) x = f x
-- Mathlib.Data.Nat.PSub
Nat.pred_eq_ppred : ∀ (n : ℕ), n.pred = n.ppred.getD 0
-- Mathlib.Algebra.Order.Module.Defs
smul_le_iff_le_one_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Monoid α] [inst_1 : Zero β] [inst_2 : MulAction α β]
  [inst_3 : Preorder α] [inst_4 : Preorder β] [SMulPosMono α β] [SMulPosReflectLE α β], 0 < b → (a • b ≤ b ↔ a ≤ 1)
-- Mathlib.Algebra.Group.Finsupp
Finsupp.sub_apply : ∀ {ι : Type u_1} {G : Type u_6} [inst : SubNegZeroMonoid G] (g₁ g₂ : ι →₀ G) (a : ι), (g₁ - g₂) a = g₁ a - g₂ a
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
WithTop.sInf_of_not_bddBelow : ∀ {α : Type u_1} [inst : LE α] [inst_1 : InfSet α] {s : Set (WithTop α)}, ¬BddBelow s → sInf s = ⊤
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → ∀ (k : α), (t₁.erase k).Equiv (t₂.erase k)
-- Mathlib.Algebra.Group.TypeTags.Hom
MonoidHom.toAdditiveRight_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : AddZeroClass α] [inst_1 : MulOneClass β] (a : Multiplicative α →* β) (a_1 : α),
  (MonoidHom.toAdditiveRight a) a_1 = Additive.ofMul (a (Multiplicative.ofAdd a_1))
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.homInhabited.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (M : CategoryTheory.AddMon C), M.homInhabited = { default := M.id }
-- Init.Data.Vector.Algebra
/-- Heterogeneous componentwise scalar multiplication of vectors.  -/
Vector.hmul : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → {n : ℕ} → [HMul α β γ] → α → Vector β n → Vector γ n
-- Std.Data.TreeMap.Raw.Basic
/-- Returns a list of all keys present in the tree map in ascending  order.  -/
Std.TreeMap.Raw.keys : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → List α
-- Mathlib.Topology.MetricSpace.Bounded
Metric.isBounded_range_of_tendsto_cofinite_uniformity : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : β → α},
  Filter.Tendsto (Prod.map f f) (Filter.cofinite ×ˢ Filter.cofinite) (uniformity α) → Bornology.IsBounded (Set.range f)
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instDistribMulAction : {α : Type u_1} →
  {R : Type u_3} →
    [inst : Monoid R] →
      [inst_1 : DistribMulAction R ENNReal] →
        [IsScalarTower R ENNReal ENNReal] → DistribMulAction R (MeasureTheory.OuterMeasure α)
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.forAsync : {α : Type} →
  (α → BaseIO Unit) → Std.Bounded.Receiver✝ α → optParam Task.Priority Task.Priority.default → BaseIO (Task Unit)
-- Mathlib.CategoryTheory.Monad.Coequalizer
CategoryTheory.Monad.beckAlgebraCofork_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} (X : T.Algebra)
  (X_1 : CategoryTheory.Limits.WalkingParallelPair),
  (CategoryTheory.Monad.beckAlgebraCofork X).ι.app X_1 =
    CategoryTheory.Limits.WalkingParallelPair.rec
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Monad.FreeCoequalizer.topMap X)
        (CategoryTheory.Monad.FreeCoequalizer.π X))
      (CategoryTheory.Monad.FreeCoequalizer.π X) X_1
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.restrict_of_comp_subtype : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  {s : Set ι}, AlgebraicIndependent R (x ∘ Subtype.val) → AlgebraicIndependent R (s.domRestrict x)
-- Init.Data.Nat.Basic
Nat.add_right_comm : ∀ (n m k : ℕ), n + m + k = n + k + m
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.toCotangent_range : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R), I.toCotangent.range = ⊤
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.SimpleFunc.integral_eq : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) (f : MeasureTheory.SimpleFunc α F),
  MeasureTheory.SimpleFunc.integral μ f = ∑ x ∈ f.range, μ.real (⇑f ⁻¹' {x}) • x
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decomposeLinearEquiv_symm_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (ℳ : ι → Submodule R M) [inst_4 : DirectSum.Decomposition ℳ] (m : DirectSum ι fun i => ↥(ℳ i)),
  (DirectSum.decomposeLinearEquiv ℳ).symm m = (DirectSum.decompose ℳ).symm m
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.Finite.vadd_set : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {s : Set β} {a : α}, s.Finite → (a +ᵥ s).Finite
-- Mathlib.Data.List.Pi
Multiset.pi_coe : ∀ {ι : Type u_1} [inst : DecidableEq ι] {α : ι → Type u_2} (l : List ι) (fs : (i : ι) → List (α i)),
  ((↑l).pi fun x => ↑(fs x)) = ↑(l.pi fs)
-- Mathlib.RingTheory.Polynomial.Vieta
/-- Vieta's formula for split polynomials over a field.  -/
Polynomial.coeff_eq_esymm_roots_of_splits : ∀ {F : Type u_2} [inst : Field F] {p : Polynomial F},
  p.Splits →
    ∀ {k : ℕ}, k ≤ p.natDegree → p.coeff k = p.leadingCoeff * (-1) ^ (p.natDegree - k) * p.roots.esymm (p.natDegree - k)
-- Mathlib.CategoryTheory.Limits.Cones
/-- The triangle made from the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.CoconeMorphism.w_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cocone F}
  (self : CategoryTheory.Limits.CoconeMorphism A B) (j : J) {Z : C} (h : B.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp (A.ι.app j) (CategoryTheory.CategoryStruct.comp self.hom h) =
    CategoryTheory.CategoryStruct.comp (B.ι.app j) h
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mk'_toAddSubgroup : ∀ {R : Type u} [inst : NonAssocRing R] {s : Set R} {sm : Submonoid R} (hm : ↑sm = s) {sa : AddSubgroup R}
  (ha : ↑sa = s), (Subring.mk' s sm sa hm ha).toAddSubgroup = sa
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toRingHom_injective : ∀ {R : Type u_4} {S : Type u_5} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S],
  Function.Injective RingEquiv.toRingHom
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.Num.gcdAux.match_1.eq_3 : ∀ (motive : ℕ → Num → Num → Sort u_1) (n : ℕ) (a b : Num) (h_1 : (x b : Num) → motive 0 x b)
  (h_2 : (n : ℕ) → (b : Num) → motive n.succ Num.zero b) (h_3 : (n : ℕ) → (a b : Num) → motive n.succ a b),
  (a = Num.zero → False) →
    (match n.succ, a, b with
      | 0, x, b => h_1 x b
      | n.succ, Num.zero, b => h_2 n b
      | n.succ, a, b => h_3 n a b) =
      h_3 n a b
-- Init.Data.Nat.Lemmas
Nat.lt_div_iff_mul_lt_of_dvd : ∀ {c b a : ℕ}, c ≠ 0 → c ∣ b → (a < b / c ↔ a * c < b)
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_neg_ofNat_of_le : ∀ {n : ℕ}, n ≤ 2 ^ 31 → (-ISize.ofNat n).toNatClampNeg = 0
-- Mathlib.Algebra.Order.Module.HahnEmbedding
/-- `HahnEmbedding.Seed.coeff` with `ArchimedeanStrata.stratum'` as domain.  -/
HahnEmbedding.Seed.coeff' : {K : Type u_1} →
  [inst : DivisionRing K] →
    [inst_1 : LinearOrder K] →
      [inst_2 : IsOrderedRing K] →
        [inst_3 : Archimedean K] →
          {M : Type u_2} →
            [inst_4 : AddCommGroup M] →
              [inst_5 : LinearOrder M] →
                [inst_6 : IsOrderedAddMonoid M] →
                  [inst_7 : Module K M] →
                    [inst_8 : IsOrderedModule K M] →
                      {R : Type u_3} →
                        [inst_9 : AddCommGroup R] →
                          [inst_10 : LinearOrder R] →
                            [inst_11 : Module K R] →
                              (seed : HahnEmbedding.Seed K M R) →
                                (c : FiniteArchimedeanClass M) → ↥(seed.stratum' c) →ₗ[K] R