mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Euclidean.MongePoint
/-- A Monge plane of an (n+2)-simplex is the (n+1)-dimensional affine
subspace of the subspace spanned by the simplex that passes through
the centroid of an n-dimensional face and is orthogonal to the
opposite edge (in 2 dimensions, this is the same as an altitude).
This definition is only intended to be used when `i₁ ≠ i₂`.  -/
Affine.Simplex.mongePlane : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] →
            {n : ℕ} → Affine.Simplex ℝ P (n + 2) → Fin (n + 3) → Fin (n + 3) → AffineSubspace ℝ P
-- Lean.Elab.Do.Legacy
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.union : Lean.Elab.Term.Do.VarSet → Lean.Elab.Term.Do.VarSet → Lean.Elab.Term.Do.VarSet
-- Mathlib.Order.Basic
le_imp_eq_iff_le_imp_ge' : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α}, b ≤ a → a = b ↔ b ≤ a → a ≤ b
-- Init.Grind.FieldNormNum
Lean.Grind.Field.NormNum.ofRat_neg : ∀ {α : Type u_1} [inst : Lean.Grind.Field α] (a : ℚ),
  Lean.Grind.Field.NormNum.ofRat (-a) = -Lean.Grind.Field.NormNum.ofRat a
-- Mathlib.CategoryTheory.LiftingProperties.Basic
/-- Given morphisms `i : A ⟶ B`, `p : X ⟶ Y`, `t : A ⟶ X`,
this is the property that a lifting exists for all squares
with `i` on left, `p` on the right and `t` on the top.  -/
CategoryTheory.HasLiftingPropertyFixedTop : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → {A B X Y : C} → (A ⟶ B) → (X ⟶ Y) → (A ⟶ X) → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_modify : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] [inst_1 : Inhabited α],
  t.WF → ∀ {k : α} {f : β k → β k}, (Std.DTreeMap.Internal.Impl.modify k f t).minKey! = t.minKey!
-- Std.Sat.AIG.Basic
/-- A node with the constant value false. The constant true can be represented
with a `Ref` to `false` with `invert` set true
 -/
Std.Sat.AIG.Decl.false : {α : Type} → Std.Sat.AIG.Decl α
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseStandaloneWeekdayNumberText : (Std.Time.Number ⊕ Std.Time.Text → Std.Time.Modifier) → String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.instSupSet.eq_1 : ∀ {E : Type u_3} [inst : AddGroup E],
  AddGroupSeminorm.instSupSet =
    {
      sSup := fun s =>
        if h : BddAbove s then { toFun := fun x => ⨆ p, ↑p x, map_zero' := ⋯, add_le' := ⋯, neg' := ⋯ } else 0 }
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.instBEqOfHashable : {α : Type u} → [BEq α] → [Hashable α] → BEq (Std.HashSet.Raw α)
-- Mathlib.Analysis.Real.Pi.Bounds
Real.sqrtTwoAddSeries_step_up : ∀ (c d : ℕ) {a b n : ℕ} {z : ℝ},
  (↑c / ↑d).sqrtTwoAddSeries n ≤ z →
    0 < b → 0 < d → (2 * b + a) * d ^ 2 ≤ c ^ 2 * b → (↑a / ↑b).sqrtTwoAddSeries (n + 1) ≤ z
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.gcd.sizeOf_spec : ∀ (a b : ℤ) (c₁ c₂ : Lean.Meta.Grind.Arith.CommRing.EqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.gcd a b c₁ c₂) = 1 + sizeOf a + sizeOf b + sizeOf c₁ + sizeOf c₂
-- Mathlib.LinearAlgebra.TensorProduct.Subalgebra
Subalgebra.lTensorBot_tmul : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S]
  {A : Subalgebra R S} (x : R) (a : ↥A), A.lTensorBot ((algebraMap R ↥⊥) x ⊗ₜ[R] a) = x • a
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.multiplicativeClosure.below.of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C}
  {motive : ⦃X Y : C⦄ → (x : X ⟶ Y) → W.multiplicativeClosure x → Prop} {x y : C} (f : x ⟶ y) (hf : W f),
  CategoryTheory.MorphismProperty.multiplicativeClosure.below ⋯
