mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.zero_mem : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (I : TwoSidedIdeal R), 0 ∈ I
-- Mathlib.Logic.Basic
dite_dite_comm : ∀ {α : Sort u_1} (P Q : Prop) [inst : Decidable P] {A : P → α} [inst_1 : Decidable Q] {B : Q → α} {C : ¬P → ¬Q → α},
  (P → ¬Q) → (if p : P then A p else if q : Q then B q else C p q) = if q : Q then B q else if p : P then A p else C p q
-- Lean.Elab.Do.Legacy
/-- If the given syntax is a `doLetExpr` or `doLetMetaExpr`, return an equivalent `doIf` that has an `else` but no `else if`s or `if let`s.   -/
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.expandDoLetExpr? : Lean.Syntax → List Lean.Syntax → Lean.MacroM (Option Lean.Syntax)
-- Mathlib.GroupTheory.NoncommPiCoprod
AddMonoidHom.addCommute_noncommPiCoprod : ∀ {M : Type u_1} [inst : AddMonoid M] {ι : Type u_2} [inst_1 : Fintype ι] {N : ι → Type u_3}
  [inst_2 : (i : ι) → AddMonoid (N i)] (ϕ : (i : ι) → N i →+ M)
  {hcomm : Pairwise fun i j => ∀ (x : N i) (y : N j), AddCommute ((ϕ i) x) ((ϕ j) y)} {m : M},
  (∀ (i : ι) (x : N i), AddCommute m ((ϕ i) x)) →
    ∀ (h : (i : ι) → N i), AddCommute m ((AddMonoidHom.noncommPiCoprod ϕ hcomm) h)
-- Lean.DocString.Types
Lean.Doc.Block.brecOn_8.go : {i : Type u} →
  {b : Type v} →
    {motive_1 : Lean.Doc.Block i b → Sort u_1} →
      {motive_2 : Array (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
        {motive_3 : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
          {motive_4 : Array (Lean.Doc.Block i b) → Sort u_1} →
            {motive_5 : List (Lean.Doc.ListItem (Lean.Doc.Block i b)) → Sort u_1} →
              {motive_6 : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) → Sort u_1} →
                {motive_7 : List (Lean.Doc.Block i b) → Sort u_1} →
                  {motive_8 : Lean.Doc.ListItem (Lean.Doc.Block i b) → Sort u_1} →
                    {motive_9 : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b) → Sort u_1} →
                      (t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) →
                        ((t : Lean.Doc.Block i b) → t.below → motive_1 t) →
                          ((t : Array (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                              Lean.Doc.Block.below_1 t → motive_2 t) →
                            ((t : Array (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                Lean.Doc.Block.below_2 t → motive_3 t) →
                              ((t : Array (Lean.Doc.Block i b)) → Lean.Doc.Block.below_3 t → motive_4 t) →
                                ((t : List (Lean.Doc.ListItem (Lean.Doc.Block i b))) →
                                    Lean.Doc.Block.below_4 t → motive_5 t) →
                                  ((t : List (Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b))) →
                                      Lean.Doc.Block.below_5 t → motive_6 t) →
                                    ((t : List (Lean.Doc.Block i b)) → Lean.Doc.Block.below_6 t → motive_7 t) →
                                      ((t : Lean.Doc.ListItem (Lean.Doc.Block i b)) →
                                          Lean.Doc.Block.below_7 t → motive_8 t) →
                                        ((t : Lean.Doc.DescItem (Lean.Doc.Inline i) (Lean.Doc.Block i b)) →
                                            Lean.Doc.Block.below_8 t → motive_9 t) →
                                          motive_9 t ×' Lean.Doc.Block.below_8 t
-- Mathlib.Algebra.BigOperators.Intervals
Finset.prod_range_diag_flip : ∀ {M : Type u_3} [inst : CommMonoid M] (n : ℕ) (f : ℕ → ℕ → M),
  ∏ m ∈ Finset.range n, ∏ k ∈ Finset.range (m + 1), f k (m - k) =
    ∏ m ∈ Finset.range n, ∏ k ∈ Finset.range (n - m), f m k
-- Mathlib.Data.EReal.Operations
_private.Mathlib.Data.EReal.Operations.0.EReal.exists_lt_add_right : ∀ {a b c : EReal}, c < a + b → ∃ b' < b, c < a + b'
-- Mathlib.CategoryTheory.Triangulated.TriangleShift
CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero_inv_app_hom₂ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] (X : CategoryTheory.Pretriangulated.Triangle C),
  ((CategoryTheory.Pretriangulated.Triangle.shiftFunctorZero C).inv.app X).hom₂ =
    (CategoryTheory.shiftFunctorZero C ℤ).inv.app X.obj₂
-- Mathlib.CategoryTheory.Adjunction.Unique
CategoryTheory.Adjunction.unit_leftAdjointUniq_hom_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F F' : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj1 : F ⊣ G) (adj2 : F' ⊣ G) {Z : CategoryTheory.Functor C C} (h : F'.comp G ⟶ Z),
  CategoryTheory.CategoryStruct.comp adj1.unit
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight (adj1.leftAdjointUniq adj2).hom G) h) =
    CategoryTheory.CategoryStruct.comp adj2.unit h
-- Mathlib.Algebra.Group.Fin.Basic
/-- Note this is more general than `Fin.addCommGroup` as it applies (vacuously) to `Fin 0` too.  -/
Fin.instInvolutiveNeg : (n : ℕ) → InvolutiveNeg (Fin n)
-- Mathlib.Order.Interval.Finset.Fin
Fin.Ioc_sub_one_eq_Icc : ∀ {n : ℕ} {a b : Fin n}, 0 < a → Finset.Ioc (a - 1) b = Finset.Icc a b
-- Mathlib.Order.Filter.Pointwise
Filter.pure_sub : ∀ {α : Type u_2} [inst : Sub α] {g : Filter α} {a : α}, pure a - g = Filter.map (fun x => a - x) g
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.mk''_obj : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  [inst_2 : CategoryTheory.Bicategory.Strict B] [inst_3 : CategoryTheory.Bicategory.Strict C]
  (S : CategoryTheory.StrictPseudofunctorPreCore B C) (a : B),
  (CategoryTheory.StrictPseudofunctor.mk'' S).obj a = S.obj a
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Mapping from types to its "structure id". We cache failures using `none`.
`typeIdOf[type]` is `some id`, then `id < structs.size`.  -/
Lean.Meta.Grind.Arith.Linear.State.typeIdOf : Lean.Meta.Grind.Arith.Linear.State → Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option ℕ)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_cons_of_true : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k}
  (h : (k == a) = true), Std.Internal.List.getValueCast? a (⟨k, v⟩ :: l) = some (cast ⋯ v)
