mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.homMk₄_app_two : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 4}
  (app₀ : f.obj' 0 _proof_361✝ ⟶ g.obj' 0 _proof_361✝) (app₁ : f.obj' 1 _proof_362✝ ⟶ g.obj' 1 _proof_362✝)
  (app₂ : f.obj' 2 _proof_363✝ ⟶ g.obj' 2 _proof_363✝) (app₃ : f.obj' 3 _proof_364✝ ⟶ g.obj' 3 _proof_364✝)
  (app₄ : f.obj' 4 _proof_365✝ ⟶ g.obj' 4 _proof_365✝)
  (w₀ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝)
          app₁ =
        CategoryTheory.CategoryStruct.comp app₀
          (g.map' 0 1 CategoryTheory.ComposableArrows.homMk₁._proof_4 _proof_362✝))
      _auto_387✝)
  (w₁ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 1 2 _proof_246✝ _proof_363✝) app₂ =
        CategoryTheory.CategoryStruct.comp app₁ (g.map' 1 2 _proof_246✝ _proof_363✝))
      _auto_389✝)
  (w₂ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 2 3 _proof_299✝ _proof_364✝) app₃ =
        CategoryTheory.CategoryStruct.comp app₂ (g.map' 2 3 _proof_299✝ _proof_364✝))
      _auto_391✝)
  (w₃ :
    autoParam
      (CategoryTheory.CategoryStruct.comp (f.map' 3 4 _proof_364✝ _proof_365✝) app₄ =
        CategoryTheory.CategoryStruct.comp app₃ (g.map' 3 4 _proof_364✝ _proof_365✝))
      _auto_393✝),
  (CategoryTheory.ComposableArrows.homMk₄ app₀ app₁ app₂ app₃ app₄ w₀ w₁ w₂ w₃).app
      ⟨2, CategoryTheory.ComposableArrows.homMk₄._proof_3⟩ =
    app₂
-- Mathlib.AlgebraicTopology.ModelCategory.Over
HomotopicalAlgebra.instIsStableUnderRetractsOverFibrations : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (S : C) [inst_1 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.fibrations C).IsStableUnderRetracts],
  (HomotopicalAlgebra.fibrations (CategoryTheory.Over S)).IsStableUnderRetracts
-- Lean.Elab.Syntax
/-- Add macro scope to `name` if it does not already have them, and `attrKind` is `local`.
 -/
_private.Lean.Elab.Syntax.0.Lean.Elab.Command.addMacroScopeIfLocal : {m : Type → Type} → [Lean.MonadQuotation m] → [Monad m] → Lean.Name → Lean.Syntax → m Lean.Name
-- Std.Async.System
Std.Async.System.instInhabitedGroupInfo.default : Std.Async.System.GroupInfo
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.algHomOfDvd.eq_1 : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (f g : Polynomial S)
  (hgf : g ∣ f), AdjoinRoot.algHomOfDvd R f g hgf = AdjoinRoot.mapAlgHom (AlgHom.id R S) f g ⋯
-- Mathlib.SetTheory.Ordinal.Enum
_private.Mathlib.SetTheory.Ordinal.Enum.0.Ordinal.enumOrd.eq_1 : ∀ (s : Set Ordinal.{u}) (o : Ordinal.{u}), Ordinal.enumOrd s o = sInf (s ∩ {b | ∀ c < o, Ordinal.enumOrd s c < b})
-- Std.Data.Internal.List.Associative
Std.Internal.List.replaceEntry_append_of_containsKey_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l l' : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k l = true →
    Std.Internal.List.replaceEntry k v (l ++ l') = Std.Internal.List.replaceEntry k v l ++ l'
-- Mathlib.Topology.ClusterPt
/-- `x` is an accumulation point of a set `C` iff every neighborhood
of `x` contains a point of `C` other than `x`.  -/
accPt_iff_nhds : ∀ {X : Type u} [inst : TopologicalSpace X] {x : X} {C : Set X},
  AccPt x (Filter.principal C) ↔ ∀ U ∈ nhds x, ∃ y ∈ U ∩ C, y ≠ x
-- Mathlib.Order.Copy
/-- A function to create a provable equal copy of a generalised co-Heyting algebra
with possibly different definitional equalities.  -/
GeneralizedCoheytingAlgebra.copy : {α : Type u} →
  (c : GeneralizedCoheytingAlgebra α) →
    (le : α → α → Prop) →
      le = LE.le →
        (bot : α) →
          bot = ⊥ →
            (sup : α → α → α) →
              sup = max →
                (inf : α → α → α) →
                  inf = min → (sdiff : α → α → α) → sdiff = SDiff.sdiff → GeneralizedCoheytingAlgebra α
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- The projection on the `i`-th coordinate of `EuclideanSpace 𝕜 ι`, as a continuous linear map.  -/
EuclideanSpace.proj : {ι : Type u_1} → {𝕜 : Type u_3} → [inst : RCLike 𝕜] → ι → StrongDual 𝕜 (EuclideanSpace 𝕜 ι)
-- Init.Data.Int.Gcd
Int.gcd_add_left_right_of_dvd : ∀ {n k : ℤ} (m : ℤ), n ∣ k → n.gcd (k + m) = n.gcd m
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.biproduct.isoCoproduct_inv : ∀ {J : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {f : J → C} [inst_2 : CategoryTheory.Limits.HasBiproduct f],
  (CategoryTheory.Limits.biproduct.isoCoproduct f).inv =
    CategoryTheory.Limits.Sigma.desc (CategoryTheory.Limits.biproduct.ι f)
-- Mathlib.Algebra.Order.Monoid.Canonical.Defs
CanonicallyOrderedMul.le_self_mul : ∀ {α : Type u_1} {inst : Mul α} {inst_1 : LE α} [self : CanonicallyOrderedMul α] (a b : α), a ≤ a * b
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.instLaxBraidedMonMapAddMon.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : CategoryTheory.SymmetricCategory C]
  [inst_5 : CategoryTheory.SymmetricCategory D] [inst_6 : F.LaxBraided],
  CategoryTheory.Functor.instLaxBraidedMonMapAddMon = { toLaxMonoidal := F.instLaxMonoidalMonMapAddMon, braided := ⋯ }
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- If two finite measures give the same mass to the whole space and coincide on a π-system made
of measurable sets, then they coincide on all sets in the σ-algebra generated by the π-system.  -/
MeasureTheory.ext_on_measurableSpace_of_generate_finite : ∀ {α : Type u_5} (m₀ : MeasurableSpace α) {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  (C : Set (Set α)),
  (∀ s ∈ C, μ s = ν s) →
    ∀ {m : MeasurableSpace α},
      m ≤ m₀ →
        m = MeasurableSpace.generateFrom C →
          IsPiSystem C → μ Set.univ = ν Set.univ → ∀ {s : Set α}, MeasurableSet s → μ s = ν s
-- Mathlib.Control.Traversable.Instances
Option.mapM.eq_2 : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Applicative m] (f : α → m β) (val : α),
  Option.mapM f (some val) = some <$> f val
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_trim_simpleFunc : ∀ {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] [CompleteSpace F] {β : Type u_6}
  {m m0 : MeasurableSpace β} {μ : MeasureTheory.Measure β} (hm : m ≤ m0) (f : MeasureTheory.SimpleFunc β F),
  MeasureTheory.Integrable (⇑f) μ → ∫ (x : β), f x ∂μ = ∫ (x : β), f x ∂μ.trim hm
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.deterministic_apply' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α → β} (hf : Measurable f)
  (a : α) {s : Set β},
  MeasurableSet s → ((ProbabilityTheory.Kernel.deterministic f hf) a) s = s.indicator (fun x => 1) (f a)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_diff_le_size_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  (m₁ \ m₂).size ≤ m₁.size
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Fintype J] (f : J → C) (X : C),
  (CategoryTheory.rightDistributor f X).hom =
    ∑ j,
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X)
        (CategoryTheory.Limits.biproduct.ι (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j)
-- Lean.Meta.InferType
/-- Converts a `LBool` into an `ArrowPropResult`.  -/
_private.Lean.Meta.InferType.0.Lean.Meta.toArrowPropResult : Lean.LBool → Lean.Meta.ArrowPropResult✝
-- Mathlib.Algebra.BigOperators.Group.Multiset.Basic
Multiset.sum_int_mod : ∀ (s : Multiset ℤ) (n : ℤ), s.sum % n = (Multiset.map (fun x => x % n) s).sum % n
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupSeminorm.instIsAddApplyReal : ∀ {E : Type u_3} [inst : Group E], IsAddApply (GroupSeminorm E) E ℝ
-- Mathlib.Data.Seq.Computation
Computation.Equiv.equivalence : ∀ {α : Type u}, Equivalence Computation.Equiv
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.instFiniteObjOppositeSimplexCategory : ∀ (n : SimplexCategory) (d : SimplexCategoryᵒᵖ), Finite ((SSet.stdSimplex.obj n).obj d)
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.CommShift.ofIso_commShiftIso_inv_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F G : CategoryTheory.Functor C D} (e : F ≅ G) (A : Type u_4)
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F.CommShift A] (a : A) (X : C),
  (CategoryTheory.Functor.commShiftIso G a).inv.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (e.inv.app X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app X)
        (e.hom.app ((CategoryTheory.shiftFunctor C a).obj X)))
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- The additive homomorphism underlying a `LocalizationMap` of `AddCommMonoid`s.  -/
AddSubmonoid.LocalizationMap.toAddHom : {M : Type u_1} →
  [inst : AddCommMonoid M] →
    {S : AddSubmonoid M} → {N : Type u_2} → [inst_1 : AddCommMonoid N] → S.LocalizationMap N → M →ₙ+ N
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
/-- When `K` is a cochain complex indexed by `ℤ` and `i < n`, this is
the isomorphism `(K.truncLE n).X i ≅ K.X i`.  -/
CochainComplex.truncLEXIso : {C : Type u_2} →
  [inst : CategoryTheory.Category.{u_3, u_2} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        (K : CochainComplex C ℤ) →
          [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] →
            (n i : ℤ) → autoParam (i < n) CochainComplex.truncLEXIso._auto_1 → ((K.truncLE n).X i ≅ K.X i)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.max_prod_le : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : LinearOrder M] [IsOrderedMonoid M] {f g : ι → M}
  {s : Finset ι}, max (s.prod f) (s.prod g) ≤ ∏ i ∈ s, max (f i) (g i)
