mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse_obj_left_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] (F : CategoryTheory.Functor C T)
  (G : CategoryTheory.Functor D T) (c : C) (Y : CategoryTheory.Comma ((CategoryTheory.Over.forget c).comp F) G),
  ((CategoryTheory.CostructuredArrow.ofCommaFstEquivalenceInverse F G c).obj Y).left.left = Y.left.left
-- Mathlib.Algebra.Group.Subgroup.Map
/-- For any subgroups `H` and `K`, view `H ⊓ K` as a subgroup of `K`.  -/
Subgroup.subgroupOf : {G : Type u_1} → [inst : Group G] → Subgroup G → (K : Subgroup G) → Subgroup ↥K
-- Mathlib.RingTheory.Multiplicity
multiplicity_add_eq_min : ∀ {α : Type u_1} [inst : Ring α] {p a b : α},
  FiniteMultiplicity p a →
    FiniteMultiplicity p b →
      multiplicity p a ≠ multiplicity p b → multiplicity p (a + b) = min (multiplicity p a) (multiplicity p b)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_eq_getValue : ∀ {α : Type u} {β : Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [instBEq : BEq α] [inst_2 : Std.LawfulBEqOrd α]
  {k : α} {t : Std.DTreeMap.Internal.Impl α fun x => β} {h : Std.DTreeMap.Internal.Impl.contains k t = true}
  (hto : t.Ordered), Std.DTreeMap.Internal.Impl.Const.get t k h = Std.Internal.List.getValue k t.toListModel ⋯
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_insert_sub : ∀ {ι : Type u_1} {G : Type u_3} {s : Finset ι} {a : ι} [inst : AddCommGroup G] [inst_1 : DecidableEq ι],
  a ∉ s → ∀ (f : ι → G), ∑ x ∈ insert a s, f x - f a = ∑ x ∈ s, f x
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_iff_isSome_getElem? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {a : α},
  a ∈ t ↔ t[a]?.isSome = true
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.instOrderBot : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Max α] → [inst_1 : Bot α] → [inst_2 : SemilatticeSup β] → [inst_3 : OrderBot β] → OrderBot (SupBotHom α β)
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The double coset `H₁gH₂` of an element `g : Δ`.  -/
HeckeCoset.mk : {G : Type u_1} → [inst : Group G] → {Δ : Submonoid G} → (H₁ H₂ : Subgroup G) → ↥Δ → HeckeCoset Δ H₁ H₂
-- Mathlib.Algebra.Algebra.Operations
/-- To show a property on elements of `M ^ n` holds, it suffices to show that it holds for scalars,
is closed under addition, and holds for `x * m` where `m ∈ M` and it holds for `x`  -/
Submodule.pow_induction_on_right : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A)
  {C : A → Prop},
  (∀ (r : R), C ((algebraMap R A) r)) →
    (∀ (x y : A), C x → C y → C (x + y)) → (∀ (x : A), C x → ∀ m ∈ M, C (x * m)) → ∀ {x : A} {n : ℕ}, x ∈ M ^ n → C x
-- Mathlib.CategoryTheory.EssentiallySmall
/-- A locally small category has small hom-types.  -/
CategoryTheory.LocallySmall.hom_small : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.LocallySmall.{w, v, u} C] (X Y : C),
  Small.{w, v} (X ⟶ Y)
