mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.Grp.Colimits
AddCommGrpCat.hasColimit : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] [Small.{w, u} J] (F : CategoryTheory.Functor J AddCommGrpCat),
  CategoryTheory.Limits.HasColimit F
-- Mathlib.Algebra.Group.Subgroup.Finite
AddSubgroup.card_le_one_iff_eq_bot : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) [Finite ↥H], Nat.card ↥H ≤ 1 ↔ H = ⊥
-- Mathlib.Data.ENat.Lattice
ENat.exists_eq_iInf : ∀ {ι : Sort u_1} [Nonempty ι] (f : ι → ℕ∞), ∃ a, f a = ⨅ x, f x
-- Mathlib.Algebra.Category.ModuleCat.Localization
ModuleCat.instPreservesFiniteLimitsLocalizationLocalizedModuleFunctor : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Small.{v, u} R] (S : Submonoid R),
  CategoryTheory.Limits.PreservesFiniteLimits (ModuleCat.localizedModuleFunctor S)
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_shiftRight : ∀ (a b : USize) (h : System.Platform.numBits = 64), (a >>> b).toBitVec64 h = a.toBitVec64 h >>> (b.toBitVec64 h % 64)
-- Std.Async.ContextAsync
/-- Cancels the current context with the given reason, cascading to all child contexts.
Cancellation is cooperative, operations must explicitly check `isCancelled` or use `awaitCancellation` to respond.
 -/
Std.Async.ContextAsync.cancel : Std.CancellationReason → Std.Async.ContextAsync Unit
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
Std.IterM.attachWith.eq_1 : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α m β] (it : Std.IterM m β)
  (P : β → Prop) (h : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out),
  it.attachWith P h = { internalState := { inner := it, invariant := h } }
