mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.ModularForms.Bounds
/-- A function on `ℍ` which is invariant under a finite-index subgroup of `SL(2, ℤ)`, and satisfies
an `O((im τ) ^ t)` bound at all cusps for some `0 ≤ t`, is in fact uniformly bounded by a multiple
of `(max (im τ) (1 / im τ)) ^ t`.  -/
ModularGroup.exists_bound_of_subgroup_invariant_of_isBigO : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {f : UpperHalfPlane → E},
  Continuous f →
    ∀ {t : ℝ},
      0 ≤ t →
        (∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ),
            (fun τ => f (g • τ)) =O[UpperHalfPlane.atImInfty] fun z => z.im ^ t) →
          ∀ {Γ : Subgroup (Matrix.SpecialLinearGroup (Fin 2) ℤ)} [Γ.FiniteIndex],
            (∀ g ∈ Γ, ∀ (τ : UpperHalfPlane), f (g • τ) = f τ) →
              ∃ C, ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C * max τ.im (1 / τ.im) ^ t
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
innerSL.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  innerSL 𝕜 = (innerₛₗ 𝕜).mkContinuous₂ 1 ⋯
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.sub_sub : ∀ (a b c : Ordinal.{u_4}), a - b - c = a - (b + c)
-- Lean.Meta.Sym.Pattern
Lean.Meta.Sym.Pattern.fnInfos : Lean.Meta.Sym.Pattern → Lean.AssocList Lean.Name Lean.Meta.Sym.ProofInstInfo
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.set.inj : ∀ {x : Lean.IR.VarId} {i : ℕ} {y : Lean.IR.Arg} {b : Lean.IR.FnBody} {x_1 : Lean.IR.VarId} {i_1 : ℕ} {y_1 : Lean.IR.Arg}
  {b_1 : Lean.IR.FnBody},
  Lean.IR.FnBody.set x i y b = Lean.IR.FnBody.set x_1 i_1 y_1 b_1 → x = x_1 ∧ i = i_1 ∧ y = y_1 ∧ b = b_1
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu
_private.Mathlib.CategoryTheory.Abelian.GrothendieckCategory.ModuleEmbedding.GabrielPopescu.0.CategoryTheory.Preadditive.homSelfLinearEquivEndMulOpposite.match_1.splitter : {C : Type u_2} →
  [inst : CategoryTheory.Category.{u_1, u_2} C] →
    (G : C) →
      (motive : (CategoryTheory.End G)ᵐᵒᵖ → Sort u_3) →
        (x : (CategoryTheory.End G)ᵐᵒᵖ) → ((f : CategoryTheory.End G) → motive { unop' := f }) → motive x
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_compTendsto' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} (b : β) {lc : Filter γ} {g : lc.Germ α}
  (hg : g.Tendsto l), (↑b).compTendsto' g hg = ↑b
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.preservesMonomorphisms_comp : ∀ {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] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.PreservesMonomorphisms] [G.PreservesMonomorphisms],
  (F.comp G).PreservesMonomorphisms
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.grind : Lean.MVarId →
  Lean.Grind.Config →
    Bool →
      Lean.TSyntaxArray `Lean.Parser.Tactic.grindParam →
        Option (Lean.TSyntax `Lean.Parser.Tactic.Grind.grindSeq) →
          optParam (Option Lean.Meta.Grind.ExtensionStateArray) none → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.Basis.mem_fixedPoints_or_exists_zpow_eq : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} (a : g.Basis) (x : α),
  x ∈ Function.fixedPoints ⇑g ∨ ∃ c, ∃ (_ : x ∈ (↑c).support), ∃ m, (g ^ m) (a c) = x
