mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_lt_withBotDegree_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f g : MvPolynomial σ R),
  m.toWithBotSyn (m.withBotDegree f) < m.toWithBotSyn (m.withBotDegree g) ↔
    m.toSyn (m.degree f) < m.toSyn (m.degree g) ∨ f = 0 ∧ g ≠ 0
-- Std.Sat.AIG.RelabelNat
/-- Assuming that we find a `Nat` for an atom in the `ofAIG` map, that `Nat` is unique in the map.
 -/
Std.Sat.AIG.RelabelNat.State.ofAIG_find_unique : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {n : ℕ} {aig : Std.Sat.AIG α} (a : α),
  (Std.Sat.AIG.RelabelNat.State.ofAIG aig)[a]? = some n →
    ∀ (a' : α), (Std.Sat.AIG.RelabelNat.State.ofAIG aig)[a']? = some n → a = a'
-- Mathlib.Order.CompleteLattice.Basic
bot_lt_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {s : ι → α}, ⊥ < ⨆ i, s i ↔ ∃ i, ⊥ < s i
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.stronglyMeasurable_cauchyPDF : ∀ (x₀ : ℝ) (γ : NNReal), MeasureTheory.StronglyMeasurable (ProbabilityTheory.cauchyPDF x₀ γ)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Language.instIsAlgebraicRing : FirstOrder.Language.ring.IsAlgebraic
-- Lean.Data.KVMap
Lean.KVMap.instBEq : BEq Lean.KVMap
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.WorkspaceEditClientCapabilities.mk : Option Bool → Option Lean.Lsp.ChangeAnnotationSupport → Option (Array String) → Lean.Lsp.WorkspaceEditClientCapabilities
-- Mathlib.Data.Nat.Factorization.Defs
Nat.eq_of_factorization_eq' : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → a.factorization = b.factorization → a = b
-- Mathlib.CategoryTheory.Equivalence
/-- The functor of an equivalence of categories is full.  -/
CategoryTheory.Equivalence.full_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E]
  (e : C ≌ E), e.functor.Full
-- Mathlib.Data.Set.Card
Set.coe_fintypeCard : ∀ {α : Type u_1} (s : Set α) [inst : Fintype ↑s], ↑(Fintype.card ↑s) = s.encard
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.preAleph_max : ∀ (o₁ o₂ : Ordinal.{u_1}), Cardinal.preAleph (max o₁ o₂) = max (Cardinal.preAleph o₁) (Cardinal.preAleph o₂)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.addConstImportData : {α : Type} →
  Lean.Core.Context →
    Lean.Environment →
      Lean.Name →
        Lean.Meta.LazyDiscrTree.ImportData →
          IO.Ref Lean.Meta.LazyDiscrTree.Cache →
            Lean.Meta.LazyDiscrTree.PreDiscrTree α →
              (Lean.Name → Lean.AsyncConstantInfo → Lean.MetaM (Array (Lean.Meta.LazyDiscrTree.InitEntry α))) →
                Lean.AsyncConstantInfo → BaseIO (Lean.Meta.LazyDiscrTree.PreDiscrTree α)
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.relativeCellComplexOfMono.Cell.ι_t_ι_eq_ι_l_b_ι : ∀ {X Y : SSet} {i : X ⟶ Y} {d : ℕ} (c : SSet.relativeCellComplexOfMono.Cell i d),
  CategoryTheory.CategoryStruct.comp c.ιSigmaBoundary
      (CategoryTheory.CategoryStruct.comp (SSet.relativeCellComplexOfMono.t i d) ((SSet.skeletonOfMono i) d).ι) =
    CategoryTheory.CategoryStruct.comp (SSet.boundary d).ι
      (CategoryTheory.CategoryStruct.comp c.ιSigmaStdSimplex
        (CategoryTheory.CategoryStruct.comp (SSet.relativeCellComplexOfMono.b i d) ((SSet.skeletonOfMono i) (d + 1)).ι))
