mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.lt_def : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] {v : Valuation R Γ₀}
  {a b : WithVal v}, a < b ↔ v a.ofVal < v b.ofVal
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getEntryLE.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] (k k_1 : α) (e_k : k = k_1)
  (t t_1 : Std.DTreeMap.Internal.Impl α β) (e_t : t = t_1) (ho : t.Ordered) (he : ∃ a ∈ t, (compare a k).isLE = true),
  Std.DTreeMap.Internal.Impl.getEntryLE k t ho he = Std.DTreeMap.Internal.Impl.getEntryLE k_1 t_1 ⋯ ⋯
-- Init.Data.UInt.BasicAux
instSubUSize : Sub USize
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
AlgHom.val_comp_rangeRestrict : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] (φ : A →ₐ[R] B), φ.range.val.comp φ.rangeRestrict = φ
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.equiv_hom_hom_apply_fst : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (c : CategoryTheory.Limits.Cone F),
  ((CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Cone.equiv F).hom) c).fst = Opposite.op c.pt
-- Mathlib.Algebra.Order.Hom.Basic
MulRingNormClass.toMulRingSeminormClass : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : NonAssocRing α} {inst_1 : Semiring β}
  {inst_2 : PartialOrder β} {inst_3 : FunLike F α β} [self : MulRingNormClass F α β], MulRingSeminormClass F α β
-- Mathlib.MeasureTheory.MeasurableSpace.Card
/-- If a sigma-algebra is generated by a set of sets `s` with cardinality at most the continuum,
then the sigma algebra has the same cardinality bound.  -/
MeasurableSpace.cardinal_generateMeasurable_le_continuum : ∀ {α : Type u} {s : Set (Set α)},
  Cardinal.mk ↑s ≤ Cardinal.continuum → Cardinal.mk ↑{t | MeasurableSpace.GenerateMeasurable s t} ≤ Cardinal.continuum
-- Mathlib.GroupTheory.Index
Subgroup.relIndex_mul_index : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G}, H ≤ K → H.relIndex K * K.index = H.index
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
/-- In a sigma-finite measure space, there exists an integrable function which is
positive everywhere (and with an arbitrarily small integral).  -/
MeasureTheory.exists_pos_lintegral_lt_of_sigmaFinite : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) [MeasureTheory.SigmaFinite μ] {ε : ENNReal},
  ε ≠ 0 → ∃ g, (∀ (x : α), 0 < g x) ∧ Measurable g ∧ ∫⁻ (x : α), ↑(g x) ∂μ < ε
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CallHierarchyOutgoingCallsParams : Type
-- Mathlib.Algebra.Module.Submodule.Invariant
Module.End.invtSubmodule.codisjoint_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}, Codisjoint p q ↔ Codisjoint ↑p ↑q
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_ofDual : ∀ {α : Type u_1} [inst : Lattice α] (a b : αᵒᵈ),
  Set.uIcc (OrderDual.ofDual a) (OrderDual.ofDual b) = ⇑OrderDual.toDual ⁻¹' Set.uIcc a b
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_eq : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (X : σ → R) (f : MvPolynomial σ R),
  (MvPolynomial.eval X) f = ∑ d ∈ f.support, MvPolynomial.coeff d f * ∏ i ∈ d.support, X i ^ d i
-- Mathlib.Algebra.Ring.GeomSum
geom_sum_Ico_mul : ∀ {R : Type u_1} [inst : Ring R] (x : R) {m n : ℕ}, m ≤ n → (∑ i ∈ Finset.Ico m n, x ^ i) * (x - 1) = x ^ n - x ^ m
-- Mathlib.Topology.Compactness.Compact
/-- The preimage of a compact set under an inducing map is a compact set.  -/
Topology.IsInducing.isCompact_preimage : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsInducing f → IsClosed (Set.range f) → ∀ {K : Set Y}, IsCompact K → IsCompact (f ⁻¹' K)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_le_size_erase : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α}, m.size ≤ (m.erase k).size + 1
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
_private.Mathlib.RingTheory.AdicCompletion.AsTensorProduct.0.AdicCompletion.tens_surj : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type}
  (f : (ι → R) →ₗ[R] M), Function.Surjective ⇑f → Function.Surjective ⇑(AdicCompletion.lTensorf✝ I M f)
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonWaitForDiagnosticsParams.toJson : Lean.Lsp.WaitForDiagnosticsParams → Lean.Json
-- Mathlib.Data.Nat.ModEq
Nat.mod_sub_of_le : ∀ {a b n : ℕ}, b ≤ a % n → a % n - b = (a - b) % n
-- Mathlib.Data.Fin.SuccPred
Fin.one_succAbove_succ : ∀ {n : ℕ} (j : Fin n), Fin.succAbove 1 j.succ = j.succ.succ
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.prod_mono_right : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (s : Subring R),
  Monotone fun t => s.prod t
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.zpow'_ofNat : ∀ {α : Type u_1} [inst : GroupWithZero α] (a : α) {n : ℕ}, n ≠ 0 → Mathlib.Tactic.FieldSimp.zpow' a ↑n = a ^ n
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than the given key,
panicking if no such pair exists.
 -/
