mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.MLList.Basic
/-- Extract a list inside the monad from a `MLList`.  -/
MLList.force : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → m (List α)
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Ref.invert : {α : Type} → [inst : Hashable α] → [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → aig.Ref → Bool
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.ToForInTermResult.mk.sizeOf_spec : ∀ (uvars : Array Lean.Elab.Term.Do.Var) (term : Lean.Syntax),
  sizeOf { uvars := uvars, term := term } = 1 + sizeOf uvars + sizeOf term
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
stronglyMeasurable_const_smul_iff : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {G : Type u_6} [inst : TopologicalSpace β] [inst_1 : Group G]
  [inst_2 : MulAction G β] [ContinuousConstSMul G β] {m : MeasurableSpace α} (c : G),
  (MeasureTheory.StronglyMeasurable fun x => c • f x) ↔ MeasureTheory.StronglyMeasurable f
-- Mathlib.FieldTheory.PurelyInseparable.Tower
/-- If `K / E / F` is a field extension tower, such that `E / F` is algebraic, then their
inseparable degrees satisfy the tower law: $[E:F]_i [K:E]_i = [K:F]_i$.  -/
Field.lift_insepDegree_mul_lift_insepDegree_of_isAlgebraic : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (K : Type w) [inst_3 : Field K]
  [inst_4 : Algebra F K] [inst_5 : Algebra E K] [IsScalarTower F E K] [Algebra.IsAlgebraic F E],
  Cardinal.lift.{w, v} (Field.insepDegree F E) * Cardinal.lift.{v, w} (Field.insepDegree E K) =
    Cardinal.lift.{v, w} (Field.insepDegree F K)
-- Mathlib.Data.Multiset.FinsetOps
Multiset.dedup_cons : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s : Multiset α}, (a ::ₘ s).dedup = Multiset.ndinsert a s.dedup
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiff.continuous : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {n : WithTop ℕ∞},
  ContMDiff I I' n f → Continuous f
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.isBlock_iff_smul_eq_of_mem : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] {B : Set X},
  MulAction.IsBlock G B ↔ ∀ ⦃g : G⦄ ⦃a : X⦄, a ∈ B → g • a ∈ B → g • B = B
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- A rational function `c` that satisfies `c * φ = Φ`. This is `ν₀(x)` in Cohn's notation.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.c : {K : Type u_1} → [inst : Field K] → IntermediateField K (RatFunc K) → RatFunc K
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- The zero complex  -/
HomologicalComplex.zero : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → [CategoryTheory.Limits.HasZeroObject V] → HomologicalComplex V c
-- Mathlib.CategoryTheory.Limits.Shapes.Countable
CategoryTheory.Limits.hasFiniteProducts_of_hasCountableProducts : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.Limits.HasCountableProducts C],
  CategoryTheory.Limits.HasFiniteProducts C
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.ne_zero_of_degree_ge_degree : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.degree ≤ q.degree → p ≠ 0 → q ≠ 0
-- Lean.Exception
Lean.MonadRecDepth : (Type → Type) → Type 1
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.instMonadShareCommonOfMonadLift : (m n : Type → Type) →
  [MonadLift m n] → [Lean.Meta.Sym.Internal.MonadShareCommon m] → Lean.Meta.Sym.Internal.MonadShareCommon n
-- Init.Grind.Config
Lean.Grind.ConfigInteractive.mk.inj : ∀ {toConfig toConfig_1 : Lean.Grind.Config},
  { toConfig := toConfig } = { toConfig := toConfig_1 } → toConfig = toConfig_1
-- Lean.Data.AssocList
Lean.List.toAssocList' : {α : Type u} → {β : Type v} → List (α × β) → Lean.AssocList α β
-- Init.GetElem
Fin.instGetElem?FinVal : {cont : Type u_1} →
  {elem : Type u_2} →
    {dom : cont → ℕ → Prop} → {n : ℕ} → [GetElem? cont ℕ elem dom] → GetElem? cont (Fin n) elem fun xs i => dom xs ↑i
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.IsCardinalPresentable.exists_eq_of_isColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular]
  {J : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} J] [CategoryTheory.IsCardinalPresentable X κ]
  [CategoryTheory.EssentiallySmall.{w, v_1, u_1} J] [CategoryTheory.IsCardinalFiltered J κ]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} (hc : CategoryTheory.Limits.IsColimit c)
  {i₁ i₂ : J} (f₁ : X ⟶ F.obj i₁) (f₂ : X ⟶ F.obj i₂),
  CategoryTheory.CategoryStruct.comp f₁ (c.ι.app i₁) = CategoryTheory.CategoryStruct.comp f₂ (c.ι.app i₂) →
    ∃ j u v, CategoryTheory.CategoryStruct.comp f₁ (F.map u) = CategoryTheory.CategoryStruct.comp f₂ (F.map v)
