mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k : α}, k ∈ t → t.get? k = some k
-- Mathlib.Data.Finset.Option
Finset.insertNone_eraseNone : ∀ {α : Type u_1} [inst : DecidableEq (Option α)] (s : Finset (Option α)),
  Finset.insertNone (Finset.eraseNone s) = insert none s
-- Mathlib.SetTheory.Cardinal.Order
/-- A variant of `Cardinal.mk_set` expressed in terms of a `Set` instead of a `Type`.  -/
Cardinal.mk_powerset : ∀ {α : Type u} (s : Set α), Cardinal.mk ↑(𝒫 s) = 2 ^ Cardinal.mk ↑s
-- Lean.Meta.CongrTheorems
_private.Lean.Meta.CongrTheorems.0.Lean.Meta.setBinderInfosD : Array Lean.Expr → Lean.LocalContext → Lean.LocalContext
-- Mathlib.LinearAlgebra.LinearIndependent.Defs
LinearIndepOn.of_comp : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {M' : Type u_5} {v : ι → M} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M'),
  LinearIndepOn R (⇑f ∘ v) s → LinearIndepOn R v s
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The lower part of the third column of the snake diagram is exact.  -/
CategoryTheory.ShortComplex.SnakeInput.exact_C₃_down : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C),
  { X₁ := S.L₁.X₃, X₂ := S.L₂.X₃, X₃ := S.L₃.X₃, f := S.v₁₂.τ₃, g := S.v₂₃.τ₃, zero := ⋯ }.Exact
-- Std.Internal.Do.Triple.Gadget
/-- A no-op computation used as a verification gadget to inject assertions into the program.

The `name` parameter is used by VCGen to name the introduced hypothesis. The `as` parameter
is the assertion to be checked. At runtime, `assertGadget` is simply `pure ⟨⟩`.  -/
Std.Internal.Do.assertGadget : {m : Type u → Type v} →
  {Pred EPred : Type u} →
    [inst : Monad m] →
      [inst_1 : Std.Internal.Do.Assertion Pred] →
        [inst_2 : Std.Internal.Do.Assertion EPred] →
          [Std.Internal.Do.WPMonad m Pred EPred] → Lean.Name → Pred → m PUnit.{u + 1}
