mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Floor.Semiring
Nat.floor_eq_iff' : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [inst_2 : FloorSemiring R] {a : R} {n : ℕ}
  [IsStrictOrderedRing R], n ≠ 0 → (⌊a⌋₊ = n ↔ ↑n ≤ a ∧ a < ↑n + 1)
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Ordinal.cof_blsub_le : ∀ {o : Ordinal.{u}} (f : (a : Ordinal.{u}) → a < o → Ordinal.{u}), (o.blsub f).cof ≤ o.card
-- Mathlib.Analysis.Normed.Group.InfiniteSum
/-- Variant of the direct comparison test for series:  if the norm of `f` is eventually bounded by a
real function `g` which is summable, then `f` is summable.  -/
Summable.of_norm_bounded_eventually_nat : ∀ {E : Type u_3} [inst : SeminormedAddCommGroup E] [CompleteSpace E] {f : ℕ → E} {g : ℕ → ℝ},
  Summable g → (∀ᶠ (i : ℕ) in Filter.atTop, ‖f i‖ ≤ g i) → Summable f
-- Mathlib.CategoryTheory.Functor.EpiMono
CategoryTheory.Functor.epi_map_iff_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) [hF₁ : F.PreservesEpimorphisms] [hF₂ : F.ReflectsEpimorphisms],
  CategoryTheory.Epi (F.map f) ↔ CategoryTheory.Epi f
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} (G : Type u_4) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : InnerProductSpace 𝕜 G] (f₁ f₂ : E →L[𝕜] F),
  ContinuousLinearMap.lTensor G (f₁ - f₂) = ContinuousLinearMap.lTensor G f₁ - ContinuousLinearMap.lTensor G f₂
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernelSubobject.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst_2 : CategoryTheory.Limits.HasKernel f],
  CategoryTheory.Limits.kernelSubobject f = CategoryTheory.Limits.kernelSubobject f_1
-- Init.Data.Nat.Lcm
Nat.lcm_mul_left_right : ∀ (m n : ℕ), n.lcm (m * n) = m * n
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
SimpleGraph.IsBipartiteWith.subgraph : ∀ {V : Type u_1} {G : SimpleGraph V} {s t : Set V},
  G.IsBipartiteWith s t → ∀ (H : G.Subgraph), H.coe.IsBipartiteWith {x | ↑x ∈ s} {x | ↑x ∈ t}
