mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
BoundedVariationOn.stieltjesFunctionRightLim_apply : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : OrderTopology α] {E : Type u_2}
  [inst_3 : NormedAddCommGroup E] [inst_4 : CompleteSpace E] {f : α → E} (hf : BoundedVariationOn f Set.univ)
  (x₀ x : α), ↑(hf.stieltjesFunctionRightLim x₀) x = variationOnFromTo (Function.rightLim f) Set.univ x₀ x
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.forM_eq_forM_toList : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {cmp : α → α → Ordering} {f : α → m PUnit.{u_1 + 1}} [inst : Monad m]
  [LawfulMonad m] {t : RBTree.RBSet α cmp}, RBTree.RBSet.forM f t = t.toList.forM f
-- Mathlib.Computability.RegularExpressions
RegularExpression.rmatch.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α] (x : RegularExpression α), x.rmatch [] = x.matchEpsilon
-- Mathlib.Algebra.CubicDiscriminant
Cubic.degree_of_a_eq_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.toPoly.degree ≤ 2
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.instSliceableRicSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.instSliceableRicSlice._auto_1) →
      Std.Ric.Sliceable (Std.TreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.Const.RicSlice α β)
-- Mathlib.CategoryTheory.Sums.Basic
CategoryTheory.Functor.inlCompSum'_hom_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor A C)
  (G : CategoryTheory.Functor B C) (X : A),
  (F.inlCompSum' G).hom.app X = CategoryTheory.CategoryStruct.id ((F.sum' G).obj (Sum.inl X))
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.localTrivAsPartialEquiv_coe : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι), ↑(Z.localTrivAsPartialEquiv i) = ↑(Z.localTriv i)
-- Lean.DocString.Types
/-- A paragraph.
 -/
Lean.Doc.Block.para : {i : Type u} → {b : Type v} → Array (Lean.Doc.Inline i) → Lean.Doc.Block i b
-- Mathlib.Logic.Function.FiberPartition
Function.Fiber.image_eq_image_mk : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} (f : Y → Z) (g : X → Y) (a : Function.Fiber (f ∘ g)),
  Function.Fiber.image (f ∘ g) a = Function.Fiber.image f (Function.Fiber.mk f (g (Function.Fiber.preimage (f ∘ g) a)))
-- Mathlib.Computability.RegularExpressions
_private.Mathlib.Computability.RegularExpressions.0.RegularExpression.matches'.match_1.eq_3 : ∀ {α : Type u_1} (motive : RegularExpression α → Sort u_2) (a : α) (h_1 : Unit → motive RegularExpression.zero)
  (h_2 : Unit → motive RegularExpression.epsilon) (h_3 : (a : α) → motive (RegularExpression.char a))
  (h_4 : (P Q : RegularExpression α) → motive (P.plus Q)) (h_5 : (P Q : RegularExpression α) → motive (P.comp Q))
  (h_6 : (P : RegularExpression α) → motive P.star),
  (match RegularExpression.char a with
    | RegularExpression.zero => h_1 ()
    | RegularExpression.epsilon => h_2 ()
    | RegularExpression.char a => h_3 a
    | P.plus Q => h_4 P Q
    | P.comp Q => h_5 P Q
    | P.star => h_6 P) =
    h_3 a
