mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- For a surjective `f : N →ₗ[R] P`,
the natural equivalence between `N ⊗[R] Q ⧸ (range (rTensor Q f))` and `P ⊗[R] Q`
(computably, given a right inverse)  -/
rTensor.linearEquiv_of_rightInverse : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {P : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      {f : M →ₗ[R] N} →
                        {g : N →ₗ[R] P} →
                          (Q : Type u_5) →
                            [inst_7 : AddCommGroup Q] →
                              [inst_8 : Module R Q] →
                                Function.Exact ⇑f ⇑g →
                                  {h : P → N} →
                                    Function.RightInverse h ⇑g →
                                      (TensorProduct R N Q ⧸ (LinearMap.rTensor Q f).range) ≃ₗ[R] TensorProduct R P Q
-- Init.Data.UInt.Bitwise
UInt32.shiftRight_xor : ∀ {a b c : UInt32}, (a ^^^ b) >>> c = a >>> c ^^^ b >>> c
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : α →*₀ β),
  f.comp (MonoidWithZeroHom.id α) = f
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.hf_modif_top : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (P : WeakFEPair E) (r : ℝ),
  (fun x => P.f_modif x - 0) =O[Filter.atTop] fun x => x ^ r
-- Init.Grind.Interactive
/-- Instantiates theorems using E-matching.
The `approx` modifier is just a marker for users to easily identify automatically generated `instantiate` tactics
that may have redundant arguments.
 -/
Lean.Parser.Tactic.Grind.instantiate : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.EqCnstrProof.neg.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Linear.EqCnstr), sizeOf (Lean.Meta.Grind.Arith.Linear.EqCnstrProof.neg c) = 1 + sizeOf c
-- Mathlib.Order.RelSeries
RelSeries.head_tail : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (len_pos : p.length ≠ 0), (p.tail len_pos).head = p.toFun 1
-- Mathlib.CategoryTheory.GuitartExact.HorizontalComposition
CategoryTheory.TwoSquare.GuitartExact.of_hComp' : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [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₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃]
  {V₁ : CategoryTheory.Functor C₁ D₁} {T₁ : CategoryTheory.Functor C₁ C₂} {B₁ : CategoryTheory.Functor D₁ D₂}
  {V₂ : CategoryTheory.Functor C₂ D₂} (w : CategoryTheory.TwoSquare T₁ V₁ V₂ B₁) {T₂ : CategoryTheory.Functor C₂ C₃}
  {B₂ : CategoryTheory.Functor D₂ D₃} {V₃ : CategoryTheory.Functor C₃ D₃} (w' : CategoryTheory.TwoSquare T₂ V₂ V₃ B₂)
  {T₁₂ : CategoryTheory.Functor C₁ C₃} {B₁₂ : CategoryTheory.Functor D₁ D₃} (eT : T₁.comp T₂ ≅ T₁₂)
  (eB : B₁.comp B₂ ≅ B₁₂) [B₁.EssSurj] [w.GuitartExact] [h : (w.hComp' w' eT eB).GuitartExact], w'.GuitartExact
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.Homotopy.h₁_assoc : ∀ {X Y : SSet} {A : X.Subcomplex} {B : Y.Subcomplex} {φ : A.toSSet ⟶ B.toSSet} {f g : SSet.RelativeMorphism A B φ}
  (self : f.Homotopy g) {Z : SSet} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp SSet.ι₁ (CategoryTheory.CategoryStruct.comp self.h h) =
    CategoryTheory.CategoryStruct.comp g.map h
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.chartAt_toPartialEquiv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (p : TangentBundle I M),
  (chartAt (ModelProd H E) p).toPartialEquiv =
    ((tangentBundleCore I M).toFiberBundleCore.localTrivAsPartialEquiv (achart H p.proj)).trans
      ((chartAt H p.proj).prod (PartialEquiv.refl E))
-- Mathlib.LinearAlgebra.Quotient.Basic
Submodule.ker_mapQ : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (p : Submodule R M)
  {R₂ : Type u_3} {M₂ : Type u_4} [inst_3 : Ring R₂] [inst_4 : AddCommGroup M₂] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  (q : Submodule R₂ M₂) (f : M →ₛₗ[τ₁₂] M₂) (h : p ≤ Submodule.comap f q),
  (p.mapQ q f h).ker = Submodule.map p.mkQ (Submodule.comap f q)
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.subRight : ∀ {R : Type u} {X : Type v} [inst : CommRing R] {a b : FreeNonUnitalNonAssocAlgebra R X}
  (c : FreeNonUnitalNonAssocAlgebra R X), FreeLieAlgebra.Rel R X a b → FreeLieAlgebra.Rel R X (a - c) (b - c)
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.leadingCoeff_toLex : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} [inst_1 : LinearOrder σ],
  AddMonoidAlgebra.leadingCoeff (⇑toLex) p = MvPolynomial.coeff (ofLex (AddMonoidAlgebra.supDegree (⇑toLex) p)) p
