mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.OrderClosed
/-- The set of monotone functions is closed.  -/
isClosed_monotone : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α]
  [inst_2 : Preorder β], IsClosed {f | Monotone f}
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.instHAddOffset_2 : HAdd Std.Time.PlainDateTime Std.Time.Hour.Offset Std.Time.PlainDateTime
-- Mathlib.Algebra.Algebra.Operations
Submodule.mul_toAddSubmonoid : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M N : Submodule R A), (M * N).toAddSubmonoid = M.toAddSubmonoid * N.toAddSubmonoid
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- Three points are affinely independent if and only if they are not collinear.  -/
affineIndependent_iff_not_collinear_of_ne : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {p : Fin 3 → P} {i₁ i₂ i₃ : Fin 3},
  i₁ ≠ i₂ → i₁ ≠ i₃ → i₂ ≠ i₃ → (AffineIndependent k p ↔ ¬Collinear k {p i₁, p i₂, p i₃})
-- Lean.Server.FileWorker.RequestHandling
_private.Lean.Server.FileWorker.RequestHandling.0.Lean.Server.FileWorker.handleFoldingRange.addRanges.popRanges : Lean.FileMap →
  List (ℕ × Option String.Pos.Raw) →
    Lean.Syntax →
      List Lean.Syntax →
        ℕ → List (ℕ × Option String.Pos.Raw) → StateT (Array Lean.Lsp.FoldingRange) Lean.Server.RequestM Unit
-- Mathlib.Order.ConditionallyCompletePartialOrder.Indexed
ciInf_const : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompletePartialOrderInf α] [hι : Nonempty ι] {a : α}, ⨅ x, a = a
-- Mathlib.Data.Num.Lemmas
Num.to_nat_to_int : ∀ (n : Num), ↑↑n = ↑n
-- Mathlib.Data.Finsupp.Interval
Finsupp.card_Iio : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : IsBotZeroClass α]
  [inst_3 : OrderBot α] [inst_4 : LocallyFiniteOrder α] [inst_5 : DecidableEq ι] [inst_6 : DecidableEq α] (f : ι →₀ α),
  (Finset.Iio f).card = ∏ i ∈ f.support, (Finset.Iic (f i)).card - 1
