mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.erase_def : ∀ {ι : Type u} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] (i : ι) (f : Π₀ (i : ι), β i),
  DFinsupp.erase i f = DFinsupp.mk (f.support.erase i) fun j => f ↑j
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertMax.eq_2 : ∀ {α : Type u} {β : α → Type v} (k : α) (v : β k) (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hr_1 : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
  Std.DTreeMap.Internal.Impl.insertMax k v (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr_1 =
    match Std.DTreeMap.Internal.Impl.insertMax k v r' ⋯ with
    | { impl := r'', balanced_impl := hr''₁, size_impl := hr''₂ } =>
      { impl := Std.DTreeMap.Internal.Impl.balanceR k' v' l' r'' ⋯ ⋯ ⋯, balanced_impl := ⋯, size_impl := ⋯ }
-- Mathlib.Order.Filter.IsBounded
Monotone.frequently_ge_map_of_frequently_ge : ∀ {R : Type u_5} {S : Type u_6} {F : Filter R} [inst : LinearOrder R] [inst_1 : LinearOrder S] {f : R → S},
  Monotone f → ∀ {l : R}, (∃ᶠ (x : R) in F, l ≤ x) → ∃ᶠ (x' : S) in Filter.map f F, f l ≤ x'
-- Mathlib.Topology.GDelta.Basic
IsGδ.iInter_of_isOpen : ∀ {X : Type u_1} {ι' : Sort u_4} [inst : TopologicalSpace X] [Countable ι'] {f : ι' → Set X},
  (∀ (i : ι'), IsOpen (f i)) → IsGδ (⋂ i, f i)
-- Mathlib.Data.EReal.Operations
EReal.mul_nonneg : ∀ {a b : EReal}, 0 ≤ a → 0 ≤ b → 0 ≤ a * b
-- Std.Async.System
Std.Async.System.CPUTimes.mk.sizeOf_spec : ∀ (userTime niceTime systemTime idleTime interruptTime : Std.Time.Millisecond.Offset),
  sizeOf
      { userTime := userTime, niceTime := niceTime, systemTime := systemTime, idleTime := idleTime,
        interruptTime := interruptTime } =
    1 + sizeOf userTime + sizeOf niceTime + sizeOf systemTime + sizeOf idleTime + sizeOf interruptTime
-- Mathlib.Order.UpperLower.LocallyFinite
Set.Finite.lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [LocallyFiniteOrderBot α], s.Finite → (↑(lowerClosure s)).Finite
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_ofList_le : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} [Std.TransCmp cmp] {l : List (α × β)},
  (Std.ExtDTreeMap.Const.ofList l cmp).size ≤ l.length
-- Init.Data.Dyadic.Basic
Dyadic.instPowNat : Pow Dyadic ℕ
-- Init.Data.Nat.Lemmas
Nat.le_one_iff_eq_zero_or_eq_one : ∀ {n : ℕ}, n ≤ 1 ↔ n = 0 ∨ n = 1
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_plift_true : Cardinal.mk (PLift True) = 1
-- Mathlib.Algebra.Group.Subsemigroup.Membership
AddSubsemigroup.isAddCommutative_iSup : ∀ {ι : Sort u_1} {M : Type u_2} [inst : Add M] {S : ι → AddSubsemigroup M} [hS : ∀ (i : ι), IsAddCommutative ↥(S i)],
  Directed (fun x1 x2 => x1 ≤ x2) S → IsAddCommutative ↥(⨆ i, S i)
-- Mathlib.GroupTheory.Congruence.Defs
Con.mk.injEq : ∀ {M : Type u_1} [inst : Mul M] (toSetoid : Setoid M)
  (mul' : ∀ {w x y z : M}, toSetoid w x → toSetoid y z → toSetoid (w * y) (x * z)) (toSetoid_1 : Setoid M)
  (mul'_1 : ∀ {w x y z : M}, toSetoid_1 w x → toSetoid_1 y z → toSetoid_1 (w * y) (x * z)),
  ({ toSetoid := toSetoid, mul' := mul' } = { toSetoid := toSetoid_1, mul' := mul'_1 }) = (toSetoid = toSetoid_1)
-- Lean.Meta.Basic
/-- `hasFwdDeps` is true if there is another parameter whose type depends on this one.  -/
Lean.Meta.ParamInfo.hasFwdDeps : Lean.Meta.ParamInfo → Bool
-- Mathlib.RepresentationTheory.Coinvariants
Rep.coinvariantsAdjunction.eq_1 : ∀ (k : Type u) (G : Type v) [inst : CommRing k] [inst_1 : Monoid G],
  Rep.coinvariantsAdjunction k G =
    {
      unit :=
        {
          app := fun X =>
            Rep.ofHom { toLinearMap := ModuleCat.Hom.hom ((Rep.coinvariantsMk k G).app X), isIntertwining' := ⋯ },
          naturality := ⋯ },
      counit :=
        { app := fun X => Rep.desc (CategoryTheory.CategoryStruct.id ((Rep.trivialFunctor k G).obj X)),
          naturality := ⋯ },
      left_triangle_components := ⋯, right_triangle_components := ⋯ }
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_eq_self : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] {s : Set α} {f : α → M}, s.mulIndicator f = f ↔ Function.mulSupport f ⊆ s
-- Init.Prelude
instMonadReaderOfMonadReaderOf : (ρ : Type u) → (m : Type u → Type v) → [MonadReaderOf ρ m] → MonadReader ρ m
-- Mathlib.Combinatorics.Schnirelmann
_private.Mathlib.Combinatorics.Schnirelmann.0.add_eq_univ_of_one_le_schirelmannDensity_add_schnirelmannDensity.match_1_1.congr_eq_1 : ∀ (motive : ℕ ⊕ ℕ → Sort u_1) (x : ℕ ⊕ ℕ) (h_1 : (x : ℕ) → motive (Sum.inl x)) (h_2 : (y : ℕ) → motive (Sum.inr y))
  (x_1 : ℕ),
  x = Sum.inl x_1 →
    (match x with
      | Sum.inl x => h_1 x
      | Sum.inr y => h_2 y) ≍
      h_1 x_1
-- Mathlib.RingTheory.PolynomialLaw.Basic
PolynomialLaw.mk.injEq : ∀ {R : Type u} [inst : CommSemiring R] {M : Type u_1} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_2}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N]
  (toFun' :
    (S : Type u) → [inst_5 : CommSemiring S] → [inst_6 : Algebra R S] → TensorProduct R S M → TensorProduct R S N)
  (isCompat' :
    autoParam
      (∀ {S : Type u} [inst_5 : CommSemiring S] [inst_6 : Algebra R S] {S' : Type u} [inst_7 : CommSemiring S']
        [inst_8 : Algebra R S'] (φ : S →ₐ[R] S'),
        ⇑(LinearMap.rTensor N φ.toLinearMap) ∘ toFun' S = toFun' S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap))
      PolynomialLaw.isCompat'._autoParam)
  (toFun'_1 :
    (S : Type u) → [inst_5 : CommSemiring S] → [inst_6 : Algebra R S] → TensorProduct R S M → TensorProduct R S N)
  (isCompat'_1 :
    autoParam
      (∀ {S : Type u} [inst_5 : CommSemiring S] [inst_6 : Algebra R S] {S' : Type u} [inst_7 : CommSemiring S']
        [inst_8 : Algebra R S'] (φ : S →ₐ[R] S'),
        ⇑(LinearMap.rTensor N φ.toLinearMap) ∘ toFun'_1 S = toFun'_1 S' ∘ ⇑(LinearMap.rTensor M φ.toLinearMap))
      PolynomialLaw.isCompat'._autoParam),
  ({ toFun' := toFun', isCompat' := isCompat' } = { toFun' := toFun'_1, isCompat' := isCompat'_1 }) =
    (toFun' = toFun'_1)
-- Mathlib.Topology.ContinuousOn
/-- **Alias** of `continuousOn_iff_continuous_domRestrict`. -/
continuousOn_iff_continuous_restrict : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  ContinuousOn f s ↔ Continuous (s.domRestrict f)
-- Mathlib.AlgebraicGeometry.Morphisms.FinitePresentation
AlgebraicGeometry.instLocallyOfFinitePresentationSndScheme : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Z) (g : Y ⟶ Z) [AlgebraicGeometry.LocallyOfFinitePresentation f],
  AlgebraicGeometry.LocallyOfFinitePresentation (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.FieldTheory.Normal.Basic
/-- A compositum of normal extensions is normal.  -/
IntermediateField.normal_iSup : ∀ (F : Type u_1) (K : Type u_2) [inst : Field F] [inst_1 : Field K] [inst_2 : Algebra F K] {ι : Type u_3}
  (t : ι → IntermediateField F K) [h : ∀ (i : ι), Normal F ↥(t i)], Normal F ↥(⨆ i, t i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.inter_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF), m₃.WF → m₁.Equiv m₂ → (m₁.inter m₃ ⋯).Equiv (m₂.inter m₃ ⋯)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.ext_get? : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  {t₁ t₂ : Std.ExtDTreeMap α β cmp}, (∀ (k : α), t₁.get? k = t₂.get? k) → t₁ = t₂
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
SSet.horn.IsCompatible.δ_pred_comp : ∀ {n : ℕ} {X : SSet} {i : Fin (n + 3)} {f : (j : Fin (n + 3)) → j ≠ i → (SSet.stdSimplex.obj { len := n + 1 } ⟶ X)},
  SSet.horn.IsCompatible f →
    ∀ (j k : Fin (n + 3)) (hj : autoParam (j ≠ i) SSet.horn.IsCompatible.δ_pred_comp._auto_1)
      (hk : autoParam (k ≠ i) SSet.horn.IsCompatible.δ_pred_comp._auto_3)
      (hjk : autoParam (j < k) SSet.horn.IsCompatible.δ_pred_comp._auto_5),
      CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ (k.pred ⋯)) (f j hj) =
        CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ (j.castPred ⋯)) (f k hk)
-- Init.Data.Int.Basic
/-- Equality predicate for kernel reduction.  -/
Int.beq' : ℤ → ℤ → Bool
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.below.whisker_left_comp : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} →
      {f g : a ⟶ b} →
        (a_1 a_2 : CategoryTheory.FreeBicategory.Hom₂ f g) → CategoryTheory.FreeBicategory.Rel a_1 a_2 → Prop}
  {a b c : B} (f : CategoryTheory.FreeBicategory.Hom a b) {g h i : CategoryTheory.FreeBicategory.Hom b c}
  (η : CategoryTheory.FreeBicategory.Hom₂ g h) (θ : CategoryTheory.FreeBicategory.Hom₂ h i),
  CategoryTheory.FreeBicategory.Rel.below ⋯
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
/-- In cartesian monoidal categories, the second product projections `snd` have a functorial choice
of pullbacks.  -/
CategoryTheory.ChosenPullbacksAlong.cartesianMonoidalCategorySnd : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      (X Y : C) → CategoryTheory.ChosenPullbacksAlong (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)
-- Mathlib.Order.Hom.CompleteLattice
instCoeTCSInfHomOfSInfHomClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] → [inst_1 : InfSet α] → [inst_2 : InfSet β] → [sInfHomClass F α β] → CoeTC F (sInfHom α β)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.Functor.toStructuredArrow_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (G : CategoryTheory.Functor E C) (X : D)
  (F : CategoryTheory.Functor C D) (f : (Y : E) → X ⟶ F.obj (G.obj Y))
  (h : ∀ {Y Z : E} (g : Y ⟶ Z), CategoryTheory.CategoryStruct.comp (f Y) (F.map (G.map g)) = f Z) {X_1 Y : E}
  (g : X_1 ⟶ Y), (G.toStructuredArrow X F f h).map g = CategoryTheory.StructuredArrow.homMk (G.map g) ⋯
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.isUnit_map_of_injective : ∀ {A : Type u_4} [inst : CommRing A] {L : Type u_7} [inst_1 : Field L] {g : A →+* L},
  Function.Injective ⇑g → ∀ (y : ↥(nonZeroDivisors A)), IsUnit (g ↑y)
-- Init.Data.Vector.Lemmas
Vector.toArray_singleton : ∀ {α : Type u_1} {x : α}, (Vector.singleton x).toArray = #[x]
-- Mathlib.RingTheory.Valuation.Quotient
/-- If `hJ : J ⊆ supp v` then `onQuotVal hJ` is the induced function on `R / J` as a function.
Note: it's just the function; the valuation is `onQuot hJ`.  -/
Valuation.onQuotVal : {R : Type u_1} →
  {Γ₀ : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] → (v : Valuation R Γ₀) → {J : Ideal R} → J ≤ v.supp → R ⧸ J → Γ₀
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.insertMany_append : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {l₁ l₂ : List ((a : α) × β a)}, t.insertMany (l₁ ++ l₂) = (t.insertMany l₁).insertMany l₂
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.ext' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} {f g : E.Hom F} (hs₀ : f.s₀ = g.s₀),
  (∀ (i : E.I₀), f.h₀ i = CategoryTheory.CategoryStruct.comp (g.h₀ i) (CategoryTheory.eqToHom ⋯)) →
    ∀ (hs₁ : ∀ (i j : E.I₀) (k : E.I₁ i j), f.s₁ k = (CategoryTheory.PreOneHypercover.congrIndexOneOfEq ⋯ ⋯) (g.s₁ k)),
      (∀ (i j : E.I₀) (k : E.I₁ i j),
          f.h₁ k =
            CategoryTheory.CategoryStruct.comp (g.h₁ k)
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.PreOneHypercover.congrIndexOneOfEqIso ⋯ ⋯ (g.s₁ k)).inv (CategoryTheory.eqToHom ⋯))) →
        f = g
-- Mathlib.Algebra.Symmetrized
SymAlg.unsym_surjective : ∀ {α : Type u_1}, Function.Surjective ⇑SymAlg.unsym
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.mapGlueData_J : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F],
  (D.mapGlueData F).J = D.J
