mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mapEquiv_top_eq_top : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] (f : M ≃L[R] N), (ClosedSubmodule.mapEquiv f) ⊤ = ⊤
-- Mathlib.Combinatorics.Optimization.ValuedCSP
/-- Fractional operation applied to a transposed table of values.  -/
FractionalOperation.tt : {D : Type u_1} → {m : ℕ} → {ι : Type u_3} → FractionalOperation D m → (Fin m → ι → D) → Multiset (ι → D)
-- Mathlib.RingTheory.AdicCompletion.Completeness
Submodule.powSMulQuotInclusion.congr_simp : ∀ {R : Type u_3} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {a b c : ℕ} (h : c = b + a) (N : Submodule R M),
  Submodule.powSMulQuotInclusion I M h N = Submodule.powSMulQuotInclusion I M h N
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_eq_one : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] [OrderBot α] {s : Finset β} {f : β → α} [inst_2 : One α]
  [IsBotOneClass α] (hs : s.Nonempty), s.sup' hs f = 1 ↔ ∀ i ∈ s, f i = 1
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.recF_eq : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} {β : Type u} (g : F (α ::: β) → β)
  (a : (MvQPF.P F).A) (f' : ((MvQPF.P F).drop.B a).Arrow α) (f : (MvQPF.P F).last.B a → (MvQPF.P F).W α),
  MvQPF.recF g ((MvQPF.P F).wMk a f' f) = g (MvQPF.abs ⟨a, TypeVec.splitFun f' (MvQPF.recF g ∘ f)⟩)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getD_eq_getD_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {a : α} {fallback : β a}, t.getD a fallback = (t.get? a).getD fallback
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.inv_comp_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (A : C) [inst_2 : CategoryTheory.GrpObj A],
  CategoryTheory.CategoryStruct.comp CategoryTheory.GrpObj.inv CategoryTheory.GrpObj.inv =
    CategoryTheory.CategoryStruct.id A
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.post_π_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasLimit F] (G : CategoryTheory.Functor C D)
  [inst_4 : CategoryTheory.Limits.HasLimit (F.comp G)] (j : J) {Z : D} (h : G.obj (F.obj j) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.post F G)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π (F.comp G) j) h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.limit.π F j)) h
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.carrier_inj : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L],
  Function.Injective ConjRootClass.carrier
-- Init.Data.UInt.Lemmas
UInt16.toFin.eq_1 : ∀ (x : UInt16), x.toFin = x.toBitVec.toFin
-- Batteries.Data.RunningStats
/-- Unbiased variance of running data stream (sample variance).  -/
Batteries.RunningStats.sampleVariance : Batteries.RunningStats → Float
-- Mathlib.RingTheory.Extension.Cotangent.Basis
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.pres.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type u_4}
  {P : Algebra.Generators R S ι} {σ : Type u_5} {b : Module.Basis σ S P.toExtension.Cotangent}
  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b),
  Algebra.Generators.PresentationOfFreeCotangent.Aux.pres✝ D =
    (Algebra.Generators.PresentationOfFreeCotangent.Aux.presRight✝ D).comp
      (Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D)
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.const_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α]
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv], CauSeq.const abv 0 = 0
-- Mathlib.NumberTheory.Transcendental.Liouville.LiouvilleWith
LiouvilleWith.sub_int : ∀ {p x : ℝ}, LiouvilleWith p x → ∀ (m : ℤ), LiouvilleWith p (x - ↑m)
-- Mathlib.AlgebraicGeometry.ColimitsOver
CategoryTheory.MorphismProperty.Over.pullback.congr_simp : ∀ {T : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} T] (P Q : CategoryTheory.MorphismProperty T)
  [inst_1 : Q.IsMultiplicative] {X Y : T} (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst_2 : P.HasPullbacksAlong f]
  [inst_3 : P.IsStableUnderBaseChangeAlong f] [inst_4 : Q.IsStableUnderBaseChange],
  CategoryTheory.MorphismProperty.Over.pullback P Q f = CategoryTheory.MorphismProperty.Over.pullback P Q f_1
