mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.single_left_inj : ∀ {k : Type u_1} {G : Type u_2} [inst : AddMonoid k] {a a' : G} {b : k},
  b ≠ 0 → (SkewMonoidAlgebra.single a b = SkewMonoidAlgebra.single a' b ↔ a = a')
-- Mathlib.Order.Interval.Set.Fin
Fin.image_natAdd_Ici : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Fin.natAdd m '' Set.Ici i = Set.Ici (Fin.natAdd m i)
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.growsPolynomially_one_add_smoothingFn : AkraBazziRecurrence.GrowsPolynomially fun x => 1 + AkraBazziRecurrence.smoothingFn x
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.map_inrX_mapHomologicalComplexObjXIso_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] {D : Type u_3} [inst_4 : CategoryTheory.Category.{v_2, u_3} D]
  [inst_5 : CategoryTheory.Preadditive D] (H : CategoryTheory.Functor C D) [inst_6 : H.Additive]
  [inst_7 : HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex c).map φ)] (i : ι) {Z : D}
  (h : (HomologicalComplex.homotopyCofiber ((H.mapHomologicalComplex c).map φ)).X i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (H.map (HomologicalComplex.homotopyCofiber.inrX φ i))
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.mapHomologicalComplexObjXIso φ H i).hom
        h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.inrX ((H.mapHomologicalComplex c).map φ) i) h
-- Mathlib.Algebra.Polynomial.Div
Polynomial.eq_of_dvd_of_natDegree_le_of_leadingCoeff : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] {p q : Polynomial R},
  p ∣ q → q.natDegree ≤ p.natDegree → p.leadingCoeff = q.leadingCoeff → p = q
-- Mathlib.CategoryTheory.Monoidal.Functor
/-- The tensorator as a natural isomorphism.  -/
CategoryTheory.Functor.Monoidal.μNatIso : {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) →
              [F.Monoidal] →
                (F.prod F).comp (CategoryTheory.MonoidalCategory.tensor D) ≅
                  (CategoryTheory.MonoidalCategory.tensor C).comp F
-- Mathlib.Algebra.Module.Basic
Set.indicator_smul_apply_left : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero R] [inst_1 : Zero M] [inst_2 : SMulWithZero R M] (s : Set α)
  (r : α → R) (f : α → M) (a : α), s.indicator (fun a => r a • f a) a = s.indicator r a • f a
-- Mathlib.Data.Set.Image
Set.preimage_sumElim : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (s : Set γ) (f : α → γ) (g : β → γ),
  Sum.elim f g ⁻¹' s = Sum.inl '' f ⁻¹' s ∪ Sum.inr '' g ⁻¹' s
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.Hom.ext : ∀ {A B : AddMonCat} {x y : A.Hom B}, x.hom' = y.hom' → x = y
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.beq : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : BEq β] [ReflBEq β], m₁.WF → m₂.WF → m₁.Equiv m₂ → (m₁ == m₂) = true
-- Mathlib.LinearAlgebra.Dimension.Finite
/-- A nontrivial finite-dimensional space has positive `finrank`.  -/
Module.finrank_pos : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] [IsDomain R] [Module.IsTorsionFree R M] [h : Nontrivial M], 0 < Module.finrank R M
-- Lean.Elab.Tactic.Omega.MinNatAbs
_private.Lean.Elab.Tactic.Omega.MinNatAbs.0.Lean.Elab.Tactic.Omega.List.minNatAbs.eq_1 : ∀ (xs : List ℤ),
  Lean.Elab.Tactic.Omega.List.minNatAbs xs = Lean.Elab.Tactic.Omega.List.nonzeroMinimum (List.map Int.natAbs xs)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.foldingRangeProvider : Lean.Lsp.ServerCapabilities → Bool