-- Mathlib.Algebra.Order.Sub.Defs
add_tsub_cancel_right : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α]
  [AddLeftReflectLE α] (a b : α), a + b - b = a
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Discrimination tree key.  -/
Lean.Meta.RefinedDiscrTree.Key : Type
-- Mathlib.ModelTheory.Encoding
/-- An encoding of bounded formulas as lists.  -/
FirstOrder.Language.BoundedFormula.encoding : {L : FirstOrder.Language} →
  {α : Type u'} →
    Computability.Encoding ((n : ℕ) × L.BoundedFormula α n) ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)
-- Mathlib.GroupTheory.Nilpotent
Subgroup.upperCentralSeries_nilpotencyClass : ∀ {G : Type u_1} [inst : Group G] [hG : Group.IsNilpotent G],
  Subgroup.upperCentralSeries G (Group.nilpotencyClass G) = ⊤
-- Mathlib.Data.Multiset.AddSub
Multiset.card_erase_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, a ∈ s → (s.erase a).card = s.card.pred
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
SheafOfModules.GeneratingSections.mk.sizeOf_spec : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} [inst_1 : CategoryTheory.HasWeakSheafify J AddCommGrpCat]
  [inst_2 : J.WEqualsLocallyBijective AddCommGrpCat] {M : SheafOfModules R} [inst_3 : SizeOf C] (I : Type u)
  (s : I → M.sections)
  (epi : autoParam (CategoryTheory.Epi (M.freeHomEquiv.symm s)) SheafOfModules.GeneratingSections.epi._autoParam),
  sizeOf { I := I, s := s, epi := epi } = 1 + sizeOf I + sizeOf epi
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- **Alias** of `Right.pos_add_of_right`. -/
add_pos_of_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [IsBotZeroClass α] [AddRightMono α] {b : α},
  0 < b → ∀ (a : α), 0 < a + b
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncLTLTIsoLT_inv_hom_id_app_eTruncLT_obj_assoc : ∀ {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) [inst_6 : CategoryTheory.IsTriangulated C] (a b : EInt) (hab : b ≤ a)
  (X : C) {Z : C} (h : (t.eTruncLT.obj b).obj ((t.eTruncLT.obj a).obj X) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((t.eTruncLTLTIsoLT a b hab).inv.app ((t.eTruncLT.obj a).obj X))
      (CategoryTheory.CategoryStruct.comp ((t.eTruncLT.obj b).map ((t.eTruncLT.obj a).map ((t.eTruncLTι a).app X))) h) =
    h
-- Mathlib.GroupTheory.Generators
Group.Generators.mk.injEq : ∀ {G : Type u_5} [inst : Group G] {ι : Type u_6} (val : ι → G) (closure_eq_top : Subgroup.closure (Set.range val) = ⊤)
  (val_1 : ι → G) (closure_eq_top_1 : Subgroup.closure (Set.range val_1) = ⊤),
  ({ val := val, closure_eq_top := closure_eq_top } = { val := val_1, closure_eq_top := closure_eq_top_1 }) =
    (val = val_1)
-- Mathlib.Order.BooleanAlgebra.Set
Set.sdiff_self_inter : ∀ {α : Type u_1} {s t : Set α}, s \ (s ∩ t) = s \ t
-- Mathlib.Topology.Connected.Basic
connectedComponentIn_eq_empty : ∀ {α : Type u} [inst : TopologicalSpace α] {F : Set α} {x : α}, x ∉ F → connectedComponentIn F x = ∅
-- Mathlib.Analysis.Fourier.Notation
FourierInvModule.mk.injEq : ∀ {R : Type u_5} {E : Type u_6} {F : outParam (Type u_7)} [inst : Add E] [inst_1 : Add F] [inst_2 : SMul R E]
  [inst_3 : SMul R F] (toFourierTransformInv : FourierTransformInv E F)
  (fourierInv_add :
    ∀ (f g : E),
      FourierTransformInv.fourierInv (f + g) = FourierTransformInv.fourierInv f + FourierTransformInv.fourierInv g)
  (fourierInv_smul : ∀ (r : R) (f : E), FourierTransformInv.fourierInv (r • f) = r • FourierTransformInv.fourierInv f)
  (toFourierTransformInv_1 : FourierTransformInv E F)
  (fourierInv_add_1 :
    ∀ (f g : E),
      FourierTransformInv.fourierInv (f + g) = FourierTransformInv.fourierInv f + FourierTransformInv.fourierInv g)
  (fourierInv_smul_1 :
    ∀ (r : R) (f : E), FourierTransformInv.fourierInv (r • f) = r • FourierTransformInv.fourierInv f),
  ({ toFourierTransformInv := toFourierTransformInv, fourierInv_add := fourierInv_add,
        fourierInv_smul := fourierInv_smul } =
      { toFourierTransformInv := toFourierTransformInv_1, fourierInv_add := fourierInv_add_1,
        fourierInv_smul := fourierInv_smul_1 }) =
    (toFourierTransformInv = toFourierTransformInv_1)
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Prequotient.of.sizeOf_spec : ∀ {J : Type v} [inst : CategoryTheory.Category.{u, v} J] {F : CategoryTheory.Functor J MonCat} [inst_1 : SizeOf J]
  (j : J) (x : ↑(F.obj j)), sizeOf (MonCat.Colimits.Prequotient.of j x) = 1 + sizeOf j + sizeOf x
-- LeanSearchClient.Syntax
LeanSearchClient.SearchResult.mk : String → Option String → Option String → Option String → Option String → LeanSearchClient.SearchResult
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.mulHead_prod : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j : ι} (w : Monoid.CoprodI.NeWord M i j)
  (x : M i) (hnotone : x * w.head ≠ 1), (w.mulHead x hnotone).prod = Monoid.CoprodI.of x * w.prod
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.end_.lift_π_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasEnd F] {X : C}
  (f : (j : J) → X ⟶ (F.obj (Opposite.op j)).obj j)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp (f i) ((F.obj (Opposite.op i)).map g) =
        CategoryTheory.CategoryStruct.comp (f j) ((F.map g.op).app j))
  (j : J) {Z : C} (h : (F.obj (Opposite.op j)).obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.lift f hf)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.end_.π F j) h) =
    CategoryTheory.CategoryStruct.comp (f j) h
