mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Basic
AlgebraicGeometry.Proj.basicOpen_zero : ∀ {σ : Type u_1} {A : Type u} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], AlgebraicGeometry.Proj.basicOpen 𝒜 0 = ⊥
-- Init.Data.List.Find
List.findSome?_guard : ∀ {α : Type u_1} {p : α → Bool} {l : List α}, List.findSome? (Option.guard p) l = List.find? p l
-- Init.Data.UInt.Lemmas
UInt16.ofNat.eq_1 : ∀ (n : ℕ), UInt16.ofNat n = { toBitVec := BitVec.ofNat 16 n }
-- Init.Grind.Order
Lean.Grind.Order.le_of_not_le : ∀ {α : Type u_1} [inst : LE α] [Std.IsLinearPreorder α] {a b : α}, ¬a ≤ b → b ≤ a
-- Std.Tactic.BVDecide.Normalize.Equal
Std.Tactic.BVDecide.Frontend.Normalize.BitVec.eq_neg_add_iff_add_eq : ∀ {w : ℕ} (a b c : BitVec w), (a == ~~~b + 1#w + c) = (a + b == c)
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.wittPolyProdRemainder_vars : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), (WittVector.wittPolyProdRemainder p n).vars ⊆ Finset.univ ×ˢ Finset.range n
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.abs_sin_lt_abs : ∀ {x : ℝ}, x ≠ 0 → |Real.sin x| < |x|
-- Mathlib.Algebra.LieRinehartAlgebra.Defs
LieRinehartAlgebra.Hom.mk : {R : Type u_1} →
  {A₁ : Type u_2} →
    {A₂ : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : CommRing A₁] →
          [inst_2 : CommRing A₂] →
            [inst_3 : Algebra R A₁] →
              [inst_4 : Algebra R A₂] →
                {σ : A₁ →ₐ[R] A₂} →
                  {L₁ : Type u_8} →
                    {L₂ : Type u_9} →
                      [inst_5 : LieRing L₁] →
                        [inst_6 : Module A₁ L₁] →
                          [inst_7 : LieRingModule L₁ A₁] →
                            [inst_8 : LieAlgebra R L₁] →
                              [inst_9 : LieRing L₂] →
                                [inst_10 : Module A₂ L₂] →
                                  [inst_11 : LieRingModule L₂ A₂] →
                                    [inst_12 : LieAlgebra R L₂] →
                                      (toLieHom : L₁ →ₗ⁅R⁆ L₂) →
                                        (∀ (a : A₁) (x : L₁), toLieHom (a • x) = σ a • toLieHom x) →
                                          (∀ (a : A₁) (x : L₁), σ ⁅x, a⁆ = ⁅toLieHom x, σ a⁆) →
                                            LieRinehartAlgebra.Hom σ L₁ L₂
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.cache : Bool → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Batteries.Data.String.Lemmas
String.prev_of_valid' : ∀ (cs cs' : List Char),
  String.Pos.Raw.prev (String.ofList (cs ++ cs')) { byteIdx := String.utf8Len cs } =
    { byteIdx := String.utf8Len cs.dropLast }
-- Mathlib.Data.Rel
SetRel.mem_id : ∀ {α : Type u_1} {a₁ a₂ : α}, (a₁, a₂) ∈ SetRel.id ↔ a₁ = a₂
-- Aesop.ElabM
Aesop.ElabM.Context.parsePriorities : Aesop.ElabM.Context → Bool
-- Mathlib.Topology.Sets.Compacts
/-- For `K` a compact subset inside an open subset `U`, `U` has a structure of open neighbourhood
of `K`  -/
TopologicalSpace.Opens.openNhdsOfCompactsInside : {α : Type u_1} → [inst : TopologicalSpace α] → {U : TopologicalSpace.Opens α} → (K : ↑U.compactsInside) → ↑(↑K).openNhds
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_unitOfList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.DHashMap.Raw.Const.unitOfList l).getKey? k' = some k
-- Init.Data.List.Basic
List.filterTR_loop_eq : ∀ {α : Type u} {p : α → Bool} {as bs : List α}, List.filterTR.loop p as bs = bs.reverse ++ List.filter p as
-- Mathlib.Data.Set.Sigma
Set.biUnion_sigma' : ∀ {ι : Type u_1} {α : ι → Type u_3} {β : Type u_5} (s : Set ι) (t : (i : ι) → Set (α i)) (f : (i : ι) → α i → Set β),
  ⋃ i ∈ s, ⋃ j ∈ t i, f i j = ⋃ ij ∈ s.sigma t, f ij.fst ij.snd
-- Mathlib.CategoryTheory.Filtered.Final
/-- If `C` is cofiltered, then `F : C ⥤ D` is initial if and only if `CostructuredArrow F d` is
cofiltered for all `d : D`.  -/
CategoryTheory.Functor.initial_iff_isCofiltered_costructuredArrow : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C],
  F.Initial ↔ ∀ (d : D), CategoryTheory.IsCofiltered (CategoryTheory.CostructuredArrow F d)
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicAt.neg_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E}, MeromorphicAt (-f) x ↔ MeromorphicAt f x
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `f` is an antitone function taking values in a complete lattice
and `g` tends to `atTop` along a nontrivial filter,
then the indexed infimum of `f ∘ g` is equal to the indexed infimum of `f`.  -/
Antitone.iInf_comp_tendsto_atTop : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : ConditionallyCompleteLattice γ]
  [OrderBot γ] {l : Filter α} [l.NeBot] {f : β → γ},
  Antitone f → ∀ {g : α → β}, Filter.Tendsto g l Filter.atTop → ⨅ a, f (g a) = ⨅ b, f b
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.map_mono : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {K K' : Subgroup G},
  K ≤ K' → Subgroup.map f K ≤ Subgroup.map f K'
-- Mathlib.Analysis.Distribution.TestFunction
/-- `TestFunctionClass B Ω F n` states that `B` is a type of `n`-times continuously
differentiable functions `E → F` with compact support contained in `Ω : Opens E`.  -/
TestFunctionClass : Type u_6 →
  {E : outParam (Type u_7)} →
    [inst : NormedAddCommGroup E] →
      [NormedSpace ℝ E] →
        outParam (TopologicalSpace.Opens E) →
          (F : outParam (Type u_8)) →
            [inst : NormedAddCommGroup F] → [NormedSpace ℝ F] → outParam ℕ∞ → Type (max (max u_6 u_7) u_8)
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.filterMap_push.match_1.eq_2 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match some b with
    | none => h_1 ()
    | some b => h_2 b) =
    h_2 b