-- Init.Data.Fin.Basic
Fin.exists_iff : ∀ {n : ℕ} {p : Fin n → Prop}, (∃ i, p i) ↔ ∃ i, ∃ (h : i < n), p ⟨i, h⟩
-- Mathlib.Combinatorics.Graph.Basic
Graph.IsLink.left_mem : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G : Graph α β}, G.IsLink e x y → x ∈ G.vertexSet
-- Init.Grind.ToInt
Lean.Grind.IntInterval.co.inj : ∀ {lo hi lo_1 hi_1 : ℤ}, Lean.Grind.IntInterval.co lo hi = Lean.Grind.IntInterval.co lo_1 hi_1 → lo = lo_1 ∧ hi = hi_1
-- Mathlib.Data.Finsupp.SMulWithZero
Finsupp.smul_apply : ∀ {α : Type u_1} {M : Type u_5} {R : Type u_11} [inst : Zero M] [inst_1 : SMulZeroClass R M] (b : R) (v : α →₀ M)
  (a : α), (b • v) a = b • v a
-- Lean.Data.Lsp.Basic
Lean.Lsp.DocumentChange.edit.injEq : ∀ (a a_1 : Lean.Lsp.TextDocumentEdit), (Lean.Lsp.DocumentChange.edit a = Lean.Lsp.DocumentChange.edit a_1) = (a = a_1)
-- Init.Prelude
/-- Sequences two reader monad computations. Both are provided with the local value, and the second is
passed the value of the first. Typically used via the `>>=` operator.
 -/
ReaderT.bind : {ρ : Type u} → {m : Type u → Type v} → [Monad m] → {α β : Type u} → ReaderT ρ m α → (α → ReaderT ρ m β) → ReaderT ρ m β
-- Mathlib.Data.BitVec
/-- The ring `BitVec m` is isomorphic to `Fin (2 ^ m)`.  -/
BitVec.equivFin : {m : ℕ} → BitVec m ≃+* Fin (2 ^ m)
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.op_i : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W₁ W₂ : CategoryTheory.MorphismProperty C) {X Y : C}
  {f : X ⟶ Y} (hf : W₁.MapFactorizationData W₂ f),
  (CategoryTheory.MorphismProperty.MapFactorizationData.op W₁ W₂ hf).i = hf.p.op
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.uliftYonedaReprXIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (F : CategoryTheory.Functor Cᵒᵖ (Type (max v v₁)))
  [inst_1 : F.IsRepresentable] (X : Cᵒᵖ) (f : ULift.{v, v₁} (Opposite.unop X ⟶ F.reprX)),
  (CategoryTheory.ConcreteCategory.hom (F.uliftYonedaReprXIso.hom.app X)) f =
    (CategoryTheory.ConcreteCategory.hom (F.map f.down.op)) F.reprx
