mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonRenameFile : Lean.ToJson Lean.Lsp.RenameFile
-- Mathlib.Algebra.GroupWithZero.Units.Equiv
mulLeft_bijective₀ : ∀ {G₀ : Type u_1} [inst : GroupWithZero G₀] (a : G₀), a ≠ 0 → Function.Bijective fun x => a * x
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coeToSubmodule_injective : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  Function.Injective fun I => ↑I
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {pullback : C}
  {p₁ : pullback ⟶ X₁} {p₂ : pullback ⟶ X₂}
  {condition : CategoryTheory.CategoryStruct.comp p₁ f₁ = CategoryTheory.CategoryStruct.comp p₂ f₂}
  {isLimit : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk p₁ p₂ condition)} {p : pullback ⟶ S}
  {hp₁ : autoParam (CategoryTheory.CategoryStruct.comp p₁ f₁ = p) CategoryTheory.Limits.ChosenPullback.hp₁._autoParam}
  {pullback_1 : C} {p₁_1 : pullback_1 ⟶ X₁} {p₂_1 : pullback_1 ⟶ X₂}
  {condition_1 : CategoryTheory.CategoryStruct.comp p₁_1 f₁ = CategoryTheory.CategoryStruct.comp p₂_1 f₂}
  {isLimit_1 : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk p₁_1 p₂_1 condition_1)}
  {p_1 : pullback_1 ⟶ S}
  {hp₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp p₁_1 f₁ = p_1) CategoryTheory.Limits.ChosenPullback.hp₁._autoParam},
  { pullback := pullback, p₁ := p₁, p₂ := p₂, condition := condition, isLimit := isLimit, p := p, hp₁ := hp₁ } =
      { pullback := pullback_1, p₁ := p₁_1, p₂ := p₂_1, condition := condition_1, isLimit := isLimit_1, p := p_1,
        hp₁ := hp₁_1 } →
    pullback = pullback_1 ∧ p₁ ≍ p₁_1 ∧ p₂ ≍ p₂_1 ∧ isLimit ≍ isLimit_1 ∧ p ≍ p_1
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- This prevents `toAbs p x` being printed as `{ ofAbs := x }` by `delabStructureInstance`.  -/
WithAbs.delabToAbs : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.inv_iInf : ∀ {G : Type u_2} [inst : Group G] {ι : Sort u_7} (S : ι → Submonoid G), (⨅ i, S i)⁻¹ = ⨅ i, (S i)⁻¹
-- Mathlib.Algebra.BigOperators.Pi
prod_mk_sum : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N] (s : Finset ι)
  (f : ι → M) (g : ι → N), (∑ x ∈ s, f x, ∑ x ∈ s, g x) = ∑ x ∈ s, (f x, g x)
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.instFaithfulSigmaIncl : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] (i : I),
  (CategoryTheory.Sigma.incl i).Faithful
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- A functor preserves the left homology of a short complex `S` if it preserves all the
left homology data of `S`.  -/
CategoryTheory.Functor.PreservesLeftHomologyOf : {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.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) → [F.PreservesZeroMorphisms] → CategoryTheory.ShortComplex C → Prop
-- Lean.Elab.Tactic.Induction
_private.Lean.Elab.Tactic.Induction.0.Lean.Elab.Tactic.ElimApp.State.targetPos : Lean.Elab.Tactic.ElimApp.State✝ → ℕ
-- Mathlib.Topology.Algebra.Group.Torsor
/-- The underlying group of a topological torsor is a topological group. This is not an instance, as
`P` cannot be inferred.  -/
IsTopologicalTorsor.to_isTopologicalGroup : ∀ (V : Type u_1) (P : Type u_2) [inst : Group V] [inst_1 : TopologicalSpace V] [inst_2 : Torsor V P]
  [inst_3 : TopologicalSpace P] [IsTopologicalTorsor P], IsTopologicalGroup V
-- Mathlib.CategoryTheory.Category.Basic
/-- We also use `aesop_cat?` to pass along a `Try this` suggestion when using `aesop_cat`
 -/