-- Mathlib.Algebra.Group.Ext
CommMonoid.toMonoid_injective : ∀ {M : Type u}, Function.Injective (@CommMonoid.toMonoid M)
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.Hom.hom.eq_1 : ∀ {X Y : AddCommMonCat} (f : X.Hom Y), f.hom = CategoryTheory.ConcreteCategory.hom f
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.contains_of_contains_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {f : α → Bool} {k : α},
  (Std.ExtTreeSet.filter f t).contains k = true → t.contains k = true
-- Mathlib.Algebra.Order.Group.Action.Synonym
OrderDual.instSMulCommClass_2 : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : SMul N α] [SMulCommClass M N α],
  SMulCommClass M N αᵒᵈ
-- Std.Async.Basic
/-- A `Task` that may resolve to a value or an error value of type `IO.Error`. Alias for `ETask IO.Error`.
 -/
Std.Async.AsyncTask : Type → Type
-- Init.Data.Repr
/-- We statically allocate and memoize reprs for small natural numbers.  -/
_private.Init.Data.Repr.0.Nat.reprArray : Array String
-- Batteries.Recycling.RBTree.Lemmas
/-- The value `x` returned by `upperBoundP?` is greater or equal to the `cut`.  -/
RBTree.RBSet.upperBoundP?_ge : ∀ {α : Type u_1} {cmp : α → α → Ordering} {cut : α → Ordering} {x : α} {t : RBTree.RBSet α cmp},
  t.upperBoundP? cut = some x → cut x ≠ Ordering.gt
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.addKeywordCompletionItem : String → Lean.Server.Completion.M✝ Unit
-- Mathlib.Probability.Density
ProbabilityTheory.IndepFun.pdf_add_eq_lconvolution_pdf : ∀ {Ω : Type u_1} {G : Type u_2} {mΩ : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω} [inst : AddGroup G]
  {mG : MeasurableSpace G} [MeasurableAdd₂ G] [MeasurableNeg G] {μ : MeasureTheory.Measure G} [μ.IsAddLeftInvariant]
  {X Y : Ω → G} [MeasureTheory.SFinite μ] [MeasureTheory.HasPDF X ℙ μ] [MeasureTheory.HasPDF Y ℙ μ]
  [MeasureTheory.IsFiniteMeasure ℙ],
  ProbabilityTheory.IndepFun X Y ℙ →
    MeasureTheory.pdf (X + Y) ℙ μ =ᵐ[μ] MeasureTheory.lconvolution (MeasureTheory.pdf X ℙ μ) (MeasureTheory.pdf Y ℙ μ) μ
-- Lean.Message
/-- Produces a `MessageData` tagged with an identifier for error `name`.

Note: this function generally should not be called directly; instead, use the macros `logNamedError`
and `throwNamedError`.
 -/
Lean.MessageData.tagWithErrorName : Lean.MessageData → Lean.Name → Lean.MessageData
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.mk : (toProfinite : Profinite) →
  [group : Group ↑toProfinite.toTop] → [topologicalGroup : IsTopologicalGroup ↑toProfinite.toTop] → ProfiniteGrp.{u}
