mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.AssociatedPrime.Finiteness
/-- If `A` is a Noetherian ring and `M` is a finitely generated `A`-module, then there exists
a chain of submodules `0 = M₀ ≤ M₁ ≤ M₂ ≤ ... ≤ Mₙ = M` of `M`, such that for each `0 ≤ i < n`,
`Mᵢ₊₁ / Mᵢ` is isomorphic to `A / pᵢ` for some prime ideal `pᵢ` of `A`.  -/
IsNoetherianRing.exists_relSeries_isQuotientEquivQuotientPrime : ∀ (A : Type u) [inst : CommRing A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M] [IsNoetherianRing A]
  [Module.Finite A M], ∃ s, s.head = ⊥ ∧ s.last = ⊤
-- Init.Grind.Norm
Lean.Grind.forall_forall_or : ∀ {α : Sort u} {β : α → Sort v} (p : α → Prop) (q : (a : α) → β a → Prop),
  (∀ (a : α), (∀ (b : β a), q a b) ∨ p a) = ∀ (a : α) (b : β a), q a b ∨ p a
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchTypeAndDiscrs.markIsDep : Lean.Elab.Term.ElabMatchTypeAndDiscrsResult → Lean.Elab.Term.ElabMatchTypeAndDiscrsResult
-- Mathlib.Algebra.Module.SpanRankOperations
_private.Mathlib.Algebra.Module.SpanRankOperations.0.term𝓀 : Lean.ParserDescr
-- Mathlib.Data.ENNReal.Operations
ENNReal.iSup_eq_zero : ∀ {ι : Sort u_1} {f : ι → ENNReal}, ⨆ i, f i = 0 ↔ ∀ (i : ι), f i = 0
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
lTensor.inverse_of_rightInverse.congr_simp : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g g_1 : N →ₗ[R] P} (e_g : g = g_1) (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  {h h_1 : P → N} (e_h : h = h_1) (hfg : Function.Exact ⇑f ⇑g) (hgh : Function.RightInverse h ⇑g),
  lTensor.inverse_of_rightInverse Q hfg hgh = lTensor.inverse_of_rightInverse Q ⋯ ⋯
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.instIsHausdorff : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsHausdorff I (AdicCompletion I M)
-- Mathlib.Algebra.Order.Floor.Defs
Int.ceil_pos : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a : α}, 0 < ⌈a⌉ ↔ 0 < a
-- Mathlib.LinearAlgebra.AffineSpace.Basis
AffineBasis.basisOf.eq_1 : ∀ {ι : Type u_1} {k : Type u_5} {V : Type u_6} {P : Type u_7} [inst : AddCommGroup V] [inst_1 : AddTorsor V P]
  [inst_2 : Ring k] [inst_3 : Module k V] (b : AffineBasis ι k P) (i : ι), b.basisOf i = Module.Basis.mk ⋯ ⋯
