mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.ExtDTreeMap.Basic
/-- Transforms the tree map into a list of mappings in ascending order.  -/
Std.ExtDTreeMap.Const.toArray : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → Array (α × β)
-- Mathlib.Data.FunLike.Ring
/-- A `FunLike` type with `(f + g) x = f x + g x` and `(f * g) x = f (g x)` is a `Semiring` if `α`
is a `Semiring`.  -/
FunLike.semiring : {F : Type u_1} →
  {α : Type u_2} →
    [inst : FunLike F α α] →
      [inst_1 : Zero F] →
        [inst_2 : One F] →
          [inst_3 : Mul F] →
            [inst_4 : Add F] →
              [inst_5 : AddCommMonoid α] →
                [IsZeroApply F α α] →
                  [IsAddApply F α α] →
                    [IsOneApplyEqSelf F α] →
                      [IsMulApplyEqComp F α] →
                        [inst_10 : SMul ℕ F] →
                          [IsSMulApply ℕ F α α] →
                            [AddMonoidHomClass F α α] → [inst_13 : NatCast F] → [IsNatCastApply F α] → Semiring F
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_disjSum : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] (s : Finset ι) (t : Finset κ) (f : ι ⊕ κ → M),
  ∑ x ∈ s.disjSum t, f x = ∑ x ∈ s, f (Sum.inl x) + ∑ x ∈ t, f (Sum.inr x)
-- Init.Data.Rat.Lemmas
Rat.lt_ceil_iff : ∀ {x : ℚ} {y : ℤ}, y < x.ceil ↔ ↑y < x
-- Mathlib.NumberTheory.LSeries.HurwitzZetaValues
_private.Mathlib.NumberTheory.LSeries.HurwitzZetaValues.0.HurwitzZeta.hurwitzZeta_neg_two_mul_nat : ∀ {k : ℕ} {x : ℝ},
  k ≠ 0 →
    x ∈ Set.Icc 0 1 →
      HurwitzZeta.hurwitzZeta (↑x) (-(2 * ↑k)) =
        -1 / (2 * ↑k + 1) * Polynomial.eval (↑x) (Polynomial.map (algebraMap ℚ ℂ) (Polynomial.bernoulli (2 * k + 1)))
-- Mathlib.Analysis.CStarAlgebra.Projection
/-- An idempotent element in a non-unital C⋆-algebra is self-adjoint iff it is normal.  -/
IsIdempotentElem.isSelfAdjoint_iff_isStarNormal : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal]
  {p : A}, IsIdempotentElem p → (IsSelfAdjoint p ↔ IsStarNormal p)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.centralizer_eq_top_iff_subset : ∀ (R : Type u) {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {s : Set A},
  Subalgebra.centralizer R s = ⊤ ↔ s ⊆ ↑(Subalgebra.center R A)
-- Std.Data.Internal.List.Associative
Std.Internal.List.mem_replaceEntry_of_true : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k : α} {v : β k},
  Std.Internal.List.containsKey k l = true → ⟨k, v⟩ ∈ Std.Internal.List.replaceEntry k v l
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.withDensity_apply_le : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : α → ENNReal) (s : Set α),
  ∫⁻ (a : α) in s, f a ∂μ ≤ (μ.withDensity f) s
-- Mathlib.RingTheory.Support
Module.notMem_support_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {p : PrimeSpectrum R}, p ∉ Module.support R M ↔ Subsingleton (LocalizedModule p.asIdeal.primeCompl M)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.tensorHom_left_snd : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X S U : C} {R T : CategoryTheory.Over X} (fS : S ⟶ X) (fU : U ⟶ X) (f : R ⟶ CategoryTheory.Over.mk fS)
  (g : T ⟶ CategoryTheory.Over.mk fU),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.tensorHom f g))
      (CategoryTheory.Limits.pullback.snd fS fU) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd R.hom T.hom) (CategoryTheory.Over.Hom.left g)
