mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Ring.Basic
/-- Try to evaluate an expression as a rational constant using `norm_num`.  -/
Mathlib.Tactic.Ring.RingCompute.derive : {u : Lean.Level} →
  {α : Q(Type u)} →
    (sα : Q(CommSemiring «$α»)) →
      (x : Q(«$α»)) →
        Lean.MetaM
          (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Ring.Common.ExSum Mathlib.Tactic.Ring.RatCoeff sα) q(«$x»))
-- Mathlib.Analysis.InnerProductSpace.Reproducing
RKHS.coe_neg : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] (f : H), ⇑(-f) = -⇑f
-- Init.Data.SInt.Lemmas
Int64.ofIntTruncate_bitVecToInt : ∀ (n : BitVec 64), Int64.ofIntClamp n.toInt = Int64.ofBitVec n
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.ofCoconeEquiv_symm_apply_desc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C} {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] {G : CategoryTheory.Functor K D}
  (h : CategoryTheory.Limits.Cocone G ≌ CategoryTheory.Limits.Cocone F) {c : CategoryTheory.Limits.Cocone G}
  (P : CategoryTheory.Limits.IsColimit c) (s : CategoryTheory.Limits.Cocone F),
  ((CategoryTheory.Limits.IsColimit.ofCoconeEquiv h).symm P).desc s =
    CategoryTheory.CategoryStruct.comp (h.functor.map (P.descCoconeMorphism (h.inverse.obj s))).hom
      (h.counitIso.hom.app s).hom
-- Mathlib.Topology.UniformSpace.UniformEmbedding
Filter.HasBasis.isUniformEmbedding_iff' : ∀ {α : Type u} {β : Type v} [inst : UniformSpace α] [inst_1 : UniformSpace β] {ι : Sort u_1} {ι' : Sort u_2}
  {p : ι → Prop} {p' : ι' → Prop} {s : ι → Set (α × α)} {s' : ι' → Set (β × β)},
  (uniformity α).HasBasis p s →
    (uniformity β).HasBasis p' s' →
      ∀ {f : α → β},
        IsUniformEmbedding f ↔
          Function.Injective f ∧
            (∀ (i : ι'), p' i → ∃ j, p j ∧ ∀ (x y : α), (x, y) ∈ s j → (f x, f y) ∈ s' i) ∧
              ∀ (j : ι), p j → ∃ i, p' i ∧ ∀ (x y : α), (f x, f y) ∈ s' i → (x, y) ∈ s j
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.zero_def : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} [inst_1 : Nontrivial R],
  0 = { point := ⟦![0, 1, 0]⟧, nonsingular := ⋯ }
-- Mathlib.RingTheory.Valuation.Basic
/-- `ValuationClass F α β` states that `F` is a type of valuations.

You should also extend this typeclass when you extend `Valuation`.  -/
ValuationClass : (F : Type u_7) →
  (R : outParam (Type u_5)) →
    (Γ₀ : outParam (Type u_6)) → [LinearOrderedCommMonoidWithZero Γ₀] → [Ring R] → [FunLike F R Γ₀] → Prop
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk_canonicalEquiv : ∀ {R : Type u_1} (K : Type u_2) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K]
  [inst_3 : IsFractionRing R K] [inst_4 : IsDomain R] (K' : Type u_3) [inst_5 : Field K'] [inst_6 : Algebra R K']
  [inst_7 : IsFractionRing R K'] (I : (FractionalIdeal (nonZeroDivisors R) K)ˣ),
  (ClassGroup.mk K') ((Units.map ↑(FractionalIdeal.canonicalEquiv (nonZeroDivisors R) K K')) I) = (ClassGroup.mk K) I
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
AlgHom.map_adjoin : ∀ {R : Type uR} {A : Type uA} {B : Type uB} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (φ : A →ₐ[R] B) (s : Set A),
  Subalgebra.map φ (Algebra.adjoin R s) = Algebra.adjoin R (⇑φ '' s)
