mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.mem_carrier : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  {E : Topology.RelCWComplex.Subcomplex C} {x : X}, x ∈ E.carrier ↔ x ∈ ↑E
-- Std.Data.DTreeMap.Internal.Queries
/-- Returns the value for the key `k`, or `none` if such a key does not exist.  -/
Std.DTreeMap.Internal.Impl.get? : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → [Std.LawfulEqOrd α] → Std.DTreeMap.Internal.Impl α β → (k : α) → Option (β k)
-- Mathlib.RingTheory.IsGaloisGroup.Basic
/-- If `G` acts on `C` commuting with `A`, then the action of `G ⧸ N` on `B` commutes with `A`.  -/
IsGaloisGroup.smulCommClassQuotient : ∀ (G : Type u_1) [inst : Group G] (A : Type u_2) (B : Type u_3) (C : Type u_4) [inst_1 : CommSemiring A]
  [inst_2 : Semiring C] [inst_3 : Algebra A C] [inst_4 : MulSemiringAction G C] (N : Subgroup G)
  [inst_5 : CommSemiring B] [inst_6 : Algebra B C] [FaithfulSMul B C] [inst_8 : N.Normal] [inst_9 : Algebra A B]
  [IsScalarTower A B C] [SMulCommClass G A C] [inst_12 : MulSemiringAction G B] [inst_13 : MulAction (G ⧸ N) B]
  [SMulDistribClass G B C] [IsScalarTower G (G ⧸ N) B], SMulCommClass (G ⧸ N) A B
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- An auxiliary definition for `liftHomotopyZero`.  -/
CategoryTheory.ProjectiveResolution.liftHomotopyZeroSucc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        {P : CategoryTheory.ProjectiveResolution Y} →
          {Q : CategoryTheory.ProjectiveResolution Z} →
            (f : P.complex ⟶ Q.complex) →
              (n : ℕ) →
                (g : P.complex.X n ⟶ Q.complex.X (n + 1)) →
                  (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 2)) →
                    f.f (n + 1) =
                        CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g +
                          CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 2) (n + 1)) →
                      (P.complex.X (n + 2) ⟶ Q.complex.X (n + 3))
-- Mathlib.RingTheory.MvPowerSeries.LinearTopology
MvPowerSeries.LinearTopology.basis.eq_1 : ∀ (σ : Type u_1) (R : Type u_2) [inst : Ring R] (Jd : TwoSidedIdeal R × (σ →₀ ℕ)),
  MvPowerSeries.LinearTopology.basis σ R Jd =
    TwoSidedIdeal.mk' {f | ∀ e ≤ Jd.2, (MvPowerSeries.coeff e) f ∈ Jd.1} ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Topology.Maps.OpenQuotient
IsOpenQuotientMap.of_isOpenMap_isQuotientMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f → Topology.IsQuotientMap f → IsOpenQuotientMap f
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
SSet.stdSimplex.instDecidableEqObjOppositeSimplexCategory : (n : SimplexCategory) → (m : SimplexCategoryᵒᵖ) → DecidableEq ((SSet.stdSimplex.obj n).obj m)
-- Mathlib.Computability.TuringMachine.Computable
/-- a polynomial time function  -/
Turing.TM2ComputableInPolyTime.time : {α β αΓ βΓ : Type} →
  {ea : α → List αΓ} → {eb : β → List βΓ} → {f : α → β} → Turing.TM2ComputableInPolyTime ea eb f → Polynomial ℕ
-- Mathlib.Topology.Algebra.FilterBasis
ModuleFilterBasis.smul_left' : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : TopologicalSpace R] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] (self : ModuleFilterBasis R M) (x₀ : R) {U : Set M},
  U ∈ self.sets → ∃ V ∈ self.sets, V ⊆ (fun x => x₀ • x) ⁻¹' U
