mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.HashMap.Lemmas
Std.HashMap.map_fst_toList_eq_keys : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  List.map Prod.fst m.toList = m.keys
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.hom_ofHom : ∀ {R : Type u} [inst : Semiring R] {X Y : Type v} [inst_1 : AddCommMonoid X] [inst_2 : Module R X]
  [inst_3 : AddCommMonoid Y] [inst_4 : Module R Y] (f : X →ₗ[R] Y), SemimoduleCat.Hom.hom (SemimoduleCat.ofHom f) = f
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
/-- For a spectral object indexed by a preorder, this is the map
`E^{n₁}(i₀ ≤ i₁ ≤ i₃ ≤ i₄) ⟶ E^{n₁}(i₀ ≤ i₂ ≤ i₃ ≤ i₄)`.  -/
CategoryTheory.Abelian.SpectralObject.mapFourδ₂Toδ₁' : {C : Type u_1} →
  {ι' : Type u_3} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Abelian C] →
        [inst_2 : Preorder ι'] →
          (X' : CategoryTheory.Abelian.SpectralObject C ι') →
            (i₀ i₁ i₂ i₃ i₄ : ι') →
              (hi₀₁ : i₀ ≤ i₁) →
                (hi₁₂ : i₁ ≤ i₂) →
                  (hi₂₃ : i₂ ≤ i₃) →
                    (hi₃₄ : i₃ ≤ i₄) →
                      (n₀ n₁ n₂ : ℤ) →
                        (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.mapFourδ₂Toδ₁'._auto_1) →
                          (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.mapFourδ₂Toδ₁'._auto_3) →
                            X'.E (CategoryTheory.homOfLE hi₀₁) (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE hi₃₄)
                                n₀ n₁ n₂ hn₁ hn₂ ⟶
                              X'.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE hi₂₃)
                                (CategoryTheory.homOfLE hi₃₄) n₀ n₁ n₂ hn₁ hn₂
-- Lean.Server.Requests
Lean.Server.RequestM.runTermElabM : {α : Type} → Lean.Server.Snapshots.Snapshot → Lean.Server.RequestT Lean.Elab.TermElabM α → Lean.Server.RequestM α
-- Mathlib.Analysis.Normed.Group.Basic
norm_div_pos_iff : ∀ {E : Type u_5} [inst : NormedGroup E] {a b : E}, 0 < ‖a / b‖ ↔ a ≠ b
-- Mathlib.Algebra.Order.Group.Finset
Multiset.toFinset_card_eq_one_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Multiset α), s.toFinset.card = 1 ↔ s.card ≠ 0 ∧ ∃ a, s = s.card • {a}
-- Init.Data.Int.DivMod.Lemmas
Int.mul_nonneg_iff_of_pos_right : ∀ {a b : ℤ}, 0 < b → (0 ≤ a * b ↔ 0 ≤ a)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.pullbackCone_fst_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : CategoryTheory.Limits.FormalCoproduct C} (f : X ⟶ Z)
  (g : Y ⟶ Z)
  (pb :
    (i : Function.Pullback f.f g.f) →
      CategoryTheory.Limits.PullbackCone (CategoryTheory.CategoryStruct.comp (f.φ (↑i).1) (CategoryTheory.eqToHom ⋯))
        (g.φ (↑i).2))
  (i : (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).pt.I),
  (CategoryTheory.Limits.FormalCoproduct.pullbackCone f g pb).fst.f i = (↑i).1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {v : β} [inst : Inhabited β],
      List.Pairwise (fun a b => ¬cmp a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l → Std.DTreeMap.Raw.Const.get! (Std.DTreeMap.Raw.Const.ofList l cmp) k' = v
-- Init.Data.Array.MapIdx
Array.getElem?_mapIdx : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {xs : Array α} {i : ℕ},
  (Array.mapIdx f xs)[i]? = Option.map (f i) xs[i]?
-- Mathlib.Analysis.Calculus.DifferentialForm.Basic
Filter.EventuallyEq.extDerivWithin_eq_of_mem : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  {ω₁ ω₂ : E → E [⋀^Fin n]→L[𝕜] F} {s : Set E} {x : E},
  ω₁ =ᶠ[nhdsWithin x s] ω₂ → x ∈ s → extDerivWithin ω₁ s x = extDerivWithin ω₂ s x
-- Init.Data.String.Slice
String.Slice.instHAppend : HAppend String String.Slice String
-- Init.Data.Int.DivMod.Lemmas
Int.eq_mul_of_ediv_eq_right : ∀ {a b c : ℤ}, b ∣ a → a / b = c → a = b * c
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.eq_C_of_minpolyX_coeff_eq_zero : ∀ {K : Type u_1} [inst : Field K] (f : RatFunc K),
  ↑((f.minpolyX ↥K⟮f⟯).coeff f.denom.natDegree) = 0 → ∃ c, f = RatFunc.C c
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.isSome_maxKey?_of_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t → t.maxKey?.isSome = true
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
/-- Negation is smooth in an additive Lie group.  -/
LieAddGroup.contMDiff_neg : ∀ {𝕜 : Type u_1} {inst : NontriviallyNormedField 𝕜} {H : Type u_2} {inst_1 : TopologicalSpace H} {E : Type u_3}
  {inst_2 : NormedAddCommGroup E} {inst_3 : NormedSpace 𝕜 E} {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} {inst_4 : AddGroup G} {inst_5 : TopologicalSpace G} {inst_6 : ChartedSpace H G}
  [self : LieAddGroup I n G], ContMDiff I I n fun a => -a
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.addEquivOp_symm_apply_coe : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring R) (b : ↥S.op), ↑(S.addEquivOp.symm b) = MulOpposite.unop ↑b
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.swap_map : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : MulOneClass M] [inst_1 : MulOneClass N]
  [inst_2 : MulOneClass M'] [inst_3 : MulOneClass N'] (f : M →* M') (g : N →* N') (x : Monoid.Coprod M N),
  (Monoid.Coprod.swap M' N') ((Monoid.Coprod.map f g) x) = (Monoid.Coprod.map g f) ((Monoid.Coprod.swap M N) x)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β], k ∉ t₂ → (t₁ ∪ t₂)[k]! = t₁[k]!
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.mkOfObjOfMapSucc_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} (obj : Fin (n + 1) → C)
  (mapSucc : (i : Fin n) → obj i.castSucc ⟶ obj i.succ) (i : Fin (n + 1)),
  (CategoryTheory.ComposableArrows.mkOfObjOfMapSucc obj mapSucc).obj i = obj i
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
MvPolynomial.coeff_rTensorAlgEquiv_monomial_tmul : ∀ {R : Type u} {N : Type v} [inst : CommSemiring R] {σ : Type u_1} {S : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : CommSemiring N] [inst_4 : Algebra R N] [inst_5 : DecidableEq σ] (e : σ →₀ ℕ) (s : S)
  (n : N) (d : σ →₀ ℕ),
  MvPolynomial.coeff d (MvPolynomial.rTensorAlgEquiv (s ⊗ₜ[R] (MvPolynomial.monomial e) n)) =
    if e = d then s ⊗ₜ[R] n else 0