-- Mathlib.LinearAlgebra.Alternating.DomCoprod
/-- summand used in `AlternatingMap.domCoprod`  -/
AlternatingMap.domCoprod.summand : {ιa : Type u_1} →
  {ιb : Type u_2} →
    [Fintype ιa] →
      [Fintype ιb] →
        {R' : Type u_3} →
          {Mᵢ : Type u_4} →
            {N₁ : Type u_5} →
              {N₂ : Type u_6} →
                [inst : CommSemiring R'] →
                  [inst_1 : AddCommGroup N₁] →
                    [inst_2 : Module R' N₁] →
                      [inst_3 : AddCommGroup N₂] →
                        [inst_4 : Module R' N₂] →
                          [inst_5 : AddCommMonoid Mᵢ] →
                            [inst_6 : Module R' Mᵢ] →
                              [DecidableEq ιa] →
                                [DecidableEq ιb] →
                                  Mᵢ [⋀^ιa]→ₗ[R'] N₁ →
                                    Mᵢ [⋀^ιb]→ₗ[R'] N₂ →
                                      Equiv.Perm.ModSumCongr ιa ιb →
                                        MultilinearMap R' (fun x => Mᵢ) (TensorProduct R' N₁ N₂)
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_add_of_right_lt : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) → m.withBotDegree (f + g) = m.withBotDegree g
-- Mathlib.Analysis.Distribution.SchwartzSpace.Fourier
/-- Plancherel's theorem for Schwartz functions.

Version where the inner product is replaced by a general sesquilinear form `M`.  -/
SchwartzMap.integral_sesq_fourier_fourier : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_3} [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : FiniteDimensional ℝ V] [inst_5 : MeasurableSpace V] [inst_6 : BorelSpace V]
  {F : Type u_4} [inst_7 : NormedAddCommGroup F] [inst_8 : NormedSpace ℂ F] {G : Type u_5}
  [inst_9 : NormedAddCommGroup G] [inst_10 : NormedSpace ℂ G] [CompleteSpace E] [CompleteSpace F] (f : SchwartzMap V E)
  (g : SchwartzMap V F) (M : E →L⋆[ℂ] F →L[ℂ] G),
  ∫ (ξ : V), (M ((FourierTransform.fourier f) ξ)) ((FourierTransform.fourier g) ξ) = ∫ (x : V), (M (f x)) (g x)
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.isLocalHom_algebraMap : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] [IsLocalHom (algebraMap R A)], IsLocalHom (algebraMap R (MonoidAlgebra A M))
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inl_comp_inl_comp_associator : ∀ (x y z : AugmentedSimplexCategory),
  CategoryTheory.CategoryStruct.comp (x.inl y)
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj x y).inl z)
        (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom) =
    x.inl (CategoryTheory.MonoidalCategoryStruct.tensorObj y z)
-- Init.Data.SInt.Bitwise
USize.toISize_and : ∀ (a b : USize), (a &&& b).toISize = a.toISize &&& b.toISize
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.cont : ∀ {R : Type u_3} [inst : CommSemiring R] {A : Type u_4} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_5} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  (self : A →A[R] B), Continuous (↑↑(↑self).toRingHom).toFun
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim_hom_app : ∀ (α : Type w₂) {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasProductsOfShape α C] (X : α → C),
  (CategoryTheory.Limits.piEquivalenceFunctorDiscreteCompLim α).hom.app X =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Limits.limit (CategoryTheory.Discrete.functor X))
