mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.SheafOfTypes
CategoryTheory.Precoverage.ZeroHypercover.Hom.isSheafFor_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {K : CategoryTheory.Precoverage C} [inst_2 : K.IsStableUnderBaseChange] {S : C}
  {F : CategoryTheory.Functor Cᵒᵖ (Type u_2)} {𝒰 : K.ZeroHypercover S} {𝒱 : K.ZeroHypercover S}
  (f : CategoryTheory.Precoverage.ZeroHypercover.Hom K 𝒰 𝒱),
  CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒰.X 𝒰.f) →
    (∀ {X : C} (f : X ⟶ S),
        CategoryTheory.Presieve.IsSeparatedFor F
          (CategoryTheory.Presieve.ofArrows (CategoryTheory.Precoverage.ZeroHypercover.pullback₂ f 𝒰).X
            (CategoryTheory.Precoverage.ZeroHypercover.pullback₂ f 𝒰).f)) →
      CategoryTheory.Presieve.IsSheafFor F (CategoryTheory.Presieve.ofArrows 𝒱.X 𝒱.f)
-- Mathlib.CategoryTheory.Extensive
CategoryTheory.FinitaryPreExtensive.hasFiniteCoproducts : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.FinitaryPreExtensive C],
  CategoryTheory.Limits.HasFiniteCoproducts C
-- Mathlib.Order.Hom.CompleteLattice
instCoeTCSSupHomOfSSupHomClass.eq_1 : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : SupSet α] [inst_2 : SupSet β]
  [inst_3 : sSupHomClass F α β], instCoeTCSSupHomOfSSupHomClass = { coe := fun f => { toFun := ⇑f, map_sSup' := ⋯ } }
-- Mathlib.Topology.MetricSpace.Infsep
Set.Nontrivial.einfsep_lt_top : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {s : Set α}, s.Nontrivial → s.einfsep < ⊤
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
rTensor.inverse_of_rightInverse_apply : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (Q : Type u_5) [inst_7 : AddCommGroup Q] [inst_8 : Module R Q]
  (hfg : Function.Exact ⇑f ⇑g) {h : P → N} (hgh : Function.RightInverse h ⇑g) (y : TensorProduct R N Q),
  (rTensor.inverse_of_rightInverse Q hfg hgh) ((LinearMap.rTensor Q g) y) = Submodule.Quotient.mk y
-- Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice
/-- Cartesian monoidal structure for the preorder category of a meet-semilattice with
a greatest element.  -/
CategoryTheory.SemilatticeInf.cartesianMonoidalCategory : (C : Type u) → [inst : SemilatticeInf C] → [OrderTop C] → CategoryTheory.CartesianMonoidalCategory C
-- Mathlib.Tactic.FieldSimp
Mathlib.Tactic.FieldSimp.DenomCondition.nonzero : {v : Lean.Level} → {M : Q(Type v)} → {iM : Q(GroupWithZero «$M»)} → Mathlib.Tactic.FieldSimp.DenomCondition iM
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_of_mem_insertIfNew : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k a : α} {v : β}, a ∈ m.insertIfNew k v → (k == a) = false → a ∈ m
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem?_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Option γ} {k k' : α},
  m.getKey? k = some k' → (Std.ExtHashMap.filterMap f m)[k]? = m[k]?.bind (f k')
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instAddCommGroup : {α : Type u_1} → [AddCommGroup α] → AddCommGroup (Lex α)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
instCommGroupObjOppositeOpensCarrierOfPresheafSmoothSheaf : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_2} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_3} →
            [inst_3 : TopologicalSpace HM] →
              (IM : ModelWithCorners 𝕜 EM HM) →
                {E : Type u_4} →
                  [inst_4 : NormedAddCommGroup E] →
                    [inst_5 : NormedSpace 𝕜 E] →
                      {H : Type u_5} →
                        [inst_6 : TopologicalSpace H] →
                          (I : ModelWithCorners 𝕜 E H) →
                            (M : Type u) →
                              [inst_7 : TopologicalSpace M] →
                                [inst_8 : ChartedSpace HM M] →
                                  (A : Type u) →
                                    [inst_9 : TopologicalSpace A] →
                                      [inst_10 : ChartedSpace H A] →
                                        [inst_11 : CommGroup A] →
                                          [LieGroup I (↑⊤) A] →
                                            (U : (TopologicalSpace.Opens ↑(TopCat.of M))ᵒᵖ) →
                                              CommGroup ((smoothSheaf IM I M A).presheaf.obj U)