-- Lean.Elab.MutualInductive
/-- Returns true if the syntax participates in the mutual inductive elaborator.
These do not need to be commands. In fact `inductive` and `structure` are registered
on the `Lean.Parser.Command.inductive` and `Lean.Parser.Command.structure` syntaxes.
 -/
Lean.Elab.Command.isInductiveCommand : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Syntax → m Bool
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.isEmpty.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Batteries.AssocList α β → Sort u_3)
  (h_1 : Unit → motive Batteries.AssocList.nil) (h_2 : (x : Batteries.AssocList α β) → motive x),
  (match Batteries.AssocList.nil with
    | Batteries.AssocList.nil => h_1 ()
    | x => h_2 x) =
    h_1 ()
-- Init.Data.SInt.Lemmas
Int8.toInt_lt : ∀ (x : Int8), x.toInt < 2 ^ 7
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.inf_mem : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} {a b : α}, a ∈ L → b ∈ L → a ⊓ b ∈ L
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_eq_bot_iff : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {p : Submodule R M} [inst_6 : RingHomSurjective σ₁₂] {σ₂₁ : R₂ →+* R} [inst_7 : RingHomInvPair σ₁₂ σ₂₁]
  [inst_8 : RingHomInvPair σ₂₁ σ₁₂] {e : M ≃ₛₗ[σ₁₂] M₂}, Submodule.map (↑e) p = ⊥ ↔ p = ⊥