-- Mathlib.Algebra.Group.Submonoid.Pointwise
Submonoid.mem_closure_inv : ∀ {G : Type u_2} [inst : Group G] (s : Set G) (x : G), x ∈ Submonoid.closure s⁻¹ ↔ x⁻¹ ∈ Submonoid.closure s
-- Std.Time.Format
/-- The DateTimeZone24Hour format, which follows the pattern `uuuu-MM-dd:HH:mm:ss.SSSSSSSSS` for
representing date, time, and time zone.
 -/
Std.Time.Formats.dateTime24Hour : Std.Time.GenericFormat (Std.Time.Awareness.only Std.Time.TimeZone.GMT)
-- Mathlib.Algebra.Category.ModuleCat.ProjectiveDimension
ModuleCat.hasProjectiveDimensionLE_of_linearEquiv : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] [Small.{v', u} R] {M : ModuleCat R} {N : ModuleCat R} (e : ↑M ≃ₗ[R] ↑N)
  (n : ℕ) [CategoryTheory.HasProjectiveDimensionLE M n], CategoryTheory.HasProjectiveDimensionLE N n
-- Mathlib.Algebra.Lie.Rank
LieAlgebra.rank_le_card : ∀ (R : Type u_1) (L : Type u_3) {ι : Type u_5} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : Module.Finite R L] [inst_4 : Module.Free R L] [inst_5 : Fintype ι] (b : Module.Basis ι R L) [Nontrivial R],
  LieAlgebra.rank R L ≤ Fintype.card ι
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor_map_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {X Y : CategoryTheory.Comon (CategoryTheory.Functor C D)} (f : X ⟶ Y)
  (X_1 : C), ((CategoryTheory.Monoidal.ComonFunctorCategoryEquivalence.functor.map f).app X_1).hom = f.hom.app X_1
-- Mathlib.CategoryTheory.Retract
/-- Retracts are preserved when passing to the opposite category.  -/
CategoryTheory.Retract.op : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → CategoryTheory.Retract X Y → CategoryTheory.Retract (Opposite.op X) (Opposite.op Y)
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.edist_fst_le : ∀ {p : ENNReal} {α : Type u_2} {β : Type u_3} [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] (x y : WithLp p (α × β)), edist x.fst y.fst ≤ edist x y
-- Mathlib.Combinatorics.Enumerative.Composition
/-- The `i`-th boundary of a composition, i.e., the leftmost point of the `i`-th block. We include
a virtual point at the right of the last block, to make for a nice equiv with
`CompositionAsSet n`.  -/
Composition.boundary : {n : ℕ} → (c : Composition n) → Fin (c.length + 1) ↪o Fin (n + 1)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft.mk : {m : Type → Type} →
  (Mathlib.Tactic.BicategoryLike.Mor₁ → Mathlib.Tactic.BicategoryLike.Structural → m Lean.Expr) →
    (Mathlib.Tactic.BicategoryLike.Atom₁ →
        Mathlib.Tactic.BicategoryLike.Structural →
          Mathlib.Tactic.BicategoryLike.WhiskerLeft →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → m Lean.Expr) →
      (Mathlib.Tactic.BicategoryLike.Mor₁ →
          Mathlib.Tactic.BicategoryLike.Mor₁ →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr →
                  Mathlib.Tactic.BicategoryLike.NormalExpr →
                    Mathlib.Tactic.BicategoryLike.NormalExpr →
                      Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr) →
        (Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → m Lean.Expr) →
          Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft m
-- Mathlib.Data.Set.Basic
/-- **Alias** of `Set.sep_ofPred`. -/
Set.sep_setOf : ∀ {α : Type u} {p q : α → Prop}, {x | x ∈ {y | p y} ∧ q x} = {x | p x ∧ q x}
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ \ m₂},
  (m₁ \ m₂).getKey k h_mem = m₁.getKey k ⋯