-- Mathlib.Condensed.Equivalence
/-- The equivalence from coherent sheaves on `Stonean` to coherent sheaves on `Profinite`.  -/
Condensed.StoneanProfinite.equivalence : (A : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    [∀ (X : Profiniteᵒᵖ),
          CategoryTheory.Limits.HasLimitsOfShape (CategoryTheory.StructuredArrow X Stonean.toProfinite.op) A] →
      CategoryTheory.Sheaf (CategoryTheory.coherentTopology Stonean) A ≌
        CategoryTheory.Sheaf (CategoryTheory.coherentTopology Profinite) A
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs.0.BirdDet.birdDet.eq_2 : ∀ {R : Type u_1} [inst : CommRing R] (A : Array R) (k : ℕ),
  BirdDet.birdDet k.succ A = (-1) ^ k * (BirdDet.stepEntry k.succ A)^[k] (BirdDet.get k.succ A) 0 0
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.locallyLinear : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (t : Finset (α × β × γ))
  [SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] [SimpleGraph.TripartiteFromTriangles.NoAccidental t],
  (SimpleGraph.TripartiteFromTriangles.graph t).LocallyLinear
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The cocone over the proposed colimit monoid.  -/
MonCat.FilteredColimits.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J MonCat) → [CategoryTheory.IsFiltered J] → CategoryTheory.Limits.Cocone F
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.AddContent.supClosure_apply_finpartition : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] (hC : MeasureTheory.IsSetSemiring C)
  (m : MeasureTheory.AddContent G C) {s : Set α} {J : Finpartition s},
  ↑J.parts ⊆ C → (m.supClosure hC) s = ∑ s ∈ J.parts, m s
-- Mathlib.Topology.Path
Filter.Tendsto.pathExtend : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {l r : Y → X} {y : Y}
  {l₁ : Filter ℝ} {l₂ : Filter X} {γ : (y : Y) → Path (l y) (r y)},
  Filter.Tendsto (↿γ) (nhds y ×ˢ Filter.map (Set.projIcc 0 1 ⋯) l₁) l₂ →
    Filter.Tendsto (↿fun x => ⇑(γ x).extend) (nhds y ×ˢ l₁) l₂
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.integralSum_neg : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} (f : (ι → ℝ) → E)
  (vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤) (π : BoxIntegral.TaggedPrepartition I),
  BoxIntegral.integralSum (-f) vol π = -BoxIntegral.integralSum f vol π
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_add_left : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Add β]
  [MeasurableAdd₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.Kernel.IndepFun (f i + f j) (f k) κ μ
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.fromEdgeSet_iUnion : ∀ {V : Type u} {ι : Sort u_2} {f : ι → Set (Sym2 V)},
  SimpleGraph.fromEdgeSet (⋃ i, f i) = ⨆ i, SimpleGraph.fromEdgeSet (f i)
-- Mathlib.GroupTheory.Nilpotent
Group.IsVirtuallyNilpotent.eq_1 : ∀ (G : Type u_1) [inst : Group G], Group.IsVirtuallyNilpotent G = ∃ N, Group.IsNilpotent ↥N ∧ N.FiniteIndex
-- Mathlib.Data.Finset.Max
/-- Induction principle for `Finset`s in any type from which a given function `f` maps to a linearly
ordered type : a predicate is true on all `s : Finset α` provided that:

* it is true on the empty `Finset`,
* for every `s : Finset α` and an element `a` such that for elements of `s` denoted by `x` we have
  `f x ≤ f a`, `p s` implies `p (insert a s)`.  -/
Finset.induction_on_max_value : ∀ {α : Type u_2} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : DecidableEq ι] (f : ι → α) {motive : Finset ι → Prop}
  (s : Finset ι),
  motive ∅ → (∀ (a : ι) (s : Finset ι), a ∉ s → (∀ x ∈ s, f x ≤ f a) → motive s → motive (insert a s)) → motive s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.Extremal
