mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.isSome_get?_iff_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, (Std.DHashMap.Raw.Const.get? m a).isSome = true ↔ a ∈ m
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.toList_reverse.go : ∀ {α : Type u_1} {xs : Array α} (as : Array α) (i j : ℕ) (hj : j < as.size),
  i + j + 1 = xs.size →
    as.size = xs.size →
      (∀ (k : ℕ), as.toList[k]? = if i ≤ k ∧ k ≤ j then xs.toList[k]? else xs.toList.reverse[k]?) →
        ∀ (k : ℕ), (Array.reverse.loop as i ⟨j, hj⟩).toList[k]? = xs.toList.reverse[k]?
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.ofNat_lt_lift_iff : ∀ {a : Cardinal.{u}} {n : ℕ} [inst : n.AtLeastTwo], OfNat.ofNat n < Cardinal.lift.{v, u} a ↔ OfNat.ofNat n < a
-- Mathlib.Order.Disjoint
disjoint_bot_right : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a : α}, Disjoint a ⊥
-- Batteries.Data.AssocList
/-- `O(n)`. Returns true if there is an element in the list whose key is equal to `a`.  -/
Batteries.AssocList.contains : {α : Type u_1} → {β : Type u_2} → [BEq α] → α → Batteries.AssocList α β → Bool
-- Mathlib.Data.QPF.Multivariate.Constructions.Sigma
/-- polynomial functor representation of a dependent sum  -/
MvQPF.Sigma.P : {n : ℕ} → {A : Type u} → (F : A → TypeVec.{u} n → Type u) → [(α : A) → MvQPF (F α)] → MvPFunctor.{u} n
-- Init.System.IO
IO.Process.Output.mk : UInt32 → String → String → IO.Process.Output
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.separatingRight_toMatrix'_iff : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {ι : Type u_6} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  {B : LinearMap.BilinForm R₂ (ι → R₂)}, (LinearMap.BilinForm.toMatrix' B).SeparatingRight ↔ LinearMap.SeparatingRight B
-- Mathlib.Algebra.Module.Submodule.Invariant
/-- Given an endomorphism, `f` of some module, this is the sublattice of all `f`-invariant
submodules.  -/
Module.End.invtSubmodule : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Module.End R M → Sublattice (Submodule R M)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.le_stabilizer_smul_left : ∀ {G : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MulAction G β]
  [inst_3 : SMul α β] [IsScalarTower G α β] (a : α) (b : β), MulAction.stabilizer G a ≤ MulAction.stabilizer G (a • b)
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Implementation of `Mon.equivLaxMonoidalFunctorPUnit`.  -/
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.counitIso : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C).comp
          (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C) ≅
        CategoryTheory.Functor.id (CategoryTheory.Mon C)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_tensor_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {W X Y Z : Cᵒᵖ}
  (f : W ⟶ X) (g : Y ⟶ Z),
  CategoryTheory.MonoidalCategoryStruct.tensorHom f.unop g.unop =
    (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).unop
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.posDef_inv_iff : ∀ {n : Type u_2} [inst : Fintype n] {K : Type u_5} [inst_1 : Field K] [inst_2 : PartialOrder K] [inst_3 : StarRing K]
  [inst_4 : DecidableEq n] {M : Matrix n n K}, M⁻¹.PosDef ↔ M.PosDef
-- Mathlib.Combinatorics.Quiver.Subquiver
/-- A wide subquiver `H` of `G` picks out a set `H a b` of arrows from `a` to `b`
for every pair of vertices `a b`.
 -/
