mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.ExtrClosure
IsExtrOn.closure : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [inst_2 : Preorder Y]
  [OrderClosedTopology Y] {f : X → Y} {s : Set X} {a : X},
  IsExtrOn f s a → ContinuousOn f (closure s) → IsExtrOn f (closure s) a
-- Lean.Meta.Basic
Lean.Meta.withImplicitBinderInfos : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Array Lean.Expr → n α → n α
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.ULift
Std.IterM.step_uLift : ∀ {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u} [inst : Std.Iterator α m β]
  [inst_1 : Monad n] {it : Std.IterM m β} [inst_2 : MonadLiftT m (Std.Iterators.ULiftT n)],
  (it.uLift n).step = do
    let __do_lift ← (monadLift it.step).run
    match __do_lift.down.inflate with
      | ⟨Std.IterStep.yield it' out, h⟩ =>
        pure (Std.Shrink.deflate (Std.PlausibleIterStep.yield (it'.uLift n) { down := out } ⋯))
      | ⟨Std.IterStep.skip it', h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.skip (it'.uLift n) ⋯))
      | ⟨Std.IterStep.done, h⟩ => pure (Std.Shrink.deflate (Std.PlausibleIterStep.done ⋯))
-- Mathlib.NumberTheory.RamificationInertia.HilbertTheory
isDecompositionField_iff : ∀ (K : Type u_2) (L : Type u_3) {B : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : CommRing B] (P : Ideal B) (D : Type u_5) [inst_4 : Field D] [inst_5 : Algebra D L]
  [inst_6 : MulSemiringAction Gal(L/K) B],
  IsDecompositionField K L P D ↔ IsGaloisGroup (↥(MulAction.stabilizer Gal(L/K) P)) D L
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.oneEquiv_naturality : ∀ {R : Type u} [inst : CommRing R] {M : Type u_1} {N : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (f : M →ₗ[R] N),
  ↑(exteriorPower.oneEquiv R N) ∘ₗ exteriorPower.map 1 f = f ∘ₗ ↑(exteriorPower.oneEquiv R M)
-- Mathlib.Data.List.Duplicate
List.Duplicate.ne_nil : ∀ {α : Type u_1} {l : List α} {x : α}, List.Duplicate x l → l ≠ []
-- Mathlib.Topology.Algebra.InfiniteSum.Defs
HasProd.unique : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {L : SummationFilter β} {f : β → α}
  [T2Space α] [L.NeBot] {a₁ a₂ : α}, HasProd f a₁ L → HasProd f a₂ L → a₁ = a₂
-- Mathlib.CategoryTheory.Limits.Types.End
CategoryTheory.Limits.chosenCoend.desc_apply : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J (Type (max w u)))} {X : Type (max w u)}
  (f : (j : J) → (F.obj (Opposite.op j)).obj j ⟶ X)
  (hf :
    ∀ ⦃i j : J⦄ (g : i ⟶ j),
      CategoryTheory.CategoryStruct.comp ((F.map g.op).app i) (f i) =
        CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op j)).map g) (f j))
  (x : CategoryTheory.Limits.chosenCoend F),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.chosenCoend.desc f hf)) x =
    Quot.lift (fun j => (CategoryTheory.ConcreteCategory.hom (f j.fst)) j.snd) ⋯ x
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracketWithin_add_right : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {s : Set M} {x : M} {V W W₁ : (x : M) → TangentSpace I x}
  [inst_6 : IsManifold I 2 M] [CompleteSpace E],
  MDiffAt[s] (T% W) x →
    MDiffAt[s] (T% W₁) x →
      UniqueMDiffAt[s] x →
        VectorField.mlieBracketWithin I V (W + W₁) s x =
          VectorField.mlieBracketWithin I V W s x + VectorField.mlieBracketWithin I V W₁ s x
