mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.Hom.naturality_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) {U U' : Y.Opens} (i : Opposite.op U' ⟶ Opposite.op U) {Z : CommRingCat}
  (h : X.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map f.base).obj U)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.map i)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app f U')
      (CategoryTheory.CategoryStruct.comp (X.presheaf.map ((TopologicalSpace.Opens.map f.base).map i.unop).op) h)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKey.induct_unfolding : ∀ {α : Type u} {β : α → Type v} (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.isEmpty = false → α → Prop),
  (∀ (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β)
      (x : (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false),
      (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r).isEmpty = false →
        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x k) →
    (∀ (size : ℕ) (k : α) (v : β k) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1) (l r r_1 : Std.DTreeMap.Internal.Impl α β)
        (h :
          (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r)
                r_1).isEmpty =
            false),
        (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1).isEmpty =
            false →
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) ⋯
              ((Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minKey ⋯) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
              h ((Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r).minKey ⋯)) →
      ∀ (t : Std.DTreeMap.Internal.Impl α β) (h : t.isEmpty = false), motive t h (t.minKey h)
-- Mathlib.Algebra.Group.Fin.Basic
Fin.addCommSemigroup : (n : ℕ) → AddCommSemigroup (Fin n)
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.Node.collision.inj : ∀ {α : Type u} {β : Type v} {ks : Array α} {vs : Array β} {h : ks.size = vs.size} {ks_1 : Array α} {vs_1 : Array β}
  {h_1 : ks_1.size = vs_1.size},
  Lean.PersistentHashMap.Node.collision ks vs h = Lean.PersistentHashMap.Node.collision ks_1 vs_1 h_1 →
    ks = ks_1 ∧ vs = vs_1
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- The identity lax prefunctor.  -/
CategoryTheory.PrelaxFunctorStruct.id : (B : Type u₁) → [inst : Quiver B] → [inst_1 : (a b : B) → Quiver (a ⟶ b)] → CategoryTheory.PrelaxFunctorStruct B B
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- `associatedHom` is the map that sends a quadratic map on a module `M` over `R` to its
associated symmetric bilinear map.  As provided here, this has the structure of an `S`-linear map
where `S` is a commutative ring and `R` is an `S`-algebra.

Over a commutative ring, use `QuadraticMap.associated`, which gives an `R`-linear map.  Over a
general ring with no nontrivial distinguished commutative subring, use `QuadraticMap.associated'`,
which gives an additive homomorphism (or more precisely a `ℤ`-linear map.)  -/
QuadraticMap.associatedHom : (S : Type u_1) →
  {R : Type u_3} →
    {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] →
                  [inst_5 : CommSemiring S] →
                    [inst_6 : Algebra S R] →
                      [inst_7 : Module S N] →
                        [inst_8 : IsScalarTower S R N] →
                          [Invertible 2] → QuadraticMap R M N →ₗ[S] LinearMap.BilinMap R M N