WideSubquiver : (V : Type u_1) → [Quiver V] → Type (max u_1 v)
-- Mathlib.LinearAlgebra.BilinearMap
/-- A version of `Function.Bijective.comp` for composition of a bilinear map with a linear map.  -/
LinearMap.bijective_compr₂_of_equiv : ∀ {R : Type u_2} [inst : CommSemiring R] {M : Type u_5} {Nₗ : Type u_8} {Pₗ : Type u_9} {Qₗ : Type u_10}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid Nₗ] [inst_3 : AddCommMonoid Pₗ] [inst_4 : AddCommMonoid Qₗ]
  [inst_5 : Module R M] [inst_6 : Module R Nₗ] [inst_7 : Module R Pₗ] [inst_8 : Module R Qₗ] (f : M →ₗ[R] Nₗ →ₗ[R] Pₗ)
  (g : Pₗ ≃ₗ[R] Qₗ), Function.Bijective ⇑f → Function.Bijective ⇑(f.compr₂ ↑g)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
/-- `Prod.map` of two continuous affine maps.  -/
ContinuousAffineMap.prodMap : {k : Type u_10} →
  {P₁ : Type u_11} →
    {P₂ : Type u_12} →
      {P₃ : Type u_13} →
        {P₄ : Type u_14} →
          {V₁ : Type u_15} →
            {V₂ : Type u_16} →
              {V₃ : Type u_17} →
                {V₄ : Type u_18} →
                  [inst : Ring k] →
                    [inst_1 : AddCommGroup V₁] →
                      [inst_2 : Module k V₁] →
                        [inst_3 : AddTorsor V₁ P₁] →
                          [inst_4 : TopologicalSpace P₁] →
                            [inst_5 : AddCommGroup V₂] →
                              [inst_6 : Module k V₂] →
                                [inst_7 : AddTorsor V₂ P₂] →
                                  [inst_8 : TopologicalSpace P₂] →
                                    [inst_9 : AddCommGroup V₃] →
                                      [inst_10 : Module k V₃] →
                                        [inst_11 : AddTorsor V₃ P₃] →
                                          [inst_12 : TopologicalSpace P₃] →
                                            [inst_13 : AddCommGroup V₄] →
                                              [inst_14 : Module k V₄] →
                                                [inst_15 : AddTorsor V₄ P₄] →
                                                  [inst_16 : TopologicalSpace P₄] →
                                                    (P₁ →ᴬ[k] P₂) → (P₃ →ᴬ[k] P₄) → P₁ × P₃ →ᴬ[k] P₂ × P₄
-- Mathlib.Algebra.Group.Subsemigroup.Operations
MulHom.mem_srange : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {f : M →ₙ* N} {y : N}, y ∈ f.srange ↔ ∃ x, f x = y
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_X' : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (n : σ), (MvPolynomial.X n).degrees ≤ {n}
-- Lean.Elab.PreDefinition.TerminationMeasure
/-- Elaborates a `TerminationBy` to an `TerminationMeasure`.

* `type` is the full type of the original recursive function, including fixed prefix.
* `hint : TerminationBy` is the syntactic `TerminationBy`.
 -/
Lean.Elab.TerminationMeasure.elab : Lean.Name → Lean.Expr → ℕ → ℕ → Lean.Elab.TerminationBy → Lean.Elab.TermElabM Lean.Elab.TerminationMeasure
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Poly.combine'.match_1.eq_2 : ∀ (motive : Int.Internal.Linear.Poly → Int.Internal.Linear.Poly → Sort u_1) (k₁ a : ℤ) (x : Int.Internal.Linear.Var)
  (p : Int.Internal.Linear.Poly)
  (h_1 : (k₁ k₂ : ℤ) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.num k₂))
  (h_2 :
    (k₁ a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) → motive (Int.Internal.Linear.Poly.num k₁) (Int.Internal.Linear.Poly.add a x p))
  (h_3 :
    (a : ℤ) →
      (x : Int.Internal.Linear.Var) →
        (p : Int.Internal.Linear.Poly) →
          (k₂ : ℤ) → motive (Int.Internal.Linear.Poly.add a x p) (Int.Internal.Linear.Poly.num k₂))
  (h_4 :
    (a₁ : ℤ) →
      (x₁ : Int.Internal.Linear.Var) →
        (p₁ : Int.Internal.Linear.Poly) →
          (a₂ : ℤ) →
            (x₂ : Int.Internal.Linear.Var) →
              (p₂ : Int.Internal.Linear.Poly) →
                motive (Int.Internal.Linear.Poly.add a₁ x₁ p₁) (Int.Internal.Linear.Poly.add a₂ x₂ p₂)),
  (match Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.add a x p with
    | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.num k₂ => h_1 k₁ k₂
    | Int.Internal.Linear.Poly.num k₁, Int.Internal.Linear.Poly.add a x p => h_2 k₁ a x p
    | Int.Internal.Linear.Poly.add a x p, Int.Internal.Linear.Poly.num k₂ => h_3 a x p k₂
    | Int.Internal.Linear.Poly.add a₁ x₁ p₁, Int.Internal.Linear.Poly.add a₂ x₂ p₂ => h_4 a₁ x₁ p₁ a₂ x₂ p₂) =
    h_2 k₁ a x p