-- Mathlib.Topology.Constructions
IsClopen.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X), IsClopen s = (IsClosed s ∧ IsOpen s)
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.isIso_homologyMap_τ₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S₁ S₂ : CategoryTheory.ShortComplex (HomologicalComplex C c)} (φ : S₁ ⟶ S₂),
  S₁.ShortExact →
    S₂.ShortExact →
      ∀ (i : ι),
        CategoryTheory.Epi (HomologicalComplex.homologyMap φ.τ₁ i) →
          CategoryTheory.IsIso (HomologicalComplex.homologyMap φ.τ₂ i) →
            (∀ (j : ι), c.Rel i j → CategoryTheory.IsIso (HomologicalComplex.homologyMap φ.τ₁ j)) →
              (∀ (j : ι), c.Rel i j → CategoryTheory.Mono (HomologicalComplex.homologyMap φ.τ₂ j)) →
                CategoryTheory.IsIso (HomologicalComplex.homologyMap φ.τ₃ i)
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- The difference `s -ₒ 0` as an additive unit.  -/
AddOreLocalization.numeratorAddUnit : {R : Type u_1} →
  [inst : AddMonoid R] →
    {S : AddSubmonoid R} → [inst_1 : AddOreLocalization.AddOreSet S] → ↥S → AddUnits (AddOreLocalization S R)
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.exists_isCycle_of_two_le_isEdgeReachable : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, u ≠ v → ∀ {n : ℕ}, 2 ≤ n → G.IsEdgeReachable n u v → ∃ w, w.IsCycle
-- Mathlib.Probability.Kernel.WithDensity
ProbabilityTheory.Kernel.withDensity_one' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (κ : ProbabilityTheory.Kernel α β)
  [inst : ProbabilityTheory.IsSFiniteKernel κ], (κ.withDensity fun x x_1 => 1) = κ
-- Mathlib.RingTheory.Perfection
/-- For a field `K` with valuation `v : K → ℝ≥0` and ring of integers `O`,
a function `O/(p) → ℝ≥0` that sends `0` to `0` and `x + (p)` to `v(x)` as long as `x ∉ (p)`.  -/
ModP.preVal : (K : Type u₁) →
  [inst : Field K] →
    Valuation K NNReal → (O : Type u₂) → [inst_1 : CommRing O] → [Algebra O K] → (p : ℕ) → ModP O p → NNReal
-- Mathlib.Topology.Order.IntermediateValue
isPreconnected_Icc_aux : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {a b : α} (x y : α) (s t : Set α),
  x ≤ y →
    IsClosed s →
      IsClosed t → Set.Icc a b ⊆ s ∪ t → x ∈ Set.Icc a b ∩ s → y ∈ Set.Icc a b ∩ t → (Set.Icc a b ∩ (s ∩ t)).Nonempty
-- Mathlib.Order.Filter.Cofinite
Function.update_eventuallyEq_cofinite : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] (f : α → β) (a : α) (b : β),
  Function.update f a b =ᶠ[Filter.cofinite] f
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Monomorphisms
CategoryTheory.IsGrothendieckAbelian.instIsStableUnderTransfiniteCompositionMonomorphisms : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [CategoryTheory.IsGrothendieckAbelian.{w, v, u} C],
  (CategoryTheory.MorphismProperty.monomorphisms C).IsStableUnderTransfiniteComposition
-- Mathlib.Algebra.Order.Interval.Set.Group
Set.add_mem_Icc_iff_left : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] {a b c d : α},
  a + b ∈ Set.Icc c d ↔ a ∈ Set.Icc (c - b) (d - b)
-- Mathlib.Algebra.MvPolynomial.Division
MvPolynomial.monomial_one_dvd_iff_modMonomial_eq_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {i : σ →₀ ℕ} {x : MvPolynomial σ R},
  (MvPolynomial.monomial i) 1 ∣ x ↔ x.modMonomial i = 0
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instReprOrdinal : Repr Std.Time.Weekday.Ordinal
-- Batteries.Data.HashMap.Basic
Batteries.HashMap.instGetElemOptionTrue : {α : Type u_1} →
  {x : BEq α} → {x_1 : Hashable α} → {β : Type u_2} → GetElem (Batteries.HashMap α β) α (Option β) fun x x_2 => True