-- Mathlib.CategoryTheory.Monoidal.DayConvolution.Braided
CategoryTheory.MonoidalCategory.DayConvolution.unit_app_braiding_inv_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.BraidedCategory C]
  [inst_4 : CategoryTheory.MonoidalCategory V] [inst_5 : CategoryTheory.BraidedCategory V]
  (F G : CategoryTheory.Functor C V) [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F G]
  [inst_7 : CategoryTheory.MonoidalCategory.DayConvolution G F] (x y : C) {Z : V}
  (h :
    (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).obj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit G F).app (x, y))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.MonoidalCategory.DayConvolution.braiding F G).inv.app
          (CategoryTheory.MonoidalCategoryStruct.tensorObj x y))
        h) =
    CategoryTheory.CategoryStruct.comp (β_ (F.obj y) (G.obj x)).inv
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolution.unit F G).app (y, x))
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).map (β_ x y).inv) h))
-- Std.Time.Format.Modifier
Std.Time.Modifier.a.inj : ∀ {presentation presentation_1 : Std.Time.Text},
  Std.Time.Modifier.a presentation = Std.Time.Modifier.a presentation_1 → presentation = presentation_1
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.RightFraction.map_s_comp_map_assoc : ∀ {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] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ : W.RightFraction X Y) (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L) {Z : D} (h : L.obj Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (L.map φ.s) (CategoryTheory.CategoryStruct.comp (φ.map L hL) h) =
    CategoryTheory.CategoryStruct.comp (L.map φ.f) h
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.mul_eq_bot_iff : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {a b : WithBot α},
  a * b = ⊥ ↔ a ≠ 0 ∧ b = ⊥ ∨ a = ⊥ ∧ b ≠ 0
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Param.toExpr : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Param pu → Lean.Expr
-- Mathlib.Analysis.Fourier.Notation
/-- The Fourier transform as a linear equivalence.  -/
FourierTransform.fourierEquiv : (R : Type u_5) →
  (E : Type u_6) →
    {F : Type u_7} →
      [inst : Semiring R] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : AddCommMonoid F] →
            [inst_3 : Module R E] →
              [inst_4 : Module R F] →
                [inst_5 : FourierTransform E F] →
                  [FourierAdd E F] →
                    [FourierSMul R E F] →
                      [inst_8 : FourierTransformInv F E] → [FourierPair E F] → [FourierInvPair F E] → E ≃ₗ[R] F
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.eval_nil : ∀ {lc : Lean.Omega.LinearCombo}, lc.eval [] = lc.const
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.instFullCommMonForget₂CommMon : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], (CategoryTheory.CommGrp.forget₂CommMon C).Full
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.checkSize.go : ℕ → Lean.Expr → OptionT (StateT ℕ Lean.MetaM) Unit
-- Mathlib.Analysis.LocallyConvex.AbsConvex
/-- [Bourbaki, *Topological Vector Spaces*, III §1.6][bourbaki1987]  -/
isCompact_closedAbsConvexHull_of_totallyBounded : ∀ {E : Type u_3} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : UniformSpace E] [IsUniformAddGroup E]
  [ContinuousSMul ℝ E] [LocallyConvexSpace ℝ E] [QuasiCompleteSpace ℝ E] {s : Set E},
  TotallyBounded s → IsCompact ((closedAbsConvexHull ℝ) s)
-- Mathlib.Topology.UniformSpace.Basic
uniformContinuous_toAdd : ∀ {α : Type ua} [inst : UniformSpace α], UniformContinuous ⇑Multiplicative.toAdd
-- Mathlib.SetTheory.Lists
_private.Mathlib.SetTheory.Lists.0.Lists'.cons.match_1.splitter : {α : Type u_1} →
  (motive : Lists α → Lists' α true → Sort u_2) →
    (x : Lists α) →
      (x_1 : Lists' α true) →
        ((fst : Bool) → (a : Lists' α fst) → (l : Lists' α true) → motive ⟨fst, a⟩ l) → motive x x_1
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.Lifting₂.compRight : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {D₁ : Type u_3} →
      {D₂ : Type u_4} →
        {E : Type u_5} →
          [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.Category.{v_4, u_4} D₂] →
                  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] →
                    (L₁ : CategoryTheory.Functor C₁ D₁) →
                      (L₂ : CategoryTheory.Functor C₂ D₂) →
                        (W₁ : CategoryTheory.MorphismProperty C₁) →
                          (W₂ : CategoryTheory.MorphismProperty C₂) →
                            (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E)) →
                              (F' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E)) →
                                [CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F F'] →
                                  {E' : Type u_7} →
                                    [inst_6 : CategoryTheory.Category.{v_7, u_7} E'] →
                                      (G : CategoryTheory.Functor E E') →
                                        CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂
                                          (F.comp ((CategoryTheory.Functor.whiskeringRight C₂ E E').obj G))
                                          (F'.comp ((CategoryTheory.Functor.whiskeringRight D₂ E E').obj G))
-- Mathlib.Order.Defs.LinearOrder
max_eq_left : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, b ≤ a → max a b = a
-- Mathlib.Topology.Separation.CountableSeparatingOn
/-- If there exists a countable family of open sets separating points of `s`, then there exists
a countable family of closed sets separating points of `s`.  -/
instHasCountableSeparatingOnIsClosedOfIsOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [h : HasCountableSeparatingOn X IsOpen s],
  HasCountableSeparatingOn X IsClosed s
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- If a function vanishes on `sᶜ`, then its integral on `s` coincides with its integral on the
whole space.  -/
MeasureTheory.setIntegral_eq_integral_of_forall_compl_eq_zero : ∀ {X : Type u_1} {E : Type u_3} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  {f : X → E} {s : Set X} {μ : MeasureTheory.Measure X}, (∀ x ∉ s, f x = 0) → ∫ (x : X) in s, f x ∂μ = ∫ (x : X), f x ∂μ
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_insertList_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l toInsert : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      ∀ (contains : Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true)
        (not_contains : Std.Internal.List.containsKey k l = false),
        Std.Internal.List.getValueCast k (Std.Internal.List.insertList l toInsert) contains =
          Std.Internal.List.getValueCast k toInsert ⋯
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.continuous_sinh : Continuous Complex.sinh
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentDataAsCoalgebra f}
  (hom : (i : ι) → D₁.obj i ⟶ D₂.obj i)
  (comm :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom i₂))) =
          CategoryTheory.CategoryStruct.comp (hom i₁) (D₂.hom i₁ i₂))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.comm._autoParam)
  (hom_1 : (i : ι) → D₁.obj i ⟶ D₂.obj i)
  (comm_1 :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂)
            ((F.map (f i₁).op.toLoc).l.toFunctor.map ((F.map (f i₂).op.toLoc).r.toFunctor.map (hom_1 i₂))) =
          CategoryTheory.CategoryStruct.comp (hom_1 i₁) (D₂.hom i₁ i₂))
      CategoryTheory.Pseudofunctor.DescentDataAsCoalgebra.Hom.comm._autoParam),
  ({ hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 }) = (hom = hom_1)