-- Init.Data.Iterators.Lemmas.Monadic.Basic
_private.Init.Data.Iterators.Lemmas.Monadic.Basic.0.Std.IterM.inductSkips.eq_def : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β]
  [inst_1 : Std.Iterators.Productive α m] (motive : Std.IterM m β → Sort x)
  (step :
    (it : Std.IterM m β) →
      ({it' : Std.IterM m β} → it.IsPlausibleStep (Std.IterStep.skip it') → motive it') → motive it)
  (it : Std.IterM m β),
  Std.IterM.inductSkips motive step it = step it fun {it'} x => Std.IterM.inductSkips motive step it'
-- Mathlib.CategoryTheory.Abelian.Opposite
/-- The kernel of `g.unop` is the opposite of `cokernel g`.  -/
CategoryTheory.kernelUnopOp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {A B : Cᵒᵖ} → (g : A ⟶ B) → Opposite.op (CategoryTheory.Limits.kernel g.unop) ≅ CategoryTheory.Limits.cokernel g
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.dblX_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.dblX P = (P 0 ^ 2) ^ 2
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.restrictScalars_of_isIntegral : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Ring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra R A] [inst_5 : Algebra S A] [IsScalarTower R S A] [NoZeroDivisors S]
  [int : Algebra.IsIntegral R S] {a : A}, IsAlgebraic S a → IsAlgebraic R a
-- Mathlib.Topology.Algebra.InfiniteSum.Order
le_hasSum' : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α]
  [CanonicallyOrderedAdd α] [inst_4 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α},
  HasSum f a → ∀ (i : ι), f i ≤ a
-- Std.Http.Data.Body.Empty
/-- Builds a request with no body.
 -/
Std.Http.Request.Builder.empty : Std.Http.Request.Builder → Std.Async.Async (Std.Http.Request Std.Http.Body.Empty)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- The forget functor `SheafOfModules R ⥤ PresheafOfModules R.val` is fully faithful.  -/
SheafOfModules.fullyFaithfulForget : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) → (SheafOfModules.forget R).FullyFaithful
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- The Gaussian pdf is positive when the variance is not zero.  -/
ProbabilityTheory.gaussianPDFReal_pos : ∀ (μ : ℝ) (v : NNReal) (x : ℝ), v ≠ 0 → 0 < ProbabilityTheory.gaussianPDFReal μ v x
-- Mathlib.GroupTheory.Abelianization.Defs
Abelianization.lift_of : ∀ {G : Type u} [inst : Group G], Abelianization.lift Abelianization.of = MonoidHom.id (Abelianization G)
-- Mathlib.Data.Finsupp.Defs
/-- The composition of `f : M → N` and `g : α →₀ M` is `mapRange f hf g : α →₀ N`,
which is well-defined when `f 0 = 0`.

This preserves the structure on `f`, and exists in various bundled forms for when `f` is itself
bundled (defined in `Mathlib/Data/Finsupp/Basic.lean`):

* `Finsupp.mapRange.equiv`
* `Finsupp.mapRange.zeroHom`
* `Finsupp.mapRange.addMonoidHom`
* `Finsupp.mapRange.addEquiv`
* `Finsupp.mapRange.linearMap`
* `Finsupp.mapRange.linearEquiv`
 -/
Finsupp.mapRange : {α : Type u_1} →
  {M : Type u_4} → {N : Type u_5} → [inst : Zero M] → [inst_1 : Zero N] → (f : M → N) → f 0 = 0 → (α →₀ M) → α →₀ N
-- Mathlib.RingTheory.Polynomial.Eisenstein.IsIntegral
/-- Let `K` be the field of fraction of an integrally closed domain `R` and let `L` be an extension
of `K`, generated by an integral power basis `B` such that the minimal polynomial of `B.gen` is
Eisenstein at `p`. Given `z : L` integral over `R`, if `Q : R[X]` is such that
`aeval B.gen Q = p • z`, then `p ∣ Q.coeff 0`.  -/
dvd_coeff_zero_of_aeval_eq_prime_smul_of_minpoly_isEisensteinAt : ∀ {R : Type u} {K : Type v} {L : Type z} {p : R} [inst : CommRing R] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : Algebra R L] [inst_5 : Algebra R K] [IsScalarTower R K L] [IsDomain R]
  [IsFractionRing R K] [IsIntegrallyClosed R] {B : PowerBasis K L},
  Prime p →
    IsIntegral R B.gen →
      ∀ {z : L} {Q : Polynomial R},
        (Polynomial.aeval B.gen) Q = p • z → IsIntegral R z → (minpoly R B.gen).IsEisensteinAt (R ∙ p) → p ∣ Q.coeff 0