-- Mathlib.Analysis.InnerProductSpace.Orientation
/-- Given an orthonormal basis and an orientation, return an orthonormal basis giving that
orientation: either the original basis, or one constructed by negating a single (arbitrary) basis
vector.  -/
OrthonormalBasis.adjustToOrientation : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : InnerProductSpace ℝ E] →
      {ι : Type u_2} →
        [inst_2 : Fintype ι] →
          [DecidableEq ι] → OrthonormalBasis ι ℝ E → Orientation ℝ E ι → [Nonempty ι] → OrthonormalBasis ι ℝ E
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_singleton_abs : ∀ {α : Type u} [inst : Ring α] (x : α) [inst_1 : LinearOrder α], Ideal.span {|x|} = Ideal.span {x}
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.of.eq_1 : ∀ (G : Type u) [inst : Group G] [inst_1 : TopologicalSpace G] [inst_2 : IsTopologicalGroup G] [inst_3 : CompactSpace G]
  [inst_4 : TotallyDisconnectedSpace G],
  ProfiniteGrp.of G = { toProfinite := Profinite.of G, group := inst, topologicalGroup := inst_2 }
-- Mathlib.AlgebraicGeometry.SpreadingOut
AlgebraicGeometry.Scheme.exists_germ_injective : ∀ (X : AlgebraicGeometry.Scheme) (x : ↥X) [X.IsGermInjectiveAt x],
  ∃ U,
    ∃ (hx : x ∈ U),
      AlgebraicGeometry.IsAffineOpen U ∧
        Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom (X.presheaf.germ U x hx))
-- Lean.Data.NameMap.Basic
Lean.NameSet.ofArray : Array Lean.Name → Lean.NameSet
-- Mathlib.GroupTheory.Coset.Card
AddSubgroup.card_dvd_of_le : ∀ {α : Type u_1} [inst : AddGroup α] {H K : AddSubgroup α}, H ≤ K → Nat.card ↥H ∣ Nat.card ↥K
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.trace_toEnd_genWeightSpace : ∀ (R : Type u_2) (L : Type u_3) (M : Type u_4) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [IsDomain R] [IsPrincipalIdealRing R] [Module.Free R M] [Module.Finite R M]
  (χ : L → R) (x : L),
  (LinearMap.trace R ↥(LieModule.genWeightSpace M χ)) ((LieModule.toEnd R L ↥(LieModule.genWeightSpace M χ)) x) =
    Module.finrank R ↥(LieModule.genWeightSpace M χ) • χ x
-- Mathlib.Analysis.Normed.Group.Quotient
/-- The norm of `x` on the quotient by a subgroup `S` is defined as the infimum of the norm on
`x + S`.  -/
QuotientAddGroup.addGroupSeminorm : {M : Type u_1} → [inst : SeminormedAddCommGroup M] → {S : AddSubgroup M} → AddGroupSeminorm (M ⧸ S)
-- Mathlib.LinearAlgebra.BilinearMap
/-- For convenience, a shorthand for the type of bilinear forms from `M` to `R`.  -/
LinearMap.BilinForm : (R : Type u_2) →
  [inst : CommSemiring R] → (M : Type u_5) → [inst_1 : AddCommMonoid M] → [Module R M] → Type (max u_2 u_5)
-- Lean.Meta.Tactic.SplitIf
_private.Lean.Meta.Tactic.SplitIf.0.Lean.Meta.findSplit?.go : Lean.Meta.SplitKind → Lean.ExprSet → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.CategoryTheory.Bicategory.Monad.Basic
/-- An oplax functor from the trivial bicategory to `B` defines a comonad in `B`.  -/
CategoryTheory.Bicategory.Comonad.ofOplaxFromUnit : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (F : CategoryTheory.OplaxFunctor (CategoryTheory.LocallyDiscrete (CategoryTheory.Discrete Unit)) B) →
      CategoryTheory.Bicategory.Comonad (F.map (CategoryTheory.CategoryStruct.id { as := { as := () } }))