-- Mathlib.Data.Rel
SetRel.prodMk_mem_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : SetRel α β} {S : SetRel β γ} {a : α} {b : β} {c : γ},
  (a, b) ∈ R → (b, c) ∈ S → (a, c) ∈ R.comp S
-- Lean.DocString.Types
Lean.Doc.instReprBlock.repr : {i : Type u_1} → {b : Type u_2} → [Repr i] → [Repr b] → Lean.Doc.Block i b → ℕ → Std.Format
-- Mathlib.Algebra.Group.Basic
mul_left_iterate : ∀ {M : Type u_4} [inst : Monoid M] (a : M) (n : ℕ), (fun x => a * x)^[n] = fun x => a ^ n * x
-- Lean.Meta.NatInstTesters
Lean.Meta.Structural.isInstOfNatNat : Lean.Expr → Lean.MetaM Bool
-- Batteries.Data.List.Scan
List.partialProds_append : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : One α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1] {l₁ l₂ : List α},
  (l₁ ++ l₂).partialProds = l₁.partialProds ++ List.map (fun x => l₁.prod * x) l₂.partialProds.tail
-- Mathlib.Logic.Equiv.Prod
Equiv.pprodEquivProd_symm_apply : ∀ {α : Type u_9} {β : Type u_10} (x : α × β), Equiv.pprodEquivProd.symm x = ⟨x.1, x.2⟩
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.isNormal_iff_lt_succ_and_blsub_eq : ∀ {f : Ordinal.{u} → Ordinal.{max u v}},
  Order.IsNormal f ↔
    (∀ (a : Ordinal.{u}), f a < f (Order.succ a)) ∧
      ∀ (o : Ordinal.{u}), Order.IsSuccLimit o → (o.blsub fun x x_1 => f x) = f o
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.getElem?_toList_eq : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α] {r : Std.Rci α} {i : ℕ}, r.toList[i]? = Std.PRange.succMany? i r.lower
-- Mathlib.CategoryTheory.GradedObject.Single
CategoryTheory.GradedObject.single_map_singleObjApplyIso_hom_assoc : ∀ {J : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Limits.HasInitial C] [inst_2 : DecidableEq J] (j : J) {X Y : C} (f : X ⟶ Y) {Z : C}
  (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.GradedObject.single j).map f j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j Y).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.singleObjApplyIso j X).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Init.Data.String.Basic
String.Pos.utf8Encode_get_eq_extract : ∀ {s : String} (pos : s.Pos) (h : pos ≠ s.endPos),
  [pos.get h].utf8Encode = s.toByteArray.extract pos.offset.byteIdx (pos.offset.byteIdx + (pos.get h).utf8Size)
-- Std.Http.Data.Headers
Std.Http.Headers.mk.sizeOf_spec : ∀ (map : Std.Internal.IndexMultiMap Std.Http.Header.Name Std.Http.Header.Value), sizeOf { map := map } = 1 + sizeOf map
-- Mathlib.Topology.UniformSpace.Ultra.Basic
IsUltraUniformity.hasBasis : ∀ {X : Type u_1} {inst : UniformSpace X} [self : IsUltraUniformity X],
  (uniformity X).HasBasis (fun s => s ∈ uniformity X ∧ s.IsSymm ∧ s.IsTrans) id
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.proj.eq_1 : ∀ {ι : Type u_1} {Γ : ι → Type u_2} [inst : (i : ι) → Inhabited (Γ i)] (i : ι),
  Turing.proj i = { f := fun a => a i, map_pt' := ⋯ }
-- Mathlib.Algebra.EuclideanDomain.Basic
/-- An explicit version of **Bézout's lemma** for Euclidean domains.  -/
EuclideanDomain.gcd_eq_gcd_ab : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R),
  EuclideanDomain.gcd a b = a * EuclideanDomain.gcdA a b + b * EuclideanDomain.gcdB a b
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin.decl.injEq : ∀ (declName declName_1 : Lean.Name),
  (Lean.Meta.Grind.Origin.decl declName = Lean.Meta.Grind.Origin.decl declName_1) = (declName = declName_1)
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_restrictFreeVar : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} [inst_1 : DecidableEq α]
  {n : ℕ} {φ : L.BoundedFormula α n} {f : ↥φ.freeVarFinset → β} {v : β → M} {xs : Fin n → M} (v' : α → M),
  (∀ (a : ↥φ.freeVarFinset), v (f a) = v' ↑a) → ((φ.restrictFreeVar f).Realize v xs ↔ φ.Realize v' xs)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.inner_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E} {i j : ι}, Orthonormal 𝕜 v → i ≠ j → inner 𝕜 (v i) (v j) = 0
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj_map : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : CategoryTheory.CommMon C)
  {X Y : CategoryTheory.Discrete PUnit.{u + 1}} (x : X ⟶ Y),
  (CategoryTheory.CommMon.EquivLaxBraidedFunctorPUnit.commMonToLaxBraidedObj A).map x =
    CategoryTheory.CategoryStruct.id A.X