Polynomial.Chebyshev.node_mem_Icc : ∀ {n i : ℕ}, Polynomial.Chebyshev.node n i ∈ Set.Icc (-1) 1
-- Mathlib.FieldTheory.IsPerfectClosure
PerfectRing.liftAux.congr_simp : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommSemiring K] [inst_1 : CommSemiring L]
  [inst_2 : CommSemiring M] (i i_1 : K →+* L) (e_i : i = i_1) (j j_1 : K →+* M),
  j = j_1 →
    ∀ (p p_1 : ℕ) (e_p : p = p_1) [inst_3 : ExpChar M p] [inst_4 : PerfectRing M p] [inst_5 : IsPRadical i p]
      (x x_1 : L), x = x_1 → PerfectRing.liftAux i j p x = PerfectRing.liftAux i_1 j_1 p_1 x_1
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- If `A` is an `R`-algebra, any `R`-submodule `p` of an `R`-module `M` may be pushed forward to
an `A`-submodule of `A ⊗ M`.

This "base change" operation is also known as "extension of scalars".  -/
Submodule.baseChange : {R : Type u_1} →
  {M : Type u_2} →
    (A : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] → [inst_4 : Module R M] → Submodule R M → Submodule A (TensorProduct R A M)
-- Mathlib.Order.Antisymmetrization
Quotient.map'.congr_simp : ∀ {α : Sort u_1} {β : Sort u_2} {s₁ : Setoid α} {s₂ : Setoid β} (f f_1 : α → β) (e_f : f = f_1)
  (h : ∀ (a b : α), s₁ a b → s₂ (f a) (f b)) (a a_1 : Quotient s₁),
  a = a_1 → Quotient.map' f h a = Quotient.map' f_1 ⋯ a_1
-- Init.Data.UInt.Lemmas
USize.ofNat_finVal : ∀ (n : Fin USize.size), USize.ofNat ↑n = USize.ofFin n
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.isExtern : Lean.IR.Decl → Bool
-- Mathlib.CategoryTheory.PathCategory.Basic
CategoryTheory.Paths.categoryPaths : (V : Type u₁) → [Quiver V] → CategoryTheory.Category.{max u₁ v₁, u₁} (CategoryTheory.Paths V)
-- Init.Data.UInt.Lemmas
UInt32.ofFin_lt_iff_lt : ∀ {a b : Fin UInt32.size}, UInt32.ofFin a < UInt32.ofFin b ↔ a < b
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.opEquiv_symm_apply : ∀ {G : Type u_2} [inst : Group G] (H : Subgroup Gᵐᵒᵖ), (RelIso.symm Subgroup.opEquiv) H = H.unop
-- Std.Data.TreeMap.Raw.Basic
/-- Transforms a list of mappings into a tree map.  -/
Std.TreeMap.Raw.ofArray : {α : Type u} →
  {β : Type v} →
    Array (α × β) → (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.ofArray._auto_1) → Std.TreeMap.Raw α β cmp
-- Lean.Compiler.ExternAttr
Lean.ExternAttrData.mk : List Lean.ExternEntry → Lean.ExternAttrData
-- Mathlib.Algebra.Group.Prod
Prod.instCommGroup.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : CommGroup G] [inst_1 : CommGroup H],
  Prod.instCommGroup = { toGroup := Prod.instGroup, mul_comm := ⋯ }
-- Lean.Meta.Instances
Lean.Meta.instInhabitedDefaultInstances.default : Lean.Meta.DefaultInstances
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.toPreOneHypercover_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] (x x_1 : E.I₀) (x_2 : PUnit.{u_2 + 1}),
  E.toPreOneHypercover.p₁ x_2 = CategoryTheory.Limits.pullback.fst (E.f x) (E.f x_1)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.sum_zero : ∀ {R : Type u_1} [inst : Semiring R] {N : Type u_5} [inst_1 : AddCommMonoid N] {f : SkewPolynomial R},
  (f.sum fun x x_1 => 0) = 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {a fallback : α}, a ∉ t → t.getKeyD a fallback = fallback