-- Mathlib.Data.Finsupp.Basic
Finsupp.range_subset_insert_frange : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M), Set.range ⇑f ⊆ insert 0 ↑f.frange
-- Mathlib.Analysis.Calculus.DSlope
dslope_same : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] (f : 𝕜 → E) (a : 𝕜), dslope f a a = deriv f a
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.revSkipWhile_copy : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat]
  [inst_1 : String.Slice.Pattern.Model.PatternModel pat] [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat]
  {s : String.Slice} {pos : s.Pos}, pos.copy.revSkipWhile pat = (pos.revSkipWhile pat).copy
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.Hom.hom_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B}
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (f : X.Hom Y), f.hom.right = f.right
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.isOpen_iff : ∀ (H : Type u) {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (s : Set M), IsOpen s ↔ ∀ (x : M), IsOpen (↑(chartAt H x) '' ((chartAt H x).source ∩ s))
-- Mathlib.Data.Fin.Parity
Fin.odd_of_odd : ∀ {n : ℕ} [inst : NeZero n], Odd n → ∀ (k : Fin n), Odd k
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeListTR.go.match_1.eq_2 : ∀ {α : Type u_1} (motive : List ℕ → List α → Array (List α) → Sort u_2) (n : ℕ) (ns : List ℕ) (xs : List α)
  (acc : Array (List α)) (h_1 : (xs : List α) → (acc : Array (List α)) → motive [] xs acc)
  (h_2 : (n : ℕ) → (ns : List ℕ) → (xs : List α) → (acc : Array (List α)) → motive (n :: ns) xs acc),
  (match n :: ns, xs, acc with
    | [], xs, acc => h_1 xs acc
    | n :: ns, xs, acc => h_2 n ns xs acc) =
    h_2 n ns xs acc
-- Init.Data.List.Nat.Count
List.countP_replace : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α} {l : List α} {p : α → Bool},
  List.countP p (l.replace a b) =
    if l.contains a = true then (List.countP p l + if p b = true then 1 else 0) - if p a = true then 1 else 0
    else List.countP p l
-- Mathlib.CategoryTheory.Category.Basic
/-- The composition of monomorphisms is again a monomorphism. This version takes `Mono f` and
`Mono g` as typeclass arguments. For a version taking them as explicit arguments, see `mono_comp'`.
 -/
CategoryTheory.mono_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (g : Z ⟶ Y) [CategoryTheory.Mono g] (f : Y ⟶ X)
  [CategoryTheory.Mono f], CategoryTheory.Mono (CategoryTheory.CategoryStruct.comp g f)
-- Mathlib.Logic.Function.Iterate
Function.iterate_zero_apply : ∀ {α : Type u} (f : α → α) (x : α), f^[0] x = x
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.map_comp_uliftYonedaEquiv_down : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ℰ : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} ℰ]
  (A : CategoryTheory.Functor C ℰ) (E : ℰ) {X Y : C} (f : X ⟶ Y)
  (g : CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.obj Y ⟶ (CategoryTheory.Presheaf.restrictedULiftYoneda A).obj E),
  CategoryTheory.CategoryStruct.comp (A.map f) (CategoryTheory.uliftYonedaEquiv g).down =
    (CategoryTheory.uliftYonedaEquiv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYoneda.{max v₂ w, v₁, u₁}.map f) g)).down
-- Mathlib.Algebra.MvPolynomial.Basic
/-- The multivariate polynomial ring over an integral domain is an integral domain.  -/
MvPolynomial.instIsDomainOfIsCancelAdd : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [IsCancelAdd R] [IsDomain R], IsDomain (MvPolynomial σ R)
-- Mathlib.CategoryTheory.Skeletal
/-- Use `Quotient.out` to create a functor out of the thin skeleton.  -/
CategoryTheory.ThinSkeleton.fromThinSkeleton : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [Quiver.IsThin C] → CategoryTheory.Functor (CategoryTheory.ThinSkeleton C) C
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.toSubgroup_one : ∀ {G : Type u_1} [inst : Group G] (A B : Subgroup G), HNNExtension.toSubgroup A B 1 = A
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_X : ∀ {R : Type u} [inst : Semiring R] {x : R}, Polynomial.eval x Polynomial.X = x
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.le_graph_iff : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {f g : E →ₗ.[R] F}, f.graph ≤ g.graph ↔ f ≤ g
-- Mathlib.Topology.Sets.BaseChangeNhds
TopologicalSpace.Opens.baseChangeCompactsInside_comp : ∀ {α : Type u_1} [inst : TopologicalSpace α] {U V W : TopologicalSpace.Opens α} (h : U ⟶ V) (k : V ⟶ W)
  (K : ↑U.compactsInside),
  TopologicalSpace.Opens.baseChangeCompactsInside (CategoryTheory.CategoryStruct.comp h k) K =
    TopologicalSpace.Opens.baseChangeCompactsInside k (TopologicalSpace.Opens.baseChangeCompactsInside h K)
