mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Equiv.Basic
Units.symm_mulRightLinearEquiv : ∀ {R : Type u_9} {A : Type u_10} [inst : Semiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (a : Aˣ), (Units.mulRightLinearEquiv R a).symm = Units.mulRightLinearEquiv R a⁻¹
-- Mathlib.Algebra.BigOperators.Pi
Fintype.sum_apply : ∀ {ι : Type u_1} {α : Type u_7} {M : α → Type u_8} [inst : Fintype ι] [inst_1 : (a : α) → AddCommMonoid (M a)] (a : α)
  (g : ι → (a : α) → M a), (∑ c, g c) a = ∑ c, g c a
-- Batteries.Data.List.Basic
List.dropSlice.eq_def : ∀ {α : Type u_1} (x x_1 : ℕ) (x_2 : List α),
  List.dropSlice x x_1 x_2 =
    match x, x_1, x_2 with
    | x, x_3, [] => []
    | 0, m, xs => List.drop m xs
    | n.succ, m, x :: xs => x :: List.dropSlice n m xs
-- Mathlib.Order.WithBot
WithBot.unbotD_mono : ∀ {α : Type u_1} {a : α} [inst : LE α] {x y : WithBot α}, x ≠ ⊥ → x ≤ y → WithBot.unbotD a x ≤ WithBot.unbotD a y
-- Mathlib.Topology.Algebra.Group.Basic
continuous_of_continuousAt_zero₂ : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {H : Type u_1} {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : TopologicalSpace M] [ContinuousAdd M] [inst_6 : AddGroup H]
  [inst_7 : TopologicalSpace H] [IsTopologicalAddGroup H] (f : G →+ H →+ M),
  ContinuousAt (fun x => (f x.1) x.2) (0, 0) →
    (∀ (x : G), ContinuousAt (⇑(f x)) 0) →
      (∀ (y : H), ContinuousAt (fun x => (f x) y) 0) → Continuous fun x => (f x.1) x.2
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- In order to check that a certain data is a `1`-hypercover of `S`, it suffices to
check that the data provides a covering of `S` and of the fibre products.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.mk' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {S : C} →
        (E : CategoryTheory.PreOneHypercover S) →
          [inst_1 : E.HasPullbacks] →
            E.sieve₀ ∈ J S →
              (∀ (i₁ i₂ : E.I₀), E.sieve₁' i₁ i₂ ∈ J (CategoryTheory.Limits.pullback (E.f i₁) (E.f i₂))) →
                J.OneHypercover S
-- Mathlib.InformationTheory.Hamming
hammingNorm.congr_simp : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] {inst_1 : (i : ι) → DecidableEq (β i)}
  [inst_2 : (i : ι) → DecidableEq (β i)] [inst_3 : (i : ι) → Zero (β i)] (x x_1 : (i : ι) → β i),
  x = x_1 → hammingNorm x = hammingNorm x_1
-- Std.Data.ExtDTreeMap.Basic
/-- Given a proof that a mapping for the given key is present, retrieves the mapping for the given key.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDTreeMap.get : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [inst : Std.TransCmp cmp] → [Std.LawfulEqCmp cmp] → (t : Std.ExtDTreeMap α β cmp) → (a : α) → a ∈ t → β a
-- Mathlib.Data.Set.Restrict
Set.domRestrict₂_comp_domRestrict₂ : ∀ {α : Type u_1} {π : α → Type u_6} {s t u : Set α} (hst : s ⊆ t) (htu : t ⊆ u),
  Set.domRestrict₂ hst ∘ Set.domRestrict₂ htu = Set.domRestrict₂ ⋯
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.mapπ₀_id_apply : ∀ {X : SSet} (x : X.π₀), SSet.mapπ₀ (CategoryTheory.CategoryStruct.id X) x = x
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_diff_eq_size_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (∀ (a : α), m₁.contains a = true → m₂.contains a = false) → (↑(m₁.diff m₂)).size = (↑m₁).size
-- Lean.Meta.Sym.Eta
_private.Lean.Meta.Sym.Eta.0.Lean.Meta.Sym.etaReduceWithCache.cache : Lean.Expr → Lean.Expr → StateRefT' IO.RealWorld (Std.HashMap Lean.Meta.Sym.ExprPtr Lean.Expr) Lean.CoreM Lean.Expr
-- Mathlib.Data.Num.ZNum
Num.mem_ofZNum' : ∀ {m : Num} {n : ZNum}, m ∈ Num.ofZNum' n ↔ n = m.toZNum
-- Mathlib.RingTheory.LocalIso
Algebra.IsLocalIso.span_isStandardOpenImmersion_eq_top : ∀ (R : Type u_1) (S : Type u_2) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [Algebra.IsLocalIso R S], Ideal.span {g | Algebra.IsStandardOpenImmersion R (Localization.Away g)} = ⊤
-- Init.Data.Array.Lemmas
Array.contains_flatMap : ∀ {β : Type u_1} {α : Type u_2} [inst : BEq β] {xs : Array α} {f : α → Array β} {x : β},
  (Array.flatMap f xs).contains x = xs.any fun a => (f a).contains x
-- Mathlib.Analysis.Convex.Between
wbtw_self_left : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] (x y : P), Wbtw R x x y
-- Init.Data.Float.Float32
/-- Computes the sine of a floating-point number in radians.