CategoryTheory.aesop_cat? : Lean.ParserDescr
-- Mathlib.Order.Hom.Bounded
BotHom.cancel_left : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Bot α] [inst_1 : Bot β] [inst_2 : Bot γ] {g : BotHom β γ}
  {f₁ f₂ : BotHom α β}, Function.Injective ⇑g → (g.comp f₁ = g.comp f₂ ↔ f₁ = f₂)
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.isSelfAdjoint_realToRCLike : ∀ {X : Type u_1} (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜] {f : C(X, ℝ)},
  IsSelfAdjoint (ContinuousMap.realToRCLike 𝕜 f)
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.map_comp : ∀ {K : Type u_1} {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {L : Type u_3}
  {W : Type u_4} [inst_3 : DivisionRing L] [inst_4 : AddCommGroup W] [inst_5 : Module L W] {F : Type u_5} {U : Type u_6}
  [inst_6 : DivisionRing F] [inst_7 : AddCommGroup U] [inst_8 : Module F U] {σ : K →+* L} {τ : L →+* F} {γ : K →+* F}
  [inst_9 : RingHomCompTriple σ τ γ] (f : V →ₛₗ[σ] W) (hf : Function.Injective ⇑f) (g : W →ₛₗ[τ] U)
  (hg : Function.Injective ⇑g) (hgf : optParam (Function.Injective ⇑(g ∘ₛₗ f)) ⋯),
  Projectivization.map (g ∘ₛₗ f) hgf = Projectivization.map g hg ∘ Projectivization.map f hf
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_union_of_not_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (∀ a ∈ m₁, a ∉ m₂) → (m₁ ∪ m₂).size = m₁.size + m₂.size
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightEq_hom_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso] (r r' : R₁ ⟶ R₂) (h : r = r')
  (hr :
    ∀ (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
      P (CategoryTheory.CategoryStruct.comp X.hom (r.app X.right)))
  (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightEq L r r' h hr).hom.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.smul_integral_comp_mul_right : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (c : ℝ),
  c • ∫ (x : ℝ) in a..b, f (x * c) = ∫ (x : ℝ) in a * c..b * c, f x
-- Mathlib.Combinatorics.Enumerative.Bell
Nat.uniformBell_mul_eq : ∀ (m : ℕ) {n : ℕ}, n ≠ 0 → m.uniformBell n * n.factorial ^ m * m.factorial = (m * n).factorial
-- Mathlib.Order.WithBot
WithBot.le_def' : ∀ {α : Type u_1} [inst : LE α] {x y : WithBot α}, y ≤ x ↔ y = ⊥ ∨ ∃ a, ∃ b ≤ a, x = ↑a ∧ y = ↑b
-- Init.Data.UInt.Lemmas
UInt32.toUInt64_ofNat' : ∀ {n : ℕ}, n < UInt32.size → (UInt32.ofNat n).toUInt64 = UInt64.ofNat n
-- Std.Data.ExtTreeMap.Basic
/-- Inserts the given mapping into the map. If there is already a mapping for the given key, then both
key and value will be replaced.
 -/
Std.ExtTreeMap.insert : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → β → Std.ExtTreeMap α β cmp
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of the sum of two formal power series
is at least the minimum of their orders.  -/
PowerSeries.min_order_le_order_add : ∀ {R : Type u_1} [inst : Semiring R] (φ ψ : PowerSeries R), min φ.order ψ.order ≤ (φ + ψ).order
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.comap_embedding_of_isReal : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] (f : k →+* K) {w : NumberField.InfinitePlace K},
  (w.comap f).IsReal → (w.comap f).embedding = w.embedding.comp f
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.stronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  (f : α →ₘ[μ] β), MeasureTheory.StronglyMeasurable ↑f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α],
  m₁.WF → m₂.WF → ∀ {k : α}, (m₁ ∩ m₂).getKey! k = if k ∈ m₂ then m₁.getKey! k else default
