mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.FinallySmall
/-- Constructor for `InitialSmall C` from an explicit small category witness.  -/
CategoryTheory.InitiallySmall.mk' : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {S : Type w} [inst_1 : CategoryTheory.SmallCategory S]
  (F : CategoryTheory.Functor S J) [F.Initial], CategoryTheory.InitiallySmall J
-- Mathlib.GroupTheory.Commutator.Basic
map_commutator_eq : ∀ (G : Type u_1) [inst : Group G] {H : Type u_4} [inst_1 : Group H] (f : G →* H),
  Subgroup.map f (commutator G) = ⁅f.range, f.range⁆
-- Lean.Environment
/-- `findAsync?` after `base` access  -/
_private.Lean.Environment.0.Lean.Environment.findAsyncCore? : Lean.Environment → Lean.Name → optParam Bool false → Option Lean.AsyncConstantInfo
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.op_closure : ∀ {M : Type u_2} [inst : MulOneClass M] (s : Set M),
  (Submonoid.closure s).op = Submonoid.closure (MulOpposite.unop ⁻¹' s)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.tan_arctan : ∀ (x : ℝ), Real.tan (Real.arctan x) = x
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddMemClass.coe_subtype : ∀ {M : Type u_1} {A : Type u_3} [inst : Add M] [inst_1 : SetLike A M] [hA : AddMemClass A M] (S' : A),
  ⇑(AddMemClass.subtype S') = Subtype.val
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- Eta-expanded form of `ContDiff.inv` -/
ContDiff.fun_inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {𝕜' : Type u_4} [inst_3 : NormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {f : E → 𝕜'}, ContDiff 𝕜 n f → (∀ (x : E), f x ≠ 0) → ContDiff 𝕜 n fun i => (f i)⁻¹
-- Lean.Elab.DocString
/-- Retrieves a repeated named argument from the arguments to a documentation extension.
 -/
Lean.Doc.getMany : {α : Type} → [Lean.Doc.FromDocArg α] → Lean.Name → StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM (Array α)
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.RationalMap.toPartialMap.congr_simp : ∀ {X Y : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsReduced X] [inst_1 : Y.IsSeparated]
  (f f_1 : X.RationalMap Y), f = f_1 → f.toPartialMap = f_1.toPartialMap
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.empty_head : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ}, Monoid.PushoutI.NormalWord.empty.head = 1
-- Mathlib.CategoryTheory.Groupoid.Grpd.Basic
CategoryTheory.Grpd.instInhabited : Inhabited CategoryTheory.Grpd
-- Init.Data.Slice.Array.Lemmas
Array.toArray_mkSlice_rco : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ}, Std.Slice.toArray (Std.Rco.Sliceable.mkSlice xs lo...hi) = xs.extract lo hi
-- Mathlib.Topology.Semicontinuity.Basic
lowerSemicontinuousOn_sum : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {ι : Type u_4} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ]
  {f : ι → α → γ} {a : Finset ι},
  (∀ i ∈ a, LowerSemicontinuousOn (f i) s) → LowerSemicontinuousOn (fun z => ∑ i ∈ a, f i z) s
-- Init.Data.String.Lemmas.Basic
String.Pos.nextn_zero : ∀ {s : String} {p : s.Pos}, p.nextn 0 = p
-- Mathlib.Probability.Kernel.Composition.Prod
/-- Product of two kernels. This is meaningful only when the kernels are s-finite.  -/
ProbabilityTheory.«term_×ₖ_» : Lean.TrailingParserDescr
-- Init.Data.UInt.Lemmas
UInt32.ofNat_uInt64ToNat : ∀ (n : UInt64), UInt32.ofNat n.toNat = n.toUInt32
-- Init.Data.Array.Basic
Array.drop_eq_extract : ∀ {α : Type u} {xs : Array α} {i : ℕ}, xs.drop i = xs.extract i
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.nsmul_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : AddMonoid γ] [inst_4 : ContinuousAdd γ] (f : C(β, γ)) (n : ℕ) (g : C(α, β)),
  (n • f).comp g = n • f.comp g
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.instFullOppositeFunctorTypeShrinkCoyoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C],
  CategoryTheory.shrinkCoyoneda.{w, v, u}.Full
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.isBoundedUnder_abs_atTop_iff : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜],
  (Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) Filter.atTop fun x => |Polynomial.eval x P|) ↔ P.degree ≤ 0
