mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
returning `none` if no such pair exists.
 -/
Std.ExtTreeMap.getEntryGT? : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → α → Option (α × β)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.stepAux.match_1.eq_1 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ]
  (motive : Turing.TM1.Stmt Γ Λ σ → σ → Turing.Tape Γ → Sort u_4) (d : Turing.Dir) (q : Turing.TM1.Stmt Γ Λ σ) (v : σ)
  (T : Turing.Tape Γ)
  (h_1 :
    (d : Turing.Dir) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.move d q) v T)
  (h_2 :
    (a : Γ → σ → Γ) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.write a q) v T)
  (h_3 :
    (s : Γ → σ → σ) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.load s q) v T)
  (h_4 :
    (p : Γ → σ → Bool) →
      (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v T)
  (h_5 : (l : Γ → σ → Λ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.goto l) v T)
  (h_6 : (v : σ) → (T : Turing.Tape Γ) → motive Turing.TM1.Stmt.halt v T),
  (match Turing.TM1.Stmt.move d q, v, T with
    | Turing.TM1.Stmt.move d q, v, T => h_1 d q v T
    | Turing.TM1.Stmt.write a q, v, T => h_2 a q v T
    | Turing.TM1.Stmt.load s q, v, T => h_3 s q v T
    | Turing.TM1.Stmt.branch p q₁ q₂, v, T => h_4 p q₁ q₂ v T
    | Turing.TM1.Stmt.goto l, v, T => h_5 l v T
    | Turing.TM1.Stmt.halt, v, T => h_6 v T) =
    h_1 d q v T
-- Mathlib.MeasureTheory.Measure.Lebesgue.VolumeOfBalls
MeasureTheory.volume_sum_rpow_le : ∀ (ι : Type u_1) [inst : Fintype ι] [Nonempty ι] {p : ℝ},
  1 ≤ p →
    ∀ (r : ℝ),
      MeasureTheory.volume {x | (∑ i, |x i| ^ p) ^ (1 / p) ≤ r} =
        ENNReal.ofReal r ^ Fintype.card ι *
          ENNReal.ofReal ((2 * Real.Gamma (1 / p + 1)) ^ Fintype.card ι / Real.Gamma (↑(Fintype.card ι) / p + 1))
-- Mathlib.Order.Filter.Tendsto
/-- **Alias** of the reverse direction of `Filter.map_mapsTo_Iic_iff_mapsTo`. -/
Set.MapsTo.filter_map_Iic : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {m : α → β},
  Set.MapsTo m s t → Set.MapsTo (Filter.map m) (Set.Iic (Filter.principal s)) (Set.Iic (Filter.principal t))
-- Mathlib.Data.Rat.Defs
Rat.mk_num_ne_zero_of_ne_zero : ∀ {q : ℚ} {n d : ℤ}, q ≠ 0 → q = Rat.divInt n d → n ≠ 0
-- Mathlib.Tactic.Widget.StringDiagram
/-- The underlying expression of a node.  -/
Mathlib.Tactic.Widget.StringDiagram.Node.e : Mathlib.Tactic.Widget.StringDiagram.Node → Lean.Expr
-- Mathlib.Order.Minimal
Set.Subsingleton.minimal_mem_iff : ∀ {α : Type u_2} {x : α} {s : Set α} [inst : Preorder α], s.Subsingleton → (Minimal (fun x => x ∈ s) x ↔ x ∈ s)
-- Mathlib.RingTheory.Polynomial.Eisenstein.Basic
Polynomial.IsWeaklyEisensteinAt.exists_mem_adjoin_mul_eq_pow_natDegree : ∀ {R : Type u} [inst : CommRing R] {f : Polynomial R} {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : R}
  {x : S},
  (Polynomial.aeval x) f = 0 →
    f.Monic →
      f.IsWeaklyEisensteinAt (R ∙ p) →
        ∃ y ∈ R[x], (algebraMap R S) p * y = x ^ (Polynomial.map (algebraMap R S) f).natDegree
-- Init.Omega.IntList
Lean.Omega.IntList.sum_add : ∀ (xs ys : Lean.Omega.IntList), (xs + ys).sum = xs.sum + ys.sum
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The indexing type of the cells of dimension `n`.  -/
Topology.CWComplex.cell : {X : Type u} → {inst : TopologicalSpace X} → (C : Set X) → [self : Topology.CWComplex C] → ℕ → Type u
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instReprBVBit.repr : Std.Tactic.BVDecide.BVBit → ℕ → Std.Format
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- Constructor for morphisms to the coend of a functor.  -/
CategoryTheory.Limits.coend.desc : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {C : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} →
          [inst_2 : CategoryTheory.Limits.HasCoend F] →
            {X : C} →
              (f : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ X) →
                (∀ ⦃i j : J⦄ (g : i ⟶ j),
                    CategoryTheory.CategoryStruct.comp ((F.map g.op).app i) (f i) =
                      CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j)) →
                  (CategoryTheory.Limits.coend F ⟶ X)
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.mul_closure_one_eq : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] {U : Set G},
  IsOpen U → U * closure {1} = U
