mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Idempotents
CompleteOrthogonalIdempotents.toOrthogonalIdempotents : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} [inst_1 : Fintype I] {e : I → R},
  CompleteOrthogonalIdempotents e → OrthogonalIdempotents e
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_X_pow : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S) {n : ℕ},
  Polynomial.eval₂ f x (Polynomial.X ^ n) = x ^ n
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.maxDegree_bot_eq_zero : ∀ {V : Type u_1} [inst : Fintype V], ⊥.maxDegree = 0
-- Mathlib.Geometry.Manifold.MFDeriv.Atlas
mdifferentiableAt_extChartAt : ∀ {𝕜 : 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] [IsManifold I 1 M] {x y : M},
  y ∈ (chartAt H x).source → MDiffAt ↑(extChartAt I x) y
-- Mathlib.Algebra.MvPolynomial.Monad
MvPolynomial.join₂_comp_map : ∀ {σ : Type u_1} {R : Type u_3} {S : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  (f : R →+* MvPolynomial σ S), MvPolynomial.join₂.comp (MvPolynomial.map f) = MvPolynomial.bind₂ f
-- Mathlib.RingTheory.Bialgebra.Hom
Bialgebra.counitBialgHom_self : ∀ {R : Type u_1} [inst : CommSemiring R], Bialgebra.counitBialgHom R R = BialgHom.id R R
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.ceil.congr_simp : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι] (m m_1 : E), m = m_1 → ZSpan.ceil b m = ZSpan.ceil b m_1
-- Mathlib.Algebra.Lie.Solvable
LieAlgebra.isSolvableBot : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L], LieAlgebra.IsSolvable ↥⊥
-- Mathlib.GroupTheory.GroupAction.Hom
MulSemiringActionHom.mk.inj : ∀ {M : Type u_1} {inst : Monoid M} {N : Type u_2} {inst_1 : Monoid N} {φ : M →* N} {R : Type u_10} {inst_2 : Semiring R}
  {inst_3 : MulSemiringAction M R} {S : Type u_12} {inst_4 : Semiring S} {inst_5 : MulSemiringAction N S}
  {toDistribMulActionHom : R →ₑ+[φ] S} {map_one' : toDistribMulActionHom.toFun 1 = 1}
  {map_mul' :
    ∀ (x y : R), toDistribMulActionHom.toFun (x * y) = toDistribMulActionHom.toFun x * toDistribMulActionHom.toFun y}
  {toDistribMulActionHom_1 : R →ₑ+[φ] S} {map_one'_1 : toDistribMulActionHom_1.toFun 1 = 1}
  {map_mul'_1 :
    ∀ (x y : R),
      toDistribMulActionHom_1.toFun (x * y) = toDistribMulActionHom_1.toFun x * toDistribMulActionHom_1.toFun y},
  { toDistribMulActionHom := toDistribMulActionHom, map_one' := map_one', map_mul' := map_mul' } =
      { toDistribMulActionHom := toDistribMulActionHom_1, map_one' := map_one'_1, map_mul' := map_mul'_1 } →
    toDistribMulActionHom = toDistribMulActionHom_1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.mem_insertMany_of_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w}
  [inst_2 : ForIn Id ρ ((a : α) × β a)] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : ρ} {k : α}, k ∈ m → k ∈ m.insertMany l