-- Mathlib.Order.Interval.Set.WithBotTop
WithTop.Ioc_coe : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioc ↑a ↑b = WithTop.some '' Set.Ioc a b
-- Mathlib.LinearAlgebra.Matrix.Permutation
Equiv.Perm.permMatrix.congr_simp : ∀ {n : Type u_1} (R : Type u_2) {inst : DecidableEq n} [inst_1 : DecidableEq n] (σ σ_1 : Equiv.Perm n),
  σ = σ_1 →
    ∀ [inst_2 : Zero R] [inst_3 : One R] (a a_1 : n),
      a = a_1 → ∀ (a_2 a_3 : n), a_2 = a_3 → Equiv.Perm.permMatrix R σ a a_2 = Equiv.Perm.permMatrix R σ_1 a_1 a_3
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.mkIso'.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (e e_1 : M ≅ N) (e_e : e = e_1)
  [inst_4 : CategoryTheory.IsMonHom e.hom], CategoryTheory.Mon.mkIso' e = CategoryTheory.Mon.mkIso' e_1
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.frequently_ae_ne_zero_of_integral_ne_zero : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  ∫ᵛ (a : X), f a ∂[B; μ] ≠ 0 → ∃ᵐ (a : X) ∂μ.variation, f a ≠ 0
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.unconsImpl : {α : Type u} → {m : Type u → Type u} → [Monad m] → MLList.MLListImpl✝ m α → m (Option (α × MLList.MLListImpl✝ m α))
-- Mathlib.LinearAlgebra.BilinearForm.Isometry
LinearMap.BilinForm.Isometry.map_app : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} (f : B₁ →bᵢ B₂) (m m' : M₁), (B₂ (f m)) (f m') = (B₁ m) m'
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.bindOfArrows.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  {R : (i : ι) → CategoryTheory.Presieve (Y i)} (i : ι) {Z : C} (g : Z ⟶ Y i),
  R i g → CategoryTheory.Presieve.bindOfArrows Y f R (CategoryTheory.CategoryStruct.comp g (f i))