-- Mathlib.Analysis.RCLike.Basic
RCLike.mul_conj : ∀ {K : Type u_1} [inst : RCLike K] (z : K), z * (starRingEnd K) z = ↑‖z‖ ^ 2
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getLetEqnsDeclVars : Lean.Syntax → Array Lean.Elab.Term.Do.Var
-- Mathlib.Computability.Partrec
Computable.sumInl : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β], Computable Sum.inl
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.coe_comp_topHom : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  [inst_3 : BoundedOrder α] [inst_4 : BoundedOrder β] [inst_5 : BoundedOrder γ] (f : BoundedOrderHom β γ)
  (g : BoundedOrderHom α β), ↑(f.comp g) = (↑f).comp ↑g
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `iteratedFDeriv_sub`

---

The iterated derivative of the difference of two functions is the difference of the iterated
derivatives.
 -/
fun_iteratedFDeriv_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {i : ℕ}
  {f g : E → F},
  ContDiff 𝕜 (↑i) f →
    ContDiff 𝕜 (↑i) g →
      (iteratedFDeriv 𝕜 i fun i => f i - g i) = fun i_1 => iteratedFDeriv 𝕜 i f i_1 - iteratedFDeriv 𝕜 i g i_1
-- Mathlib.Algebra.Lie.Semisimple.Basic
LieAlgebra.isSimple_iff_of_not_isLieAbelian : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  ¬IsLieAbelian L → (IsSimpleOrder (LieIdeal R L) ↔ LieAlgebra.IsSimple R L)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.toArrowArrowFunctor_obj_left_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  (CategoryTheory.Square.toArrowArrowFunctor.obj sq).left.hom = sq.f₁₃
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.srange_fst : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] [Nonempty N], (AddHom.fst M N).srange = ⊤
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey?_empty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {a : α}, ∅.getKey? a = none
-- Mathlib.Data.DFinsupp.Multiset
/-- Non-dependent special case of `DFinsupp.addZeroClass` to help typeclass search.  -/
DFinsupp.addZeroClass' : {α : Type u_1} → {β : Type u_2} → [inst : AddZeroClass β] → AddZeroClass (Π₀ (x : α), β)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn.hom_ext' : ∀ {n : ℕ} {X : SSet} {i : Fin (n + 2)} {f g : (SSet.horn (n + 1) i).toSSet ⟶ X},
  (∀ (j : Fin (n + 2)) (hj : j ≠ i),
      CategoryTheory.CategoryStruct.comp (SSet.horn.ι i j hj) f =
        CategoryTheory.CategoryStruct.comp (SSet.horn.ι i j hj) g) →
    f = g
