mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.AlgebraicIndependent.Defs
/-- Canonical isomorphism between polynomials and the subalgebra generated by
algebraically independent elements.
`AlgebraicIndepOn` version of `AlgebraicIndependent.aevalEquiv`.  -/
AlgebraicIndepOn.aevalEquiv : {ι : Type u_1} →
  {R : Type u_3} →
    {A : Type u_5} →
      {x : ι → A} →
        [inst : CommRing R] →
          [inst_1 : CommRing A] →
            [inst_2 : Algebra R A] →
              {s : Set ι} → AlgebraicIndepOn R x s → MvPolynomial (↑s) R ≃ₐ[R] ↥(Algebra.adjoin R (x '' s))
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
AlgebraicGeometry.Proj.pow_apply : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] {V : (TopologicalSpace.Opens ↑(ProjectiveSpectrum.top 𝒜))ᵒᵖ}
  (s : ↑((AlgebraicGeometry.ProjectiveSpectrum.Proj.structureSheaf 𝒜).obj.obj V)) (x : ↥(Opposite.unop V)) (n : ℕ),
  ↑(s ^ n) x = ↑s x ^ n
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.isBigO_atTop_F_nat_zero_sub : ∀ {a : ℝ},
  0 ≤ a →
    ∃ p,
      0 < p ∧
        (fun t => HurwitzKernelBounds.F_nat 0 a t - if a = 0 then 1 else 0) =O[Filter.atTop] fun t => Real.exp (-p * t)
-- Mathlib.Order.Fin.Basic
Fin.natAddOrderEmb_toEmbedding : ∀ {m : ℕ} (n : ℕ), (Fin.natAddOrderEmb n).toEmbedding = { toFun := Fin.natAdd n, inj' := ⋯ }
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- `AddMonoidAlgebra.single m r` is injective in `m` if `r ≠ 0`. For injectivity in `r`, see
`AddMonoidAlgebra.single_injective`. -/
AddMonoidAlgebra.single_left_injective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {r : R},
  r ≠ 0 → Function.Injective fun m => AddMonoidAlgebra.single m r
-- Mathlib.SetTheory.Ordinal.Principal
/-- We give an explicit construction for a principal ordinal larger or equal than `o`.  -/
_private.Mathlib.SetTheory.Ordinal.Principal.0.Ordinal.isPrincipal_nfp_iSup : ∀ (op : Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}) (o : Ordinal.{u_1}),
  Ordinal.IsPrincipal op (Ordinal.nfp (fun x => ⨆ y, Order.succ (op (↑y).1 (↑y).2)) o)
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `(η ◫ ηs) ▷ f`  -/
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight.mkEvalWhiskerRightAuxCons : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerRight m] →
    Mathlib.Tactic.BicategoryLike.Atom₁ →
      Mathlib.Tactic.BicategoryLike.WhiskerRight →
        Mathlib.Tactic.BicategoryLike.HorizontalComp →
          Mathlib.Tactic.BicategoryLike.NormalExpr →
            Mathlib.Tactic.BicategoryLike.NormalExpr →
              Mathlib.Tactic.BicategoryLike.NormalExpr →
                Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Order.Nucleus
Nucleus.map_himp_le : ∀ {X : Type u_1} [inst : Order.Frame X] {n : Nucleus X} {x y : X}, n (x ⇨ y) ≤ x ⇨ n y
-- Init.Data.SInt.Basic
/-- Decides whether two word-sized signed integers are equal. Usually accessed via the
`DecidableEq ISize` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `ISize.decEq 123 123 = .isTrue rfl`
 * `(if ((-7) : ISize) = 7 then "yes" else "no") = "no"`
 * `show (7 : ISize) = 7 by decide`
 -/
