mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Fourier.AddCircle
/-- The star subalgebra of `C(AddCircle T, ℂ)` generated by `fourier n` for `n ∈ ℤ` is in fact the
linear span of these functions.  -/
fourierSubalgebra_coe : ∀ {T : ℝ}, Subalgebra.toSubmodule fourierSubalgebra.toSubalgebra = Submodule.span ℂ (Set.range fourier)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
/-- Useful for replacing `f` by `Spec.map φ` everywhere in proofs.  -/
AlgebraicGeometry.Spec.map_surjective : ∀ {R S : CommRingCat}, Function.Surjective AlgebraicGeometry.Spec.map
-- Std.Sync.Channel
/-- Tried to close an already closed channel.
 -/
Std.CloseableChannel.Error.alreadyClosed : Std.CloseableChannel.Error
-- Mathlib.Order.SuccPred.Limit
Order.IsPredLimit.ne_top : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : OrderTop α], Order.IsPredLimit a → a ≠ ⊤
-- Mathlib.CategoryTheory.Types.Basic
/-- A morphism in `Type` is a monomorphism if and only if it is injective.  -/
CategoryTheory.mono_iff_injective : ∀ {X Y : Type u} (f : X ⟶ Y), CategoryTheory.Mono f ↔ Function.Injective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion.0.aux_IsBigO_mul : ∀ (k l : ℕ) (p : ℝ) {f : ℕ → ℂ},
  (f =O[Filter.atTop] fun n => ↑n ^ l) →
    (fun n => f n * (2 * ↑Real.pi * Complex.I * ↑n / ↑p) ^ k) =O[Filter.atTop] fun n => ↑(n ^ (l + k))