-- Mathlib.FieldTheory.LinearDisjoint
/-- If `A` is an intermediate field of `E / F`, `L` is an abstract field between `E / F`,
such that they are linearly disjoint over `F`, and one of them is algebraic, then
`[L : F] * [E : L(A)] = [E : A]`.  -/
IntermediateField.LinearDisjoint.lift_rank_right_mul_lift_adjoin_rank_eq_of_isAlgebraic : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {A : IntermediateField F E}
  {L : Type w} [inst_3 : Field L] [inst_4 : Algebra F L] [inst_5 : Algebra L E] [inst_6 : IsScalarTower F L E],
  A.LinearDisjoint L →
    Algebra.IsAlgebraic F ↥A ∨ Algebra.IsAlgebraic F L →
      Cardinal.lift.{v, w} (Module.rank F L) * Cardinal.lift.{w, v} (Module.rank (↥(IntermediateField.adjoin L ↑A)) E) =
        Cardinal.lift.{w, v} (Module.rank (↥A) E)
-- Mathlib.RepresentationTheory.Subrepresentation
RestrictScalars.lsmul.eq_1 : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : Semiring S] [inst_1 : AddCommMonoid M] [inst_2 : CommSemiring R]
  [inst_3 : Algebra R S] [inst_4 : Module S M], RestrictScalars.lsmul R S M = Algebra.lsmul R R (RestrictScalars R S M)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.integrable_of_lintegral_enorm_bounded : ∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
  [inst_1 : NormedAddCommGroup E] [l.NeBot] [l.IsCountablyGenerated] {φ : ι → Set α},
  MeasureTheory.AECover μ l φ →
    ∀ {f : α → E} (I : ℝ),
      MeasureTheory.AEStronglyMeasurable f μ →
        (∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ‖f x‖ₑ ∂μ ≤ ENNReal.ofReal I) → MeasureTheory.Integrable f μ
-- Mathlib.RingTheory.MvPowerSeries.Expand
MvPowerSeries.expand_C : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] (p : ℕ) (hp : p ≠ 0) (r : R),
  (MvPowerSeries.expand p hp) (MvPowerSeries.C r) = MvPowerSeries.C r
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
Metric.isUniformEmbedding_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {f : α → β},
  IsUniformEmbedding f ↔
    Function.Injective f ∧ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, dist (f a) (f b) < ε → dist a b < δ
-- Aesop.Forward.State
Aesop.instHashablePatSubstSource : Hashable Aesop.PatSubstSource
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.comp_mk₀_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y : C} {a : M} (f : CategoryTheory.ShiftedHom X Y a) (m₀ : M)
  (hm₀ : m₀ = 0), f.comp (CategoryTheory.ShiftedHom.mk₀ m₀ hm₀ (CategoryTheory.CategoryStruct.id Y)) ⋯ = f
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- The mapping `toWeakDualBCNN` from finite Borel measures to the weak dual of `Ω →ᵇ ℝ≥0` is
injective, if in the underlying space `Ω`, indicator functions of closed sets have decreasing
approximations by sequences of continuous functions (in particular if `Ω` is pseudometrizable).  -/
MeasureTheory.FiniteMeasure.injective_toWeakDualBCNN : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [HasOuterApproxClosed Ω]
  [inst_3 : BorelSpace Ω], Function.Injective MeasureTheory.FiniteMeasure.toWeakDualBCNN