-- Mathlib.Geometry.Manifold.VectorBundle.Hom
mdifferentiableAt_hom_bundle : ∀ {𝕜 : Type u_1} {B : Type u_2} {F₁ : Type u_3} {F₂ : Type u_4} {M : Type u_5} {E₁ : B → Type u_6} {E₂ : B → Type u_7}
  [inst : NontriviallyNormedField 𝕜] [inst_1 : (x : B) → AddCommGroup (E₁ x)] [inst_2 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_3 : NormedAddCommGroup F₁] [inst_4 : NormedSpace 𝕜 F₁] [inst_5 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)]
  [inst_6 : (x : B) → TopologicalSpace (E₁ x)] [inst_7 : (x : B) → AddCommGroup (E₂ x)]
  [inst_8 : (x : B) → Module 𝕜 (E₂ x)] [inst_9 : NormedAddCommGroup F₂] [inst_10 : NormedSpace 𝕜 F₂]
  [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)] [inst_12 : (x : B) → TopologicalSpace (E₂ x)] {EB : Type u_8}
  [inst_13 : NormedAddCommGroup EB] [inst_14 : NormedSpace 𝕜 EB] {HB : Type u_9} [inst_15 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_16 : TopologicalSpace B] [inst_17 : ChartedSpace HB B] {EM : Type u_10}
  [inst_18 : NormedAddCommGroup EM] [inst_19 : NormedSpace 𝕜 EM] {HM : Type u_11} [inst_20 : TopologicalSpace HM]
  {IM : ModelWithCorners 𝕜 EM HM} [inst_21 : TopologicalSpace M] [inst_22 : ChartedSpace HM M]
  [inst_23 : FiberBundle F₁ E₁] [inst_24 : VectorBundle 𝕜 F₁ E₁] [inst_25 : FiberBundle F₂ E₂]
  [inst_26 : VectorBundle 𝕜 F₂ E₂] [inst_27 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_28 : ∀ (x : B), ContinuousSMul 𝕜 (E₂ x)] (f : M → Bundle.TotalSpace (F₁ →L[𝕜] F₂) fun b => E₁ b →L[𝕜] E₂ b)
  {x₀ : M},
  MDiffAt f x₀ ↔
    (MDiffAt fun x => (f x).proj) x₀ ∧
      (MDiffAt fun x =>
          ContinuousLinearMap.inCoordinates F₁ E₁ F₂ E₂ (f x₀).proj (f x).proj (f x₀).proj (f x).proj (f x).snd)
        x₀
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalTerm.instProd : {α α' : Type} →
  [Lean.Elab.ConfigEval.EvalTerm α] → [Lean.Elab.ConfigEval.EvalTerm α'] → Lean.Elab.ConfigEval.EvalTerm (α × α')
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.comp_X_add_C_eq_zero_iff : ∀ {R : Type u} [inst : CommRing R] {p : Polynomial R} {t : R}, p.comp (Polynomial.X + Polynomial.C t) = 0 ↔ p = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
CategoryTheory.nerveFunctor_map : ∀ {X Y : CategoryTheory.Cat} (F : X ⟶ Y), CategoryTheory.nerveFunctor.map F = CategoryTheory.nerveMap F.toFunctor
-- Lean.Parser.Command
Lean.Parser.Term.precheckedQuot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoid
/-- Shorthand for the "forward" arrow corresponding to `f` in `paths <| symmetrify V`  -/
Quiver.Hom.toPosPath : {V : Type u} → [inst : Quiver V] → {X Y : V} → (X ⟶ Y) → (X ⟶ Y)
-- Mathlib.Analysis.Calculus.Deriv.Abs
HasFDerivAt.abs_of_pos : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasFDerivAt f f' x → 0 < f x → HasFDerivAt (fun x => |f x|) f' x
-- Lean.Message
Lean.instAddMessageContextOfMonadLift : (m n : Type → Type) → [MonadLift m n] → [Lean.AddMessageContext m] → Lean.AddMessageContext n
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mk_surjective : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} (f : CategoryTheory.StructuredArrow S T),
  ∃ Y g, f = CategoryTheory.StructuredArrow.mk g
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pos.skipWhile_char_eq_skipWhile_beq : ∀ {c : Char} {s : String.Slice} (curr : s.Pos), curr.skipWhile c = curr.skipWhile fun x => x == c
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdx?.eq_1 : ∀ {α : Type u} {β : α → Type v} (x : ℕ), Std.DTreeMap.Internal.Impl.leaf.keyAtIdx? x = none
-- Init.Data.SInt.Lemmas
Int32.toInt_bmod_two_pow_numBits : ∀ (x : Int32), x.toInt.bmod (2 ^ System.Platform.numBits) = x.toInt
-- Mathlib.NumberTheory.RamificationInertia.Inertia
Ideal.inertiaDeg'_le_inertiaDeg' : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  {T : Type u_2} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [IsScalarTower R S T]
  [Module.Finite R T] (Q : Ideal T) [P.LiesOver p] [Q.LiesOver P] [p.IsPrime], P.inertiaDeg' Q ≤ p.inertiaDeg' Q
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_le_iff_le_inv : ∀ {a b r : ENNReal}, r ≠ 0 → r ≠ ⊤ → (r * a ≤ b ↔ a ≤ r⁻¹ * b)
-- Batteries.Recycling.RBTree.Lemmas
_private.Batteries.Recycling.RBTree.Lemmas.0.RBTree.RBNode.balRight.match_1.eq_1 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α)
  (h_1 :
    (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.black a x b))
  (h_2 :
    (a : RBTree.RBNode α) →
      (x : α) →
        (b : RBTree.RBNode α) →
          (y : α) →
            (c : RBTree.RBNode α) →
              motive (RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c)))
  (h_3 : (l : RBTree.RBNode α) → motive l),
  (match RBTree.RBNode.node RBTree.RBColor.black a x b with
    | RBTree.RBNode.node RBTree.RBColor.black a x b => h_1 a x b
    | RBTree.RBNode.node RBTree.RBColor.red a x (RBTree.RBNode.node RBTree.RBColor.black b y c) => h_2 a x b y c
    | l => h_3 l) =
    h_1 a x b