Std.DTreeMap.getEntryGT! : {α : Type u} →
  {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited (Sigma β)] → Std.DTreeMap α β cmp → α → (a : α) × β a
-- Mathlib.Algebra.Category.MonCat.ForgetCorepresentable
/-- The forgetful functor `AddMonCat.{u} ⥤ Type u` is corepresentable.  -/
AddMonCat.coyonedaObjIsoForget : CategoryTheory.coyoneda.obj (Opposite.op (AddMonCat.of (ULift.{u, 0} ℕ))) ≅ CategoryTheory.forget AddMonCat
-- Init.Data.Nat.Lemmas
/-- Dependent variant of `forall_lt_succ_left`.  -/
Nat.forall_lt_succ_left' : ∀ {n : ℕ} {p : (m : ℕ) → m < n + 1 → Prop},
  (∀ (m : ℕ) (h : m < n + 1), p m h) ↔ p 0 ⋯ ∧ ∀ (m : ℕ) (h : m < n), p (m + 1) ⋯
-- Mathlib.RingTheory.WittVector.Basic
_private.Mathlib.RingTheory.WittVector.Basic.0.WittVector.ghostFun_pow : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (x : WittVector p R) (m : ℕ),
  WittVector.ghostFun✝ (x ^ m) = WittVector.ghostFun✝ x ^ m
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange_add' : ∀ {ι : Type u_1} {F : Type u_2} {M : Type u_3} {N : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : FunLike F M N] [inst_3 : AddMonoidHomClass F M N] {f : F} (g₁ g₂ : ι →₀ M),
  Finsupp.mapRange ⇑f ⋯ (g₁ + g₂) = Finsupp.mapRange ⇑f ⋯ g₁ + Finsupp.mapRange ⇑f ⋯ g₂
-- Mathlib.Topology.Algebra.Monoid
addHomOfTendsto.eq_1 : ∀ {α : Type u_2} {M₁ : Type u_6} {M₂ : Type u_7} [inst : TopologicalSpace M₂] [inst_1 : T2Space M₂] [inst_2 : Add M₁]
  [inst_3 : Add M₂] [inst_4 : ContinuousAdd M₂] {F : Type u_8} [inst_5 : FunLike F M₁ M₂] [inst_6 : AddHomClass F M₁ M₂]
  {l : Filter α} (f : M₁ → M₂) (g : α → F) [inst_7 : l.NeBot] (h : Filter.Tendsto (fun a x => (g a) x) l (nhds f)),
  addHomOfTendsto f g h = addHomOfMemClosureRangeCoe f ⋯
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagationsData.diseqs.sizeOf_spec : ∀ (solverId : ℕ) (ps : Lean.Meta.Grind.ParentSet) (rest : Lean.Meta.Grind.PendingSolverPropagationsData✝),
  sizeOf (Lean.Meta.Grind.PendingSolverPropagationsData.diseqs✝ solverId ps rest) =
    1 + sizeOf solverId + sizeOf ps + sizeOf rest
