mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.mk.sizeOf_spec : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ} [inst_1 : SizeOf ι]
  [inst_2 : SizeOf κ] (deg : κ → ℤ)
  (i₀ : (r : ℤ) → κ → autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_1 → ι)
  (i₁ i₂ : κ → ι)
  (i₃ : (r : ℤ) → κ → autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_3 → ι)
  (le₀₁ :
    ∀ (r : ℤ) (pq : κ) (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_5),
      i₀ r pq ⋯ ≤ i₁ pq)
  (le₁₂ : ∀ (pq : κ), i₁ pq ≤ i₂ pq)
  (le₂₃ :
    ∀ (r : ℤ) (pq : κ) (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_9),
      i₂ pq ≤ i₃ r pq ⋯)
  (hc :
    ∀ (r : ℤ) (pq pq' : κ),
      (c r).Rel pq pq' →
        autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_14 →
          deg pq + 1 = deg pq')
  (hc₀₂ :
    ∀ (r : ℤ) (pq pq' : κ),
      (c r).Rel pq pq' →
        ∀ (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_16),
          i₀ r pq ⋯ = i₂ pq')
  (hc₁₃ :
    ∀ (r : ℤ) (pq pq' : κ),
      (c r).Rel pq pq' →
        ∀ (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_20),
          i₁ pq = i₃ r pq' ⋯)
  (antitone_i₀ :
    ∀ (r r' : ℤ) (pq : κ)
      (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_24)
      (hrr' : autoParam (r ≤ r') CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_26),
      i₀ r' pq ⋯ ≤ i₀ r pq ⋯)
  (monotone_i₃ :
    ∀ (r r' : ℤ) (pq : κ)
      (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_32)
      (hrr' : autoParam (r ≤ r') CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_34),
      i₃ r pq ⋯ ≤ i₃ r' pq ⋯)
  (i₀_prev :
    ∀ (r r' : ℤ) (pq pq' : κ),
      (c r).Rel pq pq' →
        ∀ (hrr' : autoParam (r + 1 = r') CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_41)
          (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_43),
          i₀ r' pq ⋯ = i₁ pq')
  (i₃_next :
    ∀ (r r' : ℤ) (pq pq' : κ),
      (c r).Rel pq pq' →
        ∀ (hrr' : autoParam (r + 1 = r') CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_47)
          (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_49),
          i₃ r' pq' ⋯ = i₂ pq),
  sizeOf
      { deg := deg, i₀ := i₀, i₁ := i₁, i₂ := i₂, i₃ := i₃, le₀₁ := le₀₁, le₁₂ := le₁₂, le₂₃ := le₂₃, hc := hc,
        hc₀₂ := hc₀₂, hc₁₃ := hc₁₃, antitone_i₀ := antitone_i₀, monotone_i₃ := monotone_i₃, i₀_prev := i₀_prev,
        i₃_next := i₃_next } =
    1
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.instSub : {Γ : Type u_1} → {R : Type u_3} → [inst : PartialOrder Γ] → [inst_1 : AddGroup R] → Sub (HahnSeries Γ R)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.instEssSurjObjPostOfFull : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (X : T) (F : CategoryTheory.Functor T D) [F.Full] [F.EssSurj], (CategoryTheory.Over.post F).EssSurj
-- Mathlib.RingTheory.Ideal.Quotient.HasFiniteQuotients
Ring.HasFiniteQuotients.finiteQuotient : ∀ {R : Type u_1} {inst : CommRing R} [self : Ring.HasFiniteQuotients R] {I : Ideal R}, I ≠ ⊥ → Finite (R ⧸ I)
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.InducedCategory.eqToHom_hom : ∀ {C : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{u_4, u_3} D] {F : C → D}
  {X Y : CategoryTheory.InducedCategory D F} (h : X = Y), (CategoryTheory.eqToHom h).hom = CategoryTheory.eqToHom ⋯
-- Mathlib.LinearAlgebra.Matrix.Hermitian
Matrix.isHermitian_iff_isSymm : ∀ {α : Type u_1} {n : Type u_4} [inst : Star α] [TrivialStar α] {A : Matrix n n α}, A.IsHermitian ↔ A.IsSymm
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.isFaithful_iff : ∀ (R : Type u) (L : Type v) (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M],
  LieModule.IsFaithful R L M ↔ Function.Injective ⇑(LieModule.toEnd R L M)
-- Mathlib.Topology.Order
TopologicalSpace.isOpen_generateFrom_of_mem : ∀ {α : Type u} {g : Set (Set α)} {s : Set α}, s ∈ g → IsOpen s
-- Mathlib.Order.PrimeIdeal
/-- Create an element of type `Order.Ideal.PrimePair` from an ideal satisfying the predicate
`Order.Ideal.IsPrime`.  -/
Order.Ideal.IsPrime.toPrimePair : {P : Type u_1} → [inst : Preorder P] → {I : Order.Ideal P} → I.IsPrime → Order.Ideal.PrimePair P
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.support_X_empty : ∀ {R : Type u} [inst : Semiring R], 1 = 0 → Polynomial.X.support = ∅
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 0-cocycles of the complex of inhomogeneous cochains of `A` are isomorphic to
`A.ρ.invariants`, which is a simpler type.  -/
groupCohomology.cocyclesIso₀ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] → (A : Rep.{u, u, u} k G) → groupCohomology.cocycles A 0 ≅ ModuleCat.of k ↥A.ρ.invariants
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.isEmpty.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtHashSet α), m = m_1 → m.isEmpty = m_1.isEmpty
-- Mathlib.Algebra.Star.Subalgebra
/-- Turn a non-unital star subalgebra containing `1` into a `StarSubalgebra`.  -/
NonUnitalStarSubalgebra.toStarSubalgebra : {R : Type u_1} →
  {A : Type u_2} →
    [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 : NonUnitalStarSubalgebra R A) → 1 ∈ S → StarSubalgebra R A
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_eq_getD_default : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} [inst_3 : Inhabited (β a)], m.get! a = m.getD a default
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.coe_to_GLPos_to_GL_det : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R] (g : Matrix.SpecialLinearGroup n R),
  Matrix.GeneralLinearGroup.det ↑(Matrix.SpecialLinearGroup.toGLPos g) = 1
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.polyOfInterest.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ),
  WittVector.polyOfInterest p n =
    WittVector.wittMul p (n + 1) + ↑p ^ (n + 1) * MvPolynomial.X (0, n + 1) * MvPolynomial.X (1, n + 1) -
        MvPolynomial.X (0, n + 1) * (MvPolynomial.rename (Prod.mk 1)) (wittPolynomial p ℤ (n + 1)) -
      MvPolynomial.X (1, n + 1) * (MvPolynomial.rename (Prod.mk 0)) (wittPolynomial p ℤ (n + 1))
-- Mathlib.LinearAlgebra.Determinant
LinearMap.det_toLin : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type u_4}
  [inst_3 : DecidableEq ι] [inst_4 : Fintype ι] (b : Module.Basis ι R M) (f : Matrix ι ι R),
  LinearMap.det ((Matrix.toLin b b) f) = f.det
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_zero : ↑0 = 0
-- Mathlib.RingTheory.NoetherNormalization
/-- `hom2 f I` is integral.  -/
_private.Mathlib.RingTheory.NoetherNormalization.0.NoetherNormalization.hom2_isIntegral : ∀ {k : Type u_1} [inst : Field k] {n : ℕ} (f : MvPolynomial (Fin (n + 1)) k) (I : Ideal (MvPolynomial (Fin (n + 1)) k)),
  f ≠ 0 → f ∈ I → (NoetherNormalization.hom2✝ f I).IsIntegral