-- Mathlib.Data.EReal.Operations
EReal.add_lt_add_right_coe : ∀ {x y : EReal}, x < y → ∀ (z : ℝ), x + ↑z < y + ↑z
-- Mathlib.Algebra.Prime.Lemmas
prime_mul_units : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {y : M} (u : Mˣ), Prime (y * ↑u) ↔ Prime y
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.isPullback_inl_inl_coprodMap : ∀ {X Y X' Y' : AlgebraicGeometry.Scheme} (f : X ⟶ X') (g : Y ⟶ Y'),
  CategoryTheory.IsPullback f CategoryTheory.Limits.coprod.inl CategoryTheory.Limits.coprod.inl
    (CategoryTheory.Limits.coprod.map f g)
-- Mathlib.Algebra.Lie.Normalizer
LieSubmodule.le_normalizer : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (N : LieSubmodule R L M), N ≤ N.normalizer
-- Init.Data.Array.Basic
/-- Removes the last element of an array. If the array is empty, then it is returned unmodified. The
modification is performed in-place when the reference to the array is unique.

Examples:
* `#[1, 2, 3].pop = #[1, 2]`
* `#["orange", "yellow"].pop = #["orange"]`
* `(#[] : Array String).pop = #[]`
 -/
Array.pop : {α : Type u} → Array α → Array α
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.w : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cocone F) {j j' : J} (f : j' ⟶ j),
  CategoryTheory.CategoryStruct.comp (F.map f) (c.ι.app j) = c.ι.app j'
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
/-- Build an isomorphism in the category `ProfiniteGrp` from
a `ContinuousMulEquiv` between `ProfiniteGrp`s.  -/
ProfiniteGrp.ContinuousMulEquiv.toProfiniteGrpIso : {X Y : ProfiniteGrp.{u_1}} → ↑X.toProfinite.toTop ≃ₜ* ↑Y.toProfinite.toTop → (X ≅ Y)
-- Init.Data.Fin.Lemmas
Fin.castSucc_lt_castSucc_iff : ∀ {n : ℕ} {a b : Fin n}, a.castSucc < b.castSucc ↔ a < b
-- Mathlib.Data.Matrix.Mul
dotProduct_zero' : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : NonUnitalNonAssocSemiring α] (v : m → α),
  (v ⬝ᵥ fun x => 0) = 0
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- Vertical composition of modifications.  -/
CategoryTheory.Oplax.OplaxTrans.Modification.vcomp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ ι : F ⟶ G} →
            CategoryTheory.Oplax.OplaxTrans.Modification η θ →
              CategoryTheory.Oplax.OplaxTrans.Modification θ ι → CategoryTheory.Oplax.OplaxTrans.Modification η ι
-- Mathlib.Data.Set.Defs
Set.instInter : {α : Type u} → Inter (Set α)
-- Init.Data.Vector.Attach
Vector.attachWith_map_val : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {p : α → Prop} {f : α → β} {xs : Vector α n} (H : ∀ a ∈ xs, p a),
  Vector.map (fun i => f ↑i) (xs.attachWith p H) = Vector.map f xs
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_dite : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] {s : Finset ι} {p : ι → Prop} [inst_1 : DecidablePred p]
  (f : (x : ι) → p x → M) (g : (x : ι) → ¬p x → M),
  (∏ x ∈ s, if hx : p x then f x hx else g x hx) = (∏ x, f ↑x ⋯) * ∏ x, g ↑x ⋯
-- Mathlib.Algebra.Group.Hom.Defs
iterate_map_add : ∀ {M : Type u_10} {F : Type u_11} [inst : Add M] [inst_1 : FunLike F M M] [AddHomClass F M M] (f : F) (n : ℕ) (x y : M),
  (⇑f)^[n] (x + y) = (⇑f)^[n] x + (⇑f)^[n] y
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.unitOfList_eq_insertManyIfNewUnit_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {l : List α},
  Std.ExtDTreeMap.Const.unitOfList l cmp = Std.ExtDTreeMap.Const.insertManyIfNewUnit ∅ l