-- Init.Data.Int.DivMod.Bootstrap
Int.ediv_nonneg_iff_of_pos : ∀ {a b : ℤ}, 0 < b → (0 ≤ a / b ↔ 0 ≤ a)
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- If the order of a formal power series `f` is finite,
then some coefficient of degree the order of `f` is nonzero.  -/
MvPowerSeries.exists_coeff_ne_zero_and_order : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] {f : MvPowerSeries σ R},
  ↑f.order.toNat = f.order → ∃ d, (MvPowerSeries.coeff d) f ≠ 0 ∧ ↑(Finsupp.degree d) = f.order
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKeyLE!_eq_get!_getKeyLE? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α β} {k : α} [inst_1 : Inhabited α],
  Std.DTreeMap.Internal.Impl.getKeyLE! k t = (Std.DTreeMap.Internal.Impl.getKeyLE? k t).get!
-- Mathlib.GroupTheory.Index
/-- An additive subgroup has index two if and only if there exists `a` such that
for all `b`, exactly one of `b + a` and `b` belong to `H`.  -/
AddSubgroup.index_eq_two_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, H.index = 2 ↔ ∃ a, ∀ (b : G), Xor (b + a ∈ H) (b ∈ H)
-- Mathlib.RingTheory.Norm.Basic
Algebra.norm_ne_zero_iff_of_basis : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] {ι : Type w} [Finite ι]
  [IsDomain R] [IsDomain S] (b : Module.Basis ι R S) {x : S}, (Algebra.norm R) x ≠ 0 ↔ x ≠ 0
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.All.balLeft : ∀ {α : Type u_1} {p : α → Prop} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  RBTree.RBNode.All p l → p v → RBTree.RBNode.All p r → RBTree.RBNode.All p (l.balLeft v r)
-- Mathlib.CategoryTheory.Monoidal.CoherenceLemmas
CategoryTheory.MonoidalCategory.pentagon_inv_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (W X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj W X) Y Z).inv
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.MonoidalCategoryStruct.associator W X Y).hom
        (CategoryTheory.CategoryStruct.id Z)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator W X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id W)
          (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)
        (CategoryTheory.MonoidalCategoryStruct.associator W (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)
            Z).inv)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.div : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Div α] {s t : Finset α}, s.Nonempty → t.Nonempty → (s / t).Nonempty
-- Init.Data.Fin.Lemmas
Fin.cast_addNat_zero : ∀ {n n' : ℕ} (i : Fin n) (h : n + 0 = n'), Fin.cast h (i.addNat 0) = Fin.cast ⋯ i
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.instIsRightAdjointRightAdjoint : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (R : CategoryTheory.Functor D C) [inst_2 : R.IsLeftAdjoint], R.rightAdjoint.IsRightAdjoint
-- Mathlib.Algebra.Order.Archimedean.Class
/-- 1 is in its own class (see `MulArchimedeanClass.mk_eq_top_iff`),
which is also the largest class.  -/
MulArchimedeanClass.instOrderTop : {M : Type u_1} →
  [inst : CommGroup M] → [inst_1 : LinearOrder M] → [inst_2 : IsOrderedMonoid M] → OrderTop (MulArchimedeanClass M)
-- Mathlib.Topology.UrysohnsLemma
_private.Mathlib.Topology.UrysohnsLemma.0.Urysohns.CU.approx.match_1.eq_2 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (motive : ℕ → Urysohns.CU P → X → Sort u_2)
  (n : ℕ) (c : Urysohns.CU P) (x : X) (h_1 : (c : Urysohns.CU P) → (x : X) → motive 0 c x)
  (h_2 : (n : ℕ) → (c : Urysohns.CU P) → (x : X) → motive n.succ c x),
  (match n.succ, c, x with
    | 0, c, x => h_1 c x
    | n.succ, c, x => h_2 n c x) =
    h_2 n c x
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_const_one : ∀ {α : Type u_1} {E : Type u_3} (F : Type u_4) [inst : Norm E] [inst_1 : Norm F] [inst_2 : One F] [NormOneClass F]
  (c : E) (l : Filter α), (fun _x => c) =O[l] fun _x => 1