-- Mathlib.AlgebraicTopology.CechNerve
/-- A helper function used in defining the Čech conerve adjunction.  -/
CategoryTheory.CosimplicialObject.equivalenceRightToLeft : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 :
        ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
          CategoryTheory.Limits.HasWidePushout f.left (fun x => f.right) fun x => f.hom] →
      (F : CategoryTheory.Arrow C) →
        (X : CategoryTheory.CosimplicialObject.Augmented C) →
          (F ⟶ CategoryTheory.CosimplicialObject.Augmented.toArrow.obj X) → (F.augmentedCechConerve ⟶ X)
-- Mathlib.Topology.Algebra.InfiniteSum.Ring
summable_mul_right_iff : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : DivisionSemiring α] [inst_1 : TopologicalSpace α]
  [IsTopologicalSemiring α] {f : ι → α} {a : α}, a ≠ 0 → (Summable (fun i => f i * a) L ↔ Summable f L)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.comp_add : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B C : Rep.{w, u, v} k G} (f : A ⟶ B)
  (g₁ g₂ : B ⟶ C),
  CategoryTheory.CategoryStruct.comp f (g₁ + g₂) =
    CategoryTheory.CategoryStruct.comp f g₁ + CategoryTheory.CategoryStruct.comp f g₂
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.think_equiv : ∀ {α : Type u} (s : Stream'.WSeq α), s.think ~ʷ s
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.symm_adj : ∀ {ι : Sort u_1} {V : Type u} (G : SimpleGraph V) (f : ι → V), Std.Symm fun i j => G.Adj (f i) (f j)
-- Init.Data.Int.OfNat
Int.Nonneg.mod : ∀ (a b : ℤ), a ≥ 0 → a % b ≥ 0
-- Mathlib.Probability.Density
ProbabilityTheory.IndepFun.mul_hasPDF : ∀ {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [inst : Group G]
  {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G] {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant]
  {X Y : Ω → G} [MeasureTheory.SFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ]
  [MeasureTheory.IsFiniteMeasure ℙ], ProbabilityTheory.IndepFun X Y ℙ → MeasureTheory.HasPDF (X * Y) ℙ μ
-- Batteries.Tactic.PrintPrefix
/-- Include declarations whose types are propositions.  -/
Batteries.Tactic.PrintPrefixConfig.propositions : Batteries.Tactic.PrintPrefixConfig → Bool
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.checkDeprecatedCore : Lean.Name → Lean.Elab.TermElabM Unit
-- Std.Internal.Do.WP.Basic
/-- Soundness for `StateM`: if `wp prog P s` holds, then `P` holds of `(prog.run s)`.  -/
Std.Internal.Do.StateM.of_wp_run_eq : ∀ {α σ : Type u_1} {x : α × σ} {prog : StateM σ α} {s : σ},
  StateT.run prog s = x → ∀ (P : α × σ → Prop), Std.Internal.Do.wp prog (fun a s' => P (a, s')) epost⟨⟩ s → P x
-- Mathlib.Algebra.Homology.Opposite
HomologicalComplex.homologyOp_hom_naturality_assoc : ∀ {ι : Type u_1} {V : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} V] {c : ComplexShape ι}
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {K L : HomologicalComplex V c} (φ : K ⟶ L) (i : ι)
  [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] {Z : Vᵒᵖ} (h : Opposite.op (K.homology i) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap ((HomologicalComplex.opFunctor V c).map φ.op) i)
      (CategoryTheory.CategoryStruct.comp (K.homologyOp i).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp (L.homologyOp i).hom (HomologicalComplex.homologyMap φ i).op) h
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The distinguished triangle `(t.truncLE a).obj A ⟶ A ⟶ (t.truncGE b).obj A ⟶ ...`
as a functor `C ⥤ Triangle C` when `t` is a `t`-structure on a pretriangulated
category `C` and `a + 1 = b`.  -/
CategoryTheory.Triangulated.TStructure.triangleLEGE : {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] →
              CategoryTheory.Triangulated.TStructure C →
                (a b : ℤ) → a + 1 = b → CategoryTheory.Functor C (CategoryTheory.Pretriangulated.Triangle C)
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- Around the image of the base point, `(extChartAt I x).target` and `range I` coincide locally.  -/
extChartAt_target_eventuallyEq : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] {x : M},
  (extChartAt I x).target =ᶠ[nhds (↑(extChartAt I x) x)] Set.range ↑I