-- Mathlib.Probability.Kernel.Composition.KernelLemmas
ProbabilityTheory.Kernel.compProd_prodMkLeft_eq_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {mX : MeasurableSpace X} {mY : MeasurableSpace Y}
  {mZ : MeasurableSpace Z} (κ : ProbabilityTheory.Kernel X Y) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel Y Z) [ProbabilityTheory.IsSFiniteKernel η],
  κ.compProd (ProbabilityTheory.Kernel.prodMkLeft X η) = (ProbabilityTheory.Kernel.id.prod η).comp κ
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tendsto_nat_tsum : ∀ (f : ℕ → ENNReal), Filter.Tendsto (fun n => ∑ i ∈ Finset.range n, f i) Filter.atTop (nhds (∑' (n : ℕ), f n))
-- Init.Core
BEq.rfl : ∀ {α : Type u_1} [inst : BEq α] [ReflBEq α] {a : α}, (a == a) = true
-- Mathlib.Order.Bounds.Defs
/-- `a` is a least upper bound of a set `s`; for a partial order, it is unique if exists.  -/
IsLUB : {α : Type u_1} → [LE α] → Set α → α → Prop
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_insertMany!_list_of_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {l : List ((a : α) × β a)} {k k' : α},
      compare k k' = Ordering.eq →
        List.Pairwise (fun a b => ¬compare a.fst b.fst = Ordering.eq) l →
          k ∈ List.map Sigma.fst l →
            ∀ {h' : Std.DTreeMap.Internal.Impl.contains k' ↑(t.insertMany! l) = true},
              (↑(t.insertMany! l)).getKey k' h' = k
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.seq' : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {P : Std.Do.Assertion ps} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] {α β : Type u} {x : m (α → β)} {y : m α} {Q : Std.Do.PostCond β ps},
  ⦃P⦄ x ⦃(fun f => (Std.Do.wp y).apply (fun a => Q.1 (f a), Q.2), Q.2)⦄ → ⦃P⦄ (x <*> y) ⦃Q⦄
-- Lean.MetavarContext
Lean.MetavarContext.getDelayedMVarAssignmentCore? : Lean.MetavarContext → Lean.MVarId → Option Lean.DelayedMetavarAssignment
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_of_mem_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α}
  {v : β k}, a ∈ t.insert k v → cmp k a ≠ Ordering.eq → a ∈ t
-- Mathlib.MeasureTheory.Measure.PreVariation
MeasureTheory.ennrealPreVariation.congr_simp : ∀ {X : Type u_1} [inst : MeasurableSpace X] (f f_1 : Set X → ENNReal) (e_f : f = f_1)
  (hf : MeasureTheory.IsSigmaSubadditiveSetFun f) (hf' : f ∅ = 0),
  MeasureTheory.ennrealPreVariation f hf hf' = MeasureTheory.ennrealPreVariation f_1 ⋯ ⋯
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_sin_pow_aux : ∀ {a b : ℝ} (n : ℕ),
  ∫ (x : ℝ) in a..b, Real.sin x ^ (n + 2) =
    (Real.sin a ^ (n + 1) * Real.cos a - Real.sin b ^ (n + 1) * Real.cos b +
        (↑n + 1) * ∫ (x : ℝ) in a..b, Real.sin x ^ n) -
      (↑n + 1) * ∫ (x : ℝ) in a..b, Real.sin x ^ (n + 2)
-- Mathlib.Data.Multiset.UnionInter
Multiset.instDistribLattice : {α : Type u_1} → [DecidableEq α] → DistribLattice (Multiset α)
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicator.congr_simp : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ δ_1 : ℝ} (e_δ : δ = δ_1) (δ_pos : 0 < δ) (E E_1 : Set α),
  E = E_1 → thickenedIndicator δ_pos E = thickenedIndicator ⋯ E_1
-- Mathlib.Data.ENat.Lattice
ENat.smul_sSup : ∀ {R : Type u_4} [inst : SMul R ℕ∞] [IsScalarTower R ℕ∞ ℕ∞] (s : Set ℕ∞) (c : R), c • sSup s = ⨆ a ∈ s, c • a
-- Mathlib.Order.Restriction
Preorder.piCongrLeft_comp_restrictLe : ∀ {α : Type u_1} [inst : Preorder α] {π : α → Type u_2} [inst_1 : LocallyFiniteOrderBot α] {a : α},
  ⇑(Equiv.piCongrLeft (fun i => π ↑i) (Equiv.IicFinsetSet a).symm) ∘ Preorder.restrictLe a = Preorder.frestrictLe a
-- Mathlib.RepresentationTheory.Coinvariants
Representation.Coinvariants.mk_tmul_inv : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} {W : Type u_9} [inst : CommRing k] [inst_1 : Group G]
  [inst_2 : AddCommGroup V] [inst_3 : Module k V] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  (ρ : Representation k G V) (τ : Representation k G W) (x : V) (y : W) (g : G),
  (Representation.Coinvariants.mk (ρ.tprod τ)) (x ⊗ₜ[k] (τ g⁻¹) y) =
    (Representation.Coinvariants.mk (ρ.tprod τ)) ((ρ g) x ⊗ₜ[k] y)
-- Mathlib.CategoryTheory.Adjunction.ParametrizedLimits
CategoryTheory.ParametrizedAdjunction.preservesLimit_flip_obj : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {J : Type u_4}
  [inst_3 : CategoryTheory.Category.{v_4, u_4} J] (P : CategoryTheory.Functor J C₁ᵒᵖ)
  [∀ (X₂ : C₂), CategoryTheory.Limits.PreservesColimit P.leftOp (F.flip.obj X₂)] (X₃ : C₃),
  CategoryTheory.Limits.PreservesLimit P (G.flip.obj X₃)
-- Mathlib.Data.Part
Part.get_eq_get_of_eq : ∀ {α : Type u_1} (a : Part α) (ha : a.Dom) {b : Part α} (h : a = b), a.get ha = b.get ⋯
-- Mathlib.Order.Partition.Finpartition
Finpartition.ofErase.congr_simp : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : OrderBot α] [inst_2 : DecidableEq α] {a : α} (parts parts_1 : Finset α)
  (e_parts : parts = parts_1) (sup_indep : parts.SupIndep id) (sup_parts : parts.sup id = a),
  Finpartition.ofErase parts sup_indep sup_parts = Finpartition.ofErase parts_1 ⋯ ⋯
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.leftFunc_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Comma (CategoryTheory.Functor.id C) (CategoryTheory.Functor.id C)),
  CategoryTheory.Arrow.leftFunc.obj X = X.left
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatch_iff : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos ↔ (s.sliceFrom pos).copy = pat
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.ofEquiv_F : ∀ {α : Type u_1} {τ : Type u_4} {f : Filter α} (F : f.Realizer) (E : F.σ ≃ τ) (s : τ),
  (F.ofEquiv E).F.f s = F.F.f (E.symm s)