-- Mathlib.Topology.Sheaves.Skyscraper
skyscraperPresheafStalkOfSpecializes.congr_simp : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{u, v} C] (A : C) [inst_2 : CategoryTheory.Limits.HasTerminal C]
  [inst_3 : CategoryTheory.Limits.HasColimits C] {y : ↑X} (h : p₀ ⤳ y),
  skyscraperPresheafStalkOfSpecializes p₀ A h = skyscraperPresheafStalkOfSpecializes p₀ A h
-- Mathlib.Analysis.Complex.Isometry
Matrix.planeConformalMatrix.congr_simp : ∀ {R : Type u_1} [inst : Field R] (a a_1 : R) (e_a : a = a_1) (b b_1 : R) (e_b : b = b_1) (hab : a ^ 2 + b ^ 2 ≠ 0),
  Matrix.planeConformalMatrix a b hab = Matrix.planeConformalMatrix a_1 b_1 ⋯
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.uliftYonedaEquiv_symm_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} (f : X ⟶ Y)
  {F : CategoryTheory.Functor Cᵒᵖ (Type (max w v₁))} (t : F.obj X),
  CategoryTheory.uliftYonedaEquiv.symm ((CategoryTheory.ConcreteCategory.hom (F.map f)) t) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.uliftYoneda.{w, v₁, u₁}.map f.unop)
      (CategoryTheory.uliftYonedaEquiv.symm t)
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.instL : {R : Type u_1} →
  {N : Type u_2} →
    {M : Type u_4} →
      [inst : CommRing R] →
        [inst_1 : LieRing N] →
          [inst_2 : LieAlgebra R N] →
            [inst_3 : LieRing M] → [inst_4 : LieAlgebra R M] → (E : LieAlgebra.Extension R M N) → LieAlgebra R E.L
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.modify.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.LawfulEqOrd α] (k : α) (f : β k → β k),
  Std.DTreeMap.Internal.Impl.modify k f Std.DTreeMap.Internal.Impl.leaf = Std.DTreeMap.Internal.Impl.leaf
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.iSup_genWeightSpace_eq_top' : ∀ (K : Type u_1) (L : Type u_3) (M : Type u_4) [inst : LieRing L] [inst_1 : AddCommGroup M] [inst_2 : LieRingModule L M]
  [inst_3 : LieRing.IsNilpotent L] [inst_4 : Field K] [inst_5 : LieAlgebra K L] [inst_6 : Module K M]
  [inst_7 : LieModule K L M] [FiniteDimensional K M] [LieModule.IsTriangularizable K L M],
  ⨆ χ, LieModule.genWeightSpace M ⇑χ = ⊤
