mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.Prod
/-- Project a walk on `G □ H` to a walk on `H` by discarding the moves in the direction of `G`.  -/
SimpleGraph.Walk.ofBoxProdRight : {α : Type u_1} →
  {β : Type u_2} →
    {G : SimpleGraph α} →
      {H : SimpleGraph β} → [DecidableEq α] → [DecidableRel H.Adj] → {x y : α × β} → (G □ H).Walk x y → H.Walk x.2 y.2
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.refl.sizeOf_spec : ∀ (s : Lean.Grind.AC.Seq), sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.refl s) = 1 + sizeOf s
-- Mathlib.SetTheory.Ordinal.Basic
hasWellFounded_toType : (o : Ordinal.{u_1}) → WellFoundedRelation o.ToType
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the angle between two vectors is nonzero, the second vector is nonzero.  -/
Orientation.right_ne_zero_of_oangle_ne_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, o.oangle x y ≠ 0 → y ≠ 0
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpi.fac_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y W : C} (f : Y ⟶ X)
  [inst_1 : CategoryTheory.EffectiveEpi f] (e : Y ⟶ W)
  (h :
    ∀ {Z : C} (g₁ g₂ : Z ⟶ Y),
      CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f →
        CategoryTheory.CategoryStruct.comp g₁ e = CategoryTheory.CategoryStruct.comp g₂ e)
  {Z : C} (h_1 : W ⟶ Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.EffectiveEpi.desc f e ⋯) h_1) =
    CategoryTheory.CategoryStruct.comp e h_1
-- Mathlib.Algebra.Homology.ShortComplex.Linear
/-- Homotopy between morphisms of short complexes is compatible with the scalar multiplication.  -/
CategoryTheory.ShortComplex.Homotopy.smul : {R : Type u_1} →
  {C : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : CategoryTheory.Category.{v_1, u_2} C] →
        [inst_2 : CategoryTheory.Preadditive C] →
          [inst_3 : CategoryTheory.Linear R C] →
            {S₁ S₂ : CategoryTheory.ShortComplex C} →
              {φ₁ φ₂ : S₁ ⟶ S₂} →
                CategoryTheory.ShortComplex.Homotopy φ₁ φ₂ →
                  (a : R) → CategoryTheory.ShortComplex.Homotopy (a • φ₁) (a • φ₂)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → (t₁ ∪ t₂).isEmpty = (t₁.isEmpty && t₂.isEmpty)
-- Mathlib.Order.DirSupClosed
DirSupClosedOn.iInter : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α] {ι : Sort u_2} {f : ι → Set α},
  (∀ (i : ι), DirSupClosedOn D (f i)) → DirSupClosedOn D (⋂ i, f i)
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.L₁_f_φ₁_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C) {Z : C} (h : S.L₂.X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.L₀'.f (CategoryTheory.CategoryStruct.comp S.φ₁ h) =
    CategoryTheory.CategoryStruct.comp S.v₁₂.τ₁ h
-- Init.Data.Slice.Lemmas
Std.Slice.foldl_toArray : ∀ {γ : Type u} {α β : Type v} {δ : Type u_1} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  [inst_2 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id] [Std.Iterators.Finite α Id] {s : Std.Slice γ}
  {init : δ} {f : δ → β → δ}, Array.foldl f init s.toArray = Std.Slice.foldl f init s
-- Mathlib.Algebra.Star.LinearMap
Matrix.intrinsicStar_toLin' : ∀ {R : Type u_4} {m : Type u_5} {n : Type u_6} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Fintype m]
  [inst_3 : DecidableEq m] (A : Matrix n m R),
  star (WithConv.toConv (Matrix.toLin' A)) = WithConv.toConv (Matrix.toLin' (A.map star))
-- Std.Data.Internal.List.Associative
Std.Internal.List.isSome_minEntry?_of_isEmpty_eq_false : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {l : List ((a : α) × β a)},
  l.isEmpty = false → (Std.Internal.List.minEntry? l).isSome = true
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi.eq_1 : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i)),
  MeasureTheory.Measure.infinitePi μ =
    if h : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i) then (MeasureTheory.piContent μ).measure ⋯ ⋯ ⋯ else 0
