mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom_comp : ∀ {X : AlgebraicGeometry.Scheme} {I J K : X.IdealSheafData} (hIJ : I ≤ J) (hJK : J ≤ K) (U : ↑X.affineOpens),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom hJK U)
      (AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom hIJ U) =
    AlgebraicGeometry.Scheme.IdealSheafData.glueDataObjHom ⋯ U
-- Mathlib.RingTheory.KrullDimension.Regular
ringKrullDim_le_ringKrullDim_add_spanFinrank : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] [IsLocalRing R] {I : Ideal R},
  I ≠ ⊤ → ringKrullDim R ≤ ringKrullDim (R ⧸ I) + ↑(Submodule.spanFinrank I)
-- Mathlib.Order.ScottContinuity.Prod
ScottContinuous.prod : ∀ {α : Type u_1} {β : Type u_2} {α' : Type u_4} {β' : Type u_5} [inst : Preorder α] [inst_1 : Preorder β]
  [inst_2 : Preorder α'] [inst_3 : Preorder β'] {f : α → α'} {g : β → β'},
  ScottContinuous f → ScottContinuous g → ScottContinuous (Prod.map f g)
-- Mathlib.Analysis.Meromorphic.Order
/-- If `g` is analytic at `x`, and `g' x ≠ 0`, then the meromorphic order of
`f ∘ g` at `x` is the meromorphic order of `f` at `g x` (even if `f` is not meromorphic).  -/
meromorphicOrderAt_comp_of_deriv_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : 𝕜} {f : 𝕜 → E} {g : 𝕜 → 𝕜},
  AnalyticAt 𝕜 g x →
    deriv g x ≠ 0 → ∀ [CompleteSpace 𝕜] [CharZero 𝕜], meromorphicOrderAt (f ∘ g) x = meromorphicOrderAt f (g x)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.ι_evalHom_apply : ∀ {𝕜 : 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] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ)
  (x_1 : ↑(((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf).obj U)),
  (CategoryTheory.ConcreteCategory.hom (smoothSheafCommRing.evalHom IM I M R x))
      ((CategoryTheory.ConcreteCategory.hom
          (CategoryTheory.Limits.colimit.ι
            ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U))
        x_1) =
    (CategoryTheory.ConcreteCategory.hom (smoothSheafCommRing.evalAt IM I M R x (Opposite.unop U))) x_1
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalSubgroup.instSemilatticeInfOpenNormalSubgroup.eq_1 : ∀ {G : Type u} [inst : Group G] [inst_1 : TopologicalSpace G],
  OpenNormalSubgroup.instSemilatticeInfOpenNormalSubgroup = Function.Injective.semilatticeInf SetLike.coe ⋯ ⋯ ⋯ ⋯
-- Mathlib.Data.WSeq.Basic
/-- Unfortunately, `WSeq` is not a lawful monad, because it does not satisfy the monad laws exactly,
only up to sequence equivalence. Furthermore, even quotienting by the equivalence is not sufficient,
because the join operation involves lists of quotient elements, with a lifted equivalence relation,
and pure quotients cannot handle this type of construction.  -/
Stream'.WSeq.monad : Monad Stream'.WSeq
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_sub_natCast_mul : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIocMod hp a (b - ↑m * p) = toIocMod hp a b
-- Aesop.Rule.Name
Aesop.instInhabitedRuleName.default : Aesop.RuleName
-- Mathlib.Topology.Algebra.Module.LinearPMap
LinearPMap.HasCore.closure_eq : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] {f : E →ₗ.[R] F} {S : Submodule R E}, f.HasCore S → (f.domRestrict S).closure = f
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_symm_id : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ : CategoryTheory.Functor C D} {R₁ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁),
  (CategoryTheory.conjugateEquiv adj₁ adj₁).symm (CategoryTheory.CategoryStruct.id R₁) =
    CategoryTheory.CategoryStruct.id L₁
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
/-- Eta-expanded form of `AbsolutelyContinuousOnInterval.sub` -/
AbsolutelyContinuousOnInterval.fun_sub : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {f g : ℝ → F},
  AbsolutelyContinuousOnInterval f a b →
    AbsolutelyContinuousOnInterval g a b → AbsolutelyContinuousOnInterval (fun i => f i - g i) a b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.comm : ∀ {α : Type u} {β : α → Type v} {m₁ m₂ : Std.DHashMap.Raw α β}, m₁.Equiv m₂ ↔ m₂.Equiv m₁