-- Mathlib.Algebra.Group.Submonoid.Defs
AddSubmonoid.instInhabited.eq_1 : ∀ {M : Type u_1} [inst : AddZeroClass M], AddSubmonoid.instInhabited = { default := ⊥ }
-- Mathlib.CategoryTheory.Opposites
/-- The opposite of a functor, i.e. considering a functor `F : C ⥤ D` as a functor `Cᵒᵖ ⥤ Dᵒᵖ`.
In informal mathematics no distinction is made between these.  -/
CategoryTheory.Functor.op : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → CategoryTheory.Functor Cᵒᵖ Dᵒᵖ
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Noncomputably make a limit cone from the existence of unique factorizations.  -/
CategoryTheory.Limits.IsLimit.ofExistsUnique : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cone F} →
            (∀ (s : CategoryTheory.Limits.Cone F),
                ∃! l, ∀ (j : J), CategoryTheory.CategoryStruct.comp l (t.π.app j) = s.π.app j) →
              CategoryTheory.Limits.IsLimit t
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singletonAddMonoidHom.eq_1 : ∀ {α : Type u_2} [inst : AddZeroClass α],
  Set.singletonAddMonoidHom = { toFun := Set.singletonAddHom.toFun, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Data.NNRat.Defs
NNRat.den_ne_zero : ∀ (q : ℚ≥0), q.den ≠ 0
-- Mathlib.RingTheory.WittVector.Basic
WittVector.ghostMap_apply : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x : WittVector p R) (n : ℕ),
  WittVector.ghostMap x n = (WittVector.ghostComponent n) x
-- Mathlib.CategoryTheory.Join.Opposites
/-- The equivalence `(C ⋆ D)ᵒᵖ ≌ Dᵒᵖ ⋆ Cᵒᵖ` induced by `Join.opEquivFunctor` and
`Join.opEquivInverse`.  -/
CategoryTheory.Join.opEquiv : (C : Type u₁) →
  (D : Type u₂) →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (CategoryTheory.Join C D)ᵒᵖ ≌ CategoryTheory.Join Dᵒᵖ Cᵒᵖ
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
coe_nndist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), ↑(nndist x y) = dist x y
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
contMDiffAt_of_subsingleton : ∀ {𝕜 : 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] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M}
  {n : WithTop ℕ∞} [Subsingleton M'], ContMDiffAt I I' n f x
-- Init.Data.Dyadic.Basic
Dyadic.toRat_lt_toRat_iff : ∀ {x y : Dyadic}, x.toRat < y.toRat ↔ x < y
-- Mathlib.Logic.Equiv.Defs
/-- A `Sigma` with `fun i ↦ ULift (PLift (P i))` fibers is equivalent to `{ x // P x }`.
Variant of `sigmaPLiftEquivSubtype`.
 -/
Equiv.sigmaULiftPLiftEquivSubtype : {α : Type v} → (P : α → Prop) → (i : α) × ULift.{u_1, 0} (PLift (P i)) ≃ Subtype P
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Iteration over the iterator `it` in the manner expected by `for` loops.
 -/
Std.IteratorLoop.forIn : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      {inst : Std.Iterator α m β} →
        {n : Type x → Type x'} →
          [self : Std.IteratorLoop α m n] →
            ((γ : Type w) → (δ : Type x) → (γ → n δ) → m γ → n δ) →
              (γ : Type x) →
                (plausible_forInStep : β → γ → ForInStep γ → Prop) →
                  (it : Std.IterM m β) →
                    γ →
                      ((b : β) → it.IsPlausibleIndirectOutput b → (c : γ) → n (Subtype (plausible_forInStep b c))) → n γ
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toSemiring : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → (S : Subalgebra R A) → Semiring ↥S
-- Batteries.Recycling.RBTree.WF
/-- The `balance2` function preserves the ordering invariants.  -/
RBTree.RBNode.Ordered.balance2 : ∀ {α : Type u_1} {cmp : α → α → Ordering} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp x v) l →
    RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp v x) r →
      RBTree.RBNode.Ordered cmp l → RBTree.RBNode.Ordered cmp r → RBTree.RBNode.Ordered cmp (l.balance2 v r)
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.comap_top : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] [inst_7 : IsScalarTower R B B] [inst_8 : SMulCommClass R B B] (f : A →ₙₐ[R] B),
  NonUnitalSubalgebra.comap f ⊤ = ⊤
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_eq_integral_pos_part_sub_integral_neg_part : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.Integrable f μ → ∫ (a : α), f a ∂μ = ∫ (a : α), ↑(f a).toNNReal ∂μ - ∫ (a : α), ↑(-f a).toNNReal ∂μ
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.coe_preimage_infty : ∀ {X : Type u_1}, OnePoint.some ⁻¹' {OnePoint.infty} = ∅
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.skeleton_obj_eq_top : ∀ (X : SSet) {d n : ℕ}, d < n → (X.skeleton n).obj (Opposite.op { len := d }) = ⊤
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.LoogleResult.failure.injEq : ∀ (error : String) (suggestions : Option (List String)) (error_1 : String) (suggestions_1 : Option (List String)),
  (LeanSearchClient.LoogleResult.failure error suggestions =
      LeanSearchClient.LoogleResult.failure error_1 suggestions_1) =
    (error = error_1 ∧ suggestions = suggestions_1)
