mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.Widget.StringDiagram
/-- The list of nodes at the top of a string diagram. The position is counted from the
specified natural number.  -/
Mathlib.Tactic.BicategoryLike.NormalExpr.nodesAux : {ρ : Type} →
  [Mathlib.Tactic.BicategoryLike.MonadMor₁ (Mathlib.Tactic.BicategoryLike.CoherenceM ρ)] →
    ℕ →
      Mathlib.Tactic.BicategoryLike.NormalExpr →
        Mathlib.Tactic.BicategoryLike.CoherenceM ρ (List (List Mathlib.Tactic.Widget.StringDiagram.Node))
-- Init.Data.Array.Range
Array.range'_append_1 : ∀ {s m n : ℕ}, Array.range' s m ++ Array.range' (s + m) n = Array.range' s (m + n)
-- Mathlib.Algebra.Order.BigOperators.Group.LocallyFinite
Finset.prod_prod_Ioi_mul_eq_prod_prod_off_diag : ∀ {α : Type u_1} {M : Type u_2} [inst : CommMonoid M] [inst_1 : LinearOrder α] [inst_2 : Fintype α]
  [inst_3 : LocallyFiniteOrderTop α] [LocallyFiniteOrderBot α] (f : α → α → M),
  ∏ i, ∏ j > i, f j i * f i j = ∏ i, ∏ j ∈ {i}ᶜ, f j i
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.PUnit
FundamentalGroupoid.instSubsingletonHomPUnit : ∀ {x y : FundamentalGroupoid PUnit.{u_1 + 1}}, Subsingleton (x ⟶ y)
-- Lean.Meta.RecursorInfo
/-- Compute number of parameters for (user-defined) recursor.
We assume a parameter is anything that occurs before the motive  -/
_private.Lean.Meta.RecursorInfo.0.Lean.Meta.getNumParams : Array Lean.Expr → Lean.Expr → ℕ → ℕ
-- Mathlib.CategoryTheory.Comma.Arrow
/-- `Arrow T` is equivalent to a sigma type.  -/
CategoryTheory.Arrow.equivSigma : (T : Type u) → [inst : CategoryTheory.Category.{v, u} T] → CategoryTheory.Arrow T ≃ (X : T) × (Y : T) × (X ⟶ Y)
-- Mathlib.Analysis.Normed.Unbundled.AlgebraNorm
AlgebraNorm.mk.inj : ∀ {R : Type u_1} {inst : SeminormedCommRing R} {S : Type u_2} {inst_1 : Ring S} {inst_2 : Algebra R S}
  {toRingNorm : RingNorm S} {smul' : ∀ (a : R) (x : S), toRingNorm.toFun (a • x) = ‖a‖ * toRingNorm.toFun x}
  {toRingNorm_1 : RingNorm S} {smul'_1 : ∀ (a : R) (x : S), toRingNorm_1.toFun (a • x) = ‖a‖ * toRingNorm_1.toFun x},
  { toRingNorm := toRingNorm, smul' := smul' } = { toRingNorm := toRingNorm_1, smul' := smul'_1 } →
    toRingNorm = toRingNorm_1
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given Localization maps `f : M →* N, k : P →* U` for Submonoids `S, T` respectively, an
isomorphism `j : M ≃* P` such that `j(S) = T` induces an isomorphism of localizations `N ≃* U`.  -/
Submonoid.LocalizationMap.mulEquivOfMulEquiv : {M : Type u_1} →
  [inst : CommMonoid M] →
    {S : Submonoid M} →
      {N : Type u_2} →
        [inst_1 : CommMonoid N] →
          {P : Type u_3} →
            [inst_2 : CommMonoid P] →
              S.LocalizationMap N →
                {T : Submonoid P} →
                  {Q : Type u_4} →
                    [inst_3 : CommMonoid Q] →
                      T.LocalizationMap Q → {j : M ≃* P} → Submonoid.map j.toMonoidHom S = T → N ≃* Q
-- Mathlib.Analysis.Normed.Module.Alternating.Curry
ContinuousAlternatingMap.curryLeft_add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {n : ℕ}
  (f g : E [⋀^Fin (n + 1)]→L[𝕜] F), (f + g).curryLeft = f.curryLeft + g.curryLeft
-- Mathlib.Topology.Instances.CantorSet
/-- Given `x` in the Cantor set, return its ternary representation `(d₀, d₁, …)`
using only digits `0` and `2`, such that `x = 0.d₀d₁...` in base-3.  -/
cantorToTernary : ℝ → Stream' (Fin 3)
-- Init.Data.Vector.Extract
Vector.extract_eq_pop : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {stop : ℕ} (h : stop = n - 1), xs.extract 0 stop = Vector.cast ⋯ xs.pop
-- Mathlib.LinearAlgebra.FiniteDimensional.Basic
/-- The submodule generated by a supremum of finite-dimensional submodules, indexed by a finite
sort is finite-dimensional.  -/
Submodule.finiteDimensional_iSup : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Sort u_1}
  [Finite ι] (S : ι → Submodule K V) [∀ (i : ι), FiniteDimensional K ↥(S i)], FiniteDimensional K ↥(⨆ i, S i)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.h : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.tmul_neg : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {P : Type u_4} [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup P] [inst_3 : Module R M] [inst_4 : Module R P] (m : M) (p : P), m ⊗ₜ[R] (-p) = -m ⊗ₜ[R] p
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.ext : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] (N N' : LieSubmodule R L M), (∀ (m : M), m ∈ N ↔ m ∈ N') → N = N'
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.seq_destruct_think : ∀ {α : Type u} (s : Stream'.WSeq α), Stream'.Seq.destruct s.think = some (none, s)
-- Mathlib.Algebra.Polynomial.UnitTrinomial
/-- Shorthand for a trinomial  -/
Polynomial.trinomial : {R : Type u_1} → [inst : Semiring R] → ℕ → ℕ → ℕ → R → R → R → Polynomial R
-- Lean.Structure
/-- The fields should be in the order that they appear in the structure's constructor.  -/
Lean.StructureDescr.fields : Lean.StructureDescr → Array Lean.StructureFieldInfo
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.setLAverage_congr_fun : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α} {f g : α → ENNReal},
  MeasurableSet s → Set.EqOn f g s → ⨍⁻ (x : α) in s, f x ∂μ = ⨍⁻ (x : α) in s, g x ∂μ
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.inductionOn : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] {G : ι → Type w} [inst_1 : (i : ι) → L.Structure (G i)]
  {f : (i j : ι) → i ≤ j → L.Embedding (G i) (G j)} [inst_2 : IsDirectedOrder ι]
  [inst_3 : DirectedSystem G fun i j h => ⇑(f i j h)] [inst_4 : Nonempty ι]
  {C : FirstOrder.Language.DirectLimit G f → Prop} (z : FirstOrder.Language.DirectLimit G f),
  (∀ (i : ι) (x : G i), C ((FirstOrder.Language.DirectLimit.of L ι G f i) x)) → C z
