mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Elab.Command
/-- Returns syntax for `private` if `attrKind` is `local` and `public` otherwise.
 -/
Lean.Parser.Command.visibility.ofAttrKind : Lean.TSyntax `Lean.Parser.Term.attrKind → Lean.TSyntax `Lean.Parser.Command.visibility
-- Init.Data.BitVec.Lemmas
BitVec.getElem_ofFin : ∀ {n : ℕ} (x : Fin (2 ^ n)) (i : ℕ) (h : i < n), { toFin := x }[i] = (↑x).testBit i
-- Mathlib.Algebra.Category.Grp.FilteredColimits
CommGrpCat.FilteredColimits.colimitCocone.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J CommGrpCat),
  CommGrpCat.FilteredColimits.colimitCocone F =
    { pt := CommGrpCat.FilteredColimits.colimit F,
      ι :=
        {
          app := fun J_1 =>
            CommGrpCat.ofHom
              (GrpCat.Hom.hom
                ((GrpCat.FilteredColimits.colimitCocone (F.comp (CategoryTheory.forget₂ CommGrpCat GrpCat))).ι.app
                  J_1)),
          naturality := ⋯ } }
-- Mathlib.Analysis.Polynomial.Basic
Polynomial.tendsto_atBot_of_leadingCoeff_nonpos : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] (P : Polynomial 𝕜)
  [OrderTopology 𝕜],
  0 < P.degree → P.leadingCoeff ≤ 0 → Filter.Tendsto (fun x => Polynomial.eval x P) Filter.atTop Filter.atBot
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
instFiniteTypeCarrierObjCommAlgCat : ∀ (R : Type u) [inst : CommRing R] (A : FGAlgCat R), Algebra.FiniteType R ↑A.obj
-- Mathlib.Data.ENat.Basic
ENat.add_le_add_iff_right : ∀ {m n k : ℕ∞}, k ≠ ⊤ → (n + k ≤ m + k ↔ n ≤ m)
-- Mathlib.NumberTheory.Height.NumberField
/-- The absolute multiplicative height of an algebraic number. This is defined for elements of any
field of characteristic zero, with a junk value of `0` if the element is not algebraic.  -/
NumberField.absMulHeight₁ : {K : Type u_2} → [inst : Field K] → [CharZero K] → K → ℝ
-- Mathlib.Analysis.Calculus.Deriv.Comp
HasDerivWithinAt.comp_hasFDerivAt : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type w} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕜' : Type u_1} [inst_3 : NontriviallyNormedField 𝕜'] [inst_4 : NormedAlgebra 𝕜 𝕜']
  {h₂ : 𝕜' → 𝕜'} {h₂' : 𝕜'} {f : E → 𝕜'} {f' : E →L[𝕜] 𝕜'} {t : Set 𝕜'} (x : E),
  HasDerivWithinAt h₂ h₂' t (f x) →
    HasFDerivAt f f' x → (∀ᶠ (x' : E) in nhds x, f x' ∈ t) → HasFDerivAt (h₂ ∘ f) (h₂' • f') x
-- Lean.Util.MonadCache
Lean.MonadHashMapCacheAdapter.getCache : {α β : Type} →
  {m : Type → Type} →
    {inst : BEq α} → {inst_1 : Hashable α} → [self : Lean.MonadHashMapCacheAdapter α β m] → m (Std.HashMap α β)