-- Mathlib.GroupTheory.NoncommCoprod
/-- Variant of `MulHom.noncommCoprod_apply` with the product written in the other direction.  -/
MulHom.noncommCoprod_apply' : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Semigroup P] (f : M →ₙ* P)
  (g : N →ₙ* P) (comm : ∀ (m : M) (n : N), Commute (f m) (g n)) (mn : M × N),
  (f.noncommCoprod g comm) mn = g mn.2 * f mn.1
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.GetLsbD
Std.Tactic.BVDecide.BVPred.blastGetLsbD : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → Std.Tactic.BVDecide.BVPred.GetLsbDTarget aig → aig.Ref
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.codExtend'_baseSet : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {s : Set B}
  (hs : IsOpen s) {proj : Z → ↑s} (e : Bundle.Pretrivialization F proj) [inst_2 : Nonempty (B → F → Z)],
  (Bundle.Pretrivialization.codExtend' hs e).baseSet = Subtype.val '' e.baseSet
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- When the second map `S.g` is zero, this is the right homology data on `S` given
by any colimit cokernel cofork of `S.g`  -/
CategoryTheory.ShortComplex.RightHomologyData.ofIsColimitCokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        S.g = 0 →
          (c : CategoryTheory.Limits.CokernelCofork S.f) → CategoryTheory.Limits.IsColimit c → S.RightHomologyData
-- Lean.Meta.Tactic.Grind.EMatch
/-- Constraints to be processed.  -/
Lean.Meta.Grind.EMatch.Choice.cnstrs : Lean.Meta.Grind.EMatch.Choice → List Lean.Meta.Grind.EMatch.Cnstr
-- Lean.Elab.PatternVar
Lean.Elab.Term.CollectPatternVars.State.mk : Lean.NameSet → Array Lean.Elab.Term.PatternVar → Lean.Elab.Term.CollectPatternVars.State
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- When both maps `S.f` and `S.g` of a short complex `S` are zero, this is the homology map
data (for the identity of `S`) which relates the homology data
`HomologyData.ofIsLimitKernelFork` and `ofZeros` .  -/
CategoryTheory.ShortComplex.HomologyMapData.compatibilityOfZerosOfIsLimitKernelFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} →
        (hf : S.f = 0) →
          (hg : S.g = 0) →
            (c : CategoryTheory.Limits.KernelFork S.g) →
              (hc : CategoryTheory.Limits.IsLimit c) →
                CategoryTheory.ShortComplex.HomologyMapData (CategoryTheory.CategoryStruct.id S)
                  (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S hf c hc)
                  (CategoryTheory.ShortComplex.HomologyData.ofZeros S hf hg)
-- Init.Data.String.Basic
/-- Constructs a valid position on `s` from a position and a proof that it is valid.  -/
String.pos : (s : String) → (off : String.Pos.Raw) → String.Pos.Raw.IsValid s off → s.Pos
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isEmpty_inter_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t₁.isEmpty = true → (t₁ ∩ t₂).isEmpty = true
-- Mathlib.CategoryTheory.Sites.CoproductSheafCondition
Equiv.sigmaPUnit.eq_1 : ∀ (α : Type u_9),
  Equiv.sigmaPUnit α = { toFun := fun p => p.fst, invFun := fun a => ⟨a, PUnit.unit⟩, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₃Toδ₂_app_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₂₃ : i₁ ⟶ i₃) (f₃₄ : i₂ ⟶ i₄) (h₂₃ : CategoryTheory.CategoryStruct.comp f₂ f₃ = f₂₃)
  (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄),
  (CategoryTheory.ComposableArrows.fourδ₃Toδ₂ f₁ f₂ f₃ f₄ f₂₃ f₃₄ h₂₃ h₃₄).app 0 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃₄).obj 0)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Consumer.normal.injEq : ∀ {α : Type} (promise promise_1 : IO.Promise (Option α)),
  (Std.CloseableChannel.Consumer.normal✝ promise = Std.CloseableChannel.Consumer.normal✝ promise_1) =
    (promise = promise_1)