-- Mathlib.Order.LiminfLimsup
/-- If `Filter.limsup u atTop ≤ x`, then for all `ε > 0`, eventually we have `u b < x + ε`.  -/
Filter.eventually_lt_add_pos_of_limsup_le : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : Preorder β]
  [inst_2 : AddZeroClass α] [AddLeftStrictMono α] {x ε : α} {u : β → α},
  Filter.IsBoundedUnder LE.le Filter.atTop u →
    Filter.limsup u Filter.atTop ≤ x → 0 < ε → ∀ᶠ (b : β) in Filter.atTop, u b < x + ε
-- Mathlib.Algebra.Group.Pi.Lemmas
Pi.evalMulHom_apply : ∀ {I : Type u} (f : I → Type v) [inst : (i : I) → Mul (f i)] (i : I) (g : (i : I) → f i), (Pi.evalMulHom f i) g = g i
-- Mathlib.Analysis.Normed.Lp.SmoothApprox
/-- For every continuous compactly supported function `f` there exists a smooth compactly supported
function `g` such that `f - g` is arbitrary small in the `Lp`-norm for `p < ∞`.  -/
HasCompactSupport.exist_eLpNorm_sub_le_of_continuous : ∀ {E : Type u_3} {F : Type u_4} [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace ℝ E] [FiniteDimensional ℝ E] [BorelSpace E]
  [inst_6 : NormedSpace ℝ F]
  (μ : autoParam (MeasureTheory.Measure E) HasCompactSupport.exist_eLpNorm_sub_le_of_continuous._auto_1)
  [MeasureTheory.IsFiniteMeasureOnCompacts μ] {p : ENNReal} {ε : ℝ},
  0 < ε →
    ∀ {f : E → F},
      HasCompactSupport f →
        Continuous f →
          ∃ g, HasCompactSupport g ∧ ContDiff ℝ (↑⊤) g ∧ MeasureTheory.eLpNorm (f - g) p μ ≤ ENNReal.ofReal ε
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.forM.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} {m : Type w → Type w₂} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : Std.TransCmp cmp] (f f_1 : α → m PUnit.{w + 1}),
  f = f_1 → ∀ (t t_1 : Std.ExtTreeSet α cmp), t = t_1 → Std.ExtTreeSet.forM f t = Std.ExtTreeSet.forM f_1 t_1
-- Mathlib.Tactic.Linter.FlexibleLinter
_private.Mathlib.Tactic.Linter.FlexibleLinter.0.Mathlib.Linter.Flexible.StainData.mk : Mathlib.Linter.Flexible.Stained✝ →
  Lean.Syntax → Lean.Elab.ContextInfo → Lean.MetavarContext → List Lean.MVarId → Mathlib.Linter.Flexible.StainData✝