-- Lean.Util.Diff
/-- Leave the item in the source  -/
Lean.Diff.Action.skip : Lean.Diff.Action
-- Mathlib.CategoryTheory.Sites.Equivalence
CategoryTheory.GrothendieckTopology.PreservesSheafification.transport : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (K : CategoryTheory.GrothendieckTopology D)
  (G : CategoryTheory.Functor D C) {A : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} A] (B : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor A B) [G.IsCoverDense J] [G.Full]
  [inst_6 : G.IsContinuous K J] [(G.sheafPushforwardContinuous B K J).EssSurj]
  [(G.sheafPushforwardContinuous A K J).EssSurj] [K.PreservesSheafification F], J.PreservesSheafification F
-- Mathlib.FieldTheory.Relrank
IntermediateField.lift_relrank_comap_comap_eq_lift_relrank_of_surjective : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {L : Type w} [inst_3 : Field L]
  [inst_4 : Algebra F L] (A B : IntermediateField F E) (f : L →ₐ[F] E),
  Function.Surjective ⇑f →
    Cardinal.lift.{v, w} ((IntermediateField.comap f A).relrank (IntermediateField.comap f B)) =
      Cardinal.lift.{w, v} (A.relrank B)
-- Init.Data.SInt.Basic
instMinInt16 : Min Int16
-- Mathlib.Order.CompleteBooleanAlgebra
iSup_inf_eq : ∀ {α : Type u} {ι : Sort w} [inst : Order.Frame α] (f : ι → α) (a : α), (⨆ i, f i) ⊓ a = ⨆ i, f i ⊓ a
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.instLawfulFunctor : LawfulFunctor MeasureTheory.OuterMeasure
-- Lean.Parser.Term
/-- Throws an error exception, tagging the associated message as a named error with the specified name
and validating that an associated error explanation exists. The message may be passed as an
interpolated string or a `MessageData` term. The result of `getRef` is used as position information.
 -/
Lean.Parser.Term.throwNamedErrorMacro : Lean.Parser.Parser
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.coe_natCast : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : AddCommGroupWithOne R] (n : ℕ), ↑↑n = ↑n
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.hom_hom_ofHom : ∀ {X Y : Type u} [inst : Nonempty X] [inst_1 : LinearOrder X] [inst_2 : Fintype X] [inst_3 : Nonempty Y]
  [inst_4 : LinearOrder Y] [inst_5 : Fintype Y] (f : X →o Y), LinOrd.Hom.hom (NonemptyFinLinOrd.ofHom f).hom = f
-- Std.Async.Basic
Std.Async.BaseAsync.instMonad : Monad Std.Async.BaseAsync
-- Mathlib.Probability.Kernel.Disintegration.CondCDF
/-- Conditional cdf of the measure given the value on `α`, as a Stieltjes function.  -/
ProbabilityTheory.condCDF : {α : Type u_1} → {mα : MeasurableSpace α} → MeasureTheory.Measure (α × ℝ) → α → StieltjesFunction ℝ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_union!_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k fallback : α},
        Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.union! m₂).getKeyD k fallback = m₂.getKeyD k fallback
-- Mathlib.Tactic.Sat.FromLRAT
Sat.Fmla.reify.mk : ∀ {v : Sat.Valuation} {f : Sat.Fmla} {p : Prop}, (¬v.satisfies_fmla f → p) → Sat.Fmla.reify v f p
-- Mathlib.NumberTheory.FactorisationProperties
Nat.Weird.pos : ∀ {n : ℕ}, n.Weird → 0 < n
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.ext_getKey_getElem?_iff : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {m₁ m₂ : Std.ExtHashMap α β},
  m₁ = m₂ ↔ (∀ (k : α) (hk : k ∈ m₁) (hk' : k ∈ m₂), m₁.getKey k hk = m₂.getKey k hk') ∧ ∀ (k : α), m₁[k]? = m₂[k]?
-- Init.Control.ExceptCps
/-- Returns the value of a computation, forgetting whether it was an exception or a success.

This corresponds to early return.
 -/
ExceptCpsT.runCatch : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → ExceptCpsT α m α → m α
-- Lean.Widget.Diff
_private.Lean.Widget.Diff.0.Lean.Widget.ExprDiff.mk.injEq : ∀ (changesBefore changesAfter changesBefore_1 changesAfter_1 : Lean.SubExpr.PosMap Lean.Widget.ExprDiffTag✝),
  ({ changesBefore := changesBefore, changesAfter := changesAfter } =
      { changesBefore := changesBefore_1, changesAfter := changesAfter_1 }) =
    (changesBefore = changesBefore_1 ∧ changesAfter = changesAfter_1)
-- Mathlib.NumberTheory.NumberField.InfiniteAdeleRing
NumberField.instCommRingInfiniteAdeleRing : (K : Type u_1) → [inst : Field K] → CommRing (NumberField.InfiniteAdeleRing K)
-- Mathlib.Order.Defs.Unbundled
Equivalence.of_isEquiv : ∀ {α : Sort u_1} (lt : α → α → Prop) [IsEquiv α lt], Equivalence lt
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
/-- The composition of `Ext`, as a bilinear map.  -/
CategoryTheory.Abelian.Ext.bilinearComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : CategoryTheory.HasExt C] →
        (X Y Z : C) →
          (a b c : ℕ) →
            a + b = c →
              CategoryTheory.Abelian.Ext X Y a →+ CategoryTheory.Abelian.Ext Y Z b →+ CategoryTheory.Abelian.Ext X Z c