-- Mathlib.Order.Category.BoolAlg
BoolAlg.coe_of : ∀ (X : Type u) [inst : BooleanAlgebra X], ↑{ carrier := X, str := inst } = X
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
MeasureTheory.VectorMeasure.setIntegral_biUnion_finset : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G}
  {ι : Type u_7} (t : Finset ι) {s : ι → Set X},
  (∀ i ∈ t, MeasurableSet (s i)) →
    (↑t).Pairwise (Function.onFun Disjoint s) →
      (∀ i ∈ t, μ.IntegrableOn f (s i)) →
        ∫ᵛ (x : X) in ⋃ i ∈ t, s i, f x ∂[B; μ] = ∑ i ∈ t, ∫ᵛ (x : X) in s i, f x ∂[B; μ]
-- Mathlib.Data.List.NodupEquivFin
/-- If `l` has no duplicates, then `List.get` defines an equivalence between `Fin (length l)` and
the set of elements of `l`.  -/
List.Nodup.getEquiv : {α : Type u_1} → [DecidableEq α] → (l : List α) → l.Nodup → Fin l.length ≃ { x // x ∈ l }
-- Mathlib.Data.Sigma.Interval
Sigma.Ioi_mk : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Preorder (α i)] [inst_1 : (i : ι) → LocallyFiniteOrderTop (α i)]
  (i : ι) (a : α i), Finset.Ioi ⟨i, a⟩ = Finset.map (Function.Embedding.sigmaMk i) (Finset.Ioi a)
-- Mathlib.Analysis.Matrix.Order
Matrix.PosSemidef.det_sqrt : ∀ {𝕜 : Type u_1} {n : Type u_2} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n 𝕜},
  A.PosSemidef → (CFC.sqrt A).det = RCLike.sqrt A.det
-- Mathlib.Topology.Homotopy.Basic
/-- value of the homotopy at 1  -/
ContinuousMap.HomotopyLike.map_one_left : ∀ {X : outParam (Type u_3)} {Y : outParam (Type u_4)} {inst : TopologicalSpace X} {inst_1 : TopologicalSpace Y}
  {F : Type u_5} {f₀ f₁ : outParam C(X, Y)} {inst_2 : FunLike F (↑unitInterval × X) Y}
  [self : ContinuousMap.HomotopyLike F f₀ f₁] (f : F) (x : X), f (1, x) = f₁ x
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.medial.congr_simp : ∀ {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] {n : ℕ} [inst_4 : NeZero n] [inst_5 : CharZero k] (s s_1 : Affine.Simplex k P n),
  s = s_1 → s.medial = s_1.medial
-- Mathlib.Order.Lattice.Nat
Nat.sSup_def : ∀ {s : Set ℕ} (h : ∃ n, ∀ a ∈ s, a ≤ n), sSup s = Nat.find h
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_norm_diagonal : ∀ {n : Type u_4} {α : Type u_5} [inst : Fintype n] [inst_1 : SeminormedAddCommGroup α] [inst_2 : DecidableEq n]
  (v : n → α), ‖Matrix.diagonal v‖ = ‖WithLp.toLp 2 v‖
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type is a division commutative monoid if `β` is a division commutative monoid.  -/
FunLike.divisionCommMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Mul F] →
          [inst_2 : One F] →
            [inst_3 : Pow F ℕ] →
              [inst_4 : Inv F] →
                [inst_5 : Div F] →
                  [inst_6 : Pow F ℤ] →
                    [inst_7 : DivisionCommMonoid β] →
                      [IsOneApply F α β] →
                        [IsMulApply F α β] →
                          [IsInvApply F α β] →
                            [IsDivApply F α β] → [IsPowApply ℕ F α β] → [IsPowApply ℤ F α β] → DivisionCommMonoid F
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.antipode_left : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (X : C) [self : CategoryTheory.HopfObj X],
  CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.comul
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.HopfObj.antipode X)
        CategoryTheory.MonObj.mul) =
    CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one