-- Mathlib.Analysis.ODE.Transform
IsIntegralCurveAt.comp_add : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E} {t₀ : ℝ},
  IsIntegralCurveAt γ v t₀ → ∀ (dt : ℝ), IsIntegralCurveAt (γ ∘ fun x => x + dt) (v ∘ fun x => x + dt) (t₀ - dt)
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegralFun_segment : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : NormedSpace ℝ E]
  (ω : E → E →L[𝕜] F) (a b : E) {t : ℝ},
  t ∈ unitInterval → curveIntegralFun ω (Path.segment a b) t = (ω ((AffineMap.lineMap a b) t)) (b - a)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_filter_le_size : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {f : α → β → Bool}, t.WF → (Std.TreeMap.Raw.filter f t).size ≤ t.size
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map.congr_simp : ∀ {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] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ φ_1 : W.LeftFraction X Y),
  φ = φ_1 → ∀ (L : CategoryTheory.Functor C D) (hL : W.IsInvertedBy L), φ.map L hL = φ_1.map L hL
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.fst_inr : ∀ (R : Type u) {M : Type v} [inst : Zero R] (m : M), (TrivSqZeroExt.inr m).fst = 0
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue!_eq_default : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Inhabited β] {l : List ((_ : α) × β)} {a : α},
  Std.Internal.List.containsKey a l = false → Std.Internal.List.getValue! a l = default
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.coe_eq_empty : ∀ {α : Type u_2} [inst : TopologicalSpace α] {U : TopologicalSpace.Opens α}, ↑U = ∅ ↔ U = ⊥
-- Init.Data.Range.Polymorphic.Iterators
/-- Returns the elements of the given left-closed right-open range as an array in ascending order.
 -/
Std.Rco.toArray : {α : Type u} →
  [inst : LT α] →
    [DecidableLT α] →
      [inst_2 : Std.PRange.UpwardEnumerable α] →
        [Std.PRange.LawfulUpwardEnumerable α] → [Std.Rxo.IsAlwaysFinite α] → Std.Rco α → Array α
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instOne : {α : Type u_1} → {β : Type u_2} → [inst : MeasurableSpace α] → [One β] → One (MeasureTheory.SimpleFunc α β)
-- Mathlib.Topology.Algebra.Valued.ValuationTopology
/-- A valued ring is a ring that comes equipped with a distinguished valuation. The class `Valued`
is designed for the situation that there is a canonical valuation on the ring.

TODO: show that there always exists an equivalent valuation taking values in a type belonging to
the same universe as the ring.