-- Mathlib.Algebra.Homology.SpectralObject.Basic
/-- The natural transformation that is part of a morphism between spectral objects.  -/
CategoryTheory.Abelian.SpectralObject.Hom.hom : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{u_3, u_1} C] →
      [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          {X X' : CategoryTheory.Abelian.SpectralObject C ι} → X.Hom X' → (n : ℤ) → X.H n ⟶ X'.H n
-- Mathlib.Algebra.GroupWithZero.Defs
mul_div_cancel_left₀ : ∀ {M₀ : Type u_1} [inst : CommMonoidWithZero M₀] [inst_1 : Div M₀] [MulDivCancelClass M₀] (b : M₀) {a : M₀},
  a ≠ 0 → a * b / a = b
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffAt_snd : ∀ {𝕜 : 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] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {G : Type u_9} [inst_8 : TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} {p : M × N},
  ContMDiffAt (I.prod J) J n Prod.snd p
-- Std.Data.DHashMap.Internal.AssocList.Basic
Std.DHashMap.Internal.AssocList.cons.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)] (key : α) (value : β key)
  (tail : Std.DHashMap.Internal.AssocList α β),
  sizeOf (Std.DHashMap.Internal.AssocList.cons key value tail) = 1 + sizeOf key + sizeOf value + sizeOf tail
-- Init.Data.String.PosRaw
String.Pos.Raw.unoffsetBy_zero : ∀ {p : String.Pos.Raw}, p.unoffsetBy 0 = p
-- Mathlib.Computability.RegularExpressions
RegularExpression.plus : {α : Type u} → RegularExpression α → RegularExpression α → RegularExpression α
-- Mathlib.Tactic.NormNum.Ineq
/-- The `norm_num` extension which identifies expressions of the form `a < b`,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalLT : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.CategoryTheory.ComposableArrows.Basic
_private.Mathlib.CategoryTheory.ComposableArrows.Basic.0.CategoryTheory.ComposableArrows.Mk₁.obj.match_1.eq_2 : ∀ (motive : Fin 2 → Sort u_1) (isLt : 1 < 2) (h_1 : (isLt : 0 < 2) → motive ⟨0, isLt⟩)
  (h_2 : (isLt : 1 < 2) → motive ⟨1, isLt⟩),
  (match ⟨1, isLt⟩ with
    | ⟨0, isLt⟩ => h_1 isLt
    | ⟨1, isLt⟩ => h_2 isLt) =
    h_2 isLt
-- Mathlib.Order.Filter.Basic
Filter.le_principal_iff : ∀ {α : Type u} {s : Set α} {f : Filter α}, f ≤ Filter.principal s ↔ s ∈ f
-- Mathlib.GroupTheory.IsSubnormal
/-- The quotient of a subnormal subgroup by a normal subgroup is subnormal.  -/
Subgroup.IsSubnormal.quotient : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} [inst_1 : K.Normal],
  H.IsSubnormal → (Subgroup.map (QuotientGroup.mk' K) H).IsSubnormal
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.leadCoeff.match_1.splitter : (motive : Int.Internal.Linear.Poly → Sort u_1) →
  (p : Int.Internal.Linear.Poly) →
    ((a : ℤ) →
        (v : Int.Internal.Linear.Var) → (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.add a v p)) →
      ((x : Int.Internal.Linear.Poly) →
          (∀ (a : ℤ) (v : Int.Internal.Linear.Var) (p : Int.Internal.Linear.Poly),
              x = Int.Internal.Linear.Poly.add a v p → False) →
            motive x) →
        motive p
-- Mathlib.Data.Finset.Basic
Finset.filter_cons_of_pos : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (a : α) (s : Finset α) (ha : a ∉ s),
  p a → Finset.filter p (Finset.cons a s ha) = Finset.cons a (Finset.filter p s) ⋯
-- Mathlib.Topology.Bornology.BoundedOperation
/-- A typeclass saying that `(p : R × R) ↦ p.1 - p.2` maps any product of bounded sets to a bounded
set. This property automatically holds for seminormed additive groups, but it also holds, e.g.,
for `ℝ≥0`.  -/
BoundedSub : (R : Type u_1) → [Bornology R] → [Sub R] → Prop
-- Std.Data.Internal.List.Associative
Std.Internal.List.keys_insertEntryIfNew_perm : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] (k : α) (v : β k) {l : List ((a : α) × β a)},
  (Std.Internal.List.keys (Std.Internal.List.insertEntryIfNew k v l)).Perm
    (if Std.Internal.List.containsKey k l = true then Std.Internal.List.keys l else k :: Std.Internal.List.keys l)
-- Mathlib.LinearAlgebra.Multilinear.Basic
MultilinearMap.toFun_eq_coe : ∀ {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₂), f.toFun = ⇑f
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_eq_some_of_contains : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α},
  m.contains k = true → m.getKey? k = some k