-- Mathlib.Analysis.Normed.Group.Basic
mul_mem_ball_iff_norm : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a b : E} {r : ℝ}, a * b ∈ Metric.ball a r ↔ ‖b‖ < r
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.instDecidableEqIterator.decEq.match_1.splitter : (motive : String.Legacy.Iterator → String.Legacy.Iterator → Sort u_1) →
  (x x_1 : String.Legacy.Iterator) →
    ((a : String) →
        (a_1 : String.Pos.Raw) →
          (b : String) → (b_1 : String.Pos.Raw) → motive { s := a, i := a_1 } { s := b, i := b_1 }) →
      motive x x_1
-- Mathlib.CategoryTheory.Limits.Types.Colimits
/-- (internal implementation) the colimit cocone of a functor,
implemented as a quotient of a sigma type
 -/
CategoryTheory.Limits.Types.TypeMax.colimitCocone : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J (Type (max v u))) → CategoryTheory.Limits.Cocone F
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
ContinuousLinearMap.lTensor_eq_mapL : ∀ {𝕜 : Type u_1} (E : Type u_2) {G : Type u_4} {H : Type u_5} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup G] [inst_4 : InnerProductSpace 𝕜 G]
  [inst_5 : NormedAddCommGroup H] [inst_6 : InnerProductSpace 𝕜 H] (g : G →L[𝕜] H),
  ContinuousLinearMap.lTensor E g = TensorProduct.mapL (ContinuousLinearMap.id 𝕜 E) g