-- Mathlib.Order.Heyting.Basic
himp_inf_himp_inf_le : ∀ {α : Type u_2} [inst : GeneralizedHeytingAlgebra α] {a b c : α}, (b ⇨ c) ⊓ (a ⇨ b) ⊓ a ≤ c
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv_eqOn : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {f' : 𝕜 → F},
  IsOpen s → (∀ x ∈ s, HasDerivWithinAt f (f' x) s x) → Set.EqOn (deriv f) f' s
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.Coloring.colorable : ∀ {V : Type u} {G : SimpleGraph V} {α : Type u_2} [inst : Fintype α] (C : G.Coloring α), G.Colorable (Fintype.card α)
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- Suppose that a function `f : ℂ → E` is continuous on a closed rectangle with opposite corners at
`z w : ℂ`, is *real* differentiable at all but countably many points of the corresponding open
rectangle, and $\frac{\partial f}{\partial \bar z}$ is integrable on this rectangle. Then the
integral of `f` over the boundary of the rectangle is equal to the integral of
$2i\frac{\partial f}{\partial \bar z}=i\frac{\partial f}{\partial x}-\frac{\partial f}{\partial y}$
over the rectangle.  -/
Complex.integral_boundary_rect_of_hasFDerivAt_real_off_countable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (f' : ℂ → ℂ →L[ℝ] E) (z w : ℂ)
  (s : Set ℂ),
  s.Countable →
    ContinuousOn f (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) →
      (∀ x ∈ Set.Ioo (min z.re w.re) (max z.re w.re) ×ℂ Set.Ioo (min z.im w.im) (max z.im w.im) \ s,
          HasFDerivAt f (f' x) x) →
        MeasureTheory.IntegrableOn (fun z => Complex.I • (f' z) 1 - (f' z) Complex.I)
            (Set.uIcc z.re w.re ×ℂ Set.uIcc z.im w.im) MeasureTheory.volume →
          (((∫ (x : ℝ) in z.re..w.re, f (↑x + ↑z.im * Complex.I)) -
                  ∫ (x : ℝ) in z.re..w.re, f (↑x + ↑w.im * Complex.I)) +
                Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑w.re + ↑y * Complex.I)) -
              Complex.I • ∫ (y : ℝ) in z.im..w.im, f (↑z.re + ↑y * Complex.I) =
            ∫ (x : ℝ) in z.re..w.re,
              ∫ (y : ℝ) in z.im..w.im, Complex.I • (f' (↑x + ↑y * Complex.I)) 1 - (f' (↑x + ↑y * Complex.I)) Complex.I
-- Mathlib.Data.Finset.Card
Finset.strongInduction.eq_1 : ∀ {α : Type u_1} {p : Finset α → Sort u_4} (H : (s : Finset α) → ((t : Finset α) → t ⊂ s → p t) → p s) (x : Finset α),
  Finset.strongInduction H x =
    H x fun t h =>
      have this := ⋯;
      Finset.strongInduction H t
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.ofCoeff_inj : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {x y : M →₀ R},
  MonoidAlgebra.ofCoeff x = MonoidAlgebra.ofCoeff y ↔ x = y
-- Mathlib.Data.Int.Bitwise
Int.lxor_bit : ∀ (a : Bool) (m : ℤ) (b : Bool) (n : ℤ), (Int.bit a m).xor (Int.bit b n) = Int.bit (a ^^ b) (m.xor n)
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty_symm_apply_apply : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β]
  [inst_3 : CompactSpace α] (f : ZeroAtInftyContinuousMap α β) (a : α),
  (ZeroAtInftyContinuousMap.ContinuousMap.liftZeroAtInfty.symm f) a = f a
-- Mathlib.Data.Nat.Dist
Nat.dist_mul_right : ∀ (n k m : ℕ), (n * k).dist (m * k) = n.dist m * k
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getThenInsertIfNew?.congr_simp : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} [inst : LawfulBEq α] (m m_1 : Std.ExtDHashMap α β),
  m = m_1 → ∀ (a : α) (b b_1 : β a), b = b_1 → m.getThenInsertIfNew? a b = m_1.getThenInsertIfNew? a b_1
-- Batteries.Data.Fin.Lemmas
Fin.foldr_assoc : ∀ {α : Sort u_1} {n : ℕ} {op : α → α → α} [ha : Std.Associative op] {f : Fin n → α} {a₁ a₂ : α},
  Fin.foldr n (fun i x => op (f i) x) (op a₁ a₂) = op (Fin.foldr n (fun i x => op (f i) x) a₁) a₂
-- Mathlib.RingTheory.FilteredAlgebra.Basic
IsFiltration.mk : ∀ {ι : Type u_1} {σ : Type u_3} [inst : Preorder ι] [inst_1 : Preorder σ] {F : ι → σ} {F_lt : outParam (ι → σ)},
  Monotone F →
    (∀ {i j : ι}, i < j → F i ≤ F_lt j) → (∀ (B : σ) (j : ι), (∀ i < j, F i ≤ B) → F_lt j ≤ B) → IsFiltration F F_lt
-- Lean.Meta.Tactic.Simp.Types
_private.Lean.Meta.Tactic.Simp.Types.0.Lean.Meta.Simp.removeUnnecessaryCasts.elimDummyEqRec : Lean.Expr → Lean.Expr
-- Mathlib.Data.Int.Init
/-- The positive case of `Int.inductionOn'`.  -/
Int.inductionOn'.pos : {motive : ℤ → Sort u_1} → (b : ℤ) → motive b → ((k : ℤ) → b ≤ k → motive k → motive (k + 1)) → (n : ℕ) → motive (b + ↑n)
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.truncTotal.congr_simp : ∀ {σ : Type u_1} [inst : Finite σ] {R : Type u_4} [inst_1 : CommSemiring R] (n n_1 : ℕ),
  n = n_1 → MvPowerSeries.truncTotal n = MvPowerSeries.truncTotal n_1
-- Mathlib.Algebra.Regular.SMul
IsSMulRegular.isLeftRegular : ∀ {R : Type u_1} [inst : Mul R] {a : R}, IsSMulRegular R a → IsLeftRegular a
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.IsOpenImmersion.instPreservesLimitSchemeLocallyRingedSpaceWalkingCospanCospanForgetToLocallyRingedSpace : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [H : AlgebraicGeometry.IsOpenImmersion f],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan f g)
    AlgebraicGeometry.Scheme.forgetToLocallyRingedSpace
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- The equalizer diagram for the sheaf condition.
 -/
TopCat.Presheaf.SheafConditionEqualizerProducts.diagram : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        TopCat.Presheaf C X →
          {ι : Type v'} →
            (ι → TopologicalSpace.Opens ↑X) → CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey_of_mem : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)} {x : (a : α) × β a},
  x ∈ l →
    Std.Internal.List.DistinctKeys l →
      ∀ {h' : Std.Internal.List.containsKey x.fst l = true}, Std.Internal.List.getKey x.fst l h' = x.fst
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.mk.injEq : ∀ {𝕜 : Type u_1} {V : Type u_2} {V₂ : Type u_5} {P : Type u_10} {P₂ : Type u_11} [inst : NormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P]
  [inst_4 : NormedAddTorsor V P] [inst_5 : SeminormedAddCommGroup V₂] [inst_6 : NormedSpace 𝕜 V₂]
  [inst_7 : PseudoMetricSpace P₂] [inst_8 : NormedAddTorsor V₂ P₂] (toAffineEquiv : P ≃ᵃ[𝕜] P₂)
  (norm_map : ∀ (x : V), ‖toAffineEquiv.linear x‖ = ‖x‖) (toAffineEquiv_1 : P ≃ᵃ[𝕜] P₂)
  (norm_map_1 : ∀ (x : V), ‖toAffineEquiv_1.linear x‖ = ‖x‖),
  ({ toAffineEquiv := toAffineEquiv, norm_map := norm_map } =
      { toAffineEquiv := toAffineEquiv_1, norm_map := norm_map_1 }) =
    (toAffineEquiv = toAffineEquiv_1)
-- Mathlib.GroupTheory.PGroup
IsPGroup.le_or_disjoint_of_coprime : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [hp : Fact (Nat.Prime p)] {P : Subgroup G},
  IsPGroup p ↥P → ∀ {H : Subgroup G} [H.Normal], (Nat.card ↥H).Coprime H.index → P ≤ H ∨ Disjoint H P
-- Lean.Meta.Tactic.Grind.Attr
Lean.Meta.Grind.AttrKind.inj.sizeOf_spec : sizeOf Lean.Meta.Grind.AttrKind.inj = 1
-- Mathlib.MeasureTheory.Integral.CircleIntegral
continuous_circleMap_inv : ∀ {R : ℝ} {z w : ℂ}, w ∈ Metric.ball z R → Continuous fun θ => (circleMap z R θ - w)⁻¹
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
/-- **Alias** of `Left.nsmul_nonpos`. -/
nsmul_nonpos : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftMono M] {a : M}, a ≤ 0 → ∀ (n : ℕ), n • a ≤ 0
-- Mathlib.Algebra.Algebra.Spectrum.Basic
spectrum.vadd_eq : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (a : A) (r : R),
  r +ᵥ spectrum R a = spectrum R ((algebraMap R A) r + a)
-- Mathlib.Algebra.Group.Action.End
AddAut.applyAddAction.eq_1 : ∀ {M : Type u_2} [inst : AddMonoid M],
  AddAut.applyAddAction = { vadd := fun x1 x2 => x1 x2, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Data.Finset.Defs
Finset.mem_val : ∀ {α : Type u_1} {a : α} {s : Finset α}, (a ∈ s.val) = (a ∈ s)
-- Mathlib.CategoryTheory.CopyDiscardCategory.Widesubcategory
CategoryTheory.MorphismProperty.instCopyDiscardCategoryWideSubcategoryOfIsStableUnderComonoid : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.MorphismProperty C) →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : CategoryTheory.CopyDiscardCategory C] →
          [inst_3 : P.IsStableUnderBraiding] →
            [∀ (c : C), P.IsStableUnderComonoid c] →
              CategoryTheory.CopyDiscardCategory (CategoryTheory.WideSubcategory P)