-- Mathlib.Algebra.Module.Rat
IsScalarTower.nnrat : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : Module ℚ≥0 R]
  [inst_4 : Module ℚ≥0 M], IsScalarTower ℚ≥0 R M
-- Mathlib.Data.List.Cycle
Cycle.chain_range_succ : ∀ (r : ℕ → ℕ → Prop) (n : ℕ), Cycle.Chain r ↑(List.range n.succ) ↔ r n 0 ∧ ∀ m < n, r m m.succ
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Folds a monadic function over an iterator from the left, accumulating a value starting with `init`.
The accumulated value is combined with the each element of the list in order, using `f`.

The monadic effects of `f` are interleaved with potential effects caused by the iterator's step
function. Therefore, it may *not* be equivalent to `(← it.toList).foldlM`.
 -/
Std.IterM.foldM : {m : Type w → Type w'} →
  {n : Type w → Type w''} →
    [Monad n] →
      {α β γ : Type w} →
        [inst : Std.Iterator α m β] →
          [Std.IteratorLoop α m n] → [MonadLiftT m n] → (γ → β → n γ) → γ → Std.IterM m β → n γ
-- Std.Time.DateTime.WallTime
/-- Adds a `Minute.Offset` to the given `WallTime`.
 -/
Std.Time.WallTime.addMinutes : Std.Time.WallTime → Std.Time.Minute.Offset → Std.Time.WallTime
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.dist_inr : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A]
  [inst_2 : NormedSpace 𝕜 A] [inst_3 : IsScalarTower 𝕜 A A] [inst_4 : SMulCommClass 𝕜 A A]
  [inst_5 : RegularNormedAlgebra 𝕜 A] (a b : A), dist ↑a ↑b = dist a b