-- Mathlib.Topology.Order.OrderClosed
Ici_mem_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  a < b → Set.Ici a ∈ nhds b
-- Init.Data.BitVec.Lemmas
BitVec.toFin_not : ∀ {w : ℕ} (x : BitVec w), (~~~x).toFin = x.toFin.rev
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.IsometryEquiv.pi_toLinearEquiv : ∀ {ι : Type u_1} {R : Type u_2} {P : Type u_7} {Mᵢ : ι → Type u_8} {Nᵢ : ι → Type u_9} [inst : CommSemiring R]
  [inst_1 : (i : ι) → AddCommMonoid (Mᵢ i)] [inst_2 : (i : ι) → AddCommMonoid (Nᵢ i)] [inst_3 : AddCommMonoid P]
  [inst_4 : (i : ι) → Module R (Mᵢ i)] [inst_5 : (i : ι) → Module R (Nᵢ i)] [inst_6 : Module R P] [inst_7 : Fintype ι]
  {Q : (i : ι) → QuadraticMap R (Mᵢ i) P} {Q' : (i : ι) → QuadraticMap R (Nᵢ i) P}
  (e : (i : ι) → (Q i).IsometryEquiv (Q' i)),
  (QuadraticMap.IsometryEquiv.pi e).toLinearEquiv = LinearEquiv.piCongrRight fun i => (e i).toLinearEquiv
-- Qq.Macro
Qq.Impl.UnquoteState.mk.injEq : ∀ (mvars : List (Lean.Expr × Qq.Impl.MVarSynth)) (levelSubst : Std.HashMap Lean.Expr Lean.Level)
  (exprSubst : Std.HashMap Lean.Expr Lean.Expr) (unquoted : Lean.LocalContext)
  (exprBackSubst : Std.HashMap Lean.Expr Qq.Impl.ExprBackSubstResult)
  (levelBackSubst : Std.HashMap Lean.Level Lean.Expr) (abstractedFVars : Array Lean.FVarId)
  (levelNames : List Lean.Name) (mayPostpone : Bool) (mvars_1 : List (Lean.Expr × Qq.Impl.MVarSynth))
  (levelSubst_1 : Std.HashMap Lean.Expr Lean.Level) (exprSubst_1 : Std.HashMap Lean.Expr Lean.Expr)
  (unquoted_1 : Lean.LocalContext) (exprBackSubst_1 : Std.HashMap Lean.Expr Qq.Impl.ExprBackSubstResult)
  (levelBackSubst_1 : Std.HashMap Lean.Level Lean.Expr) (abstractedFVars_1 : Array Lean.FVarId)
  (levelNames_1 : List Lean.Name) (mayPostpone_1 : Bool),
  ({ mvars := mvars, levelSubst := levelSubst, exprSubst := exprSubst, unquoted := unquoted,
        exprBackSubst := exprBackSubst, levelBackSubst := levelBackSubst, abstractedFVars := abstractedFVars,
        levelNames := levelNames, mayPostpone := mayPostpone } =
      { mvars := mvars_1, levelSubst := levelSubst_1, exprSubst := exprSubst_1, unquoted := unquoted_1,
        exprBackSubst := exprBackSubst_1, levelBackSubst := levelBackSubst_1, abstractedFVars := abstractedFVars_1,
        levelNames := levelNames_1, mayPostpone := mayPostpone_1 }) =
    (mvars = mvars_1 ∧
      levelSubst = levelSubst_1 ∧
        exprSubst = exprSubst_1 ∧
          unquoted = unquoted_1 ∧
            exprBackSubst = exprBackSubst_1 ∧
              levelBackSubst = levelBackSubst_1 ∧
                abstractedFVars = abstractedFVars_1 ∧ levelNames = levelNames_1 ∧ mayPostpone = mayPostpone_1)
-- Mathlib.Topology.Instances.NNReal.Lemmas
NNReal.summable_comp_injective : ∀ {α : Type u_2} {β : Type u_3} {f : α → NNReal}, Summable f → ∀ {i : β → α}, Function.Injective i → Summable (f ∘ i)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionIdentifier.fvar.injEq : ∀ (id id_1 : Lean.FVarId),
  (Lean.Lsp.CompletionIdentifier.fvar id = Lean.Lsp.CompletionIdentifier.fvar id_1) = (id = id_1)
-- Mathlib.Data.Finset.Defs
Finset.coe_ssubset : ∀ {α : Type u_1} {s₁ s₂ : Finset α}, ↑s₁ ⊂ ↑s₂ ↔ s₁ ⊂ s₂
-- Lean.Meta.Offset
/-- Similar to `getOffset` but returns `none` if the expression is not an offset.
 -/
Lean.Meta.isOffset? : Lean.Expr → OptionT Lean.MetaM (Lean.Expr × ℕ)
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is any function and `g` is analytic without zero in `U`, then `f` is
meromorphic in normal form on `U` iff `f * g` is meromorphic in normal form on
`U`.
 -/
meromorphicNFOn_mul_iff_left_of_analyticOnNhd : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {f g : 𝕜 → 𝕜},
  AnalyticOnNhd 𝕜 g U → (∀ u ∈ U, g u ≠ 0) → (MeromorphicNFOn (f * g) U ↔ MeromorphicNFOn f U)
-- Mathlib.Topology.UniformSpace.Basic
UniformSpace.isGLB_sInf : ∀ {α : Type ua} {tt : Set (UniformSpace α)}, IsGLB tt (sInf tt)
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sum.eq_1 : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : (i : ι) → (x : β i) → Decidable (x ≠ 0)] [inst_3 : AddCommMonoid γ] (f : Π₀ (i : ι), β i)
  (g : (i : ι) → β i → γ), f.sum g = ∑ i ∈ f.support, g i (f i)
-- Mathlib.CategoryTheory.CatCommSq
/-- In a square of categories, when the top and bottom functors are part
of equivalence of categories, it is equivalent to show 2-commutativity for
the functors of these equivalences or for their inverses.  -/
CategoryTheory.CatCommSq.hInvEquiv : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [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} C₄] →
                (T : C₁ ≌ C₂) →
                  (L : CategoryTheory.Functor C₁ C₃) →
                    (R : CategoryTheory.Functor C₂ C₄) →
                      (B : C₃ ≌ C₄) →
                        CategoryTheory.CatCommSq T.functor L R B.functor ≃
                          CategoryTheory.CatCommSq T.inverse R L B.inverse
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.CotangentSpace.map_tmul : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] (f : P.Hom P') (x : S) (y : P.Ring),
  (Algebra.Extension.CotangentSpace.map f) (x ⊗ₜ[P.Ring] (KaehlerDifferential.D R P.Ring) y) =
    (algebraMap S S') x ⊗ₜ[P'.Ring] (KaehlerDifferential.D R' P'.Ring) (f.toAlgHom y)
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The second projection in a product is `C^∞`.  -/
contDiff_snd : ∀ {𝕜 : 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] {n : WithTop ℕ∞},
  ContDiff 𝕜 n Prod.snd
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, (t.erase k).get? a = if cmp k a = Ordering.eq then none else t.get? a
-- Aesop.Forward.State.Initial
Aesop.LocalRuleSet.mkInitialForwardState : Lean.MVarId → Aesop.LocalRuleSet → Aesop.BaseM (Aesop.ForwardState × Array Aesop.ForwardRuleMatch)
-- Mathlib.Order.WithBot
WithBot.lt_coe_bot : ∀ {α : Type u_1} [inst : Preorder α] {x : WithBot α} [inst_1 : OrderBot α], x < ↑⊥ ↔ x = ⊥
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.core : Lean.Expr →
  Lean.Expr → Lean.Grind.CommRing.Expr → Lean.Grind.CommRing.Expr → Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof
-- Mathlib.NumberTheory.LSeries.DirichletContinuation
/-- The L-function of an odd Dirichlet character vanishes at negative odd integers.  -/
DirichletCharacter.Odd.LFunction_neg_two_mul_nat_sub_one : ∀ {N : ℕ} [inst : NeZero N] {χ : DirichletCharacter ℂ N},
  χ.Odd → ∀ (n : ℕ), DirichletCharacter.LFunction χ (-(2 * ↑n) - 1) = 0
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautologicalRelations_R : ∀ (A : Type u) [inst : Ring A] (M : Type v) [inst_1 : AddCommGroup M] [inst_2 : Module A M],
  (Module.Presentation.tautologicalRelations A M).R = Module.Presentation.tautological.R A M
-- Mathlib.ModelTheory.Arithmetic.Presburger.Basic
FirstOrder.presburgerFunc.one.sizeOf_spec : sizeOf FirstOrder.presburgerFunc.one = 1
-- Mathlib.Topology.Order.OrderClosed
eventually_ge_nhds : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b : α},
  b < a → ∀ᶠ (x : α) in nhds a, b ≤ x