ISize.decEq : (a b : ISize) → Decidable (a = b)
-- Init.Data.Nat.Basic
Nat.zero_sub : ∀ (n : ℕ), 0 - n = 0
-- Init.Data.UInt.Lemmas
USize.sub_self : ∀ (a : USize), a - a = 0
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_add_eq' : ∀ {a : ℕ} (n : ℕ), a ≤ n + n → (n ^ 2 + a).sqrt = n
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.colimit.homIso_hom : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] {W : C},
  (CategoryTheory.Limits.colimit.homIso F W).hom =
    TypeCat.ofHom fun f =>
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.cocone F).ι
        ((CategoryTheory.Functor.const J).map f.down)
-- Mathlib.Algebra.Star.Free
/-- `star` as an `AlgEquiv`  -/
FreeAlgebra.starHom : {R : Type u_1} → [inst : CommSemiring R] → {X : Type u_2} → FreeAlgebra R X ≃ₐ[R] (FreeAlgebra R X)ᵐᵒᵖ
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- Given `SlashInvariantForm`'s `f i` of weight `k i` for `i : ι`, define the form which as a
function is a product of those indexed by `s : Finset ι` with weight `m = ∑ i ∈ s, k i`.  -/
SlashInvariantForm.prod : {ι : Type} →
  {s : Finset ι} →
    {k : ι → ℤ} →
      (m : ℤ) →
        m = ∑ i ∈ s, k i →
          {Γ : Subgroup (GL (Fin 2) ℝ)} →
            [Γ.HasDetPlusMinusOne] → ((i : ι) → SlashInvariantForm Γ (k i)) → SlashInvariantForm Γ m
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_cos_add_sin_mul_I_coe_angle : ∀ (θ : Real.Angle), ↑(↑θ.cos + ↑θ.sin * Complex.I).arg = θ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_of_mem_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α},
  k ∈ Std.ExtDHashMap.Const.insertMany m l → (List.map Prod.fst l).contains k = false → k ∈ m
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.vsub_subset_vsub_right : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] [inst_1 : DecidableEq α] {s₁ s₂ t : Finset β},
  s₁ ⊆ s₂ → s₁ -ᵥ t ⊆ s₂ -ᵥ t
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Ring.inverse_of_isUnit : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {x : M₀} (h : IsUnit x), Ring.inverse x = ↑h.unit⁻¹
-- Init.Data.Array.Subarray
Subarray.instSliceSizeSubarrayData : {α : Type u_1} → Std.Slice.SliceSize (Std.Slice.Internal.SubarrayData α)
-- Mathlib.Order.Filter.CountablyGenerated
/-- `IsCountablyGenerated f` means `f = generate s` for some countable `s`.  -/
Filter.IsCountablyGenerated : {α : Type u_1} → Filter α → Prop
-- Mathlib.MeasureTheory.Function.L1Space.AEEqFun
MeasureTheory.Integrable.toL1_smul : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  {𝕜 : Type u_5} [inst_1 : NormedRing 𝕜] [inst_2 : Module 𝕜 β] [inst_3 : IsBoundedSMul 𝕜 β] (f : α → β)
  (hf : MeasureTheory.Integrable f μ) (k : 𝕜),
  MeasureTheory.Integrable.toL1 (fun a => k • f a) ⋯ = k • MeasureTheory.Integrable.toL1 f hf
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
CurveIntegrable.sub : ∀ {𝕜 : 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] {a b : E}
  {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b}, CurveIntegrable ω₁ γ → CurveIntegrable ω₂ γ → CurveIntegrable (ω₁ - ω₂) γ
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dvdTight.injEq : ∀ (c₁ : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) (c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr)
  (c₁_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr) (c₂_1 : Lean.Meta.Grind.Arith.Cutsat.LeCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dvdTight c₁ c₂ =
      Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.dvdTight c₁_1 c₂_1) =
    (c₁ = c₁_1 ∧ c₂ = c₂_1)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instSubNegAddMonoid : {α : Type u_1} → [SubNegMonoid α] → SubNegMonoid (Colex α)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.rfl : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}, t.Equiv t
-- Lean.Server.Rpc.Basic
_private.Lean.Server.Rpc.Basic.0.Lean.Server.WithRpcRef.mk'.injEq : ∀ {α : Type u} (val : α) (id : USize) (val_1 : α) (id_1 : USize),
  ({ val := val, id := id } = { val := val_1, id := id_1 }) = (val = val_1 ∧ id = id_1)
