mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sync.Barrier
_private.Std.Sync.Barrier.0.Std.BarrierState.mk.sizeOf_spec : ∀ (count generationId : ℕ),
  sizeOf { count := count, generationId := generationId } = 1 + sizeOf count + sizeOf generationId
-- Mathlib.Order.Filter.Bases.Basic
Filter.HasBasis.ker : ∀ {α : Type u_1} {ι : Sort u_4} {l : Filter α} {p : ι → Prop} {s : ι → Set α},
  l.HasBasis p s → l.ker = ⋂ i, ⋂ (_ : p i), s i
-- Mathlib.Analysis.Complex.MeanValue
/-- The **Generalized Mean Value Property** of complex differentiable functions: If `f : ℂ → E` is
continuous on a closed disc of radius `R` and center `c`, and is complex differentiable at all but
countably many points of its interior, then for every point `w` in the disk, the circle average
`circleAverage (fun z ↦ ((z - c) * (z - w)⁻¹) • f z) c R` equals `f w`.
 -/
circleAverage_sub_sub_inv_smul_of_differentiable_on_off_countable : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E} {R : ℝ}
  {c w : ℂ} {s : Set ℂ},
  s.Countable →
    ContinuousOn f (Metric.closedBall c |R|) →
      (∀ z ∈ Metric.ball c |R| \ s, DifferentiableAt ℂ f z) →
        w ∈ Metric.ball c |R| → Real.circleAverage (fun z => ((z - c) / (z - w)) • f z) c R = f w
-- Mathlib.Data.QPF.Multivariate.Basic
/-- A qpf is said to be uniform if every polynomial functor
representing a single value all have the same range.  -/
MvQPF.IsUniform : {n : ℕ} → {F : TypeVec.{u} n → Type u_1} → [q : MvQPF F] → Prop
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.mkCustomEliminator : Lean.Name → Bool → Lean.MetaM Lean.Meta.CustomEliminator
-- Mathlib.Data.UInt
UInt32.toFin_injective : Function.Injective UInt32.toFin
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKey_alter_eq_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  {f : Option β → Option β} {he : (t.alter k f).isEmpty = false},
  (t.alter k f).minKey he = k ↔ (f t[k]?).isSome = true ∧ ∀ k' ∈ t, (cmp k k').isLE = true
-- Mathlib.MeasureTheory.OuterMeasure.BorelCantelli
/-- A version of the **Borel-Cantelli lemma**: if `sᵢ` is a sequence of sets such that
`∑' i, μ sᵢ` is finite, then for almost all `x`, `x` does not belong to `sᵢ` for large `i`.  -/
MeasureTheory.ae_eventually_notMem : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [inst_1 : MeasureTheory.OuterMeasureClass F α]
  {μ : F} {s : ℕ → Set α}, ∑' (i : ℕ), μ (s i) ≠ ⊤ → ∀ᵐ (x : α) ∂μ, ∀ᶠ (n : ℕ) in Filter.atTop, x ∉ s n
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionParams.mk.sizeOf_spec : ∀ (toTextDocumentPositionParams : Lean.Lsp.TextDocumentPositionParams),
  sizeOf { toTextDocumentPositionParams := toTextDocumentPositionParams } = 1 + sizeOf toTextDocumentPositionParams
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Equalizers
/-- Any functor preserves coequalizers of split pairs.  -/
CategoryTheory.Limits.preservesSplitCoequalizers : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {X Y : C} (f g : X ⟶ Y) [CategoryTheory.HasSplitCoequalizer f g],
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair f g) G
-- Lean.Meta.Tactic.Grind.Util
/-- Normalizes the given expression using the `grind` simplification theorems and simprocs.
This function is used for normalizing E-matching patterns. Note that it does not return a proof.
 -/
Lean.Meta.Grind.normalize : Lean.Expr → Lean.Grind.Config → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.Jacobson.Ideal
Ideal.isRadical_jacobson : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R), I.jacobson.IsRadical
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.instLT : {A : Type u_1} → [inst : CommSemiring A] → {I : Ideal A} → {hI : DividedPowers I} → LT hI.SubDPIdeal
-- Init.MetaTypes
/-- If `ground` is `true` (default: `false`), then ground terms are reduced.
A term is ground when it does not contain free or meta variables.
Reduction is interrupted at a function application `f ...` if `f` is marked to not be unfolded.
Ground term reduction applies `@[seval]` lemmas.
 -/