-- Mathlib.CategoryTheory.EpiMono
/-- The map splitting `f`  -/
CategoryTheory.SplitEpi.section_ : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] → {X Y : C} → {f : X ⟶ Y} → CategoryTheory.SplitEpi f → (Y ⟶ X)
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_lt_of_lt_map_of_injective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Injective ⇑f → ∀ {p : Submodule R M} {q : Submodule R₂ M₂}, q < Submodule.map f p → Submodule.comap f q < p
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
/-- `DerivedCategory.singleFunctor` commutes with `F` and `F.mapDerivedCategory`.  -/
CategoryTheory.Functor.mapDerivedCategorySingleFunctor : {C₁ : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
    [inst_1 : CategoryTheory.Abelian C₁] →
      [inst_2 : HasDerivedCategory C₁] →
        {C₂ : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_4 : CategoryTheory.Abelian C₂] →
              [inst_5 : HasDerivedCategory C₂] →
                (F : CategoryTheory.Functor C₁ C₂) →
                  [inst_6 : F.Additive] →
                    [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F] →
                      [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] →
                        (n : ℤ) →
                          (DerivedCategory.singleFunctor C₁ n).comp F.mapDerivedCategory ≅
                            F.comp (DerivedCategory.singleFunctor C₂ n)
-- Mathlib.NumberTheory.LSeries.Convolution
/-- The abscissa of absolute convergence of `f ⍟ g` is at most the maximum of those
of `f` and `g`.  -/
LSeries.abscissaOfAbsConv_convolution_le : ∀ (f g : ℕ → ℂ),
  LSeries.abscissaOfAbsConv (LSeries.convolution f g) ≤ max (LSeries.abscissaOfAbsConv f) (LSeries.abscissaOfAbsConv g)
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.eta_fin_two : ∀ {α : Type u} (A : Matrix (Fin 2) (Fin 2) α), A = !![A 0 0, A 0 1; A 1 0, A 1 1]
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.braiding_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X X' Y Y' : C} (f : X ⟶ Y) (g : X' ⟶ Y') {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y' Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
      (CategoryTheory.CategoryStruct.comp (β_ Y Y').hom h) =
    CategoryTheory.CategoryStruct.comp (β_ X X').hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f) h)
-- Std.Data.HashSet.Lemmas
/-- This is a restatement of `contains_insert` that is written to exactly match the proof
obligation in the statement of `get_insert`.  -/
Std.HashSet.contains_of_contains_insert' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k a : α},
  (m.insert k).contains a = true → ¬((k == a) = true ∧ m.contains k = false) → m.contains a = true
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.instAlgebraSubtypePreLpMemAddSubgroupTopENNReal : {𝕜 : Type u_1} →
  {I : Type u_5} →
    {B : I → Type u_6} →
      [inst : NormedField 𝕜] →
        [inst_1 : (i : I) → NormedRing (B i)] →
          [(i : I) → NormedAlgebra 𝕜 (B i)] → [inst_3 : ∀ (i : I), NormOneClass (B i)] → Algebra 𝕜 ↥(lp B ⊤)
-- Init.Data.BitVec.Lemmas
BitVec.smtUDiv_eq : ∀ {w : ℕ} (x y : BitVec w), x.smtUDiv y = if y = 0#w then BitVec.allOnes w else x / y
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {f : β → β},
  t.modify k f ≠ ∅ →
    ∀ {fallback : α},
      (t.modify k f).minKeyD fallback = if cmp (t.minKeyD fallback) k = Ordering.eq then k else t.minKeyD fallback
-- Init.Data.Range.Polymorphic.UpwardEnumerable
Std.PRange.UpwardEnumerable.succMany.congr_simp : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.PRange.InfinitelyUpwardEnumerable α] (n n_1 : ℕ),
  n = n_1 → ∀ (a a_1 : α), a = a_1 → Std.PRange.succMany n a = Std.PRange.succMany n_1 a_1
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.comp_mk_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  [inst_1 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y]
  [inst_2 : CategoryTheory.Localization.HasSmallLocalizedHom W Y Y] (α : CategoryTheory.Localization.SmallHom W X Y),
  α.comp (CategoryTheory.Localization.SmallHom.mk W (CategoryTheory.CategoryStruct.id Y)) = α
-- Mathlib.Algebra.Group.End
MulAut.conj_apply : ∀ {G : Type u_3} [inst : Group G] (g h : G), (MulAut.conj g) h = g * h * g⁻¹
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.comap_bot : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (f : G →* N), Subgroup.comap f ⊥ = f.ker
-- Init.Data.Vector.Lemmas
/-- Flattening a reverse is the same as reversing all parts and reversing the flattened result.  -/
Vector.flatten_reverse : ∀ {α : Type u_1} {m n : ℕ} {xss : Vector (Vector α m) n},
  xss.reverse.flatten = (Vector.map Vector.reverse xss).flatten.reverse
-- Mathlib.Algebra.Group.Units.Basic
IsUnit.inv_mul_cancel_right : ∀ {α : Type u} [inst : DivisionMonoid α] {b : α}, IsUnit b → ∀ (a : α), a * b⁻¹ * b = a
-- Lean.Meta.Basic
/-- Configuration flags for the `MetaM` monad.
Many of them are used to control the `isDefEq` function that checks whether two terms are definitionally equal or not.
Recall that when `isDefEq` is trying to check whether
`?m@C a₁ ... aₙ` and `t` are definitionally equal (`?m@C a₁ ... aₙ =?= t`), where
`?m@C` as a shorthand for `C |- ?m : ty` where `ty` is the type of `?m`.
We solve it using the assignment `?m := fun a₁ ... aₙ => t` if
1) `a₁ ... aₙ` are pairwise distinct free variables that are ​*not*​ let-variables.
2) `a₁ ... aₙ` are not in `C`
3) `t` only contains free variables in `C` and/or `{a₁, ..., aₙ}`
4) For every metavariable `?m'@C'` occurring in `t`, `C'` is a subprefix of `C`
5) `?m` does not occur in `t`
 -/