-- Mathlib.LinearAlgebra.Span.Basic
AddSubmonoid.toNatSubmodule_closure : ∀ {M : Type u_4} [inst : AddCommMonoid M] (s : Set M),
  AddSubmonoid.toNatSubmodule (AddSubmonoid.closure s) = Submodule.span ℕ s
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.Comonad.right_counit_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (self : CategoryTheory.Comonad C) (X : C) {Z : C}
  (h : self.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.δ.app X) (CategoryTheory.CategoryStruct.comp (self.map (self.ε.app X)) h) = h
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.instBot : {R : Type u} → [inst : NonUnitalNonAssocRing R] → Bot (NonUnitalSubring R)
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.Localization.instHasSmallLocalizedHomObjShiftFunctor_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C) {M : Type w'}
  [inst_1 : AddMonoid M] [inst_2 : CategoryTheory.HasShift C M] (X Y : C)
  [CategoryTheory.Localization.HasSmallLocalizedShiftedHom W M X Y] (m : M),
  CategoryTheory.Localization.HasSmallLocalizedHom W ((CategoryTheory.shiftFunctor C m).obj X) Y
-- Mathlib.Analysis.Normed.Algebra.Spectrum
spectrum.resolvent_tendsto_cobounded : ∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [CompleteSpace A] (a : A), Filter.Tendsto (resolvent a) (Bornology.cobounded 𝕜) (nhds 0)
-- Mathlib.Topology.GDelta.Basic
/-- To check that `s` is nowhere dense, it suffices to check that `closure s` is not a
neighborhood of any point of `s`.  -/
isNowhereDense_iff_forall_notMem_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsNowhereDense s ↔ ∀ x ∈ s, closure s ∉ nhds x
-- Init.Data.SInt.Lemmas
Int32.toInt_ofIntClamp : ∀ {x : ℤ}, Int32.minValue.toInt ≤ x → x ≤ Int32.maxValue.toInt → (Int32.ofIntClamp x).toInt = x
-- Mathlib.Analysis.SpecialFunctions.OrdinaryHypergeometric
/-- The coefficients in the ordinary hypergeometric sum.  -/
ordinaryHypergeometricCoefficient : {𝕂 : Type u_1} → [Field 𝕂] → 𝕂 → 𝕂 → 𝕂 → ℕ → 𝕂
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.extern.inj : ∀ {f : Lean.IR.FunId} {xs : Array Lean.IR.Param} {type : Lean.IR.IRType} {ext : Lean.ExternAttrData}
  {f_1 : Lean.IR.FunId} {xs_1 : Array Lean.IR.Param} {type_1 : Lean.IR.IRType} {ext_1 : Lean.ExternAttrData},
  Lean.IR.Decl.extern f xs type ext = Lean.IR.Decl.extern f_1 xs_1 type_1 ext_1 →
    f = f_1 ∧ xs = xs_1 ∧ type = type_1 ∧ ext = ext_1
-- Mathlib.Order.Filter.Pointwise
Filter.neg_le_neg : ∀ {α : Type u_2} [inst : Neg α] {f g : Filter α}, f ≤ g → -f ≤ -g
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get!_ofList_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {l : List α}
  {k k' : α},
  (k == k') = true → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.HashSet.Raw.ofList l).get! k' = k
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.lof.eq_1 : ∀ {I : Type u} [inst : DecidableEq I] (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] (i : I),
  LinearAlgebra.FreeProduct.lof R A i = LinearAlgebra.FreeProduct.ι' R A ∘ₗ DirectSum.lof R I A i
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_eq_one_iff : ∀ {α : Type u_1} (d : α →₀ ℕ), (d.sum fun x n => n) = 1 ↔ ∃ a, d = fun₀ | a => 1
-- Mathlib.CategoryTheory.Monad.Kleisli
/-- The Kleisli adjunction which gives rise to the monad `(T, η_ T, μ_ T)`.
cf Lemma 5.2.11 of [Riehl][riehl2017].  -/
CategoryTheory.Kleisli.Adjunction.adj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (T : CategoryTheory.Monad C) →
      CategoryTheory.Kleisli.Adjunction.toKleisli T ⊣ CategoryTheory.Kleisli.Adjunction.fromKleisli T
-- Lean.Parser.Command
Lean.Parser.Term.precheckedQuot : Lean.Parser.Parser
-- Mathlib.Algebra.FreeMonoid.Basic
/-- The identity equivalence between `List α` and `FreeAddMonoid α`.  -/
FreeAddMonoid.ofList : {α : Type u_1} → List α ≃ FreeAddMonoid α
-- Mathlib.Algebra.Lie.Weights.Killing
LieAlgebra.IsKilling.traceForm_coroot : ∀ {K : Type u_2} {L : Type u_3} [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L]
  [inst_3 : FiniteDimensional K L] {H : LieSubalgebra K L} [inst_4 : H.IsCartanSubalgebra]
  [inst_5 : LieAlgebra.IsKilling K L] (α : LieModule.Weight K (↥H) L) (x : ↥H),
  ((LieModule.traceForm K (↥H) L) (LieAlgebra.IsKilling.coroot α)) x =
    2 • (α ((LieAlgebra.IsKilling.cartanEquivDual H).symm (LieModule.Weight.toLinear K (↥H) L α)))⁻¹ • α x
-- Mathlib.Algebra.Order.Hom.Monoid
OrderMonoidIso.strictMono_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Mul α] [inst_3 : Mul β]
  (f : α ≃*o β), StrictMono ⇑f.symm
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.id_apply : ∀ {X : TopCat} {x : ↑X} {U : TopologicalSpace.OpenNhds x} (f : U ⟶ U) (y : ↥↑U), f y = y
-- Init.Data.Order.Ord
Std.OrientedCmp.not_gt_of_isGE : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α}, (cmp a b).isGE = true → cmp b a ≠ Ordering.gt
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.coe_toCoalgEquiv : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B), ⇑e.toAlgEquiv = ⇑e
-- Mathlib.Order.Category.LinOrd
LinOrd.instCategory : CategoryTheory.Category.{u, u + 1} LinOrd
-- Lean.Level
Lean.Level.isSucc : Lean.Level → Bool
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem?_toArray_ric : ∀ {n i : ℕ}, (*...=n).toArray[i]? = if i ≤ n then some i else none
-- Mathlib.Data.TypeVec
TypeVec.toSubtype.eq_def : ∀ (x : ℕ) (x_1 : TypeVec.{u} x) (x_2 : x_1.Arrow (TypeVec.repeat x Prop)) (x_3 : Fin2 x)
  (x_4 : { x_4 // TypeVec.ofRepeat (x_2 x_3 x_4) }),
  TypeVec.toSubtype x_2 x_3 x_4 =
    match x, x_1, x_2, x_3, x_4 with
    | n.succ, x, p, i.fs, x_5 => TypeVec.toSubtype (TypeVec.dropFun p) i x_5
    | n.succ, x, x_5, Fin2.fz, x_6 => x_6
-- Mathlib.Topology.Algebra.UniformConvergence
instZeroUniformFun : {α : Type u_1} → {β : Type u_2} → [Zero β] → Zero (UniformFun α β)
-- Mathlib.MeasureTheory.Integral.Lebesgue.Norm
MeasureTheory.lintegral_enorm_of_ae_nonneg : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ℝ},
  0 ≤ᵐ[μ] f → ∫⁻ (x : α), ‖f x‖ₑ ∂μ = ∫⁻ (x : α), ENNReal.ofReal (f x) ∂μ
-- Mathlib.Order.Basic
/-- Pull back a `PartialOrder` instance along an injective function.

See note [reducible non-instances].  -/
Function.Injective.partialOrder : {α : Type u_2} →
  {β : Type u_3} →
    [inst : PartialOrder β] →
      [inst_1 : LE α] →
        [inst_2 : LT α] →
          (f : α → β) →
            Function.Injective f → (∀ {x y : α}, f x ≤ f y ↔ x ≤ y) → (∀ {x y : α}, f x < f y ↔ x < y) → PartialOrder α
-- Mathlib.Algebra.Ring.Ext
Ring.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : Ring R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ HMul.hMul = HMul.hMul
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.one_le : ∀ {G : Type u_1} [inst : Group G] {A : Set G} {K : ℝ}, IsApproximateSubgroup K A → 1 ≤ K
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.coeff_monomial_mul : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (m s : σ →₀ ℕ) (r : R) (p : MvPolynomial σ R),
  MvPolynomial.coeff (s + m) ((MvPolynomial.monomial s) r * p) = r * MvPolynomial.coeff m p
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
instContMDiffInv₀ModelWithCornersSelf : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}, ContMDiffInv₀ (modelWithCornersSelf 𝕜 𝕜) n 𝕜
-- Lean.DocString.Parser
/-- Parses inline code.
 -/