-- Mathlib.Probability.Moments.SubGaussian
ProbabilityTheory.HasSubgaussianMGF.integrable : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {X : Ω → ℝ} {c : NNReal},
  ProbabilityTheory.HasSubgaussianMGF X c μ → MeasureTheory.Integrable X μ
-- Mathlib.NumberTheory.ModularForms.QExpansion
UpperHalfPlane.IsZeroAtImInfty.valueAtInfty_eq_zero : ∀ {f : UpperHalfPlane → ℂ}, UpperHalfPlane.IsZeroAtImInfty f → UpperHalfPlane.valueAtInfty f = 0
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult : Type
-- Mathlib.Order.Heyting.Basic
ne_hnot_self : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a : α} [Nontrivial α], a ≠ ￢a
-- Mathlib.LinearAlgebra.TensorProduct.Defs
TensorProduct.Eqv.of_zero_left : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_7} {N : Type u_8} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (n : N),
  TensorProduct.Eqv R M N (FreeAddMonoid.of (0, n)) 0
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.HeapNode.rankTR_eq.go : ∀ {α : Type u_1} (s : Batteries.BinomialHeap.Imp.HeapNode α) (n : ℕ),
  Batteries.BinomialHeap.Imp.HeapNode.rankTR.go s n = s.rank + n
-- Mathlib.LinearAlgebra.Projectivization.Basic
Projectivization.mk.congr_simp : ∀ (K : Type u_1) {V : Type u_2} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (v v_1 : V)
  (e_v : v = v_1) (hv : v ≠ 0), Projectivization.mk K v hv = Projectivization.mk K v_1 ⋯
-- Mathlib.Order.RelSeries
RelSeries.toList_append : ∀ {α : Type u_1} {r : SetRel α α} (p q : RelSeries r) (connect : (p.last, q.head) ∈ r),
  (p.append q connect).toList = p.toList ++ q.toList
-- Init.Data.UInt.Lemmas
Nat.toUInt16_eq : ∀ {n : ℕ}, n.toUInt16 = UInt16.ofNat n
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_bot : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] (f : α → E) (g : α → F), f =o[⊥] g
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instSMul : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] →
            [inst_2 : Module R V] →
              [inst_3 : TopologicalSpace P] →
                [inst_4 : AddTorsor V P] →
                  [inst_5 : AddCommGroup W] →
                    [inst_6 : Module R W] →
                      {S : Type u_10} →
                        [inst_7 : TopologicalSpace W] →
                          [inst_8 : Monoid S] →
                            [inst_9 : DistribMulAction S W] →
                              [SMulCommClass R S W] → [ContinuousConstSMul S W] → SMul S (P →ᴬ[R] W)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Further truncation of truncated cosimplicial objects.  -/
CategoryTheory.CosimplicialObject.Truncated.trunc : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    (n m : ℕ) →
      autoParam (m ≤ n) CategoryTheory.CosimplicialObject.Truncated.trunc._auto_1 →
        CategoryTheory.Functor (CategoryTheory.CosimplicialObject.Truncated C n)
          (CategoryTheory.CosimplicialObject.Truncated C m)
-- Mathlib.Data.Seq.Computation
Computation.instBind : Bind Computation
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Coalgebra.Repr.tmul_index : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {ι : Type u_4} {κ : Type u_5} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Bialgebra R A] [inst_3 : Semiring B] [inst_4 : Bialgebra R B] {a : A} {b : B}
  (ℛa : Coalgebra.Repr R a ι) (ℛb : Coalgebra.Repr R b κ), (ℛa.tmul ℛb).index = ℛa.index ×ˢ ℛb.index
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.stalkSpecializes_stalkFunctor_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  {F G : TopCat.Presheaf C X} (f : F ⟶ G) {x y : ↑X} (h : x ⤳ y),
  CategoryTheory.CategoryStruct.comp (F.stalkSpecializes h) ((TopCat.Presheaf.stalkFunctor C x).map f) =
    CategoryTheory.CategoryStruct.comp ((TopCat.Presheaf.stalkFunctor C y).map f) (G.stalkSpecializes h)
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.toMatrix'.eq_1 : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Type u_4} {n : Type u_5} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  LinearMap.toMatrix' =
    { toFun := fun f => Matrix.of fun i j => f (Pi.single j 1) i, map_add' := ⋯, map_smul' := ⋯,
      invFun := Matrix.mulVecLin, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.mapWhiskerLeft_leftUnitor_hom : ∀ (A : Type u_1) {B : Type u_2} {C : Type u_3} [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]
  (F : CategoryTheory.Functor B C),
  CategoryTheory.Join.mapWhiskerLeft (CategoryTheory.Functor.id A) F.leftUnitor.hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Join.mapCompRight A (CategoryTheory.Functor.id B) F).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Functor.whiskerRight CategoryTheory.Join.mapPairId.hom
          (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) F))
        (CategoryTheory.Join.mapPair (CategoryTheory.Functor.id A) F).leftUnitor.hom)