-- Lean.Parser.Basic
/-- A multimap indexed by tokens. Used for indexing parsers by their leading token.  -/
Lean.Parser.TokenMap : Type → Type
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.nonCommRing.injEq : ∀ (id id_1 : ℕ),
  (Lean.Meta.Sym.Arith.ClassifyResult.nonCommRing id = Lean.Meta.Sym.Arith.ClassifyResult.nonCommRing id_1) =
    (id = id_1)
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.mk.sizeOf_spec : ∀ {S : Type u_2} {M : Type u_3} [inst : SMul S M] [inst_1 : SizeOf S] [inst_2 : SizeOf M] (toSetoid : Setoid M)
  (smul : ∀ (s : S) {x y : M}, toSetoid x y → toSetoid (s • x) (s • y)),
  sizeOf { toSetoid := toSetoid, smul := smul } = 1 + sizeOf toSetoid
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_sdiff_right' : ∀ {α : Type u} {x y z : α} [inst : GeneralizedBooleanAlgebra α], x \ (y \ z) = x \ y ⊔ x ⊓ z
-- Mathlib.Topology.Category.Profinite.Product
/-- `indexCone` is a limit cone.  -/
Profinite.indexCone_isLimit : {ι : Type u} →
  {X : ι → Type} →
    [inst : (i : ι) → TopologicalSpace (X i)] →
      {C : Set ((i : ι) → X i)} →
        [inst_1 : ∀ (i : ι), T2Space (X i)] →
          [inst_2 : ∀ (i : ι), TotallyDisconnectedSpace (X i)] →
            (hC : IsCompact C) → CategoryTheory.Limits.IsLimit (Profinite.indexCone hC)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_addNat_Ioi : ∀ {n : ℕ} (m : ℕ) (i : Fin n), (fun x => x.addNat m) '' Set.Ioi i = Set.Ioi (i.addNat m)
-- Mathlib.Algebra.Order.Ring.Synonym
Lex.instAddMonoidWithOne : {R : Type u_1} → [AddMonoidWithOne R] → AddMonoidWithOne (Lex R)
-- Mathlib.Data.ENNReal.Inv
ENNReal.instInvolutiveInv : InvolutiveInv ENNReal
-- Mathlib.Algebra.Category.BialgCat.Basic
BialgCat.Hom.mk : {R : Type u} → [inst : CommRing R] → {V W : BialgCat R} → (V.carrier →ₐc[R] W.carrier) → V.Hom W
-- Lean.Elab.DefView
Lean.Elab.instNonemptyDefsParsedSnapshot : Nonempty Lean.Elab.DefsParsedSnapshot
-- Lean.Meta.Tactic.Assert
Lean.Meta.AssertAfterResult.subst : Lean.Meta.AssertAfterResult → Lean.Meta.FVarSubst
-- Mathlib.GroupTheory.GroupAction.Pointwise
/-- General version of `preimage_smul_setₛₗ`.
This version assumes that the scalar multiplication by `c` is surjective
while the scalar multiplication by `σ c` is injective.  -/
preimage_smul_setₛₗ' : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [inst : SMul M α]
  [inst_1 : SMul N β] [inst_2 : FunLike F α β] [MulActionSemiHomClass F σ α β] {f : F} {t : Set β} {c : M},
  (Function.Surjective fun m => c • m) → (Function.Injective fun n => σ c • n) → ⇑f ⁻¹' (σ c • t) = c • ⇑f ⁻¹' t