-- Std.Time.Format.Modifier
_private.Std.Time.Format.Modifier.0.Std.Time.parseNumber : (Std.Time.Number → Std.Time.Modifier) → String → Std.Internal.Parsec.String.Parser Std.Time.Modifier
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.GrothendieckTopology.overMapPullback_id_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u')
  [inst_1 : CategoryTheory.Category.{v', u'} A] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (J.overMapPullbackComp A (CategoryTheory.CategoryStruct.id X) f).inv
      (CategoryTheory.CategoryStruct.comp ((J.overMapPullback A f).whiskerLeft (J.overMapPullbackId A X).hom)
        (J.overMapPullback A f).rightUnitor.hom) =
    (J.overMapPullbackCongr A ⋯).hom
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
deriv_cos : ∀ {f : ℝ → ℝ} {x : ℝ}, DifferentiableAt ℝ f x → deriv (fun x => Real.cos (f x)) x = -Real.sin (f x) * deriv f x
-- Mathlib.Analysis.Normed.Lp.ProdLp
LinearIsometryEquiv.withLpProdCongr_symm_apply : ∀ (p : ENNReal) {𝕜 : Type u_1} {α : Type u_2} {β : Type u_3} {α' : Type u_5} {β' : Type u_6} [hp : Fact (1 ≤ p)]
  [inst : Semiring 𝕜] [inst_1 : SeminormedAddCommGroup α] [inst_2 : Module 𝕜 α] [inst_3 : SeminormedAddCommGroup β]
  [inst_4 : Module 𝕜 β] [inst_5 : SeminormedAddCommGroup α'] [inst_6 : Module 𝕜 α'] [inst_7 : SeminormedAddCommGroup β']
  [inst_8 : Module 𝕜 β'] (f : α ≃ₗᵢ[𝕜] α') (g : β ≃ₗᵢ[𝕜] β') (a : WithLp p (α' × β')),
  (LinearIsometryEquiv.withLpProdCongr p f g).symm a = WithLp.toLp p (f.symm a.fst, g.symm a.snd)
-- Init.NotationExtra
unexpandEqNDRec : Lean.PrettyPrinter.Unexpander
-- Mathlib.Algebra.Star.Basic
/-- **Alias** of the reverse direction of `commute_star_star`. -/
Commute.star_star : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x y : R}, Commute x y → Commute (star x) (star y)
-- Mathlib.MeasureTheory.Integral.Bochner.Set
/-- Consider a parameterized integral `x ↦ ∫ y, f x y` where `f` is continuous and uniformly
compactly supported. Then the integral depends continuously on `x`.  -/
continuousOn_integral_of_compact_support : ∀ {Y : Type u_2} {E : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : MeasurableSpace Y] [OpensMeasurableSpace Y] {μ : MeasureTheory.Measure Y} [inst_4 : NormedAddCommGroup E]
  [inst_5 : NormedSpace ℝ E] {f : X → Y → E} {s : Set X} {k : Set Y} [MeasureTheory.IsFiniteMeasureOnCompacts μ],
  IsCompact k →
    ContinuousOn (Function.uncurry f) (s ×ˢ Set.univ) →
      (∀ (p : X) (x : Y), p ∈ s → x ∉ k → f p x = 0) → ContinuousOn (fun x => ∫ (y : Y), f x y ∂μ) s
-- Mathlib.Order.OrderDual
OrderDual.toDual_le_toDual : ∀ {α : Type u_1} [inst : LE α] {a b : α}, OrderDual.toDual a ≤ OrderDual.toDual b ↔ b ≤ a
-- Lean.Compiler.ModPkgExt
/-- Persistent environment extension for storing a single serializable value per module.  -/
Lean.ModuleEnvExtension : Type → Type
-- Mathlib.Topology.Continuous
/-- Given a function `f : X → Y` with dense range and `y : Y`, returns some `x : X`.  -/
DenseRange.some : {X : Type u_1} → [inst : TopologicalSpace X] → {α : Type u_4} → {f : α → X} → DenseRange f → X → α
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.sieve₁₀_apply : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {X : C} (data : F.PreOneHypercoverDenseData X) {i₁ i₂ : data.I₀} {W₀ : C₀}
  (p₁ : W₀ ⟶ data.X i₁) (p₂ : W₀ ⟶ data.X i₂) (Z₀ : C₀) (g : Z₀ ⟶ W₀),
  (data.sieve₁₀ p₁ p₂).arrows g =
    ∃ j h,
      CategoryTheory.CategoryStruct.comp g p₁ = CategoryTheory.CategoryStruct.comp h (data.p₁ j) ∧
        CategoryTheory.CategoryStruct.comp g p₂ = CategoryTheory.CategoryStruct.comp h (data.p₂ j)
-- Lean.DocString.Add
/-- Adds a Verso docstring to the specified declaration, which should already be present in the
environment. The docstring is added from a string value, rather than syntax, which means that the
interactive features are disabled.
 -/
Lean.versoDocStringFromString : Lean.Name → String → Lean.Elab.TermElabM Lean.VersoDocResult
-- Mathlib.Analysis.SpecialFunctions.Log.PosLog
/-- Presentation of `log` in terms of its positive part.  -/
Real.posLog_sub_posLog_inv : ∀ {x : ℝ}, x.posLog - x⁻¹.posLog = Real.log x
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Product
/-- Equivalence between the categories of cones over the objects `π Xᵢ` written in two ways  -/
FundamentalGroupoidFunctor.coneDiscreteComp : {I : Type u} →
  (X : I → TopCat) →
    CategoryTheory.Limits.Cone
        ((CategoryTheory.Discrete.functor X).comp FundamentalGroupoid.fundamentalGroupoidFunctor) ≌
      CategoryTheory.Limits.Cone
        (CategoryTheory.Discrete.functor fun i => FundamentalGroupoid.fundamentalGroupoidFunctor.obj (X i))
-- Mathlib.Combinatorics.Enumerative.Pentagonal.Ring
/-- `powMulProdOneSubPow` and `aux` have relation

$$ a_{k,n} + x^{3k + 5}a_{k + 1, n} = b_{k, n+1} - b_{k, n} $$  -/
_private.Mathlib.Combinatorics.Enumerative.Pentagonal.Ring.0.Pentagonal.aux_sub_aux : ∀ {R : Type u_1} [inst : CommRing R] (k n : ℕ) (x : R),
  Pentagonal.powMulProdOneSubPow✝ k n x + x ^ (3 * k + 5) * Pentagonal.powMulProdOneSubPow✝ (k + 1) n x =
    Pentagonal.aux✝ k (n + 1) x - Pentagonal.aux✝ k n x
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Initial.conesEquiv_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Initial] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  (G : CategoryTheory.Functor D E),
  (CategoryTheory.Functor.Initial.conesEquiv F G).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun c =>
        CategoryTheory.Limits.Cone.ext
          (CategoryTheory.Iso.refl
            (((CategoryTheory.Limits.Cone.whiskering F).comp CategoryTheory.Functor.Initial.extendCone).obj c).pt)
          ⋯)
      ⋯