-- Init.Data.Array.Lemmas
Array.getElem_swapIfInBounds_left : ∀ {α : Type u_1} {xs : Array α} {i j : ℕ} (hj : j < xs.size) (hi : i < (xs.swapIfInBounds i j).size),
  (xs.swapIfInBounds i j)[i] = xs[j]
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.bernoulli_one : Polynomial.bernoulli 1 = Polynomial.X - Polynomial.C 2⁻¹
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsBigO.exists_nonneg : ∀ {α : Type u_1} {E : Type u_3} {F' : Type u_7} [inst : Norm E] [inst_1 : SeminormedAddCommGroup F'] {f : α → E}
  {g' : α → F'} {l : Filter α}, f =O[l] g' → ∃ c ≥ 0, Asymptotics.IsBigOWith c l f g'
-- Mathlib.Data.Real.Basic
Real.instCommSemiring : CommSemiring ℝ
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `0` and `+` is an additive commutative group, if it
admits an injective map that preserves `0` and `+` to an additive commutative group.  -/
Function.Injective.addCommGroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Add M₁] →
      [inst_1 : Zero M₁] →
        [inst_2 : SMul ℕ M₁] →
          [inst_3 : Neg M₁] →
            [inst_4 : Sub M₁] →
              [inst_5 : SMul ℤ M₁] →
                [inst_6 : AddCommGroup M₂] →
                  (f : M₁ → M₂) →
                    Function.Injective f →
                      f 0 = 0 →
                        (∀ (x y : M₁), f (x + y) = f x + f y) →
                          (∀ (x : M₁), f (-x) = -f x) →
                            (∀ (x y : M₁), f (x - y) = f x - f y) →
                              (∀ (x : M₁) (n : ℕ), f (n • x) = n • f x) →
                                (∀ (x : M₁) (n : ℤ), f (n • x) = n • f x) → AddCommGroup M₁
-- Lean.Elab.MutualDef
/-- `DefView` plus header elaboration data and snapshot.  -/
Lean.Elab.DefViewElabHeader : Type
-- Mathlib.AlgebraicGeometry.EllipticCurve.Reduction
/-- A minimal Weierstrass equation has split multiplicative reduction if and only if
the polynomial `c₄ T ^ 2 + a₁ c₄ T - (54 b₆ - 3 b₂ b₄ + a₂ c₄)` splits in the residue field.

To see how this expression arises, note that the node `(x₀, y₀)` has second order Taylor expansion
`(Y - y₀)^2 + a_1(X - x₀)(Y - y₀) - (3x₀ + a_2)(X - x₀)^2` where `x₀ = (18 b₆ - b₂ b₄) / c₄`.  -/
WeierstrassCurve.HasSplitMultiplicativeReduction : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsDomain R] →
      [IsDiscreteValuationRing R] →
        {K : Type u_2} → [inst_3 : Field K] → [inst_4 : Algebra R K] → [IsFractionRing R K] → WeierstrassCurve K → Prop
-- Std.Internal.Parsec.ByteArray
/-- Parses while a predicate is satisfied, consuming at most `limit` bytes.
Unlike `takeWhileUpTo`, succeeds even if input ends before the predicate stops holding.
 -/