-- Mathlib.Algebra.Order.Group.End
RelIso.coe_one : ∀ {α : Type u_1} {r : α → α → Prop}, ⇑1 = id
-- Mathlib.Algebra.Category.MonCat.Colimits
MonCat.Colimits.Prequotient.brecOn.go : {J : Type v} →
  [inst : CategoryTheory.Category.{u, v} J] →
    {F : CategoryTheory.Functor J MonCat} →
      {motive : MonCat.Colimits.Prequotient F → Sort u_1} →
        (t : MonCat.Colimits.Prequotient F) →
          ((t : MonCat.Colimits.Prequotient F) → MonCat.Colimits.Prequotient.below t → motive t) →
            motive t ×' MonCat.Colimits.Prequotient.below t
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- For a bounded set `s : Set ℝ`, its `Metric.diam` is equal to `sSup s - sInf s`.  -/
Real.diam_eq : ∀ {s : Set ℝ}, Bornology.IsBounded s → Metric.diam s = sSup s - sInf s
-- Mathlib.Algebra.Lie.Engel
/-- Engel's theorem.

See also `LieModule.isNilpotent_iff_forall'` which assumes that `M` is Noetherian instead of `L`.  -/
LieModule.isNilpotent_iff_forall : ∀ {R : Type u₁} {L : Type u₂} {M : Type u₄} [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]
  [IsNoetherian R L], LieModule.IsNilpotent L M ↔ ∀ (x : L), IsNilpotent ((LieModule.toEnd R L M) x)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.map_polynomialX : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Projective R) {S : Type s} [inst_1 : CommRing S]
  (f : R →+* S), (W'.map f).polynomialX = (MvPolynomial.map f) W'.polynomialX
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKey!_unitOfList_of_contains_eq_false : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] [inst_2 : Inhabited α]
  {l : List α} {k : α}, l.contains k = false → (Std.ExtHashMap.unitOfList l).getKey! k = default
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.subsingleton_iff : ∀ {R : Type u_1} [Semiring R], Subsingleton (PowerSeries R) ↔ Subsingleton R
-- Mathlib.Geometry.Group.Growth.LinearLowerBound
Finset.pow_right_strictMonoOn : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {X : Finset G},
  1 ∈ X → X.Nontrivial → StrictMonoOn (fun n => X ^ n) {n | ↑X ^ (n - 1) ≠ ↑(Subgroup.closure ↑X)}
-- Mathlib.GroupTheory.Solvable
Equiv.Perm.not_isSolvable_fin_5 : ¬Group.IsSolvable (Equiv.Perm (Fin 5))
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainBialgHom_id : ∀ {R : Type u_1} {M : Type u_8} [inst : CommSemiring R] [inst_1 : Monoid M],
  MonoidAlgebra.mapDomainBialgHom R (MonoidHom.id M) = BialgHom.id R (MonoidAlgebra R M)
-- Mathlib.Order.CompleteLattice.Basic
iSup_iSup_eq_right : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {b : β} {f : (x : β) → b = x → α},
  ⨆ x, ⨆ (h : b = x), f x h = f b ⋯
-- Mathlib.GroupTheory.OrderOfElement
orderOf_pow_dvd : ∀ {G : Type u_1} [inst : Monoid G] {x : G} (n : ℕ), orderOf (x ^ n) ∣ orderOf x
-- Init.Grind.ToInt
_private.Init.Grind.ToInt.0.Lean.Grind.instBEqIntInterval.beq_spec_2 : ∀ (a b : ℤ), (Lean.Grind.IntInterval.ci a == Lean.Grind.IntInterval.ci b) = (a == b)
-- Mathlib.RingTheory.Idempotents
OrthogonalIdempotents.unique : ∀ {R : Type u_1} [inst : Semiring R] {I : Type u_3} {e : I → R} [inst_1 : Unique I],
  OrthogonalIdempotents e ↔ IsIdempotentElem (e default)
-- Mathlib.Data.Set.Finite.Basic
Set.exists_subset_image_finite_and : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α} {p : Set β → Prop},
  (∃ t ⊆ f '' s, t.Finite ∧ p t) ↔ ∃ t ⊆ s, t.Finite ∧ p (f '' t)