-- Init.Data.UInt.Bitwise
UInt8.ofBitVec_shiftLeft_mod : ∀ (a : BitVec 8) (b : ℕ), { toBitVec := a <<< (b % 8) } = { toBitVec := a } <<< UInt8.ofNat b
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.comp_apply : ∀ {R S T : RingCat} (f : R ⟶ S) (g : S ⟶ T) (r : ↑R),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) r =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) r)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getThenInsertIfNew?.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp),
  t = t_1 →
    ∀ (a a_1 : α), a = a_1 → ∀ (b b_1 : β), b = b_1 → t.getThenInsertIfNew? a b = t_1.getThenInsertIfNew? a_1 b_1
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.comapEq_inv_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {β γ : Type w} {f g : β → γ} (h : f = g)
  (X : CategoryTheory.GradedObject γ C) (b : β),
  (CategoryTheory.GradedObject.comapEq C h).inv.app X b = CategoryTheory.eqToHom ⋯
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instToStringAnchorRef : ToString Lean.Meta.Grind.AnchorRef
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.unitsSMulCommClass : ∀ (α : Type u_1) {M : Type u_2} [inst : Monoid M] [inst_1 : SMul α M] [SMulCommClass α M M] [IsScalarTower α M M],
  SMulCommClass α (ConjAct Mˣ) M
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.deriv.match_1.eq_5 : ∀ {α : Type u_1} (motive : RegularExpression α → α → Sort u_2) (P Q : RegularExpression α) (a : α)
  (h_1 : (x : α) → motive RegularExpression.zero x) (h_2 : (x : α) → motive RegularExpression.epsilon x)
  (h_3 : (a₁ a₂ : α) → motive (RegularExpression.char a₁) a₂)
  (h_4 : (P Q : RegularExpression α) → (a : α) → motive (P.plus Q) a)
  (h_5 : (P Q : RegularExpression α) → (a : α) → motive (P.comp Q) a)
  (h_6 : (P : RegularExpression α) → (a : α) → motive P.star a),
  (match P.comp Q, a with
    | RegularExpression.zero, x => h_1 x
    | RegularExpression.epsilon, x => h_2 x
    | RegularExpression.char a₁, a₂ => h_3 a₁ a₂
    | P.plus Q, a => h_4 P Q a
    | P.comp Q, a => h_5 P Q a
    | P.star, a => h_6 P a) =
    h_5 P Q a
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.instFiniteElemProdNatPreimageHAddFstSndSingletonSet : ∀ (n : ℕ), Finite ↑((fun i => i.1 + i.2) ⁻¹' {n})
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Expand the square  -/
norm_sub_mul_self : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x y : E), ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * RCLike.re (inner 𝕜 x y) + ‖y‖ * ‖y‖
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.map_apply_ι : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u4}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N) (m : M),
  (ExteriorAlgebra.map f) ((ExteriorAlgebra.ι R) m) = (ExteriorAlgebra.ι R) (f m)
-- Init.Grind.Injective
Lean.Grind.leftInv_eq : ∀ {α : Sort u} {β : Sort v} (f : α → β) (hf : Function.Injective f) [inst : Nonempty α] (a : α), f⁻¹ (f a) = a
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.sub_mem_Ico_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a - b ∈ Set.Ico c d ↔ b ∈ Set.Ioc (a - d) (a - c)
-- Mathlib.Analysis.Normed.Group.Pointwise
/-- **Alias** of `infEDist_neg`. -/
infEdist_neg : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (x : E) (s : Set E), Metric.infEDist (-x) s = Metric.infEDist x (-s)
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.toDual.congr_simp : ∀ {R : Type uR} {M : Type uM} {ι : Type uι} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {inst_3 : DecidableEq ι} [inst_4 : DecidableEq ι] (b b_1 : Module.Basis ι R M), b = b_1 → b.toDual = b_1.toDual
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalyzeTrustKnownFOType2TypeHOFuns : Lean.Options → Bool
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.norm_integral_le_of_norm_le_const : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G}
  [MeasureTheory.IsFiniteMeasure μ.variation] {C : ℝ},
  (∀ᵐ (x : X) ∂μ.variation, ‖f x‖ ≤ C) → ‖∫ᵛ (x : X), f x ∂[B; μ]‖ ≤ C * ‖B‖ * μ.variation.real Set.univ