-- Init.Data.UInt.Basic
/-- Bitwise exclusive or for 64-bit unsigned integers. Usually accessed via the `^^^` operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of both input
integers are set.

This function is overridden at runtime with an efficient implementation.
 -/
UInt64.xor : UInt64 → UInt64 → UInt64
-- Std.Do.WP.SimpLemmas
Std.Do.WP.modifyGet_MonadStateOf : ∀ {m : Type u → Type v} {σ : Type u} {n : Type u → Type u_1} {α : Type u} {ps : Std.Do.PostShape}
  {Q : Std.Do.PostCond α ps} [inst : MonadStateOf σ m] [inst_1 : MonadLift m n] [inst_2 : Std.Do.WP n ps]
  (f : σ → α × σ),
  (Std.Do.wp (MonadStateOf.modifyGet f)).apply Q = (Std.Do.wp (MonadLift.monadLift (modifyGet f))).apply Q
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.prod_mono : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : StarRing A]
  [inst_3 : Module R A] [inst_4 : NonUnitalSemiring B] [inst_5 : StarRing B] [inst_6 : Module R B]
  {S T : NonUnitalStarSubalgebra R A} {S₁ T₁ : NonUnitalStarSubalgebra R B}, S ≤ T → S₁ ≤ T₁ → S.prod S₁ ≤ T.prod T₁
-- Mathlib.Data.Set.Function
/-- **Alias** of the reverse direction of `Set.InjOn.ne_iff`. -/
Set.InjOn.ne : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f : α → β} {x y : α}, Set.InjOn f s → x ∈ s → y ∈ s → x ≠ y → f x ≠ f y
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh.eq_1 : ∀ (x : ℝ), Real.artanh x = Real.log √((1 + x) / (1 - x))
-- Std.Data.String.ToInt
Nat.toInt?_repr : ∀ (n : ℕ), n.repr.toInt? = some ↑n
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
TateCohomology.exact₃ : ∀ {R G : Type u} [inst : CommRing R] [inst_1 : Group G] [inst_2 : Fintype G]
  {S : CategoryTheory.ShortComplex (Rep.{u, u, u} R G)} (hS : S.ShortExact) (n : ℤ),
  { X₁ := (tateCohomologyFunctor n).obj S.X₂, X₂ := (tateCohomologyFunctor n).obj S.X₃,
      X₃ := tateCohomology S.X₁ (n + 1), f := (tateCohomologyFunctor n).map S.g, g := TateCohomology.δ hS n,
      zero := ⋯ }.Exact