-- Mathlib.Order.CompleteLattice.Basic
iSup_plift_up : ∀ {α : Type u_1} {ι : Sort u_4} [inst : SupSet α] (f : PLift ι → α), ⨆ i, f { down := i } = ⨆ i, f i
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakPullbacks
CategoryTheory.Limits.HasWeakPullbacksOfHasPullbacks : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.Limits.HasWeakPullbacks C
-- Mathlib.Analysis.Normed.Affine.AddTorsorBases
/-- Given a finite-dimensional normed real vector space, the interior of the convex hull of an
affine basis is the set of points whose barycentric coordinates are strictly positive with respect
to this basis.

TODO Restate this result for affine spaces (instead of vector spaces) once the definition of
convexity is generalised to this setting.  -/
AffineBasis.interior_convexHull : ∀ {ι : Type u_1} {E : Type u_2} [Finite ι] [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (b : AffineBasis ι ℝ E), interior ((convexHull ℝ) (Set.range ⇑b)) = {x | ∀ (i : ι), 0 < (b.coord i) x}
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.zeroLocus_isClosed : ∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  (s : Set ↑(X.presheaf.obj (Opposite.op U))), IsClosed (X.zeroLocus s)
-- Lean.Elab.BuiltinCommand
/-- 'Delaborate' open declarations.
Current limitations:
- does not check whether or not successive namespaces need `_root_`
- does not combine commands with `renaming` clauses into a single command
 -/
_private.Lean.Elab.BuiltinCommand.0.Lean.Elab.Command.elabWhere.describeOpenDecls : List Lean.OpenDecl → Lean.Elab.Command.CommandElabM (Option Lean.MessageData)
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeAction.fromJson : Lean.Json → Except String Lean.Lsp.CodeAction
-- Mathlib.Computability.NFA
/-- Set of accepting states  -/
NFA.accept : {α : Type u} → {σ : Type v} → NFA α σ → Set σ
-- Mathlib.Algebra.MonoidAlgebra.Support
AddMonoidAlgebra.support_coeff_one : ∀ {k : Type u₁} {G : Type u₂} [inst : Semiring k] [inst_1 : Zero G] [NeZero 1], (AddMonoidAlgebra.coeff 1).support = 0
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.foldl_eq_foldl_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {δ : Type w} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  {f : δ → α → β → δ} {init : δ},
  Std.DTreeMap.Raw.foldl f init t = List.foldl (fun a b => f a b.1 b.2) init (Std.DTreeMap.Raw.Const.toList t)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.sum_coeff_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (f : AddMonoidAlgebra R M), f.coeff.sum AddMonoidAlgebra.single = f
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.FactorSet.sup_add_inf_eq_add : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : DecidableEq (Associates α)] (a b : Associates.FactorSet α),
  a ⊔ b + a ⊓ b = a + b