-- Mathlib.Analysis.Normed.Field.Basic
Real.nnnorm_mul_toNNReal : ∀ (x : ℝ) {y : ℝ}, 0 ≤ y → ‖x‖₊ * y.toNNReal = ‖x * y‖₊
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₁.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 1}
  (left left_1 :
    F.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 ⟶ G.obj' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4)
  (e_left : left = left_1)
  (right right_1 :
    F.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 ⟶ G.obj' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5)
  (e_right : right = right_1)
  (w :
    CategoryTheory.CategoryStruct.comp
        (F.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5)
        right =
      CategoryTheory.CategoryStruct.comp left
        (G.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 CategoryTheory.ComposableArrows.homMk₁._proof_5)),
  CategoryTheory.ComposableArrows.homMk₁ left right w = CategoryTheory.ComposableArrows.homMk₁ left_1 right_1 ⋯
-- Init.Data.List.Count
List.count_eq_countP : ∀ {α : Type u_1} [inst : BEq α] {a : α} {l : List α}, List.count a l = List.countP (fun x => x == a) l
-- Mathlib.Data.SetLike.Basic
SetLike.mem_mk : ∀ {X : Type u_3} {S : Type u_4} [inst : SetLike S X] {p : S → Prop} {U : S} {h : p U} {x : X}, x ∈ ⟨U, h⟩ ↔ x ∈ U
-- Mathlib.Data.Finmap
Finmap.instUnion : {α : Type u} → {β : α → Type v} → [DecidableEq α] → Union (Finmap β)
-- Mathlib.CategoryTheory.Limits.Creates
/-- `F` preserves the colimit of `K` if it creates the colimit and `K ⋙ F` has the colimit.  -/
CategoryTheory.preservesColimit_of_createsColimit_and_hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J] (K : CategoryTheory.Functor J C)
  (F : CategoryTheory.Functor C D) [CategoryTheory.CreatesColimit K F] [CategoryTheory.Limits.HasColimit (K.comp F)],
  CategoryTheory.Limits.PreservesColimit K F
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.mk : Lean.Syntax →
  Lean.Elab.DefKind →
    List Lean.Name →
      Lean.Elab.Modifiers →
        Lean.Name → Lean.Syntax → ℕ → Lean.Expr → Lean.Expr → Lean.Elab.TerminationHints → Lean.Elab.PreDefinition
-- Mathlib.Data.Num.Lemmas
Num.partialOrder : PartialOrder Num
-- Lean.Elab.MutualInductive
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.ResultingUniverseResult.mk.sizeOf_spec : ∀ (u : Lean.Level) (assign? : Option (Lean.LMVarId × Lean.Level)),
  sizeOf { u := u, assign? := assign? } = 1 + sizeOf u + sizeOf assign?
-- Init.Internal.Order.Basic
Lean.Order.monotone_const : ∀ {α : Sort u} [inst : Lean.Order.PartialOrder α] {β : Sort v} [inst_1 : Lean.Order.PartialOrder β] (c : β),
  Lean.Order.monotone fun x => c
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
/-- `ContinuousLinearMap.pi`, upgraded to a continuous linear equivalence between
`Π i, E →Lₚₜ[𝕜] F i` and `E →Lₚₜ[𝕜] Π i, F i`.  -/
PointwiseConvergenceCLM.piEquivL : (𝕜 : Type u_3) →
  [inst : NormedField 𝕜] →
    (E : Type u_7) →
      [inst_1 : AddCommGroup E] →
        [inst_2 : TopologicalSpace E] →
          [inst_3 : Module 𝕜 E] →
            {ι : Type u_11} →
              (F : ι → Type u_12) →
                [inst_4 : (i : ι) → AddCommGroup (F i)] →
                  [inst_5 : (i : ι) → Module 𝕜 (F i)] →
                    [inst_6 : (i : ι) → TopologicalSpace (F i)] →
                      [inst_7 : ∀ (i : ι), IsTopologicalAddGroup (F i)] →
                        [inst_8 : ∀ (i : ι), ContinuousConstSMul 𝕜 (F i)] →
                          ((i : ι) → E →Lₚₜ[𝕜] F i) ≃L[𝕜] E →Lₚₜ[𝕜] (i : ι) → F i
-- Lean.AddDecl
_private.Lean.AddDecl.0.Lean.addDeclCore.doAdd : Lean.Declaration → Lean.CoreM Unit
-- Mathlib.Algebra.GroupWithZero.Shrink
instMulZeroOneClassShrink : {α : Type u_2} → [inst : Small.{v, u_2} α] → [MulZeroOneClass α] → MulZeroOneClass (Shrink.{v, u_2} α)
-- Mathlib.Analysis.Complex.Order
Complex.neg_re_eq_norm : ∀ {z : ℂ}, -z.re = ‖z‖ ↔ z ≤ 0
-- Mathlib.Tactic.Module
/-- Given two terms `l₁`, `l₂` of type `qNF R M`, i.e. lists of `(Q($R) × Q($M)) × ℕ`s (two `Expr`s
and a natural number), construct another such term `l`, which will have the property that in the
`$R`-module `$M`, the sum of the "linear combinations" represented by `l₁` and `l₂` is the linear
combination represented by `l`.

The construction assumes, to be valid, that the lists `l₁` and `l₂` are in strictly increasing order
by `ℕ`-component, and that if pairs `(a₁, x₁)` and `(a₂, x₂)` appear in `l₁`, `l₂` respectively with
the same `ℕ`-component `k`, then the expressions `x₁` and `x₂` are equal.

The construction is as follows: merge the two lists, except that if pairs `(a₁, x₁)` and `(a₂, x₂)`
appear in `l₁`, `l₂` respectively with the same `ℕ`-component `k`, then contribute a term
`(a₁ + a₂, x₁)` to the output list with `ℕ`-component `k`.  -/
Mathlib.Tactic.Module.qNF.add : {u v : Lean.Level} →
  {M : Q(Type v)} →
    {R : Q(Type u)} →
      Q(Semiring «$R») → Mathlib.Tactic.Module.qNF R M → Mathlib.Tactic.Module.qNF R M → Mathlib.Tactic.Module.qNF R M
-- Aesop.Script.Tactic
Aesop.Script.Tactic : Type
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ψ_four : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.ψ 4 = Polynomial.C W.preΨ₄ * W.ψ₂
-- Init.Prelude
/-- The current macro scope.  -/
Lean.Macro.Context.currMacroScope : Lean.Macro.Context → Lean.MacroScope
-- Mathlib.Algebra.Lie.IdealOperations
LieSubmodule.lie_mem_lie : ∀ {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]
  {I : LieIdeal R L} {x : L} {m : M}, x ∈ I → m ∈ N → ⁅x, m⁆ ∈ ⁅I, N⁆
-- Mathlib.Analysis.Calculus.MeanValue
/-- General fencing theorem for continuous functions with an estimate on the derivative.
Let `f` and `B` be continuous functions on `[a, b]` such that

* `‖f a‖ ≤ B a`;
* `B` has right derivative at every point of `[a, b)`;
* for each `x ∈ [a, b)` the right-side limit inferior of `(‖f z‖ - ‖f x‖) / (z - x)`
  is bounded above by a function `f'`;
* we have `f' x < B' x` whenever `‖f x‖ = B x`.

Then `‖f x‖ ≤ B x` everywhere on `[a, b]`.  -/
image_norm_le_of_liminf_right_slope_norm_lt_deriv_boundary : ∀ {a b : ℝ} {E : Type u_3} [inst : NormedAddCommGroup E] {f : ℝ → E} {f' : ℝ → ℝ},
  ContinuousOn f (Set.Icc a b) →
    (∀ x ∈ Set.Ico a b, ∀ (r : ℝ), f' x < r → ∃ᶠ (z : ℝ) in nhdsWithin x (Set.Ioi x), slope (norm ∘ f) x z < r) →
      ∀ {B B' : ℝ → ℝ},
        ‖f a‖ ≤ B a →
          ContinuousOn B (Set.Icc a b) →
            (∀ x ∈ Set.Ico a b, HasDerivWithinAt B (B' x) (Set.Ici x) x) →
              (∀ x ∈ Set.Ico a b, ‖f x‖ = B x → f' x < B' x) → ∀ ⦃x : ℝ⦄, x ∈ Set.Icc a b → ‖f x‖ ≤ B x
-- Init.Data.UInt.Lemmas
UInt16.ofNatClamp_uInt8ToNat : ∀ (n : UInt8), UInt16.ofNatClamp n.toNat = n.toUInt16
-- Lean.Elab.InfoTree.Types
/-- Map from holes in the infotree to child infotrees.  -/
Lean.Elab.InfoState.assignment : Lean.Elab.InfoState → Lean.PersistentHashMap Lean.MVarId Lean.Elab.InfoTree
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.addSubmonoidMap_surjective : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M),
  Function.Surjective ⇑(f.addSubmonoidMap M')
-- Mathlib.Geometry.Manifold.Notation
/-- Attempt to find a model with corners on the complex unit circle  -/
_private.Mathlib.Geometry.Manifold.Notation.0.Manifold.Elab.findModelInner.fromCircle : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Data.Finsupp.Lex
Finsupp.Lex.lt_iff_of_unique : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : Unique α] [inst_2 : LT N] [inst_3 : Preorder α]
  {x y : Lex (α →₀ N)}, x < y ↔ (ofLex x) default < (ofLex y) default
-- Batteries.Data.Fin.Lemmas
Fin.isNone_findRev?_iff : ∀ {n : ℕ} {p : Fin n → Bool}, (Fin.findRev? p).isNone = true ↔ ∀ (i : Fin n), p i = false
-- Lean.Server.GoTo
Lean.Server.locationLinksFromFieldInfo : Lean.Elab.FieldInfo → Lean.Server.GoToM (Array Lean.Lsp.LeanLocationLink)
-- Mathlib.Topology.Algebra.Module.Star
/-- The decomposition of elements of a star module into their self- and skew-adjoint parts,
as a continuous linear equivalence.  -/
StarModule.decomposeProdAdjointL : (R : Type u_1) →
  (A : Type u_2) →
    [inst : Semiring R] →
      [inst_1 : StarMul R] →
        [inst_2 : TrivialStar R] →
          [inst_3 : AddCommGroup A] →
            [inst_4 : Module R A] →
              [inst_5 : StarAddMonoid A] →
                [inst_6 : StarModule R A] →
                  [Invertible 2] →
                    [inst_8 : TopologicalSpace A] →
                      [IsTopologicalAddGroup A] →
                        [ContinuousStar A] → [ContinuousConstSMul R A] → A ≃L[R] ↥(selfAdjoint A) × ↥(skewAdjoint A)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Products
CategoryTheory.Limits.instHasColimitDiscreteOppositeCompInverseOppositeOpFunctor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {α : Type u_1} {Z : α → C}
  [CategoryTheory.Limits.HasProduct Z],
  CategoryTheory.Limits.HasColimit
    ((CategoryTheory.Discrete.opposite α).inverse.comp (CategoryTheory.Discrete.functor Z).op)
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.integral_prod_smul : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  [inst_4 : NormedSpace ℝ E] [MeasureTheory.SFinite μ] {𝕜 : Type u_5} [inst_6 : RCLike 𝕜] [inst_7 : NormedSpace 𝕜 E]
  (f : α → 𝕜) (g : β → E), ∫ (z : α × β), f z.1 • g z.2 ∂μ.prod ν = (∫ (x : α), f x ∂μ) • ∫ (y : β), g y ∂ν
-- Mathlib.Probability.Independence.InfinitePi
/-- Random variables are independent iff their joint distribution is the product measure.  -/
ProbabilityTheory.iIndepFun_iff_map_fun_eq_infinitePi_map : ∀ {ι : Type u_1} {Ω : Type u_2} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {𝓧 : ι → Type u_3}
  {m𝓧 : (i : ι) → MeasurableSpace (𝓧 i)} {X : (i : ι) → Ω → 𝓧 i} [MeasureTheory.IsProbabilityMeasure P],
  (∀ (i : ι), Measurable (X i)) →
    (ProbabilityTheory.iIndepFun X P ↔
      MeasureTheory.Measure.map (fun ω i => X i ω) P =
        MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.map (X i) P)
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.ofCompletion_toCompletion : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K) (x : v.Completion),
  { toCompletion := x.toCompletion } = x
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.insert : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] (k : α) (v : β k), m₁.Equiv m₂ → (m₁.insert k v).Equiv (m₂.insert k v)
-- Mathlib.AlgebraicTopology.DoldKan.HomotopyEquivalence
AlgebraicTopology.DoldKan.homotopyPInftyToId_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (i j : ℕ),
  (AlgebraicTopology.DoldKan.homotopyPInftyToId X).hom i j = (AlgebraicTopology.DoldKan.homotopyPToId X (j + 1)).hom i j
-- Mathlib.MeasureTheory.Measure.Complex
/-- The imaginary part of a complex measure is a signed measure.  -/
MeasureTheory.ComplexMeasure.im : {α : Type u_1} → {m : MeasurableSpace α} → MeasureTheory.ComplexMeasure α →ₗ[ℝ] MeasureTheory.SignedMeasure α
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.quarterPairs : Vector String 4 → Array (String × Std.Time.Month.Quarter)
-- Mathlib.RingTheory.Localization.Basic
IsLocalization.algebraMap_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] (Rₘ : Type u_4) (Sₘ : Type u_5) [inst_3 : CommSemiring Rₘ] [inst_4 : CommSemiring Sₘ]
  [inst_5 : Algebra R Rₘ] [inst_6 : IsLocalization M Rₘ] [inst_7 : Algebra S Sₘ]
  [i : IsLocalization (Algebra.algebraMapSubmonoid S M) Sₘ] [inst_8 : Algebra Rₘ Sₘ] [inst_9 : Algebra R Sₘ]
  [IsScalarTower R Rₘ Sₘ] [IsScalarTower R S Sₘ] (x : R) (y : ↥M),
  (algebraMap Rₘ Sₘ) (IsLocalization.mk' Rₘ x y) = IsLocalization.mk' Sₘ ((algebraMap R S) x) ⟨(algebraMap R S) ↑y, ⋯⟩
-- Mathlib.NumberTheory.Height.MvPolynomial
_private.Mathlib.NumberTheory.Height.MvPolynomial.0.Height.iSup_fun_eq_max : ∀ (f : Fin 2 → ℝ), iSup f = max (f 0) (f 1)
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
DirectedOn.csInf_le_iff : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderInf α] {s : Set α} {a : α},
  DirectedOn (fun x1 x2 => x2 ≤ x1) s → BddBelow s → s.Nonempty → (sInf s ≤ a ↔ ∀ b ∈ lowerBounds s, b ≤ a)
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.leftDistributor_inv_comp_biproduct_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (X : C) (f : J → C) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.leftDistributor X f).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.Limits.biproduct.π f j)) =
    CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj X (f j)) j
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.mk_lt_mk : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x y : R) (t s : ↥(ValuativeRel.posSubmonoid R)),
  ValuativeRel.ValueGroupWithZero.mk x t < ValuativeRel.ValueGroupWithZero.mk y s ↔ x * ↑s <ᵥ y * ↑t