-- Std.Net.Addr
Std.Net.instInhabitedAddressFamily : Inhabited Std.Net.AddressFamily
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.mem_saturation_of_mul_mem_right : ∀ {R : Type u_1} {S : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  {s : Subalgebra R S} {M : Submonoid S} {H : M ≤ s.toSubmonoid} {x y : S},
  x * y ∈ s.saturation M H → y ∈ M → x ∈ s.saturation M H
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- The second projection `ROfRel ⟶ X`.  -/
TypeCat.p₂OfRel : {X : Type w} → (φ : X → X → Prop) → TypeCat.ROfRel φ ⟶ X
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- The eigenvalues of a self-adjoint operator are real.  -/
LinearMap.IsSymmetric.conj_eigenvalue_eq_self : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E}, T.IsSymmetric → ∀ {μ : 𝕜}, Module.End.HasEigenvalue T μ → (starRingEnd 𝕜) μ = μ
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.nonempty_uIoc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b : α}, (Set.uIoc a b).Nonempty ↔ a ≠ b
-- Mathlib.MeasureTheory.Group.ModularCharacter
MeasureTheory.Measure.map_right_add_eq_addModularCharacterFun_vadd : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [inst_2 : IsTopologicalAddGroup G]
  [inst_3 : LocallyCompactSpace G] [inst_4 : MeasurableSpace G] [BorelSpace G] (μ : MeasureTheory.Measure G)
  [μ.IsAddHaarMeasure] [μ.InnerRegular] (g : G),
  MeasureTheory.Measure.map (fun x => x + g) μ = MeasureTheory.Measure.addModularCharacterFun g • μ
-- Lean.Meta.Tactic.Apply
_private.Lean.Meta.Tactic.Apply.0.Lean.MVarId.splitAndCore.go : Lean.Name → Lean.Expr → StateRefT' IO.RealWorld (Array Lean.MVarId) Lean.MetaM Lean.Expr
-- Mathlib.CategoryTheory.Monad.Comonadicity
CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction_counit_f : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C} {adj : F ⊣ G}
  [inst_2 : ∀ (A : adj.toComonad.Coalgebra), CategoryTheory.Limits.HasEqualizer (G.map A.a) (adj.unit.app (G.obj A.A))]
  (A : adj.toComonad.Coalgebra),
  ((CategoryTheory.Comonad.ComonadicityInternal.comparisonAdjunction adj).counit.app A).f =
    (CategoryTheory.Comonad.beckEqualizer A).lift (CategoryTheory.Comonad.ComonadicityInternal.counitFork A)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int64.reduceToInt : Lean.Meta.Simp.DSimproc
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.instPreservesColimitDiscreteFunctorObjFunctorEval : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} A]
  [inst_2 : CategoryTheory.Limits.HasCoproducts A] (J : Type w) (f : J → CategoryTheory.Limits.FormalCoproduct C)
  (F : CategoryTheory.Functor C A),
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Discrete.functor f)
    ((CategoryTheory.Limits.FormalCoproduct.eval C A).obj F)