Lean.Meta.Simp.Config.ground : Lean.Meta.Simp.Config → Bool
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
IsLocalDiffeomorphAt.localInverse_left_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (hf : IsLocalDiffeomorphAt I J n f x) {x' : M},
  x' ∈ hf.localInverse.target → ↑hf.localInverse.toPartialEquiv (f x') = x'
-- Mathlib.Algebra.Group.TypeTags.Basic
instZeroAdditiveOfOne : {α : Type u} → [One α] → Zero (Additive α)
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
/-- A function is `AEFinStronglyMeasurable` with respect to a measure if it is almost everywhere
equal to the limit of a sequence of simple functions with support with finite measure.  -/
MeasureTheory.AEFinStronglyMeasurable : {α : Type u_1} →
  {β : Type u_2} →
    [TopologicalSpace β] →
      [Zero β] →
        {x : MeasurableSpace α} →
          (α → β) → autoParam (MeasureTheory.Measure α) MeasureTheory.AEFinStronglyMeasurable._auto_1 → Prop
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.cast_apply : ∀ {ι : Type u_9} {M : ι → Type u_10} [inst : (i : ι) → Mul (M i)] {i j : ι} (h : i = j) (a : M i),
  (MulEquiv.cast h) a = cast ⋯ a
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.pow_log_eq_self : ∀ {M : Type u_1} [inst : Monoid M] [inst_1 : DecidableEq M] {n : M} (p : ↥(Submonoid.powers n)),
  Submonoid.pow n (Submonoid.log p) = p
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.Unsafe.levelsEqualUpToIdsCore' : Lean.Level → Lean.Level → Aesop.EqualUpToIdsM Bool
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.instIsTorsionFree : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  {S : NonUnitalSubalgebra R A} [Module.IsTorsionFree R A], Module.IsTorsionFree R ↥S
-- Mathlib.Order.Filter.IsBounded
Filter.IsBounded.eq_1 : ∀ {α : Type u_1} (r : α → α → Prop) (f : Filter α), Filter.IsBounded r f = ∃ b, ∀ᶠ (x : α) in f, r x b
-- ProofWidgets.Data.Html
ProofWidgets.LayoutKind.inline.sizeOf_spec : sizeOf ProofWidgets.LayoutKind.inline = 1
-- Mathlib.RingTheory.Ideal.Operations
Ideal.subset_union : ∀ {R : Type u} [inst : Ring R] {I J K : Ideal R}, ↑I ⊆ ↑J ∪ ↑K ↔ I ≤ J ∨ I ≤ K
-- Mathlib.Algebra.Group.Subgroup.Basic
/-- `H` is fixed by all automorphisms  -/
AddSubgroup.Characteristic.fixed : ∀ {A : Type u_4} [inst : AddGroup A] {H : AddSubgroup A},
  H.Characteristic → ∀ (ϕ : A ≃+ A), AddSubgroup.comap ϕ.toAddMonoidHom H = H
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransformMorphism.ext_iff : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  {inst : CategoryTheory.Category.{v₁, u₁} A} {inst_1 : CategoryTheory.Category.{v₂, u₂} B}
  {inst_2 : CategoryTheory.Category.{v₃, u₃} C} {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  {inst_3 : CategoryTheory.Category.{v₄, u₄} A'} {inst_4 : CategoryTheory.Category.{v₅, u₅} B'}
  {inst_5 : CategoryTheory.Category.{v₆, u₆} C'} {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'}
  {x y : CategoryTheory.Limits.CatCospanTransformMorphism ψ ψ'},
  x = y ↔ x.left = y.left ∧ x.right = y.right ∧ x.base = y.base
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
instInhabitedFormalMultilinearSeries : (𝕜 : Type u_3) →
  (E : Type u_1) →
    (F : Type u_2) →
      [inst : Semiring 𝕜] →
        [inst_1 : AddCommMonoid E] →
          [inst_2 : Module 𝕜 E] →
            [inst_3 : TopologicalSpace E] →
              [inst_4 : ContinuousAdd E] →
                [inst_5 : ContinuousConstSMul 𝕜 E] →
                  [inst_6 : AddCommMonoid F] →
                    [inst_7 : Module 𝕜 F] →
                      [inst_8 : TopologicalSpace F] →
                        [inst_9 : ContinuousAdd F] →
                          [inst_10 : ContinuousConstSMul 𝕜 F] → Inhabited (FormalMultilinearSeries 𝕜 E F)
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.tsum_eval : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] {α : Type u_5}
  {p : α → E [⋀^ι]→L[𝕜] F} [T2Space F], Summable p → ∀ (m : ι → E), (∑' (a : α), p a) m = ∑' (a : α), (p a) m
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.isZero_cokernel_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [CategoryTheory.Epi f] [inst_3 : CategoryTheory.Limits.HasCokernel f],
  CategoryTheory.Limits.IsZero (CategoryTheory.Limits.cokernel f)
-- Mathlib.Tactic.Translate.Reorder
/-- `ArgReorder` represents a permutation of arguments in a translation.  -/
Mathlib.Tactic.Translate.ArgReorder : Type
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- The `n`-dimensional generalized loops based at `x` in a space `X` are
continuous functions `I^n → X` that sends the boundary to `x`.
We allow an arbitrary indexing type `N` in place of `Fin n` here.  -/
GenLoop : (N : Type u_1) → (X : Type u_2) → [inst : TopologicalSpace X] → X → Set C(N → ↑unitInterval, X)
-- Lean.Elab.App
/-- Try to synthesize metavariables are `instMVars` using type class resolution.
The ones that cannot be synthesized yet stay in the `instMVars` list.
Remark: we use this method
  - before trying to apply coercions to function,
  - before unifying the expected type.
 -/
Lean.Elab.Term.ElabAppArgs.trySynthesizeAppInstMVars : Lean.Elab.Term.ElabAppArgs.M Unit
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.one : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.End.invtSubmodule 1 = ⊤
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- A function is `C^(n + 1)` if and only if it is differentiable,
and its derivative (formulated in terms of `fderiv`) is `C^n`.  -/
contDiff_succ_iff_fderiv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞},
  ContDiff 𝕜 (n + 1) f ↔ Differentiable 𝕜 f ∧ (n = ⊤ → AnalyticOnNhd 𝕜 f Set.univ) ∧ ContDiff 𝕜 n (fderiv 𝕜 f)
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.exists_epiModSerre_comp_eq_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass] {X Y : C} (f : X ⟶ Y),
  (∃ X' s, ∃ (_ : P.epiModSerre s), CategoryTheory.CategoryStruct.comp s f = 0) ↔ P (CategoryTheory.Abelian.image f)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.norm_normAtAllPlaces : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.mixedSpace K),
  NumberField.mixedEmbedding.norm
      (NumberField.mixedEmbedding.mixedSpaceOfRealSpace (NumberField.mixedEmbedding.normAtAllPlaces x)) =
    NumberField.mixedEmbedding.norm x
-- Mathlib.Analysis.Seminorm
Seminorm.instOrderBot : {𝕜 : Type u_3} →
  {E : Type u_7} →
    [inst : SeminormedRing 𝕜] → [inst_1 : AddCommGroup E] → [inst_2 : Module 𝕜 E] → OrderBot (Seminorm 𝕜 E)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `signExtend` on `BitVec`s.  -/
BitVec.reduceSignExtend : Lean.Meta.Simp.DSimproc
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instOrderBot : {α : Type u_1} →
  {β : Type u_2} → [inst : MeasurableSpace α] → [inst_1 : LE β] → [OrderBot β] → OrderBot (MeasureTheory.SimpleFunc α β)
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.instBracket : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] →
              [inst_4 : LieAlgebra R L] → (ψ : L →ₗ⁅R⁆ LieDerivation R K K) → Bracket (K ⋊⁅ψ⁆ L) (K ⋊⁅ψ⁆ L)