-- Batteries.Data.List.Lemmas
List.isChain_cons_of_isChain_cons_cons : ∀ {α : Type u_1} {R : α → α → Prop} {a b : α} {l : List α}, List.IsChain R (a :: b :: l) → List.IsChain R (b :: l)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.ofList_equiv_foldl : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {l : List (α × β)},
  (Std.TreeMap.Raw.ofList l cmp).Equiv (List.foldl (fun acc p => acc.insert p.1 p.2) ∅ l)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.instIsClosedUnderLimitsOfShapeOppositeOpOfIsClosedUnderColimitsOfShape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) (J : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} J] [P.IsClosedUnderColimitsOfShape J], P.op.IsClosedUnderLimitsOfShape Jᵒᵖ
-- Mathlib.Topology.Sheaves.Alexandrov
Alexandrov.isSheaf_principalsKanExtension : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasLimits C] {X : TopCat}
  [inst_2 : Preorder ↑X] [inst_3 : Topology.IsUpperSet ↑X] (F : CategoryTheory.Functor (↑X) C),
  TopCat.Presheaf.IsSheaf (Alexandrov.principalsKanExtension F)
-- Lean.Declaration
Lean.InductiveType.mk.injEq : ∀ (name : Lean.Name) (type : Lean.Expr) (ctors : List Lean.Constructor) (name_1 : Lean.Name) (type_1 : Lean.Expr)
  (ctors_1 : List Lean.Constructor),
  ({ name := name, type := type, ctors := ctors } = { name := name_1, type := type_1, ctors := ctors_1 }) =
    (name = name_1 ∧ type = type_1 ∧ ctors = ctors_1)
-- Mathlib.Geometry.Manifold.VectorBundle.LocalFrame
/-- **Alias** of `Bundle.Trivialization.localFrameCoeff_eq_coeff`.

---

Suppose `e` is a compatible trivialisation around `x ∈ M`, and `s` a bundle section.
Then the coefficient of `s` w.r.t. the local frame induced by `b` and `e`
equals the coefficient of "`s x` read in the trivialisation `e`" for `b i`.  -/
Bundle.Trivialization.localFrame_coeff_eq_coeff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] [inst_13 : VectorBundle 𝕜 F V] {ι : Type u_7}
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_14 : MemTrivializationAtlas e] {b : Module.Basis ι 𝕜 F}
  [inst_15 : ContMDiffVectorBundle 1 F V I] {x : M} {s : (x : M) → V x},
  x ∈ e.baseSet →
    ∀ {i : ι}, (Bundle.Trivialization.localFrameCoeff I e b i x) (s x) = (b.repr (↑e ((fun x => ⟨x, s x⟩) x)).2) i
-- Mathlib.Analysis.InnerProductSpace.Projection.Submodule
/-- If `K₁` admits an orthogonal projection and is contained in `K₂`,
then `K₁` and `K₁ᗮ ⊓ K₂` span `K₂`.  -/
Submodule.sup_orthogonal_inf_of_hasOrthogonalProjection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {K₁ K₂ : Submodule 𝕜 E}, K₁ ≤ K₂ → ∀ [K₁.HasOrthogonalProjection], K₁ ⊔ K₁ᗮ ⊓ K₂ = K₂
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.reverse_reverse : ∀ {α : Type u_1} {a : FreeAddMonoid α}, a.reverse.reverse = a
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonImportInfo : Lean.FromJson Lean.Lsp.ImportInfo
-- Mathlib.Algebra.Order.Group.Synonym
ofColex_eq_one : ∀ {α : Type u_1} [inst : One α] {a : Colex α}, ofColex a = 1 ↔ a = 1
-- Init.Data.BitVec.Lemmas
BitVec.not_and_self : ∀ {w : ℕ} (x : BitVec w), ~~~x &&& x = 0
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
hasFTaylorSeriesUpTo_zero_iff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : E → FormalMultilinearSeries 𝕜 E F}, HasFTaylorSeriesUpTo 0 f p ↔ Continuous f ∧ ∀ (x : E), (p x 0).curry0 = f x
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.preimageHomeomorph_symm_apply : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {s : Set B} (hb : s ⊆ e.baseSet) (p : ↑s × F),
  (e.preimageHomeomorph hb).symm p = ⟨↑e.symm (↑p.1, p.2), ⋯⟩
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- `esymmPart` is the product of the symmetric polynomials `esymm μᵢ`,
where `μ = (μ₁, μ₂, ...)` is a partition.
 -/