-- Mathlib.Data.List.Sym
List.sym2_eq_nil_iff : ∀ {α : Type u_1} {xs : List α}, xs.sym2 = [] ↔ xs = []
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Internal.Raw₀.diff.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  m₁.diff m₂ =
    if (↑m₁).size ≤ (↑m₂).size then Std.DHashMap.Internal.Raw₀.filter (fun k x => !m₂.contains k) m₁
    else ↑(m₁.eraseManyEntries ↑m₂)
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.inverts : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [L.IsLocalization W], W.IsInvertedBy L
-- Mathlib.Data.Set.Lattice
Set.iUnion₂_inter : ∀ {α : Type u_1} {ι : Sort u_5} {κ : ι → Sort u_8} (s : (i : ι) → κ i → Set α) (t : Set α),
  (⋃ i, ⋃ j, s i j) ∩ t = ⋃ i, ⋃ j, s i j ∩ t
-- Mathlib.Computability.Primrec.List
Primrec.list_head? : ∀ {α : Type u_1} [inst : Primcodable α], Primrec List.head?
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem!_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α}
  [inst : Inhabited β] {f : β → β}, (t.modify k f)[k]! = (Option.map f t[k]?).get!
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.le_trailingDegree_C : ∀ {R : Type u} {a : R} [inst : Semiring R], 0 ≤ (Polynomial.C a).trailingDegree
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.finrank_rootSpan_map_polarization_eq_finrank_corootSpan : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [IsDomain R] [inst_5 : Module R M] [inst_6 : Module R N]
  (P : RootPairing ι R M N) [P.IsAnisotropic],
  Module.finrank R ↥(Submodule.map P.Polarization (P.rootSpan R)) = Module.finrank R ↥(P.corootSpan R)
-- Init.Data.Nat.Control
/-- Executes a monadic action on all the numbers less than some bound, in increasing order.

Example:
````lean example
#eval Nat.forM 5 fun i _ => IO.println i
````
````output
0
1
2
3
4
````
 -/
Nat.forM : {m : Type → Type u_1} → [Monad m] → (n : ℕ) → ((i : ℕ) → i < n → m Unit) → m Unit
-- Mathlib.GroupTheory.PGroup
IsPGroup.of_surjective : ∀ {p : ℕ} {G : Type u_1} [inst : Group G],
  IsPGroup p G → ∀ {H : Type u_2} [inst_1 : Group H] (ϕ : G →* H), Function.Surjective ⇑ϕ → IsPGroup p H
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.forIn_eq_forIn_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : α → δ → m (ForInStep δ)} {init : δ},
  (forIn t init fun a d => f a.1 d) = forIn t.keys init f
-- Mathlib.Topology.NoetherianSpace
TopologicalSpace.instWellFoundedLTClosedsOfNoetherianSpace : ∀ {α : Type u_1} [inst : TopologicalSpace α] [TopologicalSpace.NoetherianSpace α],
  WellFoundedLT (TopologicalSpace.Closeds α)
-- Mathlib.Analysis.Asymptotics.Theta
Asymptotics.isTheta_const_const_iff : ∀ {α : Type u_1} {E'' : Type u_9} {F'' : Type u_10} [inst : NormedAddCommGroup E''] [inst_1 : NormedAddCommGroup F'']
  {l : Filter α} [l.NeBot] {c₁ : E''} {c₂ : F''}, ((fun x => c₁) =Θ[l] fun x => c₂) ↔ (c₁ = 0 ↔ c₂ = 0)