-- Mathlib.Data.Complex.Basic
Complex.instField : Field ℂ
-- Mathlib.Computability.Reduce
OneOneEquiv.of_equiv : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {e : α ≃ β},
  e.Computable → ∀ {p : β → Prop}, OneOneEquiv (p ∘ ⇑e) p
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.directive.withFencePos : ℕ → (Lean.Position → Lean.Parser.ParserFn) → Lean.Parser.ParserFn
-- Mathlib.Analysis.CStarAlgebra.GelfandDuality
CommCStarAlgebra.nnnorm_sum_eq_sup : ∀ {A : Type u_1} [inst : NonUnitalCommCStarAlgebra A] {ι : Type u_2} {f : ι → A} (s : Finset ι),
  Pairwise (Function.onFun (fun x1 x2 => x1 * x2 = 0) f) → ‖∑ i ∈ s, f i‖₊ = s.sup fun x => ‖f x‖₊
-- Mathlib.Data.List.Infix
List.inits_append : ∀ {α : Type u_1} (s t : List α), (s ++ t).inits = s.inits ++ List.map (fun l => s ++ l) t.inits.tail
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.Any.decidable : {α : Type u_1} → {P : α → Prop} → (t : Ordnode α) → [DecidablePred P] → Decidable (Ordnode.Any P t)
-- Mathlib.Analysis.Convex.Deriv
StrictConcaveOn.leftDeriv_lt_slope : ∀ {S : Set ℝ} {f : ℝ → ℝ} {x y : ℝ},
  StrictConcaveOn ℝ S f →
    x ∈ S → y ∈ S → x < y → DifferentiableWithinAt ℝ f (Set.Iio y) y → derivWithin f (Set.Iio y) y < slope f x y
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.exact : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.mk L₁ = FreeGroup.mk L₂ ↔ Relation.Join FreeGroup.Red L₁ L₂
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.soIndefiniteEquiv.eq_1 : ∀ (p : Type u_2) (q : Type u_3) (R : Type u₂) [inst : DecidableEq p] [inst_1 : DecidableEq q] [inst_2 : CommRing R]
  [inst_3 : Fintype p] [inst_4 : Fintype q] {i : R} (hi : i * i = -1),
  LieAlgebra.Orthogonal.soIndefiniteEquiv p q R hi =
    (skewAdjointMatricesLieSubalgebraEquiv (LieAlgebra.Orthogonal.indefiniteDiagonal p q R)
          (LieAlgebra.Orthogonal.Pso p q R i) (LieAlgebra.Orthogonal.invertiblePso p q R hi)).trans
      (LieEquiv.ofEq
        (skewAdjointMatricesLieSubalgebra
          ((LieAlgebra.Orthogonal.Pso p q R i).transpose * LieAlgebra.Orthogonal.indefiniteDiagonal p q R *
            LieAlgebra.Orthogonal.Pso p q R i))
        (LieAlgebra.Orthogonal.so (p ⊕ q) R) ⋯)
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.and_congr : ∀ (w : ℕ) (lhs rhs lhs' rhs' : BitVec w), lhs' = lhs → rhs' = rhs → lhs' &&& rhs' = lhs &&& rhs
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.bmod_length : ∀ (x : Lean.Omega.Coeffs) (m : ℕ), (x.bmod m).length ≤ x.length
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.coe_toAffineMap : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), ⇑↑e = ⇑e
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.ext : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : Semiring 𝕜] [inst_1 : AddCommMonoid E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousConstSMul 𝕜 E] [inst_6 : AddCommMonoid F]
  [inst_7 : Module 𝕜 F] [inst_8 : TopologicalSpace F] [inst_9 : ContinuousAdd F] [inst_10 : ContinuousConstSMul 𝕜 F]
  {p q : FormalMultilinearSeries 𝕜 E F}, (∀ (n : ℕ), p n = q n) → p = q