-- Mathlib.Algebra.Group.Units.Defs
val_div_eq_divp : ∀ {α : Type u} [inst : Monoid α] (u₁ u₂ : αˣ), ↑(u₁ / u₂) = ↑u₁ /ₚ u₂
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.instIsNormalMonoCategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.IsNormalMonoCategory (CategoryTheory.ShortComplex C)
-- Lean.Data.NameMap.Basic
Lean.mkNameMap : (α : Type) → Lean.NameMap α
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.AssocList.forInStep.go.match_3.eq_2 : ∀ {α : Type u_2} {β : α → Type u_1} {δ : Type u_4} (motive : Std.DHashMap.Internal.AssocList α β → δ → Sort u_3) (k : α)
  (v : β k) (t : Std.DHashMap.Internal.AssocList α β) (acc : δ)
  (h_1 : (acc : δ) → motive Std.DHashMap.Internal.AssocList.nil acc)
  (h_2 :
    (k : α) →
      (v : β k) →
        (t : Std.DHashMap.Internal.AssocList α β) →
          (acc : δ) → motive (Std.DHashMap.Internal.AssocList.cons k v t) acc),
  (match Std.DHashMap.Internal.AssocList.cons k v t, acc with
    | Std.DHashMap.Internal.AssocList.nil, acc => h_1 acc
    | Std.DHashMap.Internal.AssocList.cons k v t, acc => h_2 k v t acc) =
    h_2 k v t acc
