mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.contains_alter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (Std.DHashMap.Const.alter m k f).contains k' =
    if (k == k') = true then (f (Std.DHashMap.Const.get? m k)).isSome else m.contains k'
-- Mathlib.Computability.RE
ComputablePred.not : ∀ {α : Type u_1} [inst : Primcodable α] {p : α → Prop}, ComputablePred p → ComputablePred fun a => ¬p a
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.HomotopyEquiv.refl_homotopyInvHomId : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C),
  (CategoryTheory.ShortComplex.HomotopyEquiv.refl S).homotopyInvHomId = CategoryTheory.ShortComplex.Homotopy.ofEq ⋯
-- Mathlib.Algebra.Group.Basic
smul_dite : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul β α] (p : Prop) [inst_1 : Decidable p] (a : p → α) (b : ¬p → α) (c : β),
  (c • if h : p then a h else b h) = if h : p then c • a h else c • b h
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.denote.eq_3 : ∀ (ctx : Int.Internal.Linear.Context) (a : Int.Internal.Linear.Expr),
  Int.Internal.Linear.Expr.denote ctx a.neg = -Int.Internal.Linear.Expr.denote ctx a
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.changeFunctor_unitIso_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) {G : CategoryTheory.Functor C D} (iso : e.functor ≅ G) (X : C),
  (e.changeFunctor iso).unitIso.hom.app X =
    CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app X) (e.inverse.map (iso.hom.app X))
-- Mathlib.SetTheory.ZFC.Basic
/-- The membership relation for ZFC sets is inherited from the membership relation for pre-sets.  -/
ZFSet.Mem : ZFSet.{u_1} → ZFSet.{u_1} → Prop
-- Init.Data.SInt.Basic
/-- Arithmetic right shift for 8-bit signed integers. Usually accessed via the `<<<` operator.

The high bits are filled with the value of the most significant bit.

This function is overridden at runtime with an efficient implementation.
 -/
Int8.shiftRight : Int8 → Int8 → Int8
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.kernelIsoOfEq_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g h : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] [inst_3 : CategoryTheory.Limits.HasKernel g]
  [inst_4 : CategoryTheory.Limits.HasKernel h] (w₁ : f = g) (w₂ : g = h),
  CategoryTheory.Limits.kernelIsoOfEq w₁ ≪≫ CategoryTheory.Limits.kernelIsoOfEq w₂ =
    CategoryTheory.Limits.kernelIsoOfEq ⋯
-- Mathlib.Data.Fintype.Sets
/-- Membership of a set with a `Fintype` instance is decidable.

Using this as an instance leads to potential loops with `Subtype.fintype` under certain decidability
assumptions, so it should only be declared a local instance.  -/
Set.decidableMemOfFintype : {α : Type u_1} → [DecidableEq α] → (s : Set α) → [Fintype ↑s] → (a : α) → Decidable (a ∈ s)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getEntryGTD_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α}
  {fallback : (a : α) × β a}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryGTD k fallback = t₂.getEntryGTD k fallback
-- Batteries.Data.List.Scan
List.partialSums_append : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Zero α] [Std.Associative fun x1 x2 => x1 + x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0] {l₁ l₂ : List α},
  (l₁ ++ l₂).partialSums = l₁.partialSums ++ List.map (fun x => l₁.sum + x) l₂.partialSums.tail
-- Mathlib.GroupTheory.Abelianization.Defs
/-- An Abelian group is equivalent to its own abelianization.  -/
Abelianization.equivOfComm : {H : Type u_1} → [inst : CommGroup H] → H ≃* Abelianization H
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.opIso_hom_app_hom_apply : ∀ (n : SimplexCategory) (X : SimplexCategoryᵒᵖ) (x : (SSet.stdSimplex.obj n).op.obj X),
  (CategoryTheory.ConcreteCategory.hom ((SSet.stdSimplex.opIso n).hom.app X)) x = SSet.stdSimplex.opObjEquiv x
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_min : ∀ (r p : NNReal), ↑(min r p) = min ↑r ↑p
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_eraseKey_of_beq : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α},
  Std.Internal.List.DistinctKeys l →
    (k == a) = true → Std.Internal.List.getValue? a (Std.Internal.List.eraseKey k l) = none
-- Init.Data.UInt.Log2
/-- Base-two logarithm of 64-bit unsigned integers. Returns `⌊max 0 (log₂ a)⌋`.

This function is overridden at runtime with an efficient implementation. This definition is
the logical model.

