mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
/-- A spectral object in a pretriangulated category `C` indexed by a category `ι` consists
of a functor `ω₁ : ComposableArrows ι 1 ⥤ C`, and a functorial distinguished triangle
from the category `ComposableArrows ι 2`, which must be of the form
`ω₁.obj (mk₁ f) ⟶ ω₁.obj (mk₁ (f ≫ g)) ⟶ ω₁.obj (mk₁ g) ⟶ ...` when evaluated
on `mk₂ f g : ComposableArrows ι 2`.  -/
CategoryTheory.Triangulated.SpectralObject : (C : Type u_1) →
  (ι : Type u_2) →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
          [inst_3 : CategoryTheory.HasShift C ℤ] →
            [inst_4 : CategoryTheory.Preadditive C] →
              [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
                [CategoryTheory.Pretriangulated C] → Type (max (max (max u_1 u_2) v_1) v_2)
-- Lean.Data.Options
Lean.Options.setBool : Lean.Options → Lean.Name → Bool → Lean.Options
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.op_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂),
  h.op.h₁ = h.h₂.op
-- Mathlib.Algebra.Ring.Defs
/-- A non-associative commutative semiring is a `NonAssocSemiring` with commutative
multiplication.  -/
NonAssocCommSemiring : Type u → Type u
-- Mathlib.AlgebraicGeometry.SpreadingOut
/-- Given `S`-schemes `X Y` and points `x : X` `y : Y` over `s : S`.
Suppose we have the following diagram of `S`-schemes
```
Spec 𝒪_{X, x} ⟶ X
    |
  Spec(φ)
    ↓
Spec 𝒪_{Y, y} ⟶ Y
```
Then the map `Spec(φ)` spreads out to an `S`-morphism on an open subscheme `U ⊆ X`,
```
Spec 𝒪_{X, x} ⟶ U ⊆ X
    |             |
  Spec(φ)         |
    ↓             ↓
Spec 𝒪_{Y, y} ⟶ Y
```
provided that `Y` is locally of finite type over `S` and
`X` is "germ-injective" at `x` (e.g. when it's integral or locally Noetherian).

TODO: The condition on `X` is unnecessary when `Y` is locally of finite presentation.
 -/
AlgebraicGeometry.spread_out_of_isGermInjective : ∀ {X Y S : AlgebraicGeometry.Scheme} (sX : X ⟶ S) (sY : Y ⟶ S) [AlgebraicGeometry.LocallyOfFiniteType sY] {x : ↥X}
  [X.IsGermInjectiveAt x] {y : ↥Y} (e : sX x = sY y) (φ : Y.presheaf.stalk y ⟶ X.presheaf.stalk x),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.stalkMap sY y) φ =
      CategoryTheory.CategoryStruct.comp (S.presheaf.stalkSpecializes ⋯) (AlgebraicGeometry.Scheme.Hom.stalkMap sX x) →
    ∃ U,
      ∃ (hxU : x ∈ U),
        ∃ f,
          CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map φ) (Y.fromSpecStalk y) =
              CategoryTheory.CategoryStruct.comp (U.fromSpecStalkOfMem x hxU) f ∧
            CategoryTheory.CategoryStruct.comp f sY = CategoryTheory.CategoryStruct.comp U.ι sX
-- Mathlib.Order.Heyting.Basic
sdiff_left_inj : ∀ {α : Type u_2} [inst : GeneralizedCoheytingAlgebra α] {a b c : α}, c ≤ a → c ≤ b → (a \ c = b \ c ↔ a = b)
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.mapTriangleRotateIso_hom_app_hom₁ : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Preadditive C] [inst_6 : CategoryTheory.Preadditive D] [inst_7 : F.Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleRotateIso.hom.app X).hom₁ = CategoryTheory.CategoryStruct.id (F.obj X.obj₂)
-- Init.Grind.Attr
/-- Like `@[lia]`, but enforces the minimal indexable subexpression condition (see `@[grind!]`).  -/
Lean.Parser.Attr.lia! : Lean.ParserDescr
-- Batteries.Data.Char.AsciiCasing
Char.isLower.eq_1 : ∀ (c : Char), c.isLower = (decide (c.val ≥ 'a'.val) && decide (c.val ≤ 'z'.val))
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.isEmpty_filter_key_eq_false_iff : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α] {f : α → Bool},
  (↑m).WF →
    ((↑(Std.DHashMap.Internal.Raw₀.filter (fun a x => f a) m)).isEmpty = false ↔
      ∃ k, ∃ (h : m.contains k = true), f (m.getKey k h) = true)