-- Mathlib.Topology.UniformSpace.Uniformizable
completelyRegularSpace_iff_exists_uniformSpace : ∀ {X : Type u_1} [t : TopologicalSpace X], CompletelyRegularSpace X ↔ ∃ u, u.toTopologicalSpace = t
-- Mathlib.Data.PFunctor.Multivariate.M
_private.Mathlib.Data.PFunctor.Multivariate.M.0.TypeVec.append1.match_1.eq_2 : ∀ {n : ℕ} (motive : Fin2 (n + 1) → Sort u_1) (h_1 : (i : Fin2 n) → motive i.fs) (h_2 : Unit → motive Fin2.fz),
  (match Fin2.fz with
    | i.fs => h_1 i
    | Fin2.fz => h_2 ()) =
    h_2 ()
-- Mathlib.Tactic.Conv
/-- * `#simp => e` runs `simp` on the expression `e` and displays the resulting expression after
  simplification.
* `#simp only [lems] => e` runs `simp only [lems]` on `e`.
* The `=>` is optional, so `#simp e` and `#simp only [lems] e` have the same behavior.
  It is mostly useful for disambiguating the expression `e` from the lemmas.
 -/
Mathlib.Tactic.Conv.«command#simpOnly_=>__» : Lean.ParserDescr
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_eq_empty_of_le : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α], b ≤ a → Finset.Ioc a b = ∅
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instRightCancelMonoidOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : RightCancelMonoid Mᵐᵒᵖ], DomMulAct.instRightCancelMonoidOfMulOpposite = inst
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- `caseSplits` is `true` if cutsat is searching for model and already performed case splits.
This information is used to decide whether a conflict should immediately close the
current `grind` goal or not.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.caseSplits : Lean.Meta.Grind.Arith.Cutsat.State → Bool
-- Mathlib.AlgebraicGeometry.Sites.AffineEtale
AlgebraicGeometry.Scheme.AffineEtale.sheafEquiv_inverse : ∀ (S : AlgebraicGeometry.Scheme) (A : Type u') [inst : CategoryTheory.Category.{u, u'} A]
  [inst_1 : CategoryTheory.Limits.HasLimits A],
  (AlgebraicGeometry.Scheme.AffineEtale.sheafEquiv S A).inverse =
    (AlgebraicGeometry.Scheme.AffineEtale.Spec S).sheafPushforwardContinuous A
      (AlgebraicGeometry.Scheme.AffineEtale.topology S) S.smallEtaleTopology
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.FirstByte.threeMore : ByteArray.utf8DecodeChar?.FirstByte
-- Mathlib.Algebra.Lie.Subalgebra
/-- Given a Lie algebra `L` containing a Lie subalgebra `L' ⊆ L`, together with a Lie ring module
`M` of `L`, we may regard `M` as a Lie ring module of `L'` by restriction.  -/
LieSubalgebra.lieRingModule : {R : Type u} →
  {L : Type v} →
    [inst : CommRing R] →
      [inst_1 : LieRing L] →
        [inst_2 : LieAlgebra R L] →
          (L' : LieSubalgebra R L) →
            {M : Type w} → [inst_3 : AddCommGroup M] → [LieRingModule L M] → LieRingModule (↥L') M
-- Mathlib.Tactic.WithoutCDot
Lean.Elab.Term.withoutCDot.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.instFullToCompHausLike : ∀ {P P' : TopCat → Prop} (h : ∀ (X : CompHausLike P), P X.toTop → P' X.toTop), (CompHausLike.toCompHausLike h).Full
-- Mathlib.LinearAlgebra.Matrix.Stochastic
Matrix.rowStochastic.congr_simp : ∀ (R : Type u_3) (n : Type u_4) [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Semiring R]
  [inst_3 : PartialOrder R] [inst_4 : IsOrderedRing R], Matrix.rowStochastic R n = Matrix.rowStochastic R n
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {he : t.isEmpty = false} {km : α},
  t.min he = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- A family of morphisms `π a : X a ⟶ B` indexed by `α` is effective epimorphic
provided that the `π a` exhibit `B` as a colimit of the diagram of all "relations"
`R → X a₁`, `R ⟶ X a₂` for all `a₁ a₂ : α`.
 -/
CategoryTheory.EffectiveEpiFamily : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → {B : C} → {α : Type u_2} → (X : α → C) → ((a : α) → X a ⟶ B) → Prop
-- Mathlib.Topology.CantorBendixson
CantorBendixson.iteratedDerivedSet_mono : ∀ {X : Type u} [inst : TopologicalSpace X], Monotone fun s => CantorBendixson.iteratedDerivedSet s
-- Mathlib.Algebra.Lie.Basic
LieHom.coe_comp : ∀ {R : Type u} {L₁ : Type v} {L₂ : Type w} {L₃ : Type w₁} [inst : CommRing R] [inst_1 : LieRing L₁]
  [inst_2 : LieAlgebra R L₁] [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] [inst_5 : LieRing L₃]
  [inst_6 : LieAlgebra R L₃] (f : L₂ →ₗ⁅R⁆ L₃) (g : L₁ →ₗ⁅R⁆ L₂), ⇑(f.comp g) = ⇑f ∘ ⇑g
-- Mathlib.RingTheory.Valuation.Basic
/-- `comap` preserves equivalence.  -/
Valuation.IsEquiv.comap : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀} {S : Type u_7}
  [inst_3 : Ring S] (f : S →+* R), v₁.IsEquiv v₂ → (Valuation.comap f v₁).IsEquiv (Valuation.comap f v₂)
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.MutuallySingular.neg_right : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  {N : Type u_6} [inst_2 : AddCommGroup N] [inst_3 : TopologicalSpace N] [inst_4 : IsTopologicalAddGroup N]
  {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N},
  v.MutuallySingular w → v.MutuallySingular (-w)
-- Mathlib.Data.Finset.Sups
Finset.univ_infs_univ : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : SemilatticeInf α] [inst_2 : Fintype α],
  Finset.univ ⊼ Finset.univ = Finset.univ
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
IsSMulRegular.mem_nonZeroSMulDivisors : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {M : Type u_4} [inst_1 : Zero M] [inst_2 : MulActionWithZero M₀ M]
  {m₀ : M₀}, IsSMulRegular M m₀ → m₀ ∈ nonZeroSMulDivisors M₀ M