-- Mathlib.Data.Fin.VecNotation
Matrix.range_cons : ∀ {α : Type u} {n : ℕ} (x : α) (u : Fin n → α), Set.range (Matrix.vecCons x u) = {x} ∪ Set.range u
-- Mathlib.Order.Directed
exists_ge_ge : ∀ {α : Type u_1} [inst : LE α] [IsDirectedOrder α] (a b : α), ∃ c, a ≤ c ∧ b ≤ c
-- Mathlib.Data.Int.AbsoluteValue
AbsoluteValue.map_units_int : ∀ {S : Type u_2} [inst : CommRing S] [inst_1 : LinearOrder S] [IsStrictOrderedRing S] (abv : AbsoluteValue ℤ S)
  (x : ℤˣ), abv ↑x = 1
-- Mathlib.Tactic.NormNum.GCD
/-- Evaluates the `Rat.num` function.  -/
Mathlib.Meta.NormNum.evalRatNum : Mathlib.Meta.NormNum.NormNumExt
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Steps through the whole iterator, counting the number of outputs emitted.

**Performance**:

This function's runtime is linear in the number of steps taken by the iterator.
 -/
Std.IterM.count : {α : Type u_1} →
  {m : Type u_1 → Type u_2} →
    {β : Type u_1} →
      [inst : Std.Iterator α m β] → [Std.IteratorLoop α m m] → [Monad m] → Std.IterM m β → m (ULift.{u_1, 0} ℕ)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.count_eq_match_step : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β},
  it.length =
    match ↑it.step with
    | Std.IterStep.yield it' out => it'.length + 1
    | Std.IterStep.skip it' => it'.length
    | Std.IterStep.done => 0