-- Mathlib.MeasureTheory.Measure.Regular
/-- A measure `μ` is weakly regular if
- it is outer regular: `μ(A) = inf {μ(U) | A ⊆ U open}` for `A` measurable;
- it is inner regular for open sets, using closed sets:
  `μ(U) = sup {μ(F) | F ⊆ U closed}` for `U` open.  -/
MeasureTheory.Measure.WeaklyRegular : {α : Type u_1} → [inst : MeasurableSpace α] → [TopologicalSpace α] → MeasureTheory.Measure α → Prop
-- Mathlib.Topology.MetricSpace.GromovHausdorff
GromovHausdorff.AuxGluingStruct.embed : {A : Type} → [inst : MetricSpace A] → (self : GromovHausdorff.AuxGluingStruct A) → A → self.Space
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.add_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  (x x' y : RingCat.Colimits.Prequotient F),
  RingCat.Colimits.Relation F x x' → RingCat.Colimits.Relation F (x.add y) (x'.add y)
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.normalizedDerivOfComplex_add : ∀ (F G : UpperHalfPlane → ℂ),
  MDiff F →
    MDiff G →
      Derivative.normalizedDerivOfComplex (F + G) =
        Derivative.normalizedDerivOfComplex F + Derivative.normalizedDerivOfComplex G
