mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.shiftClosure_eq_self : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] [P.IsClosedUnderIsomorphisms] [P.IsStableUnderShift A],
  P.shiftClosure A = P
-- Lean.Meta.Tactic.Cleanup
_private.Lean.Meta.Tactic.Cleanup.0.Lean.Meta.cleanupCore.addUsedFVars : Lean.Expr → StateRefT' IO.RealWorld (Bool × Lean.FVarIdSet) Lean.MetaM Unit
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- **Alias** of `CategoryTheory.PreZeroHypercover.comp_s₀`. -/
AlgebraicGeometry.Scheme.Cover.comp_idx_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {X Y Z : CategoryTheory.PreZeroHypercover S}
  (f : X.Hom Y) (g : Y.Hom Z) (a : X.I₀), (CategoryTheory.CategoryStruct.comp f g).s₀ a = g.s₀ (f.s₀ a)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.filterMap_equiv_map : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {γ : α → Type w} [EquivBEq α] [LawfulHashable α] {f : (a : α) → β a → γ a},
  (↑m).WF →
    (↑(Std.DHashMap.Internal.Raw₀.filterMap (fun k v => some (f k v)) m)).Equiv ↑(Std.DHashMap.Internal.Raw₀.map f m)
-- Mathlib.Algebra.FiveLemma
/-- A special case of the five lemma in terms of additive groups.
For a diagram explaining the variables, see the module docstring.  -/
AddMonoidHom.bijective_of_bijective_of_injective_of_left_exact : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} [inst : AddGroup M₁]
  [inst_1 : AddGroup M₂] [inst_2 : AddGroup M₃] [inst_3 : AddGroup N₁] [inst_4 : AddGroup N₂] [inst_5 : AddGroup N₃]
  (f₁ : M₁ →+ M₂) (f₂ : M₂ →+ M₃) (g₁ : N₁ →+ N₂) (g₂ : N₂ →+ N₃) (i₁ : M₁ →+ N₁) (i₂ : M₂ →+ N₂) (i₃ : M₃ →+ N₃),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      Function.Exact ⇑f₁ ⇑f₂ →
        Function.Exact ⇑g₁ ⇑g₂ →
          Function.Bijective ⇑i₂ →
            Function.Injective ⇑i₃ → Function.Injective ⇑f₁ → Function.Injective ⇑g₁ → Function.Bijective ⇑i₁
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- An auxiliary structure containing the data to construct the presentation in
`Generators.exists_presentation_of_free`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            (P : Algebra.Generators R S ι) →
              {σ : Type u_5} → Module.Basis σ S P.toExtension.Cotangent → Type (max u_1 u_4)
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.isIso_eTruncGE_obj_map_truncGEπ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) [CategoryTheory.IsTriangulated C] (a b : EInt),
  a ≤ b → ∀ (X : C), CategoryTheory.IsIso ((t.eTruncGE.obj b).map ((t.eTruncGEπ a).app X))