-- Mathlib.CategoryTheory.ExtremalEpi
CategoryTheory.ExtremalEpi.isIso : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : C} (f : X ⟶ Y) [self : CategoryTheory.ExtremalEpi f]
  {Z : C} (p : X ⟶ Z) (i : Z ⟶ Y),
  CategoryTheory.CategoryStruct.comp p i = f → ∀ [CategoryTheory.Mono i], CategoryTheory.IsIso i
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso_hom_app_hom : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (X : CategoryTheory.Mon C),
  ((CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso C).hom.app X).hom = CategoryTheory.CategoryStruct.id X.X
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.constantCoeff_toSubring : ∀ {R : Type u_1} [inst : Ring R] (p : PowerSeries R) (T : Subring R) (hp : ∀ (n : ℕ), (PowerSeries.coeff n) p ∈ T),
  ↑(PowerSeries.constantCoeff (p.toSubring T hp)) = PowerSeries.constantCoeff p
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
/-- When both maps `S.f` and `S.g` of a short complex `S` are zero, this is the left homology map
data (for the identity of `S`) which relates the left homology data
`LeftHomologyData.ofIsLimitKernelFork` and `ofZeros` .  -/
CategoryTheory.ShortComplex.LeftHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        (hf : S.f = 0) →
          (hg : S.g = 0) →
            (c : CategoryTheory.Limits.KernelFork S.g) →
              (hc : CategoryTheory.Limits.IsLimit c) →
                CategoryTheory.ShortComplex.LeftHomologyMapData (CategoryTheory.CategoryStruct.id S)
                  (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc)
                  (CategoryTheory.ShortComplex.LeftHomologyData.ofZeros S hf hg)