Std.Internal.Parsec.ByteArray.takeWhileAtMost : (UInt8 → Bool) → ℕ → Std.Internal.Parsec.ByteArray.Parser ByteSlice
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKeyD_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a fallback : α}
  {v : β k},
  Std.Internal.List.getKeyD a (Std.Internal.List.insertEntryIfNew k v l) fallback =
    if (k == a) = true ∧ Std.Internal.List.containsKey k l = false then k else Std.Internal.List.getKeyD a l fallback
-- Lean.Meta.CtorRecognizer
/-- If `e` is a constructor application,
then return the corresponding `ConstructorVal`.
 -/
Lean.Meta.isConstructorAppCore? : Lean.Expr → Lean.MetaM (Option Lean.ConstructorVal)
-- Mathlib.RingTheory.LinearDisjoint
/-- If `A` and `B` are linearly disjoint subalgebras in a commutative algebra `S` over `R`
such that `A ⊔ B = S`, then this is the natural isomorphism
`A ⊗[R] B ≃ₐ[A] S` induced by multiplication in `S`.
 -/
Subalgebra.LinearDisjoint.mulMapLeftOfSupEqTop : {R : Type u} →
  {S : Type v} →
    [inst : CommSemiring R] →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {A B : Subalgebra R S} → A.LinearDisjoint B → A ⊔ B = ⊤ → TensorProduct R ↥A ↥B ≃ₐ[↥A] S
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- The map from `Matrix n n R` to bilinear maps on `n → R`.

This is an auxiliary definition for the equivalence `Matrix.toLinearMap₂'`.  -/
Matrix.toLinearMap₂'Aux : {R₁ : Type u_2} →
  {S₁ : Type u_3} →
    {R₂ : Type u_4} →
      {S₂ : Type u_5} →
        {N₂ : Type u_10} →
          {n : Type u_11} →
            {m : Type u_12} →
              [inst : Semiring R₁] →
                [inst_1 : Semiring S₁] →
                  [inst_2 : Semiring R₂] →
                    [inst_3 : Semiring S₂] →
                      [inst_4 : AddCommMonoid N₂] →
                        [inst_5 : Module S₁ N₂] →
                          [inst_6 : Module S₂ N₂] →
                            [inst_7 : SMulCommClass S₂ S₁ N₂] →
                              [Fintype n] →
                                [Fintype m] →
                                  (σ₁ : R₁ →+* S₁) →
                                    (σ₂ : R₂ →+* S₂) → Matrix n m N₂ → (n → R₁) →ₛₗ[σ₁] (m → R₂) →ₛₗ[σ₂] N₂
-- Mathlib.Data.Set.Image
Set.image_compl_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set α}, Function.Injective f → f '' sᶜ ⊆ (f '' s)ᶜ
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instTop : {G : Type u_1} → [inst : Group G] → [inst_1 : TopologicalSpace G] → Top (OpenSubgroup G)
-- Mathlib.Algebra.Category.MonCat.Yoneda
AddCommMonCat.coyoneda_obj_obj_coe : ∀ (M : AddCommMonCatᵒᵖ) (N : AddCommMonCat), ↑((AddCommMonCat.coyoneda.obj M).obj N) = (↑(Opposite.unop M) →+ ↑N)
-- Mathlib.Order.Nucleus
/-- See `Nucleus.giRestrict` for the public-facing version.  -/
_private.Mathlib.Order.Nucleus.0.Nucleus.giAux : {X : Type u_1} → [inst : Order.Frame X] → (n : Nucleus X) → GaloisInsertion (Set.rangeFactorization ⇑n) Subtype.val
-- Mathlib.Data.Nat.Choose.Sum
Nat.choose_middle_le_pow : ∀ (n : ℕ), (2 * n + 1).choose n ≤ 4 ^ n
-- Mathlib.LinearAlgebra.Finsupp.Pi
FunOnFinite.map.congr_simp : ∀ {M : Type u_5} [inst : AddCommMonoid M] {X : Type u_6} {Y : Type u_7} [inst_1 : Finite X] [inst_2 : Finite Y]
  (f f_1 : X → Y),
  f = f_1 → ∀ (s s_1 : X → M), s = s_1 → ∀ (a a_1 : Y), a = a_1 → FunOnFinite.map f s a = FunOnFinite.map f_1 s_1 a_1