-- Mathlib.Algebra.BigOperators.ModEq
Nat.ModEq.sum : ∀ {α : Type u_1} {n : ℕ} {f g : α → ℕ} {s : Finset α},
  (∀ x ∈ s, f x ≡ g x [MOD n]) → ∑ x ∈ s, f x ≡ ∑ x ∈ s, g x [MOD n]
-- Init.Prelude
/-- Cast across a type equality. If `h : α = β` is an equality of types, and
`a : α`, then `a : β` will usually not typecheck directly, but this function
will allow you to work around this and embed `a` in type `β` as `cast h a : β`.

It is best to avoid this function if you can, because it is more complicated
to reason about terms containing casts, but if the types don't match up
definitionally sometimes there isn't anything better you can do.

For more information: [Equality](https://lean-lang.org/theorem_proving_in_lean4/quantifiers_and_equality.html#equality)
 -/
cast : {α β : Sort u} → α = β → α → β
-- Mathlib.Data.Finset.Empty
Finset.Nonempty.to_type : ∀ {α : Type u_1} {s : Finset α}, s.Nonempty → Nonempty α
-- Mathlib.Topology.Spectral.Hom
IsCompact.preimage_of_isOpen : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set β},
  IsSpectralMap f → IsCompact s → IsOpen s → IsCompact (f ⁻¹' s)
-- Mathlib.Algebra.Module.LinearMap.End
/-- **Alias** of `DistribSMul.toLinearMap`.

---

Each element of the monoid defines a linear map.

This is a stronger version of `DistribSMul.toAddMonoidHom`.  -/
DistribMulAction.toLinearMap : (R : Type u_1) →
  {S : Type u_3} →
    (M : Type u_4) →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid M] →
          [inst_2 : Module R M] → [inst_3 : DistribSMul S M] → [SMulCommClass S R M] → S → M →ₗ[R] M