-- Mathlib.NumberTheory.Modular
/-- Classify the `z` and `g` with `z ∈ 𝒟` and `g • z ∈ 𝒟`.  -/
ModularGroup.cases_of_mem_fd_smul_mem_fd : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fd →
    g • z ∈ ModularGroup.fd →
      (g = 1 ∨ g = -1) ∨
        (g = ModularGroup.T ∨ g = -ModularGroup.T) ∧ z.re = -1 / 2 ∨
          (g = ModularGroup.T⁻¹ ∨ g = -ModularGroup.T⁻¹) ∧ z.re = 1 / 2 ∨
            (g = ModularGroup.S ∨ g = -ModularGroup.S) ∧ ‖↑z‖ = 1 ∨
              (g = ModularGroup.T * ModularGroup.S ∨ g = -(ModularGroup.T * ModularGroup.S)) ∧
                  z = 1 +ᵥ UpperHalfPlane.ρ ∨
                (g = ModularGroup.T⁻¹ * ModularGroup.S * ModularGroup.T⁻¹ ∨
                      g = -(ModularGroup.T⁻¹ * ModularGroup.S * ModularGroup.T⁻¹)) ∧
                    z = 1 +ᵥ UpperHalfPlane.ρ ∨
                  (g = ModularGroup.S * ModularGroup.T⁻¹ ∨ g = -(ModularGroup.S * ModularGroup.T⁻¹)) ∧
                      z = 1 +ᵥ UpperHalfPlane.ρ ∨
                    (g = ModularGroup.S * ModularGroup.T ∨ g = -(ModularGroup.S * ModularGroup.T)) ∧
                        z = UpperHalfPlane.ρ ∨
                      (g = ModularGroup.T * ModularGroup.S * ModularGroup.T ∨
                            g = -(ModularGroup.T * ModularGroup.S * ModularGroup.T)) ∧
                          z = UpperHalfPlane.ρ ∨
                        (g = ModularGroup.T⁻¹ * ModularGroup.S ∨ g = -(ModularGroup.T⁻¹ * ModularGroup.S)) ∧
                          z = UpperHalfPlane.ρ
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_cancel : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (m : M) (s : ↥S), IsLocalizedModule.mk' f (s • m) s = f m
-- Mathlib.Tactic.Positivity.Core
/-- A variation on `assumption` which checks if the hypothesis `ldecl` is `a [</≤/=] e`
where `a` is a numeral.  -/
Mathlib.Meta.Positivity.compareHyp : {u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      (pα : Q(PartialOrder «$α»)) →
        (e : Q(«$α»)) → Lean.LocalDecl → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e (some pα))
-- Mathlib.Data.Nat.Cast.Commute
Nat.cast_comm : ∀ {α : Type u_1} [inst : NonAssocSemiring α] (n : ℕ) (x : α), ↑n * x = x * ↑n
-- Init.Data.Dyadic.Round
Dyadic.roundDown_le : ∀ {x : Dyadic} {prec : ℤ}, x.roundDown prec ≤ x
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.gcd_dvd_step : ∀ {k a b x : ℤ}, k ∣ a * x + b → Int.Internal.Linear.gcd✝ a k ∣ b
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- Every element in the adic completion is represented by a Cauchy sequence.  -/
AdicCompletion.mk_surjective : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Function.Surjective ⇑(AdicCompletion.mk I M)
-- Mathlib.RingTheory.Localization.Finiteness
Module.Finite.of_isLocalizedModule : ∀ {R : Type u} [inst : CommSemiring R] (S : Submonoid R) {Rₚ : Type v} [inst_1 : CommSemiring Rₚ]
  [inst_2 : Algebra R Rₚ] [IsLocalization S Rₚ] {M : Type w} [inst_4 : AddCommMonoid M] [inst_5 : Module R M]
  {Mₚ : Type t} [inst_6 : AddCommMonoid Mₚ] [inst_7 : Module R Mₚ] [inst_8 : Module Rₚ Mₚ] [IsScalarTower R Rₚ Mₚ]
  (f : M →ₗ[R] Mₚ) [IsLocalizedModule S f] [Module.Finite R M], Module.Finite Rₚ Mₚ
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Remove the minimum element from the tree, or do nothing if it is already empty.

```
eraseMin {1, 2, 3} = {2, 3}
eraseMin ∅ = ∅
```  -/
Ordnode.eraseMin : {α : Type u_1} → Ordnode α → Ordnode α
-- Mathlib.Order.Hom.Lattice
InfHom.toFun_eq_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Min β] (f : InfHom α β), f.toFun = ⇑f
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.ofFun_div : ∀ {α : Type u_1} {β : Type u_2} {𝔖 : Set (Set α)} [inst : Div β] (f g : α → β),
  (UniformOnFun.ofFun 𝔖) (f / g) = (UniformOnFun.ofFun 𝔖) f / (UniformOnFun.ofFun 𝔖) g