-- Mathlib.Topology.DiscreteQuotient
/-- Construct a discrete quotient from a clopen set.  -/
DiscreteQuotient.ofIsClopen : {X : Type u_2} → [inst : TopologicalSpace X] → {A : Set X} → IsClopen A → DiscreteQuotient X
-- Mathlib.Analysis.Convex.Segment
/-- A point is in an `Ico` iff it can be expressed as a semistrict convex combination of the
endpoints.  -/
Convex.mem_Ico : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {x y z : 𝕜},
  x < y → (z ∈ Set.Ico x y ↔ ∃ a b, 0 < a ∧ 0 ≤ b ∧ a + b = 1 ∧ a * x + b * y = z)
-- Mathlib.AlgebraicGeometry.Normalization
AlgebraicGeometry.Scheme.Hom.normalizationDesc_comp : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.QuasiCompact f]
  [inst_1 : AlgebraicGeometry.QuasiSeparated f] {T : AlgebraicGeometry.Scheme} (f₁ : X ⟶ T) (f₂ : T ⟶ Y)
  [inst_2 : AlgebraicGeometry.IsIntegralHom f₂] (H : f = CategoryTheory.CategoryStruct.comp f₁ f₂),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.normalizationDesc f f₁ f₂ H) f₂ =
    AlgebraicGeometry.Scheme.Hom.fromNormalization f
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.zero_ne_one_cert : Lean.Grind.Linarith.Poly → Bool
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.δ.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
  X.δ f g = X.δ'.app (CategoryTheory.ComposableArrows.mk₂ f g)
-- Mathlib.RepresentationTheory.Homological.ContCohomology.Basic
TopRep.resolution'd_eq : ∀ {k : Type u_1} {G : Type u_2} [inst : Ring k] [inst_1 : Group G] [inst_2 : TopologicalSpace k]
  [inst_3 : TopologicalSpace G] [inst_4 : IsTopologicalGroup G] (X : TopRep k G) (n : ℕ), X.resolution'd n = X.d (n + 1)
-- Mathlib.Topology.Algebra.Group.Pointwise
mul_singleton_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Group α] [ContinuousConstSMul αᵐᵒᵖ α] {s : Set α} (a : α) {b : α},
  s ∈ nhds b → s * {a} ∈ nhds (b * a)
-- Mathlib.RingTheory.Length
Module.coe_length : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  ↑(Module.length R M) = Order.krullDim (Submodule R M)
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.base_start : ∀ {pat s : String.Slice} (h : pat.isEmpty = false),
  String.Slice.Pattern.Model.ForwardSliceSearcher.Invariants.base✝ ⋯ = s.startPos
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- a triangle is distinguished iff it is so after rotating it  -/
CategoryTheory.Pretriangulated.rotate_distinguished_triangle : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Limits.HasZeroObject C}
  {inst_2 : CategoryTheory.HasShift C ℤ} {inst_3 : CategoryTheory.Preadditive C}
  {inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive} [self : CategoryTheory.Pretriangulated C]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔
    T.rotate ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Init.Prelude
/-- A potential namespace reference  -/
Lean.Syntax.Preresolved.namespace : Lean.Name → Lean.Syntax.Preresolved
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
OpenPartialHomeomorph.ofSet_trans' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {s : Set X} (hs : IsOpen s),
  (OpenPartialHomeomorph.ofSet s hs).trans e = e.restr (e.source ∩ s)
-- Mathlib.Algebra.Algebra.Opposite
/-- An algebra is isomorphic to the opposite of its opposite.  -/
AlgEquiv.opOp : (R : Type u_1) →
  (A : Type u_3) → [inst : CommSemiring R] → [inst_1 : Semiring A] → [inst_2 : Algebra R A] → A ≃ₐ[R] Aᵐᵒᵖᵐᵒᵖ
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Hom.isoImage_inv_homOfLE : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (U V : X.Opens) (e : U ≤ V),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.isoImage f U).inv (X.homOfLE e) =
    CategoryTheory.CategoryStruct.comp (Y.homOfLE ⋯) (AlgebraicGeometry.Scheme.Hom.isoImage f V).inv