-- Mathlib.Data.Finset.Erase
Finset.erase_val : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Finset α) (a : α), (s.erase a).val = s.val.erase a
-- Init.Data.Vector.Attach
Vector.mem_attach : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (x : { x // x ∈ xs }), x ∈ xs.attach
-- Mathlib.Tactic.Core
/-- `iterateExactly' n t` executes `t` `n` times. If any iteration fails, the whole tactic fails.
 -/
Lean.Elab.Tactic.iterateExactly' : {m : Type → Type u} → [Monad m] → ℕ → m Unit → m Unit
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.head?_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] [inst : Min α]
  [inst_1 : LE α] [Std.LawfulOrderCmp cmp] [Std.LawfulOrderMin α] [Std.LawfulOrderLeftLeaningMin α]
  [Std.LawfulEqCmp cmp], t.keys.head? = t.minKey?
-- Mathlib.Data.Set.Card
Set.encard_pos : ∀ {α : Type u_1} {s : Set α}, 0 < s.encard ↔ s.Nonempty
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.eq_eq_subst : ∀ {α : Type u_1} [inst : Lean.Grind.IntModule α] (ctx : Lean.Grind.Linarith.Context α) (x : Lean.Grind.Linarith.Var)
  (p₁ p₂ p₃ : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.eq_eq_subst_cert x p₁ p₂ p₃ = true →
    Lean.Grind.Linarith.Poly.denote' ctx p₁ = 0 →
      Lean.Grind.Linarith.Poly.denote' ctx p₂ = 0 → Lean.Grind.Linarith.Poly.denote' ctx p₃ = 0
-- Init.Data.List.Lemmas
List.isEqv.eq_2 : ∀ {α : Type u} (x : α → α → Bool) (a : α) (as : List α) (b : α) (bs : List α),
  (a :: as).isEqv (b :: bs) x = (x a b && as.isEqv bs x)
-- Mathlib.CategoryTheory.Abelian.Basic
/-- `Abelian.image` as a functor from the arrow category.  -/
CategoryTheory.Abelian.im : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Abelian C] → CategoryTheory.Functor (CategoryTheory.Arrow C) C
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_isZero_leftHomology : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology], S.Exact ↔ CategoryTheory.Limits.IsZero S.leftHomology
-- Mathlib.MeasureTheory.Measure.Haar.NormedSpace
MonoidHom.exists_nhds_isBounded : ∀ {G : Type u_1} {H : Type u_2} [inst : MeasurableSpace G] [inst_1 : Group G] [inst_2 : TopologicalSpace G]
  [IsTopologicalGroup G] [BorelSpace G] [LocallyCompactSpace G] [inst_6 : MeasurableSpace H]
  [inst_7 : SeminormedGroup H] [OpensMeasurableSpace H] (f : G →* H),
  Measurable ⇑f → ∀ (x : G), ∃ s ∈ nhds x, Bornology.IsBounded (⇑f '' s)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.unshift_shift : ∀ {𝕜 : Type u} {E : Type v} {F : Type w} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {p : FormalMultilinearSeries 𝕜 E (E →L[𝕜] F)} {z : F}, (p.unshift z).shift = p
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.equivQuotientZPowOfEquiv_symm : ∀ {A B : Type u} [inst : CommGroup A] [inst_1 : CommGroup B] (e : A ≃* B) (n : ℤ),
  (QuotientGroup.equivQuotientZPowOfEquiv e n).symm = QuotientGroup.equivQuotientZPowOfEquiv e.symm n