-- Batteries.Tactic.Lint.Frontend
/-- Get the list of all declarations in the environment.  -/
Batteries.Tactic.Lint.getAllDecls : Lean.CoreM (Array Lean.Name)
-- Mathlib.AlgebraicGeometry.Noetherian
/-- Let `R` be a ring, and `f i` a finite collection of elements of `R` generating the unit ideal.
If the localization of `R` at each `f i` is Noetherian, so is `R`.

We follow the proof given in [Har77], Proposition II.3.2  -/
AlgebraicGeometry.isNoetherianRing_of_away : ∀ {R : Type u} [inst : CommRing R] (S : Finset R),
  Ideal.span ↑S = ⊤ → (∀ (s : ↥S), IsNoetherianRing (Localization.Away ↑s)) → IsNoetherianRing R
-- Std.Time.Time.Unit.Hour
/-- Converts an `Ordinal` into a relative hour in the range of 1 to 12.
 -/
Std.Time.Hour.Ordinal.toRelative : Std.Time.Hour.Ordinal → Std.Time.Internal.Bounded.LE 1 12
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.Hom.left.sizeOf_spec : ∀ {ι : Type v} [inst : SizeOf ι] (i j : ι), sizeOf (CategoryTheory.Pairwise.Hom.left i j) = 1 + sizeOf i + sizeOf j
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.associator_eqToHom_hom_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y z t : B} (e₁ : x = y) (e₂ : y = z) (e₃ : z = t) {Z : x ⟶ t}
  (h :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom e₁)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom e₂) (CategoryTheory.eqToHom e₃)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator (CategoryTheory.eqToHom e₁) (CategoryTheory.eqToHom e₂)
          (CategoryTheory.eqToHom e₃)).hom
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.eqToHomTransIso e₁ e₂).inv
        (CategoryTheory.eqToHom e₃))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.eqToHomTransIso ⋯ e₃).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.eqToHomTransIso e₁ ⋯).hom
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.eqToHom e₁)
              (CategoryTheory.Bicategory.eqToHomTransIso e₂ e₃).hom)
            h)))