-- Lean.Meta.IndPredBelow
_private.Lean.Meta.IndPredBelow.0.Lean.Meta.IndPredBelow.NewDecl.below.sizeOf_spec : ∀ (decl : Lean.LocalDecl) (indName : Lean.Name) (vars : Array Lean.FVarId),
  sizeOf (Lean.Meta.IndPredBelow.NewDecl.below✝ decl indName vars) = 1 + sizeOf decl + sizeOf indName + sizeOf vars
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles_f : ∀ {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.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.kernelSequenceCycles._auto_1),
  (X.kernelSequenceCycles f g n₀ n₁ hn₁).f = X.iCycles f g n₀
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.nnnorm_integral_le : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E] (f : ↥(MeasureTheory.Lp E 1 μ)),
  ‖MeasureTheory.L1.integral f‖₊ ≤ ‖f‖₊
-- Mathlib.Data.Set.Function
Function.leftInvOn_invFunOn_of_subset_image_image : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} [inst : Nonempty α],
  s ⊆ Function.invFunOn f s '' f '' s → Set.LeftInvOn (Function.invFunOn f s) f s
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_mul : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Mul α] [inst_2 : Mul β]
  [inst_3 : FunLike F α β] [MulHomClass F α β] (f : F) {s t : Finset α} [inst_5 : DecidableEq β],
  Finset.image (⇑f) (s * t) = Finset.image (⇑f) s * Finset.image (⇑f) t
-- Lean.Elab.Do.Basic
Lean.Elab.Do.ContInfo.continueCont : Lean.Elab.Do.ContInfo → Option (Lean.Elab.Do.DoElabM Lean.Expr)
-- Mathlib.Geometry.Euclidean.PerpBisector
AffineSubspace.perpBisector.eq_1 : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (p₁ p₂ : P),
  AffineSubspace.perpBisector p₁ p₂ = AffineSubspace.mk' (midpoint ℝ p₁ p₂) ((innerₛₗ ℝ) (p₂ -ᵥ p₁)).ker
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.FullyFaithful.compUliftYonedaCompWhiskeringLeft_inv_app_app_hom_apply_down : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (hF : F.FullyFaithful) (X : C) (X_1 : Cᵒᵖ)
  (x : (CategoryTheory.uliftYoneda.{v₂, v₁, u₁}.obj X).obj X_1),
  ((CategoryTheory.ConcreteCategory.hom ((hF.compUliftYonedaCompWhiskeringLeft.inv.app X).app X_1)) x).down =
    F.map x.down
-- Lean.Meta.Tactic.Grind.PropagatorAttr
Lean.Meta.Grind.PropagatorMap : Type
-- Mathlib.Algebra.Group.Prod
/-- Given additive monoids `A`, `B`, the natural projection homomorphism
from `A × B` to `A`  -/
AddMonoidHom.fst : (M : Type u_3) → (N : Type u_4) → [inst : AddZeroClass M] → [inst_1 : AddZeroClass N] → M × N →+ M
-- Mathlib.Analysis.Convex.Deriv
/-- If `f` is concave on `S` and differentiable at all points of `S`, then its derivative is
antitone (monotone decreasing) on `S`.  -/
ConcaveOn.antitoneOn_deriv : ∀ {S : Set ℝ} {f : ℝ → ℝ}, ConcaveOn ℝ S f → (∀ x ∈ S, DifferentiableAt ℝ f x) → AntitoneOn (deriv f) S
-- Mathlib.Algebra.Group.InjSurj
Function.Injective.addSemigroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Add M₁] [inst_1 : AddSemigroup M₂] (f : M₁ → M₂) (hf : Function.Injective f)
  (mul : ∀ (x y : M₁), f (x + y) = f x + f y),
  Function.Injective.addSemigroup f hf mul = { toAdd := inst, add_assoc := ⋯ }