Examples:
 * `UInt64.log2 0 = 0`
 * `UInt64.log2 1 = 0`
 * `UInt64.log2 2 = 1`
 * `UInt64.log2 4 = 2`
 * `UInt64.log2 7 = 2`
 * `UInt64.log2 8 = 3`
 -/
UInt64.log2 : UInt64 → UInt64
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.localTriv_symmL : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField R] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace R F] [inst_3 : TopologicalSpace B] {ι : Type u_5} (Z : VectorBundleCore R B F ι) {i : ι}
  {b : B},
  b ∈ (Z.localTriv i).baseSet → Bundle.Trivialization.symmL R (Z.localTriv i) b = Z.coordChange i (Z.indexAt b) b
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
CategoryTheory.Limits.PreservesCoequalizer.iso_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCoequalizer f g]
  [inst_3 : CategoryTheory.Limits.HasCoequalizer (G.map f) (G.map g)]
  [inst_4 : CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G],
  (CategoryTheory.Limits.PreservesCoequalizer.iso G f g).hom = CategoryTheory.Limits.coequalizerComparison f g G
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.instIsContinuousOverLeftIteratedSliceForwardOver : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {X : C}
  (f : CategoryTheory.Over X), f.iteratedSliceForward.IsContinuous ((J.over X).over f) (J.over f.left)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_addNat_uIoo_addNat : ∀ {n : ℕ} (m : ℕ) (i j : Fin n), (fun x => x.addNat m) ⁻¹' Set.uIoo (i.addNat m) (j.addNat m) = Set.uIoo i j
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.comp_lipschitzOnWith : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β]
  [inst_2 : PseudoEMetricSpace γ] {Kf Kg : NNReal} {f : β → γ} {g : α → β} {s : Set α},
  LipschitzWith Kf f → LipschitzOnWith Kg g s → LipschitzOnWith (Kf * Kg) (f ∘ g) s
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.commaCategory : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            {L : CategoryTheory.Functor A T} →
              {R : CategoryTheory.Functor B T} →
                CategoryTheory.Category.{max v₂ v₁, max (max u₂ u₁) v₃} (CategoryTheory.Comma L R)
-- Mathlib.Probability.Kernel.Condexp
ProbabilityTheory.condExp_ae_eq_integral_condExpKernel' : ∀ {Ω : Type u_1} {F : Type u_2} {m : MeasurableSpace Ω} [mΩ : MeasurableSpace Ω] [inst : StandardBorelSpace Ω]
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] [inst_2 : NormedAddCommGroup F] {f : Ω → F}
  [inst_3 : NormedSpace ℝ F] [CompleteSpace F],
  MeasureTheory.Integrable f μ → μ[f | m ⊓ mΩ] =ᵐ[μ] fun ω => ∫ (y : Ω), f y ∂(ProbabilityTheory.condExpKernel μ m) ω
-- Mathlib.CategoryTheory.Galois.Basic
/-- The evaluation map is injective for connected objects.  -/
CategoryTheory.PreGaloisCategory.evaluation_injective_of_isConnected : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  [inst_1 : CategoryTheory.PreGaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] (A X : C)
  [CategoryTheory.PreGaloisCategory.IsConnected A] (a : (F.obj A).obj),
  Function.Injective fun f => (CategoryTheory.ConcreteCategory.hom (F.map f)) a
-- Init.Data.Array.Erase
Array.size_eraseP_of_mem : ∀ {α : Type u_1} {a : α} {p : α → Bool} {xs : Array α}, a ∈ xs → p a = true → (xs.eraseP p).size = xs.size - 1
-- Mathlib.SetTheory.Ordinal.Basic
/-- **Alias** of `Cardinal.mk_Iio_ordinal`. -/
Ordinal.mk_Iio_ordinal : ∀ (o : Ordinal.{u}), Cardinal.mk ↑(Set.Iio o) = Cardinal.lift.{u + 1, u} o.card
-- Mathlib.Data.Multiset.Pi
Multiset.Pi.cons_same : ∀ {α : Type u_1} [inst : DecidableEq α] {δ : α → Sort u_2} {m : Multiset α} {a : α} {b : δ a}
  {f : (a : α) → a ∈ m → δ a} (h : a ∈ a ::ₘ m), Multiset.Pi.cons m a b f a h = b
