mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.MemBaseSet.filter : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} {c : NNReal} {l : BoxIntegral.IntegrationParams}
  {π : BoxIntegral.TaggedPrepartition I} {r : (ι → ℝ) → ↑(Set.Ioi 0)},
  l.MemBaseSet I c r π → ∀ (p : BoxIntegral.Box ι → Prop), l.MemBaseSet I c r (π.filter p)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ElabImage : Type
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.RxoIterator.step.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v : β k) (t : Std.DTreeMap.Internal.Impl α β)
  (it : Std.DTreeMap.Internal.Zipper α β) (upper : α),
  { iter := Std.DTreeMap.Internal.Zipper.cons k v t it, upper := upper }.step =
    if (compare k upper).isLT = true then
      Std.IterStep.yield { internalState := { iter := Std.DTreeMap.Internal.Zipper.prependMap t it, upper := upper } }
        ⟨k, v⟩
    else Std.IterStep.done
-- Lean.Meta.Tactic.Cleanup
_private.Lean.Meta.Tactic.Cleanup.0.Lean.Meta.cleanupCore.collectProps : StateRefT' IO.RealWorld (Bool × Lean.FVarIdSet) Lean.MetaM Unit
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.addUnits_bot : ∀ {M : Type u_1} [inst : AddMonoid M], ⊥.addUnits = ⊥
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_anti_set_of_nonpos' : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f : ι → N} [AddLeftMono N],
  (∀ (x : ι), f x ≤ 0) → Antitone fun s => ∑ x ∈ s, f x
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomain_injective : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] {f : M → N},
  Function.Injective f → Function.Injective (MonoidAlgebra.mapDomain f)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instInhabitedTheoremForm.default : Mathlib.Meta.FunProp.TheoremForm
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.RightHomotopyRel.exists_very_good_pathObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {f g : X ⟶ Y} [HomotopicalAlgebra.IsCofibrant X],
  HomotopicalAlgebra.RightHomotopyRel f g → ∃ P, P.IsVeryGood ∧ Nonempty (P.RightHomotopy f g)
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.wEquiv.symm : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x y : (MvQPF.P F).W α),
  MvQPF.WEquiv x y → MvQPF.WEquiv y x
-- Mathlib.Order.Interval.Finset.Defs
WithTop.some_mem_insertTop : ∀ {α : Type u_1} {s : Finset α} {a : α}, ↑a ∈ WithTop.insertTop s ↔ a ∈ s
-- Mathlib.CategoryTheory.Sites.CoversTop.Basic
CategoryTheory.Presheaf.FamilyOfElementsOnObjects.IsCompatible.existsUnique_section : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type w)} {I : Type u_1} {Y : I → C}
  {x : CategoryTheory.Presheaf.FamilyOfElementsOnObjects F Y},
  x.IsCompatible → J.CoversTop Y → CategoryTheory.Presheaf.IsSheaf J F → ∃! s, ∀ (i : I), ↑s (Opposite.op (Y i)) = x i
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_adjoin_coe_preimage : ∀ {R : Type uR} {A : Type uA} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A},
  Algebra.adjoin R (Subtype.val ⁻¹' s) = ⊤
-- Mathlib.Algebra.Group.Basic
add_eq_zero_iff_eq_neg' : ∀ {G : Type u_3} [inst : AddGroup G] {a b : G}, a + b = 0 ↔ b = -a
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- `ζ - 1` is prime if `ζ` is a primitive `p`-th root of unity.  -/
IsPrimitiveRoot.zeta_sub_one_prime' : ∀ {p : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [h : IsCyclotomicExtension {p} ℚ K] (hζ : IsPrimitiveRoot ζ p), Prime (hζ.toInteger - 1)
-- Init.Grind.Norm
Lean.Grind.ite_true_false : ∀ {p : Prop} {x : Decidable p}, (if p then True else False) = p
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.inr_comp_associator : ∀ (x y z : AugmentedSimplexCategory),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategoryStruct.tensorObj x y).inr z)
      (CategoryTheory.MonoidalCategoryStruct.associator x y z).hom =
    CategoryTheory.CategoryStruct.comp (y.inr z) (x.inr (CategoryTheory.MonoidalCategoryStruct.tensorObj y z))
-- Mathlib.Analysis.Normed.Module.Basic
/-- Warning: This declaration should be used judiciously.
Please consider using `IsScalarTower` instead.

This definition allows the `RestrictScalars.normedAlgebra` instance to be put directly on `E`
rather on `RestrictScalars 𝕜 𝕜' E`. This would be a very bad instance; both because `𝕜'` cannot be
inferred, and because it is likely to create instance diamonds.