-- Mathlib.Analysis.Seminorm
Seminorm.instSeminormClass : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E],
  SeminormClass (Seminorm 𝕜 E) 𝕜 E
-- Mathlib.Topology.Instances.AddCircle.DenseSubgroup
/-- The multiples of a number `a` are dense on a circle of length `p > 0`
iff `a` has infinite additive order.  -/
AddCircle.denseRange_zsmul_iff : ∀ {p : ℝ} [Fact (0 < p)] {a : AddCircle p}, (DenseRange fun x => x • a) ↔ addOrderOf a = 0
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k fallback : α}, k ∉ m₂ → (m₁ ∩ m₂).getKeyD k fallback = fallback
-- Mathlib.MeasureTheory.Integral.Asymptotics
/-- If `f` is locally integrable, `‖f(-x)‖ = ‖f(x)‖`, and `f =O[atTop] g`, for some
`g` integrable at `atTop`, then `f` is integrable.  -/
MeasureTheory.LocallyIntegrable.integrable_of_isBigO_atTop_of_norm_isNegInvariant : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] {f : α → E} {g : α → F}
  [inst_1 : TopologicalSpace α] [SecondCountableTopology α] [inst_3 : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_4 : NormedAddCommGroup F] [inst_5 : AddCommGroup α] [inst_6 : LinearOrder α] [IsOrderedAddMonoid α]
  [CompactIccSpace α] [Filter.atTop.IsMeasurablyGenerated] [MeasurableNeg α] [μ.IsNegInvariant],
  MeasureTheory.LocallyIntegrable f μ →
    norm ∘ f =ᵐ[μ] norm ∘ f ∘ Neg.neg →
      f =O[Filter.atTop] g → MeasureTheory.IntegrableAtFilter g Filter.atTop μ → MeasureTheory.Integrable f μ
-- Mathlib.RepresentationTheory.Basic
Representation.norm_self_apply : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Group G] [inst_2 : Fintype G]
  [inst_3 : AddCommMonoid V] [inst_4 : Module k V] (ρ : Representation k G V) (g : G) (x : V),
  ρ.norm ((ρ g) x) = ρ.norm x
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instUnique : (A : Type u_3) → (E : Type u_4) → [Unique E] → Unique (WithCStarModule A E)
-- Lean.Meta.Match.Match
Lean.Meta.Match.State.mk.injEq : ∀ (used : Std.HashSet ℕ) (overlaps : Lean.Meta.Match.Overlaps) (counterExamples : Array (List Lean.Meta.Match.Example))
  (used_1 : Std.HashSet ℕ) (overlaps_1 : Lean.Meta.Match.Overlaps)
  (counterExamples_1 : Array (List Lean.Meta.Match.Example)),
  ({ used := used, overlaps := overlaps, counterExamples := counterExamples } =
      { used := used_1, overlaps := overlaps_1, counterExamples := counterExamples_1 }) =
    (used = used_1 ∧ overlaps = overlaps_1 ∧ counterExamples = counterExamples_1)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- A functor between preadditive categories that preserves (zero morphisms and) finite biproducts
