mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.isContinuous_of_preservesOneHypercovers : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (J : CategoryTheory.GrothendieckTopology C)
  (K : CategoryTheory.GrothendieckTopology D) [F.PreservesOneHypercovers J K] [J.IsGeneratedByOneHypercovers],
  F.IsContinuous J K
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.completion_add : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  (f g : NormedAddGroupHom G H), (f + g).completion = f.completion + g.completion
-- Mathlib.Geometry.Euclidean.Volume.Measure
/-- `μHE[0]` and `μH[0]` are equal.  -/
MeasureTheory.Measure.euclideanHausdorffMeasure_zero : ∀ {X : Type u_1} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X],
  MeasureTheory.Measure.euclideanHausdorffMeasure 0 = MeasureTheory.Measure.hausdorffMeasure 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue?_modifyKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getValue? k' (Std.Internal.List.Const.modifyKey k f l) =
      if (k == k') = true then Option.map f (Std.Internal.List.getValue? k l) else Std.Internal.List.getValue? k' l
-- Mathlib.LinearAlgebra.Matrix.AbsoluteValue
Matrix.det_sum_smul_le : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [Nontrivial R] [inst_2 : CommRing S] [inst_3 : LinearOrder S]
  [IsStrictOrderedRing S] {n : Type u_3} [inst_5 : Fintype n] [inst_6 : DecidableEq n] {ι : Type u_4} (s : Finset ι)
  {c : ι → R} {A : ι → Matrix n n R} {abv : AbsoluteValue R S} {x : S},
  (∀ (k : ι) (i j : n), abv (A k i j) ≤ x) →
    ∀ {y : S},
      (∀ (k : ι), abv (c k) ≤ y) →
        abv (∑ k ∈ s, c k • A k).det ≤ (Fintype.card n).factorial • (s.card • y * x) ^ Fintype.card n
-- Std.Sync.Mutex
/-- Attempts to lock a `BaseMutex`. If the mutex is not available return `false`, otherwise lock it and
return `true`.

This function does not block.

The current thread must not have already locked the mutex.
Reentrant locking is undefined behavior (inherited from the C++ implementation).
If this is unavoidable in your code, consider using `BaseRecursiveMutex`.
 -/
Std.BaseMutex.tryLock : Std.BaseMutex → BaseIO Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.limitBiconeOfUnique_bicone_pt : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_2 : Unique J] (f : J → C),
  (CategoryTheory.Limits.limitBiconeOfUnique f).bicone.pt = f default
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrixAux_eq : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} [inst_3 : Fintype n] [inst_4 : DecidableEq n] (b : Module.Basis n R₁ M₁)
  (B : LinearMap.BilinForm R₁ M₁), (LinearMap.BilinForm.toMatrixAux ⇑b) B = (LinearMap.BilinForm.toMatrix b) B
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Precylinder.map_I : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (P : HomotopicalAlgebra.Precylinder X) {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] (F : CategoryTheory.Functor C D), (P.map F).I = F.obj P.I
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {k : α},
  (t₁ ∩ t₂).get! k = if k ∈ t₂ then t₁.get! k else default
-- Mathlib.Order.Ideal
/-- There is a bottom ideal when `P` has a bottom element.  -/
Order.Ideal.instOrderBot : {P : Type u_1} → [inst : Preorder P] → [OrderBot P] → OrderBot (Order.Ideal P)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonDefinitionParams : Lean.ToJson Lean.Lsp.DefinitionParams
-- Std.Data.HashSet.Lemmas
Std.HashSet.all_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulHashable α] [EquivBEq α] {p : α → Bool},
  m.toList.all p = m.all p
-- Mathlib.Algebra.Group.Action.Pi
Pi.isCentralVAdd : ∀ {ι : Type u_1} {M : Type u_2} {α : ι → Type u_4} [inst : (i : ι) → VAdd M (α i)] [inst_1 : (i : ι) → VAdd Mᵃᵒᵖ (α i)]
  [∀ (i : ι), IsCentralVAdd M (α i)], IsCentralVAdd M ((i : ι) → α i)