-- Init.Data.UInt.Lemmas
USize.toUInt16_le : ∀ {a b : USize}, a.toUInt16 ≤ b.toUInt16 ↔ a % 65536 ≤ b % 65536
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
/-- Product of two infinite sums indexed by arbitrary types.
See also `tsum_mul_tsum_of_summable_norm` if `f` and `g` are absolutely summable.  -/
Summable.tsum_mul_tsum : ∀ {ι : Type u_1} {κ : Type u_2} {α : Type u_3} [inst : TopologicalSpace α] [T3Space α]
  [inst_2 : NonUnitalNonAssocSemiring α] [IsTopologicalSemiring α] {f : ι → α} {g : κ → α},
  Summable f →
    Summable g → (Summable fun x => f x.1 * g x.2) → (∑' (x : ι), f x) * ∑' (y : κ), g y = ∑' (z : ι × κ), f z.1 * g z.2
-- Mathlib.CategoryTheory.ConcreteCategory.Forget
/-- `HasForget₂ C D`, where `C` and `D` are both concrete categories, provides a functor
`forget₂ C D : C ⥤ D` and a proof that `forget₂ ⋙ (forget D) = forget C`.
 -/
CategoryTheory.HasForget₂ : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {FC : outParam (C → C → Type u_2)} →
      {CC : outParam (C → Type w)} →
        [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))] →
          [CategoryTheory.ConcreteCategory C FC] →
            (D : Type u_3) →
              [inst : CategoryTheory.Category.{v_2, u_3} D] →
                {FD : outParam (D → D → Type u_4)} →
                  {CD : outParam (D → Type w)} →
                    [inst_2 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] →
                      [CategoryTheory.ConcreteCategory D FD] → Type (max (max (max u_1 u_3) v_1) v_2)
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueMul.set_subsingleton : ∀ {G : Type u_1} [inst : Mul G] {A B : Finset G} {a0 b0 : G},
  UniqueMul A B a0 b0 → {ab | ab.1 ∈ A ∧ ab.2 ∈ B ∧ ab.1 * ab.2 = a0 * b0}.Subsingleton
