mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
/-- The second hexagon identity.  -/
CategoryTheory.BraidedCategory.hexagon_reverse_assoc : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.BraidedCategory C] (X Y Z : C) {Z_1 : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj Z X) Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp (β_ (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z).hom
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).hom Y) h))
-- Mathlib.Logic.Encodable.Basic
Encodable.encodeSum.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Encodable α] [inst_1 : Encodable β] (a : α),
  Encodable.encodeSum (Sum.inl a) = 2 * Encodable.encode a
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- a map `𝟙_ V ⟶ (ι.obj <| 𝟙_ D).obj (𝟙_ C)`, that we think of as defining a
natural transformation
`fromPUnit.{0} (𝟙_ V) ⟶ Functor.fromPUnit.{0} (𝟙_ C) ⋙ (ι.obj <| 𝟙_ D)`.  -/
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.unitUnit : (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.MonoidalCategory V} →
            (D : Type u₃) →
              {inst_4 : CategoryTheory.Category.{v₃, u₃} D} →
                {inst_5 : CategoryTheory.MonoidalCategoryStruct D} →
                  [self : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] →
                    CategoryTheory.MonoidalCategoryStruct.tensorUnit V ⟶
                      ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj
                            (CategoryTheory.MonoidalCategoryStruct.tensorUnit D)).obj
                        (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.Algebra.Free
/-- Embedding from additive magma to its free additive semigroup.  -/
AddMagma.FreeAddSemigroup.of : {α : Type u} → [inst : Add α] → α →ₙ+ AddMagma.FreeAddSemigroup α
-- Init.Data.Vector.Attach
Vector.countP_attachWith : ∀ {α : Type u_1} {n : ℕ} {p : α → Prop} {q : α → Bool} {xs : Vector α n} {H : ∀ a ∈ xs, p a},
  Vector.countP (fun a => q ↑a) (xs.attachWith p H) = Vector.countP q xs
-- Mathlib.Topology.Bases
/-- A countable disjoint union of second countable spaces is second countable.  -/
TopologicalSpace.instSecondCountableTopologySigmaOfCountable : ∀ {ι : Type u_1} {E : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (E i)] [Countable ι]
  [∀ (i : ι), SecondCountableTopology (E i)], SecondCountableTopology ((i : ι) × E i)
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.op_unop : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R Aᵐᵒᵖ), S.unop.op = S
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.Scheme.Opens.ι_image_basicOpen_topIso_inv : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens) (r : ↑(X.presheaf.obj (Opposite.op U))),
  (AlgebraicGeometry.Scheme.Hom.opensFunctor U.ι).obj
      ((↑U).basicOpen ((CategoryTheory.ConcreteCategory.hom U.topIso.inv) r)) =
    X.basicOpen r
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'₀₁₃_hom : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f),
  (F.mapComp' f₀₁ f₁₃ f ⋯).hom =
    CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).hom (F.map f₂₃))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).hom
          (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)))
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
/-- When a functor `F` preserves the left homology of a short complex `S`, this is the
canonical isomorphism `(S.map F).leftHomology ≅ F.obj S.leftHomology`.  -/
CategoryTheory.ShortComplex.mapLeftHomologyIso : {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] →
        [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (S : CategoryTheory.ShortComplex C) →
              (F : CategoryTheory.Functor C D) →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [inst_5 : S.HasLeftHomology] →
                    [inst_6 : F.PreservesLeftHomologyOf S] → (S.map F).leftHomology ≅ F.obj S.leftHomology
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiffAt_pi_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M} {n : WithTop ℕ∞} {ι : Type u_16}
  [inst_6 : Fintype ι] {Fi : ι → Type u_17} [inst_7 : (i : ι) → NormedAddCommGroup (Fi i)]
  [inst_8 : (i : ι) → NormedSpace 𝕜 (Fi i)] {φ : M → (i : ι) → Fi i},
  ContMDiffAt I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) n φ x ↔
    ∀ (i : ι), ContMDiffAt I (modelWithCornersSelf 𝕜 (Fi i)) n (fun x => φ x i) x