-- Lean.Elab.DocString
/-- The state used by `DocM`.
 -/
Lean.Doc.State : Type
-- Init.Sym.Lemmas
Lean.Sym.Nat.le_eq_false : ∀ (a b : ℕ), decide (a ≤ b) = false → (a ≤ b) = False
-- Mathlib.Analysis.Normed.Algebra.Exponential
Filter.Tendsto.exp : ∀ {𝔸 : Type u_1} [inst : NormedRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] {α : Type u_3} {l : Filter α} {f : α → 𝔸}
  {a : 𝔸}, Filter.Tendsto f l (nhds a) → Filter.Tendsto (fun x => NormedSpace.exp (f x)) l (nhds (NormedSpace.exp a))
-- Mathlib.FieldTheory.Relrank
IntermediateField.relfinrank_top_right : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (A : IntermediateField F E),
  A.relfinrank ⊤ = Module.finrank (↥A) E
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.instTrans : {α : Type u} → {cmp : α → α → Ordering} → Trans Std.TreeSet.Equiv Std.TreeSet.Equiv Std.TreeSet.Equiv
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
/-- If `g` and `f` are `R`-linear graded algebra homomorphisms with the domain of `g` equal to
the codomain of `f`, then `g.comp f` is the graded algebra homomorphism `x ↦ g (f x)`.
 -/