Lean.Meta.Config : Type
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.isoFromComma_inv : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  {L : CategoryTheory.Functor A T} {R : CategoryTheory.Functor B T} {P : CategoryTheory.MorphismProperty T}
  {Q : CategoryTheory.MorphismProperty A} {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative]
  [inst_4 : W.IsMultiplicative] [inst_5 : Q.RespectsIso] [inst_6 : W.RespectsIso]
  {X Y : CategoryTheory.MorphismProperty.Comma L R P Q W} (i : X.toComma ≅ Y.toComma),
  (CategoryTheory.MorphismProperty.Comma.isoFromComma i).inv =
    CategoryTheory.MorphismProperty.Comma.homFromCommaOfIsIso i.inv
-- Mathlib.Algebra.Regular.Basic
/-- An element admitting a right additive opposite is add-right-regular.  -/
isAddRightRegular_of_add_eq_zero : ∀ {R : Type u_1} [inst : AddMonoid R] {a b : R}, a + b = 0 → IsAddRightRegular a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.instLawfulVecOperatorTwoPowShiftTargetTwoPowShift : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Tactic.BVDecide.BVExpr.bitblast.TwoPowShiftTarget fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRight.twoPowShift
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.f_le_g_nat : ∀ (k : ℕ) {a t : ℝ}, 0 ≤ a → 0 < t → ∀ (n : ℕ), ‖HurwitzKernelBounds.f_nat k a t n‖ ≤ HurwitzKernelBounds.g_nat k a t n
-- Mathlib.Geometry.Manifold.DerivationBundle
/-- The heterogeneous differential as a linear map, denoted as `𝒅ₕ` within the `Manifold` namespace.
Instead of taking a function as an argument, this
differential takes `h : f x = y`. It is particularly handy for situations where the points
at which it has to be evaluated are equal but not definitionally equal.  -/
hfdifferential : {𝕜 : 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] →
                      {E' : Type u_5} →
                        [inst_6 : NormedAddCommGroup E'] →
                          [inst_7 : NormedSpace 𝕜 E'] →
                            {H' : Type u_6} →
                              [inst_8 : TopologicalSpace H'] →
                                {I' : ModelWithCorners 𝕜 E' H'} →
                                  {M' : Type u_7} →
                                    [inst_9 : TopologicalSpace M'] →
                                      [inst_10 : ChartedSpace H' M'] →
                                        {f : ContMDiffMap I I' M M' ↑⊤} →
                                          {x : M} → {y : M'} → f x = y → PointDerivation I x →ₗ[𝕜] PointDerivation I' y
-- Mathlib.CategoryTheory.Bicategory.Coherence
/-- The normalization pseudofunctor for the free bicategory on a quiver `B`.  -/
CategoryTheory.FreeBicategory.normalize : (B : Type u) →
  [inst : Quiver B] →
    CategoryTheory.Pseudofunctor (CategoryTheory.FreeBicategory B)
      (CategoryTheory.LocallyDiscrete (CategoryTheory.Paths B))
-- Mathlib.RingTheory.Ideal.Operations
Ideal.sup_mul_left_self : ∀ {R : Type u} [inst : Semiring R] {I J : Ideal R}, I ⊔ J * I = I
-- Std.Sat.AIG.RefVec
_private.Std.Sat.AIG.RefVec.0.Std.Sat.AIG.BinaryRefVec.cast.match_1.eq_1 : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig1 : Std.Sat.AIG α}
  (motive : aig1.BinaryRefVec len → Sort u_1) (lhs rhs : aig1.RefVec len)
  (h_1 : (lhs rhs : aig1.RefVec len) → motive { lhs := lhs, rhs := rhs }),
  (match { lhs := lhs, rhs := rhs } with
    | { lhs := lhs, rhs := rhs } => h_1 lhs rhs) =
    h_1 lhs rhs
-- Mathlib.Analysis.SumOverResidueClass
Finset.sum_indicator_mod : ∀ {R : Type u_1} [inst : AddCommMonoid R] (m : ℕ) [inst_1 : NeZero m] (f : ℕ → R), f = ∑ a, {n | ↑n = a}.indicator f
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
Unitary.expUnitary_eq_mul_inv : ∀ {A : Type u_1} [inst : CStarAlgebra A] (u v : ↥(unitary A)),
  ‖↑u - ↑v‖ < 2 → selfAdjoint.expUnitary (Unitary.argSelfAdjoint (u * star v)) = u * star v
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.eq_succMany?_of_toList_eq_append_cons : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {pref suff : List α} {cur : α} (h : r.toList = pref ++ cur :: suff),
  cur = (Std.PRange.succMany? (pref.length + 1) r.lower).get ⋯
-- Mathlib.RingTheory.Coalgebra.TensorProduct
Coalgebra.TensorProduct.rid_tmul : ∀ {R : Type u_5} {S : Type u_6} {M : Type u_7} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S]
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  [inst_7 : Coalgebra S M] (r : R) (a : M), (Coalgebra.TensorProduct.rid R S M) (a ⊗ₜ[R] r) = r • a
-- Mathlib.Order.Heyting.Hom
/-- `id` as a `CoheytingHom`.  -/
CoheytingHom.id : (α : Type u_2) → [inst : CoheytingAlgebra α] → CoheytingHom α α
-- Init.Data.Int.Gcd
Int.lcm_mul_right_right_eq_mul_of_lcm_eq_mul : ∀ {n m k : ℤ}, n.lcm m = n.natAbs * m.natAbs → n.lcm (m * k) = n.lcm k * m.natAbs
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.descRightHomology.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) {A : C} (k : S.X₂ ⟶ A) (hk : CategoryTheory.CategoryStruct.comp S.f k = 0)
  [inst_2 : S.HasRightHomology],
  S.descRightHomology k hk = CategoryTheory.CategoryStruct.comp S.rightHomologyι (S.descOpcycles k hk)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
spectrum_realPart : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : Algebra ℂ A]
  [inst_4 : StarModule ℂ A] [ContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A),
  autoParam (IsStarNormal a) spectrum_realPart._auto_1 → spectrum ℂ ↑(realPart a) = (fun x => ↑x.re) '' spectrum ℂ a
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.Internal.List.insertList.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] (l : List ((a : α) × β a)) (k : α) (v : β k)
  (l_1 : List ((a : α) × β a)),
  Std.Internal.List.insertList l (⟨k, v⟩ :: l_1) =
    Std.Internal.List.insertList (Std.Internal.List.insertEntry k v l) l_1
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Finite
CategoryTheory.Limits.createsLimitsOfShapeOfCreatesFiniteProducts : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [CategoryTheory.Limits.CreatesFiniteProducts F] →
            (J : Type w) → [Finite J] → CategoryTheory.CreatesLimitsOfShape (CategoryTheory.Discrete J) F
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.map_lieSpan : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {L₂ : Type w}
  [inst_3 : LieRing L₂] [inst_4 : LieAlgebra R L₂] (f : L →ₗ⁅R⁆ L₂) {s : Set L},
  LieSubalgebra.map f (LieSubalgebra.lieSpan R L s) = LieSubalgebra.lieSpan R L₂ (⇑f '' s)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_getElem?_eq_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, t[a]?.isSome = t.contains a
-- Init.Data.Iterators.Basic
/-- `IterStep α β` represents a step taken by an iterator (`Iter β` or `IterM m β`).
 -/
Std.IterStep : Sort u_1 → Sort u_2 → Sort (max (max 1 u_1) u_2)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.log_of_left_le_one : ∀ {b : Ordinal.{u_1}}, b ≤ 1 → ∀ (x : Ordinal.{u_1}), Ordinal.log b x = 0
-- Mathlib.RingTheory.TensorProduct.Finite
Subalgebra.finite_sup : ∀ {K : Type u_1} {L : Type u_2} [inst : CommSemiring K] [inst_1 : CommSemiring L] [inst_2 : Algebra K L]
  (E1 E2 : Subalgebra K L) [Module.Finite K ↥E1] [Module.Finite K ↥E2], Module.Finite K ↥(E1 ⊔ E2)
-- Mathlib.Analysis.Normed.Module.Bases
/-- Constructs a Schauder basis from rank one decomposition.  -/
SchauderBasis.RankOneDecomposition.basis : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {X : Type u_2} →
      [inst_1 : NormedAddCommGroup X] →
        [inst_2 : NormedSpace 𝕜 X] → SchauderBasis.RankOneDecomposition 𝕜 X → SchauderBasis 𝕜 X
-- Mathlib.LinearAlgebra.Span.Basic
AddSubgroup.toIntSubmodule_closure : ∀ {M : Type u_11} [inst : AddCommGroup M] (s : Set M),
  AddSubgroup.toIntSubmodule (AddSubgroup.closure s) = Submodule.span ℤ s
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.continuous_toUpper : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : TopologicalSpace α] [ClosedIicTopology α],
  Continuous ⇑Topology.WithUpper.toUpper
-- Mathlib.Topology.CompactOpen
/-- The map from `X × C(Y, Z)` to `C(Y, X × Z)` is continuous.  -/
ContinuousMap.continuous_prodMk_const : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z], Continuous fun p => (ContinuousMap.const Y p.1).prodMk p.2
-- Mathlib.Combinatorics.SetFamily.LYM
Finset.slice.eq_1 : ∀ {α : Type u_1} (𝒜 : Finset (Finset α)) (r : ℕ), 𝒜.slice r = {A ∈ 𝒜 | A.card = r}
-- Mathlib.Tactic.Linarith.Verification
/-- A typesafe version of `mulExpr`.  -/
Mathlib.Tactic.Linarith.mulExpr' : {u : Lean.Level} →
  ℕ →
    {α :
        have u := u;
        Q(Type u)} →
      Q(Semiring «$α») → Q(«$α») → Q(«$α»)
-- Init.Data.Iterators.Lemmas.Combinators.Take
Std.Iter.toList_take_of_finite : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {n : ℕ} [Std.Iterators.Finite α Id] {it : Std.Iter β},
  (Std.Iter.take n it).toList = List.take n it.toList
-- Mathlib.LinearAlgebra.Semisimple
Module.End.isSemisimple_of_squarefree_aeval_eq_zero : ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f : Module.End K M}
  {p : Polynomial K}, Squarefree p → (Polynomial.aeval f) p = 0 → f.IsSemisimple
-- Mathlib.Algebra.ContinuedFractions.Determinant
/-- The determinant formula `Aₙ * Bₙ₊₁ - Bₙ * Aₙ₊₁ = (-a₀) * (-a₁) * .. * (-aₙ)`.  -/
GenContFract.determinant : ∀ {K : Type u_1} [inst : Field K] {g : GenContFract K} {n : ℕ},
  g.nums n * g.dens (n + 1) - g.dens n * g.nums (n + 1) = ∏ i ∈ Finset.range (n + 1), -(g.partNums.get? i).getD 0
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.instIsOpenImmersionCommRingCatMapSheafedSpaceForgetToSheafedSpace : ∀ {X Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  AlgebraicGeometry.SheafedSpace.IsOpenImmersion (AlgebraicGeometry.LocallyRingedSpace.forgetToSheafedSpace.map f)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Reverse the bits in a bitvector.
 -/
Std.Tactic.BVDecide.BVUnOp.reverse : Std.Tactic.BVDecide.BVUnOp
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsCondKernelCDF.toKernel.congr_simp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {x : MeasurableSpace β}
  {κ κ_1 : ProbabilityTheory.Kernel α (β × ℝ)} (e_κ : κ = κ_1) {ν ν_1 : ProbabilityTheory.Kernel α β} (e_ν : ν = ν_1)
  (f f_1 : α × β → StieltjesFunction ℝ) (e_f : f = f_1) (hf : ProbabilityTheory.IsCondKernelCDF f κ ν),
  ProbabilityTheory.IsCondKernelCDF.toKernel f hf = ProbabilityTheory.IsCondKernelCDF.toKernel f_1 ⋯
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
Algebra.finite_adjoin_simple_of_isIntegral : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {x : B},
  IsIntegral R x → Module.Finite R ↥R[x]
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.instTop : {G : Type u_1} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → Top (OpenAddSubgroup G)
-- Mathlib.RingTheory.Ideal.Prime
IsDomain.of_bot_isPrime : ∀ (A : Type u_1) [inst : Ring A] [hbp : ⊥.IsPrime], IsDomain A
-- Mathlib.Data.Int.Sqrt
Int.sqrt_natCast : ∀ (n : ℕ), Int.sqrt ↑n = ↑n.sqrt
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.eq_comp_symm : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β]
  (e : α ≃+o β) (f : β → α) (g : α → α), f = g ∘ ⇑e.symm ↔ f ∘ ⇑e = g
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.exists_eccent_eq_ediam_of_ne_top : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α], G.ediam ≠ ⊤ → ∃ u, G.eccent u = G.ediam
-- Batteries.Lean.Position
/-- Return the beginning of the line contatining character `pos`.  -/
Lean.findLineStart : String → String.Pos.Raw → String.Pos.Raw
-- Init.Data.String.Basic
String.atEnd : String → String.Pos.Raw → Bool
-- Mathlib.LinearAlgebra.Matrix.SemiringInverse
Matrix.Nonsingular.of_isEmpty : ∀ {n : Type u_1} {R : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommSemiring R] (A : Matrix n n R)
  [IsEmpty n], A.Nonsingular
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Summable.of_neg : ∀ {α : Type u_1} {β : Type u_2} {L : SummationFilter β} [inst : AddCommGroup α] [inst_1 : TopologicalSpace α]
  [IsTopologicalAddGroup α] {f : β → α}, Summable (fun b => -f b) L → Summable f L