-- Mathlib.Algebra.Ring.Subring.Basic
/-- Product of a multiset of elements in a subring of a `CommRing` is in the subring.  -/
Subring.multiset_prod_mem : ∀ {R : Type u_1} [inst : CommRing R] (s : Subring R) (m : Multiset R), (∀ a ∈ m, a ∈ s) → m.prod ∈ s
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.Hom.mk.inj : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C} {D : Type u₂}
  {inst_2 : CategoryTheory.Category.{v₂, u₂} D} {inst_3 : CategoryTheory.MonoidalCategory D}
  {F G : CategoryTheory.LaxMonoidalFunctor C D} {hom : F.toFunctor ⟶ G.toFunctor}
  {isMonoidal :
    autoParam (CategoryTheory.NatTrans.IsMonoidal hom) CategoryTheory.LaxMonoidalFunctor.Hom.isMonoidal._autoParam}
  {hom_1 : F.toFunctor ⟶ G.toFunctor}
  {isMonoidal_1 :
    autoParam (CategoryTheory.NatTrans.IsMonoidal hom_1) CategoryTheory.LaxMonoidalFunctor.Hom.isMonoidal._autoParam},
  { hom := hom, isMonoidal := isMonoidal } = { hom := hom_1, isMonoidal := isMonoidal_1 } → hom = hom_1
-- Mathlib.Analysis.SpecialFunctions.Log.RpowTendsto
Real.norm_inv_mul_rpow_sub_one_sub_log_le : ∀ {p x : ℝ}, 0 < p → 0 < x → ‖p * Real.log x‖ ≤ 1 → ‖p⁻¹ * (x ^ p - 1) - Real.log x‖ ≤ p * ‖Real.log x‖ ^ 2
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.topEquiv_apply : ∀ {G : Type u_1} [inst : AddGroup G] (x : ↥⊤), AddSubgroup.topEquiv x = ↑x
-- Mathlib.Algebra.Order.BigOperators.Ring.Multiset
Multiset.mem_le_prod_of_one_le : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoidWithZero β] [inst_1 : PartialOrder β] [PosMulMono β]
  [ZeroLEOneClass β] {f : α → β},
  (∀ (a : α), 1 ≤ f a) → ∀ {s : Multiset α} {a : α}, a ∈ s → f a ≤ (Multiset.map f s).prod
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.excenterExists_reindex : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {m n : ℕ} [inst_4 : NeZero m] [inst_5 : NeZero n] (s : Affine.Simplex ℝ P n)
  {e : Fin (n + 1) ≃ Fin (m + 1)} {signs : Finset (Fin (m + 1))},
  (s.reindex e).ExcenterExists signs ↔ s.ExcenterExists (Finset.map e.symm.toEmbedding signs)
-- Mathlib.Topology.Constructions
Topology.IsOpenEmbedding.sigmaMk : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] {i : ι},
  Topology.IsOpenEmbedding (Sigma.mk i)
-- Mathlib.MeasureTheory.SetAlgebra
/-- An algebra of sets is closed by intersection.  -/
MeasureTheory.IsSetAlgebra.inter_mem : ∀ {α : Type u_1} {𝒜 : Set (Set α)} {s t : Set α}, MeasureTheory.IsSetAlgebra 𝒜 → s ∈ 𝒜 → t ∈ 𝒜 → s ∩ t ∈ 𝒜
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_diff_of_contains_eq_false_left : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF),
  m₂.WF →
    ∀ {k : α} {fallback : β k},
      Std.DTreeMap.Internal.Impl.contains k m₁ = false → (m₁.diff m₂ ⋯).getD k fallback = fallback
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_of_mem_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∈ t₁ ∪ t₂ → k ∉ t₁ → k ∈ t₂
-- Mathlib.Algebra.Order.Floor.Defs
Int.le_ceil_iff : ∀ {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {z : ℤ} {a : α}, z ≤ ⌈a⌉ ↔ ↑z - 1 < a
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.ofLeftInverse_apply : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] {f : G →* N} {g : N →* G}
  (h : Function.LeftInverse ⇑g ⇑f) (x : G), ↑((MonoidHom.ofLeftInverse h) x) = f x