-- Mathlib.RingTheory.Ideal.Maps
Module.annihilator_dfinsupp : ∀ {R : Type u_1} [inst : Semiring R] {ι : Type u_4} {M : ι → Type u_5} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)], Module.annihilator R (Π₀ (i : ι), M i) = ⨅ i, Module.annihilator R (M i)
-- Mathlib.Data.Seq.Computation
Computation.map_think : ∀ {α : Type u} {β : Type v} (f : α → β) (s : Computation α), Computation.map f s.think = (Computation.map f s).think
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_insert : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α} {v : β}, a ∈ m.insert k v ↔ (k == a) = true ∨ a ∈ m
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Exact.leftHomologyDataOfIsLimitKernelFork_H : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (hS : S.Exact) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  (kf : CategoryTheory.Limits.KernelFork S.g) (hkf : CategoryTheory.Limits.IsLimit kf),
  (hS.leftHomologyDataOfIsLimitKernelFork kf hkf).H = 0
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The monoidal structure on the category of endofunctors is left distributive.  -/
CategoryTheory.isMonoidalLeftDistrib.of_endofunctors : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C],
  CategoryTheory.IsMonoidalLeftDistrib (CategoryTheory.Functor C C)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
/-- The index of the first non-zero coefficient in `p` (or `0` if all coefficients are zero). This
is the order of the isolated zero of an analytic function `f` at a point if `p` is the Taylor
series of `f` at that point.  -/
FormalMultilinearSeries.order : {𝕜 : Type u} →
  {E : Type v} →
    {F : Type w} →
      [inst : Semiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : TopologicalSpace E] →
              [inst_4 : ContinuousAdd E] →
                [inst_5 : ContinuousConstSMul 𝕜 E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module 𝕜 F] →
                      [inst_8 : TopologicalSpace F] →
                        [inst_9 : ContinuousAdd F] →
                          [inst_10 : ContinuousConstSMul 𝕜 F] → FormalMultilinearSeries 𝕜 E F → ℕ