This function does not reduce in the kernel. It is implemented in compiled code by the C function
`sinf`.
 -/
Float32.sin : Float32 → Float32
-- Std.Http.Data.URI.Basic
Std.Http.URI.UserInfo.mk : Std.Http.URI.EncodedUserInfo → Option Std.Http.URI.EncodedUserInfo → Std.Http.URI.UserInfo
-- Mathlib.Logic.Function.Basic
Classical.arbitrary.congr_simp : ∀ (α : Sort u_3) [h : Nonempty α], Classical.arbitrary α = Classical.arbitrary α
-- Std.Data.HashSet.Lemmas
Std.HashSet.get!_eq_get!_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] [inst : Inhabited α]
  {a : α}, m.get! a = (m.get? a).get!
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.cyclotomic.eq_1 : ∀ (n : ℕ) (R : Type u_1) [inst : Ring R],
  Polynomial.cyclotomic n R = if h : n = 0 then 1 else Polynomial.map (Int.castRingHom R) ⋯.choose
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trStmts₁.eq_1 : ∀ (p : Turing.PartrecToTM2.Γ' → Bool) (k₁ k₂ : Turing.PartrecToTM2.K') (q : Turing.PartrecToTM2.Λ'),
  Turing.PartrecToTM2.trStmts₁ (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) =
    insert (Turing.PartrecToTM2.Λ'.move p k₁ k₂ q) (Turing.PartrecToTM2.trStmts₁ q)
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.SpecIso_inv_over : ∀ {n : Type u} (R : CommRingCat),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.SpecIso n R).inv
      (AlgebraicGeometry.AffineSpace n (AlgebraicGeometry.Spec R) ↘ AlgebraicGeometry.Spec R) =
    AlgebraicGeometry.Spec.map (CommRingCat.ofHom MvPolynomial.C)
-- Aesop.Util.OrderedHashSet
Aesop.OrderedHashSet.insert : {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → α → Aesop.OrderedHashSet α → Aesop.OrderedHashSet α
-- Init.Data.String.Iterate
/-- Creates an iterator over all bytes in `s`, starting from the last one and iterating towards
the first one.

Examples:

* `"abc".revBytes.toList = [99, 98, 97]`

* `"ab∀c".revBytes.toList = [99, 128, 136, 226, 98, 97]`
 -/
String.revBytes : String → Std.Iter UInt8
-- Mathlib.CategoryTheory.Limits.IndYoneda
CategoryTheory.Limits.colimitYonedaHomIsoLimit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] {I : Type v₁} [inst_1 : CategoryTheory.Category.{v₂, v₁} I]
  (D : CategoryTheory.Functor Iᵒᵖ Cᵒᵖ) (F : CategoryTheory.Functor Cᵒᵖ (Type u₂))
  [inst_2 : CategoryTheory.Limits.HasColimit (D.unop.comp CategoryTheory.yoneda)]
  [inst_3 : CategoryTheory.Limits.HasLimitsOfShape Iᵒᵖ (Type (max u₁ u₂))],
  CategoryTheory.Limits.colimitYonedaHomIsoLimit D F =
    CategoryTheory.Limits.colimitHomIsoLimitYoneda (D.unop.comp CategoryTheory.yoneda) F ≪≫
      CategoryTheory.Limits.HasLimit.isoOfNatIso
        ((D.comp (CategoryTheory.Prod.sectL Cᵒᵖ F)).isoWhiskerLeft (CategoryTheory.yonedaLemma C))
-- Mathlib.CategoryTheory.Monoidal.Opposite
/-- The identity functor on `C`, viewed as a functor from the monoidal opposite of `C` to `C`.  -/
CategoryTheory.unmopFunctor : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor Cᴹᵒᵖ C
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.ι_map_assoc : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f g : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f]
  [inst_3 : CategoryTheory.Limits.HasBiproduct g] (p : (j : J) → f j ⟶ g j) (j : J) {Z : C} (h : ⨁ g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι f j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.map p) h) =
    CategoryTheory.CategoryStruct.comp (p j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biproduct.ι g j) h)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.lcoeff_apply : ∀ (R : Type u) {σ : Type u_1} [inst : CommSemiring R] (m : σ →₀ ℕ) (p : MvPolynomial σ R),
  (MvPolynomial.lcoeff R m) p = MvPolynomial.coeff m p
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget.h : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {aig : Std.Sat.AIG α} {outWidth : ℕ}
  (self : Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayerTarget aig outWidth), outWidth = (self.len + 1) / 2 * self.w
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDocumentSymbolResult : Lean.ToJson Lean.Lsp.DocumentSymbolResult
-- Lean.Parser.Term
Lean.Parser.Term.funBinder.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Data.ENNReal.Inv
/-- See `ENNReal.mul_div_cancel'` for a stronger version.  -/
ENNReal.mul_div_cancel : ∀ {a b : ENNReal}, a ≠ 0 → a ≠ ⊤ → a * (b / a) = b
-- Mathlib.LinearAlgebra.Pi
LinearMap.iInf_ker_proj : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type i} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)], ⨅ i, (LinearMap.proj i).ker = ⊥
-- Init.Data.Range.Polymorphic.UInt
UInt64.rxcHasSize_eq_toBitVec : ∀ {lo : BitVec 64} {hi : UInt64}, Std.Rxc.HasSize.size { toBitVec := lo } hi = Std.Rxc.HasSize.size lo hi.toBitVec
-- Mathlib.Data.ENat.Lattice
ENat.smul_iSup : ∀ {ι : Sort u_2} {R : Type u_4} [inst : SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (f : ι → ℕ∞) (c : R),
  c • ⨆ i, f i = ⨆ i, c • f i
-- Std.Data.ExtTreeMap.Basic
/-- Returns a list of all keys present in the tree map in ascending  order.  -/
Std.ExtTreeMap.keys : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → List α
-- Init.Data.List.Basic
List.nil_removeAll : ∀ {α : Type u} [inst : BEq α] {ys : List α}, [].removeAll ys = []
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decomposeLinearEquiv_symm_lof : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (ℳ : ι → Submodule R M) [inst_4 : DirectSum.Decomposition ℳ] (i : ι) (x : ↥(ℳ i)),
  (DirectSum.decomposeLinearEquiv ℳ).symm ((DirectSum.lof R ι (fun i => ↥(ℳ i)) i) x) = ↑x
-- Aesop.Script.SpecificTactics
Aesop.Script.TacticBuilder.splitTarget : Aesop.Script.TacticBuilder
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.norm_toLp_fst : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : SeminormedAddCommGroup α]
  [inst_1 : SeminormedAddCommGroup β] (x : α), ‖WithLp.toLp p (x, 0)‖ = ‖x‖
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CompletelyPositiveMapClass.instOrderHomClass : ∀ {F : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} [inst : NonUnitalCStarAlgebra A₁] [inst_1 : NonUnitalCStarAlgebra A₂]
  [inst_2 : PartialOrder A₁] [inst_3 : PartialOrder A₂] [inst_4 : StarOrderedRing A₁] [inst_5 : StarOrderedRing A₂]
  [inst_6 : FunLike F A₁ A₂] [LinearMapClass F ℂ A₁ A₂] [CompletelyPositiveMapClass F A₁ A₂], OrderHomClass F A₁ A₂
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_eq_get!_get? : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {a : α}, Std.DHashMap.Const.get! m a = (Std.DHashMap.Const.get? m a).get!
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.instContinuousMapClass : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F], ContinuousMapClass (SchwartzMap E F) E F
-- Init.Data.UInt.Lemmas
USize.ofNat_lt_iff_lt : ∀ {a b : ℕ}, a < USize.size → b < USize.size → (USize.ofNat a < USize.ofNat b ↔ a < b)
-- Mathlib.Data.FunLike.IsApply
/-- **Alias** of `FunLike.coe_smul`. -/
FunLike.coe_smul' : ∀ {M : Type u_1} {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : SMul M F]
  [inst_2 : SMul M β] [IsSMulApply M F α β] (n : M) (f : F), ⇑(n • f) = n • ⇑f
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.corootSpace_zero_eq_bot : ∀ (K : Type u_2) (L : Type u_3) [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] (H : LieSubalgebra K L) [inst_4 : H.IsCartanSubalgebra] [LieAlgebra.IsKilling K L],
  LieAlgebra.corootSpace 0 = ⊥