-- Mathlib.RingTheory.Ideal.Quotient.Operations
DoubleQuot.quotQuotEquivComm_symm : ∀ {R : Type u} [inst : CommRing R] (I J : Ideal R),
  (DoubleQuot.quotQuotEquivComm I J).symm = DoubleQuot.quotQuotEquivComm J I
-- Mathlib.Logic.Function.FiberPartition
/-- The indexing set of the partition.  -/
Function.Fiber : {Y : Type u_2} → {Z : Type u_3} → (Y → Z) → Type u_2
-- Mathlib.Analysis.Normed.Module.Bases
SchauderBasis.RankOneDecomposition.mk : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {X : Type u_2} →
      [inst_1 : NormedAddCommGroup X] →
        [inst_2 : NormedSpace 𝕜 X] →
          (P : ℕ → X →L[𝕜] X) →
            (e : ℕ → X) →
              P 0 = 0 →
                (∀ (n : ℕ), Module.finrank 𝕜 ↥(↑(P n)).range = n) →
                  (∀ (n m : ℕ) (x : X), (P n) ((P m) x) = (P (min n m)) x) →
                    (∀ (x : X), Filter.Tendsto (fun n => (P n) x) Filter.atTop (nhds x)) →
                      (∀ (n : ℕ), e n ∈ (↑(SchauderBasis.succSub P n)).range) →
                        (∀ (n : ℕ), e n ≠ 0) → SchauderBasis.RankOneDecomposition 𝕜 X
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableSpace.comap_not : ∀ {α : Type u_1} (p : α → Prop),
  MeasurableSpace.comap (fun a => ¬p a) inferInstance = MeasurableSpace.comap p inferInstance
