mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.SyntheticMVars
/-- Collect unassigned metavariables at `e` that have associated tactic blocks, and then execute them using `runTactic`.
We use this method at the `match .. with` elaborator when it cannot be postponed anymore, but it is still waiting
the result of a tactic block.
 -/
Lean.Elab.Term.runPendingTacticsAt : Lean.Expr → Lean.Elab.TermElabM Unit
-- Mathlib.Topology.UniformSpace.Closeds
hausdorffEntourage_comp : ∀ {α : Type u_1} (U V : SetRel α α), hausdorffEntourage (U.comp V) = (hausdorffEntourage U).comp (hausdorffEntourage V)
-- Mathlib.FieldTheory.Fixed
/-- Bijection between `G` and algebra endomorphisms of `F` that fix the fixed points.  -/
FixedPoints.toAlgHomEquiv : (G : Type u_2) →
  (F : Type u_3) →
    [inst : Group G] →
      [inst_1 : Field F] →
        [inst_2 : MulSemiringAction G F] → [Finite G] → [FaithfulSMul G F] → G ≃ (F →ₐ[↥(FixedPoints.subfield G F)] F)
-- Mathlib.Analysis.Fourier.AddCircle
/-- The family of monomials `fourier n`, parametrized by `n : ℤ` and considered as
elements of the `Lp` space of functions `AddCircle T → ℂ`.  -/
fourierLp : {T : ℝ} → [hT : Fact (0 < T)] → (p : ENNReal) → [Fact (1 ≤ p)] → ℤ → ↥(MeasureTheory.Lp ℂ p AddCircle.haarAddCircle)
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors_toPrefunctor_obj : ∀ {B : Type u₁} [inst : Quiver B] [inst_1 : (a b : B) → Quiver (a ⟶ b)] {C : Type u₂} [inst_2 : Quiver C]
  [inst_3 : (a b : C) → Quiver (a ⟶ b)] (F : B → C) (F' : (a b : B) → (a ⟶ b) ⥤q (F a ⟶ F b)) (a : B),
  (CategoryTheory.PrelaxFunctorStruct.mkOfHomPrefunctors F F').obj a = F a
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedSimplicialObject_unitIso_inv_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X : CategoryTheory.Functor (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ C)
  (X_1 : (CategoryTheory.WithInitial SimplexCategory)ᵒᵖ),
  (AugmentedSimplexCategory.equivAugmentedSimplicialObject.unitIso.inv.app X).app X_1 =
    CategoryTheory.CategoryStruct.comp
      (match
          match Opposite.unop X_1 with
          | CategoryTheory.WithInitial.of x => CategoryTheory.WithTerminal.of (Opposite.op x)
          | CategoryTheory.WithInitial.star => CategoryTheory.WithTerminal.star with
        | CategoryTheory.WithTerminal.of x =>
          (CategoryTheory.Iso.refl
                (CategoryTheory.WithTerminal.incl.comp
                  ((CategoryTheory.WithInitial.opEquiv SimplexCategory).inverse.comp X))).app
            x
        | CategoryTheory.WithTerminal.star =>
          CategoryTheory.Iso.refl (X.obj (Opposite.op CategoryTheory.WithInitial.star))).inv
      (X.map
        (match Opposite.unop X_1 with
          | CategoryTheory.WithInitial.of x => CategoryTheory.Iso.refl (Opposite.op (CategoryTheory.WithInitial.of x))
          | CategoryTheory.WithInitial.star =>
            CategoryTheory.Iso.refl (Opposite.op CategoryTheory.WithInitial.star)).inv)
-- Mathlib.Algebra.Group.Hom.Instances
OneHom.instZPow : {M : Type uM} → {N : Type uN} → [inst : One M] → [inst_1 : Group N] → Pow (OneHom M N) ℤ
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.ValueGroup₀.embedding_inj : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : GroupWithZero B] {f : A →*₀ B}
  {a b : f.ValueGroup₀}, MonoidWithZeroHom.ValueGroup₀.embedding a = MonoidWithZeroHom.ValueGroup₀.embedding b ↔ a = b
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Set.Finite.toFinset_smul_set : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {a : α} {s : Set β} (hs : s.Finite)
  (hf : optParam (a • s).Finite ⋯), hf.toFinset = a • hs.toFinset
-- Std.Internal.Do.Triple.Basic
Std.Internal.Do.Triple.bind : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Monad m] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred]
  {α β : Type u} {pre : Pred} {epost : EPred} {post : β → Pred} (x : m α) (f : α → m β) (mid : α → Pred),
  ⦃ pre ⦄ x ⦃ mid; epost ⦄ → (∀ (a : α), ⦃ mid a ⦄ f a ⦃ post; epost ⦄) → ⦃ pre ⦄ x >>= f ⦃ post; epost ⦄
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.attachCodeDecls : {pu : Lean.Compiler.LCNF.Purity} →
  Array (Lean.Compiler.LCNF.CodeDecl pu) → Lean.Compiler.LCNF.Code pu → Lean.Compiler.LCNF.Code pu
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.mono : ∀ {G : Type u_1} [inst : AddGroup G] {A : Set G} {K L : ℝ},
  K ≤ L → IsApproximateAddSubgroup K A → IsApproximateAddSubgroup L A