-- Init.Data.Vector.Extract
Vector.extract_sub_one : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i j : ℕ} (h : j < n),
  xs.extract i (j - 1) = Vector.cast ⋯ (xs.extract i j).pop
-- Lean.Util.LeanOptions
Lean.instReprLeanOptionValue : Repr Lean.LeanOptionValue
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.denseRange_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] {f : β → α},
  DenseRange f ↔ ∀ (x : α), ∀ r > 0, ∃ y, dist x (f y) < r
-- Mathlib.RingTheory.PowerBasis
PowerBasis.equivOfMinpoly_apply : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] {S' : Type u_7}
  [inst_3 : Ring S'] [inst_4 : Algebra A S'] (pb : PowerBasis A S) (pb' : PowerBasis A S')
  (h : minpoly A pb.gen = minpoly A pb'.gen) (a : S), (pb.equivOfMinpoly pb' h) a = (pb.lift pb'.gen ⋯) a
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_max : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {he : t.isEmpty = false}, t.get! (t.max he) = t.max he
-- Mathlib.Analysis.Normed.Group.Continuity
tendsto_iff_norm_neg_add_tendsto_zero : ∀ {α : Type u_1} {E : Type u_4} [inst : SeminormedAddGroup E] {f : α → E} {a : Filter α} {b : E},
  Filter.Tendsto f a (nhds b) ↔ Filter.Tendsto (fun e => ‖-f e + b‖) a (nhds 0)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mul_eq_right : ∀ {a b : Cardinal.{u_1}}, Cardinal.aleph0 ≤ b → a ≤ b → a ≠ 0 → a * b = b
-- Mathlib.Order.Hom.CompleteLattice
CompleteLatticeHom.coe_tosInfHom : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice α] [inst_1 : CompleteLattice β] (f : CompleteLatticeHom α β),
  ⇑f.tosInfHom = ⇑f
-- Mathlib.Data.Finset.Lattice.Union
Finset.inf'_biUnion : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] (f : β → α) [inst_1 : DecidableEq β]
  {s : Finset γ} (Hs : s.Nonempty) {t : γ → Finset β} (Ht : ∀ (b : γ), (t b).Nonempty),
  (s.biUnion t).inf' ⋯ f = s.inf' Hs fun b => (t b).inf' ⋯ f
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.add_mem_Ioc_iff_right : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a + b ∈ Set.Ioc c d ↔ b ∈ Set.Ioc (c - a) (d - a)
-- Init.Data.SInt.Lemmas
ISize.toNatClampNeg_ofIntLE : ∀ {n : ℤ} (h₁ : ISize.minValue.toInt ≤ n) (h₂ : n ≤ ISize.maxValue.toInt),
  (ISize.ofIntLE n h₁ h₂).toNatClampNeg = n.toNat
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.evalOp_obj_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] (A : Type u₁) [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasProducts A] (F : CategoryTheory.Functor Cᵒᵖ A)
  (X : (CategoryTheory.Limits.FormalCoproduct C)ᵒᵖ),
  ((CategoryTheory.Limits.FormalCoproduct.evalOp C A).obj F).obj X =
    ∏ᶜ fun i => F.obj (Opposite.op ((Opposite.unop X).obj i))
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.isPositive_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {T : ι → E →L[𝕜] E} (s : Finset ι), (∀ i ∈ s, (T i).IsPositive) → (∑ i ∈ s, T i).IsPositive
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_trans_aeeq_right : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b c : E} (ω : E → E →L[𝕜] F)
  (γab : Path a b) (γbc : Path b c),
  curveIntegralFun ω (γab.trans γbc) =ᵐ[MeasureTheory.volume.restrict (Set.uIoc (1 / 2) 1)] fun t =>
    2 • curveIntegralFun ω γbc (2 * t - 1)