-- Mathlib.Combinatorics.Matroid.Minor.Delete
Matroid.delete_delete_eq_delete_sdiff : ∀ {α : Type u_1} (M : Matroid α) (D₁ D₂ : Set α), (M.delete D₁).delete D₂ = (M.delete D₁).delete (D₂ \ D₁)
-- Mathlib.AlgebraicGeometry.Morphisms.RingHomProperties
AlgebraicGeometry.HasRingHomProperty.isMultiplicative : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop}
  [AlgebraicGeometry.HasRingHomProperty P Q],
  (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.ContainsIdentities fun {R S} [CommRing R] [CommRing S] => Q) → P.IsMultiplicative
-- Std.Time.Time.Unit.Basic
/-- Converts a `Second.Offset` to a `Minute.Offset`.
 -/
Std.Time.Second.Offset.toMinutes : Std.Time.Second.Offset → Std.Time.Minute.Offset
-- Mathlib.Data.List.Sym
/-- `xs.sym n` is all unordered `n`-tuples from the list `xs` in some order.  -/
List.sym : {α : Type u_1} → (n : ℕ) → List α → List (Sym α n)
-- Init.Data.SInt.Bitwise
Int16.xor_zero : ∀ {a : Int16}, a ^^^ 0 = a
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.addGroup : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddGroup α] → AddGroup (Matrix m n α)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.get_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).get k h_mem = t₁.get k ⋯
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balanceL.match_7.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (l : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (r : Std.DTreeMap.Internal.Impl α β) →
      r.Balanced → Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size → Sort u_3)
  (r : Std.DTreeMap.Internal.Impl α β) (hrb : r.Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size r.size)
  (h_1 :
    (hrb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size Std.DTreeMap.Internal.Impl.leaf.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hrb hlr)
  (h_2 :
    (rs : ℕ) →
      (k : α) →
        (v : β k) →
          (l_1 r : Std.DTreeMap.Internal.Impl α β) →
            (hrb : (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r) hrb hlr)
  (rs : ℕ) (k : α) (v : β k) (l_1 r_1 : Std.DTreeMap.Internal.Impl α β)
  (hrb_1 : (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r_1).Balanced)
  (hlr_1 : Std.DTreeMap.Internal.Impl.BalanceLPrecond l.size (Std.DTreeMap.Internal.Impl.inner rs k v l_1 r_1).size),
  r = Std.DTreeMap.Internal.Impl.inner rs k v l_1 r_1 →
    hrb ≍ hrb_1 →
      hlr ≍ hlr_1 →
        (match r, hrb, hlr with
          | Std.DTreeMap.Internal.Impl.leaf, hrb, hlr => h_1 hrb hlr
          | Std.DTreeMap.Internal.Impl.inner rs k v l_2 r, hrb, hlr => h_2 rs k v l_2 r hrb hlr) ≍
          h_2 rs k v l_1 r_1 hrb_1 hlr_1
-- Mathlib.Data.List.DropRight
List.rdropWhile_concat_neg : ∀ {α : Type u_1} (p : α → Bool) (l : List α) (x : α), ¬p x = true → List.rdropWhile p (l ++ [x]) = l ++ [x]
-- Init.Data.Slice.List.Lemmas
List.toArray_mkSlice_roc : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  Std.Slice.toArray (Std.Roc.Sliceable.mkSlice xs lo<...=hi) = (List.drop (lo + 1) (List.take (hi + 1) xs)).toArray
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
/-- **Alias** of `Real.volume_eball`. -/
Real.volume_emetric_ball : ∀ (a : ℝ) (r : ENNReal), MeasureTheory.volume (Metric.eball a r) = 2 * r
-- Mathlib.CategoryTheory.Monoidal.Closed.FunctorCategory.Groupoid
CategoryTheory.Functor.ihom_ev_app : ∀ {D : Type u} {C : Type u_1} [inst : CategoryTheory.Groupoid D] [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalClosed C]
  (F G : CategoryTheory.Functor D C), (CategoryTheory.ihom.ev F).app G = F.closedCounit.app G
-- Init.Data.SInt.Lemmas
Int32.toNatClampNeg_toInt64 : ∀ (x : Int32), x.toInt64.toNatClampNeg = x.toNatClampNeg
-- Lean.Parser.Term
Lean.Parser.Term.rightact.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.withDensity.instSigmaFinite : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.SigmaFinite μ],
  MeasureTheory.SigmaFinite (ν.withDensity (μ.rnDeriv ν))
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.maxKeyD.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α β) →
        (x_1 : α) →
          ((fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback) →
            ((size : ℕ) →
                (k : α) →
                  (v : β k) →
                    (l : Std.DTreeMap.Internal.Impl α β) →
                      (x : α) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β k) →
                      (l : Std.DTreeMap.Internal.Impl α β) →
                        (size_1 : ℕ) →
                          (k_1 : α) →
                            (v_1 : β k_1) →
                              (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                                (fallback : α) →
                                  motive
                                    (Std.DTreeMap.Internal.Impl.inner size k v l
                                      (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
                                    fallback) →
                motive x x_1
-- Mathlib.Order.Filter.ListTraverse
Filter.mem_traverse : ∀ {α β γ : Type u} {f : β → Filter α} {s : γ → Set α} (fs : List β) (us : List γ),
  List.Forall₂ (fun b c => s c ∈ f b) fs us → traverse s us ∈ traverse f fs
-- Mathlib.CategoryTheory.Presentable.Directed
/-- [Stacks Tag 0032](https://stacks.math.columbia.edu/tag/0032) -/
CategoryTheory.IsFiltered.exists_directed : ∀ (J : Type w) [inst : CategoryTheory.SmallCategory J] [CategoryTheory.IsFiltered J],
  ∃ α x, ∃ (_ : IsDirected α fun x1 x2 => x1 ≤ x2) (_ : Nonempty α), ∃ F, F.Final
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.cast.congr_simp : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig1 aig2 : Std.Sat.AIG α}
  (s s_1 : aig1.RefVec len), s = s_1 → ∀ (h : aig1.decls.size ≤ aig2.decls.size), s.cast h = s_1.cast h
-- Mathlib.FieldTheory.Separable
Polynomial.card_rootSet_eq_natDegree_iff_of_splits : ∀ {F : Type u} [inst : Field F] {K : Type v} [inst_1 : Field K] [inst_2 : Algebra F K] {f : Polynomial F},
  f ≠ 0 → (Polynomial.map (algebraMap F K) f).Splits → (Fintype.card ↑(f.rootSet K) = f.natDegree ↔ f.Separable)
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
Ideal.emultiplicity_eq_emultiplicity_span : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsPrincipalIdealRing R] {a b : R},
  emultiplicity (Ideal.span {a}) (Ideal.span {b}) = emultiplicity a b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_insertIfNew_le_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k} {kmi : α},
  (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKey?.get ⋯ = kmi → (compare kmi k).isLE = true
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k fallback : α},
  (Std.DTreeMap.filter f t).getKeyD k fallback = ((t.getKey? k).pfilter fun x h' => f x (t.get x ⋯)).getD fallback
-- Mathlib.CategoryTheory.Core
CategoryTheory.Iso.coreRightUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D},
  F.rightUnitor.core =
    F.coreComp (CategoryTheory.Functor.id D) ≪≫
      F.core.isoWhiskerLeft (CategoryTheory.Functor.coreId D) ≪≫ F.core.rightUnitor
-- Mathlib.Algebra.Torsor.Defs
/-- Scalar multiplication and division with the same element cancels out.  -/
Torsor.smul_sdiv' : ∀ {G : outParam (Type u_1)} {P : Type u_2} {inst : Group G} [self : Torsor G P] (g : G) (p : P), g • p /ₛ p = g
-- Init.Data.Float.Model.Format.Basic
/-- The total number of bits in the packed representation.  -/
Float.Model.Format.numBits : Float.Model.Format → ℕ
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.addConst_le_card : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A B : Finset G}, A.addConst B ≤ ↑B.card
-- Mathlib.LinearAlgebra.BilinearForm.Basic
LinearMap.BilinForm.coeFnAddMonoidHom_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) (x y : M), LinearMap.BilinForm.coeFnAddMonoidHom B x y = (B x) y
-- Mathlib.Topology.MetricSpace.DilationEquiv
/-- Typeclass saying that `F` is a type of bundled equivalences such that all `e : F` are
dilations.  -/
DilationEquivClass : (F : Type u_1) →
  (X : outParam (Type u_2)) →
    (Y : outParam (Type u_3)) → [PseudoEMetricSpace X] → [PseudoEMetricSpace Y] → [EquivLike F X Y] → Prop