-- Mathlib.CategoryTheory.Filtered.Small
_private.Mathlib.CategoryTheory.Filtered.Small.0.CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  (f : α → C),
  CategoryTheory.IsCofiltered.CofilteredClosureSmall.bundledAbstractCofilteredClosure✝ f 0 =
    ⟨ULift.{v, w} α, f ∘ ULift.down⟩
-- Mathlib.RepresentationTheory.Coinvariants
/-- The quotient map from a representation to its coinvariants as a linear map.  -/
Representation.Coinvariants.mk : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] →
          [inst_2 : AddCommGroup V] → [inst_3 : Module k V] → (ρ : Representation k G V) → V →ₗ[k] ρ.Coinvariants
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.positive.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {e : Q(«$α»)} {pα : Q(PartialOrder «$α»)}
  (pf pf_1 : Q(0 < «$e»)),
  (Mathlib.Meta.Positivity.Strictness.positive pf = Mathlib.Meta.Positivity.Strictness.positive pf_1) = (pf = pf_1)
-- Init.Data.Range.Polymorphic.Char
Char.instIsAlwaysFinite : Std.Rxc.IsAlwaysFinite Char
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.smul_finset_subset_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : Group α] [inst_2 : MulAction α β] {s t : Finset β}
  {a : α}, a • s ⊆ t ↔ s ⊆ a⁻¹ • t
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.setLIntegral_smul_measure : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {R : Type u_4} [inst : SMul R ENNReal]
  [inst_1 : IsScalarTower R ENNReal ENNReal] (c : R) (f : α → ENNReal) (s : Set α),
  ∫⁻ (a : α) in s, f a ∂c • μ = c • ∫⁻ (a : α) in s, f a ∂μ
-- Mathlib.NumberTheory.EulerProduct.Basic
/-- The following statement says that summing over `N`-smooth numbers
for large enough `N` gets us arbitrarily close to the sum over all natural numbers
(assuming `f` is norm-summable and `f 0 = 0`; the latter since `0` is not smooth).  -/
EulerProduct.norm_tsum_smoothNumbers_sub_tsum_lt : ∀ {R : Type u_1} [inst : NormedCommRing R] {f : ℕ → R} [CompleteSpace R],
  Summable f → f 0 = 0 → ∀ {ε : ℝ}, 0 < ε → ∃ N₀, ∀ N ≥ N₀, ‖∑' (m : ℕ), f m - ∑' (m : ↑N.smoothNumbers), f ↑m‖ < ε
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
/-- `LinearEquiv.ofEq` as a `LinearIsometryEquiv`.  -/
LinearIsometryEquiv.ofEq : {E : Type u_5} →
  [inst : SeminormedAddCommGroup E] →
    {R' : Type u_12} → [inst_1 : Ring R'] → [inst_2 : Module R' E] → (p q : Submodule R' E) → p = q → ↥p ≃ₗᵢ[R'] ↥q
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.mem_lift : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {F : IntermediateField K L}
  {E : IntermediateField K ↥F} (x : ↥F), ↑x ∈ IntermediateField.lift E ↔ x ∈ E
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.expandIfNecessary.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DHashMap.Internal.Raw₀ α β → Sort u_3) →
      (m : Std.DHashMap.Internal.Raw₀ α β) →
        ((size : ℕ) →
            (buckets : Array (Std.DHashMap.Internal.AssocList α β)) →
              (hm : 0 < { size := size, buckets := buckets }.buckets.size) →
                motive ⟨{ size := size, buckets := buckets }, hm⟩) →
          motive m