-- Mathlib.Topology.Compactness.CompactlyGeneratedSpace
instUCompactlyGeneratedSpaceOfDiscreteTopology : ∀ (X : Type v) [t : TopologicalSpace X] [DiscreteTopology X], UCompactlyGeneratedSpace X
-- Mathlib.Algebra.Algebra.RestrictScalars
RestrictScalars.isCentralScalar : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : Semiring S] [inst_1 : AddCommMonoid M] [inst_2 : CommSemiring R]
  [inst_3 : Algebra R S] [inst_4 : Module S M] [inst_5 : Module Sᵐᵒᵖ M] [IsCentralScalar S M],
  IsCentralScalar R (RestrictScalars R S M)
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
quasispectrumRestricts_iff : ∀ {R : Type u_3} {S : Type u_4} {A : Type u_5} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : NonUnitalRing A] [inst_3 : Module R A] [inst_4 : Module S A] [inst_5 : Algebra R S] (a : A) (f : S → R),
  QuasispectrumRestricts a f ↔
    Set.RightInvOn f (⇑(algebraMap R S)) (quasispectrum S a) ∧ Function.LeftInverse f ⇑(algebraMap R S)
-- Init.Data.List.Nat.Sublist
List.suffix_iff_eq_append : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+ l₂ ↔ List.take (l₂.length - l₁.length) l₂ ++ l₁ = l₂
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.hom_inv_id_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (e : f ≅ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right e.hom) (CategoryTheory.Arrow.Hom.right e.inv) =
    CategoryTheory.CategoryStruct.id f.right
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv_eq : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f f' : 𝕜 → F}, (∀ (x : 𝕜), HasDerivAt f (f' x) x) → deriv f = f'
-- Mathlib.LinearAlgebra.Dimension.Basic
LinearMap.rank_le_of_injective : ∀ {R : Type u} {M M₁ : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (f : M →ₗ[R] M₁),
  Function.Injective ⇑f → Module.rank R M ≤ Module.rank R M₁
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.maxEntryD.match_1.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → (a : α) × β a → Sort u_3) (size : ℕ)
  (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (x : (a : α) × β a)
  (h_1 : (fallback : (a : α) × β a) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (x : (a : α) × β a) →
              motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      (fallback : (a : α) × β a) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback) =
    h_2 size k v l x
-- Mathlib.CategoryTheory.MorphismProperty.Quotient
/-- The property of morphisms that is induced by `W : MorphismProperty C`
on the quotient category by `homRel : HomRel C` when `W.HasQuotient homRel` holds.  -/
CategoryTheory.MorphismProperty.quotient : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (W : CategoryTheory.MorphismProperty C) →
      (homRel : HomRel C) →
        [inst_1 : CategoryTheory.HomRel.IsStableUnderPrecomp homRel] →
          [inst_2 : CategoryTheory.HomRel.IsStableUnderPostcomp homRel] →
            [W.HasQuotient homRel] → CategoryTheory.MorphismProperty (CategoryTheory.Quotient homRel)
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.d₁₀_comp_coinvariantsMk_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : G →₀ ↑A),
  (Representation.Coinvariants.mk A.ρ) ((CategoryTheory.ConcreteCategory.hom (groupHomology.d₁₀ A)) x) = 0 x