-- Init.Data.Nat.Div.Basic
Nat.mul_sub_div : ∀ (x n p : ℕ), x < n * p → (n * p - (x + 1)) / n = p - (x / n + 1)
-- Mathlib.LinearAlgebra.Contraction
comp_dualTensorHom : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : Module.Dual R M) (n : N) (g : Module.Dual R N) (p : P),
  (dualTensorHom R N P) (g ⊗ₜ[R] p) ∘ₗ (dualTensorHom R M N) (f ⊗ₜ[R] n) = g n • (dualTensorHom R M P) (f ⊗ₜ[R] p)
-- Mathlib.Order.SuccPred.Tree
instSetLikeSubRootedTreeα : (t : RootedTree) → SetLike (SubRootedTree t) ↑t
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
/-- The covariant involution `rev : SimplexCategory ⥤ SimplexCategory` which,
via the equivalence between the simplex category and the
category of nonempty finite linearly ordered types, corresponds to
the *covariant* functor which sends a type `α` to `αᵒᵈ`.
This functor sends the object `⦋n⦌` to `⦋n⦌` and a map `f : ⦋n⦌ ⟶ ⦋m⦌`
is sent to the monotone map `(i : Fin (n + 1)) ↦ (f i.rev).rev`.  -/
SimplexCategory.rev : CategoryTheory.Functor SimplexCategory SimplexCategory
-- Mathlib.Topology.Category.Sequential
Sequential.isoEquivHomeo_symm_apply : ∀ {X Y : Sequential} (f : ↑X.toTop ≃ₜ ↑Y.toTop), Sequential.isoEquivHomeo.symm f = Sequential.isoOfHomeo f
-- Init.Data.List.Lex
List.lt_trans : ∀ {α : Type u_1} [inst : LT α] [i₁ : Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2]
  {l₁ l₂ l₃ : List α}, l₁ < l₂ → l₂ < l₃ → l₁ < l₃
-- Mathlib.Order.SymmDiff
symmDiff_compl_self : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a : α), symmDiff a aᶜ = ⊤
-- Mathlib.Algebra.Order.Group.Opposite
AddOpposite.instPreorder : {α : Type u_1} → [Preorder α] → Preorder αᵃᵒᵖ
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.homologyMapIso'_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.HomologyData) (h₂ : S₂.HomologyData),
  (CategoryTheory.ShortComplex.homologyMapIso' e h₁ h₂).inv = CategoryTheory.ShortComplex.homologyMap' e.inv h₂ h₁
-- Init.Data.UInt.Bitwise
USize.toFin_or : ∀ (a b : USize), (a ||| b).toFin = a.toFin ||| b.toFin