mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Iter.step.eq_1 : ∀ {α β : Type w} [inst : Std.Iterator α Id β] (it : Std.Iter β), it.step = it.toIterM.step.run.inflate.toPure
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.mem_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp] {l : List α} {k : α},
  k ∈ Std.DTreeMap.Raw.Const.unitOfList l cmp ↔ l.contains k = true
-- Mathlib.Data.Matrix.DMatrix
/-- `DMatrix.col u` is the column matrix whose entries are given by `u`.  -/
DMatrix.col : {m : Type u_1} → {α : m → Type v} → ((i : m) → α i) → DMatrix m Unit fun i _j => α i
-- Mathlib.Algebra.FiniteSupport.Basic
/-- Eta-expanded form of `Function.HasFiniteSupport.smul_right` -/
Function.HasFiniteSupport.fun_smul_right : ∀ {α : Type u_1} {R : Type u_2} {M : Type u_3} [inst : Zero M] [inst_1 : SMulZeroClass R M] (f : α → R) {g : α → M},
  Function.HasFiniteSupport g → Function.HasFiniteSupport fun i => f i • g i
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.forIn_array : ∀ {α : Type u₁} {β : Type (max u₁ u₂)} {m : Type (max u₁ u₂) → Type v} {Pred EPred : Type (max u₁ u₂)} [inst : Monad m]
  [inst_1 : Std.Internal.Do.Assertion Pred] [inst_2 : Std.Internal.Do.Assertion EPred]
  [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {xs : Array α} {init : β} {f : α → β → m (ForInStep β)}
  (inv : Std.Internal.Do.Invariant xs.toList β Pred) {epost : EPred},
  (∀ (pref : List α) (cur : α) (suff : List α) (h : xs.toList = pref ++ cur :: suff) (b : β),
      ⦃ inv { «prefix» := pref, suffix := cur :: suff, property := ⋯ } b ⦄ f cur b ⦃ fun r =>
        match r with
        | ForInStep.yield b' => inv { «prefix» := pref ++ [cur], suffix := suff, property := ⋯ } b'
        | ForInStep.done b' => inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b';
        epost ⦄) →
    ⦃ inv { «prefix» := [], suffix := xs.toList, property := ⋯ } init ⦄ forIn xs init f ⦃ fun b =>
      inv { «prefix» := xs.toList, suffix := [], property := ⋯ } b; epost ⦄
-- Std.Time.Time.Unit.Hour
/-- `Offset` represents an offset in hours, defined as an `Int`. This can be used to express durations
or differences in hours.
 -/
Std.Time.Hour.Offset : Type
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.instHasProjectiveDimensionLTOfNatNat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C],
  CategoryTheory.HasProjectiveDimensionLT 0 0
-- Mathlib.Algebra.Homology.Factorizations.CM5a
/-- Given a monomorphism `f : K ⟶ L` between complexes that are strictly `≥ n₀ + 1`,
this is a projective system in `(cofFib f).FullSubcategory` given by the
sequence of morphisms `CofFibFactorizationQuasiIsoLE.toSequenceNext`.  -/
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.functor : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {K L : CochainComplex C ℤ} →
        (f : K ⟶ L) →
          [CategoryTheory.EnoughInjectives C] →
            [CategoryTheory.Mono f] →
              (n₀ : ℤ) →
                [K.IsStrictlyGE (n₀ + 1)] →
                  [L.IsStrictlyGE (n₀ + 1)] →
                    CategoryTheory.Functor ℕᵒᵖ
                      (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.cofFib✝ f).FullSubcategory
-- Std.Sat.CNF.RelabelFin
/-- An upper bound for the amount of distinct literals in `f`.
 -/
Std.Sat.CNF.numLiterals : Std.Sat.CNF ℕ → ℕ
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.neg_subset_closure : ∀ {G : Type u_2} [inst : AddGroup G] (S : Set G), -S ⊆ ↑(AddSubgroup.closure S)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SemanticTokensRangeParams : Type
-- Mathlib.Analysis.BoxIntegral.Box.Basic
/-- Closed box corresponding to `I : BoxIntegral.Box ι`.  -/
BoxIntegral.Box.Icc : {ι : Type u_1} → BoxIntegral.Box ι ↪o Set (ι → ℝ)
-- Mathlib.RingTheory.Derivation.MapCoeffs
Differential.implicitDeriv_X : ∀ {A : Type u_1} [inst : CommRing A] [inst_1 : Differential A] (v : Polynomial A),
  (Differential.implicitDeriv v) Polynomial.X = v