-- Std.Time.Format.Modifier
Std.Time.instInhabitedNumber : Inhabited Std.Time.Number
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.map_left_cancel : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  (f : S.LocalizationMap N) {x y : M} {c : ↥S}, f (x + ↑c) = f (y + ↑c) → f x = f y
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.ringInverse : ∀ {A : Type u_2} {a : A} [inst : Semiring A] [inst_1 : StarRing A], IsSelfAdjoint a → IsSelfAdjoint (Ring.inverse a)
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.sub : Nat.Primrec (Nat.unpaired fun x1 x2 => x1 - x2)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Basic
CategoryTheory.Pretriangulated.opShiftFunctorEquivalence_counitIso_inv_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ] (n : ℤ)
  {X Y : Cᵒᵖ} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp f
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app Y) =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.inv.app X)
      ((CategoryTheory.shiftFunctor Cᵒᵖ n).map ((CategoryTheory.shiftFunctor C n).map f.unop).op)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_rescale : ∀ {R : Type u_1} [inst : CommSemiring R] (f : PowerSeries R) (a : R) (n : ℕ),
  (PowerSeries.coeff n) ((PowerSeries.rescale a) f) = a ^ n * (PowerSeries.coeff n) f
-- Std.Sync.Broadcast
/-- Tried to unsubscribe a channel that already is not part of it.
 -/
Std.Broadcast.Error.notSubscribed : Std.Broadcast.Error
-- Mathlib.Order.Partition.Finpartition
Finpartition.empty_parts : ∀ (α : Type u_1) [inst : Lattice α] [inst_1 : OrderBot α], (Finpartition.empty α).parts = ∅
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.mem_iff_mem_toList : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} {t : RBTree.RBSet α cmp},
  x ∈ t ↔ ∃ y ∈ t.toList, cmp x y = Ordering.eq
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.conjugate : ∀ {R : Type u_1} [inst : Semigroup R] [inst_1 : StarMul R] {x : R},
  IsSelfAdjoint x → ∀ (z : R), IsSelfAdjoint (z * x * star z)
-- Mathlib.Algebra.Order.Quantale
AddQuantale.add_iSup_distrib : ∀ {α : Type u_1} {ι : Type u_2} {x : α} {f : ι → α} [inst : AddSemigroup α] [inst_1 : CompleteLattice α]
  [IsAddQuantale α], x + ⨆ i, f i = ⨆ i, x + f i
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.mk.sizeOf_spec : ∀ {numVarsSucc : ℕ} (clause : Std.Sat.CNF.Clause (Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc))
  (nodupkey :
    autoParam (∀ (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin numVarsSucc), (l, true) ∉ clause ∨ (l, false) ∉ clause)
      Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodupkey._autoParam)
  (nodup : autoParam (List.Nodup clause) Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.nodup._autoParam),
  sizeOf { clause := clause, nodupkey := nodupkey, nodup := nodup } = 1 + sizeOf clause + sizeOf nodup
-- Mathlib.Data.FinEnum
FinEnum.instSubtypeMemListOfDecidableEq : {α : Type u} → [DecidableEq α] → (xs : List α) → FinEnum { x // x ∈ xs }
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_inter_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ ∩ m₂).getKey? k = m₁.getKey? k
-- Mathlib.Data.Sum.Order
Sum.swap_lt_swap_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : LT α] [inst_1 : LT β] {a b : α ⊕ β}, a.swap < b.swap ↔ a < b
-- Mathlib.Combinatorics.Digraph.Basic
Digraph.top_adj : ∀ {V : Type u_2} (v w : V), ⊤.Adj v w
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBasis'.encard_eq_encard : ∀ {α : Type u_1} {M : Matroid α} {I X J : Set α}, M.IsBasis' I X → M.IsBasis' J X → I.encard = J.encard
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.CommMonoid.add_sum_eraseIdx : ∀ {M : Type u_4} [inst : AddCommMonoid M] {l : List M} {i : ℕ} (h : i < l.length), l[i] + (l.eraseIdx i).sum = l.sum
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.toList_rccIter : ∀ {α : Type u_1} {β : α → Type u_2} [inst : Ord α] [Std.TransOrd α] {t : Std.DTreeMap.Internal.Impl α β}
  {t_ord : t.Ordered} {lowerBound upperBound : α},
  (Std.DTreeMap.Internal.rccIterator t lowerBound upperBound).toList =
    List.filter (fun e => decide ((compare e.fst lowerBound).isGE = true ∧ (compare e.fst upperBound).isLE = true))
      t.toList
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_iInf_comap_of_surjective : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  [inst_3 : RingHomClass F R S] {ι : Sort u_3},
  Function.Surjective ⇑f → ∀ (K : ι → Ideal S), Ideal.map f (⨅ i, Ideal.comap f (K i)) = iInf K