-- Mathlib.Data.ENNReal.Operations
ENNReal.add_biSup : ∀ {a : ENNReal} {ι : Type u_3} {s : Set ι}, s.Nonempty → ∀ (f : ι → ENNReal), a + ⨆ i ∈ s, f i = ⨆ i ∈ s, a + f i
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstr : Type
-- Mathlib.RingTheory.Trace.Defs
/-- The trace of an element `s` of an `R`-algebra is the trace of `(s * ·)`,
as an `R`-linear map.  -/
Algebra.trace : (R : Type u_1) → (S : Type u_2) → [inst : CommRing R] → [inst_1 : CommRing S] → [inst_2 : Algebra R S] → S →ₗ[R] R
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.roots_map : ∀ {R : Type u_1} {S : Type u_2} [inst : Field R] [inst_1 : CommRing S] [inst_2 : IsDomain S] {f : Polynomial R},
  f.Splits → ∀ (i : R →+* S), (Polynomial.map i f).roots = Multiset.map (⇑i) f.roots
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_smul_non_comm : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {α : Type v} [inst : Star R] [inst_1 : Star α] [inst_2 : SMul R α]
  [inst_3 : SMul Rᵐᵒᵖ α] (c : R) (M : Matrix m n α),
  (∀ (r : R) (a : α), star (r • a) = MulOpposite.op (star r) • star a) →
    (c • M).conjTranspose = MulOpposite.op (star c) • M.conjTranspose
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ico_subset_Ico_left : ∀ {α : Type u_2} {a₁ a₂ b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  a₁ ≤ a₂ → Finset.Ico a₂ b ⊆ Finset.Ico a₁ b
-- Batteries.Data.MLList.Basic
_private.Batteries.Data.MLList.Basic.0.MLList.Spec.squash : {m : Type u → Type u} →
  (self : MLList.Spec✝ m) → {α : Type u} → (Unit → m (MLList.Spec.listM✝ self α)) → MLList.Spec.listM✝ self α
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.self_le_max!_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → ∀ {k : α}, (cmp k (t.insert k).max!).isLE = true
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.instIsAlgebraicSubtypeMemBot : ∀ {K : Type u} [inst : Field K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L], Algebra.IsAlgebraic K ↥⊥
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_congr : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a b : α}, (a == b) = true → m.contains a = m.contains b
-- Mathlib.Topology.MetricSpace.MetricSeparated
Metric.AreSeparated.union_left_iff : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s t s' : Set X},
  Metric.AreSeparated (s ∪ s') t ↔ Metric.AreSeparated s t ∧ Metric.AreSeparated s' t
-- Mathlib.Topology.OmegaCompletePartialOrder
Topology.IsScott.ωScottContinuous_iff_continuous : ∀ {α : Type u_1} [inst : OmegaCompletePartialOrder α] [inst_1 : TopologicalSpace α]
  [Topology.IsScott α (Set.range fun c => Set.range ⇑c)] {f : α → Prop},
  OmegaCompletePartialOrder.ωScottContinuous f ↔ Continuous f
-- Mathlib.CategoryTheory.Category.Quiv
/-- Arrows in `Quiv` define prefunctors.  -/
CategoryTheory.Prefunctor.ofQuivHom : {C D : CategoryTheory.Quiv} → (C ⟶ D) → ↑C ⥤q ↑D
-- Mathlib.Combinatorics.Matroid.Rank.ENat
Matroid.restrict_eRk_eq : ∀ {α : Type u_1} {X : Set α} (M : Matroid α) {R : Set α}, X ⊆ R → (M.restrict R).eRk X = M.eRk X
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.tensorKaehlerEquivBase_tmul : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) (B : Type u_4) [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (a : S) (b : Ω[A⁄R]),
  (KaehlerDifferential.tensorKaehlerEquivBase R S A B) (a ⊗ₜ[R] b) = a • (KaehlerDifferential.map R S A B) b
-- Mathlib.CategoryTheory.Limits.Constructions.EpiMono
CategoryTheory.preservesMonomorphisms_of_preservesLimitsOfShape : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimitsOfShape CategoryTheory.Limits.WalkingCospan F],
  F.PreservesMonomorphisms