-- Std.Do.SPred.Notation
/-- Embedding of pure Lean values into `SVal`. An alias for `SPred.pure`.  -/
Std.Do.«term⌜_⌝» : Lean.ParserDescr
-- Mathlib.Order.ConditionallyCompleteLattice.Group
ciInf_add_ciInf_le_ciInf_add : ∀ {α : Type u_1} {ι : Sort u_2} [Nonempty ι] [inst : ConditionallyCompleteLattice α] [inst_1 : Add α] [AddLeftMono α]
  [AddRightMono α] {f g : ι → α},
  BddBelow (Set.range f) → BddBelow (Set.range g) → (⨅ i, f i) + ⨅ i, g i ≤ ⨅ i, f i + g i
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonColorInformation : Lean.FromJson Lean.Lsp.ColorInformation
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Limits.CoproductsOfShapeDisjoint.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {ι : Type u_2},
  (∀ (X : ι → C), CategoryTheory.Limits.CoproductDisjoint X) → CategoryTheory.Limits.CoproductsOfShapeDisjoint C ι
-- Mathlib.CategoryTheory.Equivalence
CategoryTheory.Equivalence.functor_unit_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : C ≌ D) (X : C),
  CategoryTheory.CategoryStruct.comp (e.functor.map (e.unit.app X)) (e.counit.app (e.functor.obj X)) =
    CategoryTheory.CategoryStruct.id (e.functor.obj X)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.idealOfLE_le_of_le : ∀ {K : Type u} [inst : Field K] (A R S : ValuationSubring K) (hR : A ≤ R) (hS : A ≤ S),
  R ≤ S → A.idealOfLE S hS ≤ A.idealOfLE R hR
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.isAlgClosed : ∀ (k : Type u) [inst : Field k], IsAlgClosed (AlgebraicClosure k)
-- Mathlib.Analysis.Calculus.Deriv.Inv
hasStrictFDerivAt_inv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜},
  x ≠ 0 → HasStrictFDerivAt (fun x => x⁻¹) (ContinuousLinearMap.toSpanSingleton 𝕜 (-(x ^ 2)⁻¹)) x
-- Mathlib.Topology.Category.LightProfinite.Basic
/-- The inverse part of the equivalence `LightProfinite ≌ LightDiagram`  -/
lightDiagramToLightProfinite : CategoryTheory.Functor LightDiagram LightProfinite
-- Batteries.Data.String.Lemmas
String.valid_mkIterator : ∀ (s : String), (String.Legacy.mkIterator s).Valid
-- Mathlib.RingTheory.Length
Module.length_ne_top_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.length R M ≠ ⊤ ↔ IsFiniteLength R M
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- The sequence `stirlingSeq ∘ succ` is monotone decreasing  -/
Stirling.stirlingSeq'_antitone : Antitone (Stirling.stirlingSeq ∘ Nat.succ)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A regular monomorphism is a morphism which is the equalizer of some parallel pair.  -/
CategoryTheory.RegularMono : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → (X ⟶ Y) → Type (max u₁ v₁)
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMono.mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (se : CategoryTheory.SplitMono f),
  CategoryTheory.Mono f
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Monad.id_η_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (X : C),
  (CategoryTheory.Monad.id C).η.app X = CategoryTheory.CategoryStruct.id X
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
/-- The set of all maximal tangent spaces to the sphere `s`.  -/
EuclideanGeometry.Sphere.tangentSet : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] → EuclideanGeometry.Sphere P → Set (AffineSubspace ℝ P)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.colimitIsoColimitCurryCompColim_ι_ι_inv_assoc : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C) [inst_3 : CategoryTheory.Limits.HasColimitsOfShape K C]
  [inst_4 : CategoryTheory.Limits.HasColimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim)]
  {j : J} {k : K} {Z : C} (h : CategoryTheory.Limits.colimit G ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).obj j) k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.colimit.ι ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.colim) j)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitIsoColimitCurryCompColim G).inv h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G (j, k)) h
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.isoMk_hom_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (hl : f.left ≅ g.left)
  (hw : autoParam (CategoryTheory.CategoryStruct.comp hl.hom g.hom = f.hom) CategoryTheory.Over.isoMk._auto_1),
  (CategoryTheory.Over.isoMk hl hw).hom.left = hl.hom
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RxcIterator.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : SizeOf α] [inst_2 : (a : α) → SizeOf (β a)]
  (iter : Std.DTreeMap.Internal.Zipper α β) (upper : α),
  sizeOf { iter := iter, upper := upper } = 1 + sizeOf iter + sizeOf upper
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.NonnegCoeffs : Lean.Grind.Linarith.Poly → Prop
-- Mathlib.Tactic.NormNum.NatFib
Mathlib.Meta.NormNum.isFibAux_two_mul_done : ∀ {n a b n' a' : ℕ}, Mathlib.Meta.NormNum.IsFibAux n a b → 2 * n = n' → a * (2 * b - a) = a' → Nat.fib n' = a'
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.Spec_essSurj : AlgebraicGeometry.AffineScheme.Spec.EssSurj
-- Mathlib.Topology.Algebra.Constructions
Units.instT2Space : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Monoid M] [T2Space M], T2Space Mˣ
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_ofNatClamp_of_lt : ∀ {n : ℕ}, n < UInt16.size → (UInt16.ofNatClamp n).toUInt8 = UInt8.ofNat n
-- Mathlib.Algebra.GradedMulAction
/-- The homogeneous multiplication map `smul`  -/
GradedMonoid.GSMul.smul : {ιA : Type u_1} →
  {ιM : Type u_3} →
    {A : ιA → Type u_4} →
      {M : ιM → Type u_5} →
        {inst : VAdd ιA ιM} → [self : GradedMonoid.GSMul A M] → {i : ιA} → {j : ιM} → A i → M j → M (i +ᵥ j)