-- Mathlib.GroupTheory.Focal
AddSubgroup.focalAddSubgroup.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G),
  H.focalAddSubgroup = AddSubgroup.closure {g | g ∈ H ∧ ∃ x ∈ H, ∃ u, g = ⁅x, u⁆}
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {m₁ m₂ : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Raw.Const.getD (m₁ ∩ m₂) k fallback =
          if m₂.contains k = true then Std.DTreeMap.Raw.Const.getD m₁ k fallback else fallback
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.PreInstance.mk : Lean.Expr → Array Lean.Expr → Lean.Meta.Grind.PreInstance
-- Mathlib.Analysis.RCLike.Basic
/-- The real part in an `RCLike` field, as a continuous linear map.  -/
RCLike.reCLM : {K : Type u_1} → [inst : RCLike K] → StrongDual ℝ K
-- Mathlib.CategoryTheory.Iso
CategoryTheory.Functor.map_hom_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) [inst_2 : CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.comp (F.map f) (F.map (CategoryTheory.inv f)) =
    CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Data.List.Defs
/-- Right-biased version of `List.map₂`. `map₂Right f as bs` applies `f` to each
pair `aᵢ ∈ as` and `bᵢ ∈ bs`. If `as` is shorter than `bs`, `f` is applied to
`none` for the remaining `bᵢ`.

```
map₂Right Prod.mk [1, 2] ['a'] = [(some 1, 'a')]

map₂Right Prod.mk [1] ['a', 'b'] = [(some 1, 'a'), (none, 'b')]

map₂Right f as bs = (map₂Right' f as bs).fst
```
 -/
List.map₂Right : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → (Option α → β → γ) → List α → List β → List γ
-- Mathlib.Algebra.BigOperators.Ring.Finset
Nat.sum_div : ∀ {ι : Type u_5} {s : Finset ι} {f : ι → ℕ} {n : ℕ}, (∀ i ∈ s, n ∣ f i) → (∑ i ∈ s, f i) / n = ∑ i ∈ s, f i / n
-- Mathlib.Topology.Algebra.Group.Matrix
/-- The determinant is continuous as a map from the general linear group to the units.  -/
Matrix.GeneralLinearGroup.continuous_det : ∀ {n : Type u_1} {R : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing R]
  [inst_3 : TopologicalSpace R] [IsTopologicalRing R], Continuous ⇑Matrix.GeneralLinearGroup.det
-- Mathlib.Algebra.Group.Action.Pi
Pi.faithfulSMul : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [Nonempty ι] [inst : (i : ι) → SMul M (α i)]
  [∀ (i : ι), Nonempty (α i)] [∀ (i : ι), FaithfulSMul M (α i)], FaithfulSMul M ((i : ι) → α i)
-- Mathlib.MeasureTheory.Order.Lattice
/-- **Alias** of `AEMeasurable.sup`. -/
AEMeasurable.sup' : ∀ {M : Type u_1} [inst : MeasurableSpace M] {α : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → M} [inst_1 : Max M] [MeasurableSup₂ M], AEMeasurable f μ → AEMeasurable g μ → AEMeasurable (f ⊔ g) μ
-- Mathlib.SetTheory.Ordinal.Veblen
_private.Mathlib.SetTheory.Ordinal.Veblen.0.Ordinal.veblenWith.match_1.splitter : (o : Ordinal.{u_1}) →
  (motive : { x // x ∈ Set.Iio o } → Sort u_2) →
    (x : { x // x ∈ Set.Iio o }) → ((x : Ordinal.{u_1}) → (property : x ∈ Set.Iio o) → motive ⟨x, property⟩) → motive x
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.diagramIsoParallelFamily_inv_app : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C)
  (X : CategoryTheory.Limits.WalkingParallelFamily J),
  (CategoryTheory.Limits.diagramIsoParallelFamily F).inv.app X = CategoryTheory.eqToHom ⋯
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropPrefix?_congr : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s t : String.Slice},
  s.copy = t.copy → Option.map String.Slice.copy (s.dropPrefix? pat) = Option.map String.Slice.copy (t.dropPrefix? pat)
-- Mathlib.Algebra.GroupWithZero.Defs
/-- A type `M` is a `CancelMonoidWithZero` if it is a monoid with zero element, `0` is left
and right absorbing, and left/right multiplication by a non-zero element is injective.  -/
CancelMonoidWithZero : Type u_2 → Type u_2
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint_y : ∀ {X Y S : AlgebraicGeometry.Scheme} {f : X ⟶ S} {g : Y ⟶ S} (t : ↥(CategoryTheory.Limits.pullback f g)),
  (AlgebraicGeometry.Scheme.Pullback.Triplet.ofPoint t).y = (CategoryTheory.Limits.pullback.snd f g) t
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visitChild.match_1.eq_5 : ∀ (motive : Lean.Expr → Sort u_1) (declName : Lean.Name) (us : List Lean.Level)
  (h_1 : (a : Lean.Literal) → motive (Lean.Expr.lit a)) (h_2 : (mvarId : Lean.MVarId) → motive (Lean.Expr.mvar mvarId))
  (h_3 : (deBruijnIndex : ℕ) → motive (Lean.Expr.bvar deBruijnIndex))
  (h_4 : (fvarId : Lean.FVarId) → motive (Lean.Expr.fvar fvarId))
  (h_5 : (declName : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const declName us))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (e : Lean.Expr) → motive e),
  (match Lean.Expr.const declName us with
    | Lean.Expr.lit a => h_1 a
    | Lean.Expr.mvar mvarId => h_2 mvarId
    | Lean.Expr.bvar deBruijnIndex => h_3 deBruijnIndex
    | Lean.Expr.fvar fvarId => h_4 fvarId
    | Lean.Expr.const declName us => h_5 declName us
    | Lean.Expr.sort u => h_6 u
    | e => h_7 e) =
    h_5 declName us
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.variable : Lean.Lsp.SymbolKind
-- Mathlib.Order.Filter.Extr
/-- **Alias** of the reverse direction of `isMinOn_dual_iff`. -/
IsMaxOn.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {s : Set α} {a : α},
  IsMaxOn f s a → IsMinOn (⇑OrderDual.toDual ∘ f) s a
-- Mathlib.CategoryTheory.EpiMono
/-- A split epimorphism is a morphism `f : X ⟶ Y` with a given section `section_ f : Y ⟶ X`
such that `section_ f ≫ f = 𝟙 Y`.
(Note that `section` is a reserved keyword, so we append an underscore.)

Every split epimorphism is an epimorphism.
 -/
CategoryTheory.SplitEpi : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (X ⟶ Y) → Type v₁
-- Lean.PrettyPrinter.Delaborator.Basic
/-- Registers an unexpander for applications of a given constant.

`@[app_unexpander c]` registers a `Lean.PrettyPrinter.Unexpander` for applications of the constant
`c`. The unexpander is passed the result of pre-pretty printing the application *without*
implicitly passed arguments. If `pp.explicit` is set to true or `pp.notation` is set to false,
it will not be called at all.

Unexpanders work as an alternative for delaborators (`@[app_delab]`) that can be used without
special imports. This however also makes them much less capable since they can only transform
syntax and don't have access to the expression tree.
 -/
Lean.PrettyPrinter.Delaborator.appUnexpanderAttribute : Lean.KeyedDeclsAttribute Lean.PrettyPrinter.Unexpander
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- **Alias** of `MonoidAlgebra.coeff_mul_apply_left`. -/
MonoidAlgebra.mul_apply_left : ∀ {R : Type u_1} {G : Type u_3} [inst : Semiring R] [inst_1 : Group G] (x y : MonoidAlgebra R G) (g : G),
  (x * y).coeff g = x.coeff.sum fun h r => r * y.coeff (h⁻¹ * g)
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
TensorProduct.tensorQuotEquivQuotSMul_symm_mk : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (I : Ideal R)
  (x : M), (TensorProduct.tensorQuotEquivQuotSMul M I).symm (Submodule.Quotient.mk x) = x ⊗ₜ[R] 1
-- Mathlib.Topology.Bornology.Basic
Bornology.IsCobounded.superset : ∀ {α : Type u_2} {x : Bornology α} {s t : Set α}, Bornology.IsCobounded s → s ⊆ t → Bornology.IsCobounded t
-- Mathlib.CategoryTheory.ObjectProperty.Opposite
CategoryTheory.ObjectProperty.unop_monotone : ∀ {C : Type u} [inst : CategoryTheory.CategoryStruct.{v, u} C] {P Q : CategoryTheory.ObjectProperty Cᵒᵖ},
  P ≤ Q → P.unop ≤ Q.unop
-- Mathlib.Order.Filter.Prod
Filter.comap_prodMap_prod : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (lb : Filter β) (ld : Filter δ),
  Filter.comap (Prod.map f g) (lb ×ˢ ld) = Filter.comap f lb ×ˢ Filter.comap g ld
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.mapHomologicalComplexObjIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (F : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel] {D : Type u_3}
  [inst_3 : CategoryTheory.Category.{v_2, u_3} D] [inst_4 : CategoryTheory.Preadditive D]
  (H : CategoryTheory.Functor C D) [inst_5 : H.Additive]
  [inst_6 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (F.X i) (F.X i)]
  [inst_7 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F) (-CategoryTheory.CategoryStruct.id F))]
  [inst_8 :
    ∀ (i : ι),
      CategoryTheory.Limits.HasBinaryBiproduct (((H.mapHomologicalComplex c).obj F).X i)
        (((H.mapHomologicalComplex c).obj F).X i)]
  [inst_9 :
    HomologicalComplex.HasHomotopyCofiber
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F))
        (-CategoryTheory.CategoryStruct.id ((H.mapHomologicalComplex c).obj F)))]
  [inst_10 :
    HomologicalComplex.HasHomotopyCofiber
      ((H.mapHomologicalComplex c).map
        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id F) (-CategoryTheory.CategoryStruct.id F)))]
  (hc : ∀ (j : ι), ∃ i, c.Rel i j),
  HomologicalComplex.cylinder.mapHomologicalComplexObjIso F H hc =
    HomologicalComplex.cylinder.mapHomologicalComplexObjIso F H hc
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.isCycle_cycleBypass : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] {w : G.Walk v v},
  w ≠ SimpleGraph.Walk.nil → w.IsTrail → w.cycleBypass.IsCycle
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.forget_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {X Y : CategoryTheory.AddMon C} (f : X ⟶ Y), (CategoryTheory.AddMon.forget C).map f = f.hom
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.evalWithUnfoldingAll : Lean.Elab.Tactic.Tactic
-- Std.Http.Data.URI.Basic
Std.Http.URI.instBEqHost : BEq Std.Http.URI.Host
-- Mathlib.CategoryTheory.Monoidal.Closed.Ideal
/-- If the reflector preserves binary products, the subcategory is an exponential ideal.
This is the converse of `preservesBinaryProductsOfExponentialIdeal`.
 -/