-- Lean.Widget.Types
/-- Name of the `@[widget_module]`.  -/
Lean.Widget.WidgetInstance.id : Lean.Widget.WidgetInstance → Lean.Name
-- Std.Data.HashSet.Lemmas
Std.HashSet.all_eq_true_iff_forall_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulBEq α] {p : α → Bool},
  m.all p = true ↔ ∀ a ∈ m, p a = true
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.additiveObjIsoBiproduct_naturality'_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts D] (F : CategoryTheory.Functor (CategoryTheory.Mat_ C) D)
  [inst_5 : F.Additive] {M N : CategoryTheory.Mat_ C} (f : M ⟶ N) {Z : D} (h : F.obj N ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F M).inv
      (CategoryTheory.CategoryStruct.comp (F.map f) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.matrix fun i j => F.map ((CategoryTheory.Mat_.embedding C).map (f i j)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Mat_.additiveObjIsoBiproduct F N).inv h)
-- Mathlib.Geometry.Manifold.MFDeriv.Defs
/-- `MDifferentiable I I' f` indicates that the function `f` between manifolds
has a derivative everywhere.
This is a generalization of `Differentiable` to manifolds.  -/
MDifferentiable : {𝕜 : 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] →
              ModelWithCorners 𝕜 E H →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [ChartedSpace H M] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                ModelWithCorners 𝕜 E' H' →
                                  {M' : Type u_7} →
                                    [inst : TopologicalSpace M'] → [ChartedSpace H' M'] → (M → M') → Prop
-- Mathlib.Geometry.Manifold.IsManifold.Basic
contDiffPregroupoid.eq_1 : ∀ (n : WithTop ℕ∞) {𝕜 : 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),
  contDiffPregroupoid n I =
    { property := fun f s => ContDiffOn 𝕜 n (↑I ∘ f ∘ ↑I.symm) (↑I.symm ⁻¹' s ∩ Set.range ↑I), comp := ⋯, id_mem := ⋯,
      locality := ⋯, congr := ⋯ }
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- `t` is the morphism witnessing transitivity  -/
CategoryTheory.TransitiveRelation.t : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} → {p₁ p₂ : R ⟶ X} → (self : CategoryTheory.TransitiveRelation p₁ p₂) → self.c.pt ⟶ R
-- Mathlib.SetTheory.Cardinal.ToNat
Cardinal.toNat_eq_iff : ∀ {c : Cardinal.{u}} {n : ℕ}, n ≠ 0 → (Cardinal.toNat c = n ↔ c = ↑n)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α} {fallback : β},
  (List.map Prod.fst l).contains k = false → (m.insertMany l).getD k fallback = m.getD k fallback
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.ofFunctor.inj : ∀ {C D : CategoryTheory.Cat} {toFunctor toFunctor_1 : CategoryTheory.Functor ↑C ↑D},
  { toFunctor := toFunctor } = { toFunctor := toFunctor_1 } → toFunctor = toFunctor_1
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δAux.congr_simp : ∀ (R : Type u₁) {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  (Q : Algebra.Generators S T ι), Algebra.Generators.H1Cotangent.δAux R Q = Algebra.Generators.H1Cotangent.δAux R Q
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.reassign.sizeOf_spec : ∀ (xs : Array Lean.Elab.Term.Do.Var) (doElem : Lean.Syntax) (k : Lean.Elab.Term.Do.Code),
  sizeOf (Lean.Elab.Term.Do.Code.reassign xs doElem k) = 1 + sizeOf xs + sizeOf doElem + sizeOf k
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Fix.rec_unique : ∀ {F : Type u → Type u} [q : QPF F] {α : Type u} (g : F α → α) (h : QPF.Fix F → α),
  (∀ (x : F (QPF.Fix F)), h (QPF.Fix.mk x) = g (h <$> x)) → QPF.Fix.rec g = h
-- Mathlib.CategoryTheory.Localization.Monoidal.Braided
_private.Mathlib.CategoryTheory.Localization.Monoidal.Braided.0.CategoryTheory.Localization.Monoidal.termL' : Lean.ParserDescr
-- Lean.Server.Utils
/-- Finds the URI corresponding to `modName` in `searchSearchPath`.
Yields `none` if the file corresponding to `modName` has been deleted in the mean-time.
 -/
Lean.Server.documentUriFromModule? : Lean.Name → IO (Option Lean.Lsp.DocumentUri)
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Asymptotic
/-- A non-negative function with locally finite support has finite support if and only if its
logarithmic counting function is big-O of `log`.
 -/
Function.locallyFinsuppWithin.finite_support_iff_logCounting_isBigO_log : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : ProperSpace E] {D : Function.locallyFinsupp E ℤ},
  0 ≤ D →
    ((Function.locallyFinsuppWithin.support D).Finite ↔
      Function.locallyFinsuppWithin.logCounting D =O[Filter.atTop] Real.log)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.coind₁ι_toFun : ∀ {R : Type u_1} {V : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] {G : Type u_7} [inst_5 : Group G]
  [inst_6 : TopologicalSpace G] [inst_7 : TopologicalSpace R] [inst_8 : ContinuousSMul R V]
  [inst_9 : IsTopologicalGroup G] (π : ContRepresentation R G V) (b : V), π.coind₁ι b = ContinuousMap.const G b