-- Mathlib.Analysis.Calculus.Deriv.Add
derivWithin_const_add : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜} {s : Set 𝕜} (c : F),
  derivWithin (fun x => c + f x) s x = derivWithin f s x
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.lpMeasSubgroupToLpTrim_ae_eq : ∀ {α : Type u_1} {F : Type u_2} {p : ENNReal} [inst : NormedAddCommGroup F] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} (hm : m ≤ m0) (f : ↥(MeasureTheory.lpMeasSubgroup F m p μ)),
  ↑↑(MeasureTheory.lpMeasSubgroupToLpTrim F p μ hm f) =ᵐ[μ] ↑↑↑f
-- Init.Data.UInt.Bitwise
USize.toBitVec_or : ∀ (a b : USize), (a ||| b).toBitVec = a.toBitVec ||| b.toBitVec
-- Mathlib.CategoryTheory.Limits.Cones
/-- **Alias** of `CategoryTheory.Limits.Cone.functorialityEquivalence`.

---

If `e : C ≌ D` is an equivalence of categories, then `functoriality F e.functor` induces an
equivalence between cones over `F` and cones over `F ⋙ e.functor`.
 -/
CategoryTheory.Limits.Cones.functorialityEquivalence : {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) →
              (e : C ≌ D) → CategoryTheory.Limits.Cone F ≌ CategoryTheory.Limits.Cone (F.comp e.functor)