-- Mathlib.Algebra.Free
Magma.AssocRel.left : ∀ {α : Type u} [inst : Mul α] (w x y z : α), Magma.AssocRel α (w * (x * y * z)) (w * (x * (y * z)))
-- Plausible.Shrinkable
Plausible.Option.shrinkable : {α : Type u_1} → [Plausible.Shrinkable α] → Plausible.Shrinkable (Option α)
-- Mathlib.Geometry.Manifold.Bordism
SingularManifold.mk.sizeOf_spec : ∀ {X : Type u_1} [inst : TopologicalSpace X] {k : WithTop ℕ∞} {E : Type u_2} {H : Type u_3}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : FiniteDimensional ℝ E]
  [inst_4 : TopologicalSpace H] {I : ModelWithCorners ℝ E H} [inst_5 : SizeOf X] [inst_6 : SizeOf E] [inst_7 : SizeOf H]
  (M : Type u) [topSpaceM : TopologicalSpace M] [chartedSpace : ChartedSpace H M] [isManifold : IsManifold I k M]
  [compactSpace : CompactSpace M] [boundaryless : BoundarylessManifold I M] (f : M → X) (hf : Continuous f),
  sizeOf
      { M := M, topSpaceM := topSpaceM, chartedSpace := chartedSpace, isManifold := isManifold,
        compactSpace := compactSpace, boundaryless := boundaryless, f := f, hf := hf } =
    1 + sizeOf M + sizeOf topSpaceM + sizeOf chartedSpace + sizeOf isManifold + sizeOf compactSpace +
        sizeOf boundaryless +
      sizeOf hf
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyIncomingCallsParams.mk.injEq : ∀ (item item_1 : Lean.Lsp.CallHierarchyItem), ({ item := item } = { item := item_1 }) = (item = item_1)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.filter.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (Unit → motive true) → (Unit → motive false) → motive x
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.sub_mod : ∀ {R : Type u} [inst : Field R] (p₁ p₂ q : Polynomial R), (p₁ - p₂) % q = p₁ % q - p₂ % q
-- Mathlib.CategoryTheory.Pi.Basic
/-- The bifunctor combining an `I`-indexed family of objects with a `J`-indexed family of objects
to obtain an `I ⊕ J`-indexed family of objects.
 -/
CategoryTheory.Pi.sum : {I : Type w₀} →
  (C : I → Type u₁) →
    [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] →
      {J : Type w₀} →
        {D : J → Type u₁} →
          [inst_1 : (j : J) → CategoryTheory.Category.{v₁, u₁} (D j)] →
            CategoryTheory.Functor ((i : I) → C i)
              (CategoryTheory.Functor ((j : J) → D j) ((s : I ⊕ J) → Sum.elim C D s))
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.comm_comp_comm : ∀ (R : Type u_1) [inst : CommSemiring R] (M : Type u_7) (N : Type u_8) [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N],
  ↑(TensorProduct.comm R N M) ∘ₗ ↑(TensorProduct.comm R M N) = LinearMap.id
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.regular_addMod_vadd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (A : C)
  [inst_2 : CategoryTheory.AddMonObj A], CategoryTheory.AddModObj.vadd = CategoryTheory.AddMonObj.add
-- Mathlib.RingTheory.Localization.FractionRing
FractionRing.instIsScalarTower_1 : ∀ (A : Type u_4) [inst : CommRing A] [IsDomain A] (k : Type u_6) (K : Type u_7) [inst_2 : Field k] [inst_3 : Field K]
  [inst_4 : Algebra A k] [inst_5 : Algebra A K] [inst_6 : Algebra k K] [inst_7 : FaithfulSMul A k]
  [inst_8 : FaithfulSMul A K] [IsScalarTower A k K], IsScalarTower (FractionRing A) k K
-- Batteries.Tactic.Alias
/-- Given a possibly forall-quantified iff expression `prf`, produce a value for one
of the implication directions (determined by `mp`).
 -/
Batteries.Tactic.Alias.mkIffMpApp : Bool → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.ENNReal.Holder
ENNReal.HolderConjugate.sub_one_mul_inv : ∀ (p q : ENNReal) [p.HolderConjugate q], p ≠ ⊤ → (p - 1) * p⁻¹ = q⁻¹
-- Mathlib.Probability.Moments.Basic
ProbabilityTheory.cgf_zero' : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω},
  ProbabilityTheory.cgf X μ 0 = Real.log (μ.real Set.univ)