-- Mathlib.Data.List.MinMax
List.getD_max?_eq_unbotD_maximum : ∀ {α : Type u_1} [inst : LinearOrder α] (l : List α) (d : α), l.max?.getD d = WithBot.unbotD d l.maximum
-- Mathlib.Topology.Inseparable
GeneralizingMap.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z}, GeneralizingMap f → GeneralizingMap g → GeneralizingMap (g ∘ f)
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.le_prev_iff_lt : ∀ {s : String.Slice} {p q : s.Pos} {h : q ≠ s.startPos}, p ≤ q.prev h ↔ p < q
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- [Stacks Tag 01Z4](https://stacks.math.columbia.edu/tag/01Z4) ((1)) -/
AlgebraicGeometry.exists_isAffineOpen_preimage_eq : ∀ {I : Type u} [inst : CategoryTheory.Category.{u, u} I] (D : CategoryTheory.Functor I AlgebraicGeometry.Scheme)
  (c : CategoryTheory.Limits.Cone D) (hc : CategoryTheory.Limits.IsLimit c) [CategoryTheory.IsCofiltered I]
  [∀ {i j : I} (f : i ⟶ j), AlgebraicGeometry.IsAffineHom (D.map f)] [∀ (i : I), QuasiSeparatedSpace ↥(D.obj i)]
  (U : c.pt.Opens),
  AlgebraicGeometry.IsAffineOpen U →
    ∃ i V, AlgebraicGeometry.IsAffineOpen V ∧ (TopologicalSpace.Opens.map (c.π.app i).base).obj V = U
-- Lean.Meta.Tactic.Induction
_private.Lean.Meta.Tactic.Induction.0.Lean.Meta.finalize : Lean.MVarId →
  Array Lean.Meta.AltVarNames →
    Lean.Meta.RecursorInfo →
      Array Lean.FVarId →
        Lean.Expr → Array Lean.Expr → Lean.Meta.FVarSubst → Lean.Expr → Lean.MetaM (Array Lean.Meta.InductionSubgoal)
-- Mathlib.Data.Multiset.Functor
/-- Map each element of a `Multiset` to an action, evaluate these actions in order,
and collect the results.
 -/
Multiset.traverse : {F : Type u → Type u} →
  [inst : Applicative F] → [CommApplicative F] → {α' β' : Type u} → (α' → F β') → Multiset α' → F (Multiset β')
-- Mathlib.Topology.Neighborhoods
/-- A set `s` is closed iff for every point `x`, if there is a point `y` close to `x` that belongs
to `s` then `x` is in `s`.  -/
isClosed_iff_frequently : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, IsClosed s ↔ ∀ (x : X), (∃ᶠ (y : X) in nhds x, y ∈ s) → x ∈ s
-- Mathlib.Analysis.Calculus.IteratedDeriv.Lemmas
iteratedDerivWithin_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : ℕ} {x : 𝕜} {s : Set 𝕜},
  x ∈ s →
    UniqueDiffOn 𝕜 s →
      ∀ {𝔸 : Type u_5} [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸] {f g : 𝕜 → 𝔸},
        ContDiffWithinAt 𝕜 (↑n) f s x →
          ContDiffWithinAt 𝕜 (↑n) g s x →
            iteratedDerivWithin n (f * g) s x =
              ∑ i ∈ Finset.range (n + 1),
                ↑(n.choose i) * iteratedDerivWithin i f s x * iteratedDerivWithin (n - i) g s x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insertMany_cons : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l : List ((a : α) × β a)} {p : (a : α) × β a}, t.insertMany (p :: l) = (t.insert p.fst p.snd).insertMany l
-- Mathlib.Order.SuccPred.Limit
/-- **Alias** of `Order.isPredPrelimit_iff_isMax`. -/
Order.isPredPrelimit_iff : ∀ {α : Type u_1} {a : α} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α],
  Order.IsPredPrelimit a ↔ IsMax a
-- Lean.Parser.Term
Lean.Parser.Term.trueVal.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.Assignment.instToString.match_1.splitter : (motive : Std.Tactic.BVDecide.LRAT.Internal.Assignment → Sort u_1) →
  (a : Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
    (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.pos) →
      (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.neg) →
        (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.both) →
          (Unit → motive Std.Tactic.BVDecide.LRAT.Internal.Assignment.unassigned) → motive a
-- Mathlib.RingTheory.Multiplicity
finiteMultiplicity_iff_emultiplicity_ne_top : ∀ {α : Type u_1} [inst : Monoid α] {a b : α}, FiniteMultiplicity a b ↔ emultiplicity a b ≠ ⊤
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- The continuous image of an analytic set is analytic  -/
MeasureTheory.AnalyticSet.image_of_continuousOn : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_3} [inst_1 : TopologicalSpace β] {s : Set α},
  MeasureTheory.AnalyticSet s → ∀ {f : α → β}, ContinuousOn f s → MeasureTheory.AnalyticSet (f '' s)
-- Batteries.CodeAction.Misc
/-- Invoking hole code action "Generate a list of equations for a recursive definition" in the
following:
```lean
def foo : Expr → Unit := _
```

produces:

```lean
def foo : Expr → Unit := fun
  | .bvar deBruijnIndex => _
  | .fvar fvarId => _
  | .mvar mvarId => _
  | .sort u => _
  | .const declName us => _
  | .app fn arg => _
  | .lam binderName binderType body binderInfo => _
  | .forallE binderName binderType body binderInfo => _
  | .letE declName type value body nonDep => _
  | .lit _ => _
  | .mdata data expr => _
  | .proj typeName idx struct => _
```

 -/
Batteries.CodeAction.eqnStub : Lean.CodeAction.HoleCodeAction
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.eHomWhiskerLeft_comp : ∀ (V : Type u') [inst : CategoryTheory.Category.{v', u'} V] [inst_1 : CategoryTheory.MonoidalCategory V] {C : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} C] [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V C] (X : C)
  {Y Y' Y'' : C} (g : Y ⟶ Y') (g' : Y' ⟶ Y''),
  CategoryTheory.eHomWhiskerLeft V X (CategoryTheory.CategoryStruct.comp g g') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eHomWhiskerLeft V X g) (CategoryTheory.eHomWhiskerLeft V X g')
-- Mathlib.RingTheory.TensorProduct.Quotient
/-- `(A ⧸ I) ⊗[A] B` is isomorphic as an `A ⧸ I`-algebra to `B ⧸ I B`.  -/
Algebra.TensorProduct.quotIdealMapEquivQuotTensor : {A : Type u_1} →
  (B : Type u_2) →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra A B] → (I : Ideal A) → (B ⧸ Ideal.map (algebraMap A B) I) ≃ₐ[A ⧸ I] TensorProduct A (A ⧸ I) B
-- Std.Http.Data.Chunk
/-- Creates an empty trailer with no headers.
 -/
Std.Http.Trailer.empty : Std.Http.Trailer
-- Std.Data.DTreeMap.Internal.WF.Defs
/-- The empty tree is well-formed. Later shown to be subsumed by `.wf`.  -/
Std.DTreeMap.Internal.Impl.WF.empty : ∀ {α : Type u} [inst : Ord α] {x : α → Type v}, Std.DTreeMap.Internal.Impl.empty.WF
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.cons_ne_zero : ∀ {M : Type u_1} [inst : GroupWithZero M] (r : ℤ) {x : M},
  x ≠ 0 → ∀ {l : Mathlib.Tactic.FieldSimp.NF M}, l.eval ≠ 0 → ((r, x) ::ᵣ l).eval ≠ 0
-- Lean.Environment
_private.Lean.Environment.0.Lean.ImportState.mk : Std.HashMap Lean.Name Lean.ImportedModule✝ → Array Lean.Name → Lean.ImportState
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- Given a Localization map `f : M →+ N` for a Submonoid `S ⊆ M`, for all `x₁ : M`
and `y₁ ∈ S`, if `x₂ : M, y₂ ∈ S` are such that `(f x₁ - f y₁) + f y₂ = f x₂`, then there exists
`c ∈ S` such that `x₁ + y₂ + c = x₂ + y₁ + c`.  -/
AddSubmonoid.LocalizationMap.exists_of_sec_mk' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) (x : M) (y : ↥S), ∃ c, ↑c + (↑(f.sec (f.mk' x y)).2 + x) = ↑c + (↑y + (f.sec (f.mk' x y)).1)
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Comma.hasFiniteLimits : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} [CategoryTheory.Limits.HasFiniteLimits A] [CategoryTheory.Limits.HasFiniteLimits B]
  [CategoryTheory.Limits.PreservesFiniteLimits R], CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Comma L R)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.instHasZeroMorphisms.eq_1 : ∀ {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} D]
  [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory D],
  CategoryTheory.Mon.instHasZeroMorphisms = { zero := CategoryTheory.Mon.instZeroHom, comp_zero := ⋯, zero_comp := ⋯ }
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap_comp_assoc : ∀ {J : Type w} [inst : CategoryTheory.SmallCategory J] {κ : Cardinal.{w}}
  {D₁ D₂ D₃ : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ} (h₁₂ : D₁ ≤ D₂)
  (h₂₃ : D₂ ≤ D₃) {Z : J} (h : D₃.top ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap h₁₂)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap h₂₃)
        h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.functorMap ⋯) h
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.mem_source : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : Z}, x ∈ e.source ↔ proj x ∈ e.baseSet
-- Mathlib.Order.Interval.Finset.Basic
Set.Infinite.not_bddAbove : ∀ {α : Type u_2} [inst : Preorder α] [LocallyFiniteOrderBot α] {s : Set α}, s.Infinite → ¬BddAbove s
-- Mathlib.GroupTheory.Complement
Subgroup.smul_toLeftFun : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {F : Type u_2} [inst_1 : Group F] [inst_2 : MulAction F G]
  [inst_3 : MulAction.QuotientAction F H] (f : F) (S : H.LeftTransversal) (g : G),
  f • ↑(⋯.toLeftFun g) = ↑(⋯.toLeftFun (f • g))