MvPolynomial.esymmPart : (σ : Type u_5) → (R : Type u_6) → [inst : CommSemiring R] → [Fintype σ] → {n : ℕ} → n.Partition → MvPolynomial σ R
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
/-- Choice of continuous left inverse for `f : F →L[R] E`, given that such an inverse exists.  -/
ContinuousLinearMap.HasLeftInverse.leftInverse : {R : Type u_1} →
  [inst : Semiring R] →
    {E : Type u_2} →
      {F : Type u_4} →
        [inst_1 : TopologicalSpace E] →
          [inst_2 : AddCommMonoid E] →
            [inst_3 : Module R E] →
              [inst_4 : TopologicalSpace F] →
                [inst_5 : AddCommMonoid F] → [inst_6 : Module R F] → {f : E →L[R] F} → f.HasLeftInverse → F →L[R] E
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.inclusionObj.match_1.splitter : {C : Type u_1} →
  (motive : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C → Sort u_2) →
    (x : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) →
      (Unit → motive CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.unit) →
        ((n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) → (a : C) → motive (n.tensor a)) → motive x
-- Mathlib.ModelTheory.Algebra.Ring.Definability
FirstOrder.Ring.mvPolynomial_zeroLocus_definable : ∀ {ι : Type u_1} {K : Type u_2} [inst : Field K] [inst_1 : FirstOrder.Ring.CompatibleRing K]
  (S : Finset (MvPolynomial ι K)),
  (⋃ p ∈ S, (fun m => MvPolynomial.coeff m p) '' ↑p.support).Definable FirstOrder.Language.ring
    (MvPolynomial.zeroLocus K (Ideal.span ↑S))
-- Mathlib.FieldTheory.RatFunc.Defs
RatFunc.ofFractionRing_injective : ∀ {K : Type u} [inst : CommRing K], Function.Injective RatFunc.ofFractionRing
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RcoSlice : (α : Type u_1) → Type u_2 → [Ord α] → Type (max u_2 u_1)
-- Lean.Expr
/-- Return `some e'` if `e = mkAnnotation kind e'`
 -/