-- Mathlib.Data.NNReal.Defs
NNReal.eq_iff : ∀ {n m : NNReal}, n = m ↔ ↑n = ↑m
-- Lean.ToExpr
Lean.instToExprInt8.mkNat : ℕ → Lean.Expr
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.id_toFun : ∀ (A : Type u_2) [inst : Monoid A] [inst_1 : TopologicalSpace A] (x : A), (ContinuousMonoidHom.id A) x = x
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cocone.equivalenceOfReindexing_counitIso : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor J C}
  {G : CategoryTheory.Functor K C} (e : K ≌ J) (α : e.functor.comp F ≅ G),
  (CategoryTheory.Limits.Cocone.equivalenceOfReindexing e α).counitIso =
    (((CategoryTheory.Limits.Cocone.precompose α.hom).comp
              ((CategoryTheory.Limits.Cocone.whiskering e.inverse).comp
                (CategoryTheory.Limits.Cocone.precompose (e.invFunIdAssoc F).inv))).associator
          (CategoryTheory.Limits.Cocone.whiskering e.functor) (CategoryTheory.Limits.Cocone.precompose α.inv)).symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight
          ((CategoryTheory.Limits.Cocone.precompose α.hom).associator
            ((CategoryTheory.Limits.Cocone.whiskering e.inverse).comp
              (CategoryTheory.Limits.Cocone.precompose (e.invFunIdAssoc F).inv))
            (CategoryTheory.Limits.Cocone.whiskering e.functor))
          (CategoryTheory.Limits.Cocone.precompose α.inv) ≪≫
        CategoryTheory.Functor.isoWhiskerRight
            ((CategoryTheory.Limits.Cocone.precompose α.hom).isoWhiskerLeft
              (CategoryTheory.NatIso.ofComponents'
                (fun s => CategoryTheory.Limits.Cocone.extInv (CategoryTheory.Iso.refl s.pt) ⋯) ⋯))
            (CategoryTheory.Limits.Cocone.precompose α.inv) ≪≫
          CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Limits.Cocone.precompose α.hom).rightUnitor
              (CategoryTheory.Limits.Cocone.precompose α.inv) ≪≫
            CategoryTheory.NatIso.ofComponents'
              (fun s => CategoryTheory.Limits.Cocone.extInv (CategoryTheory.Iso.refl s.pt) ⋯) ⋯
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokens.mk.sizeOf_spec : ∀ (resultId? : Option String) (data : Array ℕ),
  sizeOf { resultId? := resultId?, data := data } = 1 + sizeOf resultId? + sizeOf data
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
/-- For a groupoid `G` which is `ClosedUnderRestriction`, being a local structomorphism is a local
invariant property.  -/
StructureGroupoid.isLocalStructomorphWithinAt_localInvariantProp : ∀ {H : Type u_1} [inst : TopologicalSpace H] (G : StructureGroupoid H) [ClosedUnderRestriction G],
  G.LocalInvariantProp G G.IsLocalStructomorphWithinAt
-- Mathlib.Topology.Compactness.Lindelof
eq_open_union_nat : ∀ {X : Type u} [inst : TopologicalSpace X] [HereditarilyLindelofSpace X] {ι : Type u_2} [Nonempty ι] (U : ι → Set X),
  (∀ (i : ι), IsOpen (U i)) → ∃ k, ⋃ n, U (k n) = ⋃ i, U i
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.liftOnAddUnits.eq_1 : ∀ {M : Type u_1} {α : Type u_4} [inst : AddMonoid M] {c : AddCon M} (u : AddUnits c.Quotient)
  (f : (x y : M) → c (x + y) 0 → c (y + x) 0 → α)
  (Hf :
    ∀ (x y : M) (hxy : c (x + y) 0) (hyx : c (y + x) 0) (x' y' : M) (hxy' : c (x' + y') 0) (hyx' : c (y' + x') 0),
      c x x' → c y y' → f x y hxy hyx = f x' y' hxy' hyx'),
  AddCon.liftOnAddUnits u f Hf = AddCon.hrecOn₂ (↑u) (↑(-u)) (fun x y hxy hyx => f x y ⋯ ⋯) ⋯ ⋯ ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.entryAtIdxD_eq_getD_map_getElem? : ∀ {α : Type u} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β},
  t.Balanced →
    ∀ {i : ℕ} {fallback : α × β},
      Std.DTreeMap.Internal.Impl.Const.entryAtIdxD t i fallback =
        (Option.map (fun x => (x.fst, x.snd)) t.toListModel[i]?).getD fallback
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Heterobasic version of `TensorProduct.curry`:

Given a linear map `M ⊗[R] N →[A] P`, compose it with the canonical
bilinear map `M →[A] N →[R] M ⊗[R] N` to form a bilinear map `M →[A] N →[R] P`.  -/
TensorProduct.AlgebraTensorModule.curry : {R : Type uR} →
  {A : Type uA} →
    {M : Type uM} →
      {N : Type uN} →
        {P : Type uP} →
          [inst : CommSemiring R] →
            [inst_1 : Semiring A] →
              [inst_2 : Algebra R A] →
                [inst_3 : AddCommMonoid M] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module A M] →
                      [inst_6 : IsScalarTower R A M] →
                        [inst_7 : AddCommMonoid N] →
                          [inst_8 : Module R N] →
                            [inst_9 : AddCommMonoid P] →
                              [inst_10 : Module R P] →
                                [inst_11 : Module A P] →
                                  [inst_12 : IsScalarTower R A P] → (TensorProduct R M N →ₗ[A] P) → M →ₗ[A] N →ₗ[R] P
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.π_comp_colimitOpIsoOpLimit_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] (j : J) {Z : Cᵒᵖ}
  (h : CategoryTheory.Limits.colimit F.op ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.π F j).op
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimitOpIsoOpLimit F).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F.op (Opposite.op j)) h
-- Mathlib.Algebra.Homology.HomologicalComplexLimits
HomologicalComplex.instPreservesLimitsOfShapeSingle : ∀ {C : Type u_1} {ι : Type u_2} {J : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_3} J] {c : ComplexShape ι}
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : DecidableEq ι] (i : ι), CategoryTheory.Limits.PreservesLimitsOfShape J (HomologicalComplex.single C c i)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.addHom_ext_iff : ∀ {R : Type u} [inst : Semiring R] {M : Type u_1} [inst_1 : AddZeroClass M] {f g : Polynomial R →+ M},
  f = g ↔ ∀ (n : ℕ) (a : R), f ((Polynomial.monomial n) a) = g ((Polynomial.monomial n) a)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar.congr_simp : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [inst_3 : CommRing R]
  [inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)],
  IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar n K R =
    IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar n K R
-- Mathlib.Topology.Algebra.Order.LiminfLimsup
le_limsup_add : ∀ {ι : Type u_1} {α : Type u_2} [inst : AddCommGroup α] [inst_1 : ConditionallyCompleteLinearOrder α] [DenselyOrdered α]
  [AddLeftMono α] {f : Filter ι} [f.NeBot] {u v : ι → α},
  autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f u) le_limsup_add._auto_1 →
    autoParam (Filter.IsCoboundedUnder (fun x1 x2 => x1 ≤ x2) f u) le_limsup_add._auto_3 →
      autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) f v) le_limsup_add._auto_5 →
        autoParam (Filter.IsBoundedUnder (fun x1 x2 => x1 ≥ x2) f v) le_limsup_add._auto_7 →
          Filter.limsup u f + Filter.liminf v f ≤ Filter.limsup (u + v) f
-- Init.Data.UInt.Lemmas
UInt8.le_zero_iff : ∀ {a : UInt8}, a ≤ 0 ↔ a = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp)
  (e_t : t = t_1) (h : t ≠ ∅), t.minKey h = t_1.minKey ⋯
-- Init.Conv
/-- `case'` is similar to the `case tag => tac` tactic, but does not ensure the goal
has been solved after applying `tac`, nor admits the goal if `tac` failed.
Recall that `case` closes the goal using `sorry` when `tac` fails, and
the tactic execution is not interrupted.
 -/