Lean.Doc.Parser.code : Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.hasFiniteColimits : CategoryTheory.Limits.HasFiniteColimits FintypeCat
-- Lean.Data.Json.Basic
Lean.Json.num.inj : ∀ {n n_1 : Lean.JsonNumber}, Lean.Json.num n = Lean.Json.num n_1 → n = n_1
-- Mathlib.CategoryTheory.Monoidal.Hopf_
CategoryTheory.HopfObj.mul_antipode₁ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (A : C) [inst_3 : CategoryTheory.HopfObj A],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.comul CategoryTheory.ComonObj.comul)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.associator A A (CategoryTheory.MonoidalCategoryStruct.tensorObj A A)).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
            (CategoryTheory.MonoidalCategoryStruct.associator A A A).inv)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A
              (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ A A).hom A))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.MonoidalCategoryStruct.associator A (CategoryTheory.MonoidalCategoryStruct.tensorObj A A)
                  A).inv
              (CategoryTheory.CategoryStruct.comp
                (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                  (CategoryTheory.MonoidalCategoryStruct.associator A A A).inv A)
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.MonObj.mul A) A)
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.MonoidalCategoryStruct.whiskerRight
                      (CategoryTheory.MonoidalCategoryStruct.whiskerRight CategoryTheory.HopfObj.antipode A) A)
                    (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator A A A).hom
                      (CategoryTheory.CategoryStruct.comp
                        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A CategoryTheory.MonObj.mul)
                        CategoryTheory.MonObj.mul))))))))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.ComonObj.counit CategoryTheory.ComonObj.counit)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
        CategoryTheory.MonObj.one)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.cocyclesMap_comp : ∀ {k : Type u} [inst : CommRing k] {G H K : Type u} [inst_1 : Group G] [inst_2 : Group H] [inst_3 : Group K]
  {A : Rep.{u, u, u} k K} {B : Rep.{u, u, u} k H} {C : Rep.{u, u, u} k G} (f : H →* K) (g : G →* H)
  (φ : Rep.res f A ⟶ B) (ψ : Rep.res g B ⟶ C) (n : ℕ),
  groupCohomology.cocyclesMap (f.comp g) (CategoryTheory.CategoryStruct.comp ((Rep.resFunctor g).map φ) ψ) n =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap f φ n) (groupCohomology.cocyclesMap g ψ n)