-- Lean.Parser.Extension
Lean.Parser.compileParserDescr : Lean.Parser.ParserCategories → Lean.ParserDescr → Lean.ImportM Lean.Parser.Parser
-- Lean.Server.InfoUtils
Lean.Elab.Info.lctx : Lean.Elab.Info → Lean.LocalContext
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.whiskerLeft_natTransExtension : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] {F G : CategoryTheory.Functor W.Localization D}
  (τ : W.Q.comp F ⟶ W.Q.comp G), W.Q.whiskerLeft (CategoryTheory.Localization.Construction.natTransExtension τ) = τ
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.j_compHom : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] {c₁ c₂ c₃ : R} (q : QuaternionAlgebra.Basis A c₁ c₂ c₃) (F : A →ₐ[R] B),
  (q.compHom F).j = F q.j
-- Mathlib.Data.Set.Lattice
Set.pi_def : ∀ {α : Type u_1} {π : α → Type u_12} (i : Set α) (s : (a : α) → Set (π a)), i.pi s = ⋂ a ∈ i, Function.eval a ⁻¹' s a
-- Lean.Data.Json.Basic
Lean.JsonNumber.exponent : Lean.JsonNumber → ℕ
-- Mathlib.Topology.Connected.Clopen
/-- In a preconnected space, any finite disjoint cover by non-empty closed subsets has at most one
element.  -/
subsingleton_of_disjoint_isClosed_iUnion_eq_univ : ∀ {α : Type u} {ι : Type u_1} [inst : TopologicalSpace α] [PreconnectedSpace α] {s : ι → Set α},
  (∀ (i : ι), (s i).Nonempty) →
    Pairwise (Function.onFun Disjoint s) →
      ∀ [Finite ι], (∀ (i : ι), IsClosed (s i)) → ⋃ i, s i = Set.univ → Subsingleton ι
-- Mathlib.Data.Matrix.Basis
Matrix.submatrix_single_equiv : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_7} [inst : DecidableEq l]
  [inst_1 : DecidableEq m] [inst_2 : DecidableEq n] [inst_3 : DecidableEq o] [inst_4 : Zero α] (f : l ≃ n) (g : m ≃ o)
  (i : n) (j : o) (r : α), (Matrix.single i j r).submatrix ⇑f ⇑g = Matrix.single (f.symm i) (g.symm j) r
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
Finsupp.DegLex.wellFounded : ∀ {α : Type u_1} {r : α → α → Prop} [Std.Trichotomous r],
  WellFounded (Function.swap r) →
    ∀ {s : ℕ → ℕ → Prop}, WellFounded s → (∀ ⦃n : ℕ⦄, ¬s n 0) → WellFounded (Finsupp.DegLex r s)
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_le : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {f : M →ₗ[R] N →ₗ[R] P} {p : Submodule R M} {q : Submodule R N} {r : Submodule R P},
  Submodule.map₂ f p q ≤ r ↔ ∀ m ∈ p, ∀ n ∈ q, (f m) n ∈ r