-- Mathlib.Data.Finset.Union
/-- `disjiUnion s f h` is the set such that `a ∈ disjiUnion s f` iff `a ∈ f i` for some `i ∈ s`.
It is the same as `s.biUnion f`, but it does not require decidable equality on the type. The
hypothesis ensures that the sets are disjoint.  -/
Finset.disjiUnion : {α : Type u_1} → {β : Type u_2} → (s : Finset α) → (t : α → Finset β) → (↑s).PairwiseDisjoint t → Finset β
-- Mathlib.MeasureTheory.MeasurableSpace.Card
MeasurableSpace.self_subset_generateMeasurableRec : ∀ {α : Type u} (s : Set (Set α)) (i : Ordinal.{u_1}), s ⊆ MeasurableSpace.generateMeasurableRec s i
-- Mathlib.Algebra.Order.Ring.Defs
/-- An ordered semiring is a semiring with a partial order such that addition is monotone and
multiplication by a nonnegative number is monotone.  -/
IsOrderedRing : (R : Type u_1) → [Semiring R] → [PartialOrder R] → Prop
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.ker_eq_top_of_isEmpty : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X.Hom Y) [IsEmpty ↥X], f.ker = ⊤
-- Mathlib.Algebra.Module.LinearMap.Defs
IsLinearMap.isLinearMap_neg : ∀ {R : Type u_1} {M : Type u_8} [inst : Semiring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  IsLinearMap R fun z => -z
-- Mathlib.Analysis.Matrix.LDL
LDL.invertibleLowerInv : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {n : Type u_2} →
      [inst_1 : LinearOrder n] →
        [inst_2 : WellFoundedLT n] →
          [inst_3 : LocallyFiniteOrderBot n] →
            {S : Matrix n n 𝕜} → [inst_4 : Fintype n] → (hS : S.PosDef) → Invertible (LDL.lowerInv hS)
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.mk.sizeOf_spec : ∀ {G : Type u_6} [inst : AddGroup G] [inst_1 : SizeOf G] (toAddGroupSeminorm : AddGroupSeminorm G)
  (eq_zero_of_map_eq_zero' : ∀ (x : G), toAddGroupSeminorm.toFun x = 0 → x = 0),
  sizeOf { toAddGroupSeminorm := toAddGroupSeminorm, eq_zero_of_map_eq_zero' := eq_zero_of_map_eq_zero' } =
    1 + sizeOf toAddGroupSeminorm
-- Std.Sync.Channel
/-- A multi-producer multi-consumer FIFO channel that offers both bounded and unbounded buffering
and an asynchronous API, to switch into synchronous mode use `CloseableChannel.sync`.

Additionally `Std.CloseableChannel` can be closed if necessary, unlike `Std.Channel`.
This introduces a need for error handling in some cases, thus it is usually easier to use
`Std.Channel` if applicable.
 -/
Std.CloseableChannel : Type → Type
-- Mathlib.Topology.MetricSpace.Sequences
/-- A version of **Bolzano-Weierstrass**: in a proper metric space (e.g. $ℝ^n$),
every bounded sequence has a converging subsequence. This version assumes only
that the sequence is frequently in some bounded set.  -/
tendsto_subseq_of_frequently_bounded : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] [ProperSpace X] {s : Set X},
  Bornology.IsBounded s →
    ∀ {x : ℕ → X},
      (∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s) →
        ∃ a ∈ closure s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
-- Lean.Parser.Do
Lean.Parser.Term.letIdDeclNoBinders : Lean.Parser.Parser
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop.eq_1 : ∀ {M : Type u_2} [inst : Add M] (x : AddSubsemigroup Mᵃᵒᵖ), x.unop = { carrier := AddOpposite.op ⁻¹' ↑x, add_mem' := ⋯ }
-- Init.Grind.Lemmas
Lean.Grind.eqNDRec_heq : ∀ {α : Sort u_2} {a : α} {motive : α → Sort u_1} (v : motive a) {b : α} (h : a = b), h ▸ v ≍ v
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- A submodule of finrank 1 is spanned by any of its nonzero elements.  -/
eq_span_singleton_of_mem_of_finrank_eq_one : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {S : Submodule K V}
  {w : V}, Module.finrank K ↥S = 1 → w ∈ S → w ≠ 0 → S = K ∙ w
-- Mathlib.Analysis.Normed.Group.AddCircle
AddCircle.norm_eq' : ∀ (p : ℝ), 0 < p → ∀ {x : ℝ}, ‖↑x‖ = p * |p⁻¹ * x - ↑(round (p⁻¹ * x))|
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_add : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] (f g : P →ᴬ[R] W),
  ⇑(f + g) = ⇑f + ⇑g
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Sets of complete matches for norm/safe/unsafe rules.  -/
Aesop.ForwardRuleMatches : Type
-- Mathlib.RingTheory.Artinian.Module
IsArtinian.set_has_minimal : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [IsArtinian R M]
  (a : Set (Submodule R M)), a.Nonempty → ∃ M' ∈ a, ∀ I ∈ a, ¬I < M'
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.maxKey_modifyKey : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α} {f : β → β} {he : (Std.Internal.List.Const.modifyKey k f l).isEmpty = false},
      Std.Internal.List.maxKey (Std.Internal.List.Const.modifyKey k f l) he =
        if (Std.Internal.List.maxKey l ⋯ == k) = true then k else Std.Internal.List.maxKey l ⋯
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.univ_sum_single_apply' : ∀ {α : Type u_1} {M : Type u_8} [inst : AddCommMonoid M] [inst_1 : Fintype α] (i : α) (m : M),
  ∑ j, (fun₀ | j => m) i = m
-- Std.Async.Process
/-- Number of IPC messages sent
 -/