-- Init.Data.UInt.Lemmas
UInt32.neg_neg : ∀ {a : UInt32}, - -a = a
-- Mathlib.NumberTheory.RamificationInertia.Unramified
_private.Mathlib.NumberTheory.RamificationInertia.Unramified.0.«termE(_|_)» : Lean.ParserDescr
-- Mathlib.Condensed.Discrete.Colimit
Condensed.isoFinYoneda_hom_app_hom_apply : ∀ (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) [inst : CategoryTheory.Limits.PreservesFiniteProducts F]
  (X : FintypeCatᵒᵖ)
  (x :
    (CategoryTheory.Limits.Fan.mk
        (F.obj (Opposite.op (Condensed.fintypeCatAsCofan (FintypeCat.toProfinite.obj (Opposite.unop X))).pt)) fun j =>
        F.map ((Condensed.fintypeCatAsCofan (FintypeCat.toProfinite.obj (Opposite.unop X))).inj j).op).pt)
  (j : ↑(FintypeCat.toProfinite.obj (Opposite.unop X)).toTop),
  (CategoryTheory.ConcreteCategory.hom ((Condensed.isoFinYoneda F).hom.app X)) x j =
    (CategoryTheory.ConcreteCategory.hom
        (F.map ((Condensed.fintypeCatAsCofan (Profinite.of (Opposite.unop X).obj)).inj j).op))
      x
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- A set `S` of continuous linear maps with topology of uniform convergence on sets `s ∈ 𝔖`
is von Neumann bounded iff for any `s ∈ 𝔖`,
the set `{f x | (f ∈ S) (x ∈ s)}` is von Neumann bounded.  -/
UniformConvergenceCLM.isVonNBounded_iff : ∀ {𝕜₁ : 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 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] {R : Type u_6} [inst_7 : NormedDivisionRing R]
  [inst_8 : TopologicalSpace F] [inst_9 : IsTopologicalAddGroup F] [inst_10 : Module R F]
  [inst_11 : ContinuousConstSMul R F] [inst_12 : SMulCommClass 𝕜₂ R F] {𝔖 : Set (Set E)}
  {S : Set (UniformConvergenceCLM σ F 𝔖)},
  Bornology.IsVonNBounded R S ↔ ∀ s ∈ 𝔖, Bornology.IsVonNBounded R (Set.image2 (fun f x => f x) S s)
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
HomotopicalAlgebra.Precylinder.LeftHomotopy.unop_h : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : Cᵒᵖ} {P : HomotopicalAlgebra.Precylinder X}
  {f g : X ⟶ Y} (h : P.LeftHomotopy f g), h.unop.h = h.h.unop