-- Mathlib.LinearAlgebra.TensorProduct.Quotient
/-- Left tensoring a module with a quotient of the ring is the same as
quotienting that module by the corresponding submodule.  -/
TensorProduct.quotTensorEquivQuotSMul : {R : Type u_1} →
  (M : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (I : Ideal R) → TensorProduct R (R ⧸ I) M ≃ₗ[R] M ⧸ I • ⊤
-- Mathlib.Condensed.Discrete.Colimit
/-- The restriction of a finite-product-preserving presheaf `F` on `Profinite` to the category of
finite sets is isomorphic to `finYoneda F`.
 -/
Condensed.isoFinYoneda : (F : CategoryTheory.Functor Profiniteᵒᵖ (Type (u + 1))) →
  [CategoryTheory.Limits.PreservesFiniteProducts F] → FintypeCat.toProfinite.op.comp F ≅ Condensed.finYoneda F
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.comap_bot' : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] (f : F), Submonoid.comap f ⊥ = MonoidHom.mker f
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
SSet.Subcomplex.Pairing.RankFunction.Cell.subcomplex_not_le_image_horn : ∀ {X : SSet} {A : X.Subcomplex} {P : A.Pairing} {ι : Type v} [inst : LinearOrder ι] {f : P.RankFunction ι} {i : ι}
  (c : f.Cell i) [inst_1 : P.IsProper], ¬(↑c.s).subcomplex ≤ c.horn.image c.map
-- Std.Internal.Do.Triple.Basic
Std.Internal.Do.Triple.map : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Monad m] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred]
  {α β : Type u} {pre : Pred} {post : β → Pred} {epost : EPred} [LawfulMonad m] (f : α → β) (x : m α),
  ⦃ pre ⦄ x ⦃ fun a => post (f a); epost ⦄ → ⦃ pre ⦄ f <$> x ⦃ post; epost ⦄
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.AddConvolutionExists.add_distrib : ∀ {M : Type u_1} {S : Type u_2} {E : Type u_3} {E' : Type u_4} {F : Type u_6} [inst : AddMonoid M]
  [inst_1 : CommSemiring S] [inst_2 : AddCommMonoid E] [inst_3 : AddCommMonoid E'] [inst_4 : AddCommMonoid F]
  [inst_5 : Module S E] [inst_6 : Module S E'] [inst_7 : Module S F] [inst_8 : TopologicalSpace F] [T2Space F]
  [ContinuousAdd F] {f f' : M → E} {g : M → E'} (L : E →ₗ[S] E' →ₗ[S] F),
  DiscreteConvolution.AddConvolutionExists L f g →
    DiscreteConvolution.AddConvolutionExists L f' g →
      DiscreteConvolution.addConvolution L (f + f') g =
        DiscreteConvolution.addConvolution L f g + DiscreteConvolution.addConvolution L f' g
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremKind.eqBoth.sizeOf_spec : ∀ (gen : Bool), sizeOf (Lean.Meta.Grind.EMatchTheoremKind.eqBoth gen) = 1 + sizeOf gen
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.dvd_C_mul_X_sub_one_pow_add_one : ∀ {R : Type u_1} [inst : CommRing R] {p : ℕ},
  Nat.Prime p →
    p ≠ 2 → ∀ (a r : R), r ∣ a ^ p → r ∣ ↑p * a → Polynomial.C r ∣ (Polynomial.C a * Polynomial.X - 1) ^ p + 1
-- Lean.Data.Json.Basic
Lean.Json.instHashable : Hashable Lean.Json
-- Mathlib.Topology.NoetherianSpace
/-- Spaces that are both Noetherian and Hausdorff are finite.  -/
TopologicalSpace.NoetherianSpace.finite : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.NoetherianSpace α] [T2Space α], Finite α
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.sc₃_f : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n₀ n₁ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.sc₃._auto_1),
  (X.sc₃ f g fg h n₀ n₁ hn₁).f = (X.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)
-- Std.Time.Date.Unit.Week
Std.Time.Week.OfYear.instTransOrdOrdinal : Std.TransOrd Std.Time.Week.OfYear.Ordinal
-- Mathlib.Data.Fin.Basic
Fin.modNat_rev : ∀ {n m : ℕ} (i : Fin (m * n)), i.rev.modNat = i.modNat.rev
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHomClass.toMonoidHomClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : Semiring A} {inst_2 : Algebra R A} {inst_3 : Semiring B} {inst_4 : Algebra R B}
  {inst_5 : CoalgebraStruct R A} {inst_6 : CoalgebraStruct R B} {inst_7 : FunLike F A B} [self : BialgHomClass F R A B],
  MonoidHomClass F A B
-- Mathlib.Analysis.Calculus.FDeriv.Analytic
FormalMultilinearSeries.derivSeries_apply_diag : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type v} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  (p : FormalMultilinearSeries 𝕜 E F) (n : ℕ) (x : E),
  ((p.derivSeries n) fun x_1 => x) x = (n + 1) • (p (n + 1)) fun x_1 => x
-- Mathlib.Order.Heyting.Hom
/-- Composition of `HeytingHom`s as a `HeytingHom`.  -/
HeytingHom.comp : {α : Type u_2} →
  {β : Type u_3} →
    {γ : Type u_4} →
      [inst : HeytingAlgebra α] →
        [inst_1 : HeytingAlgebra β] → [inst_2 : HeytingAlgebra γ] → HeytingHom β γ → HeytingHom α β → HeytingHom α γ
-- Mathlib.Order.CompleteLatticeIntervals
subset_sInf_of_not_bddBelow : ∀ {α : Type u_2} (s : Set α) [inst : Preorder α] [inst_1 : InfSet α] [inst_2 : Inhabited ↑s] {t : Set ↑s},
  ¬BddBelow t → sInf t = default
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Embedding.subtype_equivRange : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f : L.Embedding M N), f.toHom.range.subtype.comp f.equivRange.toEmbedding = f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonCallHierarchyItem : Lean.FromJson Lean.Lsp.CallHierarchyItem
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.toPoly'.eq_1 : ∀ (e : Int.Internal.Linear.Expr), e.toPoly' = Int.Internal.Linear.Expr.toPoly'.go 1 e (Int.Internal.Linear.Poly.num 0)
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instCommMonoidOfContinuousMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] → [inst_2 : CommMonoid β] → [ContinuousMul β] → CommMonoid C(α, β)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.support_esymm : ∀ (σ : Type u_5) (R : Type u_6) [inst : CommSemiring R] [inst_1 : Fintype σ] [inst_2 : DecidableEq σ] [Nontrivial R]
  (n : ℕ),
  (MvPolynomial.esymm σ R n).support =
    Finset.image (fun t => ∑ i ∈ t, fun₀ | i => 1) (Finset.powersetCard n Finset.univ)