-- Mathlib.Algebra.GroupWithZero.Associated
Prime.associated_of_dvd : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] {p q : M}, Prime p → Prime q → p ∣ q → Associated p q
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.all_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {p : (a : α) → β a → Bool}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.all p = t₂.all p
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
CliffordAlgebra.EquivEven.v_sq_scalar : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (Q : QuadraticForm R M) (m : M),
  (CliffordAlgebra.EquivEven.v Q) m * (CliffordAlgebra.EquivEven.v Q) m =
    (algebraMap R (CliffordAlgebra (CliffordAlgebra.EquivEven.Q' Q))) (Q m)
-- Mathlib.ModelTheory.FinitelyGenerated
FirstOrder.Language.Substructure.FG.of_map_embedding : ∀ {L : FirstOrder.Language} {M : Type u_1} [inst : L.Structure M] {N : Type u_2} [inst_1 : L.Structure N]
  (f : L.Embedding M N) {s : L.Substructure M}, (FirstOrder.Language.Substructure.map f.toHom s).FG → s.FG
-- Mathlib.Algebra.Category.ModuleCat.FilteredColimits
ModuleCat.FilteredColimits.colimit.congr_simp : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.SmallCategory J]
  [inst_2 : CategoryTheory.IsFiltered J] (F F_1 : CategoryTheory.Functor J (ModuleCat R)),
  F = F_1 → ModuleCat.FilteredColimits.colimit F = ModuleCat.FilteredColimits.colimit F_1
-- Mathlib.Order.Partition.Equipartition
/-- An equipartition of a finset with `n` elements into `k` parts has
`n % k` parts of size `n / k + 1`.  -/
Finpartition.IsEquipartition.card_large_parts_eq_mod : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {P : Finpartition s},
  P.IsEquipartition → {p ∈ P.parts | p.card = s.card / P.parts.card + 1}.card = s.card % P.parts.card
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.ext_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace β]
  {f g : α →ₘ[μ] β}, f = g ↔ ↑f =ᵐ[μ] ↑g
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instInhabitedOffset : Inhabited Std.Time.Nanosecond.Offset
-- Mathlib.Topology.UrysohnsLemma
/-- Urysohn's lemma: if `s` and `t` are two disjoint sets in a regular locally compact topological
space `X`, with `s` compact and `t` closed, then there exists a continuous
function `f : X → ℝ` such that

* `f` equals zero on `t`;
* `f` equals one on `s`;
* `0 ≤ f x ≤ 1` for all `x`.
 -/
exists_continuous_zero_one_of_isCompact' : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] [LocallyCompactSpace X] {s t : Set X},
  IsCompact s → IsClosed t → Disjoint s t → ∃ f, Set.EqOn (⇑f) 0 t ∧ Set.EqOn (⇑f) 1 s ∧ ∀ (x : X), f x ∈ Set.Icc 0 1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.ι_mul_ι_add_swap_of_isOrtho : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {a b : M},
  QuadraticMap.IsOrtho Q a b →
    (CliffordAlgebra.ι Q) a * (CliffordAlgebra.ι Q) b + (CliffordAlgebra.ι Q) b * (CliffordAlgebra.ι Q) a = 0
-- Mathlib.Data.Nat.ModEq
/-- Modular equality. `n.ModEq a b`, or `a ≡ b [MOD n]`, means that `a % n = b % n`.  -/
Nat.ModEq : ℕ → ℕ → ℕ → Prop
-- Init.Data.Iterators.Consumers.Loop
/-- Returns `true` if the monadic predicate `p` returns `true` for
any element emitted by the iterator `it`.

`O(|xs|)`. Short-circuits upon encountering the first match. The elements in `it` are
examined in order of iteration.

This variant terminates after finitely many steps and requires a proof that the iterator is
finite. If such a proof is not available, consider using `Iter.anyM`.
 -/
Std.Iter.Total.anyM : {α β : Type w} →
  {m : Type → Type w'} →
    [Monad m] →
      [inst : Std.Iterator α Id β] →
        [Std.IteratorLoop α Id m] → [Std.Iterators.Finite α Id] → (β → m Bool) → Std.Iter.Total β → m Bool
-- Batteries.Data.List.Lemmas
List.IsChain.imp : ∀ {α : Type u_1} {R S : α → α → Prop} {l : List α}, (∀ ⦃a b : α⦄, R a b → S a b) → List.IsChain R l → List.IsChain S l
-- Mathlib.RingTheory.IntegralClosure.IntegrallyClosed
IsIntegrallyClosed.of_isIntegrallyClosedIn : ∀ (R : Type u_4) (K : Type u_5) [inst : CommRing R] [inst_1 : Field K] [inst_2 : Algebra R K] [FaithfulSMul R K]
  [IsIntegrallyClosedIn R K], IsIntegrallyClosed R
-- Mathlib.Lean.Expr.Basic
/-- Update the level parameters of a `ConstantInfo`.  -/
Lean.ConstantInfo.updateLevelParams : Lean.ConstantInfo → List Lean.Name → Lean.ConstantInfo
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.normConfig_zetaDelta : Lean.Meta.Grind.normConfig✝.zetaDelta = true
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.instCountableOrCountablyGeneratedOfCountable : ∀ {β : Type u_2} {α : Type u_3} [h1 : Countable α] [inst : MeasurableSpace β],
  MeasurableSpace.CountableOrCountablyGenerated α β
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
ContinuousAlternatingMap.ofSubsingletonLIE_symm_apply : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] [inst_6 : Subsingleton ι] (i : ι) (a : E [⋀^ι]→L[𝕜] F),
  (ContinuousAlternatingMap.ofSubsingletonLIE i).symm a = (ContinuousAlternatingMap.ofSubsingleton 𝕜 E F i).symm a
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.rightUnitor_inv_iso_hom : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Pith B} (x : a ⟶ b),
  (CategoryTheory.Bicategory.rightUnitor x).inv.iso.hom = (CategoryTheory.Bicategory.rightUnitor x.of).inv