-- Mathlib.GroupTheory.SchurZassenhaus
/-- Do not use this lemma: It is made obsolete by `exists_right_complement'_of_coprime`  -/
_private.Mathlib.GroupTheory.SchurZassenhaus.0.Subgroup.SchurZassenhausInduction.step2 : ∀ {G : Type u} [inst : Group G] {N : Subgroup G} [N.Normal],
  (Nat.card ↥N).Coprime N.index →
    (∀ (G' : Type u) [inst : Group G'] [Finite G'],
        Nat.card G' < Nat.card G →
          ∀ {N' : Subgroup G'} [N'.Normal], (Nat.card ↥N').Coprime N'.index → ∃ H', N'.IsComplement' H') →
      (∀ (H : Subgroup G), ¬N.IsComplement' H) → ∀ [Finite G] (K : Subgroup G) [K.Normal], K ≤ N → K = ⊥ ∨ K = N
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {a fallback : α},
  t.contains a = false → t.getD a fallback = fallback
-- Mathlib.Algebra.BigOperators.Fin
List.alternatingSum_eq_finsetSum : ∀ {G : Type u_3} [inst : SubtractionCommMonoid G] (L : List G), L.alternatingSum = ∑ i, (-1) ^ ↑i • L[i]
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.floor_le_floor_add_of_mem_closure : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι] {x y : ι → ℕ}
  {i : ↑(IsProperLinearSet.basisSet✝ hs)},
  y ∈ AddSubmonoid.closure (IsProperLinearSet.basisSet✝ hs) →
    IsProperLinearSet.floor✝ hs x i ≤ IsProperLinearSet.floor✝ hs (x + y) i
-- Lean.Message
Lean.MessageData.instCoeString : Coe String Lean.MessageData
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
/-- Convergence in the topology of `𝔖`-convergence means uniform convergence on `S` (in the sense
of `TendstoUniformlyOn`) for all `S ∈ 𝔖`.  -/
UniformOnFun.tendsto_iff_tendstoUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} {p : Filter ι} [inst : UniformSpace β] {𝔖 : Set (Set α)}
  {F : ι → UniformOnFun α β 𝔖} {f : UniformOnFun α β 𝔖},
  Filter.Tendsto F p (nhds f) ↔ ∀ s ∈ 𝔖, TendstoUniformlyOn (⇑(UniformOnFun.toFun 𝔖) ∘ F) ((UniformOnFun.toFun 𝔖) f) p s
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2}, Height.logHeight 0 = 0
-- Init.Data.String.Lemmas.Intercalate
String.toList_intercalate : ∀ {s : String} {l : List String}, (s.intercalate l).toList = s.toList.intercalate (List.map String.toList l)
-- Mathlib.Analysis.SpecialFunctions.MulExpNegMulSq
Real.mulExpNegMulSq_one_le_one : ∀ (x : ℝ), Real.mulExpNegMulSq 1 x ≤ 1
-- Init.Data.Int.DivMod.Lemmas
Int.natAbs_tdiv_le_natAbs : ∀ (a b : ℤ), (a.tdiv b).natAbs ≤ a.natAbs
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.toDivisionRing : {K : Type u} → [inst : DivisionRing K] → (s : Subfield K) → DivisionRing ↥s
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.coe_multilinearMap_mk : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : (ι → M) → N)
  (h₁ :
    ∀ [inst : DecidableEq ι] (m : ι → M) (i : ι) (x y : M),
      f (Function.update m i (x + y)) = f (Function.update m i x) + f (Function.update m i y))
  (h₂ :
    ∀ [inst_5 : DecidableEq ι] (m : ι → M) (i : ι) (c : R) (x : M),
      f (Function.update m i (c • x)) = c • f (Function.update m i x))
  (h₃ :
    ∀ (v : ι → M) (i j : ι),
      v i = v j → i ≠ j → { toFun := f, map_update_add' := ⋯, map_update_smul' := ⋯ }.toFun v = 0),
  ↑{ toFun := f, map_update_add' := ⋯, map_update_smul' := ⋯, map_eq_zero_of_eq' := h₃ } =
    { toFun := f, map_update_add' := h₁, map_update_smul' := h₂ }
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.equiv_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (f : α ≃ₜ β)
  (K : TopologicalSpace.Compacts α), (TopologicalSpace.Compacts.equiv f) K = TopologicalSpace.Compacts.map ⇑f ⋯ K
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurable_infEDist : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] {s : Set α},
  Measurable fun x => Metric.infEDist x s