Lean.Parser.Tactic.Conv.case' : Lean.ParserDescr
-- Mathlib.Data.ENNReal.Real
ENNReal.toReal_add_le : ∀ {a b : ENNReal}, (a + b).toReal ≤ a.toReal + b.toReal
-- Lean.LocalContext
Lean.LocalContext.mk.sizeOf_spec : ∀ (fvarIdToDecl : Lean.PersistentHashMap Lean.FVarId Lean.LocalDecl)
  (decls : Lean.PersistentArray (Option Lean.LocalDecl)) (auxDeclToFullName : Lean.FVarIdMap Lean.Name),
  sizeOf { fvarIdToDecl := fvarIdToDecl, decls := decls, auxDeclToFullName := auxDeclToFullName } =
    1 + sizeOf fvarIdToDecl + sizeOf decls + sizeOf auxDeclToFullName
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.mk.inj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  {inst : CategoryTheory.Category.{v₁, u₁} A} {inst_1 : CategoryTheory.Category.{v₂, u₂} B}
  {inst_2 : CategoryTheory.Category.{v₃, u₃} C} {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {inst_3 : CategoryTheory.Category.{v₄, u₄} A'} {inst_4 : CategoryTheory.Category.{v₅, u₅} B'}
  {inst_5 : CategoryTheory.Category.{v₆, u₆} C'} {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} {left : ψ.left ⟶ ψ'.left} {right : ψ.right ⟶ ψ'.right}
  {base : ψ.base ⟶ ψ'.base}
  {left_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
          (CategoryTheory.Functor.whiskerRight left F') =
        CategoryTheory.CategoryStruct.comp (F.whiskerLeft base) (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
      CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence._autoParam}
  {right_coherence :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
          (CategoryTheory.Functor.whiskerRight right G') =
        CategoryTheory.CategoryStruct.comp (G.whiskerLeft base)
          (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom)
      CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence._autoParam}
  {left_1 : ψ.left ⟶ ψ'.left} {right_1 : ψ.right ⟶ ψ'.right} {base_1 : ψ.base ⟶ ψ'.base}
  {left_coherence_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso F ψ.left ψ.base F').hom
          (CategoryTheory.Functor.whiskerRight left_1 F') =
        CategoryTheory.CategoryStruct.comp (F.whiskerLeft base_1)
          (CategoryTheory.CatCommSq.iso F ψ'.left ψ'.base F').hom)
      CategoryTheory.Limits.CatCospanTransformMorphism.left_coherence._autoParam}
  {right_coherence_1 :
    autoParam
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.CatCommSq.iso G ψ.right ψ.base G').hom
          (CategoryTheory.Functor.whiskerRight right_1 G') =
        CategoryTheory.CategoryStruct.comp (G.whiskerLeft base_1)
          (CategoryTheory.CatCommSq.iso G ψ'.right ψ'.base G').hom)
      CategoryTheory.Limits.CatCospanTransformMorphism.right_coherence._autoParam},
  { left := left, right := right, base := base, left_coherence := left_coherence, right_coherence := right_coherence } =
      { left := left_1, right := right_1, base := base_1, left_coherence := left_coherence_1,
        right_coherence := right_coherence_1 } →
    left = left_1 ∧ right = right_1 ∧ base = base_1
-- Mathlib.RingTheory.MvPolynomial.Ideal
/-- `x` is in a monomial ideal generated by variables `X` iff every element of its support
has a component in `s`.  -/
MvPolynomial.mem_ideal_span_X_image : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {x : MvPolynomial σ R} {s : Set σ},
  x ∈ Ideal.span (MvPolynomial.X '' s) ↔ ∀ m ∈ x.support, ∃ i ∈ s, m i ≠ 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
CFC.le_one : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A},
  (∀ x ∈ spectrum R a, x ≤ 1) → autoParam (p a) CFC.le_one._auto_1 → a ≤ 1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rii.toArray_eq_match_roi : ∀ {α : Type u} {r : Std.Rii α} [inst : Std.PRange.Least? α] [inst_1 : Std.PRange.UpwardEnumerable α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_4 : Std.Rxi.IsAlwaysFinite α],
  r.toArray =
    match Std.PRange.least? with
    | none => #[]
    | some init => #[init] ++ init<...*.toArray
-- Mathlib.Algebra.Ring.Nat
Nat.instIsDomain : IsDomain ℕ
-- Mathlib.Order.Category.HeytAlg
HeytAlg.comp_apply : ∀ {X Y Z : HeytAlg} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.ground_nonempty : ∀ {α : Type u_1} (M : Matroid α) [M.Nonempty], M.E.Nonempty
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.toEnd_mul : ∀ {α : Type u_5} [inst : NonUnitalNonAssocSemiring α] (x y : CentroidHom α), (x * y).toEnd = x.toEnd * y.toEnd
-- Init.Data.Order.Classes
/-- If both `a` and `b` satisfy some property `P`, then so does `max a b`, because it is equal to
either `a` or `b`.
 -/
Std.MaxEqOr.elim : ∀ {α : Type u} [inst : Max α] [Std.MaxEqOr α] {P : α → Prop} {a b : α}, P a → P b → P (a ⊔ b)