-- Mathlib.Data.Vector.Defs
/-- `shiftRightFill v i` is the vector obtained by right-shifting `v` `i` times and padding with the
`fill` argument. If `v.length < i` then this will return `replicate n fill`.  -/
List.Vector.shiftRightFill : {α : Type u_1} → {n : ℕ} → List.Vector α n → ℕ → α → List.Vector α n
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.Mon_tensor_one_mul : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (M N : C) [inst_3 : CategoryTheory.MonObj M]
  [inst_4 : CategoryTheory.MonObj N],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one))
        (CategoryTheory.MonoidalCategoryStruct.tensorObj M N))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
        (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul)) =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj M N)).hom
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imJ_im : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : Zero R], a.im.imJ = a.imJ
-- Mathlib.Order.SuccPred.Basic
Order.lt_succ_bot_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a : α} [inst_2 : OrderBot α] [NoMaxOrder α],
  a < Order.succ ⊥ ↔ a = ⊥
-- Mathlib.Data.Sign.Basic
SignType.zpow_odd : ∀ (s : SignType) {z : ℤ}, Odd z → s ^ z = s
-- Mathlib.Tactic.ClickSuggestions.ApplyAt
/-- The new goals.  -/
Mathlib.Tactic.ClickSuggestions.ApplyAtKey.newGoals : Mathlib.Tactic.ClickSuggestions.ApplyAtKey → Array Lean.Meta.AbstractMVarsResult
-- Mathlib.RingTheory.Congruence.Defs
/-- A congruence relation on a type with an addition and multiplication is an equivalence relation
which preserves both.  -/
RingCon : (R : Type u_1) → [Add R] → [Mul R] → Type u_1
-- Lean.Meta.Tactic.Simp.SimpTheorems
_private.Lean.Meta.Tactic.Simp.SimpTheorems.0.Lean.Meta.preprocess.go : Bool → Bool → Lean.Expr → Lean.Expr → Lean.MetaM (List (Lean.Expr × Lean.Expr))
-- Lean.Elab.Task
/-- Given a monadic value in `CoreM`, creates a task that runs it in the current state,
returning
* a cancellation hook and
* a monadic value with the cached result (and subsequent state as it was after running).