-- Mathlib.Data.Set.Operations
Set.instSProd : {α : Type u} → {β : Type v} → SProd (Set α) (Set β) (Set (α × β))
-- Mathlib.Data.Sym.Sym2
Sym2.fromRel_toRel : ∀ {α : Type u_1} (s : Set (Sym2 α)), Sym2.fromRel ⋯ = s
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- Let `S` be a subspace of a finite-dimensional complex inner product space `V`.  A linear
isometry mapping `S` into `V` can be extended to a full isometry of `V`.

TODO:  The case when `S` is a finite-dimensional subspace of an infinite-dimensional `V`.  -/
LinearIsometry.extend : {𝕜 : Type u_3} →
  [inst : RCLike 𝕜] →
    {V : Type u_7} →
      [inst_1 : NormedAddCommGroup V] →
        [inst_2 : InnerProductSpace 𝕜 V] → [FiniteDimensional 𝕜 V] → {S : Submodule 𝕜 V} → (↥S →ₗᵢ[𝕜] V) → V →ₗᵢ[𝕜] V
-- Mathlib.Topology.MetricSpace.Bounded
/-- Every open set in a metric space is a countable union of bounded open sets.  -/
Metric.eq_countable_union_of_isBounded_of_isOpen : ∀ {α : Type u} [inst : PseudoMetricSpace α] {U : Set α},
  IsOpen U → ∃ f, Monotone f ∧ ⋃ i, f i = U ∧ ∀ (i : ℕ), Bornology.IsBounded (f i) ∧ IsOpen (f i)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.ENNReal
ENNReal.finStronglyMeasurable_of_measurable : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  ∫⁻ (x : α), f x ∂μ ≠ ⊤ → Measurable f → MeasureTheory.FinStronglyMeasurable f μ
-- Init.Data.Vector.InsertIdx
Vector.getElem?_insertIdx_of_ge : ∀ {α : Type u} {n : ℕ} {xs : Vector α n} {x : α} {i k : ℕ} (w : i < k) (h : k ≤ n),
  (xs.insertIdx i x ⋯)[k]? = xs[k - 1]?
-- Mathlib.Algebra.Free
FreeMagma.traverse_mul : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β) (x y : FreeMagma α),
  traverse F (x * y) = (fun x1 x2 => x1 * x2) <$> traverse F x <*> traverse F y
-- Mathlib.CategoryTheory.Galois.Basic
CategoryTheory.PreGaloisCategory.fiberPullbackEquiv_symm_snd_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F] {X A B : C}
  {f : A ⟶ X} {g : B ⟶ X} (a : (F.obj A).obj) (b : (F.obj B).obj)
  (h : (CategoryTheory.ConcreteCategory.hom (F.map f)) a = (CategoryTheory.ConcreteCategory.hom (F.map g)) b),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.Limits.pullback.snd f g)))
      ((CategoryTheory.PreGaloisCategory.fiberPullbackEquiv F f g).symm ⟨(a, b), h⟩) =
    b
-- Std.Tactic.BVDecide.LRAT.Actions
Std.Tactic.BVDecide.LRAT.Action.addRup.injEq : ∀ {β : Type u} {α : Type v} (id : ℕ) (c : β) (rupHints : Array ℕ) (id_1 : ℕ) (c_1 : β) (rupHints_1 : Array ℕ),
  (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints = Std.Tactic.BVDecide.LRAT.Action.addRup id_1 c_1 rupHints_1) =
    (id = id_1 ∧ c = c_1 ∧ rupHints = rupHints_1)
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity_empty : schnirelmannDensity ∅ = 0
-- Lean.Meta.InferType
/-- If `type : sort` and `sort` reduces to `Sort u` for some `u`, then `getLevel type` returns `u`.

If `sort` is an assignable MVar, then `getLevel type` produces a fresh level metavariable `?u`,
assigns the MVar to `Sort ?u` and returns `?u`.
 -/