-- Mathlib.Data.Set.Card
Set.Finite.exists_bijOn_of_encard_eq : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} [Nonempty β],
  s.Finite → s.encard = t.encard → ∃ f, Set.BijOn f s t
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The continuous homomorphism given by addition.  -/
ContinuousAddMonoidHom.add : (E : Type u_6) → [inst : AddCommMonoid E] → [inst_1 : TopologicalSpace E] → [ContinuousAdd E] → E × E →ₜ+ E
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.algebraMap_right_injective : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] {S : Type u_3} [inst_1 : CommSemiring R]
  [inst_2 : Ring S] [inst_3 : Algebra R S] (v : Valuation S Γ₀),
  Function.Injective ⇑(algebraMap R S) → Function.Injective ⇑(algebraMap R (WithVal v))
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Left.one_lt_mul_of_left`. -/
one_lt_mul_of_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [IsBotOneClass α] [MulLeftMono α] {a : α},
  1 < a → ∀ (b : α), 1 < a * b
-- Std.Http.Data.Body.Any
Std.Http.Body.instAny : Std.Http.Body Std.Http.Body.Any
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.prod_eq_pow_single : ∀ {M : Type u_5} [inst : CommMonoid M] {s : Multiset M} [inst_1 : DecidableEq M] (a : M),
  (∀ (a' : M), a' ≠ a → a' ∈ s → a' = 1) → s.prod = a ^ Multiset.count a s
-- Lean.Elab.Tactic.RCases
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.processConstructor.match_3.eq_3 : ∀ (motive : List Lean.Elab.Tactic.RCases.RCasesPatt → Sort u_1) (ps : List Lean.Elab.Tactic.RCases.RCasesPatt)
  (h_1 : Unit → motive []) (h_2 : (p : Lean.Elab.Tactic.RCases.RCasesPatt) → motive [p])
  (h_3 : (ps : List Lean.Elab.Tactic.RCases.RCasesPatt) → motive ps),
  (ps = [] → False) →
    (∀ (p : Lean.Elab.Tactic.RCases.RCasesPatt), ps = [p] → False) →
      (match ps with
        | [] => h_1 ()
        | [p] => h_2 p
        | ps => h_3 ps) =
        h_3 ps
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Colimit cocones on `F` are unique up to isomorphism.  -/
CategoryTheory.Limits.IsColimit.uniqueUpToIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          {s t : CategoryTheory.Limits.Cocone F} →
            CategoryTheory.Limits.IsColimit s → CategoryTheory.Limits.IsColimit t → (s ≅ t)
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ιMulti_apply : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ}
  (v : Fin n → M), (ExteriorAlgebra.ιMulti R n) v = (List.ofFn fun i => (ExteriorAlgebra.ι R) (v i)).prod
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedAddCommGroup.toAddCommGroup : {E : Type u_8} → [self : SeminormedAddCommGroup E] → AddCommGroup E
-- Mathlib.CategoryTheory.Enriched.Basic
CategoryTheory.EnrichedCategory.id_comp : ∀ {V : Type v} {inst : CategoryTheory.Category.{w, v} V} {inst_1 : CategoryTheory.MonoidalCategory V} {C : Type u₁}
  [self : CategoryTheory.EnrichedCategory V C] (X Y : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.leftUnitor (X ⟶[V] Y)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.EnrichedCategory.id X) (X ⟶[V] Y))
        (CategoryTheory.EnrichedCategory.comp X X Y)) =
    CategoryTheory.CategoryStruct.id (X ⟶[V] Y)
-- Mathlib.Data.Multiset.Powerset
Multiset.powerset_zero : ∀ {α : Type u_1}, Multiset.powerset 0 = {0}
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.p_opcyclesMap : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {K L : HomologicalComplex C c} (φ : K ⟶ L) (i : ι) [inst_2 : K.HasHomology i]
  [inst_3 : L.HasHomology i],
  CategoryTheory.CategoryStruct.comp (K.pOpcycles i) (HomologicalComplex.opcyclesMap φ i) =
    CategoryTheory.CategoryStruct.comp (φ.f i) (L.pOpcycles i)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_X_sub_C_pow : ∀ {R : Type u} [inst : CommRing R] (c : R) (m : ℕ),
  Polynomial.derivative ((Polynomial.X - Polynomial.C c) ^ m) =
    Polynomial.C ↑m * (Polynomial.X - Polynomial.C c) ^ (m - 1)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
Bundle.Trivialization.localFrameCoeff_apply_of_notMem_baseSet : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V] {ι : Type u_7}
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_14 : MemTrivializationAtlas e] (b : Module.Basis ι 𝕜 F)
  [inst_15 : ContMDiffVectorBundle 1 F V I] {x : M},
  x ∉ e.baseSet → ∀ (i : ι), Bundle.Trivialization.localFrameCoeff I e b i x = 0
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C.eq_4 : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  Polynomial.Chebyshev.C R (Int.negSucc n) =
    Polynomial.X * Polynomial.Chebyshev.C R (-↑n) - Polynomial.Chebyshev.C R (-↑n + 1)
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.mapCompIso.eq_1 : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  {F G H : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} (α : F ⟶ G) (β : G ⟶ H),
  CategoryTheory.Pseudofunctor.Grothendieck.mapCompIso α β =
    CategoryTheory.NatIso.ofComponents (fun x => CategoryTheory.eqToIso ⋯) ⋯
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
AlgebraicTopology.DoldKan.PInfty_comp_map_mono_eq_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) {n : ℕ} {Δ' : SimplexCategory} (i : Δ' ⟶ { len := n })
  [hi : CategoryTheory.Mono i],
  Δ'.len ≠ n →
    ¬AlgebraicTopology.DoldKan.Isδ₀ i →
      CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.PInfty.f n) (X.map i.op) = 0
-- Mathlib.RingTheory.MvPowerSeries.GaussNorm
MvPowerSeries.antidiagonal_dominant : ∀ {R : Type u_1} {σ : Type u_2} (v : R → ℝ) [inst : Ring R] [inst_1 : DecidableEq σ] (f g : MvPowerSeries σ R)
  (i j : σ →₀ ℕ),
  IsNonarchimedean v →
    (∀ (a b : R), v (a * b) = v a * v b) →
      (∀ (a : R), v a = v (-a)) →
        (∀ p ∈ Finset.HasAntidiagonal.antidiagonal (i + j),
            p ≠ (i, j) →
              v ((MvPowerSeries.coeff p.1) f * (MvPowerSeries.coeff p.2) g) <
                v ((MvPowerSeries.coeff i) f) * v ((MvPowerSeries.coeff j) g)) →
          v ((MvPowerSeries.coeff (i + j)) (f * g)) = v ((MvPowerSeries.coeff i) f * (MvPowerSeries.coeff j) g)
-- Mathlib.NumberTheory.Divisors
Int.divisorsAntidiagonal_three : Int.divisorsAntidiag 3 = {(1, 3), (3, 1), (-1, -3), (-3, -1)}
-- Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
MeasureTheory.eLpNorm'_le_eLpNormEssSup : ∀ {α : Type u_1} {ε : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ε}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {q : ℝ},
  0 < q → ∀ [MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.eLpNorm' f q μ ≤ MeasureTheory.eLpNormEssSup f μ
-- Mathlib.Algebra.GroupWithZero.Basic
/-- **Alias** of `pow_ne_zero_iff`. -/
IsReduced.pow_ne_zero_iff : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} {n : ℕ} [IsReduced M₀], n ≠ 0 → (a ^ n ≠ 0 ↔ a ≠ 0)
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
/-- The morphisms `DescentData.hom`, as isomorphisms.  -/
CategoryTheory.Pseudofunctor.DescentData.iso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} →
      {ι : Type t} →
        {S : C} →
          {X : ι → C} →
            {f : (i : ι) → X i ⟶ S} →
              (D : F.DescentData f) →
                ⦃Y : C⦄ →
                  (q : Y ⟶ S) →
                    ⦃i₁ i₂ : ι⦄ →
                      (f₁ : Y ⟶ X i₁) →
                        (f₂ : Y ⟶ X i₂) →
                          autoParam (CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q)
                              CategoryTheory.Pseudofunctor.DescentData.iso._auto_1 →
                            autoParam (CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q)
                                CategoryTheory.Pseudofunctor.DescentData.iso._auto_3 →
                              ((F.map f₁.op.toLoc).toFunctor.obj (D.obj i₁) ≅
                                (F.map f₂.op.toLoc).toFunctor.obj (D.obj i₂))
-- Init.Data.Iterators.Basic
Std.Iter.internalState_toIterM : ∀ {α β : Type u_1} (it : Std.Iter β), it.toIterM.internalState = it.internalState
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncateFun_one : ∀ (p n : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)], WittVector.truncateFun n 1 = 1
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁_X₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i₀ i₁ i₂ i₃ : ι} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂) (f₃ : i₂ ⟶ i₃)
  (f₁₂ : i₀ ⟶ i₂) (f₂₃ : i₁ ⟶ i₃) (h₁₂ : CategoryTheory.CategoryStruct.comp f₁ f₂ = f₁₂)
  (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.shortComplexOpcyclesThreeδ₂Toδ₁._auto_3),
  (X.shortComplexOpcyclesThreeδ₂Toδ₁ f₁ f₂ f₃ f₁₂ f₂₃ h₁₂ h₂₃ n₀ n₁ n₂ hn₁ hn₂).X₁ = X.opcycles f₁ f₂₃ n₁
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
IsDedekindDomain.idealFactorsFunOfQuotHom.eq_1 : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : IsDedekindDomain A] {I : Ideal R}
  {J : Ideal A} {f : R ⧸ I →+* A ⧸ J} (hf : Function.Surjective ⇑f),
  IsDedekindDomain.idealFactorsFunOfQuotHom hf =
    { toFun := fun X => ⟨Ideal.comap (Ideal.Quotient.mk J) (Ideal.map f (Ideal.map (Ideal.Quotient.mk I) ↑X)), ⋯⟩,
      monotone' := ⋯ }
-- Mathlib.Topology.Instances.ZMultiples
/-- Under the coercion from `ℤ` to `ℝ`, inverse images of compact sets are finite.  -/
Int.tendsto_coe_cofinite : Filter.Tendsto Int.cast Filter.cofinite (Filter.cocompact ℝ)
-- Std.Sync.CancellationContext
/-- Next available ID
 -/
Std.CancellationContext.State.id : Std.CancellationContext.State → UInt64
-- Mathlib.Logic.Equiv.Defs
Equiv.equivCongr_refl : ∀ {α : Sort u_1} {β : Sort u_2}, (Equiv.refl α).equivCongr (Equiv.refl β) = Equiv.refl (α ≃ β)
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.noSibling_deleteMin : ∀ {α : Type u_1} {le : α → α → Bool} {a : α} {s' s : Batteries.PairingHeapImp.Heap α},
  Batteries.PairingHeapImp.Heap.deleteMin le s = some (a, s') → s'.NoSibling
-- Mathlib.Combinatorics.SimpleGraph.Matching
_private.Mathlib.Combinatorics.SimpleGraph.Matching.0.SimpleGraph.IsCycles.reachable_sdiff_toSubgraph_spanningCoe_aux : ∀ {V : Type u_1} {G : SimpleGraph V} [Finite V] {v w : V},
  G.IsCycles → ∀ (p : G.Walk v w), p.IsPath → (G \ p.toSubgraph.spanningCoe).Reachable w v
-- Lean.Elab.InfoTree.Main
_private.Lean.Elab.InfoTree.Main.0.Lean.Elab.formatStxRange : Lean.Elab.ContextInfo → Lean.Syntax → Std.Format
-- Mathlib.Algebra.Order.Ring.Abs
sq_eq_sq_iff_abs_eq_abs : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a b : α), a ^ 2 = b ^ 2 ↔ |a| = |b|
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.instNonUnitalNormedRing : {α : Type u} →
  [inst : TopologicalSpace α] →
    {R : Type u_1} → [inst_1 : NonUnitalNormedRing R] → NonUnitalNormedRing (BoundedContinuousFunction α R)
-- Mathlib.Algebra.Group.Defs
Semigroup.ext_iff : ∀ {G : Type u} {x y : Semigroup G}, x = y ↔ Mul.mul = Mul.mul
-- Mathlib.Topology.Instances.NNReal.Lemmas
/-- `Real.toNNReal` bundled as a continuous map for convenience.  -/
ContinuousMap.realToNNReal : C(ℝ, NNReal)
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_id : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (x : 𝕜) (s : Set 𝕜), HasDerivWithinAt id 1 s x
-- Mathlib.Topology.Separation.Regular
hasBasis_nhds_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] (x : X), (nhds x).HasBasis (fun s => s ∈ nhds x) closure
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.combine : Lean.Meta.Grind.Arith.Linear.IneqCnstr →
  Lean.Meta.Grind.Arith.Linear.IneqCnstr → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.monic_denom : ∀ {K : Type u} [inst : Field K] (x : RatFunc K), x.denom.Monic
-- Std.Time.Format.Modifier
Std.Time.Modifier.X.injEq : ∀ (presentation presentation_1 : Std.Time.OffsetX),
  (Std.Time.Modifier.X presentation = Std.Time.Modifier.X presentation_1) = (presentation = presentation_1)
-- Std.Data.DTreeMap.Raw.Lemmas
_private.Std.Data.DTreeMap.Raw.Lemmas.0.Break.runK.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
RootPairing.weylGroup.eq_1 : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N),
  P.weylGroup = Subgroup.closure (Set.range (RootPairing.Equiv.reflection P))
-- Mathlib.Algebra.Order.Monoid.Prod
Prod.Lex.isOrderedAddMonoid : ∀ {α : Type u_1} {β : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [AddLeftStrictMono α]
  [inst_3 : AddCommMonoid β] [inst_4 : Preorder β] [IsOrderedAddMonoid β], IsOrderedAddMonoid (Lex (α × β))
-- Mathlib.Topology.Algebra.Support
locallyFinite_mulSupport_iff : ∀ {X : Type u_1} {M : Type u_7} {ι : Type u_9} [inst : TopologicalSpace X] [inst_1 : One M] {f : ι → X → M},
  (LocallyFinite fun i => Function.mulSupport (f i)) ↔ LocallyFinite fun i => mulTSupport (f i)
-- Mathlib.Tactic.DepRewrite
/-- Apply `rewrite!` to the goal.  -/
Mathlib.Tactic.DepRewrite.depRewriteTarget : Lean.Syntax → Bool → optParam Mathlib.Tactic.DepRewrite.Config { } → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNormEssSup_congr_ae : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] {f g : α → ε},
  f =ᵐ[μ] g → MeasureTheory.eLpNormEssSup f μ = MeasureTheory.eLpNormEssSup g μ
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_roc_eq_some : ∀ {m n i : ℕ}, i < n - m → (m<...=n).toArray[i]? = some (m + 1 + i)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospan_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z),
  (CategoryTheory.Limits.cospan f g).obj CategoryTheory.Limits.WalkingCospan.left = X
-- Init.Data.Function
Function.HasRightInverse.surjective : ∀ {α : Sort u_1} {β : Sort u_2} {f : α → β}, Function.HasRightInverse f → Function.Surjective f
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.IsShortNF.a₃ : ∀ {R : Type u_1} {inst : CommRing R} {W : WeierstrassCurve R} [self : W.IsShortNF], W.a₃ = 0
-- Mathlib.NumberTheory.MulChar.Basic
/-- Evaluation of the trivial character  -/
MulChar.one_apply_coe : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (a : Rˣ), 1 ↑a = 1
-- Init.WF
PSigma.RevLex.left : ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} {a₁ a₂ : α} (b : β),
  r a₁ a₂ → PSigma.RevLex r s ⟨a₁, b⟩ ⟨a₂, b⟩
-- Mathlib.Data.ENNReal.Operations
ENNReal.le_iInf_add_iInf : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} {κ : Sort u_2} {g : κ → ENNReal},
  (∀ (i : ι) (j : κ), a ≤ f i + g j) → a ≤ iInf f + iInf g
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Reachable.elim : ∀ {V : Type u} {G : SimpleGraph V} {p : Prop} {u v : V}, G.Reachable u v → (∀ (a : G.Walk u v), p) → p
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.min!_le_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, t.contains k = true → (cmp t.min! k).isLE = true
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR.eq_1 : ∀ {α : Type u_1} (l : List α) (le : α → α → Bool),
  List.MergeSort.Internal.mergeSortTR l le = List.MergeSort.Internal.mergeSortTR.run✝ le ⟨l, ⋯⟩
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.dvd_gcd : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] {a b c : R},
  c ∣ a → c ∣ b → c ∣ EuclideanDomain.gcd a b
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.closure_singleton_zero : ∀ {R : Type u} [inst : NonAssocRing R], Subring.closure {0} = ⊥
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.uniformSpace : {E : Type u_3} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {Ω : TopologicalSpace.Opens E} →
        {F : Type u_4} →
          [inst_2 : NormedAddCommGroup F] → [inst_3 : NormedSpace ℝ F] → {n : ℕ∞} → UniformSpace (TestFunction Ω F n)
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.Hom.app_smul : ∀ {X : AlgebraicGeometry.Scheme} {M N : X.Modules} {U : X.Opens} (φ : M ⟶ N) (r : ↑(X.presheaf.obj (Opposite.op U)))
  (x : ↑(M.presheaf.obj (Opposite.op U))),
  (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app φ U)) (r • x) =
    r • (CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.Modules.Hom.app φ U)) x
-- Mathlib.Analysis.SpecificLimits.Normed
NormedAddCommGroup.cauchy_series_of_le_geometric'' : ∀ {α : Type u_1} [inst : SeminormedAddCommGroup α] {C : ℝ} {u : ℕ → α} {N : ℕ} {r : ℝ},
  0 < r → r < 1 → (∀ n ≥ N, ‖u n‖ ≤ C * r ^ n) → CauchySeq fun n => ∑ k ∈ Finset.range (n + 1), u k
-- Mathlib.Data.Num.ZNum
ZNum.pred.eq_3 : ∀ (a : PosNum), (ZNum.neg a).pred = ZNum.neg a.succ
-- Mathlib.Algebra.Module.Injective
Module.Injective.mk : ∀ {R : Type u} [inst : Ring R] {Q : Type v} [inst_1 : AddCommGroup Q] [inst_2 : Module R Q],
  (∀ ⦃X Y : Type v⦄ [inst_3 : AddCommGroup X] [inst_4 : AddCommGroup Y] [inst_5 : Module R X] [inst_6 : Module R Y]
      (f : X →ₗ[R] Y), Function.Injective ⇑f → ∀ (g : X →ₗ[R] Q), ∃ h, ∀ (x : X), h (f x) = g x) →
    Module.Injective R Q
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem?_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, k ∉ m₂ → (m₁ ∩ m₂)[k]? = none
-- Mathlib.InformationTheory.KullbackLeibler.Basic
InformationTheory.klDiv_ne_top : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α},
  μ.AbsolutelyContinuous ν → MeasureTheory.Integrable (MeasureTheory.llr μ ν) μ → InformationTheory.klDiv μ ν ≠ ⊤