-- Init.Data.String.Lemmas.Iterate
String.toList_positionsFrom : ∀ {s : String} {p : s.Pos}, (s.positionsFrom p).toList = String.Model.positionsFrom p
-- Mathlib.Topology.MetricSpace.IsometricSMul
instIsIsometricSMulForall : ∀ {M : Type u} {ι : Type u_3} {X : ι → Type u_2} [inst : Fintype ι] [inst_1 : (i : ι) → SMul M (X i)]
  [inst_2 : (i : ι) → PseudoEMetricSpace (X i)] [∀ (i : ι), IsIsometricSMul M (X i)], IsIsometricSMul M ((i : ι) → X i)
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_eq_zero : ∀ {a : Cardinal.{u_1}}, a.ord = 0 ↔ a = 0
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.opFunctorCompFst_inv_app : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) (X : (CategoryTheory.Comma L R)ᵒᵖ),
  (CategoryTheory.Comma.opFunctorCompFst L R).inv.app X =
    CategoryTheory.CategoryStruct.id (Opposite.op (Opposite.unop X).right)
-- Mathlib.Order.Bounded
Set.bounded_lt_Iio : ∀ {α : Type u_1} [inst : Preorder α] (a : α), Set.Bounded (fun x1 x2 => x1 < x2) (Set.Iio a)
-- Mathlib.Data.PNat.Basic
OrderIso.pnatIsoNat_symm_apply : ⇑OrderIso.pnatIsoNat.symm = Nat.succPNat
-- Mathlib.CategoryTheory.GradedObject.Bifunctor
/-- The isomorphism `mapBifunctorMapObj F p X₁ Y₁ ≅ mapBifunctorMapObj F p X₂ Y₂`
induced by isomorphisms `X₁ ≅ X₂` and `Y₁ ≅ Y₂`.  -/
CategoryTheory.GradedObject.mapBifunctorMapMapIso : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) →
              {I : Type u_4} →
                {J : Type u_5} →
                  {K : Type u_6} →
                    (p : I × J → K) →
                      {X₁ X₂ : CategoryTheory.GradedObject I C₁} →
                        {Y₁ Y₂ : CategoryTheory.GradedObject J C₂} →
                          [inst_3 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₁).obj Y₁).HasMap p] →
                            [inst_4 : (((CategoryTheory.GradedObject.mapBifunctor F I J).obj X₂).obj Y₂).HasMap p] →
                              (X₁ ≅ X₂) →
                                (Y₁ ≅ Y₂) →
                                  (CategoryTheory.GradedObject.mapBifunctorMapObj F p X₁ Y₁ ≅
                                    CategoryTheory.GradedObject.mapBifunctorMapObj F p X₂ Y₂)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_filter_not_contains : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((_ : α) × β)} {l₂ : List α} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    ∀ {h₁ : Std.Internal.List.containsKey k (List.filter (fun p => !l₂.contains p.fst) l₁) = true}
      {h₂ : Std.Internal.List.containsKey k l₁ = true},
      Std.Internal.List.getValue k (List.filter (fun p => !l₂.contains p.fst) l₁) h₁ =
        Std.Internal.List.getValue k l₁ h₂
-- Std.Data.HashMap.Raw
/-- Hash maps without a bundled well-formedness invariant, suitable for use in nested
inductive types. The well-formedness invariant is called `Raw.WF`. When in doubt, prefer `HashMap`
over `HashMap.Raw`. Lemmas about the operations on `Std.Data.HashMap.Raw` are available in the
module `Std.Data.HashMap.RawLemmas`.

This is a simple separate-chaining hash table. The data of the hash map consists of a cached size
and an array of buckets, where each bucket is a linked list of key-value pairs. The number of buckets
is always a power of two. The hash map doubles its size upon inserting an element such that the
number of elements is more than 75% of the number of buckets.

The hash table is backed by an `Array`. Users should make sure that the hash map is used linearly to
avoid expensive copies.

The hash map uses `==` (provided by the `BEq` typeclass) to compare keys and `hash` (provided by
the `Hashable` typeclass) to hash them. To ensure that the operations behave as expected, `==`
should be an equivalence relation and `a == b` should imply `hash a = hash b` (see also the
`EquivBEq` and `LawfulHashable` typeclasses). Both of these conditions are automatic if the BEq
instance is lawful, i.e., if `a == b` implies `a = b`.

Dependent hash maps, in which keys may occur in their values' types, are available as
`Std.Data.Raw.DHashMap`.
 -/