-- Mathlib.Data.Set.Basic
Set.ssubset_iff_exists : ∀ {α : Type u} {s t : Set α}, s ⊂ t ↔ s ⊆ t ∧ ∃ x ∈ t, x ∉ s
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- an endomorphism of the object  -/
CategoryTheory.Idempotents.Karoubi.p : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → (self : CategoryTheory.Idempotents.Karoubi C) → self.X ⟶ self.X
-- Mathlib.ModelTheory.Encoding
FirstOrder.Language.BoundedFormula.listDecode.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} (x : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)),
  FirstOrder.Language.BoundedFormula.listDecode x =
    match x with
    | Sum.inr (Sum.inr n.succ.succ) :: l =>
      ⟨n, FirstOrder.Language.BoundedFormula.falsum⟩ :: FirstOrder.Language.BoundedFormula.listDecode l
    | Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l =>
      (if h : n₁ = n₂ then ⟨n₁, FirstOrder.Language.BoundedFormula.equal t₁ (⋯.mp t₂)⟩ else default) ::
        FirstOrder.Language.BoundedFormula.listDecode l
    | Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l =>
      (if h : ∀ (i : Fin n), (List.map Sum.getLeft? l)[i]?.join.isSome = true then
          if h' : ∀ (i : Fin n), ((List.map Sum.getLeft? l)[i]?.join.get ⋯).fst = k then
            ⟨k, FirstOrder.Language.BoundedFormula.rel R fun i => ⋯.mp ((List.map Sum.getLeft? l)[i]?.join.get ⋯).snd⟩
          else default
        else default) ::
        FirstOrder.Language.BoundedFormula.listDecode (List.drop n l)
    | Sum.inr (Sum.inr 0) :: l =>
      if h : 2 ≤ (FirstOrder.Language.BoundedFormula.listDecode l).length then
        FirstOrder.Language.BoundedFormula.sigmaImp (FirstOrder.Language.BoundedFormula.listDecode l)[0]
            (FirstOrder.Language.BoundedFormula.listDecode l)[1] ::
          List.drop 2 (FirstOrder.Language.BoundedFormula.listDecode l)
      else []
    | Sum.inr (Sum.inr 1) :: l =>
      if h : 1 ≤ (FirstOrder.Language.BoundedFormula.listDecode l).length then
        FirstOrder.Language.BoundedFormula.sigmaAll (FirstOrder.Language.BoundedFormula.listDecode l)[0] ::
          List.drop 1 (FirstOrder.Language.BoundedFormula.listDecode l)
      else []
    | x => []