Lean.annotation? : Lean.Name → Lean.Expr → Option Lean.Expr
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.decLevel?.processMax : Lean.Level → Lean.Level → Option Lean.Level
-- Init.Data.List.Sort.Impl
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.mergeSortTR.run : {α : Type u_1} → (α → α → Bool) → {n : ℕ} → { l // l.length = n } → List α
-- Mathlib.Data.Set.Lattice
Set.sUnion_symmDiff_sUnion_subset : ∀ {α : Type u_1} {S T : Set (Set α)},
  S.Nonempty → T.Nonempty → symmDiff (⋃₀ S) (⋃₀ T) ⊆ ⋃₀ Set.image2 (fun x1 x2 => symmDiff x1 x2) S T
-- Mathlib.MeasureTheory.Measure.Tilted
MeasureTheory.tilted_const : ∀ {α : Type u_1} {mα : MeasurableSpace α} (μ : MeasureTheory.Measure α) [MeasureTheory.IsProbabilityMeasure μ] (c : ℝ),
  (μ.tilted fun x => c) = μ
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.id_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  (E : J.OneHypercover S) (a : E.I₀), (CategoryTheory.CategoryStruct.id E).s₀ a = a
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.top_toSubmodule : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A], ⊤.toSubmodule = ⊤
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.coe_injective : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X], Function.Injective DFunLike.coe
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
DifferentiableWithinAt.sinh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E} {s : Set E},
  DifferentiableWithinAt ℝ f s x → DifferentiableWithinAt ℝ (fun x => Real.sinh (f x)) s x
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofFVarAliasInfo.injEq : ∀ (i i_1 : Lean.Elab.FVarAliasInfo), (Lean.Elab.Info.ofFVarAliasInfo i = Lean.Elab.Info.ofFVarAliasInfo i_1) = (i = i_1)
-- Mathlib.Order.Partition.Finpartition
Finpartition.subset : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} (P : Finpartition s) {a : Finset α}, a ∈ P.parts → a ⊆ s
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_eq_none_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a : α}, t.contains a = false → t.getKey? a = none
-- Mathlib.Data.Set.Insert
Set.subset_insert_iff_of_notMem : ∀ {α : Type u_1} {s t : Set α} {a : α}, a ∉ s → (s ⊆ insert a t ↔ s ⊆ t)
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.biUnion_assoc : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I)
  (πi : (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J)
  (πi' : BoxIntegral.Box ι → (J : BoxIntegral.Box ι) → BoxIntegral.Prepartition J),
  (π.biUnion fun J => (πi J).biUnion (πi' J)) = (π.biUnion πi).biUnion fun J => πi' (π.biUnionIndex πi J) J
-- Init.Data.UInt.Bitwise
UInt8.ofNatLT_xor : ∀ (a b : ℕ) (ha : a < 2 ^ 8) (hb : b < 2 ^ 8), UInt8.ofNatLT (a ^^^ b) ⋯ = UInt8.ofNatLT a ha ^^^ UInt8.ofNatLT b hb
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Poly.brecOn.go : {motive : Lean.Grind.Linarith.Poly → Sort u} →
  (t : Lean.Grind.Linarith.Poly) →
    ((t : Lean.Grind.Linarith.Poly) → Lean.Grind.Linarith.Poly.below t → motive t) →
      motive t ×' Lean.Grind.Linarith.Poly.below t
-- Mathlib.RingTheory.Finiteness.Defs
Submodule.fg_span_iff_fg_span_finset_subset : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
  (Submodule.span R s).FG ↔ ∃ s', ↑s' ⊆ s ∧ Submodule.span R s = Submodule.span R ↑s'
-- Mathlib.NumberTheory.Modular
/-- The standard fundamental domain truncated at height `y`.  -/
ModularGroup.truncatedFundamentalDomain : ℝ → Set UpperHalfPlane
-- Mathlib.Data.List.Forall2
List.SublistForall₂.brecOn : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}
  {motive : (a : List α) → (a_1 : List β) → List.SublistForall₂ R a a_1 → Prop} {a : List α} {a_1 : List β}
  (t : List.SublistForall₂ R a a_1),
  (∀ (a : List α) (a_2 : List β) (t : List.SublistForall₂ R a a_2), List.SublistForall₂.below t → motive a a_2 t) →
    motive a a_1 t
-- Mathlib.Analysis.Normed.Module.RCLike.Extend
StrongDual.toContinuousLinearEquiv_extendRCLikeₗᵢ : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup F] [inst_2 : NormedSpace 𝕜 F]
  [inst_3 : NormedSpace ℝ F] [inst_4 : IsScalarTower ℝ 𝕜 F], ↑StrongDual.extendRCLikeₗᵢ = StrongDual.extendRCLikeL
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHom_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G),
  CochainComplex.HomComplex.Cochain.ofHom (-φ) = -CochainComplex.HomComplex.Cochain.ofHom φ
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
LinearMap.restrictScalars.congr_simp : ∀ (R : Type u_1) {S : Type u_5} {M : Type u_8} {M₂ : Type u_10} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module S M] [inst_7 : Module S M₂] [inst_8 : LinearMap.CompatibleSMul M M₂ R S] (fₗ fₗ_1 : M →ₗ[S] M₂),
  fₗ = fₗ_1 → ↑R fₗ = ↑R fₗ_1
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.isFiltered_op_of_isCofiltered : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.IsCofiltered C], CategoryTheory.IsFiltered Cᵒᵖ
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMonC.go.eq_def : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (c : ℕ) (a : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulMonC.go k m c a =
    match a with
    | Lean.Grind.CommRing.Poly.num k' =>
      have k := k * k' % ↑c;
      bif k == 0 then Lean.Grind.CommRing.Poly.num 0
      else Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.num 0)
    | Lean.Grind.CommRing.Poly.add k' m' p =>
      have k_1 := k * k' % ↑c;
      bif k_1 == 0 then Lean.Grind.CommRing.Poly.mulMonC.go k m c p
      else Lean.Grind.CommRing.Poly.add k_1 (m.mul m') (Lean.Grind.CommRing.Poly.mulMonC.go k m c p)
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- The natural transformation of homology functors in a morphism of
`HomologyPretheory`s.  -/
TopPair.HomologyPretheory.Hom.hom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} → {HP HP' : TopPair.HomologyPretheory C c} → HP.Hom HP' → (i : ι) → HP.H i ⟶ HP'.H i
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.type₁_simplex : ∀ {X : SSet} {A : X.Subcomplex} (h : A.PairingCore) (s : h.ι), (h.type₁ s).simplex = h.simplex s
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.symm.sizeOf_spec : ∀ (c : Lean.Meta.Grind.Arith.Linear.RingEqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.symm c) = 1 + sizeOf c
-- Mathlib.Algebra.Homology.Augment
/-- A chain map from a chain complex to a single object chain complex in degree zero
can be reinterpreted as a chain complex.

This is the inverse construction of `truncateTo`.
 -/
ChainComplex.toSingle₀AsComplex : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject V] →
        (C : ChainComplex V ℕ) → (X : V) → (C ⟶ (ChainComplex.single₀ V).obj X) → ChainComplex V ℕ
-- Mathlib.Analysis.SpecialFunctions.BinaryEntropy
/-- Outside the usual range of `binEntropy`, it is negative. This is due to `log p = log |p|`  -/
Real.binEntropy_neg_of_one_lt : ∀ {p : ℝ}, 1 < p → Real.binEntropy p < 0
-- Init.Data.BitVec.Basic
/-- Transforms a bitvector of length `w` into a bitvector of length `v`, padding as needed with the most
significant bit's value.