-- Mathlib.Analysis.CStarAlgebra.Module.Defs
_private.Mathlib.Analysis.CStarAlgebra.Module.Defs.0.CStarModule.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Algebra.BigOperators.Finprod
/-- Given a family of pairwise disjoint finite sets `t i` indexed by a finite type, the
sum of `f a` over the union `⋃ i, t i` is equal to the sum over all indexes `i` of the
sums of `f a` over `a ∈ t i`.  -/
finsum_mem_iUnion : ∀ {α : Type u_1} {ι : Type u_3} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} [Finite ι] {t : ι → Set α},
  Pairwise (Function.onFun Disjoint t) →
    (∀ (i : ι), (t i).Finite) → ∑ᶠ (a : α) (_ : a ∈ ⋃ i, t i), f a = ∑ᶠ (i : ι) (a : α) (_ : a ∈ t i), f a
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.subtheoryModel_struc : ∀ {L : FirstOrder.Language} {T : L.Theory} (M : T.ModelType) {T' : L.Theory} (h : T' ⊆ T),
  (M.subtheoryModel h).struc = M.struc
-- Mathlib.Algebra.Group.Units.Hom
AddUnits.liftRight_neg_add : ∀ {M : Type u} {N : Type v} [inst : AddMonoid M] [inst_1 : AddMonoid N] {f : M →+ N} {g : M → AddUnits N}
  (h : ∀ (x : M), ↑(g x) = f x) (x : M), ↑(-(AddUnits.liftRight f g h) x) + f x = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.foldrM_eq_foldrM_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → β → δ → m δ} {init : δ},
  Std.TreeMap.Raw.foldrM f init t = List.foldrM (fun a b => f a.1 a.2 b) init t.toList