-- Mathlib.GroupTheory.PushoutI
/-- We have exactly one element of each coset of the base group  -/
Monoid.PushoutI.NormalWord.Transversal.compl : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} (self : Monoid.PushoutI.NormalWord.Transversal φ) (i : ι),
  Subgroup.IsComplement (↑(φ i).range) (self.set i)
-- Std.Http.Data.Headers.Basic
Std.Http.Header.instReprContentLength : Repr Std.Http.Header.ContentLength
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.parentD_of_not_lt : ∀ {i : ℕ} {arr : Array Batteries.UFNode}, ¬i < arr.size → Batteries.UnionFind.parentD arr i = i
-- Aesop.RuleTac.Preprocess
/-- This `RuleTac` is applied once to the root goal, before any other rules are
tried.
 -/
Aesop.RuleTac.preprocess : Aesop.RuleTac
-- Mathlib.CategoryTheory.Sites.Point.Category
CategoryTheory.GrothendieckTopology.Point.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {Φ₁ Φ₂ : J.Point}
  {f g : Φ₁ ⟶ Φ₂}, f.hom = g.hom → f = g
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.generateFrom_iUnion_memPartition_le : ∀ {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α},
  (∀ (n : ℕ), MeasurableSet (t n)) → MeasurableSpace.generateFrom (⋃ n, memPartition t n) ≤ m
