mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Defs
/-- `get n A i j` returns the (i, j)th entry of the `n × n` matrix whose entries are
stored in `A` in row-major order.

The function does not check the matrix index bounds.
 -/
BirdDet.get : {R : Type u_1} → [CommRing R] → ℕ → Array R → ℕ → ℕ → R
-- Mathlib.RingTheory.Morita.Matrix
ModuleCat.matrixEquivalence_unitIso : ∀ (R : Type u) {ι : Type v} [inst : Ring R] [inst_1 : Fintype ι] [inst_2 : DecidableEq ι] (i : ι),
  (ModuleCat.matrixEquivalence R i).unitIso = (MatrixModCat.unitIso R i).symm
-- Init.Data.Array.Lemmas
Array.filter_reverse : ∀ {α : Type u_1} {p : α → Bool} {xs : Array α}, Array.filter p xs.reverse = (Array.filter p xs).reverse
-- Batteries.Classes.Order
Std.TransCmp.le_trans : ∀ {α : Type u_1} {cmp : α → α → Ordering} [Std.TransCmp cmp] {x y z : α},
  cmp x y ≠ Ordering.gt → cmp y z ≠ Ordering.gt → cmp x z ≠ Ordering.gt
-- Init.Data.Array.Attach
Array.reverse_wfParam : ∀ {α : Type u_1} {xs : Array α}, (wfParam xs).reverse = xs.attach.unattach.reverse
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instInhabited : {k : Type u_1} → {G : Type u_2} → [inst : AddMonoid k] → Inhabited (SkewMonoidAlgebra k G)
-- Mathlib.Analysis.ODE.Transform
IsIntegralCurve.comp_mul : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {γ : ℝ → E} {v : ℝ → E → E},
  IsIntegralCurve γ v → ∀ (a : ℝ), IsIntegralCurve (γ ∘ fun x => x * a) (a • v ∘ fun x => x * a)
-- Mathlib.Topology.Algebra.UniformMulAction
smul_uniformity : ∀ {M : Type v} {X : Type x} [inst : UniformSpace X] [inst_1 : Group M] [inst_2 : MulAction M X]
  [UniformContinuousConstSMul M X] (c : M), c • uniformity X = uniformity X
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
/-- The indefinite version of the `Γ` function, `Γ(s, X) = ∫ x ∈ 0..X, exp(-x) x ^ (s - 1)`.  -/
Complex.partialGamma : ℂ → ℝ → ℂ
-- Mathlib.GroupTheory.MonoidLocalization.Maps
Localization.mulEquivOfQuotient_symm_monoidOf : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  {f : S.LocalizationMap N} (x : M), (Localization.mulEquivOfQuotient f).symm (f x) = (Localization.monoidOf S) x
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.ext_iff : ∀ {A : Type u_1} {ι : Type u_2} {E : ι → Type u_3} {x y : WithCStarModule A ((i : ι) → E i)},
  x = y ↔ ∀ (i : ι), x i = y i