Std.IO.Process.ResourceUsageStats.messagesSent : Std.IO.Process.ResourceUsageStats → UInt64
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
/-- Pull an opposite subgroup back to a subgroup along `MulOpposite.op`  -/
Subgroup.unop : {G : Type u_2} → [inst : Group G] → Subgroup Gᵐᵒᵖ → Subgroup G
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.ValueGroupWithZero.mk_mul_mk : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (a b : R) (c d : ↥(ValuativeRel.posSubmonoid R)),
  ValuativeRel.ValueGroupWithZero.mk a c * ValuativeRel.ValueGroupWithZero.mk b d =
    ValuativeRel.ValueGroupWithZero.mk (a * b) (c * d)
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_le_mul_of_nonpos_right : ∀ {R : Type u} [inst : Semiring R] [inst_1 : Preorder R] {a b c : R} [ExistsAddOfLE R] [MulPosMono R] [AddRightMono R]
  [AddRightReflectLE R], b ≤ a → c ≤ 0 → a * c ≤ b * c
-- Mathlib.Data.Multiset.Count
Multiset.countP_True : ∀ {α : Type u_1} {s : Multiset α}, Multiset.countP (fun x => True) s = s.card
-- Mathlib.Topology.Algebra.UniformConvergence
instAddCommMonoidUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [AddCommMonoid β] → AddCommMonoid (UniformOnFun α β 𝔖)
-- ProofWidgets.Util
instMonadSaveCtxReaderT : {m n : Type → Type} → [MonadSaveCtx m n] → {ρ : Type} → MonadSaveCtx (ReaderT ρ m) n
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.map_add_one' : ∀ (self : CircleDeg1Lift) (x : ℝ), self.toFun (x + 1) = self.toFun x + 1
-- Mathlib.CategoryTheory.IsConnected
/-- If `J` is connected, then `Jᵒᵖ` is connected as well.  -/
CategoryTheory.isConnected_op : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsConnected J],
  CategoryTheory.IsConnected Jᵒᵖ
-- Mathlib.Data.Fin.Tuple.Curry
Function.FromTypes.uncurry_apply_succ : ∀ {n : ℕ} {p : Fin (n + 1) → Type u} {τ : Type u} (f : Function.FromTypes p τ) (args : (i : Fin (n + 1)) → p i),
  f.uncurry args = (f (args 0)).uncurry (Fin.tail args)
-- Mathlib.RingTheory.Artinian.Module
isArtinian_sup : ∀ {R : Type u_1} {P : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup P] [inst_2 : Module R P] (M₁ M₂ : Submodule R P)
  [IsArtinian R ↥M₁] [IsArtinian R ↥M₂], IsArtinian R ↥(M₁ ⊔ M₂)
-- Mathlib.Analysis.Analytic.Constructions
AnalyticOn.const_smul : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F} {s : Set E}
  {R : Type u_9} [inst_5 : NormedRing R] [inst_6 : Module R F] [IsBoundedSMul R F] [SMulCommClass 𝕜 R F] {c : R},
  AnalyticOn 𝕜 f s → AnalyticOn 𝕜 (c • f) s
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR.run.eq_2 : ∀ {α : Type u_1} (le : α → α → Bool) (a : α) (property : [a].length = 1),
  List.MergeSort.Internal.mergeSortTR.run✝ le ⟨[a], property⟩ = [a]
-- Lean.Elab.Util
Lean.Elab.MacroStackElem : Type
-- Mathlib.Topology.JacobsonSpace
JacobsonSpace.mk : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  (∀ {Z : Set X}, IsClosed Z → closure (Z ∩ closedPoints X) = Z) → JacobsonSpace X
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.of_mul_right : ∀ {R : Type u_1} [inst : Semiring R] {p q : Polynomial R} {m n : ℕ},
  q.IsMonicOfDegree n → (p * q).IsMonicOfDegree (m + n) → p.IsMonicOfDegree m
-- Std.Http.Protocol.H1.Writer
/-- Writing a connection-close body (HTTP/1.0 server, unknown length).
Raw bytes are written without chunk framing; the peer reads until the connection closes.
 -/