-- Mathlib.MeasureTheory.Group.Arithmetic
AddSubgroup.instMeasurableConstVAdd : ∀ {G : Type u_2} {α : Type u_3} [inst : MeasurableSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [MeasurableConstVAdd G α] (s : AddSubgroup G), MeasurableConstVAdd (↥s) α
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_eq_zero_of_le_one : ∀ {x : ℝ}, x ≤ 1 → Chebyshev.psi x = 0
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.val_sub : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  (x y : P.Cotangent), (x - y).val = x.val - y.val
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.SheafCondition.bijective_toPullbackObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] {S : J.MayerVietorisSquare}
  {P : CategoryTheory.Functor Cᵒᵖ (Type v')}, S.SheafCondition P → Function.Bijective (S.toPullbackObj P)
-- Init.Data.List.Nat.TakeDrop
List.drop_append_of_le_length : ∀ {α : Type u_1} {l₁ l₂ : List α} {i : ℕ}, i ≤ l₁.length → List.drop i (l₁ ++ l₂) = List.drop i l₁ ++ l₂
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
OrderDual.instNoZeroDivisors : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [NoZeroDivisors α], NoZeroDivisors αᵒᵈ
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.smul_mem : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (C : ConvexCone R M) {c : R} {x : M}, 0 < c → x ∈ C → c • x ∈ C
-- Mathlib.Data.Fintype.Order
Set.subset_iUnion_iff_of_directed : ∀ {ι : Sort u_1} {α : Type u_2} {s : Set α} {f : ι → Set α} [Nonempty ι] [Finite ι],
  Directed (fun x1 x2 => x1 ⊆ x2) f → (s ⊆ ⋃ i, f i ↔ ∃ i, s ⊆ f i)
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
UniqueFactorizationMonoid.dvd_iff_emultiplicity_le : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b : R},
  a ≠ 0 → (a ∣ b ↔ ∀ (p : R), Prime p → emultiplicity p a ≤ emultiplicity p b)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.trans_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (e : C ≌ D) (f : D ≌ E),
  (e.trans f).functor = e.functor.comp f.functor
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.exp_injOn_Ico : ∀ {a b : ℝ}, b - a ≤ 2 * Real.pi → Set.InjOn (⇑Circle.exp) (Set.Ico a b)
-- Mathlib.Data.Stream.Init
Stream'.cycle_g_cons : ∀ {α : Type u} (a a₁ : α) (l₁ : List α) (a₀ : α) (l₀ : List α), Stream'.cycleG (a, a₁ :: l₁, a₀, l₀) = (a₁, l₁, a₀, l₀)
-- Mathlib.Topology.Order.OrderClosed
iUnion_Ici_eq_Ioi_of_lt_of_tendsto : ∀ {α : Type u} {ι : Type u_1} {F : Filter ι} [F.NeBot] [inst : ConditionallyCompleteLinearOrder α]
  [inst_1 : TopologicalSpace α] [ClosedIciTopology α] {a : α} {f : ι → α},
  (∀ (i : ι), a < f i) → Filter.Tendsto f F (nhds a) → ⋃ i, Set.Ici (f i) = Set.Ioi a
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
Filter.EventuallyEq.mlieBracketWithin_vectorField_of_insert : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M}
  {V W V₁ W₁ : (x : M) → TangentSpace I x},
  V₁ =ᶠ[nhdsWithin x (insert x s)] V →
    W₁ =ᶠ[nhdsWithin x (insert x s)] W →
      VectorField.mlieBracketWithin I V₁ W₁ s x = VectorField.mlieBracketWithin I V W s x
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_self_eq_one : ∀ {b : ℝ}, 1 < b → Real.logb b b = 1
-- Mathlib.Topology.Algebra.Order.Floor
tendsto_floor_atTop : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] [IsStrictOrderedRing α],
  Filter.Tendsto Int.floor Filter.atTop Filter.atTop
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.instT5Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [T5Space M], T5Space Mᵈᵃᵃ
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.mkOfSucc_one_eq_δ : SimplexCategory.mkOfSucc 1 = SimplexCategory.δ 0
-- Mathlib.Geometry.Manifold.BumpFunction
/-- Given a smooth bump function `f : SmoothBumpFunction I c`, the closed ball of radius `f.R` is
known to include the support of `f`. These closed balls (in the model normed space `E`) intersected
with `Set.range I` form a basis of `𝓝[range I] (extChartAt I c c)`.  -/
SmoothBumpFunction.nhdsWithin_range_basis : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M},
  (nhdsWithin (↑(extChartAt I c) c) (Set.range ↑I)).HasBasis (fun x => True) fun f =>
    Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.zpow'_of_ne_zero_right : ∀ {α : Type u_1} [inst : GroupWithZero α] (a : α) (n : ℤ), n ≠ 0 → Mathlib.Tactic.FieldSimp.zpow' a n = a ^ n
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorμ_comp_μ_tensorHom_μ_comp_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.LaxBraided] (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ (F.obj W) (F.obj X) (F.obj Y) (F.obj Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Functor.LaxMonoidal.μ F W Y)
          (CategoryTheory.Functor.LaxMonoidal.μ F X Z))
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj W Y)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X Z))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.Functor.LaxMonoidal.μ F W X)
        (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj W X)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
        (F.map (CategoryTheory.MonoidalCategory.tensorμ W X Y Z)))