-- Mathlib.Geometry.Manifold.SmoothEmbedding
/-- Given `C^n` manifolds `M` and `N`, `Sum.inr : N → M ⊕ N` is a `C^n` embedding.  -/
Manifold.IsSmoothEmbedding.sumInr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E₁ : Type u_2} [inst_1 : NormedAddCommGroup E₁]
  [inst_2 : NormedSpace 𝕜 E₁] {H : Type u_6} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E₁ H} {M : Type u_10}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞} {M' : Type u_14}
  [inst_6 : TopologicalSpace M'] [inst_7 : ChartedSpace H M'] [IsManifold I n M] [IsManifold I n M'],
  Manifold.IsSmoothEmbedding I I n Sum.inr
-- Mathlib.GroupTheory.Congruence.Defs
/-- For additive congruence relations `c, d` on a type `M` with an addition, `c ≤ d`
iff `∀ x y ∈ M`, `x` is related to `y` by `d` if `x` is related to `y` by `c`.  -/
AddCon.instLE : {M : Type u_1} → [inst : Add M] → LE (AddCon M)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.radical_mono : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, I ≤ J → I.radical ≤ J.radical
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.maxEntryD.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3) (size : ℕ)
  (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (x : α × β)
  (h_1 : (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      (fallback : α × β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1),
      fallback => h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h fallback) =
    h_2 size k v l x
-- Init.Data.BitVec.Bitblast
/-- In the shift subtract input, the dividend is at least one bit long (`wn > 0`), so
the remainder has bits to be computed (`wr < w`).
 -/
BitVec.DivModState.wr_lt_w : ∀ {w : ℕ} {args : BitVec.DivModArgs w} {qr : BitVec.DivModState w}, BitVec.DivModState.Poised args qr → qr.wr < w
-- Mathlib.Analysis.Real.Sqrt
Real.sqrt_div_self : ∀ {x : ℝ}, √x / x = (√x)⁻¹
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_inv_log : ∀ {x : ℝ}, 0 < x → x ≠ 1 → x ^ (Real.log x)⁻¹ = Real.exp 1
-- Mathlib.Analysis.Convex.Jensen
/-- **Minimum principle** for concave functions on a segment. If a function `f` is concave on the
segment `[x, y]`, then the eventual minimum of `f` on `[x, y]` is at `x` or `y`.  -/
ConcaveOn.min_le_of_mem_segment : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : LinearOrder β] [IsOrderedAddMonoid β]
  [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β} {x y z : E},
  ConcaveOn 𝕜 s f → x ∈ s → y ∈ s → z ∈ segment 𝕜 x y → min (f x) (f y) ≤ f z
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
SemimoduleCat.MonoidalCategory.triangle : ∀ {R : Type u} [inst : CommSemiring R] (M N : SemimoduleCat R),
  CategoryTheory.CategoryStruct.comp (SemimoduleCat.MonoidalCategory.associator M (SemimoduleCat.of R R) N).hom
      (SemimoduleCat.MonoidalCategory.tensorHom (CategoryTheory.CategoryStruct.id M)
        (SemimoduleCat.MonoidalCategory.leftUnitor N).hom) =
    SemimoduleCat.MonoidalCategory.tensorHom (SemimoduleCat.MonoidalCategory.rightUnitor M).hom
      (CategoryTheory.CategoryStruct.id N)
-- Init.Coe
/-- Coerces a value of type `α` to `β`, which must be a universe.  -/
CoeSort.coe : {α : Sort u} → {β : outParam (Sort v)} → [self : CoeSort α β] → α → β
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.comap_coe_nhds : ∀ {X : Type u_1} [inst : TopologicalSpace X] (x : X), Filter.comap OnePoint.some (nhds ↑x) = nhds x
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_smul : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] (φ : MvPolynomial σ R) (r : R), ↑(r • φ) = r • ↑φ
-- Init.Data.Vector.Nat
Vector.prod_replicate_nat : ∀ {n a : ℕ}, (Vector.replicate n a).prod = a ^ n
-- Std.Http.Protocol.H1.Parser
/-- Parses the trailer section that follows the last chunk size line (`0\r\n`).
 -/
Std.Http.Protocol.H1.parseLastChunkBody : Std.Http.Protocol.H1.Config → Std.Internal.Parsec.ByteArray.Parser Unit
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get!_inter_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {k : α}, k ∉ t₁ → Std.DTreeMap.Const.get! (t₁ ∩ t₂) k = default
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.subset_sdiff_singleton`. -/
Set.subset_diff_singleton : ∀ {α : Type u_1} {s t : Set α} {a : α}, s ⊆ t → a ∉ s → s ⊆ t \ {a}
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
/-- `nthRoot n a ^ n ≤ a` unless both `n` and `a` are zeros.  -/
Nat.pow_nthRoot_le_iff : ∀ {n a : ℕ}, n.nthRoot a ^ n ≤ a ↔ n ≠ 0 ∨ a ≠ 0
-- Lean.Widget.UserWidget
Lean.Widget.evalModule : Lean.Expr → Lean.MetaM Lean.Widget.Module
-- Mathlib.CategoryTheory.Limits.Shapes.DisjointCoproduct
CategoryTheory.Limits.CoproductsOfShapeDisjoint.coproductDisjoint : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {ι : Type u_2}
  [self : CategoryTheory.Limits.CoproductsOfShapeDisjoint C ι] (X : ι → C), CategoryTheory.Limits.CoproductDisjoint X
-- Mathlib.Algebra.Module.Torsion.Basic
/-- The submodule containing all elements `x` of `M` such that `a • x = 0` for all `a` in `s`.  -/
Submodule.torsionBySet : (R : Type u_1) →
  (M : Type u_2) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → Set R → Submodule R M
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
instTopologicalSpaceTangentBundle : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {M : Type u_6} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] → [IsManifold I 1 M] → TopologicalSpace (TangentBundle I M)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.Basic
/-- The normalised level 1 Eisenstein series of weight 4.  -/
ModularForm.E₄ : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 4
-- Mathlib.Algebra.Group.End
/-- **Alias** of `AddAut.neg_apply_self`. -/
AddAut.inv_apply_self : ∀ (M : Type u_2) [inst : Add M] (e : AddAut M) (m : M), (-e) (e m) = m
-- Mathlib.Order.RelIso.Basic
/-- The underlying function of a `RelHom`  -/
RelHom.toFun : {α : Type u_5} → {β : Type u_6} → {r : α → α → Prop} → {s : β → β → Prop} → r →r s → α → β
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_sub_one' : ∀ {x y : ℝ}, 0 ≤ x → y - 1 ≠ 0 → x ^ (y - 1) = x ^ y / x
-- Mathlib.LinearAlgebra.Matrix.Echelon.Decomposition
/-- A certificate of an echelon form decomposition of `A`, certifying that
`L * (A.submatrix σ id)` is in echelon form by providing a pivot, where `L`
is lower triangular with nonzero diagonal, and `σ` the permutation on the rows
of `A`.
This version does not store the final echelon form itself as it can be computed
by the data enclosed.
 -/
Echelon.Decomposition : {m : Type u_1} →
  [Fintype m] →
    [LinearOrder m] →
      {n : Type u_2} → [LinearOrder n] → {R : Type u_3} → [CommRing R] → Matrix m n R → Type (max (max u_1 u_2) u_3)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.fderivCLM_apply_of_gt : ∀ (𝕜 : 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] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n k : ℕ∞} {K : TopologicalSpace.Compacts E} (f : ContDiffMapSupportedIn E F n K),
  n < k + 1 → (ContDiffMapSupportedIn.fderivCLM 𝕜 n k) f = 0
-- Init.Data.UInt.Lemmas
USize.toUInt64_sub : ∀ (a b : USize), (a - b).toUInt64 = (a.toUInt64 - b.toUInt64) % UInt64.ofNat USize.size
-- Mathlib.Algebra.Pointwise.Stabilizer
AddAction.vadd_set_stabilizer_subset : ∀ {G : Type u_1} [inst : AddCommGroup G] {s : Set G} {a : G}, a ∈ s → a +ᵥ ↑(AddAction.stabilizer G s) ⊆ s
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.map.congr_simp : ∀ {R : Type u} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {M : Type v} {N : Type w}
  (g g_1 : M → N),
  g = g_1 →
    ∀ (f f_1 : Convexity.StdSimplex R M), f = f_1 → Convexity.StdSimplex.map g f = Convexity.StdSimplex.map g_1 f_1
-- Mathlib.CategoryTheory.Category.ReflQuiv
/-- The functor sending a reflexive quiver to the free category it generates, a quotient of
its path category  -/
CategoryTheory.Cat.freeRefl : CategoryTheory.Functor CategoryTheory.ReflQuiv CategoryTheory.Cat
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.uset.inj : ∀ {x : Lean.IR.VarId} {i : ℕ} {y : Lean.IR.VarId} {b : Lean.IR.FnBody} {x_1 : Lean.IR.VarId} {i_1 : ℕ}
  {y_1 : Lean.IR.VarId} {b_1 : Lean.IR.FnBody},
  Lean.IR.FnBody.uset x i y b = Lean.IR.FnBody.uset x_1 i_1 y_1 b_1 → x = x_1 ∧ i = i_1 ∧ y = y_1 ∧ b = b_1
-- Init.Data.Nat.Div.Basic
Nat.div_mul_le_self : ∀ (m n : ℕ), m / n * n ≤ m
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.of_mul_right_left : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsRelPrime x (y * z) → IsRelPrime x y
-- Mathlib.Data.Multiset.Antidiagonal
Multiset.antidiagonal_zero : ∀ {α : Type u_1}, Multiset.antidiagonal 0 = {(0, 0)}
-- Mathlib.Topology.Algebra.Module.Equiv
/-- Continuous linear equivalences between modules. We only put the type classes that are necessary
for the definition, although in applications `M` and `M₂` will be topological modules over the
topological semiring `R`.  -/
ContinuousLinearEquiv : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : Semiring S] →
        (σ : R →+* S) →
          {σ' : S →+* R} →
            [RingHomInvPair σ σ'] →
              [RingHomInvPair σ' σ] →
                (M : Type u_3) →
                  [TopologicalSpace M] →
                    [inst_5 : AddCommMonoid M] →
                      (M₂ : Type u_4) →
                        [TopologicalSpace M₂] →
                          [inst_7 : AddCommMonoid M₂] → [Module R M] → [Module S M₂] → Type (max u_3 u_4)
-- Mathlib.CategoryTheory.Enriched.Opposite
/-- When composing a tensor product of morphisms with the `V`-composition morphism in `Cᵒᵖ`,
this re-writes the `V`-composition to be in `C` and moves the braiding to the left.  -/
CategoryTheory.tensorHom_eComp_op_eq : ∀ (V : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} V] [inst_1 : CategoryTheory.MonoidalCategory V]
  [inst_2 : CategoryTheory.BraidedCategory V] {C : Type u} [inst_3 : CategoryTheory.EnrichedCategory V C] {x y z : Cᵒᵖ}
  {v w : V} (f : v ⟶ z ⟶[V] y) (g : w ⟶ y ⟶[V] x),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f g)
      (CategoryTheory.eComp V z y x) =
    CategoryTheory.CategoryStruct.comp (β_ v w).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom g f)
        (CategoryTheory.eComp V (Opposite.unop x) (Opposite.unop y) (Opposite.unop z)))
-- Mathlib.GroupTheory.MonoidLocalization.Basic
AddSubmonoid.LocalizationMap.instFunLike.eq_1 : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N],
  AddSubmonoid.LocalizationMap.instFunLike = { coe := fun f => ⇑f.toAddMonoidHom, coe_injective := ⋯ }
-- Init.Data.Ord.Basic
/-- Constructs the lexicographic order on products `α × β` from orders for `α` and `β`.
 -/
Ord.lex : {α : Type u_1} → {β : Type u_2} → Ord α → Ord β → Ord (α × β)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RciSliceData.mk : {α : Type u} →
  {β : Type v} →
    [inst : Ord α] →
      (Std.DTreeMap.Internal.Impl α fun x => β) → Std.Rci α → Std.DTreeMap.Internal.Const.RciSliceData α β
-- Std.Http.Data.Body.Empty
Std.Http.Body.instInhabitedEmpty : Inhabited Std.Http.Body.Empty
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.IsPredictable.martingalePart_eq : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0}
  [MeasureTheory.SigmaFiniteFiltration μ ℱ],
  MeasureTheory.IsStronglyPredictable ℱ f →
    (∀ (n : ℕ), MeasureTheory.Integrable (f n) μ) → ∀ (n : ℕ), MeasureTheory.martingalePart f ℱ μ n =ᵐ[μ] f 0
-- Lean.Language.Basic
/-- Non-interactive message log.  -/
Lean.Language.Snapshot.Diagnostics.msgLog : Lean.Language.Snapshot.Diagnostics → Lean.MessageLog
-- Mathlib.RingTheory.WittVector.Verschiebung
/-- `WittVector.verschiebung` is a polynomial function.  -/
WittVector.verschiebung_isPoly : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], WittVector.IsPoly p fun x x_1 => ⇑WittVector.verschiebung
-- Mathlib.Data.Nat.Factorization.Basic
Nat.factorization_gcd : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → (a.gcd b).factorization = a.factorization ⊓ b.factorization