-- Mathlib.CategoryTheory.Sites.Coherent.Basic
/-- The condition `Preregular C` is a property that effective epis can be "pulled back" along any
morphism. This is satisfied e.g. by categories that have pullbacks that preserve effective
epimorphisms (like `Profinite` and `CompHaus`), and categories where every object is projective
(like  `Stonean`).
 -/
CategoryTheory.Preregular : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Mathlib.Data.ENNReal.Inv
ENNReal.add_thirds : ∀ (a : ENNReal), a / 3 + a / 3 + a / 3 = a
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mrefinePat⟨_⟩» : Lean.ParserDescr
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.LiftRel.trans : ∀ {α : Type u} (R : α → α → Prop) [IsTrans α R], IsTrans (Stream'.WSeq α) (Stream'.WSeq.LiftRel R)
-- Init.Data.Vector.Lemmas
Vector.findFinIdx?_toList : ∀ {α : Type u_1} {n : ℕ} {p : α → Bool} {xs : Vector α n},
  List.findFinIdx? p xs.toList = Option.map (Fin.cast ⋯) (Vector.findFinIdx? p xs)
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNNRat.to_isNat : ∀ {α : Type u_1} [inst : Semiring α] {a : α} {n : ℕ},
  Mathlib.Meta.NormNum.IsNNRat a n 1 → Mathlib.Meta.NormNum.IsNat a n