preserves finite products.  -/
CategoryTheory.Limits.preservesProduct_of_preservesBiproduct : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {J : Type u_1} [Finite J] {f : J → C}
  [CategoryTheory.Limits.PreservesBiproduct f F],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) F
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Auxiliary definition for `vComp`.  -/
CategoryTheory.Lax.OplaxTrans.vCompApp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G H : CategoryTheory.LaxFunctor B C} →
          CategoryTheory.Lax.OplaxTrans F G → CategoryTheory.Lax.OplaxTrans G H → (a : B) → F.obj a ⟶ H.obj a
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_empty : ∀ (R : Type uR) (A : Type uA) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A], R[] = ⊥
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_mulRight : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : InvolutiveStar R] {E : Type u_6} [inst_2 : NonUnitalNonAssocSemiring E]
  [inst_3 : StarRing E] [inst_4 : Module R E] [inst_5 : StarModule R E] [inst_6 : SMulCommClass R E E]
  [inst_7 : IsScalarTower R E E] (x : E),
  star (WithConv.toConv (LinearMap.mulRight R x)) = WithConv.toConv (LinearMap.mulLeft R (star x))
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_of_support_subset : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] (f : α →₀ M) {s : Finset α},
  f.support ⊆ s → ∀ (g : α → M → N), (∀ i ∈ s, g i 0 = 1) → f.prod g = ∏ x ∈ s, g x (f x)
-- Mathlib.Data.ENat.Basic
/-- **Alias** of `ENat.natCast_lt_natCast`. -/
ENat.coe_lt_coe : ∀ {n m : ℕ}, ↑n < ↑m ↔ n < m
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
/-- Checking exact limits of shape `Discrete ℕ` is enough for countable AB4\*, provided that the
category has finite biproducts and finite colimits.
 -/
CategoryTheory.CountableAB4Star.of_hasExactLimitsOfShape_nat : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteBiproducts C] [CategoryTheory.Limits.HasFiniteColimits C]
  [inst_4 : CategoryTheory.Limits.HasCountableProducts C]
  [CategoryTheory.HasExactLimitsOfShape (CategoryTheory.Discrete ℕ) C], CategoryTheory.CountableAB4Star C
-- Std.Data.ExtHashMap.Lemmas
/-- Simpler variant of `getElem?_filter` when `LawfulBEq` is available.  -/
Std.ExtHashMap.getElem?_filter' : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α]
  {f : α → β → Bool} {k : α}, (Std.ExtHashMap.filter f m)[k]? = Option.filter (f k) m[k]?
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
/-- If `H : C ⥤ D` is an additive functor and `φ` is a morphism of cochain complexes
in `C`, this is the comparison isomorphism (in each degree `n`) between the image
by `H` of `mappingCone φ` and the mapping cone of the image by `H` of `φ`.
It is an auxiliary definition for `mapHomologicalComplexXIso` and
`mapHomologicalComplexIso`. This definition takes an extra
parameter `m : ℤ` such that `n + 1 = m` which may help getting better
definitional properties. See also the equational lemma `mapHomologicalComplexXIso_eq`.  -/
CochainComplex.mappingCone.mapHomologicalComplexXIso' : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v', u_2} D] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Preadditive D] →
            {F G : CochainComplex C ℤ} →
              (φ : F ⟶ G) →
                [inst_4 : HomologicalComplex.HasHomotopyCofiber φ] →
                  (H : CategoryTheory.Functor C D) →
                    [inst_5 : H.Additive] →
                      [inst_6 :
                          HomologicalComplex.HasHomotopyCofiber ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)] →
                        (n m : ℤ) →
                          n + 1 = m →
                            (((H.mapHomologicalComplex (ComplexShape.up ℤ)).obj (CochainComplex.mappingCone φ)).X n ≅
                              (CochainComplex.mappingCone ((H.mapHomologicalComplex (ComplexShape.up ℤ)).map φ)).X n)