See Note [forgetful inheritance] for why we extend `UniformSpace`, `IsUniformAddGroup`.  -/
Valued : (R : Type u) → [Ring R] → (Γ₀ : outParam (Type v)) → [LinearOrderedCommGroupWithZero Γ₀] → Type (max u v)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.postcompLM.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {F' : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : SMulCommClass ℝ 𝕜 F] [inst_7 : NormedAddCommGroup F'] [inst_8 : NormedSpace ℝ F']
  [inst_9 : NormedSpace 𝕜 F'] [inst_10 : SMulCommClass ℝ 𝕜 F'] {n : ℕ∞} {K : TopologicalSpace.Compacts E}
  [inst_11 : LinearMap.CompatibleSMul F F' ℝ 𝕜] (T T_1 : F →L[𝕜] F'),
  T = T_1 → ContDiffMapSupportedIn.postcompLM T = ContDiffMapSupportedIn.postcompLM T_1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Basic
Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow.eq_def : ∀ (basis : Tactic.ComputeAsymptotics.Basis) (n : ℕ) (r : ℝ),
  Tactic.ComputeAsymptotics.MultiseriesExpansion.monomialRpow basis n r =
    match basis with
    | [] => default
    | basis_hd :: basis_tl =>
      Tactic.ComputeAsymptotics.MultiseriesExpansion.mk
        (Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.monomialRpow basis_hd basis_tl n r)
        ((basis_hd :: basis_tl)[n]! ^ r)
-- Mathlib.Analysis.Normed.Group.Real
Real.normedAddCommGroup : NormedAddCommGroup ℝ
-- Mathlib.Tactic.Positivity.Core
/-- Attempts to prove a `Strictness` result when `e` evaluates to a literal number.  -/
Mathlib.Meta.Positivity.normNumPositivity : {u : Lean.Level} →
  {α : Q(Type u)} →
    (zα : Q(Zero «$α»)) →
      (pα : Q(PartialOrder «$α»)) → (e : Q(«$α»)) → Lean.MetaM (Mathlib.Meta.Positivity.Strictness zα e (some pα))
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.SavedState.mk : Lean.Meta.SavedState → Lean.Elab.Term.State → Lean.Elab.Term.SavedState
-- Init.SimpLemmas
instIdempotentOpBoolAnd : Std.IdempotentOp fun x1 x2 => x1 && x2
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.id_mapId : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (a : B),
  (CategoryTheory.StrictlyUnitaryLaxFunctor.id B).mapId a =
    CategoryTheory.CategoryStruct.id (CategoryTheory.CategoryStruct.id a)
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- Auxiliary definition for differentials for `ChainComplex.of`.  -/
ChainComplex.of.d : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [CategoryTheory.Limits.HasZeroMorphisms V] →
      {α : Type u_2} →
        [inst_2 : AddRightCancelSemigroup α] →
          [inst_3 : One α] → [DecidableEq α] → (X : α → V) → ((n : α) → X (n + 1) ⟶ X n) → (i j : α) → X i ⟶ X j
-- Mathlib.Algebra.Homology.CochainComplexPlus
CochainComplex.Plus.instIsStableUnderRetractsQuasiIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.CategoryWithHomology C], (CochainComplex.Plus.quasiIso C).IsStableUnderRetracts
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Stepwise.d_step1C : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.CommRing α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (k : ℤ) (init p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon)
  (p₂ p : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Stepwise.d_step1_certC p₁ k₂ m₂ p₂ p c = true →
    ↑k * Lean.Grind.CommRing.Poly.denote ctx init = Lean.Grind.CommRing.Poly.denote ctx p₁ →
      Lean.Grind.CommRing.Poly.denote ctx p₂ = 0 →
        ↑k * Lean.Grind.CommRing.Poly.denote ctx init = Lean.Grind.CommRing.Poly.denote ctx p
-- Mathlib.FieldTheory.Normal.Defs
AlgHom.restrictNormal_commutes : ∀ {F : Type u_1} [inst : Field F] {K₁ : Type u_3} {K₂ : Type u_4} [inst_1 : Field K₁] [inst_2 : Field K₂]
  [inst_3 : Algebra F K₁] [inst_4 : Algebra F K₂] (ϕ : K₁ →ₐ[F] K₂) (E : Type u_6) [inst_5 : Field E]
  [inst_6 : Algebra F E] [inst_7 : Algebra E K₁] [inst_8 : Algebra E K₂] [inst_9 : IsScalarTower F E K₁]
  [inst_10 : IsScalarTower F E K₂] [inst_11 : Normal F E] (x : E),
  (algebraMap E K₂) ((ϕ.restrictNormal E) x) = ϕ ((algebraMap E K₁) x)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_one_right_eq_X_pow : ∀ {R : Type u} [inst : Semiring R] (n : ℕ), (Polynomial.monomial n) 1 = Polynomial.X ^ n
-- Mathlib.Tactic.Linter.UnusedInstancesInType
/-- Collects free variables that do not appear in proofs. Ignores `sorry`s (and their types).  -/
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.collectFVarsOutsideOfProofs : Lean.Expr → StateRefT' IO.RealWorld Lean.FVarIdSet Lean.MetaM Unit
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor_map_f : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) (X₂ : C₂)
  {X Y : (Φ.LeftResolution X₂)ᵒᵖ} (φ : X ⟶ Y),
  ((CategoryTheory.LocalizerMorphism.LeftResolution.opFunctor Φ X₂).map φ).f = φ.unop.f.op