-- Mathlib.LinearAlgebra.Basis.VectorSpace
Module.Basis.coe_ofVectorSpace : ∀ (K : Type u_3) (V : Type u_4) [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V],
  ⇑(Module.Basis.ofVectorSpace K V) = Subtype.val
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered monoids M, N, the natural projection ordered homomorphism from M × N to N.  -/
OrderMonoidHom.snd : (α : Type u_1) →
  (β : Type u_2) →
    [inst : Monoid α] → [inst_1 : PartialOrder α] → [inst_2 : Monoid β] → [inst_3 : Preorder β] → α × β →*o β
-- Lean.Meta.Tactic.Intro
Lean.Meta.intro1Core : Lean.MVarId → Bool → Lean.MetaM (Lean.FVarId × Lean.MVarId)
-- Mathlib.Data.Finset.Image
Finset.mem_range_iff_mem_finset_range_of_mod_eq' : ∀ {α : Type u_1} [inst : DecidableEq α] {f : ℕ → α} {a : α} {n : ℕ},
  0 < n → (∀ (i : ℕ), f (i % n) = f i) → (a ∈ Set.range f ↔ a ∈ Finset.image (fun i => f i) (Finset.range n))
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk_eq_one_of_coe_ideal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {I : (FractionalIdeal (nonZeroDivisors R) (FractionRing R))ˣ}
  {I' : Ideal R}, ↑I = ↑I' → ((ClassGroup.mk (FractionRing R)) I = 1 ↔ ∃ x, x ≠ 0 ∧ I' = Ideal.span {x})
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- **Integration by parts on (a, ∞).**
For finite intervals, see: `intervalIntegral.integral_mul_deriv_eq_deriv_mul`.  -/
MeasureTheory.integral_Ioi_mul_deriv_eq_deriv_mul : ∀ {A : Type u_1} [inst : NormedRing A] [inst_1 : NormedAlgebra ℝ A] {a : ℝ} {a' b' : A} {u v u' v' : ℝ → A}
  [CompleteSpace A],
  (∀ x ∈ Set.Ioi a, HasDerivAt u (u' x) x) →
    (∀ x ∈ Set.Ioi a, HasDerivAt v (v' x) x) →
      MeasureTheory.IntegrableOn (u * v') (Set.Ioi a) MeasureTheory.volume →
        MeasureTheory.IntegrableOn (u' * v) (Set.Ioi a) MeasureTheory.volume →
          Filter.Tendsto (u * v) (nhdsWithin a (Set.Ioi a)) (nhds a') →
            Filter.Tendsto (u * v) Filter.atTop (nhds b') →
              ∫ (x : ℝ) in Set.Ioi a, u x * v' x = b' - a' - ∫ (x : ℝ) in Set.Ioi a, u' x * v x
-- Mathlib.CategoryTheory.Quotient
/-- `r` is an equivalence on every hom-set.  -/
CategoryTheory.Congruence.equivalence : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {r : HomRel C} [self : CategoryTheory.Congruence r]
  {X Y : C}, Equivalence r
-- Mathlib.LinearAlgebra.TensorProduct.Basis
Module.Basis.baseChange_apply : ∀ {R : Type u_1} {M : Type u_3} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (S : Type u_7) [inst_3 : Semiring S] [inst_4 : Algebra R S] (b : Module.Basis ι R M) (i : ι),
  (Module.Basis.baseChange S b) i = 1 ⊗ₜ[R] b i
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Naturality of the lax naturality constraint.  -/
CategoryTheory.Lax.LaxTrans.naturality_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.LaxTrans F G) {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  CategoryTheory.CategoryStruct.comp (self.naturality f)
      (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (self.app b)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.map₂ η))
      (self.naturality g)
-- Lean.Meta.Sym.AlphaShareBuilder
_private.Lean.Meta.Sym.AlphaShareBuilder.0.Lean.Meta.Sym.Internal.dummy : Lean.Meta.Sym.AlphaKey
-- Mathlib.Algebra.Order.Group.Action.End
RelHom.apply_faithfulSMul : ∀ {α : Type u_1} {r : α → α → Prop}, FaithfulSMul (r →r r) α
-- Mathlib.Algebra.Lie.Semisimple.Defs
LieAlgebra.instHasTrivialRadicalOfSubsingleton : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] [Subsingleton L],
  LieAlgebra.HasTrivialRadical R L
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.unop_X₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square Cᵒᵖ),
  sq.unop.X₁ = Opposite.unop sq.X₄
-- Mathlib.Analysis.Normed.Lp.lpSpace
/-- Two continuous additive maps from `lp E p` agree if they agree on `lp.single`.

See note [partially-applied ext lemmas].  -/
lp.ext_continuousAddMonoidHom : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] [inst_1 : DecidableEq α]
  {F : Type u_5} [inst_2 : AddCommMonoid F] [inst_3 : TopologicalSpace F] [T2Space F] [inst_5 : Fact (1 ≤ p)],
  p ≠ ⊤ →
    ∀ ⦃f g : ↥(lp E p) →ₜ+ F⦄,
      (∀ (i : α), f.comp (lp.singleContinuousAddMonoidHom E p i) = g.comp (lp.singleContinuousAddMonoidHom E p i)) →
        f = g
-- Mathlib.Algebra.Category.ModuleCat.ExteriorPower
ModuleCat.exteriorPower.functor_map : ∀ (R : Type u) [inst : CommRing R] (n : ℕ) {X Y : ModuleCat R} (f : X ⟶ Y),
  (ModuleCat.exteriorPower.functor R n).map f = ModuleCat.exteriorPower.map f n
-- Mathlib.Probability.Process.HittingTime
/-- A discrete hitting time is a stopping time.  -/
MeasureTheory.Adapted.isStoppingTime_hittingBtwn : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : ConditionallyCompleteLinearOrder ι]
  [WellFoundedLT ι] [Countable ι] {x : MeasurableSpace β} {f : MeasureTheory.Filtration ι m} {u : ι → Ω → β} {s : Set β}
  {n n' : ι},
  MeasureTheory.Adapted f u →
    MeasurableSet s → MeasureTheory.IsStoppingTime f fun ω => ↑(MeasureTheory.hittingBtwn u s n n' ω)
-- Mathlib.RingTheory.Derivation.Basic
Derivation.leibniz_zpow : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {K : Type u_4}
  [inst_3 : Field K] [inst_4 : Module K M] [inst_5 : Algebra R K] (D : Derivation R K M) (a : K) (n : ℤ),
  D (a ^ n) = n • a ^ (n - 1) • D a
-- Lean.Elab.InfoTree.Types
Lean.Elab.TermInfo : Type
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.comp_hom_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} {X Y Z : CategoryTheory.SpectralSequence C c r₀} (f : X.Hom Y) (g : Y.Hom Z) (r : ℤ)
  (hr : r₀ ≤ r) {Z_1 : HomologicalComplex C (c r)} (h : Z.page r ⋯ ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp f g).hom r hr) h =
    CategoryTheory.CategoryStruct.comp (f.hom r ⋯) (CategoryTheory.CategoryStruct.comp (g.hom r ⋯) h)
-- Mathlib.Order.Hom.Basic
OrderHom.prod_mono : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {f₁ f₂ : α →o β}, f₁ ≤ f₂ → ∀ {g₁ g₂ : α →o γ}, g₁ ≤ g₂ → f₁.prod g₁ ≤ f₂.prod g₂
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
/-- If `D` is already an enriched ordinary category, there is a canonical functor from
`ForgetEnrichment V D` to `D`.  -/
CategoryTheory.ForgetEnrichment.equivFunctor : (V : Type u') →
  [inst : CategoryTheory.Category.{v', u'} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      (D : Type u'') →
        [inst_2 : CategoryTheory.Category.{v'', u''} D] →
          [inst_3 : CategoryTheory.EnrichedOrdinaryCategory V D] →
            CategoryTheory.Functor (CategoryTheory.ForgetEnrichment V D) D
-- Init.Data.String.Defs
String.lengthAssumingAscii_eq : ∀ {s : String}, s.lengthAssumingAscii = s.utf8ByteSize
-- Mathlib.Data.ZMod.Basic
ZMod.val_zero : ∀ {n : ℕ}, ZMod.val 0 = 0
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.liftIsometry_symm_apply : ∀ {ι : Type u_1} [inst : Fintype ι] {𝕜 : Type u_2} {E : ι → Type u_3} [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] {F : Type u_4}
  [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F] (l : (PiTensorProduct 𝕜 fun i => E i) →L[𝕜] F),
  (PiTensorProduct.liftIsometry 𝕜 E F).symm l = l.compContinuousMultilinearMap (PiTensorProduct.tprodL 𝕜)
-- Mathlib.RingTheory.Polynomial.Chebyshev
/-- Another induction principle used for proving facts about Chebyshev polynomials,
which is sometimes easier to use  -/
Polynomial.Chebyshev.induct' : ∀ (motive : ℤ → Prop),
  motive 0 →
    motive 1 →
      (∀ (n : ℕ), motive (↑n + 1) → motive ↑n → motive (↑n + 2)) →
        (∀ (n : ℤ), motive n → motive (-n)) → ∀ (a : ℤ), motive a
-- Lean.Syntax
Lean.SyntaxNode.withArgs : {β : Sort u_1} → Lean.SyntaxNode → (Array Lean.Syntax → β) → β
-- Mathlib.Algebra.Module.Defs
Semiring.toModule : {R : Type u_1} → [inst : Semiring R] → Module R R
-- Mathlib.LinearAlgebra.DFinsupp
DFinsupp.mrange_mapRangeAddMonoidHom : ∀ {ι : Type u_1} {β₁ : ι → Type u_8} {β₂ : ι → Type u_9} [inst : (i : ι) → AddCommMonoid (β₁ i)]
  [inst_1 : (i : ι) → AddCommMonoid (β₂ i)] (f : (i : ι) → β₁ i →+ β₂ i),
  AddMonoidHom.mrange (DFinsupp.mapRange.addMonoidHom f) =
    AddSubmonoid.comap DFinsupp.coeFnAddMonoidHom (AddSubmonoid.pi Set.univ fun i => AddMonoidHom.mrange (f i))
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
/-- Equivalence between `k + 1` vectors of length `n` and `k` vectors of length `n` along with a
vector in the complement of their span.
 -/
equiv_linearIndependent : {K : Type u_3} →
  {V : Type u} →
    [inst : DivisionRing K] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : Module K V] →
          (n : ℕ) →
            { s // LinearIndependent K s } ≃
              (s : { s // LinearIndependent K s }) × ↑(↑(Submodule.span K (Set.range ↑s)))ᶜ
-- Mathlib.LinearAlgebra.Span.Basic
Submodule.apply_mem_span_image_of_mem_span : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_4} {M₂ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : Semiring R₂] {σ₁₂ : R →+* R₂} [inst_4 : AddCommMonoid M₂] [inst_5 : Module R₂ M₂]
  [RingHomSurjective σ₁₂] (f : M →ₛₗ[σ₁₂] M₂) {x : M} {s : Set M},
  x ∈ Submodule.span R s → f x ∈ Submodule.span R₂ (⇑f '' s)
-- Batteries.Data.AssocList
_private.Batteries.Data.AssocList.0.Batteries.AssocList.beq.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : Batteries.AssocList α β → Batteries.AssocList α β → Sort u_3) (key : α)
  (value : β) (tail : Batteries.AssocList α β) (h_1 : Unit → motive Batteries.AssocList.nil Batteries.AssocList.nil)
  (h_2 :
    (key : α) →
      (value : β) →
        (tail : Batteries.AssocList α β) → motive (Batteries.AssocList.cons key value tail) Batteries.AssocList.nil)
  (h_3 :
    (key : α) →
      (value : β) →
        (tail : Batteries.AssocList α β) → motive Batteries.AssocList.nil (Batteries.AssocList.cons key value tail))
  (h_4 :
    (a : α) →
      (b : β) →
        (t : Batteries.AssocList α β) →
          (a' : α) →
            (b' : β) →
              (t' : Batteries.AssocList α β) →
                motive (Batteries.AssocList.cons a b t) (Batteries.AssocList.cons a' b' t')),
  (match Batteries.AssocList.cons key value tail, Batteries.AssocList.nil with
    | Batteries.AssocList.nil, Batteries.AssocList.nil => h_1 ()
    | Batteries.AssocList.cons key value tail, Batteries.AssocList.nil => h_2 key value tail
    | Batteries.AssocList.nil, Batteries.AssocList.cons key value tail => h_3 key value tail
    | Batteries.AssocList.cons a b t, Batteries.AssocList.cons a' b' t' => h_4 a b t a' b' t') =
    h_2 key value tail
-- Lean.Meta.Tactic.Simp.Main
Lean.Meta.Simp.simpProj : Lean.Expr → Lean.Meta.SimpM Lean.Meta.Simp.Result
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (∀ (k' : α), t.max? = some k' → (cmp k' k).isLE = true) ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Init.Data.Array.Perm
Array.Perm.of_eq : ∀ {α : Type u_1} {xs ys : Array α}, xs = ys → xs.Perm ys
-- Init.Data.UInt.Lemmas
USize.ofBitVec_uInt16ToBitVec : ∀ (n : UInt16), { toBitVec := BitVec.setWidth System.Platform.numBits n.toBitVec } = n.toUSize
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.LeCnstr.isUnsat : Lean.Meta.Grind.Arith.Cutsat.LeCnstr → Bool
-- Init.Data.List.Count
List.countP_mono_left : ∀ {α : Type u_1} {p q : α → Bool} {l : List α}, (∀ x ∈ l, p x = true → q x = true) → List.countP p l ≤ List.countP q l
-- Mathlib.Topology.DiscreteSubset
cofinite_le_codiscrete : ∀ {X : Type u_1} [inst : TopologicalSpace X] [CompactSpace X], Filter.cofinite ≤ Filter.codiscrete X
-- Lean.Data.Lsp.Basic
Lean.Lsp.Location.mk.sizeOf_spec : ∀ (uri : Lean.Lsp.DocumentUri) (range : Lean.Lsp.Range),
  sizeOf { uri := uri, range := range } = 1 + sizeOf uri + sizeOf range
-- Mathlib.Topology.Constructions
ContinuousMap.uliftEquiv_symm_apply_apply : ∀ (X : Type u) (Y : Type v) [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : C(X, Y))
  (a : ULift.{v, u} X), ((ContinuousMap.uliftEquiv X Y).symm f) a = (ULift.up ∘ ⇑f ∘ ULift.down) a
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
Real.differentiable_exp : Differentiable ℝ Real.exp
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
Finset.pluennecke_petridis_inequality_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] {A B : Finset G} (C : Finset G),
  (∀ A' ⊆ A, (A * B).card * A'.card ≤ (A' * B).card * A.card) → (C * A * B).card * A.card ≤ (A * B).card * (C * A).card
-- Mathlib.NumberTheory.Modular
/-- Classify possible `g, z` assuming `c = 1, d = 0`.  -/
_private.Mathlib.NumberTheory.Modular.0.ModularGroup.cases_c_one_d_zero : ∀ {g : Matrix.SpecialLinearGroup (Fin 2) ℤ} {z : UpperHalfPlane},
  z ∈ ModularGroup.fd →
    g • z ∈ ModularGroup.fd →
      ‖UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) g))
              ↑z‖ ≤
          1 →
        ↑g 1 0 = 1 →
          ↑g 1 1 = 0 →
            g = ModularGroup.S ∧ ‖↑z‖ = 1 ∨
              g = ModularGroup.T⁻¹ * ModularGroup.S ∧ z = UpperHalfPlane.ρ ∨
                g = ModularGroup.T * ModularGroup.S ∧ z = 1 +ᵥ UpperHalfPlane.ρ
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
abs_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {a b : α}, |dist a b| = dist a b
-- Mathlib.Algebra.Category.MonCat.Yoneda
AddCommMonCat.coyoneda_map_app : ∀ {X Y : AddCommMonCatᵒᵖ} (f : X ⟶ Y) (N : AddCommMonCat),
  (AddCommMonCat.coyoneda.map f).app N = AddCommMonCat.ofHom (AddCommMonCat.Hom.hom f.unop).compHom'
-- Mathlib.Algebra.Lie.Basic
LieModuleHom.ext_iff : ∀ {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] {f g : M →ₗ⁅R,L⁆ N}, f = g ↔ ∀ (m : M), f m = g m
-- Mathlib.GroupTheory.Congruence.Defs
AddCon.liftOn.eq_1 : ∀ {M : Type u_1} [inst : Add M] {β : Sort u_4} {c : AddCon M} (q : c.Quotient) (f : M → β)
  (h : ∀ (a b : M), c a b → f a = f b), AddCon.liftOn q f h = Quotient.liftOn' q f h
-- Mathlib.Analysis.Asymptotics.LinearGrowth
Monotone.linearGrowthInf_nonneg : ∀ {u : ℕ → EReal}, Monotone u → u ≠ ⊥ → 0 ≤ LinearGrowth.linearGrowthInf u
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.zero_opow_le : ∀ (a : Ordinal.{u_1}), 0 ^ a ≤ 1
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_toInt32 : ∀ (x : Int8), x.toInt32.toNatClampNeg = x.toNatClampNeg
-- Lean.Elab.Tactic.Basic
/-- Execute `x` with error recovery disabled  -/
Lean.Elab.Tactic.withRecover : {α : Type} → Bool → Lean.Elab.Tactic.TacticM α → Lean.Elab.Tactic.TacticM α
-- Mathlib.NumberTheory.JacobiSum.Basic
jacobiSum_comm : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : Fintype R] [inst_2 : CommRing R'] (χ ψ : MulChar R R'),
  jacobiSum χ ψ = jacobiSum ψ χ
-- Mathlib.RingTheory.Polynomial.HilbertPoly
/-- If `h : F[X]` and there exists some `N : ℕ` such that for any number `n : ℕ` bigger than `N`
we have `PowerSeries.coeff F n (p * invOneSubPow F d) = h.eval (n : F)`, then `h` is exactly
`Polynomial.hilbertPoly p d`.
 -/
Polynomial.eq_hilbertPoly_of_forall_coeff_eq_eval : ∀ {F : Type u_1} [inst : Field F] [CharZero F] {p h : Polynomial F} {d : ℕ} (N : ℕ),
  (∀ n > N, (PowerSeries.coeff n) (↑p * ↑(PowerSeries.invOneSubPow F d)) = Polynomial.eval (↑n) h) → h = p.hilbertPoly d