-- Mathlib.SetTheory.Ordinal.Notation
/-- The ordinal denoted by a notation  -/
ONote.repr : ONote → Ordinal.{0}
-- Mathlib.Algebra.Module.GradedModule
DirectSum.Gmodule.mk : {ιA : Type u_1} →
  {ιB : Type u_2} →
    {A : ιA → Type u_3} →
      {M : ιB → Type u_4} →
        [inst : AddMonoid ιA] →
          [inst_1 : VAdd ιA ιB] →
            [inst_2 : (i : ιA) → AddMonoid (A i)] →
              [inst_3 : (i : ιB) → AddMonoid (M i)] →
                [inst_4 : GradedMonoid.GMonoid A] →
                  [toGdistribMulAction : DirectSum.GdistribMulAction A M] →
                    (∀ {i : ιA} {j : ιB} (a a' : A i) (b : M j),
                        GradedMonoid.GSMul.smul (a + a') b =
                          GradedMonoid.GSMul.smul a b + GradedMonoid.GSMul.smul a' b) →
                      (∀ {i : ιA} {j : ιB} (b : M j), GradedMonoid.GSMul.smul 0 b = 0) → DirectSum.Gmodule A M
-- Mathlib.Data.Matrix.Basic
RingEquiv.mapMatrix_refl : ∀ {m : Type u_2} {α : Type u_11} [inst : Fintype m] [inst_1 : DecidableEq m] [inst_2 : NonAssocSemiring α],
  (RingEquiv.refl α).mapMatrix = RingEquiv.refl (Matrix m m α)
-- Mathlib.Algebra.Order.AbsoluteValue.Euclidean
AbsoluteValue.IsEuclidean.sub_mod_lt : ∀ {R : Type u_1} {S : Type u_2} [inst : EuclideanDomain R] [inst_1 : Semiring S] [inst_2 : PartialOrder S]
  {abv : AbsoluteValue R S}, abv.IsEuclidean → ∀ (a : R) {b : R}, b ≠ 0 → abv (a % b) < abv b
-- Mathlib.Topology.Constructible
IsRetrocompact.eq_1 : ∀ {X : Type u_2} [inst : TopologicalSpace X] (s : Set X),
  IsRetrocompact s = ∀ ⦃U : Set X⦄, IsCompact U → IsOpen U → IsCompact (s ∩ U)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.liftOfSurjective_apply : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : CommRing A] [inst_2 : CommRing M]
  [inst_3 : Algebra R A] [inst_4 : Algebra R M] {F : Type u_4} [inst_5 : FunLike F A M] [inst_6 : AlgHomClass F R A M]
  {f : F} (hf : Function.Surjective ⇑f) {d : Derivation R A A} (hd : ∀ (x : A), f x = 0 → f (d x) = 0) (x : A),
  (Derivation.liftOfSurjective hf hd) (f x) = f (d x)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get_union_of_contains_eq_false_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α] (h₁ : (↑m₁).WF) (h₂ : (↑m₂).WF) {k : α}
  (contains_eq_false : m₁.contains k = false) {h' : (m₁.union m₂).contains k = true},
  Std.DHashMap.Internal.Raw₀.Const.get (m₁.union m₂) k h' = Std.DHashMap.Internal.Raw₀.Const.get m₂ k ⋯
-- Mathlib.MeasureTheory.Measure.Tight
/-- Finite measures that are inner regular with respect to closed compact sets are tight.  -/
MeasureTheory.isTightMeasureSet_singleton_of_innerRegularWRT : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ : MeasureTheory.Measure 𝓧} [inst : TopologicalSpace 𝓧]
  [OpensMeasurableSpace 𝓧] [MeasureTheory.IsFiniteMeasure μ],
  μ.InnerRegularWRT (fun s => IsCompact s ∧ IsClosed s) MeasurableSet → MeasureTheory.IsTightMeasureSet {μ}
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_eq_right_iff : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] {x y : P}, midpoint R x y = y ↔ x = y
-- Mathlib.Data.List.Permutation
List.mem_permutations_of_perm_lemma : ∀ {α : Type u_1} {is l : List α},
  (l.Perm ([] ++ is) → (∃ ts', ∃ (_ : ts'.Perm []), l = ts' ++ is) ∨ l ∈ is.permutationsAux []) →
    l.Perm is → l ∈ is.permutations
-- Mathlib.Topology.Order.LiminfLimsup
isCobounded_le_nhds : ∀ {α : Type u_2} [inst : Preorder α] [inst_1 : TopologicalSpace α] [BoundedGENhdsClass α] (a : α),
  Filter.IsCobounded (fun x1 x2 => x1 ≤ x2) (nhds a)
-- Mathlib.CategoryTheory.Subobject.Basic
/-- A ternary version of `Subobject.lower`.  -/
CategoryTheory.Subobject.lower₂ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y Z : C} →
      CategoryTheory.Functor (CategoryTheory.MonoOver X)
          (CategoryTheory.Functor (CategoryTheory.MonoOver Y) (CategoryTheory.MonoOver Z)) →
        CategoryTheory.Functor (CategoryTheory.Subobject X)
          (CategoryTheory.Functor (CategoryTheory.Subobject Y) (CategoryTheory.Subobject Z))
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.name : LeanSearchClient.SearchResult → String
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.integralAgainstBilinCLM_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {n : ℕ∞} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_6} {F₂ : Type u_7} {F₃ : Type u_8} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : Algebra ℝ 𝕜] [inst_12 : IsScalarTower ℝ 𝕜 F₁]
  [inst_13 : NormedSpace ℝ F₃] [inst_14 : IsScalarTower ℝ 𝕜 F₃] {B : F₁ →L[𝕜] F₂ →L[𝕜] F₃} {μ : MeasureTheory.Measure E}
  {φ : E → F₂} {f : TestFunction Ω F₁ n},
  (TestFunction.integralAgainstBilinCLM B μ φ) f =
    if MeasureTheory.LocallyIntegrableOn φ (↑Ω) μ then ∫ (x : E), (B (f x)) (φ x) ∂μ else 0