-- Init.Data.Float.Model.Float
/-- Compute the sum of two `Float.Model`.
 -/
Float.Model.add : Float.Model → Float.Model → Float.Model
-- Mathlib.Order.Lattice
DistribLattice.mk : {α : Type u_1} → [toLattice : Lattice α] → (∀ (x y z : α), (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z) → DistribLattice α
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.CommSq.shortComplex_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl : X₂ ⟶ X₄} {inr : X₃ ⟶ X₄}
  (sq : CategoryTheory.CommSq f g inl inr), sq.shortComplex.f = CategoryTheory.Limits.biprod.lift f (-g)
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.coe_comap : ∀ {R : Type u_2} {E : Type u_3} {F : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] [inst_6 : AddCommMonoid F]
  [inst_7 : TopologicalSpace F] [inst_8 : Module R F] (f : E →L[R] F) (C : ProperCone R F),
  ↑(ProperCone.comap f C) = ⇑f ⁻¹' ↑C
-- Mathlib.Util.AtomM
/-- A safe version of `isDefEq` that doesn't throw errors. We use it to avoid
"unknown free variable `_fvar.102937`" errors when there may be out-of-scope free variables.

TODO: don't catch any other errors
 -/
Mathlib.Tactic.isDefEqSafe : Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Mathlib.AlgebraicGeometry.Sites.SmallAffineZariski
/-- The relative gluing data associated to a quasi-coherent `𝒪ₓ` algebra.  -/
AlgebraicGeometry.Scheme.AffineZariskiSite.relativeGluingData : {X : AlgebraicGeometry.Scheme} →
  {F : CategoryTheory.Functor X.AffineZariskiSiteᵒᵖ CommRingCat} →
    {α : (AlgebraicGeometry.Scheme.AffineZariskiSite.toOpensFunctor X).op.comp X.presheaf ⟶ F} →
      CategoryTheory.NatTrans.Coequifibered α →
        AlgebraicGeometry.Scheme.Cover.RelativeGluingData (AlgebraicGeometry.Scheme.AffineZariskiSite.directedCover X)
-- Init.Prelude
/-- Bijection between `α` and `PULift.{v} α`  -/
PULift.down_up : ∀ {α : Sort u} (a : α), { down := a }.down = a
-- Mathlib.Data.Ordmap.Ordnode
Ordnode.dual.eq_2 : ∀ {α : Type u_1} (sz : ℕ) (l : Ordnode α) (x_1 : α) (r : Ordnode α),
  (Ordnode.node sz l x_1 r).dual = Ordnode.node sz r.dual x_1 l.dual
-- Std.Http.Protocol.H1.Writer
/-- Set when the user has finished sending body data, allowing fixed-size framing
to be determined upfront.
 -/
Std.Http.Protocol.H1.Writer.userClosedBody : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → Bool
-- Plausible.DeriveArbitrary
/-- Variant of `Deriving.Util.mkInstanceCmds` which is specialized to creating `ArbitraryFueled` instances
that have `Arbitrary` inst-implicit binders.