-- Lean.Server.References
/-- Find all identifiers in `self` with a reference in this module that contains `pos` in its range.
 -/
Lean.Lsp.ModuleRefs.findAt : Lean.Lsp.ModuleRefs → Lean.Lsp.Position → optParam Bool false → Array Lean.Lsp.RefIdent
-- Mathlib.Data.Vector.Defs
/-- Vector of length from a list `v`
with witness that `v` has length `n` maps to `v` under `toList`.  -/
List.Vector.toList_mk : ∀ {α : Type u_1} {n : ℕ} (v : List α) (P : v.length = n), List.Vector.toList ⟨v, P⟩ = v
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlock.image : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X} {H : Type u_3} {Y : Type u_4}
  [inst_2 : VAdd H Y] {φ : G → H} (j : X →ₑ[φ] Y),
  Function.Surjective φ → Function.Injective ⇑j → AddAction.IsBlock G B → AddAction.IsBlock H (⇑j '' B)
-- Init.Data.Option.Array
Option.foldrM_toArray : ∀ {m : Type u_1 → Type u_2} {β : Type u_3} {α : Type u_1} [inst : Monad m] [LawfulMonad m] (o : Option β) (a : α)
  (f : β → α → m α), Array.foldrM f a o.toArray = o.elim (pure a) fun b => f b a