-- Mathlib.RingTheory.GradedAlgebra.Basic
DirectSum.coe_decompose_mul_of_left_mem_zero : ∀ {ι : Type u_1} {A : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring A] [inst_2 : SetLike σ A]
  [inst_3 : AddSubmonoidClass σ A] (𝒜 : ι → σ) {j : ι} [inst_4 : AddMonoid ι] [inst_5 : GradedRing 𝒜] {a b : A},
  a ∈ 𝒜 0 → ↑(((DirectSum.decompose 𝒜) (a * b)) j) = a * ↑(((DirectSum.decompose 𝒜) b) j)
-- Mathlib.FieldTheory.Perfect
/-- A field is perfect if every irreducible polynomial is separable.  -/
PerfectField.separable_of_irreducible : ∀ {K : Type u_1} {inst : Field K} [self : PerfectField K] {f : Polynomial K}, Irreducible f → f.Separable
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.induceHom.congr_simp : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} {s : Set V} {t : Set W} (φ φ_1 : G →g G')
  (e_φ : φ = φ_1) (φst : Set.MapsTo (⇑φ) s t), SimpleGraph.induceHom φ φst = SimpleGraph.induceHom φ_1 ⋯
-- Mathlib.GroupTheory.FreeAbelianGroup
/-- If `α` is a type, then `FreeAbelianGroup α` is the free abelian group generated by `α`.
This is an abelian group equipped with a function
`FreeAbelianGroup.of : α → FreeAbelianGroup α` which has the following universal property:
if `G` is any abelian group, and `f : α → G` is any function, then this function is
the composite of `FreeAbelianGroup.of` and a unique group homomorphism
`FreeAbelianGroup.lift f : FreeAbelianGroup α →+ G`.

A typical element of `FreeAbelianGroup α` is a formal sum of
elements of `α` and their formal inverses.
For example if `x` and `y` are terms of type `α` then `x + x + x - y` is a
"typical" element of `FreeAbelianGroup α`. In particular if `α` is empty
then `FreeAbelianGroup α` is isomorphic to the trivial group, and if `α` has one term
then `FreeAbelianGroup α` is isomorphic to `ℤ`.
One can think of `FreeAbelianGroup α` as the functions `α →₀ ℤ` with finite support,
and addition given pointwise.

TODO: rename to `FreeAddCommGroup` and introduce a multiplicative version
 -/
FreeAbelianGroup : Type u → Type u
-- Init.Grind.Util
/-- Similar to `MatchCond`, but not reducible. We use it to ensure `simp`
will not eliminate it. After we apply `simp`, we replace it with `MatchCond`.
 -/
Lean.Grind.PreMatchCond : Prop → Prop
-- Mathlib.Data.List.Cycle
Cycle.fintypeNodupCycle : {α : Type u_1} → [DecidableEq α] → [Fintype α] → Fintype { s // s.Nodup }
-- Mathlib.Data.Rat.Sqrt
Rat.sqrt_intCast : ∀ (z : ℤ), Rat.sqrt ↑z = ↑(Int.sqrt z)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.to_map_mem_maximal_iff : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (I : Ideal R)
  [hI : I.IsPrime] [inst_3 : IsLocalization.AtPrime S I] (x : R) (h : optParam (IsLocalRing S) ⋯),
  (algebraMap R S) x ∈ IsLocalRing.maximalIdeal S ↔ x ∈ I
-- Mathlib.Data.Set.Lattice
Set.biInter_lt_eq_iInter : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [NoMaxOrder α] {s : α → Set β}, ⋂ n, ⋂ m, ⋂ (_ : m < n), s m = ⋂ n, s n
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.degree_linear_lt : ∀ {R : Type u} {a b : R} [inst : Semiring R], (Polynomial.C a * Polynomial.X + Polynomial.C b).degree < 2
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.starModule : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] (s : StarSubalgebra R A), StarModule R ↥s
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Basic
/-- The composition of the unit and the counit is equal to the identity up to unitors.  -/
CategoryTheory.Bicategory.Adjunction.left_triangle : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {a b : B} {f : a ⟶ b} {g : b ⟶ a}
  (self : CategoryTheory.Bicategory.Adjunction f g),
  CategoryTheory.Bicategory.leftZigzag self.unit self.counit =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor f).hom
      (CategoryTheory.Bicategory.rightUnitor f).inv