-- Init.Grind.Ring.Field
Lean.Grind.Field.toCommRing : {α : Type u} → [self : Lean.Grind.Field α] → Lean.Grind.CommRing α
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Shift
/-- A parallel cross-section of a simplex is the image of the base under a homothety.  -/
Affine.Simplex.closedInterior_inter_shift_eq_homothety : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [IsOrderedRing k]
  [inst_3 : AddCommGroup V] [inst_4 : Module k V] [inst_5 : AddTorsor V P] {n : ℕ} [inst_6 : NeZero n]
  (s : Affine.Simplex k P n) (i : Fin (n + 1)) {x : k},
  x ∈ Set.Icc 0 1 →
    s.closedInterior ∩ ↑((affineSpan k (s.points '' {i}ᶜ)).shift (s.points i) x) =
      ⇑(AffineMap.homothety (s.points i) x) '' (s.faceOpposite i).closedInterior
-- Mathlib.RingTheory.PicardGroup
Module.Flat.instInvertibleSubtypeMemSubmoduleSubmoduleAlgebra : ∀ {R : Type u} {M : Type v} {A : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] (e : TensorProduct R A M ≃ₗ[A] A) [Module.Flat R M] [FaithfulSMul R A]
  [Module.Invertible R M], Module.Invertible R ↥(Module.Flat.submoduleAlgebra e)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.congr_right : ∀ {α : Type u} {β : α → Type v} {m₁ m₂ m₃ : Std.DHashMap.Raw α β}, m₁.Equiv m₂ → (m₃.Equiv m₁ ↔ m₃.Equiv m₂)
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instInvolutiveInv : {α : Type u_1} → {l : Filter α} → {G : Type u_6} → [InvolutiveInv G] → InvolutiveInv (l.Germ G)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Cat
CategoryTheory.Adjunction.toCat_counit_toNatTrans : ∀ {C D : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Category.{v, u} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G),
  adj.toCat.counit.toNatTrans = adj.counit
-- Mathlib.MeasureTheory.Function.L2Space
/-- The inner product in `L2` of two `indicatorConstLp`s, i.e. functions which are constant `a : E`
and `b : E` on measurable `s t : Set α` with finite measure, respectively, is `⟪a, b⟫` times the
measure of `s ∩ t`.  -/
MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_4} [inst : RCLike 𝕜] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E] {s t : Set α} [CompleteSpace E]
  (hs : MeasurableSet s) (ht : MeasurableSet t)
  (hμs : autoParam (μ s ≠ ⊤) MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp._auto_1)
  (hμt : autoParam (μ t ≠ ⊤) MeasureTheory.L2.inner_indicatorConstLp_indicatorConstLp._auto_3) (a b : E),
  inner 𝕜 (MeasureTheory.indicatorConstLp 2 hs hμs a) (MeasureTheory.indicatorConstLp 2 ht hμt b) =
    μ.real (s ∩ t) • inner 𝕜 a b
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.revAll_eq_skipSuffixWhile_beq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String.Slice},
  s.revAll pat = (s.skipSuffixWhile pat == s.startPos)
-- Init.Data.List.Lex
/-- Variant of `lex_eq_false_iff` using an arbitrary comparator.  -/
List.lex_eq_false_iff_not_lex : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : BEq α] [LawfulBEq α] (lt : α → α → Bool),
  l₁.lex l₂ lt = false ↔ ¬List.Lex (fun x y => lt x y = true) l₁ l₂