-- Mathlib.RingTheory.MvPowerSeries.Rename
MvPowerSeries.killCompl_comp_rename : ∀ {σ : Type u_1} {τ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {e : σ ↪ τ},
  (MvPowerSeries.killCompl e).comp (MvPowerSeries.rename ⇑e) = AlgHom.id R (MvPowerSeries σ R)
-- Std.Http.Data.Method
/-- Apply partial modifications to a resource.
Source: https://www.rfc-editor.org/rfc/rfc5789#section-2
 -/
Std.Http.Method.patch : Std.Http.Method
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- A projection. It stores the structure name, the projection index and the arity.  -/
Lean.Meta.RefinedDiscrTree.Key.proj : Lean.Name → ℕ → ℕ → Lean.Meta.RefinedDiscrTree.Key
-- Lean.DocString.Extension
Lean.getModuleDoc? : Lean.Environment → Lean.Name → Option (Array Lean.ModuleDoc)
-- Mathlib.Data.ZMod.Basic
AddSubgroupClass.instZModSMul : {n : ℕ} →
  {S : Type u_1} →
    {G : Type u_2} →
      [inst : AddCommGroup G] →
        [inst_1 : SetLike S G] → [AddSubgroupClass S G] → {K : S} → [Module (ZMod n) G] → SMul (ZMod n) ↥K
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedContext.mk.sizeOf_spec : ∀ (declName? : Option Lean.Name) (options : Lean.Options) (openDecls : List Lean.OpenDecl)
  (macroStack : Lean.Elab.MacroStack) (errToSorry : Bool) (levelNames : List Lean.Name)
  (fixedTermElabs : Array Lean.Elab.Term.FixedTermElabRef),
  sizeOf
      { declName? := declName?, options := options, openDecls := openDecls, macroStack := macroStack,
        errToSorry := errToSorry, levelNames := levelNames, fixedTermElabs := fixedTermElabs } =
    1 + sizeOf declName? + sizeOf options + sizeOf openDecls + sizeOf macroStack + sizeOf errToSorry +
        sizeOf levelNames +
      sizeOf fixedTermElabs
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessResult.mk.sizeOf_spec : ∀ (type cacheKeyType : Lean.Expr) (kind : Lean.Meta.PreprocessKind✝),
  sizeOf { type := type, cacheKeyType := cacheKeyType, kind := kind } =
    1 + sizeOf type + sizeOf cacheKeyType + sizeOf kind
-- Mathlib.Order.PFilter
/-- A filter on `P` is a subset of `P`.  -/
Order.PFilter.instSetLike : {P : Type u_1} → [inst : Preorder P] → SetLike (Order.PFilter P) P
-- Mathlib.Algebra.GroupWithZero.Divisibility
dvd_antisymm' : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [IsCancelMulZero α] {a b : α} [Subsingleton αˣ], a ∣ b → b ∣ a → b = a
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail.  -/
Std.DTreeMap.Internal.Impl.any : {α : Type u} → {β : α → Type v} → Std.DTreeMap.Internal.Impl α β → ((a : α) → β a → Bool) → Bool
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAt.eq : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice}
  {startPos endPos endPos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos →
    String.Slice.Pattern.Model.IsLongestMatchAt pat startPos endPos' → endPos = endPos'
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.δToCycles.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ : ℤ)
  (hn₁ : n₀ + 1 = n₁), X.δToCycles f₁ f₂ f₃ n₀ n₁ hn₁ = X.liftCycles f₁ f₂ n₁ (n₁ + 1) ⋯ (X.δ f₂ f₃ n₀ n₁ ⋯) ⋯