Note that we can't use `mkInstanceCmds` out of the box,
since it expects the inst-implicit binders and the instance we're creating to both belong to the same typeclass.  -/
_private.Plausible.DeriveArbitrary.0.Plausible.mkArbitraryFueledInstanceCmds : Lean.Elab.Deriving.Context → Array Lean.Name → optParam Bool true → Lean.Elab.TermElabM (Array Lean.Command)
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.union_mul_inter_subset_union : ∀ {α : Type u_2} [inst : Mul α] {s₁ s₂ t₁ t₂ : Set α}, (s₁ ∪ s₂) * (t₁ ∩ t₂) ⊆ s₁ * t₁ ∪ s₂ * t₂
-- Init.Internal.Order.Basic
Lean.Order.EST.bot : {ε σ α : Type} → [Nonempty ε] → EST ε σ α
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.toArray_toList : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α], m.WF → m.toList.toArray = m.toArray
-- Aesop.Tree.Data.ForwardRuleMatches
Aesop.ForwardRuleMatches.mk : Lean.PHashSet Aesop.ForwardRuleMatch →
  Lean.PHashSet Aesop.ForwardRuleMatch → Lean.PHashSet Aesop.ForwardRuleMatch → Aesop.ForwardRuleMatches
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_right_le_mk_div_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk b ≤ MulArchimedeanClass.mk (a / b) ↔ MulArchimedeanClass.mk b ≤ MulArchimedeanClass.mk a
-- Init.Data.ByteArray.Lemmas
ByteArray.getElem_set!_ne : ∀ (data : ByteArray) (i j : ℕ) (v : UInt8), i ≠ j → ∀ (hj : j < data.size), (data.set! i v)[j] = data[j]
-- Lean.Meta.MethodSpecs
_private.Lean.Meta.MethodSpecs.0.Lean.mkSpecTheoremName : Lean.Environment → Lean.Name → Bool → String → Lean.Name
-- Mathlib.Analysis.Convex.Between
Sbtw.trans_wbtw_right_ne : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] [IsDomain R] [Module.IsTorsionFree R V]
  {w x y z : P}, Sbtw R w x z → Wbtw R x y z → w ≠ y
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.ofIso_r : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (s : S₁.Splitting) (e : S₁ ≅ S₂),
  (s.ofIso e).r = CategoryTheory.CategoryStruct.comp e.inv.τ₂ (CategoryTheory.CategoryStruct.comp s.r e.hom.τ₁)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt8.reduceSub : Lean.Meta.Simp.DSimproc
-- Init.Data.Int.Lemmas
Int.subNatNat_eq_coe : ∀ {m n : ℕ}, Int.subNatNat m n = ↑m - ↑n
-- Mathlib.CategoryTheory.Presentable.CardinalFilteredPresentation
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {κ : Cardinal.{w}}
  [inst_1 : Fact κ.IsRegular], P.IsCardinalFilteredGenerator κ → P.isoClosure.IsCardinalFilteredGenerator κ
-- Mathlib.Algebra.Field.Defs
/-- The inverse of `0` in a group with zero is `0`.  -/
DivisionSemiring.inv_zero : ∀ {K : Type u_2} [self : DivisionSemiring K], 0⁻¹ = 0
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.ΓSpecIso_hom_stalkClosedPointIso_inv : ∀ (R : CommRingCat) [inst : IsLocalRing ↑R],
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).hom
      (AlgebraicGeometry.stalkClosedPointIso R).inv =
    (AlgebraicGeometry.Spec R).presheaf.germ ⊤ (IsLocalRing.closedPoint ↑R) trivial
-- Init.Data.BitVec.Lemmas
BitVec.msb_zero_length : ∀ (x : BitVec 0), x.msb = false
-- Mathlib.Tactic.FunProp.Theorems
/-- Decides whether `f` is a function corresponding to one of the lambda theorems.  -/
Mathlib.Meta.FunProp.detectLambdaTheoremArgs : Lean.Expr → Array Lean.Expr → Lean.MetaM (Option Mathlib.Meta.FunProp.LambdaTheoremArgs)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constGetEntryLT?_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α}, t₁.Equiv t₂ → Std.DTreeMap.Const.getEntryLT? t₁ k = Std.DTreeMap.Const.getEntryLT? t₂ k
-- Mathlib.MeasureTheory.OuterMeasure.Basic
/-- **Alias** of `MeasureTheory.measure_le_inter_add_sdiff`. -/
MeasureTheory.measure_le_inter_add_diff : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] (μ : F)
  (s t : Set α), μ s ≤ μ (s ∩ t) + μ (s \ t)
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
CategoryTheory.MorphismProperty.toPath_mem_paths_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  {f : X ⟶ Y}, W.paths f.toPath ↔ W f
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.size_inter_le_size_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → (m₁ ∩ m₂).size ≤ m₁.size
-- Mathlib.Algebra.Polynomial.AlgebraMap
/-- The involutive automorphism of the polynomial algebra given by `p(X) ↦ p(-X)`.  -/
Polynomial.algEquivAevalNegX : {R : Type u_3} → [inst : CommRing R] → Polynomial R ≃ₐ[R] Polynomial R
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
Homotopy.extend.homAux.eq_1 : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Preadditive C]
  {K L : HomologicalComplex C c} (φ : (i j : ι) → K.X i ⟶ L.X j) (j' : Option ι), Homotopy.extend.homAux φ none j' = 0
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.getConfig : Lean.Meta.Sym.SymM Lean.Meta.Sym.Config
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.isEmpty_filterMap!_eq_false_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [Std.TransOrd α] {f : α → β → Option γ},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filterMap! f t).isEmpty = false ↔
      ∃ k,
        ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true),
          (f (t.getKey k h) (Std.DTreeMap.Internal.Impl.Const.get t k h)).isSome = true)