See Note [reducible non-instances].
 -/
NormedAlgebra.restrictScalars : (𝕜 : Type u_1) →
  (𝕜' : Type u_2) →
    (E : Type u_3) →
      [inst : NormedField 𝕜] →
        [inst_1 : NormedField 𝕜'] →
          [NormedAlgebra 𝕜 𝕜'] → [inst_3 : SeminormedRing E] → [NormedAlgebra 𝕜' E] → NormedAlgebra 𝕜 E
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
/-- the submodule of `M.obj X`  -/
PresheafOfModules.Submodule.obj : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} →
      {M : PresheafOfModules R} → M.Submodule → (X : Cᵒᵖ) → Submodule ↑(R.obj X) ↑(M.obj X)
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.measurableSet_top : ∀ {α : Type u_1} {s : Set α}, MeasurableSet s
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
/-- The integral of the conditional expectation `μ[f|hm]` over an `m`-measurable set is equal to
the integral of `f` on that set.  -/
MeasureTheory.setIntegral_condExp : ∀ {α : Type u_1} {E : Type u_3} {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → E} {s : Set α}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] (hm : m ≤ m₀)
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  MeasureTheory.Integrable f μ → MeasurableSet s → ∫ (x : α) in s, μ[f | m] x ∂μ = ∫ (x : α) in s, f x ∂μ
-- Mathlib.ModelTheory.LanguageMap
/-- The language map extending the constant set.  -/
FirstOrder.Language.lhomWithConstantsMap : (L : FirstOrder.Language) → {α : Type w'} → {β : Type u_1} → (α → β) → (L.withConstants α →ᴸ L.withConstants β)
-- Mathlib.Topology.Sheaves.SheafCondition.PairwiseIntersections
TopCat.Presheaf.IsSheaf.isSheafPairwiseIntersections : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : TopCat} {F : TopCat.Presheaf C X} {ι : Type u_2}
  (U : ι → TopologicalSpace.Opens ↑X),
  F.IsSheaf →
    Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Functor.mapCone F (CategoryTheory.Pairwise.cocone U).op))
-- Mathlib.Topology.Separation.Hausdorff
Sigma.t2Space : ∀ {ι : Type u_4} {X : ι → Type u_3} [inst : (i : ι) → TopologicalSpace (X i)] [∀ (a : ι), T2Space (X a)],
  T2Space ((i : ι) × X i)
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.eq_of_toNormPoly : ∀ (ctx : Nat.Internal.Linear.Context) (a b : Nat.Internal.Linear.Expr),
  a.toNormPoly = b.toNormPoly → Nat.Internal.Linear.Expr.denote ctx a = Nat.Internal.Linear.Expr.denote ctx b
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of an indexed family of `n + 1` points has dimension at most `n`.  -/
finrank_vectorSpan_range_add_one_le : ∀ (k : Type u_1) {V : Type u_2} {P : Type u_3} {ι : Type u_4} [inst : DivisionRing k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : Fintype ι] [Nonempty ι] (p : ι → P),
  Module.finrank k ↥(vectorSpan k (Set.range p)) + 1 ≤ Fintype.card ι
-- Mathlib.NumberTheory.Padics.PadicNorm
/-- If a rational is not a p-adic integer, it is not an integer.  -/
padicNorm.not_int_of_not_padic_int : ∀ (p : ℕ) {a : ℚ} [hp : Fact (Nat.Prime p)], 1 < padicNorm p a → ¬a.isInt = true
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.archimedeanClassMk_pos_of_tendsto : ∀ {x : ℝ*}, Filter.Germ.Tendsto x (nhds 0) → 0 < ArchimedeanClass.mk x
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Iic_sub_one_eq_Iio : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrderBot α] [inst_3 : Sub α]
  [PredSubOrder α] [NoMinOrder α] (b : α), Finset.Iic (b - 1) = Finset.Iio b