If `x` is an empty bitvector, then the sign is treated as zero.

SMT-LIB name: `sign_extend`.
 -/
BitVec.signExtend : {w : ℕ} → (v : ℕ) → BitVec w → BitVec v
-- Mathlib.Tactic.ITauto
/-- Debugging printer for proof objects.  -/
Mathlib.Tactic.ITauto.Proof.format : Mathlib.Tactic.ITauto.Proof → Std.Format
-- Lean.Elab.Open
Lean.Elab.OpenDecl.instMonadResolveNameM : {m : Type → Type} → [Monad m] → [MonadLiftT (ST IO.RealWorld) m] → Lean.MonadResolveName Lean.Elab.OpenDecl.M
-- Mathlib.Algebra.Order.GroupWithZero.Basic
zpow_lt_one_of_neg₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 1 < a → n < 0 → a ^ n < 1
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
CategoryTheory.ExponentiableMorphism.pushforwardComp.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I J K : C} (f : I ⟶ J) (g : J ⟶ K)
  [inst_1 : CategoryTheory.ChosenPullbacksAlong f] [inst_2 : CategoryTheory.ChosenPullbacksAlong g]
  [inst_3 : CategoryTheory.ChosenPullbacksAlong (CategoryTheory.CategoryStruct.comp f g)]
  [inst_4 : CategoryTheory.ExponentiableMorphism f] [inst_5 : CategoryTheory.ExponentiableMorphism g]
  [inst_6 : CategoryTheory.ExponentiableMorphism (CategoryTheory.CategoryStruct.comp f g)],
  CategoryTheory.ExponentiableMorphism.pushforwardComp f g =
    (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj
          (CategoryTheory.CategoryStruct.comp f g)).rightAdjointUniq
      (CategoryTheory.ExponentiableMorphism.pullbackPushforwardAdj (CategoryTheory.CategoryStruct.comp f g))
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.tfst_tsnd : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] {F G : Type u → Type u} [inst_1 : Applicative F]
  [inst_2 : Applicative G] [LawfulBitraversable t] [LawfulApplicative F] [LawfulApplicative G] {α₀ α₁ β₀ β₁ : Type u}
  (f : α₀ → F α₁) (f' : β₀ → G β₁) (x : t α₀ β₀),
  Functor.Comp.mk (Bitraversable.tfst f <$> Bitraversable.tsnd f' x) =
    bitraverse (Functor.Comp.mk ∘ pure ∘ f) (Functor.Comp.mk ∘ Functor.map pure ∘ f') x
-- Mathlib.Algebra.Notation.Support
Function.mem_mulSupport : ∀ {ι : Type u_1} {M : Type u_3} [inst : One M] {f : ι → M} {x : ι}, x ∈ Function.mulSupport f ↔ f x ≠ 1
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- A function is differentiable on a union of open sets `s i`
iff it is differentiable on each `s i`.  -/
differentiableOn_iUnion_iff_of_isOpen : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {ι : Type u_4} {s : ι → Set E},
  (∀ (i : ι), IsOpen (s i)) → (DifferentiableOn 𝕜 f (⋃ i, s i) ↔ ∀ (i : ι), DifferentiableOn 𝕜 f (s i))
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionContext.fromJson : Lean.Json → Except String Lean.Lsp.CodeActionContext
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.subsingleton_iff_ker_eq_top : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {S : Submonoid R},
  Subsingleton (LocalizedModule S M) ↔ (LocalizedModule.mkLinearMap S M).ker = ⊤
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionEqualizerProducts.res_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X) (i : ι),
  CategoryTheory.CategoryStruct.comp (TopCat.Presheaf.SheafConditionEqualizerProducts.res F U)
      (CategoryTheory.Limits.limit.π (CategoryTheory.Discrete.functor fun i => F.obj (Opposite.op (U i))) { as := i }) =
    F.map (TopologicalSpace.Opens.leSupr U i).op
-- Init.Data.Vector.Basic
Vector.forM_eq_forM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {v : Vector α n} [inst : Monad m] (f : α → m PUnit.{u_1 + 1}),
  v.forM f = forM v f
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.mapPairLeft_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {E' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} E'] (Fₗ : CategoryTheory.Functor C E) (Fᵣ : CategoryTheory.Functor D E')
  (X : C),
  (CategoryTheory.Join.mapPairLeft Fₗ Fᵣ).hom.app X =
    CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left (Fₗ.obj X))