-- Mathlib.Analysis.SpecialFunctions.Stirling
/-- The Stirling sequence is bounded below by `√π`, for all positive naturals. Note that this bound
holds for all `n > 0`, rather than for sufficiently large `n`: it is effective.
 -/
Stirling.sqrt_pi_le_stirlingSeq : ∀ {n : ℕ}, n ≠ 0 → √Real.pi ≤ Stirling.stirlingSeq n
-- Mathlib.Order.Antisymmetrization
instTransLeAntisymmRel : {α : Type u_1} →
  [inst : Preorder α] → Trans (fun x1 x2 => x1 ≤ x2) (AntisymmRel fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.RingTheory.UniqueFactorizationDomain.Finsupp
factorization_zero : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] [inst_2 : NormalizationMonoid α]
  [inst_3 : DecidableEq α], factorization 0 = 0
-- Mathlib.Probability.ProbabilityMassFunction.Basic
/-- Given that `α` is a countable, measurable space with all singleton sets measurable,
we can convert any probability measure into a `PMF`, where the mass of a point
is the measure of the singleton set under the original measure.  -/
MeasureTheory.Measure.toPMF : {α : Type u_1} →
  [Countable α] →
    [inst : MeasurableSpace α] →
      [MeasurableSingletonClass α] → (μ : MeasureTheory.Measure α) → [h : MeasureTheory.IsProbabilityMeasure μ] → PMF α
-- Mathlib.Data.Sum.Interval
Finset.sumLexLift.eq_4 : ∀ {α₁ : Type u_1} {α₂ : Type u_2} {β₁ : Type u_3} {β₂ : Type u_4} {γ₁ : Type u_5} {γ₂ : Type u_6}
  (f₁ : α₁ → β₁ → Finset γ₁) (f₂ : α₂ → β₂ → Finset γ₂) (g₁ : α₁ → β₂ → Finset γ₁) (g₂ : α₁ → β₂ → Finset γ₂) (a : α₂)
  (b : β₂), Finset.sumLexLift f₁ f₂ g₁ g₂ (Sum.inr a) (Sum.inr b) = Finset.map { toFun := Sum.inr, inj' := ⋯ } (f₂ a b)
-- Mathlib.RingTheory.Regular.RegularSequence
RingTheory.Sequence.isWeaklyRegular_cons_iff : ∀ {R : Type u_1} (M : Type u_3) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R)
  (rs : List R),
  RingTheory.Sequence.IsWeaklyRegular M (r :: rs) ↔
    IsSMulRegular M r ∧ RingTheory.Sequence.IsWeaklyRegular (QuotSMulTop r M) rs