Std.HashMap.Raw : Type u → Type v → Type (max u v)
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a group `G` is a subset containing 1, closed under multiplication
and closed under multiplicative inverse. 

[Wikidata Q466109](https://www.wikidata.org/wiki/Q466109) -/
Subgroup : (G : Type u_3) → [Group G] → Type u_3
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.ranObjObjIsoLimit_hom_π : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H]
  [inst_3 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F] (F : CategoryTheory.Functor C H)
  [inst_4 : L.HasPointwiseRightKanExtension F] (X : D) (f : CategoryTheory.StructuredArrow X L),
  CategoryTheory.CategoryStruct.comp (L.ranObjObjIsoLimit F X).hom
      (CategoryTheory.Limits.limit.π ((CategoryTheory.StructuredArrow.proj X L).comp F) f) =
    CategoryTheory.CategoryStruct.comp ((L.ran.obj F).map f.hom) ((L.ranCounit.app F).app f.right)
-- Lean.Util.ParamMinimizer
_private.Lean.Util.ParamMinimizer.0.Lean.Util.ParamMinimizer.main : {m : Type → Type} → [Monad m] → Lean.Util.ParamMinimizer.M✝ m Unit
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Id for `OfNatModule.Q`  -/
Lean.Meta.Grind.Arith.Linear.NatStruct.structId : Lean.Meta.Grind.Arith.Linear.NatStruct → ℕ
-- Init.Data.SInt.Bitwise
Int8.toInt32_and : ∀ (a b : Int8), (a &&& b).toInt32 = a.toInt32 &&& b.toInt32
-- Mathlib.Data.List.Basic
List.getLast_congr : ∀ {α : Type u} {l₁ l₂ : List α} (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []), l₁ = l₂ → l₁.getLast h₁ = l₂.getLast h₂
-- Mathlib.Topology.UniformSpace.CompareReals
CompareReals.instInhabitedQ : Inhabited CompareReals.Q
-- Mathlib.Order.Filter.Basic
Filter.mem_generate_of_mem : ∀ {α : Type u} {s : Set (Set α)} {U : Set α}, U ∈ s → U ∈ Filter.generate s
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.eq_1 : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α),
  eVariationOn f s = ⨆ p, ∑ i ∈ Finset.range p.1, edist (f (↑p.2 (i + 1))) (f (↑p.2 i))
-- Init.Data.String.Lemmas.Iterate
String.Slice.Model.positionsFrom_eq_cons : ∀ {s : String.Slice} {p : s.Pos} (hp : p ≠ s.endPos),
  String.Slice.Model.positionsFrom p = ⟨p, hp⟩ :: String.Slice.Model.positionsFrom (p.next hp)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.not_step_nil : ∀ {α : Type u} {L : List (α × Bool)}, ¬FreeAddGroup.Red.Step [] L