-- Mathlib.Topology.UniformSpace.Basic
instUniformSpaceInt : UniformSpace ℤ
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.equalizer_toSubmodule : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {φ ψ : A →ₐ[R] B},
  Subalgebra.toSubmodule (φ.equalizer ψ) = (LinearMapClass.linearMap φ).eqLocus (LinearMapClass.linearMap ψ)
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.add_iSup : ∀ (o : Ordinal.{u}) {ι : Type u_1} [Small.{u, u_1} ι] [Nonempty ι] (f : ι → Ordinal.{u}), o + ⨆ i, f i = ⨆ i, o + f i
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalRingHom.coe_rangeRestrict : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocRing R] [inst_1 : NonUnitalNonAssocRing S] (f : R →ₙ+* S) (x : R),
  ↑(f.rangeRestrict x) = f x
-- Mathlib.Data.Int.Log
/-- The greatest power of `b` such that `b ^ log b r ≤ r`.  -/
Int.log : {R : Type u_1} → [inst : Semifield R] → [inst_1 : LinearOrder R] → [FloorSemiring R] → ℕ → R → ℤ
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.vadd : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ],
  MeasureTheory.IsAddFundamentalDomain G s μ → ∀ (g : G), MeasureTheory.IsAddFundamentalDomain G (g +ᵥ s) μ
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.separatingRight_toLinearMap₂_iff : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n] {M : Matrix m n R}
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂),
  ((Matrix.toLinearMap₂ b₁ b₂) M).SeparatingRight ↔ M.SeparatingRight
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- Typeclass defining manifolds with respect to a model with corners, over a
field `𝕜`. This definition includes the model with corners `I` (which might allow boundary, corners,
or not, so this class covers both manifolds with boundary and manifolds without boundary), and
a smoothness parameter `n : ℕ∞ω` (where `n = 0` means topological manifold, `n = ∞` means
smooth manifold and `n = ω` means analytic manifold).  -/
IsManifold : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              ModelWithCorners 𝕜 E H →
                WithTop ℕ∞ → (M : Type u_4) → [inst : TopologicalSpace M] → [ChartedSpace H M] → Prop
-- Mathlib.Topology.MetricSpace.ProperSpace.Real
EReal.instSecondCountableTopology : SecondCountableTopology EReal
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.Slice.endsWith_char_iff_exists_append : ∀ {c : Char} {s : String.Slice}, s.endsWith c = true ↔ ∃ t, s.copy = t ++ String.singleton c
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- Clique-freeness is preserved by `replaceVertex`.  -/
SimpleGraph.CliqueFree.replaceVertex : ∀ {α : Type u_1} {G : SimpleGraph α} {n : ℕ} [inst : DecidableEq α],
  G.CliqueFree n → ∀ (s t : α), (G.replaceVertex s t).CliqueFree n
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR₂.run'.eq_def : ∀ {α : Type u_1} (le : α → α → Bool) {n : ℕ} (a : { l // l.length = n }),
  List.MergeSort.Internal.mergeSortTR₂.run'✝ le a =
    match n, a with
    | 0, ⟨[], property⟩ => []
    | 1, ⟨[a], property⟩ => [a]
    | n.succ.succ, xs =>
      match List.MergeSort.Internal.splitRevInTwo' xs with
      | (l, r) =>
        List.MergeSort.Internal.mergeTR (List.MergeSort.Internal.mergeSortTR₂.run'✝ le r)
          (List.MergeSort.Internal.mergeSortTR₂.run✝ le l) le
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.derivWeierstrassP_sub_coe : ∀ (L : PeriodPair) (z : ℂ) (l : ↥L.lattice), L.derivWeierstrassP (z - ↑l) = L.derivWeierstrassP z
-- Mathlib.Data.Finsupp.Order
Finsupp.sum_nonneg : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Zero α] [inst_1 : AddCommMonoid β] [inst_2 : Preorder β]
  [IsOrderedAddMonoid β] {f : ι →₀ α} {h₁ : ι → α → β}, (∀ i ∈ f.support, 0 ≤ h₁ i (f i)) → 0 ≤ f.sum h₁