-- Mathlib.Order.KrullDimension
Order.height_coe_withTop : ∀ {α : Type u_1} [inst : Preorder α] (x : α), Order.height ↑x = Order.height x
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- The canonical map `WithLp.equiv` between `PiLp ∞ β` and `Π i, β i` as a linear isometric
equivalence.  -/
PiLp.equivₗᵢ : {𝕜 : Type u_1} →
  {ι : Type u_2} →
    (β : ι → Type u_4) →
      [inst : Fintype ι] →
        [inst_1 : Semiring 𝕜] →
          [inst_2 : (i : ι) → SeminormedAddCommGroup (β i)] →
            [inst_3 : (i : ι) → Module 𝕜 (β i)] → PiLp ⊤ β ≃ₗᵢ[𝕜] (i : ι) → β i
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_nsmul_of_ne_zero : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : AddMonoid α]
  [inst_3 : AddMonoid β] [inst_4 : FunLike F α β] [AddHomClass F α β] {n : ℕ},
  n ≠ 0 → ∀ (f : F) (s : Finset α), Finset.image (⇑f) (n • s) = n • Finset.image (⇑f) s
-- Mathlib.CategoryTheory.Limits.Types.Products
CategoryTheory.Limits.Types.binaryProductIso_hom_comp_snd : ∀ (X Y : Type u),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Types.binaryProductIso X Y).hom (TypeCat.ofHom Prod.snd) =
    CategoryTheory.Limits.prod.snd
-- Init.System.IOError
IO.Error.alreadyExists.sizeOf_spec : ∀ (filename : Option String) (osCode : UInt32) (details : String),
  sizeOf (IO.Error.alreadyExists filename osCode details) = 1 + sizeOf filename + sizeOf osCode + sizeOf details
-- Init.Tactics
/-- `rw?` tries to find a lemma which can rewrite the goal.

`rw?` should not be left in proofs; it is a search tool, like `apply?`.

Suggestions are printed as `rw [h]` or `rw [← h]`.

You can use `rw? [-my_lemma, -my_theorem]` to prevent `rw?` using the named lemmas.
 -/
Lean.Parser.Tactic.rewrites? : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.unit.sizeOf_spec : ∀ {C : Type u} [inst : SizeOf C], sizeOf CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.unit = 1
-- Mathlib.Topology.Bornology.Absorbs
absorbs_iUnion : ∀ {M : Type u_1} {α : Type u_2} [inst : Bornology M] [inst_1 : SMul M α] {s : Set α} {ι : Sort u_3} [Finite ι]
  {t : ι → Set α}, Absorbs M s (⋃ i, t i) ↔ ∀ (i : ι), Absorbs M s (t i)
-- Std.Data.DHashMap.Raw
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Raw.WF.wf : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β},
  0 < m.buckets.size → (∀ [EquivBEq α] [LawfulHashable α], Std.DHashMap.Internal.Raw.WFImp m) → m.WF
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey!_mem : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α], t.WF → t.isEmpty = false → t.minKey! ∈ t
-- Mathlib.Algebra.Group.Equiv.Basic
AddEquiv.symm_addMonoidHomCongrLeft : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [inst : AddZeroClass M₁] [inst_1 : AddZeroClass M₂]
  [inst_2 : AddCommMonoid N] (e : M₁ ≃+ M₂), e.addMonoidHomCongrLeft.symm = e.symm.addMonoidHomCongrLeft