-- Mathlib.Algebra.Lie.SkewAdjoint
/-- An equivalence of matrix algebras commuting with the transpose endomorphisms restricts to an
equivalence of Lie algebras of skew-adjoint matrices.  -/
skewAdjointMatricesLieSubalgebraEquivTranspose : {R : Type u} →
  {n : Type w} →
    [inst : CommRing R] →
      [inst_1 : Fintype n] →
        (J : Matrix n n R) →
          [inst_2 : DecidableEq n] →
            {m : Type w} →
              [inst_3 : DecidableEq m] →
                [inst_4 : Fintype m] →
                  (e : Matrix n n R ≃ₐ[R] Matrix m m R) →
                    (∀ (A : Matrix n n R), (e A).transpose = e A.transpose) →
                      ↥(skewAdjointMatricesLieSubalgebra J) ≃ₗ⁅R⁆ ↥(skewAdjointMatricesLieSubalgebra (e J))
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_div_const_Ioi : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b : α),
  (fun x => x / a) '' Set.Ioi b = Set.Ioi (b / a)
-- Mathlib.CategoryTheory.Products.Unitor
/-- The right inverse unitor `C ⥤ C × 1`  -/
CategoryTheory.prod.rightInverseUnitor : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (C × CategoryTheory.Discrete PUnit.{w + 1})
-- Mathlib.Algebra.Colimit.TensorProduct
Submodule.FG.exists_rTensor_fg_inclusion_eq : ∀ {R : Type u_1} {M : Type u_2} {P : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid P] [inst_4 : Module R P] {N : Submodule R P},
  N.FG →
    ∀ {x y : TensorProduct R (↥N) M},
      (LinearMap.rTensor M N.subtype) x = (LinearMap.rTensor M N.subtype) y →
        ∃ N',
          N'.FG ∧
            ∃ (h : N ≤ N'),
              (LinearMap.rTensor M (Submodule.inclusion h)) x = (LinearMap.rTensor M (Submodule.inclusion h)) y
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidHom.coe_comp_orderHom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : MulOneClass α] [inst_4 : MulOneClass β] [inst_5 : MulOneClass γ] (f : β →*o γ) (g : α →*o β),
  ↑(f.comp g) = (↑f).comp ↑g
-- Mathlib.Algebra.Group.Units.Equiv
Equiv.mulLeft_symm : ∀ {G : Type u_5} [inst : Group G] (a : G), Equiv.symm (Equiv.mulLeft a) = Equiv.mulLeft a⁻¹
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsOpenPosMeasure.inv : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : Group G] [ContinuousInv G] [μ.IsOpenPosMeasure], μ.inv.IsOpenPosMeasure
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.isOpenImmersion_stableUnderBaseChange : AlgebraicGeometry.IsOpenImmersion.IsStableUnderBaseChange
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.val_finsetSum : ∀ {ι : Type u_3} {G : Type u_4} [inst : AddCommGroup G] (H : AddSubgroup G) (f : ι → ↥H) (s : Finset ι),
  ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Std.Data.Internal.List.Defs
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.DistinctKeys : {α : Type u} → {β : α → Type v} → [BEq α] → List ((a : α) × β a) → Prop
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.contains.congr_simp : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtDTreeMap α β cmp),
  t = t_1 → ∀ (a a_1 : α), a = a_1 → t.contains a = t_1.contains a_1
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLawfulOrderLTOpposite : ∀ {α : Type u_1} {il : LE α} {it : LT α} [Std.LawfulOrderLT α], Std.LawfulOrderLT α
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instCommGroup : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [CommGroup Y] → CommGroup (LocallyConstant X Y)
-- Mathlib.Tactic.NormNum.Result
/-- Given a `NormNum.Result e` (which uses `IsNat`, `IsInt`, `IsRat` to express equality to a rational
numeral), converts it to an equality `e = Nat.rawCast n`, `e = Int.rawCast n`, or
`e = Rat.rawCast n d` to a raw cast expression, so it can be used for rewriting.
 -/