CategoryTheory.exponentialIdeal_of_preservesBinaryProducts : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  (i : CategoryTheory.Functor D C) [inst_2 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_3 : CategoryTheory.Reflective i] [inst_4 : CategoryTheory.MonoidalClosed C]
  [CategoryTheory.CartesianMonoidalCategory D]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair)
      (CategoryTheory.reflector i)],
  CategoryTheory.ExponentialIdeal i
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.normalizeBound : Lean.Expr → Lean.Meta.Grind.GrindM Lean.Meta.Grind.Arith.Cutsat.SymbolicBound
-- Mathlib.Algebra.Homology.DerivedCategory.Linear
DerivedCategory.instLinear : (R : Type t) →
  [inst : Ring R] →
    (C : Type u) →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.Abelian C] →
          [CategoryTheory.Linear R C] → [inst_4 : HasDerivedCategory C] → CategoryTheory.Linear R (DerivedCategory C)
-- Mathlib.Analysis.Meromorphic.Order
/-- The order multiplies by `n` when taking a meromorphic function to its `n`th power.  -/
meromorphicOrderAt_pow : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_4} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'} {x : 𝕜},
  MeromorphicAt f x → ∀ {n : ℕ}, meromorphicOrderAt (f ^ n) x = ↑n * meromorphicOrderAt f x