-- Mathlib.Algebra.Group.Subgroup.Even
Submonoid.coe_square : ∀ {M : Type u_1} [inst : CommMonoid M], ↑(Submonoid.square M) = {s | IsSquare s}
-- Mathlib.Algebra.Homology.EulerCharacteristic
ComplexShape.eulerCharSignsDownNat_χ : ∀ (n : ℕ), ComplexShape.EulerCharSigns.χ (ComplexShape.down ℕ) n = (-1) ^ n
-- Mathlib.Topology.Algebra.Module.Spaces.CompactConvergenceCLM
/-- **Alias** of `ContinuousLinearMap.precompCompactConvergenceCLM`.

---

Specialization of `ContinuousLinearMap.precomp_uniformConvergenceCLM` to compact
convergence.  -/
precomp_compactConvergenceCLM : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    {𝕜₃ : Type u_3} →
      [inst : NormedField 𝕜₁] →
        [inst_1 : NormedField 𝕜₂] →
          [inst_2 : NormedField 𝕜₃] →
            {σ : 𝕜₁ →+* 𝕜₂} →
              {τ : 𝕜₂ →+* 𝕜₃} →
                {ρ : 𝕜₁ →+* 𝕜₃} →
                  [RingHomCompTriple σ τ ρ] →
                    {E : Type u_4} →
                      {F : Type u_5} →
                        (G : Type u_6) →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : Module 𝕜₁ E] →
                              [inst_6 : AddCommGroup F] →
                                [inst_7 : Module 𝕜₂ F] →
                                  [inst_8 : AddCommGroup G] →
                                    [inst_9 : Module 𝕜₃ G] →
                                      [inst_10 : TopologicalSpace E] →
                                        [inst_11 : TopologicalSpace F] →
                                          [inst_12 : TopologicalSpace G] →
                                            [inst_13 : IsTopologicalAddGroup G] →
                                              [inst_14 : ContinuousConstSMul 𝕜₃ G] →
                                                (E →SL[σ] F) →
                                                  CompactConvergenceCLM τ F G →L[𝕜₃] CompactConvergenceCLM ρ E G
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.snd_natCast : ∀ {R : Type u} {M : Type v} [inst : AddMonoidWithOne R] [inst_1 : AddMonoid M] (n : ℕ), (↑n).snd = 0
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.ISize.toBitVec_cond : ∀ {c : Bool} {t e : ISize}, (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_insert_of_isEmpty : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t.isEmpty = true → ∀ {fallback : α}, (t.insert k v).minKeyD fallback = k
-- Std.Data.HashMap.Lemmas
Std.HashMap.isEmpty_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {v : β}, (m.insertIfNew k v).isEmpty = false
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.insertListConst.eq_1 : ∀ {α : Type u} {β : Type v} [inst : BEq α] (l : List ((_ : α) × β)) (toInsert : List (α × β)),
  Std.Internal.List.insertListConst l toInsert =
    Std.Internal.List.insertList l (List.map Std.Internal.List.Prod.toSigma toInsert)
-- Mathlib.Analysis.Calculus.FDeriv.Comp
fderivWithin_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {f : E → F} (x : E) {s : Set E} {g : F → G} {t : Set F},
  DifferentiableWithinAt 𝕜 g t (f x) →
    DifferentiableWithinAt 𝕜 f s x →
      Set.MapsTo f s t →
        UniqueDiffWithinAt 𝕜 s x → fderivWithin 𝕜 (g ∘ f) s x = fderivWithin 𝕜 g t (f x) ∘SL fderivWithin 𝕜 f s x
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
isGLB_ciInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α},
  BddBelow (Set.range f) → IsGLB (Set.range f) (⨅ i, f i)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.tensorRightMopIso_inv_app_unmop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : C)
  (X_1 : Cᴹᵒᵖ),
  ((CategoryTheory.MonoidalOpposite.tensorRightMopIso X).inv.app X_1).unmop =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X X_1.unmop)