-- Mathlib.Topology.Algebra.ProperAction.Torsor
/-- If `P` is a topological additive torsor over `V`, the additive action of `V` on
`P` is proper.  -/
instProperVAdd : ∀ {V : Type u_1} {P : Type u_2} [inst : AddGroup V] [inst_1 : AddTorsor V P] [inst_2 : TopologicalSpace V]
  [inst_3 : TopologicalSpace P] [IsTopologicalAddTorsor P], ProperVAdd V P
-- Mathlib.Geometry.Manifold.HasGroupoid
/-- If a structure groupoid `G` is closed under restriction, for any chart `e` in the maximal atlas,
the restriction `e.restr s` to an open set `s` is also in the maximal atlas.  -/
restr_mem_maximalAtlas : ∀ {H : Type u} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  (G : StructureGroupoid H) [ClosedUnderRestriction G] {e : OpenPartialHomeomorph M H},
  e ∈ StructureGroupoid.maximalAtlas M G → ∀ {s : Set M}, IsOpen s → e.restr s ∈ StructureGroupoid.maximalAtlas M G
-- Mathlib.GroupTheory.Coset.Card
Subgroup.card_dvd_of_le : ∀ {α : Type u_1} [inst : Group α] {H K : Subgroup α}, H ≤ K → Nat.card ↥H ∣ Nat.card ↥K
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ici_union_Iio_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b ≤ a → Set.Ici b ∪ Set.Iio a = Set.univ
-- Mathlib.NumberTheory.ModularForms.Basic
/-- The `n`-th power of `DirectSum.of _ k f` lands in grade `n * k` and is given by `f.pow n`.  -/
ModularForm.directSum_of_pow : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetPlusMinusOne] {k : ℤ} (f : ModularForm Γ k) (n : ℕ),
  (DirectSum.of (ModularForm Γ) k) f ^ n = (DirectSum.of (ModularForm Γ) (↑n * k)) (f.pow n)
-- Init.Data.Nat.Mod
Nat.mod_mul_left_div_self : ∀ (m n k : ℕ), m % (k * n) / n = m / n % k
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.toAdditive_single : ∀ {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : Mul M] (m : M) (r : R),
  (MonoidAlgebra.toAdditive R M) (MonoidAlgebra.single m r) = AddMonoidAlgebra.single (Additive.ofMul m) r
-- Mathlib.RingTheory.LocalProperties.Submodule
Submodule.eq_of_isLocalized₀_span : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Mₚ : ↑s → Type u_5) [inst_3 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_4 : (r : ↑s) → Module R (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [inst_5 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] {N P : Submodule R M},
      (∀ (r : ↑s),
          Submodule.localized₀ (Submonoid.powers ↑r) (f r) N = Submodule.localized₀ (Submonoid.powers ↑r) (f r) P) →
        N = P
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
/-- The inclusion map of the Moore complex in the alternating face map complex,
as a natural transformation  -/
AlgebraicTopology.inclusionOfMooreComplex : (A : Type u_2) →
  [inst : CategoryTheory.Category.{v_2, u_2} A] →
    [inst_1 : CategoryTheory.Abelian A] →
      AlgebraicTopology.normalizedMooreComplex A ⟶ AlgebraicTopology.alternatingFaceMapComplex A
-- Lean.Elab.App
Lean.Elab.Term.ElabElim.Context.elimInfo : Lean.Elab.Term.ElabElim.Context → Lean.Elab.Term.ElabElimInfo
-- Mathlib.Topology.Algebra.OpenSubgroup
Subgroup.instFiniteQuotientOfSeparatelyContinuousMulOfCompactSpace : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousMul G] [CompactSpace G]
  (U : OpenSubgroup G), Finite (G ⧸ ↑U)
-- Mathlib.Tactic.NormNum.Eq
Mathlib.Meta.NormNum.isNNRat_eq_false : ∀ {α : Type u_1} [inst : Semiring α] [CharZero α] {a b : α} {na nb da db : ℕ},
  Mathlib.Meta.NormNum.IsNNRat a na da →
    Mathlib.Meta.NormNum.IsNNRat b nb db → decide (na.mul db = nb.mul da) = false → ¬a = b
-- Mathlib.Topology.Algebra.Group.Basic
nhds_add : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] (x y : G),
  nhds (x + y) = nhds x + nhds y