-- Mathlib.Algebra.Group.Action.Defs
IsCentralVAdd.mk : ∀ {M : Type u_9} {α : Type u_10} [inst : VAdd M α] [inst_1 : VAdd Mᵃᵒᵖ α],
  (∀ (m : M) (a : α), AddOpposite.op m +ᵥ a = m +ᵥ a) → IsCentralVAdd M α
-- Mathlib.LinearAlgebra.Pi
Submodule.pi_mono : ∀ {R : Type u} {ι : Type x} [inst : Semiring R] {φ : ι → Type u_1} [inst_1 : (i : ι) → AddCommMonoid (φ i)]
  [inst_2 : (i : ι) → Module R (φ i)] {p q : (i : ι) → Submodule R (φ i)} {s : Set ι},
  (∀ i ∈ s, p i ≤ q i) → Submodule.pi s p ≤ Submodule.pi s q
-- Mathlib.RingTheory.MvPowerSeries.Derivative
MvPowerSeries.pderiv_X_of_ne : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i j : σ},
  j ≠ i → (MvPowerSeries.pderiv R i) (MvPowerSeries.X j) = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_eq_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] [inst : Inhabited α], t.WF → ∀ {k : α}, k ∈ t → t.getKey! k = k
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
ExistsContDiffBumpBase.y_smooth : ∀ (E : Type u_1) [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E],
  ContDiffOn ℝ (↑⊤) (Function.uncurry ExistsContDiffBumpBase.y) (Set.Ioo 0 1 ×ˢ Set.univ)
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.prec.sizeOf_spec : ∀ (a a_1 : Nat.Partrec.Code), sizeOf (a.prec a_1) = 1 + sizeOf a + sizeOf a_1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey?_modify_eq_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k : α} {f : β → β}, (t.modify k f).maxKey? = t.maxKey?
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.toEquiv_eq_coe : ∀ {R : Type uR} {A₁ : Type uA₁} {A₂ : Type uA₂} [inst : CommSemiring R] [inst_1 : Semiring A₁] [inst_2 : Semiring A₂]
  [inst_3 : Algebra R A₁] [inst_4 : Algebra R A₂] (e : A₁ ≃ₐ[R] A₂), e.toEquiv = ↑e