-- Mathlib.MeasureTheory.Integral.SetToL1
measurableSet_integrable : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {β : Type u_7} {mβ : MeasurableSpace β} [MeasureTheory.SFinite μ] ⦃f : β → α → E⦄,
  MeasureTheory.StronglyMeasurable (Function.uncurry f) → MeasurableSet {x | MeasureTheory.Integrable (f x) μ}
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.EquivEven.neg_e0_mul_v : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M),
  -(CliffordAlgebra.EquivEven.e0 Q * (CliffordAlgebra.EquivEven.v Q) m) =
    (CliffordAlgebra.EquivEven.v Q) m * CliffordAlgebra.EquivEven.e0 Q
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.inv_actionHomLeft : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {x y : D} (f : x ⟶ y)
  [inst_4 : CategoryTheory.IsIso f] (z : C),
  CategoryTheory.inv (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f z) =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft (CategoryTheory.inv f) z
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a right-angled triangle expressed using `arccos`, version subtracting vectors.  -/
InnerProductGeometry.angle_sub_eq_arccos_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → InnerProductGeometry.angle x (x - y) = Real.arccos (‖x‖ / ‖x - y‖)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.IsLimit.lift_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  {t : CategoryTheory.Limits.PullbackCone f g} (ht : CategoryTheory.Limits.IsLimit t) {W : C} (h : W ⟶ X) (k : W ⟶ Y)
  (w : CategoryTheory.CategoryStruct.comp h f = CategoryTheory.CategoryStruct.comp k g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.PullbackCone.IsLimit.lift ht h k w) t.snd = k
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.inr_comp_pushoutSymmetry_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.Limits.HasPushout f g],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g f)
      (CategoryTheory.Limits.pushoutSymmetry f g).inv =
    CategoryTheory.Limits.pushout.inl f g