-- Mathlib.Topology.Defs.Basic
/-- An open quotient map is continuous.  -/
IsOpenQuotientMap.continuous : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenQuotientMap f → Continuous f
-- Init.Data.SInt.Lemmas
ISize.one_mul : ∀ (a : ISize), 1 * a = a
-- Mathlib.Data.Multiset.NatAntidiagonal
/-- The antidiagonal of a natural number `n` is
the multiset of pairs `(i, j)` such that `i + j = n`.  -/
Multiset.Nat.antidiagonal : ℕ → Multiset (ℕ × ℕ)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.length_eq : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) [Nonempty R]
  (s : Set R), f.length s = ⨅ a, ⨅ b, ⨅ (_ : s \ botSet ⊆ Set.Ioc a b), ENNReal.ofReal (↑f b - ↑f a)
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_prodMk : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : ι → Type u_8}
  {m : (i : ι) → MeasurableSpace (β i)} {f : (i : ι) → Ω → β i},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.Kernel.IndepFun (fun a => (f i a, f j a)) (f k) κ μ
-- Mathlib.Topology.Separation.Regular
hasBasis_opens_closure : ∀ {X : Type u_1} [inst : TopologicalSpace X] [RegularSpace X] (x : X),
  (nhds x).HasBasis (fun s => x ∈ s ∧ IsOpen s) closure
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesOnBall.sum : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {r : ENNReal},
  HasFPowerSeriesOnBall f p x r → ∀ {y : E}, y ∈ Metric.eball 0 r → f (x + y) = p.sum y
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.coe_top : ∀ {α : Type u_1} [inst : LE α], ↑⊤ = Set.univ
-- Mathlib.Algebra.Category.Grp.ForgetCorepresentable
uliftZMultiplesHom_apply_apply : ∀ (G : Type u) [inst : AddGroup G] (a : G) (x : ULift.{u, 0} ℤ), ((uliftZMultiplesHom G) a) x = AddEquiv.ulift x • a
-- Mathlib.Data.Finset.Filter
Finset.filter_val : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] (s : Finset α),
  (Finset.filter p s).val = Multiset.filter p s.val
-- Mathlib.Analysis.LocallyConvex.AbsConvex
/-- **Alias** of the reverse direction of `absConvexHull_nonempty`. -/
Set.Nonempty.absConvexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : AddCommMonoid E]
  [inst_3 : PartialOrder 𝕜] {s : Set E}, s.Nonempty → ((absConvexHull 𝕜) s).Nonempty
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_ofNatClamp_of_le : ∀ {n : ℕ},
  UInt64.size ≤ n →
    (UInt64.ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) UInt32.toUInt16_ofNatClamp_of_le._proof_1
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.casesOnNum : Int.Internal.Linear.Poly → (ℤ → Bool) → Bool
-- Init.Data.Array.Basic
Array.forM_eq_forM : ∀ {α : Type u} {m : Type u_1 → Type u_2} {as : Array α} [inst : Monad m] {f : α → m PUnit.{u_1 + 1}},
  Array.forM f as = forM as f
-- Init.Data.Array.Erase
Array.eraseIdx_append_of_lt_size : ∀ {α : Type u_1} {xs : Array α} {k : ℕ} (hk : k < xs.size) (ys : Array α) (h : k < (xs ++ ys).size),
  (xs ++ ys).eraseIdx k h = xs.eraseIdx k hk ++ ys
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
CategoryTheory.Abelian.PreservesCoimage.iso_inv_π_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] {X Y : C} (f : X ⟶ Y)
  [inst_5 : CategoryTheory.Limits.HasKernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)]
  [inst_7 : CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F]
  [inst_8 :
    CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F]
  [inst_9 : CategoryTheory.Limits.HasKernel (F.map f)]
  [inst_10 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] {Z : D}
  (h : F.obj (CategoryTheory.Abelian.coimage f) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π (F.map f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.PreservesCoimage.iso F f).inv h) =
    CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Abelian.coimage.π f)) h
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey!_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] {f : α → β → Option γ} {k : α} (h : t.WF),
  (Std.DTreeMap.Raw.filterMap f t).getKey! k =
    ((t.getKey? k).pfilter fun x h' => (f x (Std.DTreeMap.Raw.Const.get t x ⋯)).isSome).get!
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.symm_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (f : M ≃* N), f.symm.symm = f
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.MemLp.integrable_sq : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ℝ},
  MeasureTheory.MemLp f 2 μ → MeasureTheory.Integrable (fun x => f x ^ 2) μ
-- Mathlib.Data.Set.Defs
/-- **Alias** of `Set.ofPred`.

---