-- Mathlib.Order.Preorder.Chain
/-- This can be used to turn `IsChain (≥)` into `IsChain (≤)` and vice-versa.  -/
IsChain.symm : ∀ {α : Type u_1} {r : α → α → Prop} {s : Set α}, IsChain r s → IsChain (flip r) s
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap_fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.HoCat.resolutionMap f)
      (CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj Y) h) =
    CategoryTheory.CategoryStruct.comp (HomotopicalAlgebra.CofibrantObject.HoCat.pResolutionObj X)
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.LinearAlgebra.TensorProduct.Associator
/-- Given linear maps `f : M → Q`, `g : N → S`, and `h : P → T`, if we identify `M ⊗ (N ⊗ P)`
with `(M ⊗ N) ⊗ P` and `Q ⊗ (S ⊗ T)` with `(Q ⊗ S) ⊗ T`, then this lemma states that
`(f ⊗ g) ⊗ h = f ⊗ (g ⊗ h)`.  -/
TensorProduct.map_map_comp_assoc_symm_eq : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_5} {N : Type u_6} {P : Type u_7} {Q : Type u_8} {S : Type u_9}
  {T : Type u_10} [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P]
  [inst_4 : AddCommMonoid Q] [inst_5 : AddCommMonoid S] [inst_6 : AddCommMonoid T] [inst_7 : Module R M]
  [inst_8 : Module R N] [inst_9 : Module R Q] [inst_10 : Module R S] [inst_11 : Module R T] [inst_12 : Module R P]
  (f : M →ₗ[R] Q) (g : N →ₗ[R] S) (h : P →ₗ[R] T),
  TensorProduct.map (TensorProduct.map f g) h ∘ₗ ↑(TensorProduct.assoc R M N P).symm =
    ↑(TensorProduct.assoc R Q S T).symm ∘ₗ TensorProduct.map f (TensorProduct.map g h)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Unbounded.State.mk : {α : Type} → Std.Queue α → Std.Queue (Std.CloseableChannel.Consumer✝ α) → Bool → Std.CloseableChannel.Unbounded.State✝ α
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycle.two_le_card_support : ∀ {α : Type u_2} {f : Equiv.Perm α} [inst : DecidableEq α] [inst_1 : Fintype α], f.IsCycle → 2 ≤ f.support.card
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
/-- If a `NonUnitalSubalgebra` over a field does not contain `1`, then its unitization is
isomorphic to its `Algebra.adjoin`.  -/
NonUnitalSubalgebra.unitizationAlgEquiv : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      [inst : Field R] →
        [inst_1 : Ring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : SetLike S A] →
              [hSA : NonUnitalSubringClass S A] →
                [hSRA : SMulMemClass S R A] → (s : S) → 1 ∉ s → Unitization R ↥s ≃ₐ[R] ↥(Algebra.adjoin R ↑s)
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_mul_const_Ioo : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a b c : α),
  (fun x => x * a) ⁻¹' Set.Ioo b c = Set.Ioo (b / a) (c / a)
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.lift_injective : Function.Injective Cardinal.lift.{u, v}
-- Lean.Declaration
Lean.ConstantInfo.toConstantVal : Lean.ConstantInfo → Lean.ConstantVal
-- Mathlib.CategoryTheory.GlueData
/-- The morphism via which `V i j ×[U i] V i k ⟶ V i j ⟶ V j i` factors through
`V j k ×[U j] V j i ⟶ V j i`  -/
CategoryTheory.GlueData.t' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v, u₁} C] →
    (self : CategoryTheory.GlueData C) →
      (i j k : self.J) →
        CategoryTheory.Limits.pullback (self.f i j) (self.f i k) ⟶
          CategoryTheory.Limits.pullback (self.f j k) (self.f j i)
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.inv_hom_id_app_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E]
  {F G : CategoryTheory.Functor C (CategoryTheory.Functor D E)} (e : F ≅ G) (X₁ : C) (X₂ : D) {Z : E}
  (h : (G.obj X₁).obj X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((e.inv.app X₁).app X₂)
      (CategoryTheory.CategoryStruct.comp ((e.hom.app X₁).app X₂) h) =
    h
-- Mathlib.LinearAlgebra.Matrix.ToLin
LinearMap.toMatrixAlgEquiv_reindexRange : ∀ {R : Type u_1} [inst : CommSemiring R] {n : Type u_4} [inst_1 : Fintype n] [inst_2 : DecidableEq n] {M₁ : Type u_5}
  [inst_3 : AddCommMonoid M₁] [inst_4 : Module R M₁] (v₁ : Module.Basis n R M₁) [inst_5 : DecidableEq M₁]
  (f : M₁ →ₗ[R] M₁) (k i : n),
  (LinearMap.toMatrixAlgEquiv v₁.reindexRange) f ⟨v₁ k, ⋯⟩ ⟨v₁ i, ⋯⟩ = (LinearMap.toMatrixAlgEquiv v₁) f k i
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
HomotopyCategory.Pretriangulated.isomorphic_distinguished : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C],
  ∀ T₁ ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C,
    ∀ (T₂ : CategoryTheory.Pretriangulated.Triangle (HomotopyCategory C (ComplexShape.up ℤ))) (e : T₂ ≅ T₁),
      T₂ ∈ HomotopyCategory.Pretriangulated.distinguishedTriangles C
-- Mathlib.Data.Nat.Prime.Basic
/-- **Alias** of the forward direction of `Nat.coprime_two_left`. -/
Nat.Coprime.odd_of_left : ∀ {n : ℕ}, Nat.Coprime 2 n → Odd n
-- Mathlib.Analysis.Calculus.FDeriv.Star
DifferentiableAt.star : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : StarRing 𝕜] {E : Type u_2} [inst_2 : NormedAddCommGroup E]
  [inst_3 : NormedSpace 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : StarAddMonoid F]
  [inst_6 : NormedSpace 𝕜 F] [StarModule 𝕜 F] [ContinuousStar F] {f : E → F} {x : E} [TrivialStar 𝕜],
  DifferentiableAt 𝕜 f x → DifferentiableAt 𝕜 (fun y => star (f y)) x
-- Mathlib.Algebra.Group.Action.Opposite
AddSemigroup.opposite_vaddCommClass : ∀ {α : Type u_3} [inst : AddSemigroup α], VAddCommClass αᵃᵒᵖ α α
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.map_injective_of_injective : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] {f : F}, Function.Injective ⇑f → Function.Injective (Submonoid.map f)