-- Mathlib.Order.Category.BddOrd
BddOrd.ofHom_hom : ∀ {X Y : BddOrd} (f : X ⟶ Y), BddOrd.ofHom (BddOrd.Hom.hom f) = f
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.range_mk' : ∀ {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] (N : LieSubmodule R L M) [inst_5 : LieAlgebra R L]
  [inst_6 : LieModule R L M], (LieSubmodule.Quotient.mk' N).range = ⊤
-- Mathlib.MeasureTheory.Integral.Lebesgue.Markov
MeasureTheory.setLIntegral_le_meas : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s t : Set α},
  MeasurableSet s →
    ∀ {f : α → ENNReal}, (∀ a ∈ s, a ∈ t → f a ≤ 1) → (∀ a ∈ s, a ∉ t → f a = 0) → ∫⁻ (a : α) in s, f a ∂μ ≤ μ t
-- Mathlib.Algebra.NeZero
three_ne_zero' : ∀ (α : Type u_2) [inst : Zero α] [inst_1 : OfNat α 3] [NeZero 3], 3 ≠ 0
-- Mathlib.Topology.MetricSpace.Isometry
/-- A map that preserves non-negative distances is an isometry.  -/
Isometry.of_nndist_eq : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  (∀ (x y : α), nndist (f x) (f y) = nndist x y) → Isometry f
-- Mathlib.LinearAlgebra.Dimension.Finite
finrank_eq_zero_of_not_exists_basis_finset : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M],
  (¬∃ s, Nonempty (Module.Basis (↥s) R M)) → Module.finrank R M = 0