-- Mathlib.Tactic.Simps.Basic
/-- Join the components with `_`, or append `_def` if there is only one component.  -/
_private.Mathlib.Tactic.Simps.Basic.0.NameStruct.toName : NameStruct✝ → Lean.Name
-- Mathlib.Topology.MetricSpace.IsometricSMul
Metric.preimage_add_left_ball : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoMetricSpace G] [IsIsometricVAdd G G] (a b : G) (r : ℝ),
  (fun x => a + x) ⁻¹' Metric.ball b r = Metric.ball (-a + b) r
-- Mathlib.Analysis.Fourier.FourierTransform
Real.Lp.coe_fourierTransformInv : ∀ {V : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [inst_2 : NormedAddCommGroup V]
  [inst_3 : InnerProductSpace ℝ V] [inst_4 : MeasurableSpace V] [inst_5 : BorelSpace V] [inst_6 : FiniteDimensional ℝ V]
  (f : ↥(MeasureTheory.Lp E 1 MeasureTheory.volume)),
  ⇑(Real.Lp.fourierTransformInv f) = FourierTransformInv.fourierInv ↑↑f
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.coe_id : ∀ (α : Type u_2) [inst : CompleteLattice α], ⇑(CompleteLatticeHom.id α) = id
-- Mathlib.Analysis.Calculus.LineDeriv.Measurable
stronglyMeasurable_lineDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [LocallyCompactSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MeasurableSpace E] [OpensMeasurableSpace E]
  {F : Type u_3} [inst_6 : NormedAddCommGroup F] [inst_7 : NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {v : E}
  [SecondCountableTopologyEither E F], Continuous f → MeasureTheory.StronglyMeasurable fun x => lineDeriv 𝕜 f x v
-- Mathlib.RingTheory.AlgebraTower
Module.Basis.algebraMapCoeffs_repr : ∀ {R : Type u_1} (A : Type u_3) {ι : Type u_5} {M : Type u_6} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M] (b : Module.Basis ι R M) (h : Function.Bijective ⇑(algebraMap R A)) (m : M),
  (Module.Basis.algebraMapCoeffs A b h).repr m = Finsupp.mapRange ⇑(algebraMap R A) ⋯ (b.repr m)
-- Mathlib.RingTheory.RingHom.FiniteType
RingHom.localization_away_map_finiteType : ∀ (R S R' S' : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing R'] [inst_3 : CommRing S']
  [inst_4 : Algebra R R'] (f : R →+* S) [inst_5 : Algebra S S'] (r : R) [inst_6 : IsLocalization.Away r R']
  [inst_7 : IsLocalization.Away (f r) S'], f.FiniteType → (IsLocalization.Away.map R' S' f r).FiniteType
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.bddBelow_projectiveSemiNormAux : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (x : PiTensorProduct 𝕜 fun i => E i),
  BddBelow (Set.range fun p => PiTensorProduct.projectiveSeminormAux ↑p)
-- Mathlib.RingTheory.Finiteness.Cardinality
Module.finite_of_finite : ∀ (R : Type u_1) {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Finite R]
  [Module.Finite R M], Finite M
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instToJsonDiagnosticRelatedInformation.toJson : Lean.Lsp.DiagnosticRelatedInformation → Lean.Json
-- Lean.Parser.Tactic.Doc
/-- Get the user-facing name and docstring for a tactic tag.
 -/
Lean.Parser.Tactic.Doc.tagInfo : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m (Option (String × Option String))
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Free
/-- The unit of `PresheafOfModules.freeAdjunction`.  -/
PresheafOfModules.freeAdjunctionUnit : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (R : CategoryTheory.Functor Cᵒᵖ RingCat) →
      (F : CategoryTheory.Functor Cᵒᵖ (Type u)) →
        F ⟶ (PresheafOfModules.freeObj F).presheaf.comp (CategoryTheory.forget Ab)
-- Mathlib.CategoryTheory.Square
/-- The top-left evaluation `Square C ⥤ C`.  -/
CategoryTheory.Square.evaluation₁ : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor (CategoryTheory.Square C) C
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsValidSearchFrom.endPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice},
  String.Slice.Pattern.Model.IsValidSearchFrom pat s.endPos []
-- Mathlib.SetTheory.Cardinal.Regular
/-- An inaccessible cardinal is a strong limit, see `IsInaccessible.isStrongLimit`.  -/
Cardinal.IsInaccessible.isStrongPrelimit : ∀ {c : Cardinal.{u_1}}, c.IsInaccessible → c.IsStrongPrelimit
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
SymmetricAlgebra.lift_ι : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  SymmetricAlgebra.lift (SymmetricAlgebra.ι R M) = AlgHom.id R (SymmetricAlgebra R M)
-- Lean.Elab.MutualDef
/-- Elaborates the termination hints in a `declVal` syntax.  -/
_private.Lean.Elab.MutualDef.0.Lean.Elab.Term.declValToTerminationHint : Lean.Syntax → Lean.Elab.TermElabM Lean.Elab.TerminationHints
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.beq'.eq_1 : ∀ (p₁ : Int.Internal.Linear.Poly),
  p₁.beq' =
    Int.Internal.Linear.Poly.rec (motive := fun x => Int.Internal.Linear.Poly → Bool)
      (fun k₁ p₂ => Int.Internal.Linear.Poly.rec (fun k₂ => k₁.beq' k₂) (fun x x_1 x_2 x_3 => false) p₂)
      (fun k₁ v₁ x ih p₂ =>
        Int.Internal.Linear.Poly.rec (fun x => false)
          (fun k₂ v₂ p₂ x => (k₁.beq' k₂).and' ((Nat.beq v₁ v₂).and' (ih p₂))) p₂)
      p₁
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
/-- `seminormFromConst_seq c f 0` is the constant sequence zero.  -/
seminormFromConst_seq_zero : ∀ {R : Type u_1} [inst : CommRing R] (c : R) {f : RingSeminorm R}, f 0 = 0 → seminormFromConst_seq c f 0 = 0
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.exact : ∀ {x y : PSet.{u_1}}, ZFSet.mk x = ZFSet.mk y → x.Equiv y
-- Mathlib.Data.Int.ModEq
Int.ModEq.add_right : ∀ {n a b : ℤ} (c : ℤ), a ≡ b [ZMOD n] → a + c ≡ b + c [ZMOD n]
-- Mathlib.Algebra.Module.Torsion.Free
smul_left_injective : ∀ (R : Type u_1) {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {m : M}
  [IsCancelMulZero R] [Module.IsTorsionFree R M], m ≠ 0 → Function.Injective fun x => x • m
-- Mathlib.Analysis.Complex.Basic
/-- The slit plane includes the open unit ball of radius `1` around `1`.  -/
Complex.ball_one_subset_slitPlane : Metric.ball 1 1 ⊆ Complex.slitPlane
-- Mathlib.MeasureTheory.Function.SpecialFunctions.Basic
AEMeasurable.log : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  AEMeasurable f μ → AEMeasurable (fun x => Real.log (f x)) μ
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Functor.IsLocalization.of_iso : ∀ {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] (W : CategoryTheory.MorphismProperty C)
  {L₁ L₂ : CategoryTheory.Functor C D} (e : L₁ ≅ L₂) [L₁.IsLocalization W], L₂.IsLocalization W
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.continuousOn_coordChange : ∀ {ι : Type u_5} {B : Type u_6} [inst : TopologicalSpace B] {F : Type u_7} [inst_1 : TopologicalSpace F]
  (self : FiberBundleCore ι B F) (i j : ι),
  ContinuousOn (fun p => self.coordChange i j p.1 p.2) ((self.baseSet i ∩ self.baseSet j) ×ˢ Set.univ)
-- Init.Data.Range.Polymorphic.SInt
Int32.instUpwardEnumerable : Std.PRange.UpwardEnumerable Int32
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.prodMap_apply : ∀ {k : Type u_10} {P₁ : Type u_11} {P₂ : Type u_12} {P₃ : Type u_13} {P₄ : Type u_14} {V₁ : Type u_15} {V₂ : Type u_16}
  {V₃ : Type u_17} {V₄ : Type u_18} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁] [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂]
  [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂] [inst_9 : AddCommGroup V₃] [inst_10 : Module k V₃]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : TopologicalSpace P₃] [inst_13 : AddCommGroup V₄] [inst_14 : Module k V₄]
  [inst_15 : AddTorsor V₄ P₄] [inst_16 : TopologicalSpace P₄] (f : P₁ →ᴬ[k] P₂) (g : P₃ →ᴬ[k] P₄) (x : P₁ × P₃),
  (f.prodMap g) x = (f x.1, g x.2)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKey_alter_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [Inhabited α] {k : α} {f : Option β → Option β} {hc : k ∈ Std.ExtDTreeMap.Const.alter t k f},
  (Std.ExtDTreeMap.Const.alter t k f).getKey k hc = k
-- Mathlib.Algebra.Order.Quantale
/-- An additive quantale is an additive semigroup distributing over a complete lattice.  -/
IsAddQuantale : (α : Type u_1) → [AddSemigroup α] → [CompleteLattice α] → Prop
-- Mathlib.Topology.Algebra.Group.Quotient
QuotientGroup.instContinuousSMul : ∀ {G : Type u_2} [inst : Group G] [inst_1 : TopologicalSpace G] [ContinuousMul G] {N : Subgroup G},
  ContinuousSMul G (G ⧸ N)
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.pow_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (e : C ≌ C), e ^ 1 = e
-- Mathlib.Analysis.Normed.Algebra.TrivSqZeroExt
TrivSqZeroExt.exp_def_of_smul_comm : ∀ {R : Type u_3} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [inst_3 : Module Rᵐᵒᵖ M]
  [inst_4 : SMulCommClass R Rᵐᵒᵖ M] [inst_5 : TopologicalSpace R] [inst_6 : TopologicalSpace M]
  [inst_7 : IsTopologicalRing R] [inst_8 : IsTopologicalAddGroup M] [inst_9 : ContinuousSMul R M]
  [inst_10 : ContinuousSMul Rᵐᵒᵖ M] [Algebra ℚ R] [Module ℚ M] [T2Space R] [T2Space M] (x : TrivSqZeroExt R M),
  MulOpposite.op x.fst • x.snd = x.fst • x.snd →
    NormedSpace.exp x = TrivSqZeroExt.inl (NormedSpace.exp x.fst) + TrivSqZeroExt.inr (NormedSpace.exp x.fst • x.snd)
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.mem_inf : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {p q : Submodule R M} {x : M}, x ∈ p ⊓ q ↔ x ∈ p ∧ x ∈ q