-- Mathlib.Geometry.Manifold.Algebra.Monoid
smoothRightMul_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) {G' : Type u_8}
  [inst_4 : Monoid G'] [inst_5 : TopologicalSpace G'] [inst_6 : ChartedSpace H G'] [inst_7 : ContMDiffMul I (↑⊤) G']
  (g' : G'), (smoothRightMul I g') 1 = g'
-- Mathlib.Data.ENNReal.Inv
ENNReal.mulRightOrderIso_toEquiv : ∀ (a : ENNReal) (ha : IsUnit a), (a.mulRightOrderIso ha).toEquiv = ha.unit.mulRight
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.topIso_inv : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens), U.topIso.inv = X.presheaf.map (CategoryTheory.eqToHom ⋯).op
-- Mathlib.Algebra.Regular.Defs
/-- A right-regular element is an element `c` such that multiplication on the right by `c`
is injective.  -/
IsRightRegular : {R : Type u_1} → [Mul R] → R → Prop
-- Init.Data.SInt.Bitwise
Int32.toBitVec_shiftLeft : ∀ (a b : Int32), (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod 32
-- Mathlib.Data.ZMod.Basic
ZMod.natAbs_min_of_le_div_two : ∀ (n : ℕ) (x y : ℤ), ↑x = ↑y → x.natAbs ≤ n / 2 → x.natAbs ≤ y.natAbs
-- Mathlib.Data.Matrix.Diagonal
Matrix.transpose_one : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α], Matrix.transpose 1 = 1
-- Mathlib.Data.Rel.Cover
SetRel.IsCover.empty : ∀ {X : Type u_1} {U : SetRel X X} {N : Set X}, U.IsCover ∅ N
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.Hom.mk.sizeOf_spec : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat} {X Y : F.CoGrothendieck}
  [inst_1 : SizeOf 𝒮] (base : X.base ⟶ Y.base) (fiber : X.fiber ⟶ (F.map base.op.toLoc).toFunctor.obj Y.fiber),
  sizeOf { base := base, fiber := fiber } = 1 + sizeOf base + sizeOf fiber
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.span_union : ∀ (R : Type u) (L : Type v) {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (s t : Set M),
  LieSubmodule.lieSpan R L (s ∪ t) = LieSubmodule.lieSpan R L s ⊔ LieSubmodule.lieSpan R L t
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_le_inf : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G) [H₁.Normal] [H₂.Normal], ⁅H₁, H₂⁆ ≤ H₁ ⊓ H₂
-- Lean.Meta.MatchUtil
/-- Return `some (α, lhs, rhs)` if `e` is of the form `@Eq α lhs rhs` or `@HEq α lhs α rhs`
 -/
Lean.Meta.matchEqHEq? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr × Lean.Expr))
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.fst_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α (β × γ)) (a : α),
  κ.fst a = MeasureTheory.Measure.map Prod.fst (κ a)
-- Mathlib.CategoryTheory.Monad.Equalizer
/-- The Beck fork is an equalizer.  -/
CategoryTheory.Comonad.beckEqualizer : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Comonad C} →
      (X : T.Coalgebra) → CategoryTheory.Limits.IsLimit (CategoryTheory.Comonad.beckFork X)
-- Lean.Server.FileWorker.SemanticHighlighting
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.HandleOverlapState.mk : Array Lean.Server.FileWorker.AbsoluteLspSemanticToken →
  Option Lean.Server.FileWorker.AbsoluteLspSemanticToken →
    List Lean.Server.FileWorker.AbsoluteLspSemanticToken → Lean.Server.FileWorker.HandleOverlapState✝
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_coe_ne_top_iff_summable : ∀ {β : Type u_2} {f : β → NNReal}, ∑' (b : β), ↑(f b) ≠ ⊤ ↔ Summable f
-- Mathlib.Order.ModularLattice
eq_of_le_of_inf_le_of_sup_le : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {x y z : α}, x ≤ y → y ⊓ z ≤ x ⊓ z → y ⊔ z ≤ x ⊔ z → x = y
-- Mathlib.LinearAlgebra.Matrix.WithConv
instNonUnitalSemiringWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [NonUnitalSemiring α] → NonUnitalSemiring (WithConv (Matrix m n α))
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- A `Multiset ℕ` induces a partition on its sum.  -/
Nat.Partition.ofMultiset : (l : Multiset ℕ) → l.sum.Partition
-- Init.Prelude
Or.resolve_right : ∀ {a b : Prop}, a ∨ b → ¬b → a
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.typeEquiv_unitIso_inv_app_hom_apply : ∀ (X : Type u) (f : PUnit.{u + 1} ⟶ X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.typeEquiv.unitIso.inv.app X)) f = (TypeCat.Hom.hom f) PUnit.unit
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.quot_out_zero : ∀ {M : Type u_1} [inst : MonoidWithZero M], Quot.out 0 = 0
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.tsum_mul_left : ∀ {α : Type u_2} {L : SummationFilter α} (a : NNReal) (f : α → NNReal), ∑'[L] (x : α), a * f x = a * ∑'[L] (x : α), f x
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.ofRestrict_invApp_apply : ∀ (X : AlgebraicGeometry.LocallyRingedSpace) {Y : TopCat} {f : Y ⟶ TopCat.of ↑↑X.toPresheafedSpace}
  (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f))
  (U : TopologicalSpace.Opens ↑↑(X.restrict h).toPresheafedSpace) (x : ↑((X.restrict h).presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp (X.ofRestrict h) U))
      x =
    (CategoryTheory.ConcreteCategory.hom
        (CategoryTheory.CategoryStruct.id ((X.restrict h).presheaf.obj (Opposite.op U))))
      x
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- Restricting to `S₁` then mapping to a larger `S₂` is the same as restricting to `S₂`.  -/
Affine.Simplex.restrict_map_inclusion : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} (s : Affine.Simplex k P n) (S₁ S₂ : AffineSubspace k P)
  (hS₁ : affineSpan k (Set.range s.points) ≤ S₁) (hS₂ : S₁ ≤ S₂),
  (s.restrict S₁ hS₁).map (AffineSubspace.inclusion hS₂) ⋯ = s.restrict S₂ ⋯
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
AlgebraicGeometry.Scheme.quasiCompactCover_iff : ∀ (S : AlgebraicGeometry.Scheme) (𝒰 : CategoryTheory.PreZeroHypercover S),
  S.quasiCompactCover 𝒰 ↔ AlgebraicGeometry.QuasiCompactCover 𝒰