-- Mathlib.Data.Multiset.Sort
Multiset.sort_range : ∀ (n : ℕ), ((Multiset.range n).sort fun a b => a ≤ b) = List.range n
-- Mathlib.RingTheory.AlgebraicIndependent.Transcendental
AlgebraicIndependent.option_iff_transcendental : ∀ {ι : Type u_1} {R : Type u_3} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A]
  [inst_2 : Algebra R A],
  AlgebraicIndependent R x →
    ∀ (a : A), (AlgebraicIndependent R fun o => o.elim a x) ↔ Transcendental (↥(Algebra.adjoin R (Set.range x))) a
-- Mathlib.Algebra.Order.Group.Abs
mabs_div : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] (a b : G), |a / b|ₘ ≤ |a|ₘ * |b|ₘ
-- Init.Data.String.Defs
String.Pos.Raw.IsValid.isValidUTF8_extract_zero : ∀ {s : String} {off : String.Pos.Raw}, String.Pos.Raw.IsValid s off → (s.toByteArray.extract 0 off.byteIdx).IsValidUTF8
-- Mathlib.Algebra.Order.Group.Lattice
pow_two_semiclosed : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] [MulLeftMono α] [MulRightMono α] {a : α}, 1 ≤ a ^ 2 → 1 ≤ a
-- Mathlib.Topology.Algebra.Group.Basic
isClosed_setOfPred_map_neg : ∀ (G₁ : Type u_2) (G₂ : Type u_3) [inst : TopologicalSpace G₂] [T2Space G₂] [inst_2 : Neg G₁] [inst_3 : Neg G₂]
  [ContinuousNeg G₂], IsClosed {f | ∀ (x : G₁), f (-x) = -f x}
-- Mathlib.Algebra.MvPolynomial.Equiv
/-- **Alias** of `RingEquiv.apply_symm_apply`. -/
MvPolynomial.sumToIter_iterToSum : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (e : R ≃+* S) (x : S),
  e (e.symm x) = x
-- Init.Omega.Int
Lean.Omega.Int.ofNat_natAbs : ∀ (a : ℤ), ↑a.natAbs = if 0 ≤ a then a else -a
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.associator_naturality_middle_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C) {Y Y' : C}
  (f : Y ⟶ Y') (Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y' Z) ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f) Z)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y' Z).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z))
        h)
-- Init.SimpLemmas
Bool.not_eq_false : ∀ (b : Bool), (¬b = false) = (b = true)
-- Mathlib.Data.Opposite
Opposite.unop_injective : ∀ {α : Sort u}, Function.Injective Opposite.unop
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- `RingFunc.one`, but with the defeq type `Language.ring.Functions 0` instead
of `RingFunc 0`  -/
FirstOrder.Ring.oneFunc : FirstOrder.Language.ring.Functions 0
-- Std.Http.Protocol.H1.Parser
/-- Parses a hexadecimal integer (one or more hex digits, up to 16 digits).
Used for chunk-size lines in chunked transfer encoding.
 -/