-- Mathlib.MeasureTheory.Measure.Support
MeasureTheory.Measure.subset_compl_support_of_isOpen : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {μ : MeasureTheory.Measure X} {t : Set X},
  IsOpen t → μ t = 0 → t ⊆ μ.supportᶜ
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.sum_mem_iSup : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : Fintype ι] {f : ι → M} {p : ι → Submodule R M}, (∀ (i : ι), f i ∈ p i) → ∑ i, f i ∈ ⨆ i, p i
-- Mathlib.Algebra.QuadraticAlgebra.Basic
/-- **Alias** of the reverse direction of `QuadraticAlgebra.norm_eq_one_iff_mem_unitary`.

---

An element of `QuadraticAlgebra R a b` has norm equal to `1`
if and only if it is contained in the submonoid of unitary elements.  -/
QuadraticAlgebra.norm_eq_one : ∀ {R : Type u_2} {a b : R} [inst : CommRing R] {z : QuadraticAlgebra R a b},
  z ∈ unitary (QuadraticAlgebra R a b) → QuadraticAlgebra.norm z = 1
-- Std.Do.WP.SimpLemmas
Std.Do.WP.orElse_Option : ∀ {α : Type u_1} {x : Option α} {h : Unit → Option α}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u_1 + 1} Std.Do.PostShape.pure)},
  (Std.Do.wp (OrElse.orElse x h)).apply Q = (Std.Do.wp x).apply (Q.1, fun x => (Std.Do.wp (h ())).apply Q, Q.2.2)
-- Mathlib.Algebra.Homology.ComplexShapeSigns
ComplexShape.add_rel : ∀ {I : Type u_7} [inst : AddMonoid I] (c : ComplexShape I) [c.TensorSigns] (r : I) {p q : I},
  c.Rel p q → c.Rel (r + p) (r + q)
-- Mathlib.Data.Seq.Basic
Stream'.Seq.dropn_add : ∀ {α : Type u} (s : Stream'.Seq α) (m n : ℕ), s.drop (m + n) = (s.drop m).drop n
-- Batteries.Recycling.RBTree.Alter
/-- The `alter` function preserves the balance invariants.  -/
RBTree.RBNode.Balanced.alter : ∀ {α : Type u_1} {c : RBTree.RBColor} {n : ℕ} {cut : α → Ordering} {f : Option α → Option α} {t : RBTree.RBNode α},
  t.Balanced c n → ∃ c n, (RBTree.RBNode.alter cut f t).Balanced c n
-- Mathlib.Combinatorics.Quiver.Path
Quiver.Reachable.trans : ∀ {V : Type u} [inst : Quiver V] {a b c : V}, Quiver.Reachable a b → Quiver.Reachable b c → Quiver.Reachable a c