-- Mathlib.NumberTheory.Multiplicity
dvd_geom_sum₂_self : ∀ {R : Type u_1} {n : ℕ} [inst : CommRing R] {x y : R}, ↑n ∣ x - y → ↑n ∣ ∑ i ∈ Finset.range n, x ^ i * y ^ (n - 1 - i)
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.linearIndependent_col_iff : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n R}
  [IsCancelAdd R], LinearIndependent R A.col ↔ A.Nonsingular
-- Mathlib.CategoryTheory.Subobject.MonoOver
/-- When `f : X ⟶ Y` is a monomorphism, `exists f` agrees with `map f`.
 -/
CategoryTheory.MonoOver.existsIsoMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      [inst_1 : CategoryTheory.Limits.HasImages C] →
        (f : X ⟶ Y) →
          [inst_2 : CategoryTheory.Mono f] → CategoryTheory.MonoOver.exists f ≅ CategoryTheory.MonoOver.map f
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₁ → k ∉ t₁ \ t₂
-- Mathlib.Data.Int.Interval
Int.card_Ico_of_le : ∀ (a b : ℤ), a ≤ b → ↑(Finset.Ico a b).card = b - a
-- Mathlib.Data.Nat.Bits
_private.Mathlib.Data.Nat.Bits.0.Nat.boddDiv2.match_1.eq_2 : ∀ (motive : Bool × ℕ → Sort u_1) (m : ℕ) (h_1 : (m : ℕ) → motive (false, m)) (h_2 : (m : ℕ) → motive (true, m)),
  (match (true, m) with
    | (false, m) => h_1 m
    | (true, m) => h_2 m) =
    h_2 m