Turn a predicate `p : α → Prop` into a set, also written as `{x | p x}`  -/
setOf : {α : Type u} → (α → Prop) → Set α
-- Lean.Data.Lsp.Basic
Lean.Lsp.instInhabitedLocation : Inhabited Lean.Lsp.Location
-- Init.Data.BitVec.Lemmas
BitVec.toNat_ge_of_msb_true : ∀ {n : ℕ} {x : BitVec n}, x.msb = true → x.toNat ≥ 2 ^ (n - 1)
-- Init.Data.Nat.MinMax
Nat.max_lt : ∀ {a b c : ℕ}, max a b < c ↔ a < c ∧ b < c
-- Lean.Elab.Tactic.Omega.MinNatAbs
/-- The maximum absolute value in a list of integers.  -/
Lean.Elab.Tactic.Omega.List.maxNatAbs : List ℤ → ℕ
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.r_of_eq : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {x y : M × ↥S},
  ↑y.2 * x.1 = ↑x.2 * y.1 → (Localization.r S) x y
-- Std.Http.Data.Response
Std.Http.Response.instInhabitedHead : Inhabited Std.Http.Response.Head
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
AddSubsemigroup.unop_eq_bot : ∀ {M : Type u_2} [inst : Add M] {S : AddSubsemigroup Mᵃᵒᵖ}, S.unop = ⊥ ↔ S = ⊥
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.mk_coe' : ∀ {M : Type u_4} {N : Type u_5} [inst : Mul M] [inst_1 : Mul N] (e : M ≃* N) (f : N → M)
  (h₁ : Function.LeftInverse (⇑e) f) (h₂ : Function.RightInverse (⇑e) f)
  (h₃ :
    ∀ (x y : N),
      { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun (x * y) =
        { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun x *
          { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂ }.toFun y),
  { toFun := f, invFun := ⇑e, left_inv := h₁, right_inv := h₂, map_mul' := h₃ } = e.symm
-- Init.Data.String.Subslice
/-- Given a position `p` within a slice `s` and a subslice `sl` of
`s.sliceFrom p`, reinterpret `sl` as a subslice of `s` by applying
`Pos.ofSliceFrom` to the endpoints.
 -/
String.Slice.Subslice.ofSliceFrom : {s : String.Slice} → {p : s.Pos} → (s.sliceFrom p).Subslice → s.Subslice
-- Mathlib.Tactic.Linter.Lint
/-- The `dupNamespace` linter produces a warning when a component of a declaration name is repeated
several times. The repetition does not have to be consecutive. Examples: `Nat.Nat.foo`,
`One.two.two`, `Nat.One.Nat`, `Nat.Prime.Nat.Prime.foo`, `Nat.Prime.Nat.bar`

The linter also warns about auto-generated declarations (such as, those generated by `to_additive`).
 -/
_private.Mathlib.Tactic.Linter.Lint.0.Mathlib.Linter.DupNamespaceLinter.dupNamespace : Lean.Linter
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.coev_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J : C} (f : I ⟶ J)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ExponentiableMorphism f]
  {X Y : CategoryTheory.Over J} (g : X ⟶ Y) {Z : CategoryTheory.Over J}
  (h :
    (CategoryTheory.ExponentiableMorphism.pushforward f).obj ((CategoryTheory.ChosenPullbacksAlong.pullback f).obj Y) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp g
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.ExponentiableMorphism.coev f).app Y) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.ExponentiableMorphism.coev f).app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.ExponentiableMorphism.pushforward f).map
          ((CategoryTheory.ChosenPullbacksAlong.pullback f).map g))
        h)
-- Mathlib.Data.Set.Card
/-- **Alias** of `Set.ncard_inter_add_ncard_sdiff_eq_ncard`. -/
Set.ncard_inter_add_ncard_diff_eq_ncard : ∀ {α : Type u_1} (s t : Set α),
  autoParam s.Finite Set.ncard_inter_add_ncard_sdiff_eq_ncard._auto_1 → (s ∩ t).ncard + (s \ t).ncard = s.ncard
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_mem_Icc : ∀ (x : ℝ), Real.sin x ∈ Set.Icc (-1) 1