-- Mathlib.Tactic.Simps.Basic
/-- Get the projections of a structure used by `@[simps]` applied to the appropriate arguments.
Returns a list of tuples
```
(corresponding right-hand-side, given projection name, projection Expression,
  future projection numbers, used by default, is prefix)
```
(where all fields except the first are packed in a `ProjectionData` structure)
one for each projection. The given projection name is the name for the projection used by the user
used to generate (and parse) projection names. For example, in the structure

  Example 1: ``getProjectionExprs env `(α × β) `(⟨x, y⟩)`` will give the output
  ```
    [(`(x), `fst, `(@Prod.fst.{u v} α β), [], true, false),
     (`(y), `snd, `(@Prod.snd.{u v} α β), [], true, false)]
  ```

  Example 2: ``getProjectionExprs env `(α ≃ α) `(⟨id, id, fun _ ↦ rfl, fun _ ↦ rfl⟩)``
  will give the output
  ```
    [(`(id), `apply, (Equiv.toFun), [], true, false),
     (`(id), `symm_apply, (fun e ↦ e.symm.toFun), [], true, false),
     ...,
     ...]
  ```
 -/
Simps.getProjectionExprs : Lean.Syntax → Lean.Expr → Lean.Expr → Simps.Config → Lean.MetaM (Array (Lean.Expr × Simps.ProjectionData))
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A set `A` is countably compact if every countably generated proper filter `f` with
`f ≤ 𝓟 A` has a cluster point in `A`.  -/
IsCountablyCompact : {E : Type u_2} → [TopologicalSpace E] → Set E → Prop
-- Mathlib.Topology.Compactness.Compact
IsCompact.elim_nhds_subcover_nhdsSet' : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X},
  IsCompact s →
    ∀ (U : (x : X) → x ∈ s → Set X), (∀ (x : X) (hx : x ∈ s), U x hx ∈ nhds x) → ∃ t, ⋃ x ∈ t, U ↑x ⋯ ∈ nhdsSet s
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_eq_of_contains : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [LawfulBEq α] [inst_3 : Inhabited α],
  m.WF → ∀ {k : α}, m.contains k = true → m.get! k = k
-- Mathlib.Topology.EMetricSpace.BoundedVariation
BoundedVariationOn.sub_le : ∀ {α : Type u_1} [inst : LinearOrder α] {f : α → ℝ} {s : Set α},
  BoundedVariationOn f s → ∀ {x y : α}, x ∈ s → y ∈ s → f x - f y ≤ (eVariationOn f s).toReal
-- Mathlib.Data.Finite.Prod
Equiv.finite_right : ∀ {α : Sort u_3} {β : Sort u_4} [Finite β], Finite (α ≃ β)
-- Mathlib.Topology.Order.Basic
lt_mem_nhds : ∀ {α : Type u} [ts : TopologicalSpace α] [inst : Preorder α] [OrderTopology α] {a b : α},
  a < b → ∀ᶠ (x : α) in nhds b, a < x
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.π_leftRightHomologyComparison'_ι_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData) {Z : C} (h : h₂.Q ⟶ Z),
  CategoryTheory.CategoryStruct.comp h₁.π
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.leftRightHomologyComparison' h₁ h₂)
        (CategoryTheory.CategoryStruct.comp h₂.ι h)) =
    CategoryTheory.CategoryStruct.comp h₁.i (CategoryTheory.CategoryStruct.comp h₂.p h)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.mk''.sizeOf_spec : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} [inst_10 : SizeOf R] [inst_11 : SizeOf G]
  [inst_12 : SizeOf V] [inst_13 : SizeOf W] (toContinuousLinearEquiv : V ≃L[R] W)
  (cont : autoParam (Continuous (↑↑toContinuousLinearEquiv).toFun) ContinuousLinearMap.cont._autoParam)
  (isIntertwining' :
    ∀ (g : G),
      { toLinearMap := ↑↑toContinuousLinearEquiv, cont := cont } ∘SL π₁ g =
        π₂ g ∘SL { toLinearMap := ↑↑toContinuousLinearEquiv, cont := cont }),
  sizeOf { toContinuousLinearEquiv := toContinuousLinearEquiv, cont := cont, isIntertwining' := isIntertwining' } =
    1 + sizeOf toContinuousLinearEquiv + sizeOf cont