-- Mathlib.RingTheory.PowerSeries.Basic
Polynomial.coe_pow : ∀ {R : Type u_1} [inst : Semiring R] {φ : Polynomial R} (n : ℕ), ↑(φ ^ n) = ↑φ ^ n
-- Mathlib.Data.ENat.Basic
ENat.coe_toNatHom : ⇑ENat.toNatHom = ENat.toNat
-- Mathlib.Algebra.Category.Grp.EpiMono
_private.Mathlib.Algebra.Category.Grp.EpiMono.0.GrpCat.SurjectiveOfEpiAuxs.termG : Lean.ParserDescr
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- This isomorphism says that hom-sets in the category `Over A` for a presheaf `A` where the domain
is of the form `(CostructuredArrow.toOver yoneda A).obj X` can instead be interpreted as
hom-sets in the category `(CostructuredArrow yoneda A)ᵒᵖ ⥤ Type v` where the domain is of the
form `yoneda.obj X` after adjusting the codomain accordingly. This is desirable because in the
latter case the Yoneda lemma can be applied.  -/
CategoryTheory.CostructuredArrow.toOverCompCoyoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).op.comp CategoryTheory.coyoneda ≅
        CategoryTheory.yoneda.op.comp
          (CategoryTheory.coyoneda.comp
            ((CategoryTheory.Functor.whiskeringLeft (CategoryTheory.Over A)
                  (CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v))
                  (Type (max u v))).obj
              (CategoryTheory.overEquivPresheafCostructuredArrow A).functor))
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.forIn_congr : ∀ {γ α β : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_3 : Std.IteratorLoop α Id m] {ita itb : Std.Iter β},
  ita = itb →
    ∀ {b b' : γ},
      b = b' → ∀ {f g : β → γ → m (ForInStep γ)}, (∀ (a : β) (b : γ), f a b = g a b) → forIn ita b f = forIn itb b' g
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wf_map₀ : ∀ {α : Type u} {β : α → Type v} {δ : α → Type w} [inst : BEq α] [inst_1 : Hashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  (↑m).WF → ∀ {f : (a : α) → β a → δ a}, (↑(Std.DHashMap.Internal.Raw₀.map f m)).WF
-- Mathlib.GroupTheory.PushoutI
/-- Given a pair `(head, tail)`, we can form a word by prepending `head` to `tail`, but
putting head into normal form first, by making sure it is expressed as an element
of the base group multiplied by an element of the transversal.  -/
Monoid.PushoutI.NormalWord.rcons : {ι : Type u_1} →
  {G : ι → Type u_2} →
    {H : Type u_3} →
      [inst : (i : ι) → Group (G i)] →
        [inst_1 : Group H] →
          {φ : (i : ι) → H →* G i} →
            {d : Monoid.PushoutI.NormalWord.Transversal φ} →
              [DecidableEq ι] →
                [(i : ι) → DecidableEq (G i)] →
                  (i : ι) → Monoid.PushoutI.NormalWord.Pair d i → Monoid.PushoutI.NormalWord d
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.size_rotateR : ∀ {α : Type u} {β : α → Type v} {k : α} {v : β k} {lk : α} {lv : β lk} {ll lr r : Std.DTreeMap.Internal.Impl α β},
  lr.Balanced →
    (Std.DTreeMap.Internal.Impl.rotateR k v lk lv ll lr r).size =
      (Std.DTreeMap.Internal.Impl.bin k v (Std.DTreeMap.Internal.Impl.bin lk lv ll lr) r).size
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.blast.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          (motive : aig.BinaryRefVec w → Sort u_1) →
            (input : aig.BinaryRefVec w) → ((lhs rhs : aig.RefVec w) → motive { lhs := lhs, rhs := rhs }) → motive input
-- Lean.Elab.Do.Basic
Lean.Elab.Do.instInhabitedDoElemCont : Inhabited Lean.Elab.Do.DoElemCont
-- Init.Data.Int.DivMod.Lemmas
Int.fmod_add_fmod : ∀ (m n k : ℤ), (m.fmod n + k).fmod n = (m + k).fmod n
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Corecursion
/-- A function on sequences is called a "friend" if any `n`-prefix of its output depends only on
the `n`-prefix of the input. Such functions can be used in the tail of (non-primitive) corecursive
definitions.  -/
Tactic.ComputeAsymptotics.Seq.FriendlyOperation : {α : Type u_1} → (Stream'.Seq α → Stream'.Seq α) → Prop
-- Batteries.Data.List.Lemmas
List.min!_eq_min?_getD : ∀ {α : Type u_1} [inst : Inhabited α] {l : List α} [inst_1 : Min α], l.min! = l.min?.getD default
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso_inv_pullbackHom : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (𝒰 : Y.OpenCover)
  (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f 𝒰.affineRefinement.openCover).I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.OpenCover.pullbackCoverAffineRefinementObjIso f 𝒰 i).inv
      (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰.affineRefinement.openCover f i) =
    AlgebraicGeometry.Scheme.Cover.pullbackHom (𝒰.X i.fst).affineCover
      (AlgebraicGeometry.Scheme.Cover.pullbackHom 𝒰 f i.fst) i.snd
-- Mathlib.Algebra.Category.Grp.Limits
AddGrpCat.forget_createsLimitsOfShape.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J],
  AddGrpCat.forget_createsLimitsOfShape = { CreatesLimit := fun {K} => inferInstance }
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, strict differentiability in the right endpoint.