_private.Std.Http.Protocol.H1.Parser.0.Std.Http.Protocol.H1.hex : Std.Internal.Parsec.ByteArray.Parser ℕ
-- Mathlib.Analysis.RCLike.Basic
LinearIsometryEquiv.smul_apply : ∀ {𝕜 : Type u_3} {V : Type u_4} {W : Type u_5} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : Module 𝕜 V] [inst_3 : SeminormedAddCommGroup W] [inst_4 : NormedSpace 𝕜 W] (e : V ≃ₗᵢ[𝕜] W)
  (α : ↥(unitary 𝕜)) (x : V), (α • e) x = ↑α • e x
-- Mathlib.Topology.Algebra.NonUnitalStarAlgebra
NonUnitalStarSubalgebra.isClosed_topologicalClosure : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : Star A]
  [inst_3 : NonUnitalSemiring A] [inst_4 : Module R A] [inst_5 : ContinuousStar A] [inst_6 : ContinuousConstSMul R A]
  [inst_7 : IsSemitopologicalSemiring A] (s : NonUnitalStarSubalgebra R A), IsClosed ↑s.topologicalClosure
-- Mathlib.CategoryTheory.Abelian.LeftDerived
CategoryTheory.Functor.leftDerivedZeroIsoSelf_hom_inv_id_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  [inst_2 : CategoryTheory.Abelian C] [inst_3 : CategoryTheory.HasProjectiveResolutions C]
  [inst_4 : CategoryTheory.Abelian D] (F : CategoryTheory.Functor C D) [inst_5 : F.Additive]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteColimits F] {Z : CategoryTheory.Functor C D} (h : F.leftDerived 0 ⟶ Z),
  CategoryTheory.CategoryStruct.comp F.fromLeftDerivedZero
      (CategoryTheory.CategoryStruct.comp F.leftDerivedZeroIsoSelf.inv h) =
    h
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.universalAddHom.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {T : Type u_2}
  [inst_2 : AddMonoid T] (f : R →+ T) (fS : ↥S →+ AddUnits T) (hf : ∀ (s : ↥S), f ↑s = ↑(fS s)),
  AddOreLocalization.universalAddHom f fS hf =
    { toFun := fun x => AddOreLocalization.liftExpand (fun r s => ↑(-fS s) + f r) ⋯ x, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.toContinuousMap_toContinuousAddMonoidHom : ∀ {A : Type u_2} {B : Type u_3} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {F : Type u_7} [inst_4 : FunLike F A B] [inst_5 : AddMonoidHomClass F A B]
  [inst_6 : ContinuousMapClass F A B] (f : F), ↑↑f = ↑f
-- Mathlib.Analysis.Fourier.LpSpace
MeasureTheory.Lp.instFourierPairInv : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [inst_2 : BorelSpace E]
  [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace ℂ F] [inst_5 : CompleteSpace F]
  [inst_6 : InnerProductSpace ℝ E] [inst_7 : FiniteDimensional ℝ E],
  FourierInvPair ↥(MeasureTheory.Lp F 2 MeasureTheory.volume) ↥(MeasureTheory.Lp F 2 MeasureTheory.volume)
-- Mathlib.Order.LiminfLimsup
Filter.liminf_eq_sSup_sInf : ∀ {ι : Type u_6} {R : Type u_7} (F : Filter ι) [inst : CompleteLattice R] (a : ι → R),
  Filter.liminf a F = sSup ((fun I => sInf (a '' I)) '' F.sets)
-- Init.Data.List.Find
List.isNone_findFinIdx? : ∀ {α : Type u_1} {l : List α} {p : α → Bool}, (List.findFinIdx? p l).isNone = l.all fun x => decide ¬p x = true
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_of_mem_insertMany_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp], t.WF → ∀ {l : List α} {k : α}, l.contains k = false → k ∈ t.insertMany l → k ∈ t
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.baseChange_equation : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve.Affine R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  {f : A →ₐ[S] B},
  Function.Injective ⇑f → ∀ (x y : A), (W.baseChange B).Equation (f x) (f y) ↔ (W.baseChange A).Equation x y
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Submodule
HomogeneousSubmodule.mk.inj : ∀ {ιA : Type u_1} {ιM : Type u_2} {σA : Type u_3} {σM : Type u_4} {A : Type u_5} {M : Type u_6} {inst : Semiring A}
  {inst_1 : AddCommMonoid M} {inst_2 : Module A M} {𝒜 : ιA → σA} {ℳ : ιM → σM} {inst_3 : DecidableEq ιA}
  {inst_4 : AddMonoid ιA} {inst_5 : SetLike σA A} {inst_6 : AddSubmonoidClass σA A} {inst_7 : GradedRing 𝒜}
  {inst_8 : DecidableEq ιM} {inst_9 : SetLike σM M} {inst_10 : AddSubmonoidClass σM M}
  {inst_11 : DirectSum.Decomposition ℳ} {inst_12 : VAdd ιA ιM} {inst_13 : SetLike.GradedSMul 𝒜 ℳ}
  {toSubmodule : Submodule A M} {is_homogeneous' : toSubmodule.IsHomogeneous ℳ} {toSubmodule_1 : Submodule A M}
  {is_homogeneous'_1 : toSubmodule_1.IsHomogeneous ℳ},
  { toSubmodule := toSubmodule, is_homogeneous' := is_homogeneous' } =
      { toSubmodule := toSubmodule_1, is_homogeneous' := is_homogeneous'_1 } →
    toSubmodule = toSubmodule_1
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Let `sᵢ`, `tᵢ` and `t'ᵢ` be families of `R`-modules, then `f : Πᵢ sᵢ → tᵢ → t'ᵢ` induces an
element of `Hom(⨂ᵢ sᵢ, Hom(⨂ tᵢ, ⨂ᵢ t'ᵢ))` defined by `⨂ᵢ aᵢ ↦ ⨂ᵢ bᵢ ↦ ⨂ᵢ fᵢ aᵢ bᵢ`.

This is `PiTensorProduct.map` for two arbitrary families of modules.
This is `TensorProduct.map₂` for families of modules.
 -/
PiTensorProduct.map₂ : {ι : Type u_1} →
  {R : Type u_4} →
    [inst : CommSemiring R] →
      {s : ι → Type u_7} →
        [inst_1 : (i : ι) → AddCommMonoid (s i)] →
          [inst_2 : (i : ι) → Module R (s i)] →
            {t : ι → Type u_11} →
              {t' : ι → Type u_12} →
                [inst_3 : (i : ι) → AddCommMonoid (t i)] →
                  [inst_4 : (i : ι) → Module R (t i)] →
                    [inst_5 : (i : ι) → AddCommMonoid (t' i)] →
                      [inst_6 : (i : ι) → Module R (t' i)] →
                        ((i : ι) → s i →ₗ[R] t i →ₗ[R] t' i) →
                          (PiTensorProduct R fun i => s i) →ₗ[R]
                            (PiTensorProduct R fun i => t i) →ₗ[R] PiTensorProduct R fun i => t' i
-- Init.Data.Order.Ord
List.instLawfulBEqCmpCompareLex : ∀ {α : Type u_1} {cmp : α → α → Ordering} [inst : BEq α] [Std.LawfulBEqCmp cmp], Std.LawfulBEqCmp (List.compareLex cmp)
-- Init.Data.Order.Lemmas
Classical.Order.instLT : {α : Type u} → [LE α] → LT α
-- Mathlib.RingTheory.HahnSeries.PowerSeries
HahnSeries.toPowerSeries_symm_apply_coeff : ∀ {R : Type u_2} [inst : Semiring R] (f : PowerSeries R) (n : ℕ),
  (HahnSeries.toPowerSeries.symm f).coeff n = (PowerSeries.coeff n) f
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
/-- The `ConnectedComponent` specialization of `Quot.lift`. Provides the stronger
assumption that the vertices are connected by a path.  -/
SimpleGraph.ConnectedComponent.lift : {V : Type u} →
  {G : SimpleGraph V} →
    {β : Sort u_1} → (f : V → β) → (∀ (v w : V) (p : G.Walk v w), p.IsPath → f v = f w) → G.ConnectedComponent → β
-- Mathlib.CategoryTheory.Equivalence.Symmetry
CategoryTheory.Equivalence.symmEquivInverse_obj_inverse : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (D : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (X : (D ≌ C)ᵒᵖ),
  ((CategoryTheory.Equivalence.symmEquivInverse C D).obj X).inverse = (Opposite.unop X).functor