-- Mathlib.NumberTheory.Modular
ModularGroup.three_lt_four_mul_im_sq_of_mem_fdo : ∀ {z : UpperHalfPlane}, z ∈ ModularGroup.fdo → 3 < 4 * z.im ^ 2
-- Mathlib.RingTheory.KrullDimension.Field
ringKrullDim_eq_zero_of_field : ∀ (F : Type u_1) [inst : Field F], ringKrullDim F = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- `HasImageMap sq` means that there is an `ImageMap` for the square `sq`.  -/
CategoryTheory.Limits.HasImageMap.has_image_map : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {f g : CategoryTheory.Arrow C}
  {inst_1 : CategoryTheory.Limits.HasImage f.hom} {inst_2 : CategoryTheory.Limits.HasImage g.hom} {sq : f ⟶ g}
  [self : CategoryTheory.Limits.HasImageMap sq], Nonempty (CategoryTheory.Limits.ImageMap sq)
-- Init.Data.List.Find
List.isSome_findSome? : ∀ {α : Type u_1} {β : Type u_2} {xs : List α} {f : α → Option β},
  (List.findSome? f xs).isSome = xs.any fun x => (f x).isSome
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_nonpos : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, a - b ≤ 0 ↔ a ≤ b
-- Mathlib.Data.List.Lookmap
List.lookmap.go.eq_def : ∀ {α : Type u_1} (f : α → Option α) (a : List α) (a_1 : Array α),
  List.lookmap.go f a a_1 =
    match a, a_1 with
    | [], acc => acc.toList
    | a :: l, acc =>
      match f a with
      | some b => acc.toListAppend (b :: l)
      | none => List.lookmap.go f l (acc.push a)
-- Init.Data.UInt.Lemmas
UInt16.neg_sub : ∀ {a b : UInt16}, -(a - b) = b - a
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imI_coe : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (x : R) [inst : Zero R], (↑x).imI = 0
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.ReflQuiv.forget_forgetToQuiv : CategoryTheory.ReflQuiv.forget.comp CategoryTheory.ReflQuiv.forgetToQuiv = CategoryTheory.Quiv.forget
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.differentiableOn_one_add_smoothingFn : DifferentiableOn ℝ (fun z => 1 + AkraBazziRecurrence.smoothingFn z) (Set.Ioi 1)
-- Lean.Data.DeclarationRange
/-- A precomputed UTF-16 `character` field as in `Lean.Lsp.Position`. We need to store this
because LSP clients want us to report the range in terms of UTF-16, but converting a Unicode
codepoint stored in `Lean.Position` to UTF-16 requires loading and mapping the target source
file, which is IO-heavy.  -/
Lean.DeclarationRange.charUtf16 : Lean.DeclarationRange → ℕ
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- The carrier of `(coextendScalars f).obj M` is `S →ₗ[R] M` where `S` is considered as an
`R`-module via restriction of scalars.  -/
ModuleCat.CoextendScalars.equiv : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          (M : ModuleCat R) →
            ↑((ModuleCat.coextendScalars f).obj M) ≃ₗ[S]
              ↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) →ₗ[R] ↑M
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.mk' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (obj₁ obj₂ obj₃ : C) →
        (obj₁ ⟶ obj₂) →
          (obj₂ ⟶ obj₃) →
            (obj₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj obj₁) → CategoryTheory.Pretriangulated.Triangle C