-- Mathlib.Algebra.Algebra.Operations
Submodule.algebraMap_mem : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (r : R),
  (algebraMap R A) r ∈ 1
-- Mathlib.Topology.MetricSpace.Infsep
Set.einfsep_le_of_mem_of_edist_le : ∀ {α : Type u_1} [inst : EDist α] {s : Set α} {d : ENNReal} {x : α},
  x ∈ s → ∀ {y : α}, y ∈ s → x ≠ y → edist x y ≤ d → s.einfsep ≤ d
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instContinuousMapClassContMDiffAddMonoidMorphism : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {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_4}
  [inst_4 : AddMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {H' : Type u_5}
  [inst_7 : TopologicalSpace H'] {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [inst_10 : AddMonoid G'] [inst_11 : TopologicalSpace G']
  [inst_12 : ChartedSpace H' G'], ContinuousMapClass (ContMDiffAddMonoidMorphism I I' n G G') G G'
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.sumElim_vecMul_fromRows : ∀ {R : Type u_1} {m₁ : Type u_3} {m₂ : Type u_4} {n : Type u_5} [inst : Semiring R] [inst_1 : Fintype m₁]
  [inst_2 : Fintype m₂] (B₁ : Matrix m₁ n R) (B₂ : Matrix m₂ n R) (v₁ : m₁ → R) (v₂ : m₂ → R),
  Matrix.vecMul (Sum.elim v₁ v₂) (B₁.fromRows B₂) = Matrix.vecMul v₁ B₁ + Matrix.vecMul v₂ B₂
-- Mathlib.Data.List.Basic
List.Perm.disjoint_left : ∀ {α : Type u} {l₁ l₂ l : List α}, l₁.Perm l₂ → (l₁.Disjoint l ↔ l₂.Disjoint l)
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.ι_colimitDesc_assoc : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsFiltered J] (F : CategoryTheory.Functor J (ModuleCat R))
  (t : CategoryTheory.Limits.Cocone F) (j : J) {Z : ModuleCat R} (h : t.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((ModuleCat.FilteredColimits.colimitCocone F).ι.app j)
      (CategoryTheory.CategoryStruct.comp (ModuleCat.FilteredColimits.colimitDesc F t) h) =
    CategoryTheory.CategoryStruct.comp (t.ι.app j) h
-- Mathlib.Data.Finset.Defs
Finset.Subset.antisymm : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, s₁ ⊆ s₂ → s₂ ⊆ s₁ → s₁ = s₂
-- Mathlib.Analysis.Normed.Group.Basic
nnnorm_le_nnnorm_add_nnnorm_div : ∀ {E : Type u_5} [inst : SeminormedGroup E] (a b : E), ‖b‖₊ ≤ ‖a‖₊ + ‖a / b‖₊
-- Mathlib.Order.Filter.CardinalInter
Filter.instCardinalInterFilterMap : ∀ {α β : Type u} {c : Cardinal.{u}} (l : Filter α) [CardinalInterFilter l c] (f : α → β),
  CardinalInterFilter (Filter.map f l) c
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_veblenWith_eq_veblenWith_iff : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ a : Ordinal.{u}},
  Order.IsNormal f →
    o₂ ≤ o₁ →
      (Ordinal.veblenWith f o₁ (Ordinal.veblenWith f o₂ a) = Ordinal.veblenWith f o₂ a ↔ Ordinal.veblenWith f o₁ a = a)
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.gc_map_comap : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] (f : F),
  GaloisConnection (NonUnitalStarSubalgebra.map f) (NonUnitalStarSubalgebra.comap f)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.addMap_of_Z_eq_zero_left : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F}
  {Q : WeierstrassCurve.Jacobian.PointClass F}, W.Nonsingular P → W.NonsingularLift Q → P 2 = 0 → W.addMap ⟦P⟧ Q = Q