-- Mathlib.Algebra.Order.Interval.Basic
Interval.one_mem_one : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : One α], 1 ∈ 1
-- Mathlib.MeasureTheory.Group.Arithmetic
Measurable.add_iff_right : ∀ {α : Type u_1} {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : MeasurableSpace α] [inst_2 : AddCommGroup G]
  [MeasurableAdd₂ G] [MeasurableNeg G] {f g : α → G}, Measurable f → (Measurable (f + g) ↔ Measurable g)
-- Mathlib.Logic.Equiv.Basic
Equiv.swap_comp_apply : ∀ {α : Sort u_1} [inst : DecidableEq α] {a b x : α} (π : Equiv.Perm α),
  (Equiv.trans π (Equiv.swap a b)) x = if π x = a then b else if π x = b then a else π x
-- Lean.Data.Json.Basic
Lean.Json.str.sizeOf_spec : ∀ (s : String), sizeOf (Lean.Json.str s) = 1 + sizeOf s
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.iSup_normal : ∀ {G : Type u_2} [inst : AddGroup G] {ι : Sort u_5} (H : ι → AddSubgroup G) [∀ (i : ι), (H i).Normal], (⨆ i, H i).Normal
-- Mathlib.CategoryTheory.Limits.IsConnected
/-- If `C` is connected, the cocone on `constPUnitFunctor` with cone point `PUnit` is a colimit
cocone.  -/
CategoryTheory.Limits.Types.isColimitPUnitCocone : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.IsConnected C] → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Types.pUnitCocone C)
-- Init.Data.SInt.Basic
/-- Bitwise exclusive or for 64-bit signed integers. Usually accessed via the `^^^` operator.