-- Mathlib.Algebra.DirectSum.Module
/-- `curry` as a linear map.  -/
DirectSum.sigmaLcurry : (R : Type u) →
  [inst : Semiring R] →
    {ι : Type v} →
      {α : ι → Type u_1} →
        {δ : (i : ι) → α i → Type w} →
          [DecidableEq ι] →
            [inst_2 : (i : ι) → (j : α i) → AddCommMonoid (δ i j)] →
              [inst_3 : (i : ι) → (j : α i) → Module R (δ i j)] →
                (DirectSum ((x : ι) × α x) fun i => δ i.fst i.snd) →ₗ[R]
                  DirectSum ι fun i => DirectSum (α i) fun j => δ i j
-- Mathlib.Tactic.GCongr.Core
/-- Attempt to resolve an (implicitly) relational goal by one of a provided list of hypotheses,
either with such a hypothesis directly or by a limited palette of relational forward-reasoning from
these hypotheses.  -/
Lean.MVarId.gcongrForward : Array Lean.Expr → Lean.MVarId → Lean.MetaM Bool
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Spec.map_eqToHom : ∀ {R S : CommRingCat} (e : R = S), AlgebraicGeometry.Spec.map (CategoryTheory.eqToHom e) = CategoryTheory.eqToHom ⋯
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.Hom.subToKer_apply_coe : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f g : P.Hom P') (c : P.Ring), ↑((f.subToKer g) c) = f.toRingHom c - g.toRingHom c
-- Lean.Meta.Tactic.Grind.Arith.CommRing.RingM
Lean.Meta.Grind.Arith.CommRing.RingM.getCommRing : Lean.Meta.Grind.Arith.CommRing.RingM Lean.Meta.Grind.Arith.CommRing.CommRing
-- Init.Data.Nat.Basic
Nat.pos_of_ne_zero : ∀ {n : ℕ}, n ≠ 0 → 0 < n