-- Init.Data.SInt.Lemmas
Int8.toInt64_lt : ∀ {a b : Int8}, a.toInt64 < b.toInt64 ↔ a < b
-- Mathlib.Data.Set.Insert
Set.ssubset_singleton_iff : ∀ {α : Type u_1} {s : Set α} {x : α}, s ⊂ {x} ↔ s = ∅
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.coe_neg : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (x : ↥S), ↑(-x) = -↑x
-- Mathlib.Order.LatticeIntervals
/-- `Ico a b` has a bottom element whenever `a < b`.  -/
Set.Ico.orderBot : {α : Type u_1} → [inst : PartialOrder α] → {a b : α} → [Fact (a < b)] → OrderBot ↑(Set.Ico a b)
-- Mathlib.Data.Sum.Basic
Sum.update_inr_apply_inr' : ∀ {α : Type u} {β : Type v} {γ : α ⊕ β → Type u_3} [inst : DecidableEq β] [inst_1 : DecidableEq (α ⊕ β)]
  {f : (i : α ⊕ β) → γ i} {i : β} {x : γ (Sum.inr i)} (j : β),
  Function.update f (Sum.inr i) x (Sum.inr j) = Function.update (fun j => f (Sum.inr j)) i x j
-- Mathlib.Data.Countable.Basic
instCountablePSigma : ∀ {α : Sort u} {π : α → Sort w} [Countable α] [∀ (a : α), Countable (π a)], Countable (PSigma π)
-- Mathlib.Data.Finset.Insert
Finset.subset_cons : ∀ {α : Type u_1} {s : Finset α} {a : α} (h : a ∉ s), s ⊆ Finset.cons a s h
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.uncurryRight_apply : ∀ {𝕜 : Type u} {n : ℕ} {Ei : Fin n.succ → Type wEi} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : Fin n.succ) → NormedAddCommGroup (Ei i)] [inst_2 : (i : Fin n.succ) → NormedSpace 𝕜 (Ei i)]
  [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G] (f : Ei i.castSucc [×n]→L[𝕜] Ei (Fin.last n) →L[𝕜] G)
  (m : (i : Fin n.succ) → Ei i), f.uncurryRight m = (f (Fin.init m)) (m (Fin.last n))
-- Mathlib.RingTheory.Lasker
/-- **Alias** of `Submodule.isLasker`.

---

The Lasker--Noether theorem: every submodule in a Noetherian module admits a decomposition into
primary submodules.  -/
Ideal.isLasker : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M],
  IsLasker R M
-- Mathlib.Algebra.Order.Monoid.Prod
Prod.instCanonicallyOrderedAdd : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : LE α] [CanonicallyOrderedAdd α] [inst_3 : Add β]
  [inst_4 : LE β] [CanonicallyOrderedAdd β], CanonicallyOrderedAdd (α × β)
-- Mathlib.Topology.Algebra.Group.SubmonoidClosure
closure_addSubmonoidClosure_eq_closure_addSubgroupClosure : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [CompactSpace G] [IsTopologicalAddGroup G]
  (s : Set G), closure ↑(AddSubmonoid.closure s) = closure ↑(AddSubgroup.closure s)