-- Mathlib.Probability.Distributions.Gamma
ProbabilityTheory.gammaPDF.eq_1 : ∀ (a r x : ℝ), ProbabilityTheory.gammaPDF a r x = ENNReal.ofReal (ProbabilityTheory.gammaPDFReal a r x)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Ric.forIn'_congr : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerableLeast? α] [inst_6 : Std.Rxc.IsAlwaysFinite α]
  [inst_7 : Std.PRange.LawfulUpwardEnumerable α] {m : Type u → Type w} [inst_8 : Monad m] {γ : Type u} {init init' : γ}
  {r r' : Std.Ric α} {f : (a : α) → a ∈ r → γ → m (ForInStep γ)} {f' : (a : α) → a ∈ r' → γ → m (ForInStep γ)}
  (hr : r = r'),
  init = init' → (∀ (a : α) (m_1 : a ∈ r') (b : γ), f a ⋯ b = f' a m_1 b) → forIn' r init f = forIn' r' init' f'
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.emptyWithCapacity_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {c : ℕ},
  Std.ExtHashSet.emptyWithCapacity c = ∅
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomMulAct.isClosedEmbedding_mk : ∀ {M : Type u_1} [inst : TopologicalSpace M], Topology.IsClosedEmbedding ⇑DomMulAct.mk
-- Init.Data.UInt.Lemmas
UInt8.ofInt_neg_one : UInt8.ofInt (-1) = -1
-- Mathlib.Topology.PartialHomeomorph.Defs
/-- The inverse of a partial homeomorphism  -/
PartialHomeomorph.symm : {X : Type u_1} →
  {Y : Type u_3} →
    [inst : TopologicalSpace X] → [inst_1 : TopologicalSpace Y] → PartialHomeomorph X Y → PartialHomeomorph Y X
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
/-- The inner product on `⋀[ℝ]^n E` as a bilinear map. This is an implementation detail
for constructing the `InnerProductSpace` instance and should not be used directly.
Use `⟪·, ·⟫` instead.  -/
_private.Mathlib.Analysis.InnerProductSpace.ExteriorPower.0.exteriorPower.innerProductForm : {n : ℕ} →
  {E : Type u_1} →
    [inst : NormedAddCommGroup E] → [inst_1 : InnerProductSpace ℝ E] → ↥(⋀[ℝ]^n E) →ₗ[ℝ] ↥(⋀[ℝ]^n E) →ₗ[ℝ] ℝ
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.sub_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {ι : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommGroup N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f g : M [⋀^ι]→L[R] N) [inst_7 : IsTopologicalAddGroup N] (m : ι → M),
  (f - g) m = f m - g m
-- Mathlib.Analysis.Calculus.LineDeriv.QuadraticMap
QuadraticMap.hasLineDerivAt : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : QuadraticMap 𝕜 E F) (a b : E),
  HasLineDerivAt 𝕜 (⇑f) (QuadraticMap.polar (⇑f) a b) a b
-- Mathlib.LinearAlgebra.TensorProduct.Basis
/-- Elements in `M ⊗ N` can be represented by sum of elements in `M` tensor elements of basis of
`N`.  -/
TensorProduct.eq_repr_basis_right : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {κ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (𝒞 : Module.Basis κ R N)
  (x : TensorProduct R M N), ∃ b, (b.sum fun i m => m ⊗ₜ[R] 𝒞 i) = x
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {a b : α},
  (a == b) = true → m.contains a = m.contains b
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.instModule : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {E : Type u_3} →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜₁ E] →
                  [inst_4 : TopologicalSpace E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : Module 𝕜₂ F] →
                        (R : Type u_6) →
                          [inst_7 : Semiring R] →
                            [inst_8 : Module R F] →
                              [SMulCommClass 𝕜₂ R F] →
                                [inst_10 : TopologicalSpace F] →
                                  [ContinuousConstSMul R F] →
                                    [inst_12 : IsTopologicalAddGroup F] →
                                      (𝔖 : Set (Set E)) → Module R (UniformConvergenceCLM σ F 𝔖)
-- Mathlib.Algebra.Star.StarProjection
IsStarProjection.map : ∀ {A : Type u_2} {B : Type u_3} [inst : Mul A] [inst_1 : Star A] [inst_2 : Mul B] [inst_3 : Star B] {F : Type u_4}
  [inst_4 : FunLike F A B] [StarHomClass F A B] [MulHomClass F A B] {x : A},
  IsStarProjection x → ∀ (f : F), IsStarProjection (f x)
-- Init.Data.Iterators.Consumers.Loop
/-- A `ForIn'` instance for iterators that is guaranteed to terminate after finitely many steps.
It is not marked as an instance because the membership predicate is difficult to work with.
 -/
Std.Iter.Total.instForIn' : {α β : Type w} →
  {n : Type x → Type x'} →
    [Monad n] →
      [inst : Std.Iterator α Id β] →
        [Std.IteratorLoop α Id n] →
          [Std.Iterators.Finite α Id] →
            ForIn' n (Std.Iter.Total β) β { mem := fun it out => it.it.IsPlausibleIndirectOutput out }
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
RingPreordering.mem_toSubsemiring : ∀ {R : Type u_1} [inst : CommRing R] {P : RingPreordering R} {x : R}, x ∈ ↑P ↔ x ∈ P
-- Mathlib.Analysis.LocallyConvex.WithSeminorms
/-- A (semi-)normed space is polynormable.  -/
instPolynormableSpace : ∀ {𝕜 : Type u_2} {E : Type u_6} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E],
  PolynormableSpace 𝕜 E
-- Lean.Environment
_private.Lean.Environment.0.Lean.readIRPartsOfMod.unsafe_1 : System.FilePath → IO (Lean.ModuleData × Lean.CompactedRegion)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Expr.toPolyS_NonnegCoeffs : ∀ {e : Lean.Grind.CommRing.Expr}, e.toPolyS.NonnegCoeffs
-- Mathlib.Topology.Order.LocalExtr
Filter.EventuallyLE.isLocalMaxOn : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {s : Set α} {f g : α → β} {a : α},
  g ≤ᶠ[nhdsWithin a s] f → f a = g a → IsLocalMaxOn f s a → IsLocalMaxOn g s a
-- ImportGraph.Imports.ImportGraph
/-- Find the imports of a given module.
 -/
Lean.Environment.importsOf : Lean.Environment → Lean.Name → Array Lean.Name
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.denote.match_1.eq_2 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (a b : Int.Internal.Linear.Expr)
  (h_1 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_2 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b)) (h_3 : (a : Int.Internal.Linear.Expr) → motive a.neg)
  (h_4 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_5 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_6 : (k : ℤ) → (e : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k e))
  (h_7 : (e : Int.Internal.Linear.Expr) → (k : ℤ) → motive (e.mulR k)),
  (match a.sub b with
    | a.add b => h_1 a b
    | a.sub b => h_2 a b
    | a.neg => h_3 a
    | Int.Internal.Linear.Expr.num k => h_4 k
    | Int.Internal.Linear.Expr.var v => h_5 v
    | Int.Internal.Linear.Expr.mulL k e => h_6 k e
    | e.mulR k => h_7 e k) =
    h_2 a b