-- Mathlib.Order.Directed
/-- A family of elements of `α` is directed (with respect to a relation `≼` on `α`)
if there is a member of the family `≼`-above any pair in the family.  -/
Directed : {α : Type u_1} → {ι : Sort u_3} → (α → α → Prop) → (ι → α) → Prop
-- Mathlib.Order.SupClosed
SupClosed.directedOn : ∀ {α : Type u_3} [inst : SemilatticeSup α] {s : Set α}, SupClosed s → DirectedOn (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.Data.List.Cycle
Cycle.nil_toMultiset : ∀ {α : Type u_1}, Cycle.nil.toMultiset = 0
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Iic_union_Ioi_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, a ≤ b → Set.Iic b ∪ Set.Ioi a = Set.univ
-- Mathlib.GroupTheory.Frattini
frattini.eq_1 : ∀ (G : Type u_1) [inst : Group G], frattini G = Order.radical (Subgroup G)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.foldM_iterM_id : ∀ {n : Type (max u_1 u_2) → Type u_3} {ps : Std.Do.PostShape} [inst : Monad n] [inst_1 : Std.Do.WPMonad n ps]
  {α β γ : Type (max u_1 u_2)} [inst_2 : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {it : Std.IterM Id β} {init : γ} {f : γ → β → n γ}
  (inv : Std.Do.Invariant it.toList.run γ ps),
  (∀ (pref : List β) (cur : β) (suff : List β) (h : it.toList.run = pref ++ cur :: suff) (b : γ),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f b cur ⦃(fun b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b'), inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := it.toList.run, property := ⋯ }, init)⦄
      Std.IterM.foldM f init
        it ⦃(fun b => inv.1 ({ «prefix» := it.toList.run, suffix := [], property := ⋯ }, b), inv.2)⦄