GradedAlgHom.comp : {R : Type u_1} →
  {A : Type u_6} →
    {B : Type u_7} →
      {C : Type u_8} →
        {ι : Type u_10} →
          [inst : CommSemiring R] →
            [inst_1 : Semiring A] →
              [inst_2 : Semiring B] →
                [inst_3 : Semiring C] →
                  [inst_4 : Algebra R A] →
                    [inst_5 : Algebra R B] →
                      [inst_6 : Algebra R C] →
                        [inst_7 : DecidableEq ι] →
                          [inst_8 : AddMonoid ι] →
                            {𝒜 : ι → Submodule R A} →
                              {ℬ : ι → Submodule R B} →
                                {𝒞 : ι → Submodule R C} →
                                  [inst_9 : GradedAlgebra 𝒜] →
                                    [inst_10 : GradedAlgebra ℬ] →
                                      [inst_11 : GradedAlgebra 𝒞] → (ℬ →ₐᵍ[R] 𝒞) → (𝒜 →ₐᵍ[R] ℬ) → 𝒜 →ₐᵍ[R] 𝒞
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_of_add_le_of_nonneg_left : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : Preorder α] [AddLeftMono α] {a b c : α}, a + b ≤ c → 0 ≤ b → a ≤ c
-- Mathlib.MeasureTheory.Measure.Map
MeasurableEquiv.map_symm_map : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  (e : α ≃ᵐ β), MeasureTheory.Measure.map (⇑e.symm) (MeasureTheory.Measure.map (⇑e) μ) = μ
-- Mathlib.MeasureTheory.Measure.Content
MeasureTheory.Content.outerMeasure_opens : ∀ {G : Type w} [inst : TopologicalSpace G] (μ : MeasureTheory.Content G) [R1Space G] (U : TopologicalSpace.Opens G),
  μ.outerMeasure ↑U = μ.innerContent U
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.instHomotopyLike : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)},
  ContinuousMap.HomotopyLike (f₀.Homotopy f₁) f₀ f₁
-- Mathlib.Algebra.BigOperators.Finprod
/-- Note that `b ∈ (s.filter (fun ab => Prod.fst ab = a)).image Prod.snd` iff `(a, b) ∈ s` so
we can simplify the right-hand side of this lemma. However the form stated here is more
useful for iterating this lemma, e.g., if we have `f : α × β × γ → M`.  -/
finsum_mem_finset_product' : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : DecidableEq α]
  [inst_2 : DecidableEq β] (s : Finset (α × β)) (f : α × β → M),
  ∑ᶠ (ab : α × β) (_ : ab ∈ s), f ab =
    ∑ᶠ (a : α) (b : β) (_ : b ∈ Finset.image Prod.snd ({ab ∈ s | ab.1 = a})), f (a, b)