-- Mathlib.RingTheory.Jacobson.Ring
Polynomial.isMaximal_comap_C_of_isJacobsonRing : ∀ {R : Type u_1} [inst : CommRing R] (P : Ideal (Polynomial R)) [hP : P.IsMaximal] [IsJacobsonRing R],
  (Ideal.comap Polynomial.C P).IsMaximal
-- Mathlib.Data.List.Cycle
/-- A `s : Cycle α` that is made up of at least two unique elements.  -/
Cycle.Nontrivial : {α : Type u_1} → Cycle α → Prop
-- Mathlib.CategoryTheory.Sites.Grothendieck
/-- A category satisfies the right Ore condition if any span can be completed to a commutative square.
NB. Any category with pullbacks obviously satisfies the right Ore condition, see
`right_ore_of_pullbacks`.
 -/
CategoryTheory.GrothendieckTopology.RightOreCondition : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Prop
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.smul_nnreal : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} (r : NNReal),
  ν.MutuallySingular μ → (r • ν).MutuallySingular μ
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- The Frobenius automorphism of `k`, as a linear equivalence  -/
Isocrystal.«term_≃ᶠˡ[_,_]_» : Lean.TrailingParserDescr
-- Mathlib.Data.Finset.Basic
Finset.erase_singleton : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α), {a}.erase a = ∅
-- Mathlib.CategoryTheory.Filtered.Final
/-- In this situation, `F` is also initial, see
`Functor.initial_of_exists_of_isCofiltered_of_fullyFaithful`.  -/
CategoryTheory.IsCofiltered.of_exists_of_isCofiltered_of_fullyFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofiltered D] [F.Full] [F.Faithful],
  (∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) → CategoryTheory.IsCofiltered C
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.localInverse_mem_target : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x), x ∈ hf.localInverse.target
-- Mathlib.Topology.EMetricSpace.Defs
Metric.ordConnected_setOfPred_eball_subset : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (x : α) (s : Set α), {r | Metric.eball x r ⊆ s}.OrdConnected
-- Mathlib.Algebra.Module.Lattice
/-- Any basis of an `R`-lattice in `V` defines a `K`-basis of `V`.  -/
Module.Basis.extendOfIsLattice : {R : Type u_1} →
  [inst : CommRing R] →
    (K : Type u_2) →
      [inst_1 : Field K] →
        [inst_2 : Algebra R K] →
          {V : Type u_3} →
            [inst_3 : AddCommGroup V] →
              [inst_4 : Module K V] →
                [inst_5 : Module R V] →
                  [inst_6 : IsScalarTower R K V] →
                    [IsFractionRing R K] →
                      {κ : Type u_4} →
                        {M : Submodule R V} → [Submodule.IsLattice K M] → Module.Basis κ R ↥M → Module.Basis κ K V
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftPropAt_symm_of_mem_maximalAtlas : ∀ {H : Type u_1} {M : Type u_2} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M]
  {G : StructureGroupoid H} {e : OpenPartialHomeomorph M H} {Q : (H → H) → Set H → H → Prop} {x : H},
  G.LocalInvariantProp G Q →
    (∀ (y : H), Q id Set.univ y) →
      e ∈ StructureGroupoid.maximalAtlas M G → x ∈ e.target → ChartedSpace.LiftPropAt Q (↑e.symm) x