-- Std.Data.ExtTreeSet.Basic
/-- Returns the `n`-th smallest element, or `none` if `n` is at least `t.size`.  -/
Std.ExtTreeSet.atIdx? : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → ℕ → Option α
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.liftUnique.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {Z : D} (F : CategoryTheory.Functor C D) (M : (x : C) → Z ⟶ F.obj x)
  (hM : ∀ (x y : C) (f : x ⟶ y), CategoryTheory.CategoryStruct.comp (M x) (F.map f) = M y)
  (G : CategoryTheory.Functor (CategoryTheory.WithInitial C) D) (h : CategoryTheory.WithInitial.incl.comp G ≅ F)
  (hG : G.obj CategoryTheory.WithInitial.star ≅ Z)
  (hh :
    ∀ (x : C),
      CategoryTheory.CategoryStruct.comp hG.symm.hom
          (G.map (CategoryTheory.WithInitial.starInitial.to (CategoryTheory.WithInitial.incl.obj x))) =
        CategoryTheory.CategoryStruct.comp (M x) (h.symm.hom.app x)),
  CategoryTheory.WithInitial.liftUnique F M hM G h hG hh =
    CategoryTheory.NatIso.ofComponents
      (fun X =>
        match X with
        | CategoryTheory.WithInitial.of x => h.app x
        | CategoryTheory.WithInitial.star => hG)
      ⋯
-- Std.Data.ByteSlice
ByteSlice.instInhabited : Inhabited ByteSlice
-- Mathlib.Tactic.CategoryTheory.MonoidalComp
/-- Compose two morphisms in a monoidal category,
inserting unitors and associators between as necessary.  -/
CategoryTheory.MonoidalCategory.«term_⊗≫_» : Lean.TrailingParserDescr
-- Mathlib.ModelTheory.Graph
FirstOrder.Language.simpleGraph_model : ∀ {V : Type u} (G : SimpleGraph V), V ⊨ FirstOrder.Language.Theory.simpleGraph
-- Mathlib.Logic.Equiv.Defs
/-- The sort of maps from `False` is equivalent to `PUnit`.  -/
Equiv.falseArrowEquivPUnit : (α : Sort u_1) → (False → α) ≃ PUnit.{u}
-- Mathlib.RingTheory.Multiplicity
emultiplicity_eq_of_associated_left : ∀ {α : Type u_1} [inst : CommMonoid α] {a b c : α}, Associated a b → emultiplicity b c = emultiplicity a c
-- Lean.Meta.Sym.Canon
/-- Check that `e` is definitionally equal to `inst` at instance transparency.
Returns `inst` on success, `e` with a reported issue on failure.  -/
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.checkDefEqInst : Lean.Expr → Lean.Expr → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
derivWithin_cosh : ∀ {f : ℝ → ℝ} {x : ℝ} {s : Set ℝ},
  DifferentiableWithinAt ℝ f s x →
    UniqueDiffWithinAt ℝ s x → derivWithin (fun x => Real.cosh (f x)) s x = Real.sinh (f x) * derivWithin f s x