-- Mathlib.RepresentationTheory.Homological.Resolution
_private.Mathlib.RepresentationTheory.Homological.Resolution.0.«termGⁿ⁺¹» : Lean.ParserDescr
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.hasFiniteRange_iff_range : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] {f : V →ₗ[K] V₂}, f.HasFiniteRange ↔ f.range.FG
-- Mathlib.Algebra.Tropical.Basic
Tropical.instOneTropical : {R : Type u} → [Zero R] → One (Tropical R)
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.annotatePos : Lean.SubExpr.Pos → Lean.Term → Lean.Term
-- Mathlib.Analysis.LocallyConvex.Polar
LinearMap.tripolar_eq_polar : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedCommRing 𝕜] [inst_1 : AddCommMonoid E]
  [inst_2 : AddCommMonoid F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) (s : Set E),
  B.polar (B.flip.polar (B.polar s)) = B.polar s
-- Mathlib.GroupTheory.Commensurable
Subgroup.Commensurable.equivalence : ∀ {G : Type u_1} [inst : Group G], Equivalence Subgroup.Commensurable
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.forIn_eq_forIn : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ},
  Std.ExtTreeSet.forIn f init t = forIn t init f
-- Mathlib.Algebra.Notation.Support
Function.mulSupport_subset_comp : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N] {g : M → N},
  (∀ {x : M}, g x = 1 → x = 1) → ∀ (f : ι → M), Function.mulSupport f ⊆ Function.mulSupport (g ∘ f)
-- Mathlib.NumberTheory.Height.NumberField
/-- Extension for the `positivity` tactic: `Height.totalWeight` is positive for number fields.  -/
Mathlib.Meta.Positivity.evalHeightTotalWeight : Mathlib.Meta.Positivity.PositivityExt
-- Init.Core
/-- Always-true relation as a `Setoid`.  -/
Setoid.trivial : (α : Sort u) → Setoid α
-- Init.Data.UInt.Lemmas
UInt8.ofBitVec_lt_iff_lt : ∀ {a b : BitVec 8}, { toBitVec := a } < { toBitVec := b } ↔ a < b
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
Matrix.GeneralLinearGroup.mkOfDetNeZero.congr_simp : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {K : Type u_1} [inst_2 : Field K] (A A_1 : Matrix n n K)
  (e_A : A = A_1) (h : A.det ≠ 0),
  Matrix.GeneralLinearGroup.mkOfDetNeZero A h = Matrix.GeneralLinearGroup.mkOfDetNeZero A_1 ⋯
-- Mathlib.Algebra.Order.Group.Indicator
Set.indicator_apply_nonpos : ∀ {α : Type u_2} {M : Type u_3} [inst : Preorder M] [inst_1 : Zero M] {s : Set α} {f : α → M} {a : α},
  (a ∈ s → f a ≤ 0) → s.indicator f a ≤ 0
-- Mathlib.RingTheory.FiniteType
/-- If `R[M]` is of finite type, then there is a `G : Finset M` such that its image
generates, as algebra, `R[M]`.  -/
MonoidAlgebra.exists_finset_adjoin_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : Monoid M] [h : Algebra.FiniteType R (MonoidAlgebra R M)],
  ∃ G, Algebra.adjoin R (⇑(MonoidAlgebra.of R M) '' ↑G) = ⊤
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
AddCommGrpCat.forget_isCorepresentable : (CategoryTheory.forget AddCommGrpCat).IsCorepresentable