-- Mathlib.RingTheory.Coalgebra.Equiv
/-- Coalgebra equivalences are transitive.  -/
CoalgEquiv.trans : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      {C : Type u_4} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid A] →
            [inst_2 : AddCommMonoid B] →
              [inst_3 : AddCommMonoid C] →
                [inst_4 : Module R A] →
                  [inst_5 : Module R B] →
                    [inst_6 : Module R C] →
                      [inst_7 : CoalgebraStruct R A] →
                        [inst_8 : CoalgebraStruct R B] →
                          [inst_9 : CoalgebraStruct R C] → (A ≃ₗc[R] B) → (B ≃ₗc[R] C) → A ≃ₗc[R] C
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.instPreadditiveOppositeShift : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (A : Type u_2) →
      [inst_1 : AddMonoid A] →
        [inst_2 : CategoryTheory.HasShift C A] →
          [CategoryTheory.Preadditive C] → CategoryTheory.Preadditive (CategoryTheory.OppositeShift C A)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.triangleLEGE_obj_mor₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b) (j : C),
  ((t.triangleLEGE a b h).obj j).mor₃ = (t.truncGEδLE a b h).app j
-- ProofWidgets.Component.RefreshComponent
_private.ProofWidgets.Component.RefreshComponent.0.ProofWidgets.RefreshToken.mk.injEq : ∀ (state : IO.Ref ProofWidgets.RefreshComponent.RefreshState) (cancelTk : IO.CancelToken)
  (promise : IO.Ref (IO.Promise Unit)) (state_1 : IO.Ref ProofWidgets.RefreshComponent.RefreshState)
  (cancelTk_1 : IO.CancelToken) (promise_1 : IO.Ref (IO.Promise Unit)),
  ({ state := state, cancelTk := cancelTk, promise := promise } =
      { state := state_1, cancelTk := cancelTk_1, promise := promise_1 }) =
    (state = state_1 ∧ cancelTk = cancelTk_1 ∧ promise = promise_1)
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Adjunction.unit_app_shift_commShiftIso_inv_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) (A : Type u_3) [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : F.CommShift A] [inst_6 : G.CommShift A] [adj.CommShift A] (a : A)
  (X : C),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C a).map (adj.unit.app X))
      ((CategoryTheory.Functor.commShiftIso (F.comp G) a).inv.app X) =
    adj.unit.app ((CategoryTheory.shiftFunctor C a).obj X)
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Multipliable.le_tprod' : ∀ {ι : Type u_1} {α : Type u_3} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedMonoid α]
  [CanonicallyOrderedMul α] [inst_4 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α},
  Multipliable f → ∀ (i : ι), f i ≤ ∏' (i : ι), f i
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.eq_mp : ∀ {δ : Type u_4} (X : δ → Type u_6) [inst : (a : δ) → MeasurableSpace (X a)] {β : Type u_7} [inst_1 : MeasurableSpace β]
  {i i' : δ} (h : i = i') {f : β → X i}, Measurable f → Measurable fun x => ⋯.mp (f x)