-- Lean.DocString.Types
Lean.Doc.Block.brecOn.eq : ∀ {i : Type u} {b : Type v} {motive_1 : Lean.Doc.Block i b → Sort u_1}
  {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1}
  {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1}
  {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1}
  {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1}
  {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1} (t : Lean.Doc.Block i b)
  (F_1 : (t : Lean.Doc.Block i b) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_1 t → motive_2 t)
  (F_3 :
    (t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_2 t → motive_3 t)
  (F_4 : (t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t)
  (F_5 : (t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) → Lean.Doc.Block.below_4 t → motive_5 t)
  (F_6 :
    (t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) → Lean.Doc.Block.below_5 t → motive_6 t)
  (F_7 : (t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t)
  (F_8 : (t : Lean.Doc.ListItem (Lean.Doc.Block i b)) → Lean.Doc.Block.below_7 t → motive_8 t)
  (F_9 : (t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Lean.Doc.Block.below_8 t → motive_9 t),
  t.brecOn F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9 =
    F_1 t (Lean.Doc.Block.brecOn.go t F_1 F_2 F_3 F_4 F_5 F_6 F_7 F_8 F_9).2
-- Lean.Meta.Tactic.Simp.Simproc
Lean.Meta.Simp.isSimproc : Lean.Name → Lean.CoreM Bool
-- Mathlib.Probability.Distributions.Bernoulli
ProbabilityTheory.bernoulliMeasure_real_apply_of_notMem_of_notMem : ∀ {X : Type u_1} [inst : MeasurableSpace X] {x y : X} (p : ↑unitInterval) {s : Set X},
  MeasurableSet s → x ∉ s → y ∉ s → (ProbabilityTheory.bernoulliMeasure x y p).real s = 0
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.homOfVector_toSpecMvPoly_assoc : ∀ {n : Type u} {S X : AlgebraicGeometry.Scheme} (f : X ⟶ S) (v : n → ↑(X.presheaf.obj (Opposite.op ⊤)))
  {Z : AlgebraicGeometry.Scheme} (h : AlgebraicGeometry.Spec (CommRingCat.of (MvPolynomial n (ULift.{u, 0} ℤ))) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.homOfVector f v)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.toSpecMvPoly n S) h) =
    CategoryTheory.CategoryStruct.comp ((AlgebraicGeometry.AffineSpace.toSpecMvPolyIntEquiv n).symm v) h
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.cmp.match_1.eq_3 : ∀ (motive : ONote → ONote → Sort u_1) (x : ONote) (h_1 : Unit → motive ONote.zero ONote.zero)
  (h_2 : (x : ONote) → motive x ONote.zero) (h_3 : (x : ONote) → motive ONote.zero x)
  (h_4 :
    (_o₁ e₁ : ONote) →
      (n₁ : ℕ+) →
        (a₁ : ONote) →
          _o₁ = e₁.oadd n₁ a₁ →
            (_o₂ e₂ : ONote) → (n₂ : ℕ+) → (a₂ : ONote) → _o₂ = e₂.oadd n₂ a₂ → motive (e₁.oadd n₁ a₁) (e₂.oadd n₂ a₂)),
  (x = ONote.zero → False) →
    (match ONote.zero, x with
      | ONote.zero, ONote.zero => h_1 ()
      | x, ONote.zero => h_2 x
      | ONote.zero, x => h_3 x
      | _o₁@h:(e₁.oadd n₁ a₁), _o₂@h_5:(e₂.oadd n₂ a₂) => h_4 _o₁ e₁ n₁ a₁ h _o₂ e₂ n₂ a₂ h_5) =
      h_3 x
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
MonotoneOn.csSup_eq_of_subset_of_forall_exists_le : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : ConditionallyCompleteLattice β] {f : α → β} {s t : Set α},
  BddAbove (f '' t) → MonotoneOn f t → s ⊆ t → (∀ y ∈ t, ∃ x ∈ s, y ≤ x) → sSup (f '' s) = sSup (f '' t)
-- Mathlib.Algebra.Ring.Defs
HasDistribNeg.toInvolutiveNeg : {α : Type u_1} → {inst : Mul α} → [self : HasDistribNeg α] → InvolutiveNeg α
-- Init.Data.UInt.Bitwise
UInt16.ofNat_xor : ∀ (a b : ℕ), UInt16.ofNat (a ^^^ b) = UInt16.ofNat a ^^^ UInt16.ofNat b