-- Mathlib.RingTheory.MvPowerSeries.Restricted
MvPowerSeries.isRestricted.neg : ∀ {R : Type u_1} [inst : NormedRing R] {σ : Type u_2} (c : σ → ℝ) {f : MvPowerSeries σ R},
  MvPowerSeries.IsRestricted c f → MvPowerSeries.IsRestricted c (-f)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
/-- Unfold a row-major matrix entry lookup.  -/
BirdDet.get_eq : ∀ {R : Type u_1} [inst : CommRing R] (n : ℕ) (A : Array R) (i j : ℕ), BirdDet.get n A i j = A.getD (n * i + j) 0
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexAlgEquiv_mul : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [inst : CommSemiring R] [inst_1 : Fintype n]
  [inst_2 : Fintype m] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] [inst_5 : Semiring A] [inst_6 : Algebra R A]
  (e : m ≃ n) (M N : Matrix m m A),
  (Matrix.reindexAlgEquiv R A e) (M * N) = (Matrix.reindexAlgEquiv R A e) M * (Matrix.reindexAlgEquiv R A e) N
-- Mathlib.Combinatorics.SimpleGraph.Density
Rel.interedges_biUnion : ∀ {ι : Type u_2} {κ : Type u_3} {α : Type u_4} {β : Type u_5} (r : α → β → Prop) [inst : (a : α) → DecidablePred (r a)]
  [inst_1 : DecidableEq α] [inst_2 : DecidableEq β] (s : Finset ι) (t : Finset κ) (f : ι → Finset α) (g : κ → Finset β),
  Rel.interedges r (s.biUnion f) (t.biUnion g) = (s ×ˢ t).biUnion fun ab => Rel.interedges r (f ab.1) (g ab.2)
-- Mathlib.Order.WithBot
WithBot.instTop : {α : Type u_1} → [Top α] → Top (WithBot α)
-- Plausible.Random
/-- Generate a random value of type `α`.  -/
Plausible.Random.rand : {m : Type u → Type u_1} → {g : Type} → (α : Type u) → [Plausible.Random m α] → [RandomGen g] → Plausible.RandGT g m α