-- Std.Data.DHashMap.Internal.Defs
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.Const.getD : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → (Std.DHashMap.Internal.Raw₀ α fun x => β) → α → β → β
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go_get : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (curr : ℕ) (hcurr : curr ≤ w)
  (cin : aig.Ref) (s : aig.RefVec curr) (lhs rhs : aig.RefVec w) (idx : ℕ) (hidx : idx < curr),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.go aig lhs rhs curr hcurr cin s).vec.get idx ⋯ = (s.get idx hidx).cast ⋯
-- Mathlib.Logic.Basic
of_not_imp : ∀ {a b : Prop}, ¬(a → b) → a
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.iff_of_isArtinianRing : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsArtinianRing R],
  Algebra.QuasiFinite R S ↔ Module.Finite R S
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor_obj_right_left_as : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor D T) (Y : T) (X : D)
  (Y_1 : CategoryTheory.StructuredArrow X (CategoryTheory.StructuredArrow.proj Y F)),
  ((CategoryTheory.StructuredArrow.ofStructuredArrowProjEquivalence.functor F Y X).obj Y_1).right.left.as = PUnit.unit
-- Init.Data.UInt.Lemmas
UInt8.neg_add : ∀ {a b : UInt8}, -(a + b) = -a - b
-- Mathlib.Algebra.Group.End
Equiv.swap_eq_one_iff : ∀ {α : Type u_4} [inst : DecidableEq α] {i j : α}, Equiv.swap i j = 1 ↔ i = j
-- Mathlib.Tactic.ENatToNat
Mathlib.Tactic.ENatToNat.coe_zero : 0 = ↑0
-- Mathlib.Algebra.Notation.Defs
SDiv.ext : ∀ {G : outParam (Type u_1)} {P : Type u_2} {x y : SDiv G P}, SDiv.sdiv = SDiv.sdiv → x = y
-- Init.Data.Option.Lemmas
Option.bind_eq_some_iff : ∀ {α : Type u_1} {b : α} {α_1 : Type u_2} {x : Option α_1} {f : α_1 → Option α},
  x.bind f = some b ↔ ∃ a, x = some a ∧ f a = some b
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- If for every cell either `A ∩ openCell n j` or `A ∩ closedCell n j` is closed then
`A` is closed.  -/
Topology.RelCWComplex.isClosed_of_isClosed_inter_openCell_or_isClosed_inter_closedCell : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] [T2Space X] {A : Set X},
  A ⊆ C →
    IsClosed (A ∩ D) →
      (∀ (n : ℕ),
          0 < n →
            ∀ (j : Topology.RelCWComplex.cell C n),
              IsClosed (A ∩ Topology.RelCWComplex.openCell n j) ∨ IsClosed (A ∩ Topology.RelCWComplex.closedCell n j)) →
        IsClosed A
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- If `F` is an equivalence, then so is the functor `(F ⋙ G, S) ⥤ (G, S)`.  -/
CategoryTheory.CostructuredArrow.isEquivalence_pre : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (S : D) [F.IsEquivalence], (CategoryTheory.CostructuredArrow.pre F G S).IsEquivalence
-- Mathlib.Algebra.Free
AddMagma.AssocRel.left : ∀ {α : Type u} [inst : Add α] (w x y z : α), AddMagma.AssocRel α (w + (x + y + z)) (w + (x + (y + z)))
-- Mathlib.Data.Set.SMulAntidiagonal
Set.vaddAntidiagonal.eq_1 : ∀ {G : Type u_1} {P : Type u_2} [inst : VAdd G P] (s : Set G) (t : Set P) (a : P),
  s.vaddAntidiagonal t a = {x | x.1 ∈ s ∧ x.2 ∈ t ∧ x.1 +ᵥ x.2 = a}
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.comap_map_eq_self_of_injective : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] {f : R →+* S},
  Function.Injective ⇑f → ∀ (s : Subsemiring R), Subsemiring.comap f (Subsemiring.map f s) = s
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Quiv.instCoeSortType : CoeSort CategoryTheory.Quiv (Type u)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
/-- **John Machin's 1706 formula**, which he used to compute π to 100 decimal places.  -/
Real.four_mul_arctan_inv_5_sub_arctan_inv_239 : 4 * Real.arctan 5⁻¹ - Real.arctan 239⁻¹ = Real.pi / 4
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.IsPresentationCore.mk.inj : ∀ {A : Type u} {inst : Ring A} {relations : Module.Relations A} {M : Type v} {inst_1 : AddCommGroup M}
  {inst_2 : Module A M} {solution : relations.Solution M}
  {desc : {N : Type w'} → [inst_3 : AddCommGroup N] → [inst_4 : Module A N] → relations.Solution N → M →ₗ[A] N}
  {postcomp_desc :
    ∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N),
      solution.postcomp (desc s) = s}
  {postcomp_injective :
    ∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] {f f' : M →ₗ[A] N},
      solution.postcomp f = solution.postcomp f' → f = f'}
  {desc_1 : {N : Type w'} → [inst_3 : AddCommGroup N] → [inst_4 : Module A N] → relations.Solution N → M →ₗ[A] N}
  {postcomp_desc_1 :
    ∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] (s : relations.Solution N),
      solution.postcomp (desc_1 s) = s}
  {postcomp_injective_1 :
    ∀ {N : Type w'} [inst_3 : AddCommGroup N] [inst_4 : Module A N] {f f' : M →ₗ[A] N},
      solution.postcomp f = solution.postcomp f' → f = f'},
  { desc := desc, postcomp_desc := postcomp_desc, postcomp_injective := postcomp_injective } =
      { desc := desc_1, postcomp_desc := postcomp_desc_1, postcomp_injective := postcomp_injective_1 } →
    desc = desc_1
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
ContDiffOn.rpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : E → ℝ} {s : Set E} {n : WithTop ℕ∞},
  ContDiffOn ℝ n f s → ContDiffOn ℝ n g s → (∀ x ∈ s, f x ≠ 0) → ContDiffOn ℝ n (fun x => f x ^ g x) s
-- Mathlib.Data.Sym.Basic
Sym.erase_mk : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (m : Multiset α) (hc : m.card = n + 1) (a : α) (h : a ∈ m),
  (Sym.mk m hc).erase a h = Sym.mk (m.erase a) ⋯
-- Mathlib.Algebra.Lie.Basic
LieModuleEquiv.symm_apply_apply : ∀ {R : Type u} {L : Type v} {M : Type w} {N : Type w₁} [inst : CommRing R] [inst_1 : LieRing L]
  [inst_2 : AddCommGroup M] [inst_3 : AddCommGroup N] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : LieRingModule L M] [inst_7 : LieRingModule L N] (e : M ≃ₗ⁅R,L⁆ N) (x : M), e.symm (e x) = x
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
/-- The "tautological" coloring of a graph, using the vertices of the graph as colors.  -/
SimpleGraph.selfColoring : {V : Type u} → (G : SimpleGraph V) → G.Coloring V
-- Mathlib.Topology.Category.LightProfinite.Sequence
_private.Mathlib.Topology.Category.LightProfinite.Sequence.0.LightProfinite.natUnionInftyEmbedding.match_1.eq_2 : ∀ (motive : OnePoint ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive none) (h_2 : (n : ℕ) → motive (some n)),
  (match some n with
    | none => h_1 ()
    | some n => h_2 n) =
    h_2 n