-- Init.Data.Nat.Lemmas
Nat.add_right_min_self : ∀ {a b : ℕ}, min (a + b) a = a
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.op_hom : ∀ {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} (α : F ≅ G), (CategoryTheory.NatIso.op α).hom = CategoryTheory.NatTrans.op α.hom
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
/-- The Stieltjes function associated to a bounded variation function. It is given by
the variation of the function `f.rightLim` from a fixed base point.
Using right limits ensures the right continuity, which is used to construct Stieltjes measures.  -/
BoundedVariationOn.stieltjesFunctionRightLim : {α : Type u_1} →
  [inst : LinearOrder α] →
    [inst_1 : TopologicalSpace α] →
      [OrderTopology α] →
        {E : Type u_2} →
          [inst_3 : NormedAddCommGroup E] →
            [CompleteSpace E] → {f : α → E} → BoundedVariationOn f Set.univ → α → StieltjesFunction α
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.cons_isCycle_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk v u) (h : G.Adj u v),
  (SimpleGraph.Walk.cons h p).IsCycle ↔ p.IsPath ∧ s(u, v) ∉ p.edges
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.supermartingale_of_setIntegral_succ_le : ∀ {Ω : Type u_1} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {𝒢 : MeasureTheory.Filtration ℕ m0}
  [MeasureTheory.IsFiniteMeasure μ] {f : ℕ → Ω → ℝ},
  MeasureTheory.StronglyAdapted 𝒢 f →
    (∀ (i : ℕ), MeasureTheory.Integrable (f i) μ) →
      (∀ (i : ℕ) (s : Set Ω), MeasurableSet s → ∫ (ω : Ω) in s, f (i + 1) ω ∂μ ≤ ∫ (ω : Ω) in s, f i ω ∂μ) →
        MeasureTheory.Supermartingale f 𝒢 μ
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.leadingCoeff_smul_of_smul_regular : ∀ {R : Type u} [inst : Semiring R] {S : Type u_1} [inst_1 : SMulZeroClass S R] {k : S} (p : Polynomial R),
  IsSMulRegular R k → (k • p).leadingCoeff = k • p.leadingCoeff
-- Mathlib.Analysis.Calculus.Deriv.Basic
hasDerivWithinAt_univ : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {f' : F} {x : 𝕜}, HasDerivWithinAt f f' Set.univ x ↔ HasDerivAt f f' x
-- Mathlib.Analysis.Calculus.ContDiff.Comp
/-- The composition of `C^n` functions at points in domains is `C^n`,
with a weaker condition on `s` and `t`.  -/
ContDiffWithinAt.comp_of_mem_nhdsWithin_image : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {t : Set F} {g : F → G}
  {f : E → F} (x : E),
  ContDiffWithinAt 𝕜 n g t (f x) →
    ContDiffWithinAt 𝕜 n f s x → t ∈ nhdsWithin (f x) (f '' s) → ContDiffWithinAt 𝕜 n (g ∘ f) s x
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isSeparator_coprod : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] (G H : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct G H],
  CategoryTheory.IsSeparator (G ⨿ H) ↔ (CategoryTheory.ObjectProperty.pair G H).IsSeparating
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- the pentagon relation expressing the compatibility of the left
and right homology data  -/
CategoryTheory.ShortComplex.HomologyData.comm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex C} (self : S.HomologyData),
  CategoryTheory.CategoryStruct.comp self.left.π (CategoryTheory.CategoryStruct.comp self.iso.hom self.right.ι) =
    CategoryTheory.CategoryStruct.comp self.left.i self.right.p
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
LinearMap.toAffineMap_linear : ∀ {k : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module k V₂] (f : V₁ →ₗ[k] V₂), f.toAffineMap.linear = f
-- Init.Data.Int.Linear
Int.Internal.Linear.dvd_solve_combine_cert.eq_1 : ∀ (d₁ : ℤ) (p₁ : Int.Internal.Linear.Poly) (d₂ : ℤ) (p₂ : Int.Internal.Linear.Poly) (d : ℤ)
  (p : Int.Internal.Linear.Poly) (g α β : ℤ),
  Int.Internal.Linear.dvd_solve_combine_cert d₁ p₁ d₂ p₂ d p g α β =
    Int.Internal.Linear.Poly.rec (fun x => false)
      (fun a₁ x₁ p₁ x =>
        Int.Internal.Linear.Poly.rec (fun x => false)
          (fun a₂ x₂ p₂ x =>
            (Nat.beq x₁ x₂).and'
              ((g.beq' (α * a₁ * d₂ + β * a₂ * d₁)).and'
                ((d.beq' (d₁ * d₂)).and'
                  (p.beq'
                    (Int.Internal.Linear.Poly.add g x₁
                      (Int.Internal.Linear.Poly.combine_mul_k (α * d₂) (β * d₁) p₁ p₂))))))
          p₂)
      p₁
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.firstReturn_nest : ∀ {p : DyckWord}, p.nest.firstReturn = (↑p).length + 1
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.cover_X : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰)
  [inst_2 : Small.{u, u_1} 𝒰.I₀] [inst_3 : Quiver.IsThin 𝒰.I₀] (a : 𝒰.I₀), d.cover.X a = d.functor.obj a
-- Mathlib.Algebra.Order.Floor.Ring
Int.image_fract : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] [IsOrderedRing R] (s : Set R),
  Int.fract '' s = ⋃ m, (fun x => x - ↑m) '' s ∩ Set.Ico 0 1
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.eq_of_revlexWF : ∀ {m₁ m₂ : Lean.Grind.CommRing.Mon}, m₁.revlexWF m₂ = Ordering.eq → m₁ = m₂
-- Std.Http.Data.URI.Encoding
Std.Http.URI.instToStringEncodedQueryString : {r : UInt8 → Bool} → ToString (Std.Http.URI.EncodedQueryString r)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.InnerRegularCompactLTTop.smul : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [h : μ.InnerRegularCompactLTTop] (c : ENNReal), (c • μ).InnerRegularCompactLTTop
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_cons : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f : β → α} {b : β}
  (h : b ∉ s), (Finset.cons b s h).inf f = f b ⊓ s.inf f