-- Lean.Elab.BindersUtil
Lean.Elab.Term.shouldExpandMatchAlt : Lean.TSyntax `Lean.Parser.Term.matchAlt → Bool
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_diff_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α},
  k ∉ m₁ → (m₁ \ m₂).get? k = none
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.ι_comp_colimitLeftOpIsoUnopLimit_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : Jᵒᵖ) {Z : C}
  (h : Opposite.unop (CategoryTheory.Limits.limit F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.leftOp j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitLeftOpIsoUnopLimit F).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F (Opposite.unop j)).unop h
-- Mathlib.GroupTheory.HNNExtension
/-- The HNN Extension of a group `G`, `HNNExtension G A B φ`. Given a group `G`, subgroups `A` and
`B` and an isomorphism `φ` of `A` and `B`, we adjoin a letter `t` to `G`, such that for
any `a ∈ A`, the conjugate of `of a` by `t` is `of (φ a)`, where `of` is the canonical
map from `G` into the `HNNExtension`.  -/
HNNExtension : (G : Type u_1) → [inst : Group G] → (A B : Subgroup G) → ↥A ≃* ↥B → Type u_1
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.instIsLeftKanExtensionOppositeTruncatedSimplexCategoryObjSkAppTruncatedUnitSkAdjTruncation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) (n : ℕ)
  [inst_1 :
    ∀ (F : CategoryTheory.Functor (SimplexCategory.Truncated n)ᵒᵖ C),
      (SimplexCategory.Truncated.inclusion n).op.HasLeftKanExtension F],
  CategoryTheory.Functor.IsLeftKanExtension ((CategoryTheory.SimplicialObject.sk n).obj X)
    ((CategoryTheory.SimplicialObject.skAdj n).unit.app ((CategoryTheory.SimplicialObject.truncation n).obj X))
-- Mathlib.Data.Seq.Computation
Computation.terminates_bind : ∀ {α : Type u} {β : Type v} (s : Computation α) (f : α → Computation β) [inst : s.Terminates] [(f s.get).Terminates],
  (s.bind f).Terminates
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.coe_codRestrict : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (f : A →ₐ[R] B) (S : Subalgebra R B) (hf : ∀ (x : A), f x ∈ S) (x : A),
  ↑((f.codRestrict S hf) x) = f x
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.instFinite : ∀ {α : Type u_2} [inst : TopologicalSpace α] [Finite α], Finite (TopologicalSpace.Opens α)
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- The map makes the triangle with the two natural transformations commute  -/
CategoryTheory.Limits.IsLimit.fac_assoc : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.IsLimit t)
  (s : CategoryTheory.Limits.Cone F) (j : J) {Z : C} (h : F.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.lift s) (CategoryTheory.CategoryStruct.comp (t.π.app j) h) =
    CategoryTheory.CategoryStruct.comp (s.π.app j) h
-- Mathlib.Topology.Compactness.Compact
exists_nhds_ne_inf_principal_neBot : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s → s.Infinite → ∃ z ∈ s, (nhdsWithin z {z}ᶜ ⊓ Filter.principal s).NeBot
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_iSup₂ : ∀ {α : Type u_1} {ι : Sort u_4} {κ : ι → Sort u_5} [inst : LE α] (f : (i : ι) → κ i → LowerSet α),
  ↑(⨆ i, ⨆ j, f i j) = ⋃ i, ⋃ j, ↑(f i j)
-- Lean.Server.References
/-- Path to the ILean file.  -/
Lean.Server.LoadedILean.ileanPath : Lean.Server.LoadedILean → System.FilePath
-- Mathlib.Analysis.Normed.Field.Dense
/-- If `K` is an algebraically closed dense subfield of a complete nonarchimedean normed field `L`
of characteristic zero, then `L` is also algebraically closed.  -/
IsAlgClosed.of_denseRange : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : NontriviallyNormedField L] [CompleteSpace L] [CharZero L]
  [IsUltrametricDist L] [inst_5 : Algebra K L], DenseRange ⇑(algebraMap K L) → ∀ [IsAlgClosed K], IsAlgClosed L
-- Lean.Elab.InfoTree.Basic
Lean.Elab.InfoTree.findInfo? : (Lean.Elab.Info → Bool) → Lean.Elab.InfoTree → Option Lean.Elab.Info
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.StrongTrans.Modification.whiskerRight_naturality_assoc : ∀ {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.StrongTrans.Modification η θ)
  {a b : B} {a' : C} (f : a ⟶ b) (g : G.obj b ⟶ a') {Z : F.obj a ⟶ a'}
  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (θ.app a) (G.map f)) g ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (F.map f) (CategoryTheory.Bicategory.whiskerRight (Γ.app b) g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (θ.app b) g).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (θ.naturality f).hom g) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (η.app b) g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom g)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (Γ.app a) (G.map f)) g) h))
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.Normal.quotient_commutative_iff_commutator_le : ∀ {G : Type u_1} [inst : Group G] {N : Subgroup G} [inst_1 : N.Normal], IsMulCommutative (G ⧸ N) ↔ commutator G ≤ N
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
AlgebraicGeometry.Scheme.Hom.ker_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z),
  AlgebraicGeometry.Scheme.Hom.ker (CategoryTheory.CategoryStruct.comp f g) = (AlgebraicGeometry.Scheme.Hom.ker f).map g
-- Lean.Meta.DiscrTree.Types
Lean.Meta.DiscrTree.Key.lit : Lean.Literal → Lean.Meta.DiscrTree.Key
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- `f` equalizes the two maps  -/
CategoryTheory.RegularMono.w_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y} (self : CategoryTheory.RegularMono f)
  {Z : C} (h : self.Z ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp self.left h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp self.right h)
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
Subalgebra.algebraicClosure.congr_simp : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [inst_3 : IsDomain R],
  Subalgebra.algebraicClosure R S = Subalgebra.algebraicClosure R S
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Linear map version of the map `toMultilinearMap` associating to a continuous alternating map
the corresponding multilinear map.  -/
ContinuousAlternatingMap.toContinuousMultilinearMapLinear : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        {ι : Type u_5} →
          [inst : Semiring R] →
            [inst_1 : Semiring A] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid N] →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : TopologicalSpace N] →
                      [inst_6 : ContinuousAdd N] →
                        [inst_7 : Module A M] →
                          [inst_8 : Module A N] →
                            [inst_9 : Module R N] →
                              [inst_10 : ContinuousConstSMul R N] →
                                [inst_11 : SMulCommClass A R N] →
                                  M [⋀^ι]→L[A] N →ₗ[R] ContinuousMultilinearMap A (fun x => M) N
-- Mathlib.Order.Category.BddDistLat
/-- The underlying `BoundedLatticeHom`.  -/
BddDistLat.Hom.hom' : {X Y : BddDistLat} → X.Hom Y → BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- `MonoOver.map f` followed by `MonoOver.pullback f` is the identity.  -/
CategoryTheory.MonoOver.pullbackMapSelf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasPullbacks C] →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Mono f] →
            (CategoryTheory.MonoOver.map f).comp (CategoryTheory.MonoOver.pullback f) ≅
              CategoryTheory.Functor.id (CategoryTheory.MonoOver X)
-- Mathlib.Topology.Bases
TopologicalSpace.IsSeparable.union : ∀ {α : Type u} [t : TopologicalSpace α] {s u : Set α},
  TopologicalSpace.IsSeparable s → TopologicalSpace.IsSeparable u → TopologicalSpace.IsSeparable (s ∪ u)
-- Mathlib.CategoryTheory.Sites.GlobalSections
/-- For sheaves of types, the global sections functor is isomorphic to the sections functor
on presheaves.  -/
CategoryTheory.Sheaf.ΓNatIsoSectionsFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      CategoryTheory.Sheaf.Γ J (Type (max u v)) ≅
        (CategoryTheory.sheafToPresheaf J (Type (max u v))).comp (CategoryTheory.Functor.sectionsFunctor Cᵒᵖ)
-- Mathlib.Data.Part
Part.instInter : {α : Type u_1} → [Inter α] → Inter (Part α)
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Expand the square  -/
norm_sub_mul_self_real : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] (x y : F),
  ‖x - y‖ * ‖x - y‖ = ‖x‖ * ‖x‖ - 2 * inner ℝ x y + ‖y‖ * ‖y‖
-- Mathlib.Analysis.Convex.Side
AffineSubspace.wOppSide_iff_exists_left : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y p₁ : P}, p₁ ∈ s → (s.WOppSide x y ↔ x ∈ s ∨ ∃ p₂ ∈ s, SameRay R (x -ᵥ p₁) (p₂ -ᵥ y))
-- Mathlib.Algebra.Module.SpanRank
Ideal.spanFinrank_map_le_of_fg : ∀ {R : Type u} [inst : Semiring R] {T : Type v} [inst_1 : Semiring T] (f : R →+* T) {I : Ideal R},
  I.FG → Submodule.spanFinrank (Ideal.map f I) ≤ Submodule.spanFinrank I
-- Mathlib.Data.Set.Disjoint
Set.disjoint_range_iff : ∀ {α : Type u} {β : Sort u_1} {γ : Sort u_2} {x : β → α} {y : γ → α},
  Disjoint (Set.range x) (Set.range y) ↔ ∀ (i : β) (j : γ), x i ≠ y j
-- Mathlib.LinearAlgebra.StdBasis
Pi.linearIndependent_single_of_ne_zero : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Ring R] [IsDomain R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [Module.IsTorsionFree R M] [inst_5 : DecidableEq ι] {v : ι → M},
  (∀ (i : ι), v i ≠ 0) → LinearIndependent R fun i => Pi.single i (v i)
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.nextn.match_1.splitter : (motive : Substring.Raw → ℕ → String.Pos.Raw → Sort u_1) →
  (x : Substring.Raw) →
    (x_1 : ℕ) →
      (x_2 : String.Pos.Raw) →
        ((x : Substring.Raw) → (p : String.Pos.Raw) → motive x 0 p) →
          ((ss : Substring.Raw) → (i : ℕ) → (p : String.Pos.Raw) → motive ss i.succ p) → motive x x_1 x_2
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
min_mul_distrib : ∀ {α : Type u} [inst : Monoid α] [inst_1 : LinearOrder α] [CanonicallyOrderedMul α] (a b c : α),
  min a (b * c) = min a (min a b * min a c)
-- Std.Data.TreeMap.Raw.WF
Std.TreeMap.Raw.WF.erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp] {a : α},
  t.WF → (t.erase a).WF
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ChangeAnnotationSupport.mk.inj : ∀ {groupsOnLabel? groupsOnLabel?_1 : Option Bool},
  { groupsOnLabel? := groupsOnLabel? } = { groupsOnLabel? := groupsOnLabel?_1 } → groupsOnLabel? = groupsOnLabel?_1
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.OpenNhdsOf.mk : {α : Type u_2} →
  [inst : TopologicalSpace α] →
    {x : α} → (toOpens : TopologicalSpace.Opens α) → x ∈ toOpens.carrier → TopologicalSpace.OpenNhdsOf x
-- Mathlib.Topology.Homeomorph.Lemmas
/-- A homeomorphism `h : X ≃ₜ Y` lifts to a homeomorphism between sets `s : Set X` and `t : Set Y`
whenever `h` maps `s` onto `t`.  -/
Homeomorph.sets : {X : Type u_1} →
  {Y : Type u_2} →
    [inst : TopologicalSpace X] →
      [inst_1 : TopologicalSpace Y] → {s : Set X} → {t : Set Y} → (h : X ≃ₜ Y) → s = ⇑h ⁻¹' t → ↑s ≃ₜ ↑t
-- Mathlib.Analysis.Normed.Affine.MazurUlam
IsometryEquiv.toRealLinearIsometryEquiv_symm_apply : ∀ {E : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (f : E ≃ᵢ F) (y : F), f.toRealLinearIsometryEquiv.symm y = f.symm (y + f 0)
-- Mathlib.Topology.Constructions
Topology.IsEmbedding.codRestrict : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {e : X → Y},
  Topology.IsEmbedding e → ∀ (s : Set Y) (hs : ∀ (x : X), e x ∈ s), Topology.IsEmbedding (Set.codRestrict e s hs)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.maxEntry?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → t₁.maxEntry? = t₂.maxEntry?
-- Mathlib.Order.RelIso.Basic
RelIso.relHomCongr_symm_apply_apply : ∀ {α₁ : Type u_5} {β₁ : Type u_6} {α₂ : Type u_7} {β₂ : Type u_8} {r₁ : α₁ → α₁ → Prop} {s₁ : β₁ → β₁ → Prop}
  {r₂ : α₂ → α₂ → Prop} {s₂ : β₂ → β₂ → Prop} (e₁ : r₁ ≃r r₂) (e₂ : s₁ ≃r s₂) (f₂ : r₂ →r s₂) (x : α₁),
  ((e₁.relHomCongr e₂).symm f₂) x = e₂.symm (f₂ (e₁ x))
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PullbackCone.unop_inl : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z}
  (c : CategoryTheory.Limits.PullbackCone f g), c.unop.inl = c.fst.unop
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isRevMatch_iff_isRevMatch_beq : ∀ {c : Char} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch c pos ↔ String.Slice.Pattern.Model.IsRevMatch (fun x => x == c) pos
-- Lean.Structure
/-- Deprecated.  -/
Lean.StructureFieldInfo.autoParam? : Lean.StructureFieldInfo → Option Lean.Expr
-- Mathlib.Algebra.Group.Defs
mul_one : ∀ {M : Type u} [inst : MulOneClass M] (a : M), a * 1 = a
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.lt_logb_iff_rpow_lt : ∀ {b x y : ℝ}, 1 < b → 0 < y → (x < Real.logb b y ↔ b ^ x < y)
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew_eq_containsₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α)
  (b : β a), (m.containsThenInsertIfNew a b).1 = m.containsₘ a
-- Mathlib.Algebra.Order.Group.OrderIso
/-- `Equiv.mulRight` as an `OrderIso`. See also `OrderEmbedding.mulRight`.  -/
OrderIso.mulRight : {α : Type u} → [inst : Group α] → [inst_1 : LE α] → [MulRightMono α] → α → α ≃o α
-- Mathlib.GroupTheory.Congruence.Defs
Con.instPartialOrder : {M : Type u_1} → [inst : Mul M] → PartialOrder (Con M)
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
jacobiSym.quadratic_reciprocity_if : ∀ {a b : ℕ},
  a % 2 = 1 → b % 2 = 1 → (if a % 4 = 3 ∧ b % 4 = 3 then -jacobiSym (↑b) a else jacobiSym (↑b) a) = jacobiSym (↑a) b
-- Mathlib.RingTheory.PolynomialAlgebra
PolyEquivTensor.toFunLinear_mul_tmul_mul : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a₁ a₂ : A)
  (p₁ p₂ : Polynomial R),
  (PolyEquivTensor.toFunLinear R A) ((a₁ * a₂) ⊗ₜ[R] (p₁ * p₂)) =
    (PolyEquivTensor.toFunLinear R A) (a₁ ⊗ₜ[R] p₁) * (PolyEquivTensor.toFunLinear R A) (a₂ ⊗ₜ[R] p₂)
-- Mathlib.Data.Multiset.AddSub
Multiset.Rel.add : ∀ {α : Type u_1} {β : Type v} {r : α → β → Prop} {s : Multiset α} {t : Multiset β} {u : Multiset α} {v : Multiset β},
  Multiset.Rel r s t → Multiset.Rel r u v → Multiset.Rel r (s + u) (t + v)
-- Mathlib.RingTheory.Polynomial.Dickson
Polynomial.map_dickson : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] {k : ℕ} {a : R} (f : R →+* S) (n : ℕ),
  Polynomial.map f (Polynomial.dickson k a n) = Polynomial.dickson k (f a) n
-- Mathlib.Algebra.Category.CommAlgCat.Basic
commAlgCatEquivUnder_functor_obj : ∀ (R : CommRingCat) (A : CommAlgCat ↑R), (commAlgCatEquivUnder R).functor.obj A = R.mkUnder ↑A
-- Lean.Message
/-- Produces a labeled hint without an associated code action (non-monadic variant of
`MessageData.hint`).
 -/
Lean.MessageData.hint' : Lean.MessageData → Lean.MessageData
-- Init.Data.List.Find
List.findIdx?.eq_1 : ∀ {α : Type u} (p : α → Bool) (l : List α), List.findIdx? p l = List.findIdx?.go p l 0
-- Std.Async.Select
_private.Std.Async.Select.0.Std.Async.Waiter.finished : {α : Type} → Std.Async.Waiter α → IO.Ref Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- The morphism between points of cokernel coforks induced by a morphism
in the category of arrows.  -/
CategoryTheory.Limits.CokernelCofork.mapOfIsColimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {X' Y' : C} →
            {f' : X' ⟶ Y'} →
              {cc : CategoryTheory.Limits.CokernelCofork f} →
                CategoryTheory.Limits.IsColimit cc →
                  (cc' : CategoryTheory.Limits.CokernelCofork f') →
                    (CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') → (cc.pt ⟶ cc'.pt)
-- Mathlib.ModelTheory.ElementarySubstructures
/-- Bundles the closure of a set meeting definable sets as an elementary substructure.  -/
FirstOrder.Language.MeetsDefinable.toElementarySubstructure : {L : FirstOrder.Language} →
  {M : Type u_1} →
    [inst : L.Structure M] → {A : Set M} → FirstOrder.Language.MeetsDefinable A → L.ElementarySubstructure M
-- Mathlib.Topology.ContinuousMap.LocallyConstant
LocallyConstant.toLinearMap_toContinuousMapAlgHom : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (R : Type u_3)
  [inst_2 : CommSemiring R] [inst_3 : Semiring Y] [inst_4 : Algebra R Y] [inst_5 : IsTopologicalSemiring Y],
  (LocallyConstant.toContinuousMapAlgHom R).toLinearMap = LocallyConstant.toContinuousMapLinearMap R
-- Mathlib.Data.Set.Basic
Set.inter_left_comm : ∀ {α : Type u} (s₁ s₂ s₃ : Set α), s₁ ∩ (s₂ ∩ s₃) = s₂ ∩ (s₁ ∩ s₃)
-- Mathlib.Algebra.Ring.Subring.Basic
/-- An induction principle for closure membership, for predicates with two arguments.  -/
Subring.closure_induction₂ : ∀ {R : Type u} [inst : NonAssocRing R] {s : Set R}
  {p : (x y : R) → x ∈ Subring.closure s → y ∈ Subring.closure s → Prop},
  (∀ (x y : R) (hx : x ∈ s) (hy : y ∈ s), p x y ⋯ ⋯) →
    (∀ (x : R) (hx : x ∈ Subring.closure s), p 0 x ⋯ hx) →
      (∀ (x : R) (hx : x ∈ Subring.closure s), p x 0 hx ⋯) →
        (∀ (x : R) (hx : x ∈ Subring.closure s), p 1 x ⋯ hx) →
          (∀ (x : R) (hx : x ∈ Subring.closure s), p x 1 hx ⋯) →
            (∀ (x y : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s), p x y hx hy → p (-x) y ⋯ hy) →
              (∀ (x y : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s), p x y hx hy → p x (-y) hx ⋯) →
                (∀ (x y z : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s) (hz : z ∈ Subring.closure s),
                    p x z hx hz → p y z hy hz → p (x + y) z ⋯ hz) →
                  (∀ (x y z : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s) (hz : z ∈ Subring.closure s),
                      p x y hx hy → p x z hx hz → p x (y + z) hx ⋯) →
                    (∀ (x y z : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s)
                        (hz : z ∈ Subring.closure s), p x z hx hz → p y z hy hz → p (x * y) z ⋯ hz) →
                      (∀ (x y z : R) (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s)
                          (hz : z ∈ Subring.closure s), p x y hx hy → p x z hx hz → p x (y * z) hx ⋯) →
                        ∀ {x y : R} (hx : x ∈ Subring.closure s) (hy : y ∈ Subring.closure s), p x y hx hy
-- Mathlib.Order.Interval.Set.Basic
Set.Iio_nonempty : ∀ {α : Type u_1} [inst : Preorder α] {a : α}, (Set.Iio a).Nonempty ↔ ¬IsMin a
-- Mathlib.Order.CompleteLattice.Defs
/-- Create a `CompleteLattice` from a `PartialOrder` and `SupSet`
that returns the least upper bound of a set. Usually this constructor provides
poor definitional equalities.  If other fields are known explicitly, they should be
provided; for example, if `inf` is known explicitly, construct the `CompleteLattice`
instance as
```
instance : CompleteLattice my_T where
  inf := better_inf
  le_inf := ...
  inf_le_right := ...
  inf_le_left := ...
  -- don't care to fix sup, sInf, bot, top
  __ := completeLatticeOfSup my_T _
```
 -/
completeLatticeOfSup : (α : Type u_8) → [H1 : PartialOrder α] → [H2 : SupSet α] → (∀ (s : Set α), IsLUB s (sSup s)) → CompleteLattice α
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.inter_smul_union_subset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : SMul α β] {s₁ s₂ : Set α} {t₁ t₂ : Set β},
  (s₁ ∩ s₂) • (t₁ ∪ t₂) ⊆ s₁ • t₁ ∪ s₂ • t₂
-- Mathlib.Algebra.CubicDiscriminant
Cubic.natDegree_of_b_eq_zero : ∀ {R : Type u_1} {P : Cubic R} [inst : Semiring R], P.a = 0 → P.b = 0 → P.toPoly.natDegree ≤ 1
-- Mathlib.Topology.MetricSpace.Thickening
/-- For the equality, see `infEDist_thickening`.  -/
Metric.infEDist_le_infEDist_thickening_add : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ} {s : Set α} {x : α},
  Metric.infEDist x s ≤ Metric.infEDist x (Metric.thickening δ s) + ENNReal.ofReal δ
-- Mathlib.Topology.Instances.Nat
Nat.isClosedEmbedding_coe_real : Topology.IsClosedEmbedding Nat.cast