-- Mathlib.Order.UpperLower.Closure
lowerClosure_eq_top_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [NoMaxOrder α] {s : Set α}, lowerClosure s = ⊤ ↔ ¬BddAbove s
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_beq : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {k : α} (h' : k ∈ m), (m.get k h' == k) = true
-- Mathlib.Combinatorics.Additive.ETransform
Finset.mulETransformLeft_fst : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Group α] (e : α) (x : Finset α × Finset α),
  (Finset.mulETransformLeft e x).1 = x.1 ∩ MulOpposite.op e • x.1
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_swap_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V W : (x : M) → TangentSpace I x},
  VectorField.mlieBracketWithin I V W s x = -VectorField.mlieBracketWithin I W V s x
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- Heterobasic version of `TensorProduct.dualDistrib`  -/
TensorProduct.AlgebraTensorModule.dualDistrib : (R : Type u_1) →
  (A : Type u_2) →
    (M : Type u_3) →
      (N : Type u_4) →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : Algebra R A] →
              [inst_3 : AddCommMonoid M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R M] →
                    [inst_6 : Module A M] →
                      [inst_7 : Module R N] →
                        [inst_8 : IsScalarTower R A M] →
                          TensorProduct R (Module.Dual A M) (Module.Dual R N) →ₗ[A] Module.Dual A (TensorProduct R M N)
-- Mathlib.Data.Fin.VecNotation
/-- Unexpander for the `![x, y, ...]` notation.  -/
Matrix.vecConsUnexpander : Lean.PrettyPrinter.Unexpander
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- The cocone at a point of the whiskering right by `G` of an extension is isomorphic to the
action of `G` on the cocone at that point for the original extension.  -/
CategoryTheory.Functor.LeftExtension.coconeAtWhiskerRightIso : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      {D : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} A] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} B] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} D] →
                (G : CategoryTheory.Functor B D) →
                  (F : CategoryTheory.Functor A B) →
                    (L : CategoryTheory.Functor A C) →
                      (E : L.LeftExtension F) →
                        (c : C) →
                          ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj E).coconeAt c ≅
                            G.mapCocone (E.coconeAt c)