-- Mathlib.Order.Preorder.Chain
Flag.ext_iff : ∀ {α : Type u_1} [inst : LE α] {s t : Flag α}, s = t ↔ ↑s = ↑t
-- Mathlib.NumberTheory.ModularForms.LevelOne.Basic
ModularForm.levelOne_weight_zero_rank_one : Module.rank ℂ (ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 0) = 1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Const
Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go_get : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (c : BitVec w) (curr : ℕ)
  (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (hidx : idx < curr),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastConst.go aig c curr s hcurr).get idx ⋯ = s.get idx hidx
-- Mathlib.Algebra.Field.Subfield.Basic
/-- The action by a subfield is the action by the underlying field.  -/
Subfield.instDistribMulActionSubtypeMem : {K : Type u} →
  [inst : DivisionRing K] →
    {X : Type u_1} → [inst_1 : AddMonoid X] → [DistribMulAction K X] → (F : Subfield K) → DistribMulAction (↥F) X
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
/-- *Note: This is a very general combinator that requires an advanced understanding of monads,
dependent types and termination proofs. The variants `filter` and `filterM` are easier to use and
sufficient for most use cases.*

If `it` is an iterator, then `it.filterWithPostcondition f` is another iterator that applies a monadic
predicate `f` to all values emitted by `it` and emits them only if they are accepted by `f`.

`f` is expected to return `PostconditionT n (ULift Bool)`. The base iterator `it` being monadic in
`m`, `n` can be different from `m`, but `it.filterWithPostcondition f` expects a `MonadLiftT m n`
instance. The `PostconditionT` transformer allows the caller to intrinsically prove properties about
`f`'s return value in the monad `n`, enabling termination proofs depending on the specific behavior
of `f`.

**Marble diagram (without monadic effects):**

```text
it                             ---a--b--c--d-e--⊥
it.filterWithPostcondition     ---a-----c-------⊥
```

(given that `f a = f c = pure true` and `f b = f d = d e = pure false`)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and
will always fail, then `it.filterWithPostcondition` will be finite -- and productive -- even if `it`
isn't.