If `f : ℝ → E` is integrable on `a..b` and `f x` has a finite limit `c` almost surely at `b`, then
`u ↦ ∫ x in a..u, f x` has derivative `c` at `b` in the sense of strict differentiability.  -/
intervalIntegral.integral_hasStrictDerivAt_of_tendsto_ae_right : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {f : ℝ → E} {c : E}
  {a b : ℝ},
  IntervalIntegrable f MeasureTheory.volume a b →
    StronglyMeasurableAtFilter f (nhds b) MeasureTheory.volume →
      Filter.Tendsto f (nhds b ⊓ MeasureTheory.ae MeasureTheory.volume) (nhds c) →
        HasStrictDerivAt (fun u => ∫ (x : ℝ) in a..u, f x) c b
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_involutive : ∀ (n : Type u_3) (α : Type v) [inst : InvolutiveStar α], Function.Involutive Matrix.conjTranspose
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.dualPairing_nondegenerate : ∀ {K : Type u_1} {V₁ : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁] (W : Subspace K V₁),
  (Submodule.dualPairing W).Nondegenerate
-- Mathlib.Order.Monotone.Basic
Int.rel_of_forall_rel_succ_of_lt : ∀ {β : Type v} (r : β → β → Prop) [IsTrans β r] {f : ℤ → β},
  (∀ (n : ℤ), r (f n) (f (n + 1))) → ∀ ⦃a b : ℤ⦄, a < b → r (f a) (f b)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey!_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → ∀ {km : α}, t.minKey! = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Topology.Separation.Basic
exists_isCompact_superset_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] [R1Space X] {s : Set X}, (∃ K, IsCompact K ∧ s ⊆ K) ↔ IsCompact (closure s)
-- Init.Data.String.Defs
String.toSubstring' : String → Substring.Raw
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normNatMulInst : Lean.Meta.Simp.DSimproc
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
/-- Each box is a sub-box of `I`  -/
BoxIntegral.Prepartition.le_of_mem' : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (self : BoxIntegral.Prepartition I), ∀ J ∈ self.boxes, J ≤ I
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
/-- **Fundamental theorem of calculus-1**, strict derivative in left endpoint for a locally finite
measure.

Let `f` be a measurable function integrable on `a..b`. Let `(la, la')` be a pair of
`intervalIntegral.FTCFilter`s around `a`. Suppose that `f` has a finite limit `c` at `la' ⊓ ae μ`.

Then `∫ x in v..b, f x ∂μ - ∫ x in u..b, f x ∂μ = -∫ x in u..v, c ∂μ + o(∫ x in u..v, (1:ℝ) ∂μ)`
as `u` and `v` tend to `la`.
 -/
intervalIntegral.measure_integral_sub_integral_sub_linear_isLittleO_of_tendsto_ae_left : ∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {a b : ℝ} {c : E}
  {la la' : Filter ℝ} {lt : Filter ι} {μ : MeasureTheory.Measure ℝ} {u v : ι → ℝ}
  [MeasureTheory.IsLocallyFiniteMeasure μ] [intervalIntegral.FTCFilter a la la'],
  IntervalIntegrable f μ a b →
    StronglyMeasurableAtFilter f la' μ →
      Filter.Tendsto f (la' ⊓ MeasureTheory.ae μ) (nhds c) →
        Filter.Tendsto u lt la →
          Filter.Tendsto v lt la →
            (fun t => ∫ (x : ℝ) in v t..b, f x ∂μ - ∫ (x : ℝ) in u t..b, f x ∂μ + ∫ (x : ℝ) in u t..v t, c ∂μ) =o[lt]
              fun t => ∫ (x : ℝ) in u t..v t, 1 ∂μ
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.Y_ne_negY_of_Y_ne' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} [NoZeroDivisors R] {P Q : Fin 3 → R},
  W'.Equation P → W'.Equation Q → P 0 * Q 2 ^ 2 = Q 0 * P 2 ^ 2 → P 1 * Q 2 ^ 3 ≠ W'.negY Q * P 2 ^ 3 → P 1 ≠ W'.negY P
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.isIso_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ⟶ G) [inst_2 : CategoryTheory.IsIso α] (X : C),
  (CategoryTheory.inv α).app X = CategoryTheory.inv (α.app X)
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.coe_bot : ↑⊥ = ∅