-- Mathlib.Tactic.ClickSuggestions.Rewrite
Mathlib.Tactic.ClickSuggestions.RwInfo.mk.injEq : ∀ (rootExpr subExpr : Lean.Expr) (rflTarget? : Option Lean.Expr) (pos : Lean.SubExpr.Pos)
  (rwKind : Mathlib.Tactic.ClickSuggestions.RwKind) (rootExpr_1 subExpr_1 : Lean.Expr) (rflTarget?_1 : Option Lean.Expr)
  (pos_1 : Lean.SubExpr.Pos) (rwKind_1 : Mathlib.Tactic.ClickSuggestions.RwKind),
  ({ rootExpr := rootExpr, subExpr := subExpr, rflTarget? := rflTarget?, pos := pos, rwKind := rwKind } =
      { rootExpr := rootExpr_1, subExpr := subExpr_1, rflTarget? := rflTarget?_1, pos := pos_1, rwKind := rwKind_1 }) =
    (rootExpr = rootExpr_1 ∧ subExpr = subExpr_1 ∧ rflTarget? = rflTarget?_1 ∧ pos = pos_1 ∧ rwKind = rwKind_1)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- The cotrident built from `wideCoequalizer.π f` is colimiting.  -/
CategoryTheory.Limits.wideCoequalizerIsWideCoequalizer : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {X Y : C} →
        (f : J → (X ⟶ Y)) →
          [inst_1 : CategoryTheory.Limits.HasWideCoequalizer f] →
            [inst_2 : Nonempty J] →
              CategoryTheory.Limits.IsColimit
                (CategoryTheory.Limits.Cotrident.ofπ (CategoryTheory.Limits.wideCoequalizer.π f) ⋯)
-- Mathlib.Algebra.GroupWithZero.Defs
/-- Zero is a left absorbing element for multiplication  -/
CommMonoidWithZero.zero_mul : ∀ {M₀ : Type u_2} [self : CommMonoidWithZero M₀] (a : M₀), 0 * a = 0
-- Mathlib.Data.Fintype.Perm
length_permsOfList : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), (permsOfList l).length = l.length.factorial
-- Mathlib.Order.Category.Frm
Frm.hom_ext_iff : ∀ {X Y : Frm} {f g : X ⟶ Y}, f = g ↔ Frm.Hom.hom f = Frm.Hom.hom g
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_mul_factorial_mul_factorial : ∀ {n k : ℕ}, k ≤ n → n.choose k * k.factorial * (n - k).factorial = n.factorial
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.op_top : ∀ {R : Type u_2} [inst : NonAssocRing R], ⊤.op = ⊤
-- Mathlib.SetTheory.ZFC.Basic
/-- A set function is "definable" if it is the image of some n-ary `PSet`
function. This isn't exactly definability, but is useful as a sufficient
condition for functions that have a computable image.  -/
ZFSet.Definable : (n : ℕ) → ((Fin n → ZFSet.{u}) → ZFSet.{u}) → Type (u + 1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.foldM_eq_foldlM_toList : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {δ : Type w} {m' : Type w → Type w'} {β : Type v}
  {m : Std.DHashMap α fun x => β} [inst : Monad m'] [LawfulMonad m'] {f : δ → α → β → m' δ} {init : δ},
  Std.DHashMap.foldM f init m = List.foldlM (fun a b => f a b.1 b.2) init (Std.DHashMap.Const.toList m)
-- Mathlib.Data.Finset.Insert
Finset.notMem_singleton : ∀ {α : Type u_1} {a b : α}, a ∉ {b} ↔ a ≠ b
-- Plausible.Sampleable
Plausible.SampleableExt.sample : {α : Sort u} → [self : Plausible.SampleableExt α] → Plausible.Arbitrary (Plausible.SampleableExt.proxy α)
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivial.vectorBundle : ∀ (𝕜 : Type u_1) (B : Type u_2) (F : Type u_3) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] [inst_3 : TopologicalSpace B], VectorBundle 𝕜 F (Bundle.Trivial B F)
-- Mathlib.NumberTheory.ModularForms.Bounds
/-- A function on `ℍ` which is invariant under an arithmetic subgroup and bounded at all cusps,
is uniformly bounded.  -/
ModularGroup.exists_bound_of_subgroup_invariant : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] {f : UpperHalfPlane → E},
  Continuous f →
    (∀ (g : Matrix.SpecialLinearGroup (Fin 2) ℤ), UpperHalfPlane.IsBoundedAtImInfty fun τ => f (g • τ)) →
      ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [Γ.IsArithmetic],
        (∀ g ∈ Γ, ∀ (τ : UpperHalfPlane), f (g • τ) = f τ) → ∃ C, ∀ (τ : UpperHalfPlane), ‖f τ‖ ≤ C