Std.Http.Protocol.H1.Writer.State.writingBodyClosingFrame : Std.Http.Protocol.H1.Writer.State
-- Mathlib.Data.ENat.Basic
ENat.WithBot.lt_add_one_iff : ∀ {n : WithBot ℕ∞} {m : ℕ}, n < ↑m + 1 ↔ n ≤ ↑m
-- Mathlib.Topology.Specialization
Specialization.toEquiv_ofEquiv : ∀ {α : Type u_1} (a : Specialization α), Specialization.toEquiv (Specialization.ofEquiv a) = a
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k fallback : α}, k ∉ m₂ → (m₁ \ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.AlgebraicGeometry.ColimitsOver
/-- The cocones on the `Dᵢ` are colimiting.  -/
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.isColimit : {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} →
  [inst : P.IsStableUnderBaseChange] →
    {S : AlgebraicGeometry.Scheme} →
      {J : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} J] →
          {D : CategoryTheory.Functor J (P.Over ⊤ S)} →
            {𝒰 : S.OpenCover} →
              [inst_2 : CategoryTheory.Category.{v_3, u_2} 𝒰.I₀] →
                [inst_3 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] →
                  (self : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰) →
                    (i : 𝒰.I₀) → CategoryTheory.Limits.IsColimit (self.cocone i)
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- The modified completed Riemann zeta function `Λ(s) + 1 / s + 1 / (1 - s)` is entire.  -/
differentiable_completedZeta₀ : Differentiable ℂ completedRiemannZeta₀
-- Mathlib.Analysis.Analytic.Order
analyticOrderAt_add_eq_right_of_lt : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f g : 𝕜 → E} {z₀ : 𝕜},
  analyticOrderAt g z₀ < analyticOrderAt f z₀ → analyticOrderAt (f + g) z₀ = analyticOrderAt g z₀
-- Mathlib.Topology.Order.LawsonTopology
/-- The Lawson topology on a partial order is T₁.  -/
Topology.IsLawson.toT1Space : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : TopologicalSpace α] [Topology.IsLawson α], T1Space α
-- Init.Data.String.Defs
_private.Init.Data.String.Defs.0.String.push.match_1.eq_1 : ∀ (motive : String → Char → Sort u_1) (b : ByteArray) (h : b.IsValidUTF8) (c : Char)
  (h_1 : (b : ByteArray) → (h : b.IsValidUTF8) → (c : Char) → motive { toByteArray := b, isValidUTF8 := h } c),
  (match { toByteArray := b, isValidUTF8 := h }, c with
    | { toByteArray := b, isValidUTF8 := h }, c => h_1 b h c) =
    h_1 b h c
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.ruleTac.inj : ∀ {decl decl_1 : Lean.Name}, Aesop.RuleTacDescr.ruleTac decl = Aesop.RuleTacDescr.ruleTac decl_1 → decl = decl_1
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.isAlgebraic_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : Ring S] {f : Polynomial R} [inst_2 : Algebra R S]
  (h : IsAdjoinRoot S f), f ≠ 0 → IsAlgebraic R h.root
-- Init.Data.UInt.Lemmas
USize.toBitVec_sub : ∀ {a b : USize}, (a - b).toBitVec = a.toBitVec - b.toBitVec
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.isHomeomorph : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (h : X ≃ₜ Y), IsHomeomorph ⇑h
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.denote.match_1.eq_5 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (v : Int.Internal.Linear.Var)
  (h_1 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_2 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b)) (h_3 : (a : Int.Internal.Linear.Expr) → motive a.neg)
  (h_4 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_5 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_6 : (k : ℤ) → (e : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k e))
  (h_7 : (e : Int.Internal.Linear.Expr) → (k : ℤ) → motive (e.mulR k)),
  (match Int.Internal.Linear.Expr.var v with
    | a.add b => h_1 a b
    | a.sub b => h_2 a b
    | a.neg => h_3 a
    | Int.Internal.Linear.Expr.num k => h_4 k
    | Int.Internal.Linear.Expr.var v => h_5 v
    | Int.Internal.Linear.Expr.mulL k e => h_6 k e
    | e.mulR k => h_7 e k) =
    h_5 v
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropOn_chart : ∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {x : M} {Q : (H → H) → Set H → H → Prop} [HasGroupoid M G],
  G.LocalInvariantProp G Q →
    (∀ (y : H), Q id Set.univ y) → ChartedSpace.LiftPropOn Q (↑(chartAt H x)) (chartAt H x).source