-- Lean.Declaration
Lean.InductiveType.mk : Lean.Name → Lean.Expr → List Lean.Constructor → Lean.InductiveType
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.smul_coe : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (x y : R) [inst : CommRing R], x • ↑y = ↑(x * y)
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.mk_out_eq_add : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α) (g : α), ∃ h, Quotient.out ↑g = g + ↑h
-- Mathlib.RepresentationTheory.Coinduced
Representation.mem_coindV : ∀ {k : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  {A : Type u_4} [inst_3 : AddCommMonoid A] [inst_4 : Module k A] (σ : Representation k G A) (f : H → A),
  f ∈ Representation.coindV φ σ ↔ ∀ (g : G) (h : H), f (φ g * h) = (σ g) (f h)
-- Mathlib.Data.Fin.SuccPred
Fin.cast_lt_cast : ∀ {n m : ℕ} (eq : n = m) {a b : Fin n}, Fin.cast eq a < Fin.cast eq b ↔ a < b
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mk_cancel_common_left : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s' s : ↥S) (m : M), LocalizedModule.mk (s' • m) (s' * s) = LocalizedModule.mk m s
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.size_inter_eq_size_left : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α], (∀ a ∈ m₁, a ∈ m₂) → (m₁ ∩ m₂).size = m₁.size
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.add_weierstrassDiv : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : IsLocalRing A] (f f' g : PowerSeries A)
  [inst_2 : IsAdicComplete (IsLocalRing.maximalIdeal A) A], (f + f') /ʷ g = f /ʷ g + f' /ʷ g
-- Mathlib.Topology.Algebra.Monoid.Defs
ContinuousOn.fun_add : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [ContinuousAdd M] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f g : X → M} {s : Set X},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun i => f i + g i) s
-- Mathlib.Algebra.Category.Ring.Basic
/-- The category of rings.  -/
RingCat : Type (u + 1)
-- Mathlib.CategoryTheory.Filtered.Small
/-- The second, fully faithful part of a factoring of a functor from a small category to a filtered
category through a small filtered category.  -/
CategoryTheory.IsFiltered.SmallFilteredIntermediate.inclusion : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFilteredOrEmpty C] →
      {D : Type u₁} →
        [inst_2 : CategoryTheory.Category.{v₁, u₁} D] →
          (F : CategoryTheory.Functor D C) →
            CategoryTheory.Functor (CategoryTheory.IsFiltered.SmallFilteredIntermediate F) C
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.relabelNat' : {α : Type} → [inst : DecidableEq α] → [inst_1 : Hashable α] → Std.Sat.AIG α → Std.Sat.AIG ℕ × Std.HashMap α ℕ
-- Mathlib.CategoryTheory.Abelian.Preradical.Colon
CategoryTheory.Abelian.Preradical.shortComplexObj_X₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Preradical C) (X : C), (Φ.shortComplexObj X).X₁ = Φ.r.obj X
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.tan_lt_tan_of_lt_of_lt_pi_div_two : ∀ {x y : ℝ}, -(Real.pi / 2) < x → y < Real.pi / 2 → x < y → Real.tan x < Real.tan y
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
normEDS_ofNat : ∀ {R : Type u_1} [inst : CommRing R] (b c d : R) (n : ℕ),
  normEDS b c d ↑n = preNormEDS' (b ^ 4) c d n * if Even n then b else 1
-- Mathlib.Algebra.Polynomial.BigOperators
Polynomial.leadingCoeffHom.congr_simp : ∀ {R : Type u} [inst : Semiring R] [inst_1 : NoZeroDivisors R], Polynomial.leadingCoeffHom = Polynomial.leadingCoeffHom
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_counitIso_inv_app_right : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₂ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).counitIso.inv.app X).right =
    CategoryTheory.CategoryStruct.id X.right
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negDblY_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} [inst_1 : DecidableEq F] {P Q : Fin 3 → F},
  W.Equation P →
    W.Equation Q →
      P 2 ≠ 0 →
        Q 2 ≠ 0 →
          P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 →
            P 1 * Q 2 ^ 3 ≠ W.negY Q * P 2 ^ 3 →
              W.negDblY P / W.dblZ P ^ 3 =
                W.toAffine.negAddY (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3)
                  (W.toAffine.slope (P 0 / P 2 ^ 2) (Q 0 / Q 2 ^ 2) (P 1 / P 2 ^ 3) (Q 1 / Q 2 ^ 3))
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Measure.setLIntegral_condKernel_eq_measure_prod : ∀ {β : Type u_1} {Ω : Type u_2} {mβ : MeasurableSpace β} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] {ρ : MeasureTheory.Measure (β × Ω)} [inst_3 : MeasureTheory.IsFiniteMeasure ρ] {s : Set β},
  MeasurableSet s → ∀ {t : Set Ω}, MeasurableSet t → ∫⁻ (b : β) in s, (ρ.condKernel b) t ∂ρ.fst = ρ (s ×ˢ t)
-- Mathlib.Algebra.Ring.Subsemiring.Basic
RingHom.injective_codRestrict : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {σS : Type u_2}
  [inst_2 : SetLike σS S] [inst_3 : SubsemiringClass σS S] {f : R →+* S} {s : σS} {h : ∀ (x : R), f x ∈ s},
  Function.Injective ⇑(f.codRestrict s h) ↔ Function.Injective ⇑f