-- Mathlib.MeasureTheory.Measure.HasOuterApproxClosedProd
Measure.eq_prod_of_integral_prod_mul_boundedContinuousFunction : ∀ {ι : Type u_1} {T : Type u_4} {X : ι → Type u_5} {mX : (i : ι) → MeasurableSpace (X i)}
  [inst : (i : ι) → TopologicalSpace (X i)] [∀ (i : ι), BorelSpace (X i)] [∀ (i : ι), HasOuterApproxClosed (X i)]
  {mT : MeasurableSpace T} [inst_3 : TopologicalSpace T] [BorelSpace T] [HasOuterApproxClosed T] [inst_6 : Fintype ι]
  {μ : MeasureTheory.Measure ((i : ι) → X i)} {ν : MeasureTheory.Measure T}
  {ξ : MeasureTheory.Measure (((i : ι) → X i) × T)} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [MeasureTheory.IsFiniteMeasure ξ],
  (∀ (f : (i : ι) → BoundedContinuousFunction (X i) ℝ) (g : BoundedContinuousFunction T ℝ),
      ∫ (p : ((i : ι) → X i) × T), (∏ i, (f i) (p.1 i)) * g p.2 ∂ξ =
        (∫ (x : (i : ι) → X i), ∏ i, (f i) (x i) ∂μ) * ∫ (t : T), g t ∂ν) →
    ξ = μ.prod ν
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateSubgroup.subgroup : ∀ {G : Type u_1} [inst : Group G] {S : Type u_2} [inst_1 : SetLike S G] [SubgroupClass S G] {H : S},
  IsApproximateSubgroup 1 ↑H
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.Hom.eq_3 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.WithInitial C),
  CategoryTheory.WithInitial.star.Hom x = PUnit.{v + 1}
-- Std.Http.Protocol.H1.Reader
/-- Gets the number of bytes remaining in the input buffer.
 -/
Std.Http.Protocol.H1.Reader.remainingBytes : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Reader dir → ℕ
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instMul : {R : Type u_1} → [inst : Monoid R] → {S : Submonoid R} → [inst_1 : OreLocalization.OreSet S] → Mul (OreLocalization S R)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get_diff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [inst_2 : EquivBEq α]
  [inst_3 : LawfulHashable α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} {h_mem : k ∈ m₁ \ m₂},
  (m₁ \ m₂).get k h_mem = m₁.get k ⋯
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.norm_intCast_lt_one_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {z : ℤ}, ‖↑z‖ < 1 ↔ ↑p ∣ z
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.submonoid.eq_1 : ∀ (α : Type u_2) (β : Type u_4) [inst : TopologicalSpace α] [inst_1 : MulOneClass β],
  HasCompactMulSupport.submonoid α β = { carrier := {f | HasCompactMulSupport f}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Lean.Widget.UserWidget
_private.Lean.Widget.UserWidget.0.Lean.Widget.builtinModulesRef : IO.Ref (Std.TreeMap UInt64 (Lean.Name × Lean.Widget.Module) compare)
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.span_univ : ∀ (R : Type u) (L : Type v) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieSubalgebra.lieSpan R L Set.univ = ⊤
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.OplaxTrans.mk.sizeOf_spec : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} [inst_2 : SizeOf B] [inst_3 : SizeOf C] (app : (a : B) → F.obj a ⟶ G.obj a)
  (naturality :
    {a b : B} →
      (f : a ⟶ b) →
        CategoryTheory.CategoryStruct.comp (F.map f) (app b) ⟶ CategoryTheory.CategoryStruct.comp (app a) (G.map f))
  (naturality_naturality :
    autoParam
      (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b)) (naturality g) =
          CategoryTheory.CategoryStruct.comp (naturality f) (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η)))
      CategoryTheory.Lax.OplaxTrans.naturality_naturality._autoParam)
  (naturality_id :
    autoParam
      (∀ (a : B),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a))
            (naturality (CategoryTheory.CategoryStruct.id a)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (app a)).inv
              (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a))))
      CategoryTheory.Lax.OplaxTrans.naturality_id._autoParam)
  (naturality_comp :
    autoParam
      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c))
            (naturality (CategoryTheory.CategoryStruct.comp f g)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).hom
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g))
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).inv
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (naturality f) (G.map g))
                  (CategoryTheory.CategoryStruct.comp
                    (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).hom
                    (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g)))))))
      CategoryTheory.Lax.OplaxTrans.naturality_comp._autoParam),
  sizeOf
      { app := app, naturality := naturality, naturality_naturality := naturality_naturality,
        naturality_id := naturality_id, naturality_comp := naturality_comp } =
    1
-- Init.Data.List.MinMax
List.min_replicate : ∀ {α : Type u_1} [inst : Min α] [Std.MinEqOr α] {n : ℕ} {a : α} (h : List.replicate n a ≠ []),
  (List.replicate n a).min h = a