-- Mathlib.CategoryTheory.Sites.LocalSite
/-- The global sections of the coconstant sheaf on a type are naturally isomorphic to that type.  -/
CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheafΓNatIsoId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] →
        [inst_2 : J.IsLocalSite] →
          (A : Type u') →
            [inst_3 : CategoryTheory.Category.{v', u'} A] →
              [inst_4 : CategoryTheory.Limits.HasProducts A] →
                [inst_5 : CategoryTheory.HasWeakSheafify J A] →
                  (CategoryTheory.GrothendieckTopology.IsLocalSite.coconstantSheaf J A).comp
                      (CategoryTheory.Sheaf.Γ J A) ≅
                    CategoryTheory.Functor.id A
-- Mathlib.Algebra.Order.Round
round_sub_natCast : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : FloorRing α] (x : α)
  (y : ℕ), round (x - ↑y) = round x - ↑y
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Given `x : R`, the typeclass `IsLocalization.Away x S` states that `S` is
isomorphic to the localization of `R` at the submonoid generated by `x`.
See `IsLocalization.Away.mk` for a specialized constructor.  -/
IsLocalization.Away : {R : Type u_1} → [inst : CommSemiring R] → R → (S : Type u_4) → [inst_1 : CommSemiring S] → [Algebra R S] → Prop
-- Mathlib.Topology.Order.UpperLowerSetTopology
Topology.IsUpperSet.monotone_to_upperTopology_continuous : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : TopologicalSpace α]
  [inst_3 : TopologicalSpace β] [Topology.IsUpperSet α] [Topology.IsUpper β] {f : α → β}, Monotone f → Continuous f
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_neg : ∀ {a : USize} (h : System.Platform.numBits = 32), (-a).toBitVec32 h = -a.toBitVec32 h
-- Init.Data.SInt.Bitwise
Int64.ofBitVec_xor : ∀ (a b : BitVec 64), Int64.ofBitVec (a ^^^ b) = Int64.ofBitVec a ^^^ Int64.ofBitVec b
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.compl_adj : ∀ {V : Type u_2} (G : Digraph V) (v w : V), Gᶜ.Adj v w ↔ ¬G.Adj v w
-- Lean.Meta.Tactic.Grind.AC.Seq
Lean.Grind.AC.instAppendSeq_lean : Append Lean.Grind.AC.Seq
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.coe_invEmbedding : ∀ {n : ℕ} (c : Composition n) (j : Fin n), ↑(c.invEmbedding j) = ↑j - c.sizeUpTo ↑(c.index j)
-- Mathlib.LinearAlgebra.Complex.FiniteDimensional
Complex.rank_real_complex : Module.rank ℝ ℂ = 2
-- Mathlib.Algebra.Order.Monoid.Submonoid
AddSubmonoid.mem_nonneg : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : Preorder M] [inst_2 : AddLeftMono M] {a : M},
  a ∈ AddSubmonoid.nonneg M ↔ 0 ≤ a
-- Std.Tactic.BVDecide.Normalize.Bool
Std.Tactic.BVDecide.Normalize.Bool.ite_then_ite : ∀ {α : Sort u_1} (cond : Bool) {a b c : α}, (bif cond then bif cond then a else b else c) = bif cond then a else c
-- Std.Http.Data.Headers.Basic
/-- Parses a `Connection` header value into normalized tokens.
 -/
Std.Http.Header.Connection.parse : Std.Http.Header.Value → Option Std.Http.Header.Connection
-- Mathlib.Algebra.Order.Star.Basic
conjugate_nonneg_of_nonneg : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [StarOrderedRing R]
  {a : R}, 0 ≤ a → ∀ {c : R}, 0 ≤ c → 0 ≤ c * a * c
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection.inv_eq : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} (hv : f v = 0) (hv' : autoParam (f (-v) = 0) LinearEquiv.transvection.inv_eq._auto_1),
  (LinearEquiv.transvection hv)⁻¹ = LinearEquiv.transvection hv'
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.coe_comap : ∀ {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : TopologicalSpace M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : TopologicalSpace N]
  [inst_6 : Module R N] (f : M →L[R] N) (s : ClosedSubmodule R N), ↑(ClosedSubmodule.comap f s) = ⇑f ⁻¹' ↑s
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.disjoint_map : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F},
  Function.Injective ⇑f →
    ∀ {H K : AddSubmonoid M}, Disjoint H K → Disjoint (AddSubmonoid.map f H) (AddSubmonoid.map f K)
-- Mathlib.Algebra.Homology.BifunctorShift
CochainComplex.mapBifunctorShift₁Iso_hom_naturality₁ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : 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} D]
  [inst_3 : CategoryTheory.Preadditive C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] {K₁ L₁ : CochainComplex C₁ ℤ} (f₁ : K₁ ⟶ L₁) (K₂ : CochainComplex C₂ ℤ)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.Additive]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (x : ℤ) [inst_8 : K₁.HasMapBifunctor K₂ F]
  [inst_9 : L₁.HasMapBifunctor K₂ F],
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.mapBifunctorMap
        ((CategoryTheory.shiftFunctor (HomologicalComplex C₁ (ComplexShape.up ℤ)) x).map f₁)
        (CategoryTheory.CategoryStruct.id K₂) F (ComplexShape.up ℤ))
      (L₁.mapBifunctorShift₁Iso K₂ F x).hom =
    CategoryTheory.CategoryStruct.comp (K₁.mapBifunctorShift₁Iso K₂ F x).hom
      ((CategoryTheory.shiftFunctor (CochainComplex D ℤ) x).map
        (HomologicalComplex.mapBifunctorMap f₁ (CategoryTheory.CategoryStruct.id K₂) F (ComplexShape.up ℤ)))