-- Mathlib.FieldTheory.SeparablyGenerated
/-- View a multivariate polynomial `F(x₁,...,xₙ)` as a polynomial in `xᵢ` with coefficients
in `F(x₁,...,xᵢ₋₁,xᵢ₊₁,...,xₙ)`.  -/
MvPolynomial.toPolynomialAdjoinImageCompl : {k : Type u_1} →
  {K : Type u_2} →
    {ι : Type u_3} →
      [inst : Field k] →
        [inst_1 : Field K] →
          [inst_2 : Algebra k K] → MvPolynomial ι k → (a : ι → K) → (i : ι) → Polynomial ↥(Algebra.adjoin k (a '' {i}ᶜ))
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
Mathlib.Tactic.BicategoryLike.HorizontalComp.of : Mathlib.Tactic.BicategoryLike.WhiskerRight → Mathlib.Tactic.BicategoryLike.HorizontalComp
-- Mathlib.Data.Sum.Interval
Sum.Lex.Icc_inr_inr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (b₁ b₂ : β),
  Finset.Icc (Sum.inrₗ b₁) (Sum.inrₗ b₂) =
    Finset.map (Function.Embedding.inr.trans toLex.toEmbedding) (Finset.Icc b₁ b₂)
-- Init.Data.BitVec.Lemmas
BitVec.neg_eq_neg_one_mul : ∀ {w : ℕ} (b : BitVec w), -b = -1#w * b
-- Mathlib.Combinatorics.Young.SemistandardTableau
/-- The entries in each row are weakly increasing (left to right).  -/
SemistandardYoungTableau.row_weak' : ∀ {μ : YoungDiagram} (self : SemistandardYoungTableau μ) {i j1 j2 : ℕ},
  j1 < j2 → (i, j2) ∈ μ → self.entry i j1 ≤ self.entry i j2
-- Mathlib.Data.Finset.Prod
Finset.filter_product : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β} (p : α → Prop) (q : β → Prop) [inst : DecidablePred p]
  [inst_1 : DecidablePred q], {x ∈ s ×ˢ t | p x.1 ∧ q x.2} = Finset.filter p s ×ˢ Finset.filter q t
-- Plausible.DeriveArbitrary
/-- Creates a `mutual ... end` block containing the definitions of the derived generators  -/
_private.Plausible.DeriveArbitrary.0.Plausible.mkMutualBlock : Lean.Elab.Deriving.Context → Lean.Elab.TermElabM Lean.Syntax
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.Eigenvalues.val_mk : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} (h : f.HasEigenvalue μ), ↑f ⟨μ, h⟩ = μ
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.toList_rii : ∀ {α : Type u} (t : Std.DTreeMap.Internal.Impl α fun x => Unit),
  Std.Slice.toList (Std.Rii.Sliceable.mkSlice t *...*) = t.keys
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Hom.mk : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {l : a ⟶ b} → {r : b ⟶ a} → CategoryTheory.Bicategory.Adjunction l r → CategoryTheory.Bicategory.Adj.Hom a b
-- Mathlib.Analysis.Convex.Hull
convexHull_vadd : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] (x : E) (s : Set E), (convexHull 𝕜) (x +ᵥ s) = x +ᵥ (convexHull 𝕜) s
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
Valuation.one_vlt_iff : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_2} [inst_2 : LinearOrderedCommMonoidWithZero Γ₀]
  (v : Valuation R Γ₀) [v.Compatible] {x : R}, 1 <ᵥ x ↔ 1 < v x
-- Lean.Data.AssocList
Lean.AssocList.foldlM : {α : Type u} →
  {β : Type v} → {δ : Type w} → {m : Type w → Type w'} → [Monad m] → (δ → α → β → m δ) → δ → Lean.AssocList α β → m δ
-- Mathlib.Util.AtomM
Mathlib.Tactic.AtomM.instInhabitedContext.default : Mathlib.Tactic.AtomM.Context
-- Mathlib.CategoryTheory.Sites.CoverLifting
CategoryTheory.Functor.IsCocontinuous.of_iso : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {J : CategoryTheory.GrothendieckTopology C}
  {K : CategoryTheory.GrothendieckTopology D} {F G : CategoryTheory.Functor C D} (e : F ≅ G) [F.IsCocontinuous J K],
  G.IsCocontinuous J K
-- Init.Data.SInt.Bitwise
Int16.not_xor : ∀ {a b : Int16}, ~~~a ^^^ b = ~~~(a ^^^ b)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.mk_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {Y : C} {T : CategoryTheory.Functor C D} (f : S ⟶ T.obj Y),
  (CategoryTheory.StructuredArrow.mk f).left = { as := PUnit.unit }