-- Mathlib.GroupTheory.NoncommPiCoprod
/-- The canonical homomorphism from a family of monoids.  -/
MonoidHom.noncommPiCoprod : {M : Type u_1} →
  [inst : Monoid M] →
    {ι : Type u_2} →
      [Fintype ι] →
        {N : ι → Type u_3} →
          [inst_2 : (i : ι) → Monoid (N i)] →
            (ϕ : (i : ι) → N i →* M) →
              (Pairwise fun i j => ∀ (x : N i) (y : N j), Commute ((ϕ i) x) ((ϕ j) y)) → ((i : ι) → N i) →* M
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
/-- The construction `CatCommSqOver.transform` respects the identity
`CatCospanTransform`s.  -/
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjId : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            (X : Type u₄) →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} X] →
                (F : CategoryTheory.Functor A B) →
                  (G : CategoryTheory.Functor C B) →
                    (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj
                        (CategoryTheory.Limits.CatCospanTransform.id F G) ≅
                      CategoryTheory.Functor.id (CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G X)
-- Mathlib.Data.ENat.Basic
ENat.mul_le_mul_right_iff : ∀ {a x y : ℕ∞}, a ≠ 0 → a ≠ ⊤ → (x * a ≤ y * a ↔ x ≤ y)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.inclusion_injective : ∀ {M : Type u_1} {α : Type u_2} [inst : AddMonoid M] [inst_1 : AddAction M α] (s : SubAddAction M α),
  Function.Injective ⇑s.inclusion
-- Mathlib.Combinatorics.Matroid.Basic
/-- Every base is contained in the ground set.  -/
Matroid.subset_ground : ∀ {α : Type u_1} (self : Matroid α) (B : Set α), self.IsBase B → B ⊆ self.E
-- Mathlib.Analysis.Normed.Group.Defs
/-- Construct a `NormedAddCommGroup` from a
`SeminormedAddCommGroup` satisfying `∀ x, ‖x‖ = 0 → x = 0`. This avoids having to go back to the
`(Pseudo)MetricSpace` level when declaring a `NormedAddCommGroup` instance as a special case
of a more general `SeminormedAddCommGroup` instance.  -/
NormedAddCommGroup.ofSeparation : {E : Type u_5} → [inst : SeminormedAddCommGroup E] → (∀ (x : E), ‖x‖ = 0 → x = 0) → NormedAddCommGroup E
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.ZNum.zNeg.match_1.eq_3 : ∀ (motive : ZNum → Sort u_1) (a : PosNum) (h_1 : Unit → motive ZNum.zero) (h_2 : (a : PosNum) → motive (ZNum.pos a))
  (h_3 : (a : PosNum) → motive (ZNum.neg a)),
  (match ZNum.neg a with
    | ZNum.zero => h_1 ()
    | ZNum.pos a => h_2 a
    | ZNum.neg a => h_3 a) =
    h_3 a
-- Mathlib.CategoryTheory.Limits.ConcreteCategory.Filtered
CategoryTheory.Limits.IsColimit.eq_iff : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C] {FC : C → C → Type u_3} {CC : C → Type u_4}
  [inst_2 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_3 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.PreservesColimitsOfShape J (CategoryTheory.forget C)] (F : CategoryTheory.Functor J C)
  [CategoryTheory.IsFilteredOrEmpty J] {t : CategoryTheory.Limits.Cocone F} (ht : CategoryTheory.Limits.IsColimit t)
  {i j : J} {xi : CategoryTheory.ToType (F.obj i)} {xj : CategoryTheory.ToType (F.obj j)},
  (CategoryTheory.ConcreteCategory.hom (t.ι.app i)) xi = (CategoryTheory.ConcreteCategory.hom (t.ι.app j)) xj ↔
    ∃ k f g, (CategoryTheory.ConcreteCategory.hom (F.map f)) xi = (CategoryTheory.ConcreteCategory.hom (F.map g)) xj
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
Matrix.isRepresentation.eq_toEnd_of_represents : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : Module R M] (b : ι → M) [inst_4 : DecidableEq ι] (hb : Submodule.span R (Set.range b) = ⊤)
  (A : ↥(Matrix.isRepresentation R b)) {f : Module.End R M},
  Matrix.Represents b (↑A) f → (Matrix.isRepresentation.toEnd R b hb) A = f
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.instFastSubsingletonForall : ∀ {α : Sort u} {β : α → Sort v} [inst : ∀ (x : α), Lean.Meta.FastSubsingleton (β x)],
  Lean.Meta.FastSubsingleton ((x : α) → β x)