-- Lean.Elab.Tactic.Omega.Frontend
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.elabOmegaConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Lean.Meta.Omega.OmegaConfig
-- Mathlib.Util.AtomM.Recurse
Mathlib.Tactic.AtomM.Recurse.Config.mk.inj : ∀ {red : Lean.Meta.TransparencyMode} {zetaDelta contextual : Bool} {red_1 : Lean.Meta.TransparencyMode}
  {zetaDelta_1 contextual_1 : Bool},
  { red := red, zetaDelta := zetaDelta, contextual := contextual } =
      { red := red_1, zetaDelta := zetaDelta_1, contextual := contextual_1 } →
    red = red_1 ∧ zetaDelta = zetaDelta_1 ∧ contextual = contextual_1
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.mem_set_normalizer_iff'' : ∀ {G : Type u_1} [inst : Group G] {S : Set G} {g : G}, g ∈ Subgroup.normalizer S ↔ ∀ (h : G), h ∈ S ↔ g⁻¹ * h * g ∈ S
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_div_intCast_eq_div_intCast_mod : ∀ {k : Type u_4} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k] [inst_3 : FloorRing k] {m : ℤ} {n : ℕ},
  Int.fract (↑m / ↑n) = ↑(m % ↑n) / ↑n
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.norm_expSeries_summable_of_mem_ball' : ∀ {𝕂 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕂] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕂 𝔸],
  ∀ x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius, Summable fun n => ‖(↑n.factorial)⁻¹ • x ^ n‖
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (f : Polynomial R),
  AdjoinRoot.quotAdjoinRootEquivQuotPolynomialQuot I f =
    (AdjoinRoot.quotMapOfEquivQuotMapCMapMk I f).trans
      ((AdjoinRoot.quotMapCMapSpanMkEquivQuotMapCQuotMapMk I f).trans
        ((Ideal.quotEquivOfEq ⋯).trans (AdjoinRoot.Polynomial.quotQuotEquivComm I f).symm))
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn
_private.Mathlib.MeasureTheory.VectorMeasure.Decomposition.Hahn.0.MeasureTheory.SignedMeasure.someExistsOneDivLT_subset' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {i j : Set α},
  MeasureTheory.SignedMeasure.someExistsOneDivLT✝ s (i \ j) ⊆ i
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsTrivialBlock.eq_1 : ∀ {X : Type u_2} (B : Set X), MulAction.IsTrivialBlock B = (B.Subsingleton ∨ B = Set.univ)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toList_roo_eq_zero : ∀ {m n : ℤ} {i : ℕ}, (n - (m + 1)).toNat ≤ i → (m<...n).toList[i]! = 0
-- Init.Data.UInt.Lemmas
UInt32.lt_irrefl : ∀ (a : UInt32), ¬a < a
-- Mathlib.Algebra.Category.MonCat.Limits
/-- Witness that the limit cone in `MonCat` is a limit cone.
(Internal use only; use the limits API.)
 -/
MonCat.HasLimits.limitConeIsLimit : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J MonCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget MonCat)).sections] →
        CategoryTheory.Limits.IsLimit (MonCat.HasLimits.limitCone F)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.degree_pow' : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.leadingCoeff ^ n ≠ 0 → (p ^ n).degree = n • p.degree
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.res.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X),
  TopCat.Presheaf.SheafConditionEqualizerProducts.res F U =
    CategoryTheory.Limits.Pi.lift fun i => F.map (TopologicalSpace.Opens.leSupr U i).op
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.inv_bot : ∀ {G : Type u_2} [inst : Group G], ⊥⁻¹ = ⊥
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.brecOn : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  {a a_1 : RingCat.Colimits.Prequotient F} (t : RingCat.Colimits.Relation F a a_1),
  (∀ (a a_2 : RingCat.Colimits.Prequotient F) (t : RingCat.Colimits.Relation F a a_2),
      RingCat.Colimits.Relation.below t → motive a a_2 t) →
    motive a a_1 t