-- Mathlib.Order.Filter.Ker
Filter.ker_iSup : ∀ {ι : Sort u_1} {α : Type u_2} (f : ι → Filter α), (⨆ i, f i).ker = ⋃ i, (f i).ker
-- Mathlib.RingTheory.LinearDisjoint
Subalgebra.LinearDisjoint.algebraMap_basisOfBasisRight_apply : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {A B : Subalgebra R S} (H : A.LinearDisjoint B) (H' : A ⊔ B = ⊤) {ι : Type u_1} (b : Module.Basis ι R ↥B) (i : ι),
  (H.basisOfBasisRight H' b) i = (algebraMap (↥B) S) (b i)
-- Mathlib.Algebra.Group.Defs
add_eq_zero_comm : ∀ {M : Type u_2} [inst : AddZero M] [IsDedekindFiniteAddMonoid M] {a b : M}, a + b = 0 ↔ b + a = 0
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.HomEquiv.below.trans : ∀ {C : Type u}
  {motive :
    {X Y : CategoryTheory.FreeMonoidalCategory C} →
      (a a_1 : X.Hom Y) → CategoryTheory.FreeMonoidalCategory.HomEquiv a a_1 → Prop}
  {X Y : CategoryTheory.FreeMonoidalCategory C} {f g h : X.Hom Y} (a : CategoryTheory.FreeMonoidalCategory.HomEquiv f g)
  (a_1 : CategoryTheory.FreeMonoidalCategory.HomEquiv g h),
  CategoryTheory.FreeMonoidalCategory.HomEquiv.below a →
    motive f g a →
      CategoryTheory.FreeMonoidalCategory.HomEquiv.below a_1 →
        motive g h a_1 → CategoryTheory.FreeMonoidalCategory.HomEquiv.below ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.Const.alterKey.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (v : β) → motive (some v)),
  (match none with
    | none => h_1 ()
    | some v => h_2 v) =
    h_1 ()
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise scalar multiplication of `f` and
`g`, which monovary together, is unchanged by a permutation if and only if `f ∘ σ` and `g` monovary
together. Stated by permuting the entries of `g`.  -/
Monovary.sum_comp_perm_smul_eq_sum_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Monovary f g → (∑ i, f (σ i) • g i = ∑ i, f i • g i ↔ Monovary (f ∘ ⇑σ) g)
-- Mathlib.Order.WellFounded
not_acc_iff_exists_descending_chain : ∀ {α : Sort u_1} {r : α → α → Prop} {x : α}, ¬Acc r x ↔ ∃ f, f 0 = x ∧ ∀ (n : ℕ), r (f (n + 1)) (f n)
-- Std.Data.ExtDTreeMap.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.ExtDTreeMap.Const.entryAtIdx? : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → ℕ → Option (α × β)
-- Init.Control.Except
/-- Returns `true` if the value is `Except.ok`, `false` otherwise.  -/
Except.toBool : {ε : Type u} → {α : Type u_1} → Except ε α → Bool
-- Mathlib.Topology.Order.LeftRight
nhdsWithin_uIoo_right_le_nhdsNE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] {a b : α},
  nhdsWithin b (Set.uIoo a b) ≤ nhdsWithin b {b}ᶜ
-- Mathlib.Algebra.Algebra.Operations
Submodule.prod_span : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {ι : Type u_1}
  (s : Finset ι) (M : ι → Set A), ∏ i ∈ s, Submodule.span R (M i) = Submodule.span R (∏ i ∈ s, M i)
-- Lean.DocString.Syntax
/-- A block-level command, which invokes an extension during documentation processing.

The `NAME` is an identifier that determines which command is being used, akin to a function name.
Each of the `ARGS` may have the following forms:
* A value, which is a string literal, natural number, or identifier
* A named argument, of the form `(NAME := VALUE)`
* A flag, of the form `+NAME` or `-NAME`
 -/
Lean.Doc.Syntax.command : Lean.ParserDescr
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The mean of a real Gaussian distribution `gaussianReal μ v` is its mean parameter `μ`.  -/
ProbabilityTheory.integral_id_gaussianReal : ∀ {μ : ℝ} {v : NNReal}, ∫ (x : ℝ), x ∂ProbabilityTheory.gaussianReal μ v = μ
-- Init.Data.UInt.Bitwise
UInt32.or_zero : ∀ {a : UInt32}, a ||| 0 = a
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.symm_mapsTo : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β},
  e.IsImage s t → Set.MapsTo (↑e.symm) (e.target ∩ t) (e.source ∩ s)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- "iff" version of `Multipliable.of_nat_of_neg_add_one`.  -/
multipliable_int_iff_multipliable_nat_and_neg_add_one : ∀ {G : Type u_2} [inst : CommGroup G] [inst_1 : UniformSpace G] [IsUniformGroup G] [CompleteSpace G] {f : ℤ → G},
  Multipliable f ↔ (Multipliable fun n => f ↑n) ∧ Multipliable fun n => f (-(↑n + 1))
-- Mathlib.LinearAlgebra.Alternating.Basic
LinearMap.compAlternatingMap_codRestrict : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} {N₂ : Type u_11} [inst_5 : AddCommMonoid N₂]
  [inst_6 : Module R N₂] (g : N →ₗ[R] N₂) (f : M [⋀^ι]→ₗ[R] N) (p : Submodule R N₂) (h : ∀ (c : N), g c ∈ p),
  (LinearMap.codRestrict p g h).compAlternatingMap f = (g.compAlternatingMap f).codRestrict p ⋯