-- Lean.Data.Lsp.Basic
/-- Controls if a cancel button should show to allow the user to cancel the operation.  -/
Lean.Lsp.WorkDoneProgressReport.cancellable : Lean.Lsp.WorkDoneProgressReport → Bool
-- Mathlib.Order.Restriction
Preorder.dependsOn_restrictLe : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} (a : α), DependsOn (Preorder.restrictLe a) (Set.Iic a)
-- Mathlib.Topology.Spectral.ConstructibleTopology
/-- The constructible topology on a topological space `X` has as a subbasis
the open and compact sets of `X` and their complements.  -/
constructibleTopology : (X : Type u_2) → [TopologicalSpace X] → TopologicalSpace X
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- Constructor for natural isomorphisms between functors constructed
with `functorMk`.  -/
CategoryTheory.Pretriangulated.Triangle.functorIsoMk' : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      {J : Type u_1} →
        [inst_2 : CategoryTheory.Category.{v_1, u_1} J] →
          {obj₁ obj₂ obj₃ : CategoryTheory.Functor J C} →
            {mor₁ : obj₁ ⟶ obj₂} →
              {mor₂ : obj₂ ⟶ obj₃} →
                {mor₃ : obj₃ ⟶ obj₁.comp (CategoryTheory.shiftFunctor C 1)} →
                  {obj₁' obj₂' obj₃' : CategoryTheory.Functor J C} →
                    {mor₁' : obj₁' ⟶ obj₂'} →
                      {mor₂' : obj₂' ⟶ obj₃'} →
                        {mor₃' : obj₃' ⟶ obj₁'.comp (CategoryTheory.shiftFunctor C 1)} →
                          (iso₁ : obj₁ ≅ obj₁') →
                            (iso₂ : obj₂ ≅ obj₂') →
                              (iso₃ : obj₃ ≅ obj₃') →
                                CategoryTheory.CategoryStruct.comp mor₁ iso₂.hom =
                                    CategoryTheory.CategoryStruct.comp iso₁.hom mor₁' →
                                  CategoryTheory.CategoryStruct.comp mor₂ iso₃.hom =
                                      CategoryTheory.CategoryStruct.comp iso₂.hom mor₂' →
                                    CategoryTheory.CategoryStruct.comp mor₃
                                          (CategoryTheory.Functor.whiskerRight iso₁.hom
                                            (CategoryTheory.shiftFunctor C 1)) =
                                        CategoryTheory.CategoryStruct.comp iso₃.hom mor₃' →
                                      (CategoryTheory.Pretriangulated.Triangle.functorMk mor₁ mor₂ mor₃ ≅
                                        CategoryTheory.Pretriangulated.Triangle.functorMk mor₁' mor₂' mor₃')
-- Mathlib.Data.Nat.Totient
/-- Euler's product formula for the totient function.  -/
Nat.totient_eq_mul_prod_factors : ∀ (n : ℕ), ↑n.totient = ↑n * ∏ p ∈ n.primeFactors, (1 - (↑p)⁻¹)
-- Mathlib.LinearAlgebra.RootSystem.Hom
/-- The identity morphism of a root pairing.  -/
RootPairing.Hom.id : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [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) → P.Hom P
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.natTransHomologyι_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} (c : ComplexShape ι) (i : ι) [inst_2 : CategoryTheory.CategoryWithHomology C]
  (K : HomologicalComplex C c), (HomologicalComplex.natTransHomologyι C c i).app K = K.homologyι i
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  CategoryTheory.IsIso (CategoryTheory.CategoryStruct.id X)
-- Init.Data.String.Lemmas.Pattern.Find.Char
String.Pos.find?_char_eq_none_iff : ∀ {c : Char} {s : String} {pos : s.Pos},
  pos.find? c = none ↔ ∀ (pos' : s.Pos), pos ≤ pos' → ∀ (h : pos' ≠ s.endPos), pos'.get h ≠ c
-- Lean.Parser.Command
/-- `omit` instructs Lean to not include a variable previously `include`d. Apart from variable names, it
can also refer to typeclass instance variables by type using the syntax `omit [TypeOfInst]`, in
which case all instance variables that unify with the given type are omitted. `omit` should usually
only be used in conjunction with `in` in order to keep the section structure simple.
 -/
Lean.Parser.Command.omit : Lean.Parser.Parser
-- Mathlib.Probability.Kernel.Composition.ParallelComp
ProbabilityTheory.Kernel.lintegral_parallelComp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel γ δ} [ProbabilityTheory.IsSFiniteKernel κ] [ProbabilityTheory.IsSFiniteKernel η]
  (ac : α × γ) {g : β × δ → ENNReal},
  Measurable g → ∫⁻ (bd : β × δ), g bd ∂(κ.parallelComp η) ac = ∫⁻ (b : β), ∫⁻ (d : δ), g (b, d) ∂η ac.2 ∂κ ac.1
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.comp_eval₂Hom : ∀ {R : Type u} {S₁ : Type v} {S₂ : Type w} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁]
  [inst_2 : CommSemiring S₂] (f : R →+* S₁) (g : σ → S₁) (φ : S₁ →+* S₂),
  φ.comp (MvPolynomial.eval₂Hom f g) = MvPolynomial.eval₂Hom (φ.comp f) fun i => φ (g i)
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.simpApp : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Mathlib.Order.Interval.Set.Fin
Fin.image_val_Ioo : ∀ {n : ℕ} (i j : Fin n), Fin.val '' Set.Ioo i j = Set.Ioo ↑i ↑j
-- Mathlib.Algebra.Module.LocalizedModule.Int
IsLocalizedModule.smul_mem_finsetIntegerMultiple_span : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {M' : Type u_3} [inst_3 : AddCommMonoid M'] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] [inst_6 : DecidableEq M] (x : M) (s : Finset M'),
  f x ∈ Submodule.span R ↑s → ∃ m, m • x ∈ Submodule.span R ↑(IsLocalizedModule.finsetIntegerMultiple S f s)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α] [inst_2 : Inhabited α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k : α},
      (List.map Sigma.fst l).contains k = false → (↑(t.insertMany! l)).getKey! k = t.getKey! k
-- Mathlib.Data.Finset.Range
Finset.notMem_range_self : ∀ {n : ℕ}, n ∉ Finset.range n
-- Mathlib.Topology.Maps.Basic
IsOpenMap.of_isEmpty : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [h : IsEmpty X] (f : X → Y),
  IsOpenMap f
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get?_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering} {a : α}, ∅.get? a = none
-- Mathlib.Data.List.Sublists
List.sublists'_map : ∀ {α : Type u} {β : Type v} (f : α → β) (l : List α), (List.map f l).sublists' = List.map (List.map f) l.sublists'
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys.constModifyKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {a : α} {f : β → β} {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l → Std.Internal.List.DistinctKeys (Std.Internal.List.Const.modifyKey a f l)
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Rat.IsIntegralClosure.intEquiv.congr_simp : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ],
  Rat.IsIntegralClosure.intEquiv R = Rat.IsIntegralClosure.intEquiv R
-- Mathlib.Computability.TuringMachine.Tape
Turing.Tape.mk'_head : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (L R : Turing.ListBlank Γ), (Turing.Tape.mk' L R).head = R.head
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.le.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Cutsat.LeCnstr), sizeOf (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.le c) = 1 + sizeOf c
-- Aesop.Frontend.Tactic
Aesop.Frontend.elabConfigUnsafe : {α : Type} → Lean.Name → Lean.Syntax → Lean.Elab.TermElabM α
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.transvection_add : ∀ {ι : Type u_1} {F : Type u_2} [inst : DecidableEq ι] [inst_1 : Fintype ι] [inst_2 : CommRing F] {i j : ι}
  (hij : i ≠ j) (b₁ b₂ : F),
  Matrix.SpecialLinearGroup.transvection hij (b₁ + b₂) =
    Matrix.SpecialLinearGroup.transvection hij b₁ * Matrix.SpecialLinearGroup.transvection hij b₂
-- Std.Async.Basic
Std.Async.EAsync.instMonadLiftBaseAsync : {ε : Type} → MonadLift Std.Async.BaseAsync (Std.Async.EAsync ε)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.insert_dep : ∀ {α : Type u_1} {M : Matroid α} {I X : Set α} {e : α}, M.IsBasis I X → e ∈ X \ I → M.Dep (insert e I)
-- Mathlib.Data.Finset.Sups
Finset.disjSups_subset_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeSup α] [inst_2 : OrderBot α]
  [inst_3 : DecidableRel Disjoint] {s₁ s₂ t : Finset α}, s₁ ⊆ s₂ → s₁.disjSups t ⊆ s₂.disjSups t
-- Mathlib.Algebra.Group.Hom.Defs
instSubsingletonMonoidHom : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] [Subsingleton M], Subsingleton (M →* N)