-- Mathlib.Data.List.OffDiag
List.offDiag_cons_perm : ∀ {α : Type u_1} (a : α) (l : List α),
  (a :: l).offDiag.Perm (List.map (fun x => (a, x)) l ++ List.map (fun x => (x, a)) l ++ l.offDiag)
-- Mathlib.Topology.Algebra.Group.Basic
/-- Conjugation is jointly continuous on `G × G` when both `add` and `neg` are continuous.  -/
IsTopologicalAddGroup.continuous_addConj_prod : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Neg G] [inst_2 : Add G] [ContinuousAdd G] [ContinuousNeg G],
  Continuous fun g => g.1 + g.2 + -g.1
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- Construct a wide pullback cone from the projections.  -/
CategoryTheory.Limits.WidePullbackCone.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_1} →
      {X : C} →
        {Y : ι → C} →
          {f : (i : ι) → Y i ⟶ X} →
            {W : C} →
              (b : W ⟶ X) →
                (π : (i : ι) → W ⟶ Y i) →
                  (∀ (i : ι), CategoryTheory.CategoryStruct.comp (π i) (f i) = b) →
                    CategoryTheory.Limits.WidePullbackCone f
-- Mathlib.Analysis.Fourier.FourierTransform
VectorFourier.fourierIntegral_add : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module 𝕜 W] {E : Type u_4}
  [inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace ℂ E] [inst_8 : TopologicalSpace 𝕜] [IsTopologicalRing 𝕜]
  [inst_10 : TopologicalSpace V] [BorelSpace V] [inst_12 : TopologicalSpace W] {e : AddChar 𝕜 Circle}
  {μ : MeasureTheory.Measure V} {L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜},
  Continuous ⇑e →
    (Continuous fun p => (L p.1) p.2) →
      ∀ {f g : V → E},
        MeasureTheory.Integrable f μ →
          MeasureTheory.Integrable g μ →
            VectorFourier.fourierIntegral e μ L (f + g) =
              VectorFourier.fourierIntegral e μ L f + VectorFourier.fourierIntegral e μ L g