-- Mathlib.Analysis.Meromorphic.Basic
/-- Finsums of meromorphic functions are meromorphic.  -/
MeromorphicOn.finsum : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {U : Set 𝕜} {ι : Type u_5} {f : ι → 𝕜 → 𝕜'},
  (∀ (σ : ι), MeromorphicOn (f σ) U) → MeromorphicOn (∑ᶠ (n : ι), f n) U
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instCommRing : {α : Type u} →
  [inst : TopologicalSpace α] →
    {R : Type u_1} → [inst_1 : SeminormedCommRing R] → CommRing (BoundedContinuousFunction α R)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Submonoid.LocalizationMap.ofMulEquivOfLocalizations.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) (k : N ≃* P),
  f.ofMulEquivOfLocalizations k = (k.toMonoidHom.comp f.toMonoidHom).toLocalizationMap ⋯ ⋯ ⋯
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.instIsAffineXSchemeCoverOfIsIsoIsOpenImmersionId : ∀ {X : AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsAffine X]
  (i : (AlgebraicGeometry.Scheme.coverOfIsIso (CategoryTheory.CategoryStruct.id X)).I₀),
  AlgebraicGeometry.IsAffine ((AlgebraicGeometry.Scheme.coverOfIsIso (CategoryTheory.CategoryStruct.id X)).X i)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.IterM.toArray_eq_match_step.match_1.eq_3 : ∀ {α β : Type u_1} {m : Type u_1 → Type u_2} (motive : Std.IterStep (Std.IterM m β) β → Sort u_3)
  (h_1 : (it' : Std.IterM m β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.IterM m β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.done with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_3 ()
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- **Alias** of the reverse direction of `ValuativeRel.mul_vlt_mul_iff_right`. -/
ValuativeRel.mul_vlt_mul_right : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x y z : R}, 0 <ᵥ x → y <ᵥ z → x * y <ᵥ x * z
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
div_le_div_right' : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [MulRightMono α] {a b : α}, a ≤ b → ∀ (c : α), a / c ≤ b / c
-- Mathlib.Algebra.GradedMonoid
/-- The submonoid `A 0` of `R`.  -/
SetLike.GradeZero.submonoid : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      [inst : SetLike S R] →
        [inst_1 : Monoid R] → [inst_2 : AddMonoid ι] → (A : ι → S) → [SetLike.GradedMonoid A] → Submonoid R
-- Mathlib.Data.Finset.Image
Finset.filter_map : ∀ {α : Type u_1} {β : Type u_2} {f : α ↪ β} {s : Finset α} {p : β → Prop} [inst : DecidablePred p],
  Finset.filter p (Finset.map f s) = Finset.map f (Finset.filter (p ∘ ⇑f) s)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.toGraphSubmatrixEmbedding_apply : ∀ {α : Type u_1} {V : Type u_2} {W : Type u_3} (A : Matrix V V α) [inst : MulZeroOneClass α] [inst_1 : Nontrivial α]
  (h : A.IsAdjMatrix) (f : W → V) (v : W), (Matrix.IsAdjMatrix.toGraphSubmatrixHom A h f) v = f v
-- Mathlib.Topology.UniformSpace.Basic
isOpen_iff_isOpen_ball_subset : ∀ {α : Type ua} [inst : UniformSpace α] {s : Set α},
  IsOpen s ↔ ∀ x ∈ s, ∃ V ∈ uniformity α, IsOpen V ∧ UniformSpace.ball x V ⊆ s
-- Mathlib.Algebra.Category.Ring.Basic
/-- Ring equivalences are isomorphisms in category of commutative semirings  -/
RingEquiv.toCommSemiRingCatIso : {R S : Type u} →
  [inst : CommSemiring R] → [inst_1 : CommSemiring S] → R ≃+* S → (CommSemiRingCat.of R ≅ CommSemiRingCat.of S)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.mem_alter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β},
  k' ∈ m.alter k f ↔ if (k == k') = true then (f m[k]?).isSome = true else k' ∈ m
-- Mathlib.Tactic.Push
_private.Mathlib.Tactic.Push.0.Mathlib.Tactic.Push.elabPushConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Mathlib.Tactic.Push.Config
-- Mathlib.Topology.Order.MonotoneContinuity
/-- If a function `f` with a densely ordered codomain is strictly monotone on a right neighborhood
of `a` and the closure of the image of this neighborhood under `f` is a right neighborhood of `f a`,
then `f` is continuous at `a` from the right.  -/
StrictMonoOn.continuousWithinAt_right_of_closure_image_mem_nhdsWithin : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [OrderTopology α]
  [inst_3 : LinearOrder β] [inst_4 : TopologicalSpace β] [OrderTopology β] [DenselyOrdered β] {f : α → β} {s : Set α}
  {a : α},
  StrictMonoOn f s →
    s ∈ nhdsWithin a (Set.Ici a) →
      closure (f '' s) ∈ nhdsWithin (f a) (Set.Ici (f a)) → ContinuousWithinAt f (Set.Ici a) a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Pred
String.endsWith_prop_eq_getLast? : ∀ {P : Char → Prop} [inst : DecidablePred P] {s : String},
  s.endsWith P = Option.any (fun x => decide (P x)) s.toList.getLast?
-- Init.Data.SInt.Lemmas
Int16.toInt_ofNat' : ∀ {n : ℕ}, (Int16.ofNat n).toInt = (↑n).bmod Int16.size
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.instIsStableUnderBaseChangeProetalePrecoverage : AlgebraicGeometry.Scheme.proetalePrecoverage.IsStableUnderBaseChange
-- Mathlib.Order.PartialSups
partialSups_zero : ∀ {α : Type u_1} [inst : SemilatticeSup α] (f : ℕ → α), (partialSups f) 0 = f 0