-- Init.Data.Vector.Lemmas
Vector.getElem?_eq_getElem : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n), xs[i]? = some xs[i]
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_nat_add' : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddCommMonoidWithOne G]
  [inst_2 : AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ) (x : G), f (↑n + x) = f x + n • b
-- Init.Data.Nat.Lemmas
Nat.pow_eq_one : ∀ {a n : ℕ}, a ^ n = 1 ↔ a = 1 ∨ n = 0
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.uniqueRingEquiv.eq_1 : ∀ {R : Type u_1} (M : Type u_4) [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Subsingleton M],
  MonoidAlgebra.uniqueRingEquiv M =
    { toEquiv := (MonoidAlgebra.coeffAddEquiv.trans (Finsupp.uniqueAddEquiv 1)).toEquiv, map_mul' := ⋯, map_add' := ⋯ }
-- Mathlib.GroupTheory.Coset.Basic
/-- An equivalence between any non-empty fiber of an `AddMonoidHom` and its kernel.  -/
AddMonoidHom.fiberEquivKer : {α : Type u_1} →
  [inst : AddGroup α] → {H : Type u_2} → [inst_1 : AddGroup H] → (f : α →+ H) → (a : α) → ↑(⇑f ⁻¹' {f a}) ≃ ↥f.ker
-- Mathlib.Data.Finset.Card
Finset.card_union : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s ∪ t).card = s.card + t.card - (s ∩ t).card
-- Init.Data.Float.Model.Unpacked.Operations.ToNat
/-- Converts an `UnpackedFloat` to a `UInt64`, truncating after the decimal point, sending `NaN` to
`0` and clamping out-of-range values and infinities.
 -/
Float.Model.UnpackedFloat.toUInt64 : Float.Model.UnpackedFloat → UInt64
-- Mathlib.FieldTheory.PerfectClosure
_private.Mathlib.FieldTheory.PerfectClosure.0.PerfectClosure.mul_aux_left : ∀ (K : Type u) [inst : CommRing K] (p : ℕ) [inst_1 : Fact (Nat.Prime p)] [inst_2 : CharP K p] (x1 x2 y : ℕ × K),
  PerfectClosure.R K p x1 x2 →
    PerfectClosure.mk K p (x1.1 + y.1, (⇑(frobenius K p))^[y.1] x1.2 * (⇑(frobenius K p))^[x1.1] y.2) =
      PerfectClosure.mk K p (x2.1 + y.1, (⇑(frobenius K p))^[y.1] x2.2 * (⇑(frobenius K p))^[x2.1] y.2)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableUniformlyOn.multipliable : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {x : β} {s : Set β}
  [inst_1 : UniformSpace α], MultipliableUniformlyOn f s → x ∈ s → Multipliable fun x_1 => f x_1 x