Lean.Meta.getLevel : Lean.Expr → Lean.MetaM Lean.Level
-- Mathlib.Analysis.LocallyConvex.Barrelled
/-- A topological vector space `E` is said to be **barrelled** if all lower semicontinuous
seminorms on `E` are actually continuous. This is not the usual definition for TVS over `ℝ` or `ℂ`,
but this has the big advantage of working and giving sensible results over *any*
`NontriviallyNormedField`. In particular, the Banach-Steinhaus theorem holds for maps between such
a space and any space whose topology is generated by a family of seminorms.  -/
BarrelledSpace : (𝕜 : Type u_1) → (E : Type u_2) → [SeminormedRing 𝕜] → [AddGroup E] → [SMul 𝕜 E] → [TopologicalSpace E] → Prop
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Functor.mapMat__obj_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v₁, u_1} D] [inst_3 : CategoryTheory.Preadditive D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Additive] (M : CategoryTheory.Mat_ C), (F.mapMat_.obj M).ι = M.ι
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.map_update_sum : ∀ {R : Type uR} {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] (f : MultilinearMap R M₁ M₂) {α : Type u_2} [inst_5 : DecidableEq ι] (t : Finset α) (i : ι)
  (g : α → M₁ i) (m : (i : ι) → M₁ i), f (Function.update m i (∑ a ∈ t, g a)) = ∑ a ∈ t, f (Function.update m i (g a))
-- Mathlib.Data.Set.SymmDiff
Set.inter_symmDiff_distrib_right : ∀ {α : Type u} (s t u : Set α), symmDiff s t ∩ u = symmDiff (s ∩ u) (t ∩ u)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l →
          ∀ {h : k' ∈ Std.DTreeMap.Const.ofList l cmp},
            Std.DTreeMap.Const.get (Std.DTreeMap.Const.ofList l cmp) k' h = v
-- Mathlib.CategoryTheory.Adjunction.Restrict
CategoryTheory.Adjunction.map_restrictFullyFaithful_counit_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] {iC : CategoryTheory.Functor C C'} {iD : CategoryTheory.Functor D D'}
  {L' : CategoryTheory.Functor C' D'} {R' : CategoryTheory.Functor D' C'} (adj : L' ⊣ R') (hiC : iC.FullyFaithful)
  (hiD : iD.FullyFaithful) {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C}
  (comm1 : iC.comp L' ≅ L.comp iD) (comm2 : iD.comp R' ≅ R.comp iC) (X : D) {Z : D'} (h : iD.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (iD.map ((adj.restrictFullyFaithful hiC hiD comm1 comm2).counit.app X)) h =
    CategoryTheory.CategoryStruct.comp (comm1.inv.app (R.obj X))
      (CategoryTheory.CategoryStruct.comp (L'.map (comm2.inv.app X))
        (CategoryTheory.CategoryStruct.comp (adj.counit.app (iD.obj X)) h))
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
NumberField.canonicalEmbedding.nnnorm_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : K),
  ‖(NumberField.canonicalEmbedding K) x‖₊ = Finset.univ.sup fun φ => ‖φ x‖₊
-- Mathlib.Analysis.Fourier.RiemannLebesgueLemma
/-- The Riemann-Lebesgue lemma for functions on `ℝ`.  -/
Real.tendsto_integral_exp_smul_cocompact : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℝ → E),
  Filter.Tendsto (fun w => ∫ (v : ℝ), Real.fourierChar (-(v * w)) • f v) (Filter.cocompact ℝ) (nhds 0)
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r : ℤ) (hr : r₀ ≤ r) (pq pq' : κ) (hpq : (c r).Rel pq pq') {i₀ i₁ i₂ i₃ i₄ i₅ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₅ : i₄ ⟶ i₅) (h₀ : i₀ = data.i₀ r pq' ⋯) (h₁ : i₁ = data.i₁ pq')
  (h₂ : i₂ = data.i₀ r pq ⋯) (h₃ : i₃ = data.i₁ pq) (h₄ : i₄ = data.i₂ pq) (h₅ : i₅ = data.i₃ r pq ⋯) (n₀ n₁ n₂ n₃ : ℤ)
  (hn₁' : n₁ = data.deg pq)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq._auto_3)
  (hn₃ : autoParam (n₂ + 1 = n₃) CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD_eq._auto_5),
  CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD X data r pq pq' ⋯ =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso X data r ⋯ pq i₂ i₃ i₄ i₅ h₂ h₃ h₄ h₅ n₀ n₁ n₂
          hn₁' hn₁ hn₂).hom
      (CategoryTheory.CategoryStruct.comp (X.d f₁ f₂ f₃ f₄ f₅ n₀ n₁ n₂ n₃ hn₁ hn₂ hn₃)
        (CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso X data r ⋯ pq' i₀ i₁ i₂ i₃ h₀ h₁ ⋯ ⋯ n₁ n₂ n₃ ⋯
            hn₂ hn₃).inv)