-- Mathlib.Algebra.Group.Equiv.Defs
/-- **Alias** of `EmbeddingLike.map_eq_one_iff`. -/
MulEquivClass.map_eq_one_iff : ∀ {F : Type u_1} {M : Type u_4} {N : Type u_5} [inst : One M] [inst_1 : One N] [inst_2 : FunLike F M N]
  [EmbeddingLike F M N] [OneHomClass F M N] {f : F} {x : M}, f x = 1 ↔ x = 1
-- Batteries.Data.Float.Lemmas
Float32.ofBits_toBits : ∀ (f : Float32), Float32.ofBits f.toBits = f
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instSMul : {S : Type u_2} → {R : Type u_3} → {A : Type u_4} → [SMul S R] → [SMul S A] → SMul S (Unitization R A)
-- Init.Data.UInt.Lemmas
instCommutativeUSizeHAdd : Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The map `E^n(f₁, f₂, f₃) ⟶ Z^n(f₁, f₂ ≫ f₃)`.  -/
CategoryTheory.Abelian.SpectralObject.EToCycles : {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₃) →
                      CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃ →
                        (n₀ n₁ n₂ : ℤ) →
                          (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.EToCycles._auto_1) →
                            (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.EToCycles._auto_3) →
                              X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.cycles f₁ f₂₃ n₁
-- Init.Data.Vector.Lemmas
Vector.back?_eq_some_iff : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {a : α},
  xs.back? = some a ↔ ∃ (w : 0 < n), ∃ ys, xs = Vector.cast ⋯ (ys.push a)
-- Mathlib.Topology.Algebra.InfiniteSum.Module
/-- **Alias** of `ContinuousLinearMap.hasSum`.

---

Applying a continuous linear map commutes with taking an (infinite) sum.  -/
HasSum.mapL : ∀ {ι : Type u_5} {R : Type u_7} {R₂ : Type u_8} {M : Type u_9} {M₂ : Type u_10} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : Module R₂ M₂] [inst_6 : TopologicalSpace M] [inst_7 : TopologicalSpace M₂] {σ : R →+* R₂}
  {L : SummationFilter ι} {f : ι → M} (φ : M →SL[σ] M₂) {x : M}, HasSum f x L → HasSum (fun b => φ (f b)) (φ x) L
-- Lean.Server.References
/-- URI for `mod`.  -/
Lean.Server.References.MatchedDefinition.modUri : {α : Type} → Lean.Server.References.MatchedDefinition α → Lean.Lsp.DocumentUri
-- Mathlib.Analysis.Convex.Caratheodory
/-- A more explicit version of `convexHull_eq_union`.  -/
eq_pos_convex_span_of_mem_convexHull : ∀ {𝕜 : Type u_1} {E : Type u} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E} {x : E},
  x ∈ (convexHull 𝕜) s →
    ∃ ι x_1 z w, Set.range z ⊆ s ∧ AffineIndependent 𝕜 z ∧ (∀ (i : ι), 0 < w i) ∧ ∑ i, w i = 1 ∧ ∑ i, w i • z i = x