-- Mathlib.Topology.Bornology.Constructions
instBoundedSpaceOrderDual : ∀ {α : Type u_1} [inst : Bornology α] [BoundedSpace α], BoundedSpace αᵒᵈ
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.Monoidal.whiskerRight_η_ε_assoc : ∀ {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) [inst_4 : F.Monoidal] (T : D) {Z : D}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) T ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.OplaxMonoidal.η F) T)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.ε F) T) h) =
    h
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
DirectedOn.notMem_of_lt_csInf : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {x : α} {s : Set α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s → x < sInf s → BddBelow s → x ∉ s
-- Mathlib.LinearAlgebra.Basis.Submodule
/-- Let `b` be an `S`-basis of `M`. Then `m : M` lies in the `R`-module spanned by `b` iff all the
coordinates of `m` on the basis `b` are in `R` (see `Basis.mem_span` for the case `R = S`).  -/
Module.Basis.mem_span_iff_repr_mem : ∀ {ι : Type u_1} (R : Type u_3) {M : Type u_5} {S : Type u_7} [inst : CommRing R] [IsDomain R] [inst_2 : Ring S]
  [Nontrivial S] [inst_4 : AddCommGroup M] [inst_5 : Algebra R S] [inst_6 : Module S M] [inst_7 : Module R M]
  [IsScalarTower R S M] [Module.IsTorsionFree R S] (b : Module.Basis ι S M) (m : M),
  m ∈ Submodule.span R (Set.range ⇑b) ↔ ∀ (i : ι), (b.repr m) i ∈ Set.range ⇑(algebraMap R S)
-- Mathlib.Tactic.Linter.TextBased
Mathlib.Linter.TextBased.instBEqErrorFormat.beq : Mathlib.Linter.TextBased.ErrorFormat → Mathlib.Linter.TextBased.ErrorFormat → Bool
-- Batteries.Data.DList.Lemmas
Batteries.DList.toList_empty : ∀ {α : Type u_1}, Batteries.DList.empty.toList = []
-- Mathlib.Data.List.Iterate
List.length_iterate : ∀ {α : Type u_1} (f : α → α) (a : α) (n : ℕ), (List.iterate f a n).length = n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ReferenceContext.includeDeclaration : Lean.Lsp.ReferenceContext → Bool
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMonNatIso_hom_app_hom : ∀ {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 F' : CategoryTheory.Functor C D} [inst_4 : F.LaxMonoidal] [inst_5 : F'.LaxMonoidal] (e : F ≅ F')
  [inst_6 : CategoryTheory.NatTrans.IsMonoidal e.hom] (X : CategoryTheory.Mon C),
  ((CategoryTheory.Functor.mapMonNatIso e).hom.app X).hom = e.hom.app X.X
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensorMonoidal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → (CategoryTheory.MonoidalCategory.tensor C).Monoidal
-- Mathlib.Data.Real.ConjExponents
Real.HolderConjugate.conjugate_eq : ∀ {p q : ℝ}, p.HolderConjugate q → q = p / (p - 1)
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
/-- The map over a ring homomorphism of a change of variables is a group homomorphism.  -/
WeierstrassCurve.VariableChange.mapHom : {R : Type u} →
  [inst : CommRing R] →
    {A : Type v} →
      [inst_1 : CommRing A] → (R →+* A) → WeierstrassCurve.VariableChange R →* WeierstrassCurve.VariableChange A
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousLinearEquiv.continuousMultilinearMapCongrLeft_apply : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {E₁ : ι → Type u_4} {F : Type u_5} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : (i : ι) → TopologicalSpace (E₁ i)]
  [inst_5 : (i : ι) → AddCommGroup (E₁ i)] [inst_6 : (i : ι) → Module 𝕜 (E₁ i)] [inst_7 : AddCommGroup F]
  [inst_8 : Module 𝕜 F] [inst_9 : TopologicalSpace F] [inst_10 : IsTopologicalAddGroup F]
  [inst_11 : ContinuousConstSMul 𝕜 F] (g : ContinuousMultilinearMap 𝕜 E₁ F) (f : (i : ι) → E i ≃L[𝕜] E₁ i),
  (ContinuousLinearEquiv.continuousMultilinearMapCongrLeft F f) g = g.compContinuousLinearMap fun i => ↑(f i)
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.BitVec.ite_else_not_ite : ∀ {w : ℕ} (cond : Bool) {a b c : BitVec w}, (bif cond then a else ~~~bif cond then b else c) = bif cond then a else ~~~c
-- Mathlib.RingTheory.MvPowerSeries.Equiv
PowerSeries.toMvPowerSeries_eq_subst : ∀ {σ : Type u_2} {R : Type u_4} [inst : CommRing R] {f : PowerSeries R} {i : σ},
  (PowerSeries.toMvPowerSeries i) f = PowerSeries.subst (MvPowerSeries.X i) f
-- Mathlib.Topology.Algebra.Group.Basic
Filter.map_mul_left_nhdsGT : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : CommGroup H] [inst_2 : PartialOrder H] [IsOrderedMonoid H]
  [ContinuousMul H] {c a : H},
  Filter.map (fun x => c * x) (nhdsWithin a (Set.Ioi a)) = nhdsWithin (c * a) (Set.Ioi (c * a))