In such situations, the missing instances can be proved manually if the postcondition bundled in
the `PostconditionT n` monad is strong enough. In the given example, a suitable postcondition might
be `fun _ => False`.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
Std.IterM.filterWithPostcondition : {α β : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      [inst : Monad n] →
        [inst_1 : MonadLiftT m n] →
          [Std.Iterator α m β] →
            (f : β → Std.Iterators.PostconditionT n (ULift.{w, 0} Bool)) → Std.IterM m β → Std.IterM n β
-- Mathlib.GroupTheory.FreeGroup.NielsenSchreier
/-- The Nielsen-Schreier theorem: a subgroup of a free group is free.  -/
subgroupIsFreeOfIsFree : ∀ {G : Type u} [inst : Group G] [IsFreeGroup G] (H : Subgroup G), IsFreeGroup ↥H
-- Mathlib.LinearAlgebra.Dual.Basis
Module.DualBases.lc_def : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (e : ι → M) (l : ι →₀ R), Module.DualBases.lc e l = (Finsupp.linearCombination R e) l
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Comonad.Coalgebra.Hom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {G : CategoryTheory.Comonad C} {A B : G.Coalgebra}
  {f : A.A ⟶ B.A}
  {h :
    autoParam (CategoryTheory.CategoryStruct.comp A.a (G.map f) = CategoryTheory.CategoryStruct.comp f B.a)
      CategoryTheory.Comonad.Coalgebra.Hom.h._autoParam}
  {f_1 : A.A ⟶ B.A}
  {h_1 :
    autoParam (CategoryTheory.CategoryStruct.comp A.a (G.map f_1) = CategoryTheory.CategoryStruct.comp f_1 B.a)
      CategoryTheory.Comonad.Coalgebra.Hom.h._autoParam},
  { f := f, h := h } = { f := f_1, h := h_1 } → f = f_1
-- Mathlib.GroupTheory.GroupAction.FixingSubgroup
/-- The submonoid fixing a set under a `MulAction`.  -/
fixingSubmonoid : (M : Type u_1) → {α : Type u_2} → [inst : Monoid M] → [MulAction M α] → Set α → Submonoid M
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefInfo.instInhabitedLocation : Inhabited Lean.Lsp.RefInfo.Location
-- Mathlib.Data.Fintype.Quotient
Quotient.finRecOn.congr_simp : ∀ {ι : Type u_1} [inst : Fintype ι] {inst_1 : DecidableEq ι} [inst_2 : DecidableEq ι] {α : ι → Sort u_2}
  {S : (i : ι) → Setoid (α i)} {C : ((i : ι) → Quotient (S i)) → Sort u_4} (q : (i : ι) → Quotient (S i))
  (f f_1 : (a : (i : ι) → α i) → C fun x => ⟦a x⟧) (e_f : f = f_1)
  (h : ∀ (a b : (i : ι) → α i) (h : ∀ (i : ι), a i ≈ b i), ⋯ ▸ f a = f b),
  Quotient.finRecOn q f h = Quotient.finRecOn q f_1 ⋯
-- Mathlib.RingTheory.Polynomial.Selmer
Polynomial.X_pow_sub_X_sub_one_irreducible_rat : ∀ {n : ℕ}, n ≠ 1 → Irreducible (Polynomial.X ^ n - Polynomial.X - 1)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
/-- The interior of `M × N` is the product of the interiors of `M` and `N`.  -/
ModelWithCorners.interior_prod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {N : Type u_7}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {J : ModelWithCorners 𝕜 E' H'},
  ModelWithCorners.interior (M × N) = ModelWithCorners.interior M ×ˢ ModelWithCorners.interior N
-- Mathlib.Order.Disjointed
sup_Ioc_disjointed_of_monotone : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α] {ι : Type u_3} [inst_1 : LinearOrder ι]
  [inst_2 : LocallyFiniteOrder ι] [inst_3 : OrderBot ι] {f : ι → α},
  Monotone f → ∀ {m n : ι}, n ≤ m → (Finset.Ioc n m).sup (disjointed f) = f m \ f n
-- Mathlib.LinearAlgebra.Matrix.Trace
Matrix.trace_replicateCol_mul_replicateRow : ∀ {n : Type u_3} {R : Type u_6} [inst : Fintype n] {ι : Type u_8} [inst_1 : Unique ι]
  [inst_2 : NonUnitalNonAssocSemiring R] (a b : n → R),
  (Matrix.replicateCol ι a * Matrix.replicateRow ι b).trace = a ⬝ᵥ b