-- Mathlib.Algebra.Group.Submonoid.Units
Submonoid.units_sInf : ∀ {M : Type u_1} [inst : Monoid M] {s : Set (Submonoid M)}, (sInf s).units = ⨅ S ∈ s, S.units
-- Aesop.Rule.Forward
Aesop.ForwardRulePriority.instOrd : Ord Aesop.ForwardRulePriority
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoidHom.inverse.eq_1 : ∀ {A : Type u_10} {B : Type u_11} [inst : AddMonoid A] [inst_1 : AddMonoid B] (f : A →+ B) (g : B → A)
  (h₁ : Function.LeftInverse g ⇑f) (h₂ : Function.RightInverse g ⇑f),
  f.inverse g h₁ h₂ = { toFun := g, map_zero' := ⋯, map_add' := ⋯ }
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.buildGlobalRule : Aesop.Frontend.RuleConfig → Aesop.ElabM (Aesop.GlobalRuleSetMember × Array Aesop.RuleSetName)
-- Mathlib.CategoryTheory.Localization.Resolution
/-- an object in the source category  -/
CategoryTheory.LocalizerMorphism.RightResolution.X₁ : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} → {X₂ : C₂} → Φ.RightResolution X₂ → C₁
-- Mathlib.Topology.Algebra.Ring.Basic
/-- The (topological) closure of a non-unital subsemiring of a non-unital topological semiring is
itself a non-unital subsemiring.  -/
NonUnitalSubsemiring.topologicalClosure : {R : Type u_1} →
  [inst : TopologicalSpace R] →
    [inst_1 : NonUnitalSemiring R] → [IsSemitopologicalSemiring R] → NonUnitalSubsemiring R → NonUnitalSubsemiring R
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
Matroid.IsBasis'.cardinalMk_le_cRk : ∀ {α : Type u} {M : Matroid α} {I X : Set α}, M.IsBasis' I X → Cardinal.mk ↑I ≤ M.cRk X
-- Init.Data.Float.Float
instToStringFloat : ToString Float
-- Mathlib.Algebra.Algebra.Defs
algebraMap.coe_natCast : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (a : ℕ), ↑↑a = ↑a
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.ΨSq_odd : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (m : ℤ),
  W.ΨSq (2 * m + 1) =
    ((W.preΨ (m + 2) * W.preΨ m ^ 3 * if Even m then W.Ψ₂Sq ^ 2 else 1) -
        W.preΨ (m - 1) * W.preΨ (m + 1) ^ 3 * if Even m then 1 else W.Ψ₂Sq ^ 2) ^
      2
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.op_iSup : ∀ {ι : Sort u_1} {G : Type u_2} [inst : AddGroup G] (S : ι → AddSubgroup G), (iSup S).op = ⨆ i, (S i).op
-- Mathlib.Order.PFilter
Order.PFilter.directed : ∀ {P : Type u_1} [inst : Preorder P] (F : Order.PFilter P), DirectedOn (fun x1 x2 => x1 ≥ x2) ↑F
-- Init.Data.BitVec.Lemmas
BitVec.ofBoolListLE.eq_1 : BitVec.ofBoolListLE [] = 0#0
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.Hom.ext : ∀ {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 X' : CategoryTheory.Abelian.SpectralObject C ι} {x y : X.Hom X'}, x.hom = y.hom → x = y
-- Mathlib.NumberTheory.Padics.ProperSpace
PadicInt.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], ℤ_[p] = { x // ‖x‖ ≤ 1 }
-- Init.Data.List.Lemmas
List.getLast?_dropLast : ∀ {α : Type u_1} {xs : List α}, xs.dropLast.getLast? = if xs.length ≤ 1 then none else xs[xs.length - 2]?
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.ediam_image_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
  {f : X → Y}, HolderWith C r f → ∀ (s : Set X), Metric.ediam (f '' s) ≤ ↑C * Metric.ediam s ^ ↑r
-- Mathlib.Topology.Compactness.Paracompact
/-- Any open cover of a paracompact space has a locally finite *precise* refinement, that is,
one indexed on the same type with each open set contained in the corresponding original one.  -/
precise_refinement : ∀ {ι : Type u} {X : Type v} [inst : TopologicalSpace X] [ParacompactSpace X] (u : ι → Set X),
  (∀ (a : ι), IsOpen (u a)) →
    ⋃ i, u i = Set.univ → ∃ v, (∀ (a : ι), IsOpen (v a)) ∧ ⋃ i, v i = Set.univ ∧ LocallyFinite v ∧ ∀ (a : ι), v a ⊆ u a
-- Mathlib.RepresentationTheory.Basic
/-- `α` gives a `k[G]`-basis of the representation `free k G α`.  -/
Representation.freeAsModuleBasis : (k : Type u_1) →
  (G : Type u_2) →
    [inst : CommSemiring k] →
      [inst_1 : Monoid G] → (α : Type u_6) → Module.Basis α (MonoidAlgebra k G) (Representation.free k G α).asModule
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- Any mono factorisation of `f` gives a mono factorisation of `f ≫ g` when `g` is a mono.  -/
CategoryTheory.Limits.MonoFactorisation.compMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        CategoryTheory.Limits.MonoFactorisation f →
          {Y' : C} →
            (g : Y ⟶ Y') →
              [CategoryTheory.Mono g] → CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The property of being `C^n`, initially defined in terms of the Fréchet derivative, can be
reformulated in terms of the one-dimensional derivative on sets with unique derivatives.  -/
contDiffOn_nat_iff_continuousOn_differentiableOn_deriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {s : Set 𝕜} {n : ℕ},
  UniqueDiffOn 𝕜 s →
    (ContDiffOn 𝕜 (↑n) f s ↔
      (∀ m ≤ n, ContinuousOn (iteratedDerivWithin m f s) s) ∧ ∀ m < n, DifferentiableOn 𝕜 (iteratedDerivWithin m f s) s)
-- Mathlib.Control.Basic
joinM.eq_1 : ∀ {m : Type u → Type u} [inst : Monad m] {α : Type u} (a : m (m α)), joinM a = a >>= id
-- Lean.Parser.Term
Lean.Parser.Term.letIdDecl.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
/-- If the forgetful functor of a concrete category reflects isomorphisms, being an isomorphism
is equivalent to being bijective.  -/
CategoryTheory.ConcreteCategory.isIso_iff_bijective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [(CategoryTheory.forget C).ReflectsIsomorphisms] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.IsIso f ↔ Function.Bijective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF →
    ∀ {k a : α} {fallback : β a}, (m.erase k).getD a fallback = if (k == a) = true then fallback else m.getD a fallback
-- Mathlib.CategoryTheory.Limits.Sifted
CategoryTheory.IsSifted.colim_preservesLimits_pair_of_sSifted : ∀ {C : Type u} [inst : CategoryTheory.SmallCategory C] [CategoryTheory.IsSifted C]
  {X Y : CategoryTheory.Functor C (Type u)},
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair X Y) CategoryTheory.Limits.colim
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
_private.Mathlib.NumberTheory.DiophantineApproximation.Basic.0.Real.convergent.match_1.splitter : (motive : ℝ → ℕ → Sort u_1) →
  (x : ℝ) → (x_1 : ℕ) → ((ξ : ℝ) → motive ξ 0) → ((ξ : ℝ) → (n : ℕ) → motive ξ n.succ) → motive x x_1
-- Init.SimpLemmas
not_false_eq_true : (¬False) = True
-- Std.Async.Basic
/-- Block until the `EAsync` finishes and returns its value. Propagates any error encountered during execution.
 -/
Std.Async.EAsync.block : {ε α : Type} → Std.Async.EAsync ε α → optParam Task.Priority Task.Priority.default → EIO ε α
-- Lean.Message
Lean.TraceResult.success.sizeOf_spec : sizeOf Lean.TraceResult.success = 1
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctorIso_hom_app_τ₂ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ)
  (hi : n + i = i') (X : CochainComplex C ℤ),
  ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).hom.app X).τ₂ = (HomologicalComplex.XIsoOfEq X ⋯).hom