The task is run with a fresh `CancelToken` in its context, so it can detect cancellation
via `Core.checkInterrupted`. The cancellation hook sets this token.

Uses `Core.wrapAsync` internally to properly handle name generators and heartbeats.

Note: We only set the cancel token and don't call `IO.cancel task`. We're uncertain whether
`IO.cancel` is also necessary - it may be required for tasks that use `IO.checkCanceled`
instead of `Core.checkInterrupted`.
 -/
Lean.Core.CoreM.asTask : {α : Type} → Lean.CoreM α → Lean.CoreM (BaseIO Unit × Task (Lean.CoreM α))
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.instInhabitedOverlaps.default : Lean.Meta.Match.Overlaps
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.isUnit_T : ∀ {R : Type u_1} [inst : Semiring R] (n : ℤ), IsUnit (LaurentPolynomial.T n)
-- Mathlib.RingTheory.KrullDimension.Basic
_private.Mathlib.RingTheory.KrullDimension.Basic.0.MvPolynomial.fin_ringKrullDim_eq_add_of_isNoetherianRing : {R : Type u_1} →
  [inst : CommSemiring R] →
    [IsNoetherianRing R] → (n : ℕ) → ProofWanted (ringKrullDim (MvPolynomial (Fin n) R) = ringKrullDim R + ↑n)
-- Std.Tactic.BVDecide.LRAT.Parser
_private.Std.Tactic.BVDecide.LRAT.Parser.0.Std.Tactic.BVDecide.LRAT.lratProofToString.serializeRatHints : Array (ℕ × Array ℕ) → String
-- Mathlib.Analysis.Normed.Operator.Banach
AffineMap.isOpenMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [CompleteSpace E] {F : Type u_5} [inst_4 : NormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F]
  [CompleteSpace F] {P : Type u_6} {Q : Type u_7} [inst_7 : MetricSpace P] [inst_8 : NormedAddTorsor E P]
  [inst_9 : MetricSpace Q] [inst_10 : NormedAddTorsor F Q] (f : P →ᵃ[𝕜] Q),
  Continuous ⇑f → Function.Surjective ⇑f → IsOpenMap ⇑f