-- Lean.Elab.Match
/-- When visiting an assigned metavariable, if it has an user-name. We save it here.
We want to preserve these user-names when generating new pattern variables.  -/
Lean.Elab.Term.ToDepElimPattern.Context.userName : Lean.Elab.Term.ToDepElimPattern.Context → Lean.Name
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Syntactic typeclass for types endowed with an inner product  -/
Inner : Type u_4 → Type u_5 → Type (max u_4 u_5)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataAsCoalgebra
CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso_hom_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F :
    CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ)
      (CategoryTheory.Bicategory.Adj CategoryTheory.Cat)}
  (ι : Type u_2) [inst_1 : Unique ι] {X S : C} (f : X ⟶ S) (X_1 : ↑(F.obj { as := Opposite.op S }).obj),
  ((CategoryTheory.Pseudofunctor.toDescentDataAsCoalgebraCompCoalgebraEquivalenceFunctorIso ι f).hom.app X_1).f =
    CategoryTheory.CategoryStruct.id ((F.map f.op.toLoc).l.toFunctor.obj X_1)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.linearOrderOverring : {K : Type u} → [inst : Field K] → (A : ValuationSubring K) → LinearOrder { S // A ≤ S }
-- Mathlib.AlgebraicTopology.SimplicialSet.Nerve
/-- The 0-simplices of the nerve of a category are equivalent to the objects of the category.  -/
CategoryTheory.nerveEquiv : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.ComposableArrows C 0 ≃ C
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.smul_iUnion₂ : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} {κ : ι → Sort u_6} [inst : SMul α β] (s : Set α)
  (t : (i : ι) → κ i → Set β), s • ⋃ i, ⋃ j, t i j = ⋃ i, ⋃ j, s • t i j
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.isNotG2_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N)
  [inst_5 : P.IsCrystallographic] [P.IsReduced] [P.IsIrreducible],
  P.IsNotG2 ↔ ∀ (i j : ι), P.pairingIn ℤ i j ∈ {-2, -1, 0, 1, 2}
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.forIn_eq_forIn_toList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {δ : Type w}
  {m' : Type w → Type w'} [inst_2 : Monad m'] [LawfulMonad m'] {f : (a : α) × β a → δ → m' (ForInStep δ)} {init : δ},
  m.WF → forIn m init f = forIn m.toList init f
-- Mathlib.Algebra.Group.Action.Equidecomp
Equidecomp.mk.inj : ∀ {X : Type u_1} {G : Type u_2} {inst : SMul G X} {toPartialEquiv : PartialEquiv X X}
  {isDecompOn' : ∃ S, Equidecomp.IsDecompOn (↑toPartialEquiv) toPartialEquiv.source S}
  {toPartialEquiv_1 : PartialEquiv X X}
  {isDecompOn'_1 : ∃ S, Equidecomp.IsDecompOn (↑toPartialEquiv_1) toPartialEquiv_1.source S},
  { toPartialEquiv := toPartialEquiv, isDecompOn' := isDecompOn' } =
      { toPartialEquiv := toPartialEquiv_1, isDecompOn' := isDecompOn'_1 } →
    toPartialEquiv = toPartialEquiv_1
-- Mathlib.Tactic.Widget.StringDiagram
/-- The horizontal position of the node in the string diagram, counting strings in domains.  -/
Mathlib.Tactic.Widget.StringDiagram.IdNode.hPosSrc : Mathlib.Tactic.Widget.StringDiagram.IdNode → ℕ
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_inter_le_size_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp],
  (t₁ ∩ t₂).size ≤ t₂.size
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → ∀ (f : α → Bool), (Std.TreeSet.Raw.filter f t₁).Equiv (Std.TreeSet.Raw.filter f t₂)
-- Mathlib.Order.Heyting.Hom
/-- The type of bi-Heyting homomorphisms from `α` to `β`. Bounded lattice homomorphisms that
preserve Heyting implication and difference.  -/
BiheytingHom : (α : Type u_6) → (β : Type u_7) → [BiheytingAlgebra α] → [BiheytingAlgebra β] → Type (max u_6 u_7)
-- Mathlib.GroupTheory.OrderOfElement
Nat.Coprime.orderOf_pow : ∀ {G : Type u_1} [inst : Monoid G] {y : G} {m : ℕ}, (orderOf y).Coprime m → orderOf (y ^ m) = orderOf y
-- Mathlib.Data.Nat.Fib.Basic
/-- Computes `Nat.fib n` using the binary representation of `n`.
Proved to be equal to `Nat.fib` in `Nat.fast_fib_eq`.  -/
Nat.fastFib : ℕ → ℕ
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformAddGroup.rightUniformSpace_eq : ∀ {G : Type u_2} [u : UniformSpace G] [inst : AddGroup G] [inst_1 : IsUniformAddGroup G],
  IsTopologicalAddGroup.rightUniformSpace G = u
-- Mathlib.Tactic.Module
/-- Operate on a `Module.NF S M` object `l`, i.e. a list of pairs in `S × M`, where `S` is some
commutative semiring, by applying to each `S`-component the algebra-map from `S` into a specified
`S`-algebra `R`.  -/
Mathlib.Tactic.Module.NF.algebraMap : {S : Type u_1} →
  (R : Type u_2) →
    {M : Type u_3} →
      [inst : CommSemiring S] →
        [inst_1 : Semiring R] → [Algebra S R] → Mathlib.Tactic.Module.NF S M → Mathlib.Tactic.Module.NF R M
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
/-- The map from the mixed space to `logSpace K` defined in such way that: 1) it factors the map
`logEmbedding`, see `logMap_eq_logEmbedding`; 2) it is constant on the sets
`{c • x | c ∈ ℝ, c ≠ 0}` if `norm x ≠ 0`, see `logMap_real_smul`.  -/
NumberField.mixedEmbedding.logMap : {K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] →
      NumberField.mixedEmbedding.mixedSpace K → NumberField.Units.dirichletUnitTheorem.logSpace K
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- For an `m × n` `α`-matrix `A`, `A.col j` is the `j`th column of `A` as a vector in `m → α`.
`A.col` is defeq to `Aᵀ`, but refers to the 'column function' of `A`
while avoiding defeq abuse and noisy eta-expansions
(and without the simplifier unfolding transposes) in expressions like `Set.Injective A.col`
and `Set.range A.col`.
(Note 2025-04-07 : the identifier `Matrix.col` used to refer to a matrix with all columns equal;
this is now called `Matrix.replicateCol`)  -/
Matrix.col : {m : Type u_2} → {n : Type u_3} → {α : Type v} → Matrix m n α → n → m → α
-- ProofWidgets.Presentation.Expr
ProofWidgets.ExprPresenter.mk.sizeOf_spec : ∀ (userName : String) (layoutKind : ProofWidgets.LayoutKind) (present : Lean.Expr → Lean.MetaM ProofWidgets.Html),
  sizeOf { userName := userName, layoutKind := layoutKind, present := present } =
    1 + sizeOf userName + sizeOf layoutKind