-- Mathlib.Data.Multiset.Basic
Multiset.toList_eq_nil : ∀ {α : Type u_1} {s : Multiset α}, s.toList = [] ↔ s = 0
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.gFunctor_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C), CategoryTheory.ShortComplex.gFunctor.obj S = CategoryTheory.Arrow.mk S.g
-- Mathlib.Topology.Algebra.Valued.WithVal
Valuation.IsEquiv.orderRingIso.congr_simp : ∀ {R : Type u_4} {Γ₀ : Type u_5} {Γ₀' : Type u_6} [inst : Ring R] [inst_1 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_2 : LinearOrderedCommGroupWithZero Γ₀'] {v : Valuation R Γ₀} {w : Valuation R Γ₀'} (h : v.IsEquiv w),
  h.orderRingIso = h.orderRingIso
-- Init.Data.Nat.Lemmas
Nat.mul_pos_iff_of_pos_left : ∀ {a b : ℕ}, 0 < a → (0 < a * b ↔ 0 < b)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙHomSuperset_apply : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p] {a : A} (ha : p a)
  {s : Set R} (hs : quasispectrum R a ⊆ s) (a_1 : ContinuousMapZero (↑s) R),
  (cfcₙHomSuperset ha hs) a_1 =
    (cfcₙHom ha) (a_1.comp { toFun := Subtype.map id hs, continuous_toFun := ⋯, map_zero' := ⋯ })
-- Mathlib.Algebra.Star.Conjneg
conjneg_one : ∀ {G : Type u_2} {R : Type u_3} [inst : AddGroup G] [inst_1 : CommSemiring R] [inst_2 : StarRing R], conjneg 1 = 1
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.LeftExtension.IsPointwiseLeftKanExtension.isIso_hom : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.LeftExtension F}
  (h : E.IsPointwiseLeftKanExtension) [L.Full] [L.Faithful], CategoryTheory.IsIso (CategoryTheory.StructuredArrow.hom E)
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
CategoryTheory.Functor.CoconeTypes.IsColimitCore.fac_apply : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {F : CategoryTheory.Functor J (Type w₀)} {c : F.CoconeTypes}
  (hc : c.IsColimitCore) (c' : F.CoconeTypes) (j : J) (x : F.obj j), hc.desc c' (c.ι j x) = c'.ι j x
-- Mathlib.Algebra.Group.Action.Defs
VAddCommClass.op_left : ∀ {M : Type u_1} {N : Type u_2} {α : Type u_5} [inst : VAdd M α] [inst_1 : VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α]
  [inst_3 : VAdd N α] [VAddCommClass M N α], VAddCommClass Mᵃᵒᵖ N α
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.ofComponents'_hom_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (app : (X : C) → F.obj X ≅ G.obj X)
  (naturality :
    autoParam
      (∀ {X Y : C} (f : Y ⟶ X),
        CategoryTheory.CategoryStruct.comp (app Y).inv (F.map f) =
          CategoryTheory.CategoryStruct.comp (G.map f) (app X).inv)
      CategoryTheory.NatIso.ofComponents'._auto_1)
  (X : C), (CategoryTheory.NatIso.ofComponents' app naturality).hom.app X = (app X).hom
-- Init.Prelude
/-- Decides whether two word-sized unsigned integers are equal. Usually accessed via the
`DecidableEq USize` instance.

This function is overridden at runtime with an efficient implementation.

Examples:
 * `USize.decEq 123 123 = .isTrue rfl`
 * `(if (6 : USize) = 7 then "yes" else "no") = "no"`
 * `show (7 : USize) = 7 by decide`
 -/
USize.decEq : (a b : USize) → Decidable (a = b)
-- Mathlib.Order.Hom.Set
OrderIso.symm_image_image : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) (s : Set α), ⇑e.symm '' ⇑e '' s = s
-- Mathlib.LinearAlgebra.CliffordAlgebra.SpinGroup
spinGroup.mul_star_self_of_mem : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {x : CliffordAlgebra Q}, x ∈ spinGroup Q → x * star x = 1
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.support_prefix_support_append : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (q : G.Walk v w), p.support <+: (p.append q).support