-- Init.Data.BitVec.Bitblast
/-- the numerator (aka, dividend)  -/
BitVec.DivModArgs.n : {w : ℕ} → BitVec.DivModArgs w → BitVec w
-- Mathlib.Algebra.Order.Ring.Abs
le_of_sq_le_sq : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {a b : α},
  a ^ 2 ≤ b ^ 2 → 0 ≤ b → a ≤ b
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instInhabitedPower : Inhabited Lean.Grind.CommRing.Power
-- Mathlib.Data.Set.Monotone
Set.EqOn.congr_strictMonoOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {f₁ f₂ : α → β} [inst : Preorder α] [inst_1 : Preorder β],
  Set.EqOn f₁ f₂ s → (StrictMonoOn f₁ s ↔ StrictMonoOn f₂ s)
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.disjoint_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M) {p q : ↥f.invtSubmodule}, Disjoint p q ↔ Disjoint ↑p ↑q
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.op_iSup : ∀ {ι : Sort u_1} {R : Type u_2} [inst : NonAssocSemiring R] (S : ι → Subsemiring R), (iSup S).op = ⨆ i, (S i).op
-- Mathlib.Topology.Constructions
Topology.IsClosedEmbedding.subtypeVal : ∀ {X : Type u} [inst : TopologicalSpace X] {p : X → Prop}, IsClosed {a | p a} → Topology.IsClosedEmbedding Subtype.val
-- Mathlib.Analysis.Normed.Operator.Asymptotics
ContinuousLinearEquiv.isBigO_comp_rev : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : SeminormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} {σ₂₁ : 𝕜₂ →+* 𝕜}
  [inst_6 : RingHomInvPair σ₁₂ σ₂₁] [inst_7 : RingHomInvPair σ₂₁ σ₁₂] (e : E ≃SL[σ₁₂] F) [RingHomIsometric σ₂₁]
  {α : Type u_7} (f : α → E) (l : Filter α), f =O[l] fun x' => e (f x')
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.prod_map_fst : ∀ (X Y : SSet) {m n : SimplexCategoryᵒᵖ} (f : m ⟶ n) (z : (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).obj m),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.tensorHom (X.map f) (Y.map f))) z).1 =
    (CategoryTheory.ConcreteCategory.hom (X.map f)) z.1
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- Isomorphic algebras have isomorphic localizations.

See `localAlgEquiv'` for a variant where the base ring is also localized.  -/
Localization.localAlgEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    {S : Type u_2} →
      [inst_1 : CommSemiring S] →
        [inst_2 : Algebra R S] →
          {P : Type u_3} →
            [inst_3 : CommSemiring P] →
              [inst_4 : Algebra R P] →
                (I : Ideal S) →
                  [inst_5 : I.IsPrime] →
                    (J : Ideal P) →
                      [inst_6 : J.IsPrime] →
                        (f : S ≃ₐ[R] P) → I = Ideal.comap f J → Localization.AtPrime I ≃ₐ[R] Localization.AtPrime J
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.adjoin.setCoe : (F : Type u_1) →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] → [inst_2 : Algebra F E] → (S : Set E) → CoeTC ↑S ↥(IntermediateField.adjoin F S)
-- Mathlib.Analysis.Complex.HasPrimitives
_private.Mathlib.Analysis.Complex.HasPrimitives.0.Complex.mem_ball_of_map_im_aux₂ : ∀ {c z : ℂ} {r : ℝ} {w : ℂ},
  w ∈ Metric.ball z (r - dist z c) → (fun y => ↑w.re + ↑y * Complex.I) '' Set.uIcc z.im w.im ⊆ Metric.ball c r
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgebra.adjoin_eq_span : ∀ {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] (s : Set A),
  (NonUnitalAlgebra.adjoin R s).toSubmodule = Submodule.span R ↑(Subsemigroup.closure s)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α},
  k ∉ m₁ → (m₁ ∪ m₂).get? k = m₂.get? k
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_eq_fallback : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = true → ∀ {fallback : α}, t.minD fallback = fallback