-- Mathlib.Algebra.Module.LinearMap.Star
/-- `M →ₗ⋆[R] N` is the type of `R`-conjugate-linear maps from `M` to `N`.  -/
«term_→ₗ⋆[_]_» : Lean.TrailingParserDescr
-- Batteries.Data.List.Count
cast.hcongr_4 : ∀ (α α' : Sort u),
  α = α' →
    ∀ (β β' : Sort u),
      β = β' → ∀ (h : α = β) (h' : α' = β'), h ≍ h' → ∀ (a : α) (a' : α'), a ≍ a' → cast h a ≍ cast h' a'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
/-- the functor on the base component  -/
CategoryTheory.Limits.CatCospanTransform.base : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {F : CategoryTheory.Functor A B} →
              {G : CategoryTheory.Functor C B} →
                {A' : Type u₄} →
                  {B' : Type u₅} →
                    {C' : Type u₆} →
                      [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] →
                        [inst_4 : CategoryTheory.Category.{v₅, u₅} B'] →
                          [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] →
                            {F' : CategoryTheory.Functor A' B'} →
                              {G' : CategoryTheory.Functor C' B'} →
                                CategoryTheory.Limits.CatCospanTransform F G F' G' → CategoryTheory.Functor B B'
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.RealImaginaryPart
quasispectrum_realPart : ∀ {A : Type u_1} [inst : TopologicalSpace A] [inst_1 : NonUnitalRing A] [inst_2 : StarRing A] [inst_3 : Module ℂ A]
  [inst_4 : IsScalarTower ℂ A A] [inst_5 : SMulCommClass ℂ A A] [inst_6 : StarModule ℂ A]
  [NonUnitalContinuousFunctionalCalculus ℂ A IsStarNormal] (a : A),
  autoParam (IsStarNormal a) quasispectrum_realPart._auto_1 →
    quasispectrum ℂ ↑(realPart a) = (fun x => ↑x.re) '' quasispectrum ℂ a
-- Mathlib.CategoryTheory.Monoidal.End
CategoryTheory.MonoidalCategory.tensoringRight_δ : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y Z : C),
  (CategoryTheory.Functor.OplaxMonoidal.δ (CategoryTheory.MonoidalCategory.tensoringRight C) X Y).app Z =
    (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).inv
-- Aesop.Stats.Basic
Aesop.instInhabitedForwardStateStats.default : Aesop.ForwardStateStats
-- Init.Data.SInt.Lemmas
Int16.ofInt_int64ToInt : ∀ (x : Int64), Int16.ofInt x.toInt = x.toInt16
-- Mathlib.AlgebraicTopology.SimplicialObject.DeltaZeroIter
CategoryTheory.SimplicialObject.σ₀Iter_δ₀Iter : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : CategoryTheory.SimplicialObject C) (i : ℕ) {n m : ℕ}
  (hi : autoParam (n + i = m) CategoryTheory.SimplicialObject.σ₀Iter_δ₀Iter._auto_1),
  CategoryTheory.CategoryStruct.comp (X.σ₀Iter i hi) (X.δ₀Iter i hi) =
    CategoryTheory.CategoryStruct.id (X.obj (Opposite.op { len := n }))
-- Std.Http.Server.Connection
_private.Std.Http.Server.Connection.0.Std.Http.Server.Connection.Recv.shutdown.sizeOf_spec : ∀ {β : Type} [inst : SizeOf β], sizeOf Std.Http.Server.Connection.Recv.shutdown✝ = 1
-- Mathlib.Topology.Filter
Filter.sInter_nhds : ∀ {α : Type u_2} (l : Filter α), ⋂₀ {s | s ∈ nhds l} = Set.Iic l
-- Mathlib.Algebra.Star.StarRingHom
NonUnitalStarRingHomClass.instCoeHeadNonUnitalStarRingHom : {F : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : NonUnitalNonAssocSemiring A] →
        [inst_1 : Star A] →
          [inst_2 : NonUnitalNonAssocSemiring B] →
            [inst_3 : Star B] →
              [inst_4 : FunLike F A B] →
                [inst_5 : NonUnitalRingHomClass F A B] → [NonUnitalStarRingHomClass F A B] → CoeHead F (A →⋆ₙ+* B)
-- Mathlib.Combinatorics.Pigeonhole
/-- The pigeonhole principle for finitely many pigeons of different weights, non-strict inequality
version: there is a pigeonhole with the total weight of pigeons in it less than or equal to `b`
provided that the total number of pigeonholes times `b` is greater than or equal to the total weight
of all pigeons.  -/
Fintype.exists_sum_fiber_le_of_sum_le_nsmul : ∀ {α : Type u} {β : Type v} {M : Type w} [inst : DecidableEq β] [inst_1 : Fintype α] [inst_2 : Fintype β] (f : α → β)
  {w : α → M} {b : M} [inst_3 : AddCommMonoid M] [inst_4 : LinearOrder M] [IsOrderedCancelAddMonoid M] [Nonempty β],
  ∑ x, w x ≤ Fintype.card β • b → ∃ y, ∑ x with f x = y, w x ≤ b
-- Mathlib.Combinatorics.Enumerative.Composition
/-- The `i`-th sublist in the splitting of a list `l` along a composition `c`, is the slice of `l`
between the indices `c.sizeUpTo i` and `c.sizeUpTo (i+1)`, i.e., the indices in the `i`-th
block of the composition.  -/
List.getElem_splitWrtComposition' : ∀ {n : ℕ} {α : Type u_1} (l : List α) (c : Composition n) {i : ℕ} (hi : i < (l.splitWrtComposition c).length),
  (l.splitWrtComposition c)[i] = List.drop (c.sizeUpTo i) (List.take (c.sizeUpTo (i + 1)) l)
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.preimage_add_right_closedEBall`. -/
EMetric.preimage_add_right_closedBall : ∀ {G : Type v} [inst : AddGroup G] [inst_1 : PseudoEMetricSpace G] [IsIsometricVAdd Gᵃᵒᵖ G] (a b : G) (r : ENNReal),
  (fun x => x + a) ⁻¹' Metric.closedEBall b r = Metric.closedEBall (b - a) r
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- If the input vectors of `gramSchmidt` are linearly independent,
then the output vectors are non-zero.  -/
InnerProductSpace.gramSchmidt_ne_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_3} [inst_3 : LinearOrder ι] [inst_4 : LocallyFiniteOrderBot ι] [inst_5 : WellFoundedLT ι] {f : ι → E}
  (n : ι), LinearIndependent 𝕜 f → InnerProductSpace.gramSchmidt 𝕜 f n ≠ 0
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
/-- This lemma is a special case of `Integrable.of_finite`.  -/
MeasureTheory.Integrable.of_isEmpty : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : NormedAddCommGroup β]
  [IsEmpty α] {f : α → β}, MeasureTheory.Integrable f μ
-- Init.Data.SInt.Bitwise
instCommutativeInt32HAnd : Std.Commutative fun x1 x2 => x1 &&& x2
-- Mathlib.Algebra.Group.Hom.Defs
instCoeTCMulHomOfMulHomClass.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Mul M] [inst_1 : Mul N] [inst_2 : FunLike F M N]
  [inst_3 : MulHomClass F M N], instCoeTCMulHomOfMulHomClass = { coe := MulHomClass.toMulHom }
-- Mathlib.GroupTheory.Nilpotent
Subgroup.commutator_upperCentralSeries_top_le : ∀ (G : Type u_1) [inst : Group G] (n : ℕ), ⁅Subgroup.upperCentralSeries G (n + 1), ⊤⁆ ≤ Subgroup.upperCentralSeries G n
-- Mathlib.Topology.UnitInterval
unitInterval.toNNReal_add_toNNReal_symm : ∀ (x : ↑unitInterval), unitInterval.toNNReal x + unitInterval.toNNReal (unitInterval.symm x) = 1
-- Mathlib.CategoryTheory.Monoidal.Cartesian.InfSemilattice
CategoryTheory.SemilatticeInf.tensorUnit : ∀ {C : Type u} [inst : SemilatticeInf C] [inst_1 : OrderTop C], CategoryTheory.MonoidalCategoryStruct.tensorUnit C = ⊤
-- Mathlib.Tactic.Linter.UnusedInstancesInType
_private.Mathlib.Tactic.Linter.UnusedInstancesInType.0.Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern.mk : Lean.FVarId → ℕ → Mathlib.Linter.UnusedInstancesInType.InstanceOfConcern✝
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.ZeroHypercover.map_toPreZeroHypercover : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C} {S : C} {D : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} D] {K : CategoryTheory.Precoverage D} (F : CategoryTheory.Functor C D)
  (E : J.ZeroHypercover S) (h : J ≤ CategoryTheory.Precoverage.comap F K),
  (CategoryTheory.Precoverage.ZeroHypercover.map F E h).toPreZeroHypercover =
    CategoryTheory.PreZeroHypercover.map F E.toPreZeroHypercover
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.mem_coeffsIn : ∀ {R : Type u_2} {S : Type u_3} {σ : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Module R S]
  {M : Submodule R S} {p : MvPolynomial σ S}, p ∈ MvPolynomial.coeffsIn σ M ↔ ∀ (i : σ →₀ ℕ), MvPolynomial.coeff i p ∈ M
-- Mathlib.Analysis.Analytic.Order
/-- **Alias** of `AnalyticOnNhd.isClopen_setOfPred_analyticOrderAt_eq_top`.

---

The set where an analytic function has infinite order is clopen in its domain of analyticity.  -/
AnalyticOnNhd.isClopen_setOf_analyticOrderAt_eq_top : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} {f : 𝕜 → E}, AnalyticOnNhd 𝕜 f U → IsClopen {u | analyticOrderAt f ↑u = ⊤}
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.toContinuousLinearMap_toLinearIsometry : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂), e.toLinearIsometry.toContinuousLinearMap = ↑↑e
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.homOver_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} {ℱ : CategoryTheory.Functor Dᵒᵖ A}
  {ℱ' : CategoryTheory.Sheaf K A} (α : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj) (X : A) (X_1 : Cᵒᵖ),
  (CategoryTheory.Functor.IsCoverDense.homOver α X).app X_1 =
    TypeCat.ofHom fun g => CategoryTheory.CategoryStruct.comp g (α.app X_1)
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.liftFun.eq_1 : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] {S : Type u_2} [inst_2 : Semiring S]
  (f : (k : ℕ) → S →+* TruncatedWittVector p k R) (s : S),
  WittVector.liftFun f s = { coeff := fun k => TruncatedWittVector.coeff (Fin.last k) ((f (k + 1)) s) }
-- Mathlib.Data.List.AList
AList.union_entries : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {s₁ s₂ : AList β},
  (s₁ ∪ s₂).entries = s₁.entries.kunion s₂.entries
-- Mathlib.Algebra.LinearRecurrence
/-- Order of the linear recurrence  -/
LinearRecurrence.order : {R : Type u_1} → [inst : CommSemiring R] → LinearRecurrence R → ℕ
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.id_apply : ∀ (M : Type u_1) [inst : Monoid M] {A : Type u_4} [inst_1 : Monoid A] [inst_2 : MulDistribMulAction M A] (x : A),
  (MulDistribMulActionHom.id M) x = x
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.ofHom_zsmul : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {X Y : Type w} [inst_2 : AddCommGroup X]
  [inst_3 : AddCommGroup Y] [inst_4 : Module k X] [inst_5 : Module k Y] {ρ : Representation k G X}
  {σ : Representation k G Y} (f : ρ.IntertwiningMap σ) (n : ℤ), Rep.ofHom (n • f) = n • Rep.ofHom f
-- Mathlib.CategoryTheory.Endomorphism
CategoryTheory.Aut.ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {φ₁ φ₂ : CategoryTheory.Aut X},
  φ₁ = φ₂ ↔ φ₁.hom = φ₂.hom
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with
`[ContinuousAdd]`. The primed version of the lemma uses an explicit continuity assumption on
addition, for application to `EReal`.  -/
UpperSemicontinuousWithinAt.add : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {x : α} {γ : Type u_5} [inst_1 : AddCommMonoid γ]
  [inst_2 : LinearOrder γ] [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] [ContinuousAdd γ]
  {f g : α → γ},
  UpperSemicontinuousWithinAt f s x →
    UpperSemicontinuousWithinAt g s x → UpperSemicontinuousWithinAt (fun z => f z + g z) s x
-- Init.Data.BitVec.Basic
/-- Auxiliary function for `rotateRight`, which does not take into account the case where
the rotation amount is greater than the bitvector width.
 -/
BitVec.rotateRightAux : {w : ℕ} → BitVec w → ℕ → BitVec w
-- Mathlib.Data.Finset.Disjoint
Finset.disjUnion.congr_simp : ∀ {α : Type u_2} (s s_1 : Finset α) (e_s : s = s_1) (t t_1 : Finset α) (e_t : t = t_1) (h : Disjoint s t),
  s.disjUnion t h = s_1.disjUnion t_1 ⋯
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
sub_le_sub_right : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [AddRightMono α] {a b : α}, a ≤ b → ∀ (c : α), a - c ≤ b - c
-- Mathlib.Algebra.Order.Group.Action
smul_mono_right : ∀ {M : Type u_2} {α : Type u_3} [inst : SMul M α] [inst_1 : Preorder α] [CovariantClass M α HSMul.hSMul LE.le] (m : M),
  Monotone (HSMul.hSMul m)