-- Mathlib.RingTheory.RingHom.StandardSmooth
Algebra.Generators.ofSurjective.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (val : ι → S)
  (h : Function.Surjective ⇑(MvPolynomial.aeval val)),
  Algebra.Generators.ofSurjective val h = { val := val, σ' := fun x => ⋯.choose, aeval_val_σ' := ⋯, algebraMap_eq := ⋯ }
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.norm.eq_1 : Lean.Grind.Linarith.Poly.nil.norm = Lean.Grind.Linarith.Poly.nil
-- Mathlib.RepresentationTheory.Basic
Representation.instAddCommGroupAsModule : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Ring k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommGroup V] → [inst_3 : Module k V] → (ρ : Representation k G V) → AddCommGroup ρ.asModule
-- Mathlib.Probability.Moments.Basic
/-- Moment-generating function of a real random variable `X`: `fun t => μ[exp(t*X)]`.  -/
ProbabilityTheory.mgf : {Ω : Type u_1} → {m : MeasurableSpace Ω} → (Ω → ℝ) → MeasureTheory.Measure Ω → ℝ → ℝ
-- Mathlib.LinearAlgebra.Matrix.Invertible
/-- A copy of `mul_invOf_cancel_left` for rectangular matrices.  -/
Matrix.mul_invOf_cancel_left : ∀ {m : Type u_1} {n : Type u_2} {α : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring α]
  (A : Matrix n n α) (B : Matrix n m α) [inst_3 : Invertible A], A * (⅟A * B) = B
-- Mathlib.CategoryTheory.Adjunction.Parametrized
CategoryTheory.ParametrizedAdjunction.homEquiv_naturality_one : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {X₂ : C₂} {X₃ : C₃}
  (f₁ : X₁ ⟶ Y₁) (g : (F.obj Y₁).obj X₂ ⟶ X₃),
  adj₂.homEquiv (CategoryTheory.CategoryStruct.comp ((F.map f₁).app X₂) g) =
    CategoryTheory.CategoryStruct.comp (adj₂.homEquiv g) ((G.map f₁.op).app X₃)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.mk'_one_X_pow : ∀ {R : Type u_1} [inst : CommSemiring R] (n : ℕ),
  IsLocalization.mk' (LaurentPolynomial R) 1 ⟨Polynomial.X ^ n, ⋯⟩ = LaurentPolynomial.T (-↑n)
-- Mathlib.Data.Set.Image
Set.exists_range_iff : ∀ {α : Type u_1} {ι : Sort u_4} {f : ι → α} {p : α → Prop}, (∃ a ∈ Set.range f, p a) ↔ ∃ i, p (f i)
-- Mathlib.Analysis.LocallyConvex.Montel
MontelSpace.isCompact_of_isClosed_of_isVonNBounded : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : Zero E] [inst_2 : SMul 𝕜 E]
  [inst_3 : TopologicalSpace E] [hm : MontelSpace 𝕜 E] {s : Set E},
  IsClosed s → Bornology.IsVonNBounded 𝕜 s → IsCompact s
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.continuous_comp_left : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : AddMonoid C]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace C] (f : A →ₜ+ B),
  Continuous fun g => g.comp f