-- Mathlib.CategoryTheory.Abelian.Opposite
/-- The kernel of `f.op` is the opposite of `cokernel f`.  -/
CategoryTheory.kernelOpUnop : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {X Y : C} → (f : X ⟶ Y) → Opposite.unop (CategoryTheory.Limits.kernel f.op) ≅ CategoryTheory.Limits.cokernel f
-- Mathlib.Data.QPF.Univariate.Basic
/-- does `abs` preserve `Liftp`?  -/
QPF.LiftpPreservation : {F : Type u → Type u} → [q : QPF F] → Prop
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.ForwardPattern.skipPrefixOfNonempty?.congr_simp : ∀ {ρ : Type} (pat : ρ) [self : String.Slice.Pattern.ForwardPattern pat] (s : String.Slice) (h : s.isEmpty = false),
  String.Slice.Pattern.ForwardPattern.skipPrefixOfNonempty? pat s h =
    String.Slice.Pattern.ForwardPattern.skipPrefixOfNonempty? pat s h
-- Lean.Meta.Sym.Eta
/-- Returns `true` if `e` can be eta-reduced. Uses pointer equality for efficiency.  -/
Lean.Meta.Sym.isEtaReducible : Lean.Expr → Bool
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
instIsIntegralQuotientIdeal : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {I : Ideal A}
  [Algebra.IsIntegral R A], Algebra.IsIntegral R (A ⧸ I)
-- Mathlib.Algebra.Group.Indicator
/-- `Set.mulIndicator` as a `monoidHom`.  -/
Set.mulIndicatorHom : {α : Type u_6} → (M : Type u_7) → [inst : MulOneClass M] → Set α → (α → M) →* α → M
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
cfcₙ_comp_im : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [inst_6 : StarModule ℂ A]
  [inst_7 : NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] [ContinuousMapZero.UniqueHom ℂ A] [T2Space A]
  (f : ℝ → ℝ) (a : A),
  autoParam (ContinuousOn f (quasispectrum ℝ ↑(imaginaryPart a))) cfcₙ_comp_im._auto_1 →
    autoParam (f 0 = 0) cfcₙ_comp_im._auto_3 →
      autoParam (IsStarNormal a) cfcₙ_comp_im._auto_5 → cfcₙ (fun x => ↑(f x.im)) a = cfcₙ f ↑(imaginaryPart a)
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- `simp [foo]` should undo a previous `attribute @[-simp] foo`.
(Note that `attribute @[simp] foo` does not undo a `attribute @[simp] foo`, see #5852)
 -/
Lean.Meta.SimpTheorems.uneraseSimpEntry : Lean.Meta.SimpTheorems → Lean.Meta.SimpEntry → Lean.Meta.SimpTheorems
-- Batteries.Classes.Order
Std.LawfulBCmp.mk : ∀ {α : Type u_1} [inst : LE α] [inst_1 : LT α] [inst_2 : BEq α] {cmp : α → α → Ordering} [toTransCmp : Std.TransCmp cmp]
  [toLawfulBEqCmp : Std.LawfulBEqCmp cmp],
  (∀ {x y : α}, cmp x y = Ordering.lt ↔ x < y) → (∀ {x y : α}, (cmp x y).isLE = true ↔ x ≤ y) → Std.LawfulBCmp cmp
-- Mathlib.CategoryTheory.Limits.Preserves.Presheaf
/-- If `C` is a small finitely cocomplete category and `A : Cᵒᵖ ⥤ Type u` is a presheaf, then
`CostructuredArrow yoneda A` is filtered if and only if `A` preserves finite limits.

Proposition 3.3.13 of [Kashiwara2006].
 -/
CategoryTheory.Limits.isFiltered_costructuredArrow_yoneda_iff_nonempty_preservesFiniteLimits : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [CategoryTheory.Limits.HasFiniteColimits C]
  (A : CategoryTheory.Functor Cᵒᵖ (Type u)),
  CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A) ↔
    CategoryTheory.Limits.PreservesFiniteLimits A