-- Init.Data.BitVec.Lemmas
BitVec.cpopNatRec_of_le : ∀ {w acc : ℕ} {x : BitVec w} (k n : ℕ), w ≤ n → x.cpopNatRec (n + k) acc = x.cpopNatRec n acc
-- Batteries.Tactic.PrintPrefix
_private.Batteries.Tactic.PrintPrefix.0.Batteries.Tactic.matchingConstants : Batteries.Tactic.PrintPrefixConfig → Lean.Name → Lean.MetaM (Array Lean.MessageData)
-- Mathlib.Data.List.Lattice
List.bagInter_singleton : ∀ {α : Type u_1} {l₁ : List α} [inst : DecidableEq α] (a : α), l₁.bagInter [a] = if a ∈ l₁ then [a] else []
-- Mathlib.Analysis.Distribution.FourierMultiplier
TemperedDistribution.fourierMultiplierCLM_smul : ∀ {E : Type u_3} {F : Type u_4} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : NormedSpace ℂ F] [inst_4 : FiniteDimensional ℝ E]
  [inst_5 : MeasurableSpace E] [inst_6 : BorelSpace E] {g : E → ℂ},
  Function.HasTemperateGrowth g →
    ∀ (c : ℂ), TemperedDistribution.fourierMultiplierCLM F (c • g) = c • TemperedDistribution.fourierMultiplierCLM F g
-- Mathlib.Topology.Separation.GDelta
Set.Countable.isGδ_compl : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X} [T1Space X], s.Countable → IsGδ sᶜ
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.restrict_closure_eq' : ∀ {α : Type u_2} (M : Matroid α) (X R : Set α), (M.restrict R).closure X = M.closure (X ∩ R) ∩ R ∪ R \ M.E
-- Mathlib.Combinatorics.Matroid.Rank.Finite
/-- **Alias** of `Matroid.IsRkFinite.isRkFinite_sdiff_iff`. -/
Matroid.IsRkFinite.isRkFinite_diff_iff : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, M.IsRkFinite X → (M.IsRkFinite (Y \ X) ↔ M.IsRkFinite Y)
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) {i' j' k' : ι} (f' : i' ⟶ j')
  (g' : j' ⟶ k') (fg : i ⟶ k) (h : CategoryTheory.CategoryStruct.comp f g = fg) (fg' : i' ⟶ k')
  (h' : CategoryTheory.CategoryStruct.comp f' g' = fg')
  (α : CategoryTheory.ComposableArrows.mk₂ f g ⟶ CategoryTheory.ComposableArrows.mk₂ f' g')
  (β : CategoryTheory.ComposableArrows.mk₁ fg ⟶ CategoryTheory.ComposableArrows.mk₁ fg') (n : ℤ),
  autoParam (β.app 0 = α.app 0) CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles._auto_1 →
    autoParam (β.app 1 = α.app 2) CategoryTheory.Abelian.SpectralObject.opcyclesMap_fromOpcycles._auto_3 →
      ∀ {Z : C} (h_1 : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ fg') ⟶ Z),
        CategoryTheory.CategoryStruct.comp (X.opcyclesMap f g f' g' α n)
            (CategoryTheory.CategoryStruct.comp (X.fromOpcycles f' g' fg' h' n) h_1) =
          CategoryTheory.CategoryStruct.comp (X.fromOpcycles f g fg h n)
            (CategoryTheory.CategoryStruct.comp ((X.H n).map β) h_1)
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.LawfulZipOperator.denote_prefix_cast_ref : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α}
  {input1 input2 : aig.BinaryInput} {f : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α}
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput f] [Std.Sat.AIG.RefVec.LawfulZipOperator α f]
  {h : aig.decls.size ≤ (f aig input1).aig.decls.size},
  ⟦assign, f (f aig input1).aig (input2.cast h)⟧ = ⟦assign, f aig input2⟧
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f + g) x = f x + g x` is a commatative additive
semigroup if `β` is a commatative additive semigroup.  -/
FunLike.addCommSemigroup : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] → [inst_2 : AddCommSemigroup β] → [IsAddApply F α β] → AddCommSemigroup F
-- Mathlib.Order.UpperLower.Basic
/-- **Alias** of the forward direction of `isUpperSet_iff_Ici_subset`. -/
IsUpperSet.Ici_subset : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, IsUpperSet s → ∀ ⦃a : α⦄, a ∈ s → Set.Ici a ⊆ s
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.BitVec
/-- Simplification procedure for `clz` (count leading zeros) on `BitVec`.  -/
BitVec.reduceClz : Lean.Meta.Simp.DSimproc