-- Mathlib.Control.Functor
/-- If `f` is a functor, if `fb : f β` and `a : α`, then `mapConstRev fb a` is the result of
applying `f.map` to the constant function `β → α` sending everything to `a`, and then
evaluating at `fb`. In other words it's `const a <$> fb`.  -/
Functor.«term_$>_» : Lean.TrailingParserDescr
-- Mathlib.Topology.EMetricSpace.Diam
/-- **Alias** of `Metric.edist_le_of_ediam_le`. -/
EMetric.edist_le_of_diam_le : ∀ {X : Type u_2} {s : Set X} {x y : X} [inst : PseudoEMetricSpace X] {d : ENNReal},
  x ∈ s → y ∈ s → Metric.ediam s ≤ d → edist x y ≤ d
-- Mathlib.Data.Fin.SuccPred
Fin.val_sub_castLT_of_le : ∀ {n m : ℕ} {a b : Fin m} (ha : ↑a < n) (h : b ≤ a), ↑(a.castLT ha - b.castLT ⋯) = ↑(a - b)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.denoteAsIntModule_go_eq_denote : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (m : Lean.Grind.CommRing.Mon)
  (acc : α), Lean.Grind.CommRing.Mon.denoteAsIntModule.go ctx m acc = acc * Lean.Grind.CommRing.Mon.denote ctx m
-- Init.Data.Int.Pow
Int.zero_pow : ∀ {n : ℕ}, n ≠ 0 → 0 ^ n = 0
-- Lean.Server.Rpc.Basic
Lean.Server.freshWithRpcRefId : IO.Ref USize
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- `post (F ⋙ G)` is isomorphic (actually equal) to `post F ⋙ post G`.  -/
CategoryTheory.Under.postComp : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : T} →
          {E : Type u_1} →
            [inst_2 : CategoryTheory.Category.{v_1, u_1} E] →
              (F : CategoryTheory.Functor T D) →
                (G : CategoryTheory.Functor D E) →
                  CategoryTheory.Under.post (F.comp G) ≅
                    (CategoryTheory.Under.post F).comp (CategoryTheory.Under.post G)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constMaxEntry!_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)], t₁.Equiv t₂ → Std.DTreeMap.Const.maxEntry! t₁ = Std.DTreeMap.Const.maxEntry! t₂
-- Mathlib.Probability.Distributions.Gaussian.Basic
ProbabilityTheory.IsGaussian.map_eq_gaussianReal : ∀ {E : Type u_1} {inst : TopologicalSpace E} {inst_1 : AddCommMonoid E} {inst_2 : Module ℝ E} {mE : MeasurableSpace E}
  {μ : MeasureTheory.Measure E} [self : ProbabilityTheory.IsGaussian μ] (L : StrongDual ℝ E),
  MeasureTheory.Measure.map (⇑L) μ =
    ProbabilityTheory.gaussianReal (∫ (x : E), L x ∂μ) (ProbabilityTheory.variance (⇑L) μ).toNNReal
-- Mathlib.Tactic.ErwQuestion
/-- If set to `true`, `erw?` will log more information as it attempts to identify subexpressions
which would block the use of `rw` instead.
 -/