-- Mathlib.RingTheory.Etale.QuasiFinite
/-- A key induction step of `exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq`.  -/
_private.Mathlib.RingTheory.Etale.QuasiFinite.0.Algebra.exists_etale_completeOrthogonalIdempotents_forall_liesOver_eq_aux : ∀ {R : Type u} {S : Type (max u v)} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R)
  [inst_3 : p.IsPrime] (q : Ideal S) (R' : Type u) [inst_4 : CommRing R'] [inst_5 : Algebra R R'] [Algebra.Etale R R']
  (P : Ideal R') [inst_7 : P.IsPrime] [inst_8 : P.LiesOver p] (e : TensorProduct R R' S)
  (P' : Ideal (TensorProduct R R' S)) [P'.IsPrime] [P'.LiesOver P],
  Ideal.comap Algebra.TensorProduct.includeRight.toRingHom P' = q →
    e ∉ P' →
      Function.Bijective ⇑(Ideal.ResidueField.mapₐ p P (Algebra.ofId R R') ⋯) →
        (∀ (P'' : Ideal (TensorProduct R R' S)), P''.IsPrime → P''.LiesOver P → e ∉ P'' → P'' = P') →
          ∀ (R'' : Type u) [inst_11 : CommRing R''] [inst_12 : Algebra R' R''] [inst_13 : Algebra R R'']
            [inst_14 : IsScalarTower R R' R''] [Algebra.Etale R' R''] (Q : Ideal R'') [inst_16 : Q.IsPrime]
            [inst_17 : Q.LiesOver P] (n : ℕ) (e' : Fin (n + 1 + 1) → TensorProduct R R'' S),
            CompleteOrthogonalIdempotents e' →
              e' 0 = (Algebra.TensorProduct.map (Algebra.ofId R' R'') (AlgHom.id R S)) e →
                ∀ (Q' : Fin n → Ideal (TensorProduct R R'' S)) [∀ (i : Fin n), (Q' i).IsPrime]
                  [∀ (i : Fin n), (Q' i).LiesOver Q],
                  Function.Bijective ⇑(Ideal.ResidueField.mapₐ P Q (Algebra.ofId R' R'') ⋯) →
                    (∀ (i : Fin n), e' i.succ.castSucc ∉ Q' i) →
                      (∀ (P'' : Ideal (TensorProduct R R'' S)),
                          e' 0 ∈ P'' →
                            P''.IsPrime →
                              P''.LiesOver Q →
                                e' (Fin.last (n + 1)) ∈ P'' ∧ ∀ (i : Fin n), e' i.succ.castSucc ∉ P'' → P'' = Q' i) →
                        ∃ R' x x_1, ∃ (_ : Algebra.Etale R R'), ∃ P, ∃ (x_3 : P.IsPrime) (x_4 : P.LiesOver p), ∃ n e, ⋯
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.le_maxKey_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  (hc : t.contains k = true), (cmp k (t.maxKey ⋯)).isLE = true
-- Lean.Syntax
Lean.Syntax.TopDown.mk : Bool → Lean.Syntax → Lean.Syntax.TopDown
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimObjMap_π : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (W : CategoryTheory.Functor J (Type w)) {F₁ F₂ : CategoryTheory.Functor J C}
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F₁] [inst_3 : CategoryTheory.Limits.HasWeightedLimit W F₂]
  (f : F₁ ⟶ F₂) ⦃j : J⦄ (x : W.obj j),
  CategoryTheory.CategoryStruct.comp (W.weightedLimObjMap f) (W.weightedLimObjObjπ F₂ x) =
    CategoryTheory.CategoryStruct.comp (W.weightedLimObjObjπ F₁ x) (f.app j)
-- Mathlib.Topology.Hom.ContinuousEvalConst
ContinuousEvalConst.continuous_eval_const : ∀ {F : Type u_1} {α : outParam (Type u_2)} {X : outParam (Type u_3)} {inst : FunLike F α X}
  {inst_1 : TopologicalSpace F} {inst_2 : TopologicalSpace X} [self : ContinuousEvalConst F α X] (x : α),
  Continuous fun f => f x
-- Mathlib.Algebra.Field.Subfield.Defs
Subfield.coe_toSubmonoid : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K), ↑s.toSubmonoid = ↑s
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.WalkingParallelPairHom.left : CategoryTheory.Limits.WalkingParallelPairHom CategoryTheory.Limits.WalkingParallelPair.zero
  CategoryTheory.Limits.WalkingParallelPair.one
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F : C ⥤ Dᵒᵖ` preserves finite colimits, then `F.leftOp : Cᵒᵖ ⥤ D` preserves finite
limits.  -/
CategoryTheory.Limits.preservesFiniteLimits_leftOp : ∀ {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.Limits.PreservesFiniteColimits F],
  CategoryTheory.Limits.PreservesFiniteLimits F.leftOp
-- Mathlib.LinearAlgebra.AffineSpace.FiniteDimensional
/-- The `vectorSpan` of collinear points is finite-dimensional.  -/
Collinear.finiteDimensional_vectorSpan : ∀ {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] {s : Set P}, Collinear k s → FiniteDimensional k ↥(vectorSpan k s)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defn.sizeOf_spec : ∀ (e : Lean.Expr) (p : Int.Internal.Linear.Poly),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.EqCnstrProof.defn e p) = 1 + sizeOf e + sizeOf p
-- Lean.LocalContext
/-- Sets the value of an `ldecl`, otherwise returns `cdecl`s unchanged.  -/
Lean.LocalDecl.setValue : Lean.LocalDecl → Lean.Expr → Lean.LocalDecl
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pattern.Model.Pos.not_matchesAt_or_isLongestMatchAt_skipWhile : ∀ {ρ : Type} (pat : ρ) [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s : String.Slice} (pos : s.Pos),
  ¬String.Slice.Pattern.Model.MatchesAt pat (pos.skipWhile pat) ∨
    String.Slice.Pattern.Model.IsLongestMatchAt pat (pos.skipWhile pat) (pos.skipWhile pat)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
/-- **Alias** of `FunLike.coe_sub`. -/
ContDiffMapSupportedIn.coe_sub : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Sub F] [inst_2 : Sub β]
  [IsSubApply F α β] (f g : F), ⇑(f - g) = ⇑f - ⇑g
-- Lean.Data.Lsp.Extra
Lean.Lsp.LineRange.end : Lean.Lsp.LineRange → ℕ
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Inhabited α] {k : α}
  {f : β → β} {hc : k ∈ t.modify k f}, (t.modify k f).getKey k hc = k
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Pasting
/-- The canonical isomorphism `(Y ⨿[X] Z) ⨿[Z] W ≅ Y ⨿[X] W`  -/
CategoryTheory.Limits.pushoutLeftPushoutInrIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Y) →
        (g : X ⟶ Z) →
          (g' : Z ⟶ W) →
            [inst_1 : CategoryTheory.Limits.HasPushout f g] →
              [inst_2 : CategoryTheory.Limits.HasPushout (CategoryTheory.Limits.pushout.inr f g) g'] →
                CategoryTheory.Limits.pushout (CategoryTheory.Limits.pushout.inr f g) g' ≅
                  CategoryTheory.Limits.pushout f (CategoryTheory.CategoryStruct.comp g g')
-- Mathlib.Combinatorics.Additive.Dissociation
Finset.sum_sub_sum_mem_addSpan : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : DecidableEq α] [inst_2 : Fintype α] {s t u : Finset α},
  t ⊆ s → u ⊆ s → ∑ a ∈ t, a - ∑ a ∈ u, a ∈ s.addSpan
-- Mathlib.Computability.Primrec.List
Primrec.list_ofFn : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ] {n : ℕ} {f : Fin n → α → σ},
  (∀ (i : Fin n), Primrec (f i)) → Primrec fun a => List.ofFn fun i => f i a
-- Mathlib.Analysis.InnerProductSpace.Basic
_private.Mathlib.Analysis.InnerProductSpace.Basic.0.termIK : Lean.ParserDescr
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_inf : ∀ {α : Type u_1} [inst : LE α] (s t : UpperSet α), ↑(s ⊓ t) = ↑s ∪ ↑t
-- Init.Data.Range.Polymorphic.Int
Std.PRange.instIsAlwaysFiniteInt : Std.Rxc.IsAlwaysFinite ℤ
-- Mathlib.Analysis.InnerProductSpace.Positive
LinearMap.isPositive_id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  LinearMap.id.IsPositive
-- Mathlib.Data.Fintype.Card
Finite.exists_univ_list : ∀ (α : Type u_4) [Finite α], ∃ l, l.Nodup ∧ ∀ (x : α), x ∈ l
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.IsPrefix.rfl : ∀ {α : Type} {decls : Array (Std.Sat.AIG.Decl α)}, Std.Sat.AIG.IsPrefix decls decls
-- Mathlib.Topology.Semicontinuity.Basic
/-- **Alias** of the forward direction of `upperSemicontinuousAt_iff_limsup_le`. -/
UpperSemicontinuousAt.limsup_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ] {f : α → γ},
  UpperSemicontinuousAt f x → Filter.limsup f (nhds x) ≤ f x
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwInfo.mk.sizeOf_spec : ∀ (rootExpr subExpr : Lean.Expr) (rflTarget? : Option Lean.Expr) (gpos : Array Mathlib.Tactic.ClickSuggestions.GrwPos)
  (rwKind : Mathlib.Tactic.ClickSuggestions.RwKind),
  sizeOf { rootExpr := rootExpr, subExpr := subExpr, rflTarget? := rflTarget?, gpos := gpos, rwKind := rwKind } =
    1 + sizeOf rootExpr + sizeOf subExpr + sizeOf rflTarget? + sizeOf gpos + sizeOf rwKind
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_one_div_of_neg : ∀ {a b : ℝ}, a < 0 → b < 0 → ∫ (x : ℝ) in a..b, 1 / x = Real.log (b / a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKeyD_alter_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [Inhabited α] (h : t.WF) {k fallback : α} {f : Option β → Option β},
  (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl.getKeyD k fallback =
    if (f (Std.DTreeMap.Internal.Impl.Const.get? t k)).isSome = true then k else fallback
-- Mathlib.Data.ZMod.Basic
ZMod.castHom.eq_1 : ∀ {n m : ℕ} (h : m ∣ n) (R : Type u_2) [inst : Ring R] [inst_1 : CharP R m],
  ZMod.castHom h R = { toFun := ZMod.cast, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.Analysis.Calculus.VectorField
VectorField.lieBracketWithin_of_mem_nhdsWithin : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E},
  t ∈ nhdsWithin x s →
    UniqueDiffWithinAt 𝕜 s x →
      DifferentiableWithinAt 𝕜 V t x →
        DifferentiableWithinAt 𝕜 W t x → VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracketWithin 𝕜 V W t x
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of `AffineSubspace.isConnected_setOfPred_sOppSide`. -/
AffineSubspace.isConnected_setOf_sOppSide : ∀ {V : Type u_2} {P : Type u_4} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V]
  [inst_2 : PseudoMetricSpace P] [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} {x : P},
  x ∉ s → (↑s).Nonempty → IsConnected {y | s.SOppSide x y}
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin.eq_1 : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (s : Set A),
  Algebra.adjoin R s = { toSubsemiring := Subsemiring.closure (Set.range ⇑(algebraMap R A) ∪ s), algebraMap_mem' := ⋯ }
-- Mathlib.Topology.Spectral.ConstructibleTopology
WithConstructibleTopology.isClosed_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set (WithConstructibleTopology X)},
  IsClosed s ↔ IsClosed (WithTopology.toTopology (constructibleTopology X) ⁻¹' s)
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.multisetProd : ∀ {R : Type u_1} [inst : CommSemiring R] {m : Multiset (Polynomial R)}, (∀ f ∈ m, f.Splits) → m.prod.Splits
-- Mathlib.LinearAlgebra.Contraction
TensorProduct.dualDistribInvOfBasis.eq_1 : ∀ {R : Type u_7} {M : Type u_8} {N : Type u_9} {ι : Type u_10} {κ : Type u_11} [inst : DecidableEq ι]
  [inst_1 : DecidableEq κ] [inst_2 : Fintype ι] [inst_3 : Fintype κ] [inst_4 : CommSemiring R]
  [inst_5 : AddCommMonoid M] [inst_6 : AddCommMonoid N] [inst_7 : Module R M] [inst_8 : Module R N]
  (b : Module.Basis ι R M) (c : Module.Basis κ R N),
  TensorProduct.dualDistribInvOfBasis b c =
    ∑ i,
      ∑ j,
        (LinearMap.ringLmapEquivSelf R ℕ (TensorProduct R (Module.Dual R M) (Module.Dual R N))).symm
            (b.dualBasis i ⊗ₜ[R] c.dualBasis j) ∘ₗ
          LinearMap.applyₗ (c j) ∘ₗ LinearMap.applyₗ (b i) ∘ₗ TensorProduct.lcurry (RingHom.id R) M N R