-- Mathlib.Data.Fintype.Card
Fintype.card_eq_zero_iff : ∀ {α : Type u_1} [inst : Fintype α], Fintype.card α = 0 ↔ IsEmpty α
-- Mathlib.Computability.Primrec.Basic
primrecPred_iff_primrec_decide : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop} [inst_1 : DecidablePred p],
  PrimrecPred p ↔ Primrec fun a => decide (p a)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.himp_ofProp : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)]
  {φ₁ φ₂ : Prop},
  Lean.Order.himp (Lean.Order.CompleteLattice.ofProp φ₁) (Lean.Order.CompleteLattice.ofProp φ₂) =
    Lean.Order.CompleteLattice.ofProp (φ₁ → φ₂)
-- Mathlib.Order.Filter.IsBounded
Filter.IsBoundedUnder.mono_ge : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {l : Filter α} {u v : α → β},
  Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l u → u ≤ᶠ[l] v → Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l v
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Specialize.pure_taut : ∀ {σs : List (Type u_1)} {φ : Prop} {P : Std.Do.SPred σs} [Std.Do.SPred.Tactic.IsPure P φ], φ → ⊢ₛ P
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
zsmul_nonneg : ∀ {G : Type u_2} [inst : SubNegMonoid G] [inst_1 : Preorder G] [AddLeftMono G] {x : G},
  0 ≤ x → ∀ {n : ℤ}, 0 ≤ n → 0 ≤ n • x
-- Mathlib.Data.PFunctor.Univariate.M
/-- The tails are equal  -/
PFunctor.M.IsBisimulation.tail : ∀ {F : PFunctor.{uA, uB}} {R : F.M → F.M → Prop},
  PFunctor.M.IsBisimulation R →
    ∀ {a : F.A} {f f' : F.B a → F.M}, R (PFunctor.M.mk ⟨a, f⟩) (PFunctor.M.mk ⟨a, f'⟩) → ∀ (i : F.B a), R (f i) (f' i)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.add_X_some : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) {T : C}
  (f : T ⟶ S) (i : E.I₀), (E.add f).X (some i) = E.X i
-- Std.Internal.Parsec.Basic
/-- Gets the next input element.
 -/
Std.Internal.Parsec.any : {ι elem idx : Type} →
  [inst : DecidableEq idx] →
    [inst_1 : DecidableEq elem] → [Std.Internal.Parsec.Input ι elem idx] → Std.Internal.Parsec ι elem
-- Lean.Parser.Types
Lean.Parser.FirstTokens.epsilon.sizeOf_spec : sizeOf Lean.Parser.FirstTokens.epsilon = 1
-- Init.Data.SInt.Lemmas
Int8.ofIntLE_sub : ∀ {a b : ℤ} {hab₁ : Int8.minValue.toInt ≤ a - b} {hab₂ : a - b ≤ Int8.maxValue.toInt},
  Int8.ofIntLE (a - b) hab₁ hab₂ = Int8.ofInt a - Int8.ofInt b
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
/-- If two points are topologically inseparable,
then they can't be separated by a Borel measurable set.  -/
Inseparable.mem_measurableSet_iff : ∀ {γ : Type u_3} [inst : TopologicalSpace γ] [inst_1 : MeasurableSpace γ] [BorelSpace γ] {x y : γ},
  Inseparable x y → ∀ {s : Set γ}, MeasurableSet s → (x ∈ s ↔ y ∈ s)
-- Batteries.Data.String.Legacy
/-- Auxuliary definition for `String.Legacy.revFind`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.
 -/
String.Legacy.revFindAux : String → (Char → Bool) → String.Pos.Raw → Option String.Pos.Raw
-- Mathlib.Order.SupClosed
supClosure_infClosure : ∀ {α : Type u_3} [inst : DistribLattice α] (s : Set α), supClosure (infClosure s) = latticeClosure s
-- Mathlib.Order.Monotone.Basic
/-- **Alias** of the reverse direction of `monotone_toDual_comp_iff`. -/
Antitone.dual_right : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  Antitone f → Monotone (⇑OrderDual.toDual ∘ f)