-- Init.Data.Dyadic.Basic
/-- Shift a dyadic number left by `i` bits.  -/
Dyadic.shiftLeft : Dyadic → ℤ → Dyadic
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.leftInverse_symm : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), Function.LeftInverse ⇑e.symm ⇑e
-- Mathlib.Data.List.Sigma
List.mem_keys_kerase_of_ne : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a₁ a₂ : α} {l : List (Sigma β)},
  a₁ ≠ a₂ → (a₁ ∈ (List.kerase a₂ l).keys ↔ a₁ ∈ l.keys)
-- Mathlib.Logic.Equiv.Option
/-- `Option α` is equivalent to `α ⊕ PUnit`  -/
Equiv.optionEquivSumPUnit : (α : Type w) → Option α ≃ α ⊕ PUnit.{v + 1}
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- `U.starProjection ∘ V.starProjection = 0` iff `U` and `V` are pairwise orthogonal.  -/
Submodule.starProjection_comp_starProjection_eq_zero_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {U V : Submodule 𝕜 E} [inst_3 : U.HasOrthogonalProjection] [inst_4 : V.HasOrthogonalProjection],
  U.starProjection ∘SL V.starProjection = 0 ↔ U ⟂ V
-- Mathlib.GroupTheory.CoprodI
MulOne.toOne.hcongr_2 : ∀ (M M' : Type u_2), M = M' → ∀ (self : MulOne M) (self' : MulOne M'), self ≍ self' → self.toOne ≍ self'.toOne
-- Mathlib.Order.SuccPred.Basic
Order.covBy_succ : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] [NoMaxOrder α] (a : α), a ⋖ Order.succ a
-- Mathlib.Algebra.DirectSum.Internal
/-- The `S`-algebra `A 0` inherited from `R` in the presence of `SetLike.GradedMonoid A`.  -/
SetLike.GradeZero.instAlgebra : {ι : Type u_1} →
  {S : Type u_3} →
    {R : Type u_4} →
      [inst : CommSemiring S] →
        [inst_1 : Semiring R] →
          [inst_2 : Algebra S R] →
            [inst_3 : AddMonoid ι] → (A : ι → Submodule S R) → [inst_4 : SetLike.GradedMonoid A] → Algebra S ↥(A 0)
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- Any neighborhood of `x` contains all the points which are close enough to `x` for the
Riemannian distance, `ℝ≥0` version.  -/
setOfPred_riemannianEDist_lt_subset_nhds : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] [inst_6 : IsManifold I 1 M]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] [RegularSpace M] {x : M} {s : Set M},
  s ∈ nhds x → ∃ c > 0, {y | Manifold.riemannianEDist I x y < ↑c} ⊆ s
-- Mathlib.Data.Set.Card
Set.encard_eq_top_iff : ∀ {α : Type u_1} {s : Set α}, s.encard = ⊤ ↔ s.Infinite
-- Lean.Meta.Tactic.FunIndCollect
Lean.Meta.FunInd.Call.mk.injEq : ∀ (expr relevantArgs expr_1 relevantArgs_1 : Lean.Expr),
  ({ expr := expr, relevantArgs := relevantArgs } = { expr := expr_1, relevantArgs := relevantArgs_1 }) =
    (expr = expr_1 ∧ relevantArgs = relevantArgs_1)