-- Mathlib.Algebra.Category.Ring.Under.Limits
/-- The fork on `𝟙 ⊗[R] f` and `𝟙 ⊗[R] g` given by `S ⊗[R] eq(f, g)`.  -/
CommRingCat.Under.tensorProdEqualizer : {R S : CommRingCat} →
  [inst : Algebra ↑R ↑S] →
    {A B : CategoryTheory.Under R} →
      (f g : A ⟶ B) → CategoryTheory.Limits.Fork ((R.tensorProd S).map f) ((R.tensorProd S).map g)
-- Mathlib.Order.Filter.Basic
Filter.frequently_or_distrib_left : ∀ {α : Type u} {f : Filter α} [f.NeBot] {p : Prop} {q : α → Prop}, (∃ᶠ (x : α) in f, p ∨ q x) ↔ p ∨ ∃ᶠ (x : α) in f, q x
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.Const.alter : {α : Type u} →
  [BEq α] →
    {β : Type v} →
      α →
        (Option β → Option β) →
          (Std.DHashMap.Internal.AssocList α fun x => β) → Std.DHashMap.Internal.AssocList α fun x => β
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.natCast_lt_toENat : ∀ {c : Cardinal.{u}} {n : ℕ}, ↑n < Cardinal.toENat c ↔ ↑n < c
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_le_natDegree : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.degree ≤ ↑p.natDegree
-- Mathlib.Topology.Algebra.Module.Multilinear.Topology
ContinuousMultilinearMap.instContinuousEvalConstForall : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {F : Type u_4} [inst : NormedField 𝕜]
  [inst_1 : (i : ι) → TopologicalSpace (E i)] [inst_2 : (i : ι) → AddCommGroup (E i)]
  [inst_3 : (i : ι) → Module 𝕜 (E i)] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F] [inst_6 : TopologicalSpace F]
  [inst_7 : IsTopologicalAddGroup F] [∀ (i : ι), ContinuousSMul 𝕜 (E i)],
  ContinuousEvalConst (ContinuousMultilinearMap 𝕜 E F) ((i : ι) → E i) F
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- The cocone `Φ.presheafFiberCocone P` is a colimit.  -/
CategoryTheory.GrothendieckTopology.Point.isColimitPresheafFiberCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            [inst_2 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
              (P : CategoryTheory.Functor Cᵒᵖ A) → CategoryTheory.Limits.IsColimit (Φ.presheafFiberCocone P)
-- Mathlib.GroupTheory.Divisible
/-- If `f : A → B` is a surjective homomorphism and `A` is `α`-rootable, then `B` is also `α`-rootable.
 -/
Function.Surjective.rootableBy : {A : Type u_1} →
  {B : Type u_2} →
    {α : Type u_3} →
      [inst : Zero α] →
        [inst_1 : Monoid A] →
          [inst_2 : Monoid B] →
            [inst_3 : Pow A α] →
              [inst_4 : Pow B α] →
                [RootableBy A α] →
                  (f : A → B) → Function.Surjective f → (∀ (a : A) (n : α), f (a ^ n) = f a ^ n) → RootableBy B α
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.ofHom_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C) {X Y : C}
  (f : X ⟶ Y) [inst_1 : W.ContainsIdentities],
  (CategoryTheory.MorphismProperty.RightFraction.ofHom W f).s = CategoryTheory.CategoryStruct.id X
-- Lean.Widget.UserWidget
Lean.Widget.instFromJsonWidgetSource : Lean.FromJson Lean.Widget.WidgetSource
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_sub : ∀ {x : NNReal}, x ≠ 0 → ∀ (y z : ℝ), x ^ (y - z) = x ^ y / x ^ z