-- Mathlib.CategoryTheory.Functor.Currying
CategoryTheory.Functor.curryObjCompIso_hom_app_app : ∀ {B : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} B] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  {D : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} D] {E : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E] (F : CategoryTheory.Functor (C × B) D) (G : CategoryTheory.Functor D E)
  (X : B) (X_1 : C),
  ((F.curryObjCompIso G).hom.app X).app X_1 = CategoryTheory.CategoryStruct.id (G.obj (F.obj (X_1, X)))
-- Mathlib.Topology.Order
TopologicalSpace.GenerateOpen.below.basic : ∀ {α : Type u} {g : Set (Set α)} {motive : (a : Set α) → TopologicalSpace.GenerateOpen g a → Prop} (s : Set α)
  (a : s ∈ g), TopologicalSpace.GenerateOpen.below ⋯
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.domRestrict₂_comp_domRestrict`. -/
Set.restrict₂_comp_restrict : ∀ {α : Type u_1} {π : α → Type u_6} {s t : Set α} (hst : s ⊆ t), Set.domRestrict₂ hst ∘ t.domRestrict = s.domRestrict
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)}, (t.alter k f).get? k = f (t.get? k)
-- Mathlib.Data.Finsupp.BigOperators
List.mem_foldr_sup_support_iff : ∀ {ι : Type u_1} {M : Type u_2} [inst : DecidableEq ι] [inst_1 : Zero M] {l : List (ι →₀ M)} {x : ι},
  x ∈ List.foldr (fun x1 x2 => x1.support ⊔ x2) ∅ l ↔ ∃ f ∈ l, x ∈ f.support
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vlt.eq_1 : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] (x y : R), (x <ᵥ y) = ¬y ≤ᵥ x
-- Mathlib.Order.Basic
Decidable.eq_iff_le_not_lt : ∀ {α : Type u_2} [inst : PartialOrder α] {a b : α} [DecidableLE α], a = b ↔ a ≤ b ∧ ¬a < b
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.inl_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : StarAddMonoid A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : StarAddMonoid B] (x : A), (NonUnitalStarAlgHom.inl R A B) x = (x, 0)
-- Init.WF
Prod.lex : {α : Type u} → {β : Type v} → WellFoundedRelation α → WellFoundedRelation β → WellFoundedRelation (α × β)
-- Mathlib.RingTheory.Etale.Kaehler
Algebra.Extension.equivH1CotangentOfFormallySmooth.eq_1 : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (P : Algebra.Extension R A)
  [inst_3 : Algebra.FormallySmooth R P.Ring],
  P.equivH1CotangentOfFormallySmooth =
    Algebra.Extension.H1Cotangent.equivOfFormallySmooth P (Algebra.Generators.self R A).toExtension
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.faceSingletonIso_one_hom_comp_ι_eq_δ_assoc : ∀ {Z : SSet} (h : SSet.stdSimplex.obj { len := 1 } ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.faceSingletonIso 1).hom
      (CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.face {1}).ι h) =
    CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ 0) h
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is inner regular for finite measure sets with respect to compact sets,
then any measurable set of finite measure can be approximated by a
compact subset. See also `MeasurableSet.exists_isCompact_lt_add`.  -/
MeasurableSet.exists_lt_isCompact_of_ne_top : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [μ.InnerRegularCompactLTTop] ⦃A : Set α⦄,
  MeasurableSet A → μ A ≠ ⊤ → ∀ {r : ENNReal}, r < μ A → ∃ K ⊆ A, IsCompact K ∧ r < μ K
-- Init.Data.Order.Lemmas
Std.instTotalNotLtOfLawfulOrderLTOfLe : ∀ {α : Type u} {x : LT α} [inst : LE α] [Std.LawfulOrderLT α], Std.Total fun x1 x2 => ¬x1 < x2
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getEntryGT?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getEntryGT? k = t₂.getEntryGT? k
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_union_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited β] {k : α},
  k ∉ t₂ → Std.ExtDTreeMap.Const.get! (t₁.union t₂) k = Std.ExtDTreeMap.Const.get! t₁ k
-- Init.Data.SInt.Lemmas
ISize.toInt32_ofIntTruncate : ∀ {n : ℤ},
  -2 ^ (System.Platform.numBits - 1) ≤ n →
    n < 2 ^ (System.Platform.numBits - 1) → (ISize.ofIntClamp n).toInt32 = Int32.ofInt n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isEmpty_emptyWithCapacity : ∀ {α : Type u} {β : α → Type v} [BEq α] [Hashable α] {c : ℕ}, (Std.DHashMap.Raw.emptyWithCapacity c).isEmpty = true
-- Mathlib.Algebra.Lie.SerreConstruction
/-- The terms corresponding to the `ad E`-relations.  -/
CartanMatrix.Relations.adE : (R : Type u) → {B : Type v} → [inst : CommRing R] → Matrix B B ℤ → B × B → FreeLieAlgebra R (CartanMatrix.Generators B)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- The underlying multivariate function of a multilinear map.  -/
MultilinearMap.toFun : {R : Type uR} →
  {ι : Type uι} →
    {M₁ : ι → Type v₁} →
      {M₂ : Type v₂} →
        [inst : Semiring R] →
          [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : (i : ι) → Module R (M₁ i)] →
                [inst_4 : Module R M₂] → MultilinearMap R M₁ M₂ → ((i : ι) → M₁ i) → M₂
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.sub_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] [inst_8 : IsTopologicalAddGroup F]
  {f g : E →SWOT[σ] F} (x : E), (f - g) x = f x - g x
-- Mathlib.LinearAlgebra.Multilinear.FiniteDimensional
_private.Mathlib.LinearAlgebra.Multilinear.FiniteDimensional.0.MultilinearMap.free_and_finite_fin : ∀ {R : Type u_2} {M₂ : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M₂] [inst_2 : Module R M₂]
  [Module.Finite R M₂] [Module.Free R M₂] (n : ℕ) (N : Fin n → Type u_5) [inst_5 : (i : Fin n) → AddCommGroup (N i)]
  [inst_6 : (i : Fin n) → Module R (N i)] [∀ (i : Fin n), Module.Finite R (N i)] [∀ (i : Fin n), Module.Free R (N i)],
  Module.Free R (MultilinearMap R N M₂) ∧ Module.Finite R (MultilinearMap R N M₂)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insertIfNew : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h : t.WF) {k a : α} {v : β}
  {h₁ : Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl = true},
  Std.DTreeMap.Internal.Impl.Const.get (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl a h₁ =
    if h₂ : compare k a = Ordering.eq ∧ k ∉ t then v else Std.DTreeMap.Internal.Impl.Const.get t a ⋯
-- Mathlib.Algebra.Group.Defs
nsmulRec_eq_nsmulBinRec : @nsmulRecAuto = @nsmulBinRecAuto
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionDisabled : Lean.ToJson Lean.Lsp.CodeActionDisabled
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_eq_mul_of_mem : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] {s : Finset ι} {f : ι → M} (a b : ι),
  a ∈ s → b ∈ s → a ≠ b → (∀ c ∈ s, c ≠ a ∧ c ≠ b → f c = 1) → ∏ x ∈ s, f x = f a * f b
-- Mathlib.GroupTheory.Finiteness
/-- A canonically ordered and well-quasi-ordered monoid must be finitely generated.  -/
CommMonoid.fg_of_wellQuasiOrderedLE : ∀ {M : Type u_5} [inst : CommMonoid M] [inst_1 : PartialOrder M] [WellQuasiOrderedLE M] [IsOrderedCancelMonoid M]
  [CanonicallyOrderedMul M], Monoid.FG M
-- Mathlib.Algebra.Order.Group.Multiset
Multiset.instAddLeftMono : ∀ {α : Type u_1}, AddLeftMono (Multiset α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.le_minKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α}, (compare k t.minKey!).isLE = true ↔ ∀ k' ∈ t, (compare k k').isLE = true
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
TwoSidedIdeal.bot_asIdeal : ∀ {R : Type u_1} [inst : Ring R], TwoSidedIdeal.asIdeal ⊥ = ⊥
-- Mathlib.Util.Export
Lean.Export.Alloc.mk.inj : ∀ {α : Type u_1} {inst : BEq α} {inst_1 : Hashable α} {map : Std.HashMap α ℕ} {next : ℕ} {map_1 : Std.HashMap α ℕ}
  {next_1 : ℕ}, { map := map, next := next } = { map := map_1, next := next_1 } → map = map_1 ∧ next = next_1
-- Mathlib.Order.Monotone.Defs
Monotone.comp_antitoneOn : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β} {s : Set α}, Monotone g → AntitoneOn f s → AntitoneOn (g ∘ f) s
-- Mathlib.Topology.Separation.Basic
/-- In a (weakly) locally compact R₁ space, compact closed neighborhoods of a point `x`
form a basis of neighborhoods of `x`.  -/
isCompact_isClosed_basis_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] [WeaklyLocallyCompactSpace X] (x : X),
  (nhds x).HasBasis (fun K => K ∈ nhds x ∧ IsCompact K ∧ IsClosed K) fun x => x
-- Init.Data.List.Lemmas
List.getElem?_tail : ∀ {α : Type u_1} {l : List α} {i : ℕ}, l.tail[i]? = l[i + 1]?
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDocumentHighlightParams : Lean.FromJson Lean.Lsp.DocumentHighlightParams
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (_P _P_1 : CategoryTheory.MorphismProperty C)
  (e__P : _P = _P_1) [inst_1 : _P.IsMultiplicative],
  CategoryTheory.WideSubcategory _P = CategoryTheory.WideSubcategory _P_1
-- Mathlib.Algebra.Algebra.Operations
Submodule.pow_mem_pow : ∀ {R : Type u} [inst : Semiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] (M : Submodule R A) {x : A}, x ∈ M → ∀ (n : ℕ), x ^ n ∈ M ^ n
-- Mathlib.Algebra.Homology.Embedding.Restriction
HomologicalComplex.restrictionXIso.congr_simp : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] {i : ι} {i' : ι'} (h : e.f i = i'),
  K.restrictionXIso e h = K.restrictionXIso e h
-- Mathlib.Algebra.Group.Units.Opposite
IsAddUnit.unop : ∀ {M : Type u_2} [inst : AddMonoid M] {m : Mᵃᵒᵖ}, IsAddUnit m → IsAddUnit (AddOpposite.unop m)
-- Mathlib.Algebra.Group.Commute.Units
/-- If a natural multiple of `x` is an additive unit, then `x` is an additive unit.  -/
AddUnits.ofNSMul : {M : Type u_1} → [inst : AddMonoid M] → (u : AddUnits M) → (x : M) → {n : ℕ} → n ≠ 0 → n • x = ↑u → AddUnits M
-- Mathlib.CategoryTheory.Monoidal.Widesubcategory
CategoryTheory.WideSubcategory.instMonoidalCategoryStruct : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.MorphismProperty C) →
      [inst_1 : CategoryTheory.MonoidalCategory C] →
        [inst_2 : P.IsMonoidalStable] → CategoryTheory.MonoidalCategoryStruct (CategoryTheory.WideSubcategory P)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.Lp.ext : ∀ {α : Type u_1} {E : Type u_4} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f g : ↥(MeasureTheory.Lp E p μ)}, ↑↑f =ᵐ[μ] ↑↑g → f = g
-- Mathlib.LinearAlgebra.Finsupp.Span
Finsupp.span_single_image : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set M) (a : α), Submodule.span R (Finsupp.single a '' s) = Submodule.map (Finsupp.lsingle a) (Submodule.span R s)
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_insertIfNew_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {v : β}, (m.insertIfNew k v).contains k = true
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.setParent_rankD_lt : ∀ {arr : Array Batteries.UFNode} {x y : Fin arr.size},
  arr[↑x].rank < arr[↑y].rank →
    ∀ {i : ℕ},
      (Batteries.UnionFind.parentD arr i ≠ i →
          Batteries.UnionFind.rankD arr i < Batteries.UnionFind.rankD arr (Batteries.UnionFind.parentD arr i)) →
        have arr' := arr.set ↑x { parent := ↑y, rank := arr[x].rank } ⋯;
        Batteries.UnionFind.parentD arr' i ≠ i →
          Batteries.UnionFind.rankD arr' i < Batteries.UnionFind.rankD arr' (Batteries.UnionFind.parentD arr' i)
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.Poly.denote'.go.match_1.eq_2 : ∀ (motive : Lean.Grind.Linarith.Poly → Sort u_1) (v : Lean.Grind.Linarith.Var) (p : Lean.Grind.Linarith.Poly)
  (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil)
  (h_2 : (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add 1 v p))
  (h_3 :
    (k : ℤ) →
      (v : Lean.Grind.Linarith.Var) → (p : Lean.Grind.Linarith.Poly) → motive (Lean.Grind.Linarith.Poly.add k v p)),
  (match Lean.Grind.Linarith.Poly.add 1 v p with
    | Lean.Grind.Linarith.Poly.nil => h_1 ()
    | Lean.Grind.Linarith.Poly.add 1 v p => h_2 v p
    | Lean.Grind.Linarith.Poly.add k v p => h_3 k v p) =
    h_2 v p
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn_toArray : ∀ {α β : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'} [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {γ : Type x} {it : Std.Iter β}
  {init : γ} {f : β → γ → m (ForInStep γ)}, forIn it.toArray init f = forIn it init f
-- Init.Data.String.Basic
/-- Constructs a valid position on `s` from a position and a proof that it is valid.  -/
String.Slice.pos : (s : String.Slice) → (off : String.Pos.Raw) → String.Pos.Raw.IsValidForSlice s off → s.Pos
-- Mathlib.Data.Nat.BinaryRec
Nat.bit_div_two : ∀ (b : Bool) (n : ℕ), Nat.bit b n / 2 = n
-- Init.Omega.LinearCombo
_private.Init.Omega.LinearCombo.0.Lean.Omega.instAppendString : Append String
-- Lean.Structure
Lean.StructureResolutionOrderConflict.mk.inj : ∀ {isDirectParent : Bool} {badParent : Lean.Name} {conflicts : Array (Bool × Lean.Name)} {isDirectParent_1 : Bool}
  {badParent_1 : Lean.Name} {conflicts_1 : Array (Bool × Lean.Name)},
  { isDirectParent := isDirectParent, badParent := badParent, conflicts := conflicts } =
      { isDirectParent := isDirectParent_1, badParent := badParent_1, conflicts := conflicts_1 } →
    isDirectParent = isDirectParent_1 ∧ badParent = badParent_1 ∧ conflicts = conflicts_1
-- Mathlib.Data.Set.Sups
Set.infs_subset_left : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s t₁ t₂ : Set α}, t₁ ⊆ t₂ → s ⊼ t₁ ⊆ s ⊼ t₂
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instContinuousSMul : ∀ {α : Type u_1} [inst : TopologicalSpace α] {R : Type u_3} {M : Type u_5} [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace R] [inst_3 : SMul R M] [inst_4 : ContinuousSMul R M], ContinuousSMul R C(α, M)
-- Mathlib.GroupTheory.SpecificGroups.KleinFour
IsAddKleinFour.instFinite : ∀ {G : Type u_1} [inst : AddGroup G] [IsAddKleinFour G], Finite G
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_ne_zero_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s : Finset β}
  {f : β → α} [Nontrivial α], s.lcm f ≠ 0 ↔ ∀ x ∈ s, f x ≠ 0
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearMap.bijective_of_linearIndependent_of_span_eq_top : ∀ {R : Type u_2} {M : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_6}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {f : M →ₗ[R] N} {ι : Type u_7} {v : ι → M},
  Submodule.span R (Set.range v) = ⊤ →
    LinearIndependent R (⇑f ∘ v) → Submodule.span R (Set.range (⇑f ∘ v)) = ⊤ → Function.Bijective ⇑f
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (a : α) (b : β a) (size : ℕ)
  (buckets : Array (Std.DHashMap.Internal.AssocList α β)) (hm : 0 < { size := size, buckets := buckets }.buckets.size),
  Std.DHashMap.Internal.Raw₀.containsThenInsertIfNew ⟨{ size := size, buckets := buckets }, hm⟩ a b =
    match Std.DHashMap.Internal.mkIdx buckets.size hm (hash a) with
    | ⟨i, h⟩ =>
      let bkt := buckets[i];
      if Std.DHashMap.Internal.AssocList.contains a bkt = true then (true, ⟨{ size := size, buckets := buckets }, hm⟩)
      else
        have size' := size + 1;
        let buckets' := buckets.uset i (Std.DHashMap.Internal.AssocList.cons a b bkt) h;
        (false, Std.DHashMap.Internal.Raw₀.expandIfNecessary ⟨{ size := size', buckets := buckets' }, ⋯⟩)
-- Init.Data.Int.Order
Int.mul_lt_mul_of_pos_left : ∀ {a b c : ℤ}, a < b → 0 < c → c * a < c * b
-- Mathlib.Algebra.Category.Grp.Basic
AddCommGrpCat.coe_comp : ∀ {X Y Z : AddCommGrpCat} {f : X ⟶ Y} {g : Y ⟶ Z},
  ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) =
    ⇑(CategoryTheory.ConcreteCategory.hom g) ∘ ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- `L` with the spectral norm is a `SeminormedRing`.  -/
spectralNorm.seminormedRing : (K : Type u) →
  [inst : NontriviallyNormedField K] →
    (L : Type v) →
      [inst_1 : Field L] →
        [inst_2 : Algebra K L] →
          [Algebra.IsAlgebraic K L] → [hu : IsUltrametricDist K] → [CompleteSpace K] → SeminormedRing L
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.neg_apply : ∀ {𝕜 : Type u_2} {α : Type u_5} [inst : AddGroup 𝕜] [inst_1 : LE α] (f : IncidenceAlgebra 𝕜 α) (a b : α),
  (-f) a b = -f a b
-- Std.Http.Data.Body.Full
/-- Builds a request body from raw bytes without setting any headers.
Use `bytes` instead if you want `Content-Type: application/octet-stream` set automatically.
 -/
Std.Http.Request.Builder.fromBytes : Std.Http.Request.Builder → ByteArray → Std.Async.Async (Std.Http.Request Std.Http.Body.Full)
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.comp_map_bijective_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} (adj : F ⊣ G) {X Y : D} (g : X ⟶ Y) (Z : C),
  (Function.Bijective fun f => CategoryTheory.CategoryStruct.comp f (G.map g)) ↔
    Function.Bijective fun f => CategoryTheory.CategoryStruct.comp f g
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.map_restrictAppIso_hom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f] (M : Y.Modules)
  {U V : X.Opens} (hUV : Opposite.op V ⟶ Opposite.op U),
  CategoryTheory.CategoryStruct.comp ((M.restrict f).presheaf.map hUV)
      (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M U).hom =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Modules.restrictAppIso f M V).hom
      (M.presheaf.map (CategoryTheory.homOfLE ⋯).op)
-- Mathlib.Order.RelSeries
RelSeries.toList_fromListIsChain : ∀ {α : Type u_1} {r : SetRel α α} (l : List α) (l_ne_nil : l ≠ []) (hl : List.IsChain (fun x1 x2 => (x1, x2) ∈ r) l),
  (RelSeries.fromListIsChain l l_ne_nil hl).toList = l
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for ensuring `OfNat.ofNat` bitvector literals are normalized.
For example, `(17 : BitVec 4)` is reduced to `(1 : BitVec 4)` when `bitVecOfNat := false`,
and to `1#4` when `bitVecOfNat := true`.
 -/
BitVec.isValue : Lean.Meta.Simp.DSimproc