-- Mathlib.Analysis.Normed.Group.Hom
/-- Composition of normed groups hom as an additive group morphism.  -/
NormedAddGroupHom.compHom : {V₁ : Type u_2} →
  {V₂ : Type u_3} →
    {V₃ : Type u_4} →
      [inst : SeminormedAddCommGroup V₁] →
        [inst_1 : SeminormedAddCommGroup V₂] →
          [inst_2 : SeminormedAddCommGroup V₃] →
            NormedAddGroupHom V₂ V₃ →+ NormedAddGroupHom V₁ V₂ →+ NormedAddGroupHom V₁ V₃
-- Mathlib.AlgebraicGeometry.Morphisms.LocalIso
AlgebraicGeometry.isLocalIso_iff : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y),
  AlgebraicGeometry.IsLocalIso f ↔
    ∀ (x : ↥X), ∃ U, x ∈ U ∧ AlgebraicGeometry.IsOpenImmersion (CategoryTheory.CategoryStruct.comp U.ι f)
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.liftExpand_of : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_3}
  [inst_2 : AddAction R X] {C : Sort u_2} {P : X → ↥S → C}
  {hP : ∀ (r : X) (t : R) (s : ↥S) (ht : t + ↑s ∈ S), P r s = P (t +ᵥ r) ⟨t + ↑s, ht⟩} (r : X) (s : ↥S),
  AddOreLocalization.liftExpand P hP (r -ₒ s) = P r s
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
/-- `Finitary` matroids have a cardinality-valued rank function.  -/
Matroid.invariantCardinalRank_of_finitary : ∀ {α : Type u} {M : Matroid α} [M.Finitary], M.InvariantCardinalRank
-- Init.Data.Int.DivMod.Lemmas
Int.add_bmod_bmod : ∀ {x y : ℤ} {n : ℕ}, (x + y.bmod n).bmod n = (x + y).bmod n
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryLT_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF) (h : t₁.Equiv t₂) {k : α} {he : ∃ a ∈ t₁, compare a k = Ordering.lt},
  Std.DTreeMap.Internal.Impl.Const.getEntryLT k t₁ ⋯ he = Std.DTreeMap.Internal.Impl.Const.getEntryLT k t₂ ⋯ ⋯
-- Mathlib.CategoryTheory.Monoidal.Cartesian.CommGrp_
CategoryTheory.yonedaCommGrpGrpObj_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : CategoryTheory.CommGrp C) {H I : (CategoryTheory.Grp C)ᵒᵖ}
  (f : H ⟶ I),
  (CategoryTheory.yonedaCommGrpGrpObj G).map f =
    CommGrpCat.ofHom { toFun := fun x => CategoryTheory.CategoryStruct.comp f.unop x, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.GroupTheory.GroupAction.MultiplePrimitivity
MulAction.instIsMultiplyPretransitiveOfIsMultiplyPreprimitive : ∀ (M : Type u_1) (α : Type u_2) [inst : Group M] [inst_1 : MulAction M α] (n : ℕ)
  [MulAction.IsMultiplyPreprimitive M α n], MulAction.IsMultiplyPretransitive M α n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ReferenceParams.mk : Lean.Lsp.TextDocumentPositionParams → Lean.Lsp.ReferenceContext → Lean.Lsp.ReferenceParams
-- Mathlib.CategoryTheory.Presentable.StrongGenerator
CategoryTheory.ObjectProperty.isCardinalFiltered_costructuredArrow_colimitsCardinalClosure_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [CategoryTheory.Limits.HasColimitsOfSize.{w, w, v, u} C] (X : C),
  CategoryTheory.IsCardinalFiltered (CategoryTheory.CostructuredArrow (P.colimitsCardinalClosure κ).ι X) κ
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.ShrinkHoms.equivalence_counitIso : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  (CategoryTheory.ShrinkHoms.equivalence C).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun x =>
        CategoryTheory.Iso.refl
          (((CategoryTheory.ShrinkHoms.inverse C).comp (CategoryTheory.ShrinkHoms.functor C)).obj x))
      ⋯