-- Init.Grind.AC
Lean.Grind.AC.instLawfulBEqSeq : LawfulBEq Lean.Grind.AC.Seq
-- Mathlib.GroupTheory.Submonoid.Inverses
Submonoid.leftInv_eq_inv : ∀ {M : Type u_1} [inst : Group M] (S : Submonoid M), S.leftInv = S⁻¹
-- Mathlib.Topology.Algebra.Monoid
Inseparable.pow : ∀ {M : Type u_6} [inst : Monoid M] [inst_1 : TopologicalSpace M] [ContinuousMul M] {a b : M},
  Inseparable a b → ∀ (n : ℕ), Inseparable (a ^ n) (b ^ n)
-- Lean.Meta.Tactic.Grind.MatchCond
_private.Lean.Meta.Tactic.Grind.MatchCond.0.Lean.Meta.Grind.collectMatchCondLhssAndAbstract.go.match_3.eq_1 : ∀ (motive : Lean.Expr × Option Lean.Expr → Sort u_1) (lhs : Lean.Expr) (α? : Option Lean.Expr)
  (h_1 : (lhs : Lean.Expr) → (α? : Option Lean.Expr) → motive (lhs, α?)),
  (match (lhs, α?) with
    | (lhs, α?) => h_1 lhs α?) =
    h_1 lhs α?
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.le_maxKeyD_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  t.contains k = true → ∀ {fallback : α}, (cmp k (t.maxKeyD fallback)).isLE = true
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Localization.mulEquivOfQuotient_mk' : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  {f : S.LocalizationMap N} (x : M) (y : ↥S),
  (Localization.mulEquivOfQuotient f) ((Localization.monoidOf S).mk' x y) = f.mk' x y
-- Mathlib.GroupTheory.OrderOfElement
pow_ne_one_of_lt_orderOf : ∀ {G : Type u_1} [inst : Monoid G] {x : G} {n : ℕ}, n ≠ 0 → n < orderOf x → x ^ n ≠ 1
-- Mathlib.Analysis.Calculus.Deriv.Basic
/-- Expressing `HasDerivAt f f' x` in terms of `HasFDerivAt`  -/
hasDerivAt_iff_hasFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] {f : 𝕜 → F} {x : 𝕜} [inst_4 : ContinuousSMul 𝕜 F] {f' : F},
  HasDerivAt f f' x ↔ HasFDerivAt f (ContinuousLinearMap.toSpanSingleton 𝕜 f') x
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {k a : α},
  Std.ExtDHashMap.Const.get! (m.erase k) a = if (k == a) = true then default else Std.ExtDHashMap.Const.get! m a
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.isCursorOnWhitespace : Lean.FileMap → String.Pos.Raw → Bool
-- Lean.CoreM
Lean.Core.State.mk : Lean.Environment →
  Lean.MacroScope →
    Lean.NameGenerator →
      Lean.DeclNameGenerator →
        Lean.TraceState →
          Lean.Core.Cache →
            Lean.MessageLog →
              Lean.Elab.InfoState → Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree) → Lean.Core.State
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A finite union of countably compact sets is countably compact.  -/
Set.Finite.isCountablyCompact_sUnion : ∀ {E : Type u_2} [inst : TopologicalSpace E] {S : Set (Set E)},
  S.Finite → (∀ s ∈ S, IsCountablyCompact s) → IsCountablyCompact (⋃₀ S)
-- Mathlib.FieldTheory.Minpoly.Basic
/-- The degree of a minimal polynomial, as a natural number, is positive.  -/
minpoly.natDegree_pos : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Algebra A B] {x : B} [Nontrivial B],
  IsIntegral A x → 0 < (minpoly A x).natDegree
-- Mathlib.Order.Hom.Lattice
LatticeHom.toSupHom : {α : Type u_6} → {β : Type u_7} → [inst : Lattice α] → [inst_1 : Lattice β] → LatticeHom α β → SupHom α β