-- Init.Data.BitVec.Lemmas
BitVec.toNat_neg_of_pos : ∀ {n : ℕ} {x : BitVec n}, 0#n < x → (-x).toNat = 2 ^ n - x.toNat
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
AddCommGroup.is_simple_iff_prime_card : ∀ {α : Type u_1} [inst : AddCommGroup α], IsSimpleAddGroup α ↔ Nat.Prime (Nat.card α)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Turing.TM2.stmts₁.match_1.eq_3 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (motive : Turing.TM2.Stmt Γ Λ σ → Sort u_5) (k : K)
  (a : σ → Option (Γ k) → σ) (q : Turing.TM2.Stmt Γ Λ σ)
  (h_1 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Γ k) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.push k a q → motive (Turing.TM2.Stmt.push k a q))
  (h_2 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.peek k a q → motive (Turing.TM2.Stmt.peek k a q))
  (h_3 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (k : K) →
        (a : σ → Option (Γ k) → σ) →
          (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.pop k a q → motive (Turing.TM2.Stmt.pop k a q))
  (h_4 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → σ) → (q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.load a q → motive (Turing.TM2.Stmt.load a q))
  (h_5 :
    (Q : Turing.TM2.Stmt Γ Λ σ) →
      (a : σ → Bool) →
        (q₁ q₂ : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.branch a q₁ q₂ → motive (Turing.TM2.Stmt.branch a q₁ q₂))
  (h_6 : (Q : Turing.TM2.Stmt Γ Λ σ) → (a : σ → Λ) → Q = Turing.TM2.Stmt.goto a → motive (Turing.TM2.Stmt.goto a))
  (h_7 : (Q : Turing.TM2.Stmt Γ Λ σ) → Q = Turing.TM2.Stmt.halt → motive Turing.TM2.Stmt.halt),
  (match Turing.TM2.Stmt.pop k a q with
    | Q@h:(Turing.TM2.Stmt.push k a q) => h_1 Q k a q h
    | Q@h:(Turing.TM2.Stmt.peek k a q) => h_2 Q k a q h
    | Q@h:(Turing.TM2.Stmt.pop k a q) => h_3 Q k a q h
    | Q@h:(Turing.TM2.Stmt.load a q) => h_4 Q a q h
    | Q@h:(Turing.TM2.Stmt.branch a q₁ q₂) => h_5 Q a q₁ q₂ h
    | Q@h:(Turing.TM2.Stmt.goto a) => h_6 Q a h
    | Q@h:Turing.TM2.Stmt.halt => h_7 Q h) =
    h_3 (Turing.TM2.Stmt.pop k a q) k a q ⋯
-- Mathlib.Logic.Equiv.PartialEquiv
Equiv.toPartialEquiv_source : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β), e.toPartialEquiv.source = Set.univ
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- For paths `p q r`, we have a homotopy from `(p.trans q).trans r` to `p.trans (q.trans r)`.  -/
Path.Homotopy.transAssoc : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {x₀ x₁ x₂ x₃ : X} →
      (p : Path x₀ x₁) → (q : Path x₁ x₂) → (r : Path x₂ x₃) → ((p.trans q).trans r).Homotopy (p.trans (q.trans r))
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Closed
ModuleCat.monoidalClosed_uncurry : ∀ {R : Type u} [inst : CommRing R] {M N P : ModuleCat R} (f : N ⟶ M ⟹ P) (x : ↑M) (y : ↑N),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalClosed.uncurry f)) (x ⊗ₜ[R] y) =
    (ModuleCat.Hom.hom ((CategoryTheory.ConcreteCategory.hom f) y)) x
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- A CW complex is of finite type if `cell C n` is finite for every `n`.  -/
Topology.RelCWComplex.FiniteType : {X : Type u} → [inst : TopologicalSpace X] → (C : Set X) → {D : Set X} → [Topology.RelCWComplex C D] → Prop