Mathlib.Tactic.Erw?.tactic.erw?.verbose : Lean.Option Bool
-- Init.Data.List.Attach
List.filter_attachWith : ∀ {α : Type u_1} {q : α → Prop} {l : List α} {p : { x // q x } → Bool} (H : ∀ x ∈ l, q x),
  List.filter p (l.attachWith q H) =
    List.map
      (fun x =>
        match x with
        | ⟨x, h⟩ => ⟨x, ⋯⟩)
      (List.filter
        (fun x =>
          match x with
          | ⟨x, h⟩ => p ⟨x, ⋯⟩)
        l.attach)
-- Mathlib.MeasureTheory.Group.Arithmetic
/-- We say that a type has `MeasurableMul₂` if `uncurry (· * ·)` is a measurable function.
For a typeclass assuming measurability of `(c * ·)` and `(· * c)` see `MeasurableMul`.  -/
MeasurableMul₂ : (M : Type u_2) → [MeasurableSpace M] → [Mul M] → Prop
-- Mathlib.Probability.Decision.Risk.Countable
ProbabilityTheory.avgRisk_fintype : ∀ {Θ : Type u_1} {𝓧 : Type u_3} {𝓨 : Type u_5} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} {P : ProbabilityTheory.Kernel Θ 𝓧} {κ : ProbabilityTheory.Kernel 𝓧 𝓨}
  {π : MeasureTheory.Measure Θ} [inst : Fintype Θ] [MeasurableSingletonClass Θ],
  ProbabilityTheory.avgRisk ℓ P κ π = ∑ θ, (∫⁻ (y : 𝓨), ℓ θ y ∂(κ.comp P) θ) * π {θ}
-- Mathlib.Algebra.Group.Fin.Basic
Fin.rev_add : ∀ {n : ℕ} (a b : Fin n), (a + b).rev = a.rev - b
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.ExtractMonadResult.returnType : Lean.Elab.Term.ExtractMonadResult → Lean.Expr
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.subtype_injective : ∀ {R : Type u} [inst : NonAssocRing R] (s : Subring R), Function.Injective ⇑s.subtype
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexLinearEquiv_apply : ∀ {m : Type u_2} {n : Type u_3} {m' : Type u_6} {n' : Type u_7} (R : Type u_11) (A : Type u_12) [inst : Semiring R]
  [inst_1 : AddCommMonoid A] [inst_2 : Module R A] (eₘ : m ≃ m') (eₙ : n ≃ n') (M : Matrix m n A),
  (Matrix.reindexLinearEquiv R A eₘ eₙ) M = (Matrix.reindex eₘ eₙ) M
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RooSliceData.mk.inj : ∀ {α : Type u} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit} {range : Std.Roo α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => Unit} {range_1 : Std.Roo α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Mathlib.Data.Finset.NatAntidiagonal
Finset.Nat.antidiagonal.snd_lt : ∀ {n : ℕ} {kl : ℕ × ℕ}, kl ∈ Finset.HasAntidiagonal.antidiagonal n → kl.2 < n + 1
-- Mathlib.Algebra.Order.IsBotOne
/-- A typeclass expressing that the `0` of a type is a bottom element. In a partial `OrderBot`, this
is equivalent to `⊥ = 0`.  -/
IsBotZeroClass : (α : Type u_1) → [LE α] → [Zero α] → Prop
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddSemigroup : {α : Type u_1} → [AddSemigroup α] → AddSemigroup αᵒᵈ
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Chinese remainder theorem** for a Dedekind domain: `R ⧸ I` factors as `Π i, R ⧸ (P i ^ e i)`,
where `P i` ranges over the prime factors of `I` and `e i` over the multiplicities.  -/
IsDedekindDomain.quotientEquivPiFactors : {R : Type u_1} →
  [inst : CommRing R] →
    [inst_1 : IsDedekindDomain R] →
      {I : Ideal R} →
        I ≠ ⊥ →
          R ⧸ I ≃+*
            ((P : ↥(UniqueFactorizationMonoid.factors I).toFinset) →
              R ⧸ ↑P ^ Multiset.count (↑P) (UniqueFactorizationMonoid.factors I))
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_vector : ∀ (α : Type u) (n : ℕ), Cardinal.mk (List.Vector α n) = Cardinal.mk α ^ n
-- Mathlib.Order.SymmDiff
compl_bihimp_compl : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (a b : α), bihimp aᶜ bᶜ = bihimp a b
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- Mapping from `Expr` to a variable representing it.  -/
Lean.Meta.Grind.Arith.Linear.Struct.varMap : Lean.Meta.Grind.Arith.Linear.Struct → Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Grind.Linarith.Var
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.mapAlgEquiv_trans : ∀ {R : Type u_1} {A : Type u_4} {B : Type u_5} {C : Type u_6} {M : Type u_7} [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 : AddMonoid M] (e₁ : A ≃ₐ[R] B) (e₂ : B ≃ₐ[R] C),
  AddMonoidAlgebra.mapAlgEquiv R M (e₁.trans e₂) =
    (AddMonoidAlgebra.mapAlgEquiv R M e₁).trans (AddMonoidAlgebra.mapAlgEquiv R M e₂)
-- Mathlib.Algebra.Module.Submodule.Bilinear
Submodule.map₂_map_map : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] {M₂ : Type u_5} {N₂ : Type u_6} [inst_7 : AddCommMonoid M₂] [inst_8 : AddCommMonoid N₂]
  [inst_9 : Module R M₂] [inst_10 : Module R N₂] (f : M₂ →ₗ[R] N₂ →ₗ[R] P) (g : M →ₗ[R] M₂) (h : N →ₗ[R] N₂)
  (p : Submodule R M) (q : Submodule R N),
  Submodule.map₂ f (Submodule.map g p) (Submodule.map h q) = Submodule.map₂ (f.compl₁₂ g h) p q
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.round_exp_one_eq_three : round (Real.exp 1) = 3
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanFileProgressKind : Type
-- Plausible.Testable
Plausible.Testable.decidableTestable : {p : Prop} → [Plausible.PrintableProp p] → [Decidable p] → Plausible.Testable p
-- Mathlib.CategoryTheory.Sums.Products
CategoryTheory.Sum.functorEquiv_inverse_map : ∀ (A : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} A] (A' : Type u_2)
  [inst_1 : CategoryTheory.Category.{v_2, u_2} A'] (B : Type u) [inst_2 : CategoryTheory.Category.{v, u} B]
  {X Y : CategoryTheory.Functor A B × CategoryTheory.Functor A' B} (η : X ⟶ Y),
  (CategoryTheory.Sum.functorEquiv A A' B).inverse.map η = CategoryTheory.NatTrans.sum' η.1 η.2
-- Mathlib.RingTheory.FormalGroup.Basic
/-- Associativity condition: $F(F(X, Y), Z) = F(X, F(Y, Z))$.  -/
FormalGroup.assoc : ∀ {R : Type u_1} [inst : CommRing R] (self : FormalGroup R),
  MvPowerSeries.subst
      ![MvPowerSeries.subst ![MvPowerSeries.X 0, MvPowerSeries.X 1] self.toPowerSeries, MvPowerSeries.X 2]
      self.toPowerSeries =
    MvPowerSeries.subst
      ![MvPowerSeries.X 0, MvPowerSeries.subst ![MvPowerSeries.X 1, MvPowerSeries.X 2] self.toPowerSeries]
      self.toPowerSeries
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
/-- You can compute a product over an encodable type by multiplying over the natural numbers and
taking a supremum.  -/
tprod_iSup_decode₂ : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {α : Type u_3} {β : Type u_4}
  [inst_2 : Encodable β] [inst_3 : CompleteLattice α] (m : α → M),
  m ⊥ = 1 → ∀ (s : β → α), ∏' (i : ℕ), m (⨆ b ∈ Encodable.decode₂ β i, s b) = ∏' (b : β), m (s b)
-- Init.Control.Basic
/-- Depending on the `Alternative` instance, collects values or recovers from `failure`s by
returning the leftmost success. Can be written using the `<|>` operator syntax.
 -/
Alternative.orElse : {f : Type u → Type v} → [self : Alternative f] → {α : Type u} → f α → (Unit → f α) → f α
-- Lean.Elab.InfoTree.Types
Lean.Elab.InfoTree.hole.injEq : ∀ (mvarId mvarId_1 : Lean.MVarId),
  (Lean.Elab.InfoTree.hole mvarId = Lean.Elab.InfoTree.hole mvarId_1) = (mvarId = mvarId_1)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.X.eq_1 : ∀ {R : Type u_1} [inst : Semiring R], SkewPolynomial.X = (SkewPolynomial.monomial 1) 1
-- Mathlib.Data.Seq.Defs
Stream'.Seq.Terminates.eq_1 : ∀ {α : Type u} (s : Stream'.Seq α), s.Terminates = ∃ n, s.TerminatedAt n