-- Mathlib.Topology.EMetricSpace.Defs
Metric.eball_eq_empty_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε : ENNReal}, Metric.eball x ε = ∅ ↔ ε = 0
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.add_neg_lt_sSup : ∀ {s : Set ℝ}, s.Nonempty → ∀ {ε : ℝ}, ε < 0 → ∃ a ∈ s, sSup s + ε < a
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
Order.cof_int : Order.cof ℤ = Cardinal.aleph0
-- Mathlib.Probability.Independence.Kernel.Indep
ProbabilityTheory.Kernel.IndepSets.bInter : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → Set (Set Ω)} {s' : Set (Set Ω)}
  {_mΩ : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {u : Set ι},
  (∃ n ∈ u, ProbabilityTheory.Kernel.IndepSets (s n) s' κ μ) → ProbabilityTheory.Kernel.IndepSets (⋂ n ∈ u, s n) s' κ μ
-- Mathlib.Topology.ContinuousMap.CocompactMap
/-- The cocompact filter on `α` tends to the cocompact filter on `β` under the function  -/
CocompactMapClass.cocompact_tendsto : ∀ {F : Type u_1} {α : outParam (Type u_2)} {β : outParam (Type u_3)} {inst : TopologicalSpace α}
  {inst_1 : TopologicalSpace β} {inst_2 : FunLike F α β} [self : CocompactMapClass F α β] (f : F),
  Filter.Tendsto (⇑f) (Filter.cocompact α) (Filter.cocompact β)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_map : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {f : α → β → γ} {k : α},
  Std.ExtDTreeMap.Const.get? (Std.ExtDTreeMap.map f t) k = Option.map (f k) (Std.ExtDTreeMap.Const.get? t k)
-- Mathlib.Algebra.Category.MonCat.Limits
/-- The forgetful functor from additive commutative monoids to types preserves all
limits.

This means the underlying type of a limit can be computed as a limit in the category of types.  -/
AddCommMonCat.forget_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{v, v, u, u, u + 1, u + 1} (CategoryTheory.forget AddCommMonCat)
-- Init.Data.Array.Count
Array.boole_getElem_le_countP : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α} {i : ℕ} (h : i < xs.size),
  (if p xs[i] = true then 1 else 0) ≤ Array.countP p xs
-- Mathlib.Algebra.Group.Basic
div_eq_div_mul_div : ∀ {G : Type u_3} [inst : CommGroup G] (a b c : G), a / b = c / b * (a / c)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.liftNatTrans_app : ∀ {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)
  (W : CategoryTheory.MorphismProperty C) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : L.IsLocalization W] (F₁ F₂ : CategoryTheory.Functor C E) (F₁' F₂' : CategoryTheory.Functor D E)
  [inst_4 : CategoryTheory.Localization.Lifting L W F₁ F₁'] [inst_5 : CategoryTheory.Localization.Lifting L W F₂ F₂']
  (τ : F₁ ⟶ F₂) (X : C),
  (CategoryTheory.Localization.liftNatTrans L W F₁ F₂ F₁' F₂' τ).app (L.obj X) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.Localization.Lifting.iso L W F₁ F₁').hom.app X)
      (CategoryTheory.CategoryStruct.comp (τ.app X) ((CategoryTheory.Localization.Lifting.iso L W F₂ F₂').inv.app X))
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
CategoryTheory.MorphismProperty.MapFactorizationData.opEquiv_symm_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W₁ W₂ : CategoryTheory.MorphismProperty C} {X Y : C}
  {f : X ⟶ Y} (φ : W₂.op.MapFactorizationData W₁.op f.op),
  CategoryTheory.MorphismProperty.MapFactorizationData.opEquiv.symm φ = φ.unop
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePullbackCone.mk_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {X : C} {Y : ι → C} {f : (i : ι) → Y i ⟶ X}
  {W : C} (b : W ⟶ X) (π : (i : ι) → W ⟶ Y i) (h : ∀ (i : ι), CategoryTheory.CategoryStruct.comp (π i) (f i) = b)
  (i : ι), (CategoryTheory.Limits.WidePullbackCone.mk b π h).π i = π i
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.pairingIn_eq_add_of_root_eq_smul_add_smul : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {S : Type u_6}
  [inst_5 : CommRing S] [inst_6 : Algebra S R] [FaithfulSMul S R] [inst_8 : P.IsValuedIn S] [inst_9 : Module S M]
  [IsScalarTower S R M] {i j k l : ι} {x y : S},
  P.root k = x • P.root i + y • P.root l → P.pairingIn S k j = x • P.pairingIn S i j + y • P.pairingIn S l j
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.mem_iSup : ∀ {R : Type u} {M : Type v} [inst : SMul R M] {ι : Sort u_1} {p : ι → SubMulAction R M} {x : M},
  x ∈ ⨆ i, p i ↔ ∃ i, x ∈ p i