Each bit of the resulting integer is set if exactly one of the corresponding bits of the input
integers is set, according to the two's complement representation.

This function is overridden at runtime with an efficient implementation.
 -/
Int64.xor : Int64 → Int64 → Int64
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.image_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] {f : α → β}, f '' 0 = {f 0}
-- Init.Data.BitVec.Lemmas
BitVec.allOnes_eq_zero_iff : ∀ {w : ℕ}, BitVec.allOnes w = 0#w ↔ w = 0
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.range_subtype : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G), H.subtype.range = H
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.sub_mul_div_left : ∀ {R : Type u} [inst : EuclideanDomain R] (x y z : R), y ≠ 0 → y ∣ x → (x - y * z) / y = x / y - z
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.mapNatBool.eq_1 : ∀ (α : Type u_1) [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α] (x : α) (n : ℕ),
  MeasurableSpace.mapNatBool α x n = decide (x ∈ MeasurableSpace.natGeneratingSequence α n)
-- Mathlib.Topology.Category.CompHaus.Frm
/-- The forgetful functor from `TopCatᵒᵖ` to `Frm`.  -/
topCatOpToFrm : CategoryTheory.Functor TopCatᵒᵖ Frm
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.HasNoetherianRange.hasFiniteRange : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} [inst : Semiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] {u : V →ₗ[K] V₂}, u.HasNoetherianRange → u.HasFiniteRange
-- Mathlib.Control.ULift
ULift.pure.eq_1 : ∀ {α : Type u}, ULift.pure = ULift.up
-- Mathlib.Analysis.Calculus.Gradient.Basic
gradient_fun_const' : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] (c : 𝕜), (gradient fun x => c) = fun x => 0
-- Init.Data.BitVec.Lemmas
BitVec.and_setWidth_allOnes : ∀ (w' w : ℕ) (b : BitVec (w' + w)), b &&& BitVec.setWidth (w' + w) (BitVec.allOnes w) = 0#w' ++ BitVec.setWidth w b
-- Mathlib.Data.Int.Cast.Lemmas
zmultiplesHom_symm_apply : ∀ (β : Type u_4) [inst : AddGroup β] (f : ℤ →+ β), (zmultiplesHom β).symm f = f 1
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_bot : ∀ {R : Type u_2} [inst : NonAssocSemiring R], ⊥.unop = ⊥
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Functor.copyObj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (obj : C → D) (e : (X : C) → F.obj X ≅ obj X) (a : C),
  (F.copyObj obj e).obj a = obj a