-- Lean.Data.KVMap
Lean.KVMap.get? : {α : Type} → [Lean.KVMap.Value α] → Lean.KVMap → Lean.Name → Option α
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'.XIsoOpcycles.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : ∀ (i' : ι'), K.HasHomology i'] {i : ι}
  (hi : e.BoundaryGE i),
  HomologicalComplex.truncGE'.XIsoOpcycles K e hi = HomologicalComplex.truncGE'.XIsoOpcycles K e hi
-- Mathlib.Algebra.Group.Action.Defs
/-- A vector addition is left-cancellative if it is pointwise injective on the left.  -/
IsLeftCancelVAdd : (G : Type u_9) → (P : Type u_10) → [VAdd G P] → Prop
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_iff_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} {k : α}, k ∈ t ↔ t.contains k = true
-- Init.Data.Array.Extract
Array.reverse_extract : ∀ {α : Type u_1} {as : Array α} {i j : ℕ}, (as.extract i j).reverse = as.reverse.extract (as.size - j) (as.size - i)
-- Mathlib.Algebra.Polynomial.Laurent
/-- The `simp` version of `mul_assoc`, in the presence of `T`'s.  -/
LaurentPolynomial.mul_T_assoc : ∀ {R : Type u_1} [inst : Semiring R] (f : LaurentPolynomial R) (m n : ℤ),
  f * LaurentPolynomial.T m * LaurentPolynomial.T n = f * LaurentPolynomial.T (m + n)
-- Mathlib.Topology.Spectral.Hom
/-- `SpectralMapClass F α β` states that `F` is a type of spectral maps.

You should extend this class when you extend `SpectralMap`.  -/
SpectralMapClass : (F : Type u_6) → (α : Type u_7) → (β : Type u_8) → [TopologicalSpace α] → [TopologicalSpace β] → [FunLike F α β] → Prop
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.aeval_pi_apply₂ : ∀ {R : Type u} [inst : CommSemiring R] {I : Type u_3} {A : I → Type u_4} [inst_1 : (i : I) → Semiring (A i)]
  [inst_2 : (i : I) → Algebra R (A i)] (x : (i : I) → A i) (p : Polynomial R) (j : I),
  (Polynomial.aeval x) p j = (Polynomial.aeval (x j)) p
-- Mathlib.RingTheory.TensorProduct.IsBaseChangePi
IsBaseChange.finsuppPow : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (ι : Type u_3)
  {M : Type u_6} {M' : Type u_7} [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M'] [inst_5 : Module R M]
  [inst_6 : Module R M'] [inst_7 : Module S M'] [inst_8 : IsScalarTower R S M'] {ε : M →ₗ[R] M'},
  IsBaseChange S ε → IsBaseChange S (Finsupp.mapRange.linearMap ε)
-- Mathlib.MeasureTheory.Measure.IntegralCharFun
MeasureTheory.integral_charFun_Icc : ∀ {μ : MeasureTheory.Measure ℝ} {r : ℝ} [MeasureTheory.IsFiniteMeasure μ],
  0 < r → ∫ (t : ℝ) in -r..r, MeasureTheory.charFun μ t = 2 * ↑r * ↑(∫ (x : ℝ), Real.sinc (r * x) ∂μ)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.ΓSpecIso_hom_fromSpec_app : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso (X.presheaf.obj (Opposite.op U))).hom
      (AlgebraicGeometry.Scheme.Hom.app hU.fromSpec U) =
    (AlgebraicGeometry.Spec (X.presheaf.obj (Opposite.op U))).presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Init.Data.String.Basic
String.Pos.ofSlice_inj : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} (pos₁ pos₂ : (s.slice p₀ p₁ h).Pos),
  String.Pos.ofSlice pos₁ = String.Pos.ofSlice pos₂ ↔ pos₁ = pos₂
-- Mathlib.NumberTheory.NumberField.Basic
/-- The ring homomorphism `(𝓞 K) →+* (𝓞 L)` given by restricting a ring homomorphism
`f : K →+* L` to `𝓞 K`.  -/
NumberField.RingOfIntegers.mapRingHom : {K : Type u_3} →
  {L : Type u_4} →
    [inst : Field K] → [inst_1 : Field L] → (K →+* L) → NumberField.RingOfIntegers K →+* NumberField.RingOfIntegers L