Mathlib.Meta.NormNum.Result.toRawEq : {u : Lean.Level} → {α : Q(Type u)} → {e : Q(«$α»)} → Mathlib.Meta.NormNum.Result e → (e' : Q(«$α»)) × Q(«$e» = «$e'»)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_insert_self : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited β], m.WF → ∀ {k : α} {v : β}, (m.insert k v)[k]! = v
-- Init.Internal.Order.While
_private.Init.Internal.Order.While.0.Lean.Loop.forIn.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b' : β) (h_1 : (b' : β) → motive (ForInStep.done b'))
  (h_2 : (b' : β) → motive (ForInStep.yield b')),
  (match ForInStep.done b' with
    | ForInStep.done b' => h_1 b'
    | ForInStep.yield b' => h_2 b') =
    h_1 b'
-- Mathlib.RingTheory.PolynomialAlgebra
polyEquivTensor_symm_apply_tmul : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : A)
  (p : Polynomial R),
  (polyEquivTensor R A).symm (a ⊗ₜ[R] p) = p.sum fun n r => (Polynomial.monomial n) (a * (algebraMap R A) r)
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.diffHypothesesBundle.withTypeDiff : Bool → Lean.Expr → Lean.Widget.InteractiveHypothesisBundle → Lean.MetaM Lean.Widget.InteractiveHypothesisBundle
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec_hom_apply_asIdeal : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A)
  (x : ↑↑((AlgebraicGeometry.Proj.toLocallyRingedSpace 𝒜).restrict ⋯).toPresheafedSpace),
  ((TopCat.Hom.hom (AlgebraicGeometry.ProjIsoSpecTopComponent.toSpec 𝒜 f)) x).asIdeal =
    AlgebraicGeometry.ProjIsoSpecTopComponent.ToSpec.carrier x
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.mk_eq_one : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x : R) (y : ↥(ValuativeRel.posSubmonoid R)),
  ValuativeRel.ValueGroupWithZero.mk x y = 1 ↔ x ≤ᵥ ↑y ∧ ↑y ≤ᵥ x
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.instCompactSpaceCarrierCarrierCommRingCatPullbackSchemeOfQuasiCompact_1 : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.QuasiCompact g] [CompactSpace ↥X],
  CompactSpace ↥(CategoryTheory.Limits.pullback f g)
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instInhabitedTransition : Inhabited Std.Time.TimeZone.Transition
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.mul_assoc : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (φ₁ φ₂ φ₃ : MvPowerSeries σ R), φ₁ * φ₂ * φ₃ = φ₁ * (φ₂ * φ₃)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.ae_sum_iff : ∀ {α : Type u_1} {ι : Type u_5} {m0 : MeasurableSpace α} [Countable ι] {μ : ι → MeasureTheory.Measure α} {p : α → Prop},
  (∀ᵐ (x : α) ∂MeasureTheory.Measure.sum μ, p x) ↔ ∀ (i : ι), ∀ᵐ (x : α) ∂μ i, p x
-- Qq.Match
_private.Qq.Match.0.Qq.liftsToTermLet : Array Qq.Lift✝ → Lean.Term → Lean.MacroM Lean.Term
-- Mathlib.Algebra.CubicDiscriminant
Cubic.zero : ∀ {R : Type u_1} [inst : Semiring R], Cubic.toPoly 0 = 0
-- Mathlib.Order.Filter.Basic
Filter.Frequently.filter_mono : ∀ {α : Type u} {p : α → Prop} {f g : Filter α}, (∃ᶠ (x : α) in f, p x) → f ≤ g → ∃ᶠ (x : α) in g, p x
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddCommMagmaOfAddHomClass.eq_1 : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → AddCommMagma (G i)] [inst_5 : ∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)],
  DirectLimit.instAddCommMagmaOfAddHomClass = { toAdd := DirectLimit.instAdd, add_comm := ⋯ }
-- Init.Data.Int.LemmasAux
Int.natCast_inj : ∀ {m n : ℕ}, ↑m = ↑n ↔ m = n
-- Mathlib.Algebra.Group.Action.Defs
Monoid.toMulAction.eq_1 : ∀ (M : Type u_1) [inst : Monoid M],
  Monoid.toMulAction M = { smul := fun x1 x2 => x1 * x2, mul_smul := ⋯, one_smul := ⋯ }
-- Init.Data.ByteArray.Lemmas
List.size_toByteArray : ∀ {l : List UInt8}, l.toByteArray.size = l.length
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.isoSpec_inv_ι_assoc : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U) {Z : AlgebraicGeometry.Scheme}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp hU.isoSpec.inv (CategoryTheory.CategoryStruct.comp U.ι h) =
    CategoryTheory.CategoryStruct.comp hU.fromSpec h