-- Mathlib.LinearAlgebra.Dimension.ErdosKaplansky
/-- The **Erdős-Kaplansky Theorem** over a field.  -/
rank_dual_eq_card_dual_of_aleph0_le_rank : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  Cardinal.aleph0 ≤ Module.rank K V → Module.rank K (V →ₗ[K] K) = Cardinal.mk (V →ₗ[K] K)
-- Mathlib.Data.List.Chain
List.isChain_nil : ∀ {α : Type u_1} {R : α → α → Prop}, List.IsChain R []
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.eval_apply : ∀ {ι : Type u_5} {X : ι → Type u_6} [inst : (i : ι) → TopologicalSpace (X i)] (i : ι) [inst_1 : DiscreteTopology (X i)]
  (f : (i : ι) → X i), (LocallyConstant.eval i) f = f i
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
/-- Bundled `n` times continuously differentiable sections of a vector bundle.
Denoted as `Cₛ^n⟮I; F, V⟯` within the `Manifold` namespace.  -/
ContMDiffSection : {𝕜 : 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] →
                      (F : Type u_5) →
                        [inst_6 : NormedAddCommGroup F] →
                          [NormedSpace 𝕜 F] →
                            WithTop ℕ∞ →
                              (V : M → Type u_6) →
                                [inst : TopologicalSpace (Bundle.TotalSpace F V)] →
                                  [inst_7 : (x : M) → TopologicalSpace (V x)] → [FiberBundle F V] → Type (max u_4 u_6)
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval₂_zero : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+* S) (x : S), Polynomial.eval₂ f x 0 = 0
-- Lean.Environment
_private.Lean.Environment.0.Lean.ImportedModule.getData? : Lean.ImportedModule✝ → Lean.OLeanLevel → Option Lean.ModuleData
-- Mathlib.Combinatorics.Graph.Simple
/-- A `Simple` graph is a `Loopless` graph where no pair of vertices are the ends of more than one
edge.  -/
Graph.Simple : {α : Type u_1} → {β : Type u_2} → Graph α β → Prop
-- Mathlib.CategoryTheory.Grothendieck
/-- Making the equality of functors into an isomorphism. Note: we should avoid equality of functors
if possible, and we should prefer `mapIdIso` to `map_id_eq` whenever we can.  -/
CategoryTheory.Grothendieck.mapIdIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C CategoryTheory.Cat} →
      (CategoryTheory.Grothendieck.map (CategoryTheory.CategoryStruct.id F)).toCatHom ≅
        CategoryTheory.CategoryStruct.id (CategoryTheory.Cat.of (CategoryTheory.Grothendieck F))
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.isNone_getElem?_toArray_rio_eq : ∀ {n i : ℕ}, ((*...n).toArray[i]?.isNone = true) = (n ≤ i)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_lift_associator_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X Y Z W : C} (f : X ⟶ Y) (g : X ⟶ Z) (h : X ⟶ W),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f (CategoryTheory.CartesianMonoidalCategory.lift g h))
      (CategoryTheory.MonoidalCategoryStruct.associator Y Z W).inv =
    CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CartesianMonoidalCategory.lift f g) h
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
/-- The identity map, as a bundled affine map of convex spaces.  -/
Convexity.ConvexSpace.AffineMap.id : {R : Type u_1} →
  [inst : PartialOrder R] →
    [inst_1 : Semiring R] →
      [inst_2 : IsStrictOrderedRing R] →
        (X : Type u_2) → [inst_3 : Convexity.ConvexSpace R X] → Convexity.ConvexSpace.AffineMap R X X
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.parallelPair_map_left : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y),
  (CategoryTheory.Limits.parallelPair f g).map CategoryTheory.Limits.WalkingParallelPairHom.left = f
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.combine.injEq : ∀ {s t : Lean.Omega.Constraint} {c : Lean.Omega.Coeffs} (j : Lean.Elab.Tactic.Omega.Justification s c)
  (k : Lean.Elab.Tactic.Omega.Justification t c) (j_1 : Lean.Elab.Tactic.Omega.Justification s c)
  (k_1 : Lean.Elab.Tactic.Omega.Justification t c), (j.combine k = j_1.combine k_1) = (j = j_1 ∧ k = k_1)
-- Mathlib.GroupTheory.Order.Min
AddMonoid.le_minOrder_iff_forall_addSubgroup : ∀ {G : Type u_1} [inst : AddGroup G] {n : ℕ∞},
  n ≤ AddMonoid.minOrder G ↔ ∀ ⦃s : AddSubgroup G⦄, s ≠ ⊥ → (↑s).Finite → n ≤ ↑(Nat.card ↥s)
-- Mathlib.Data.Set.Basic
Set.inter_subset_left : ∀ {α : Type u} {s t : Set α}, s ∩ t ⊆ s
-- Lean.Meta.Tactic.Assert
/-- Convert the given goal `Ctx |- target` into `Ctx |- type -> target`.
It assumes `val` has type `type`  -/
Lean.MVarId.assert : Lean.MVarId → Lean.Name → Lean.Expr → Lean.Expr → Lean.MetaM Lean.MVarId
-- Init.Data.SInt.Lemmas
Int32.ofInt_tdiv : ∀ {a b : ℤ},
  Int32.minValue.toInt ≤ a →
    a ≤ Int32.maxValue.toInt →
      Int32.minValue.toInt ≤ b → b ≤ Int32.maxValue.toInt → Int32.ofInt (a.tdiv b) = Int32.ofInt a / Int32.ofInt b
-- Mathlib.Order.CompleteLattice.Basic
isLUB_biSup : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {s : Set β} {f : β → α}, IsLUB (f '' s) (⨆ x ∈ s, f x)
-- Mathlib.Topology.Algebra.Group.GroupTopology
AddGroupTopology.instInhabited : {α : Type u} → [inst : AddGroup α] → Inhabited (AddGroupTopology α)