-- Mathlib.Analysis.Complex.ValueDistribution.Proximity.IntegralPresentation
/-- For every function `f : ℂ → ℂ`, the Cartan kernel of integration `cartanKernel f R α β` is
integrable as a function in `α`.
 -/
ValueDistribution.Cartan.integrableOn_cartanKernel_left : ∀ (f : ℂ → ℂ) (R β : ℝ),
  MeasureTheory.IntegrableOn (fun x => ValueDistribution.Cartan.cartanKernel f R x β) (Set.Ioc 0 (2 * Real.pi))
    MeasureTheory.volume
-- Lean.Elab.Declaration
Lean.Elab.Command.elabMutual : Lean.Elab.Command.CommandElab
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- If an alternating map in finitely many variables on a seminormed space is continuous,
then it satisfies the inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖`,
for some `C` which can be chosen to be positive.  -/
AlternatingMap.exists_bound_of_continuous : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F),
  Continuous ⇑f → ∃ C, 0 < C ∧ ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖
-- Mathlib.GroupTheory.GroupAction.Hom
MulDistribMulActionHom.toFun_eq_coe : ∀ {M : Type u_1} [inst : Monoid M] {N : Type u_2} [inst_1 : Monoid N] {φ : M →* N} {A : Type u_4} [inst_2 : Monoid A]
  [inst_3 : MulDistribMulAction M A] {B : Type u_5} [inst_4 : Monoid B] [inst_5 : MulDistribMulAction N B]
  (f : A →ₑ*[φ] B), f.toFun = ⇑f
-- Mathlib.Order.Filter.Pointwise
/-- Repeated pointwise multiplication (not the same as pointwise repeated multiplication!) of a
`Filter`. See Note [pointwise nat action].  -/
Filter.instNPow : {α : Type u_2} → [One α] → [Mul α] → Pow (Filter α) ℕ
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.equiv_push : ∀ {a b : ℕ} {self : Batteries.UnionFind}, self.push.Equiv a b ↔ self.Equiv a b
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqDiagnosticTag : BEq Lean.Lsp.DiagnosticTag
-- Mathlib.Topology.Semicontinuity.Basic
/-- The sum of two upper semicontinuous functions is upper semicontinuous. Formulated with an
explicit continuity assumption on addition, for application to `EReal`. The unprimed version of
the lemma uses `[ContinuousAdd]`.  -/
UpperSemicontinuousAt.add' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_5} [inst_1 : AddCommMonoid γ] [inst_2 : LinearOrder γ]
  [IsOrderedAddMonoid γ] [inst_4 : TopologicalSpace γ] [OrderTopology γ] {f g : α → γ},
  UpperSemicontinuousAt f x →
    UpperSemicontinuousAt g x →
      ContinuousAt (fun p => p.1 + p.2) (f x, g x) → UpperSemicontinuousAt (fun z => f z + g z) x
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.serreDerivative_eq : ∀ (k : ℂ) (F : UpperHalfPlane → ℂ),
  Derivative.serreDerivative k F = fun z =>
    Derivative.normalizedDerivOfComplex F z - k * 12⁻¹ * EisensteinSeries.E2 z * F z
-- Mathlib.Data.List.PeriodicityLemma
List.HasPeriod.drop_prefix : ∀ {α : Type u_1} {w : List α} (p : ℕ), w.HasPeriod p → List.drop p w <+: w
-- Lean.Widget.TaggedText
Lean.Widget.TaggedText.brecOn_2.eq : ∀ {α : Type u} {motive_1 : Lean.Widget.TaggedText α → Sort u_1} {motive_2 : Array (Lean.Widget.TaggedText α) → Sort u_1}
  {motive_3 : List (Lean.Widget.TaggedText α) → Sort u_1} (t : List (Lean.Widget.TaggedText α))
  (F_1 : (t : Lean.Widget.TaggedText α) → t.below → motive_1 t)
  (F_2 : (t : Array (Lean.Widget.TaggedText α)) → Lean.Widget.TaggedText.below_1 t → motive_2 t)
  (F_3 : (t : List (Lean.Widget.TaggedText α)) → Lean.Widget.TaggedText.below_2 t → motive_3 t),
  Lean.Widget.TaggedText.brecOn_2 t F_1 F_2 F_3 = F_3 t (Lean.Widget.TaggedText.brecOn_2.go t F_1 F_2 F_3).2
-- Mathlib.NumberTheory.NumberField.Units.Basic
NumberField.Units.torsionOrder.eq_1 : ∀ (K : Type u_1) [inst : Field K], NumberField.Units.torsionOrder K = Nat.card ↥(NumberField.Units.torsion K)
-- Init.Data.String.Basic
List.data_asString : ∀ {l : List Char}, (String.ofList l).toList = l
-- Batteries.Recycling.RBTree.Basic
_private.Batteries.Recycling.RBTree.Basic.0.RBTree.RBNode.balLeft.match_4.eq_2 : ∀ {α : Type u_1} (motive : RBTree.RBNode α → Sort u_2) (l : RBTree.RBNode α)
  (h_1 : (a : RBTree.RBNode α) → (x : α) → (b : RBTree.RBNode α) → motive (RBTree.RBNode.node RBTree.RBColor.red a x b))
  (h_2 : (l : RBTree.RBNode α) → motive l),
  (∀ (a : RBTree.RBNode α) (x : α) (b : RBTree.RBNode α), l = RBTree.RBNode.node RBTree.RBColor.red a x b → False) →
    (match l with
      | RBTree.RBNode.node RBTree.RBColor.red a x b => h_1 a x b
      | l => h_2 l) =
      h_2 l
-- Mathlib.Computability.NFA
NFA.Path.supp.eq_2 : ∀ {α : Type u} {σ : Type v} {M : NFA α σ} [inst : DecidableEq σ] {s t : σ} (t_3 : σ) (a : α) (x_3 : List α)
  (p : M.Path t_3 t x_3) (a_1 : t_3 ∈ M.step s a), (NFA.Path.cons t_3 s t a x_3 a_1 p).supp = {s} ∪ p.supp
-- Mathlib.GroupTheory.Index
AddSubgroup.index_map_equiv : ∀ {G : Type u_1} {G' : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup G'] (H : AddSubgroup G) (e : G ≃+ G'),
  (AddSubgroup.map (↑e) H).index = H.index
-- Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
Measurable.comp_eventuallyMeasurable : ∀ {α : Type u_1} {m : MeasurableSpace α} {l : Filter α} [inst : CountableInterFilter l] {β : Type u_2} {γ : Type u_3}
  [inst_1 : MeasurableSpace β] [inst_2 : MeasurableSpace γ] {f : α → β} {h : β → γ},
  Measurable h → EventuallyMeasurable m l f → EventuallyMeasurable m l (h ∘ f)
-- Mathlib.Analysis.RCLike.Inner
RCLike.linearIndependent_of_ne_zero_of_wInner_one_eq_zero : ∀ {ι : Type u_1} {κ : Type u_2} {𝕜 : Type u_3} [inst : Fintype ι] [inst_1 : RCLike 𝕜] {f : κ → ι → 𝕜},
  (∀ (k : κ), f k ≠ 0) → (Pairwise fun k₁ k₂ => ⟪f k₁, f k₂⟫_[𝕜] = 0) → LinearIndependent 𝕜 f
-- Batteries.Data.Random.MersenneTwister
/-- Current data index.  -/
Batteries.Random.MersenneTwister.State.index : {cfg : Batteries.Random.MersenneTwister.Config} → Batteries.Random.MersenneTwister.State cfg → Fin cfg.stateSize
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.injOn_cos : Set.InjOn Real.cos (Set.Icc 0 Real.pi)
-- Mathlib.LinearAlgebra.Pi
/-- `Equiv.piCurry` as a `LinearEquiv`.  -/
LinearEquiv.piCurry : (R : Type u) →
  [inst : Semiring R] →
    {ι : Type u_4} →
      {κ : ι → Type u_5} →
        (α : (i : ι) → κ i → Type u_6) →
          [inst_1 : (i : ι) → (k : κ i) → AddCommMonoid (α i k)] →
            [inst_2 : (i : ι) → (k : κ i) → Module R (α i k)] →
              ((i : Sigma κ) → α i.fst i.snd) ≃ₗ[R] (i : ι) → (j : κ i) → α i j
-- Mathlib.AlgebraicGeometry.Sites.QuasiCompact
AlgebraicGeometry.Scheme.bot_mem_qcPrecoverage : ∀ (X : AlgebraicGeometry.Scheme) [IsEmpty ↥X], ⊥ ∈ AlgebraicGeometry.Scheme.qcPrecoverage.coverings X