-- Aesop.Rule.Forward
/-- If a `ForwardRulePriority` contains a success probability, extract it.  -/
Aesop.ForwardRulePriority.successProbability? : Aesop.ForwardRulePriority → Option Aesop.Percent
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.trivial_addGrp_add : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.AddMonObj.add =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Mathlib.Order.CompleteLattice.Basic
sSup_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : SupSet α] [inst_1 : SupSet β] {s : Set α} {t : Set β},
  s.Nonempty → t.Nonempty → sSup (s ×ˢ t) = (sSup s, sSup t)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} (t t_1 : Std.DTreeMap α (fun x => β) cmp) (e_t : t = t_1)
  (a a_1 : α) (e_a : a = a_1) (h : a ∈ t), Std.DTreeMap.Const.get t a h = Std.DTreeMap.Const.get t_1 a_1 ⋯
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.EssImageSubcategory.associator_inv_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.Full] [inst_5 : F.Faithful]
  [inst_6 : CategoryTheory.Limits.PreservesFiniteProducts F] (X Y Z : F.EssImageSubcategory),
  (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv =
    CategoryTheory.ObjectProperty.homMk (CategoryTheory.MonoidalCategoryStruct.associator X.obj Y.obj Z.obj).inv
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.processUnassigned.congr_simp : ∀ (mvars mvars_1 : Array Lean.Expr) (e_mvars : mvars = mvars_1) (i i_1 : ℕ) (e_i : i = i_1) (v v_1 : Lean.Expr),
  v = v_1 →
    ∀ (h : i < mvars.size) (a a_1 : Lean.Meta.Grind.EMatch.Choice),
      a = a_1 →
        ∀ (a_2 a_3 : Lean.Meta.Grind.EMatch.Context),
          a_2 = a_3 →
            ∀ (a_4 a_5 : ST.Ref IO.RealWorld Lean.Meta.Grind.EMatch.SearchState),
              a_4 = a_5 →
                ∀ (a_6 a_7 : ST.Ref IO.RealWorld Lean.Meta.Grind.Goal),
                  a_6 = a_7 →
                    ∀ (a_8 a_9 : Lean.Meta.Grind.MethodsRef),
                      a_8 = a_9 →
                        ∀ (a_10 a_11 : Lean.Meta.Grind.Context),
                          a_10 = a_11 →
                            ∀ (a_12 a_13 : ST.Ref IO.RealWorld Lean.Meta.Grind.State),
                              a_12 = a_13 →
                                ∀ (a_14 a_15 : Lean.Meta.Sym.Context),
                                  a_14 = a_15 →
                                    ∀ (a_16 a_17 : ST.Ref IO.RealWorld Lean.Meta.Sym.State),
                                      a_16 = a_17 →
                                        ∀ (a_18 a_19 : Lean.Meta.Context),
                                          a_18 = a_19 →
                                            ∀ (a_20 a_21 : ST.Ref IO.RealWorld Lean.Meta.State),
                                              a_20 = a_21 →
                                                ∀ (a_22 a_23 : Lean.Core.Context),
                                                  a_22 = a_23 →
                                                    ∀ (a_24 a_25 : ST.Ref IO.RealWorld Lean.Core.State),
                                                      a_24 = a_25 →
                                                        ∀ (a_26 a_27 : Void IO.RealWorld),
                                                          a_26 = a_27 →
                                                            Lean.Meta.Grind.EMatch.processUnassigned✝ mvars i v h a a_2
                                                                a_4 a_6 a_8 a_10 a_12 a_14 a_16 a_18 a_20 a_22 a_24
                                                                a_26 =
                                                              Lean.Meta.Grind.EMatch.processUnassigned✝ mvars_1 i_1 v_1
                                                                ⋯ a_1 a_3 a_5 a_7 a_9 a_11 a_13 a_15 a_17 a_19 a_21 a_23
                                                                a_25 a_27
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.congr_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ m₃ : Std.HashSet α}, m₁.Equiv m₂ → (m₁.Equiv m₃ ↔ m₂.Equiv m₃)
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows_isoBot_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) {n : ℕ}
  (F : CategoryTheory.ComposableArrows C n) (hF : ∀ (i : Fin n), W (F.map (CategoryTheory.homOfLE ⋯))),
  (CategoryTheory.MorphismProperty.TransfiniteCompositionOfShape.ofComposableArrows W F hF).isoBot.inv =
    CategoryTheory.CategoryStruct.id (F.obj ⊥)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaMonObjIsoOfRepresentableBy_hom_app_hom_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (F : CategoryTheory.Functor Cᵒᵖ MonCat) (α : (F.comp (CategoryTheory.forget MonCat)).RepresentableBy X)
  (X_1 : Cᵒᵖ) (a : Opposite.unop X_1 ⟶ X),
  (MonCat.Hom.hom ((CategoryTheory.yonedaMonObjIsoOfRepresentableBy X F α).hom.app X_1)) a = α.homEquiv' a
-- Std.Sat.AIG.LawfulOperator
Std.Sat.AIG.LawfulOperator.decl_eq : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {β : Std.Sat.AIG α → Type}
  {f : (aig : Std.Sat.AIG α) → β aig → Std.Sat.AIG.Entrypoint α} [self : Std.Sat.AIG.LawfulOperator α β f]
  (aig : Std.Sat.AIG α) (input : β aig) (idx : ℕ) (h1 : idx < aig.decls.size) (h2 : idx < (f aig input).aig.decls.size),
  (f aig input).aig.decls[idx] = aig.decls[idx]
-- Mathlib.Data.Set.Image
Subtype.range_coe : ∀ {α : Type u_1} {s : Set α}, Set.range Subtype.val = s
-- Mathlib.Data.Fintype.EquivFin
Quot.finite : ∀ {α : Sort u_4} [Finite α] (r : α → α → Prop), Finite (Quot r)
-- Mathlib.Algebra.Group.Units.Defs
IsAddUnit.nsmul : ∀ {M : Type u_1} [inst : AddMonoid M] {a : M} (n : ℕ), IsAddUnit a → IsAddUnit (n • a)