mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Martingale.Basic
/-- A predictable supermartingale is a.e. less than or equal to its initial state.  -/
MeasureTheory.Supermartingale.le_zero_of_predictable : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {𝒢 : MeasureTheory.Filtration ℕ m0} [inst_2 : Preorder E]
  [MeasureTheory.SigmaFiniteFiltration μ 𝒢] {f : ℕ → Ω → E},
  MeasureTheory.Supermartingale f 𝒢 μ → (MeasureTheory.StronglyAdapted 𝒢 fun n => f (n + 1)) → ∀ (n : ℕ), f n ≤ᵐ[μ] f 0
-- Mathlib.Order.Filter.EventuallyConst
Filter.eventuallyConst_atTop_nat : ∀ {α : Type u_1} {f : ℕ → α}, Filter.EventuallyConst f Filter.atTop ↔ ∃ n, ∀ (m : ℕ), n ≤ m → f (m + 1) = f m
-- Init.Data.BitVec.Lemmas
_private.Init.Data.BitVec.Lemmas.0.Int.toNat.match_1.splitter : (motive : ℤ → Sort u_1) → (x : ℤ) → ((n : ℕ) → motive (Int.ofNat n)) → ((a : ℕ) → motive (Int.negSucc a)) → motive x
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- This is a helper construction that can be useful when verifying that a category has all
equalizers. Given `F : WalkingParallelPair ⥤ C`, which is really the same as
`parallelPair (F.map left) (F.map right)`, and a fork on `F.map left` and `F.map right`,
we get a cone on `F`.

If you're thinking about using this, have a look at `hasEqualizers_of_hasLimit_parallelPair`,
which you may find to be an easier way of achieving your goal.  -/
CategoryTheory.Limits.Cone.ofFork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} →
      CategoryTheory.Limits.Fork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
          (F.map CategoryTheory.Limits.WalkingParallelPairHom.right) →
        CategoryTheory.Limits.Cone F
-- Mathlib.NumberTheory.AlmostPrime
/-- `IsAtMostAlmostPrime k n` means that `n` has at most `k` prime factors,
counted with multiplicity.  -/
Nat.IsAtMostAlmostPrime : ℕ → ℕ → Prop
-- Init.Data.Vector.Perm
Vector.toArray_perm_iff : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (ys : Array α),
  xs.toArray.Perm ys ↔ ∃ (h : ys.size = n), xs.Perm (Vector.mk ys h)
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
/-- If a function and its derivative are integrable on the real line, then the integral of the
derivative is zero.  -/
MeasureTheory.integral_eq_zero_of_hasDerivAt_of_integrable : ∀ {E : Type u_1} {f f' : ℝ → E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E],
  (∀ (x : ℝ), HasDerivAt f (f' x) x) →
    MeasureTheory.Integrable f' MeasureTheory.volume →
      MeasureTheory.Integrable f MeasureTheory.volume → ∫ (x : ℝ), f' x = 0
-- Mathlib.Data.Fin.Embedding
/-- `Fin.castLE` as an `Embedding`, `castLEEmb h i` embeds `i` into a larger `Fin` type.  -/
Fin.castLEEmb : {n m : ℕ} → n ≤ m → Fin n ↪ Fin m
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.instCompleteSpace : ∀ {K : Type u_1} [inst : Field K] (v : NumberField.InfinitePlace K), CompleteSpace v.Completion
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.equivSubtype_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] (a : TopologicalSpace.IrreducibleCloseds α),
  TopologicalSpace.IrreducibleCloseds.equivSubtype a = ⟨a.carrier, ⋯⟩
-- Lean.Data.Lsp.Basic
Lean.Lsp.instInhabitedLocation.default : Lean.Lsp.Location
-- Mathlib.Analysis.Complex.Basic
Complex.isometry_intCast : Isometry Int.cast
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C.eq_3 : ∀ (R : Type u_1) [inst : CommRing R] (n : ℕ),
  Polynomial.Chebyshev.C R (Int.ofNat n.succ.succ) =
    Polynomial.X * Polynomial.Chebyshev.C R (↑n + 1) - Polynomial.Chebyshev.C R ↑n
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
_private.Mathlib.LinearAlgebra.ExteriorPower.Basic.0.exteriorPower.presentation.relations.match_1.splitter : (R : Type u_1) →
  (ι : Type u_2) →
    (M : Type u_3) →
      (motive : exteriorPower.presentation.Rels R ι M → Sort u_4) →
        (x : exteriorPower.presentation.Rels R ι M) →
          ((m : ι → M) → (i : ι) → (x y : M) → motive (exteriorPower.presentation.Rels.add m i x y)) →
            ((m : ι → M) → (i : ι) → (r : R) → (x : M) → motive (exteriorPower.presentation.Rels.smul m i r x)) →
              ((m : ι → M) →
                  (i j : ι) →
                    (hm : m i = m j) → (hij : i ≠ j) → motive (exteriorPower.presentation.Rels.alt m i j hm hij)) →
                motive x
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k fallback : α}, (t.insert k).minD fallback = t.min?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.Analysis.InnerProductSpace.Spectrum
LinearMap.IsSymmetric.orthogonalComplement_iSup_eigenspaces_eq_bot' : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →ₗ[𝕜] E} [FiniteDimensional 𝕜 E], T.IsSymmetric → (⨆ μ, Module.End.eigenspace T (↑T 1 μ))ᗮ = ⊥
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.Std.Iter.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- `η.isoLift?` is a pair of a 2-isomorphism `η'` and a proof that `η'.hom = η`. If no such `η'`
is found, returns `none`. This function does not seek `IsIso` instance.  -/
Mathlib.Tactic.BicategoryLike.Mor₂.isoLift? : Mathlib.Tactic.BicategoryLike.Mor₂ → Option Mathlib.Tactic.BicategoryLike.IsoLift
-- Mathlib.Algebra.Module.Equiv.Defs
/-- Linear equivalences are symmetric.  -/
LinearEquiv.symm : {R : Type u_1} →
  {S : Type u_6} →
    {M : Type u_7} →
      {M₂ : Type u_9} →
        [inst : Semiring R] →
          [inst_1 : Semiring S] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                {module_M : Module R M} →
                  {module_S_M₂ : Module S M₂} →
                    {σ : R →+* S} →
                      {σ' : S →+* R} →
                        {re₁ : RingHomInvPair σ σ'} → {re₂ : RingHomInvPair σ' σ} → (M ≃ₛₗ[σ] M₂) → M₂ ≃ₛₗ[σ'] M
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getD_insertIfNew : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k a : α} {fallback v : β},
  Std.ExtDTreeMap.Const.getD (t.insertIfNew k v) a fallback =
    if cmp k a = Ordering.eq ∧ k ∉ t then v else Std.ExtDTreeMap.Const.getD t a fallback
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
/-- The definition of divided powers on the codomain `B` of a surjective ring homomorphism
from a ring `A` with divided powers `hI`. This definition is tagged as noncomputable
because it makes use of `Function.extend`, but under the hypothesis
`IsSubDPIdeal hI (RingHom.ker f ⊓ I)`, `dividedPowers_unique` proves that no choices are
involved.  -/
DividedPowers.Quotient.OfSurjective.dpow : {A : Type u_1} →
  [inst : CommRing A] → {I : Ideal A} → DividedPowers I → {B : Type u_2} → [inst_1 : CommRing B] → (A →+* B) → ℕ → B → B
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.minD_le_of_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, t.contains k = true → ∀ {fallback : α}, (cmp (t.minD fallback) k).isLE = true
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.post_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  {D : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} D] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasLimit F] (G : CategoryTheory.Functor C D)
  [inst_4 : CategoryTheory.Limits.HasLimit (F.comp G)] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limit.post F G)
      (CategoryTheory.Limits.limit.π (F.comp G) j) =
    G.map (CategoryTheory.Limits.limit.π F j)
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- A regular monomorphism is an isomorphism if it is an epimorphism.  -/
CategoryTheory.isIso_of_regularMono_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (h : CategoryTheory.RegularMono f)
  [CategoryTheory.Epi f], CategoryTheory.IsIso f
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
HomotopyCategory.quotient_obj_singleFunctors_obj : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (n : ℤ) (X : C),
  (HomotopyCategory.quotient C (ComplexShape.up ℤ)).obj ((CochainComplex.singleFunctor C n).obj X) =
    (HomotopyCategory.singleFunctor C n).obj X
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebra.iSupLift_inclusion : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : IsScalarTower R A A]
  [inst_6 : SMulCommClass R A A] {ι : Sort u_1} [inst_7 : Nonempty ι] {K : ι → NonUnitalSubalgebra R A}
  {dir : Directed (fun x1 x2 => x1 ≤ x2) K} {f : (i : ι) → ↥(K i) →ₙₐ[R] B}
  {hf : ∀ (i j : ι) (h : K i ≤ K j), f i = (f j).comp (NonUnitalSubalgebra.inclusion h)} {T : NonUnitalSubalgebra R A}
  {hT : T = iSup K} {i : ι} (x : ↥(K i)) (h : K i ≤ T),
  (NonUnitalSubalgebra.iSupLift K dir f hf T hT) ((NonUnitalSubalgebra.inclusion h) x) = (f i) x
-- Mathlib.Tactic.CategoryTheory.Monoidal.Datatypes
Mathlib.Tactic.Monoidal.instMkMor₂MonoidalM : Mathlib.Tactic.BicategoryLike.MkMor₂ Mathlib.Tactic.Monoidal.MonoidalM
-- Mathlib.Data.Set.Prod
Set.update_image : ∀ {ι : Type u_1} {β : ι → Type u_3} [inst : DecidableEq ι] (x : (i : ι) → β i) (i : ι) (s : Set (β i)),
  Function.update x i '' s = Set.univ.pi (Function.update (fun j => {x j}) i s)
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.RightExtension.postcomp₁_obj_left_map : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') (f : L.comp G ⟶ L') (F : CategoryTheory.Functor C H)
  (X :
    CategoryTheory.Comma ((CategoryTheory.Functor.whiskeringLeft C D' H).obj L') (CategoryTheory.Functor.fromPUnit F))
  {X_1 Y : D} (f_1 : X_1 ⟶ Y),
  ((CategoryTheory.Functor.RightExtension.postcomp₁ G f F).obj X).left.map f_1 = X.left.map (G.map f_1)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.forIn_yield_eq_foldM : ∀ {α β γ δ : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  {n : Type w → Type w''} [inst_2 : Monad m] [inst_3 : Monad n] [LawfulMonad n] [inst_5 : Std.IteratorLoop α m n]
  [Std.LawfulIteratorLoop α m n] [inst_7 : MonadLiftT m n] {f : β → γ → n δ} {g : β → γ → δ → γ} {init : γ}
  {it : Std.IterM m β},
  (forIn it init fun c b => (fun d => ForInStep.yield (g c b d)) <$> f c b) =
    Std.IterM.foldM (fun b c => g c b <$> f c b) init it
-- Mathlib.GroupTheory.Exponent
AddMonoid.ExponentExists.addOrderOf_pos : ∀ {G : Type u} [inst : AddMonoid G], AddMonoid.ExponentExists G → ∀ (g : G), 0 < addOrderOf g
-- Lean.Parser.Basic
/-- If the leading token is an identifier `<foo>`, then it executes the parsers associated with token
`<foo>` and parsers associated with the auxiliary token “ident”, which parses identifiers.
 -/
Lean.Parser.LeadingIdentBehavior.both : Lean.Parser.LeadingIdentBehavior
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instPartialOrder : {α : Type u_1} → {β : Type u_2} → {l : Filter α} → [PartialOrder β] → PartialOrder (l.Germ β)
-- Mathlib.Topology.Algebra.Monoid.Defs
Filter.Tendsto.const_mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [SeparatelyContinuousMul M] {α : Type u_2} {f : α → M}
  {x : Filter α} {a : M} (b : M), Filter.Tendsto f x (nhds a) → Filter.Tendsto (fun x => b * f x) x (nhds (b * a))
-- Init.Data.SInt.Lemmas
Int16.sub_sub : ∀ (a b c : Int16), a - b - c = a - (b + c)
-- Std.Sat.AIG.Lemmas
_private.Std.Sat.AIG.Lemmas.0.Std.Sat.AIG.toGraphviz.go.match_1.eq_3 : ∀ {α : Type} (motive : Std.Sat.AIG.Decl α → Sort u_1) (lhs rhs : Std.Sat.AIG.Fanin)
  (h_1 : Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.false → motive Std.Sat.AIG.Decl.false)
  (h_2 : (idx : α) → Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.atom idx → motive (Std.Sat.AIG.Decl.atom idx))
  (h_3 :
    (lhs_1 rhs_1 : Std.Sat.AIG.Fanin) →
      Std.Sat.AIG.Decl.gate lhs rhs = Std.Sat.AIG.Decl.gate lhs_1 rhs_1 → motive (Std.Sat.AIG.Decl.gate lhs_1 rhs_1)),
  (match elem : Std.Sat.AIG.Decl.gate lhs rhs with
    | Std.Sat.AIG.Decl.false => h_1 elem
    | Std.Sat.AIG.Decl.atom idx => h_2 idx elem
    | Std.Sat.AIG.Decl.gate lhs_1 rhs_1 => h_3 lhs_1 rhs_1 elem) =
    h_3 lhs rhs ⋯
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Functor.mapConeInvMapCone.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {D : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} D] {F : CategoryTheory.Functor J D}
  (H : CategoryTheory.Functor D C) [inst_3 : H.IsEquivalence] (c : CategoryTheory.Limits.Cone F),
  CategoryTheory.Functor.mapConeInvMapCone H c =
    (CategoryTheory.Limits.Cone.functorialityEquivalence F H.asEquivalence).unitIso.symm.app c
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.getGrindParams : Lean.TSyntax `tactic → Array Lean.Syntax
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.mul_nc.eq_def : ∀ (m₁ m₂ : Lean.Grind.CommRing.Mon),
  m₁.mul_nc m₂ =
    match m₁ with
    | Lean.Grind.CommRing.Mon.unit => m₂
    | Lean.Grind.CommRing.Mon.mult pw Lean.Grind.CommRing.Mon.unit => Lean.Grind.CommRing.Mon.mulPow_nc pw m₂
    | Lean.Grind.CommRing.Mon.mult pw m₁ => Lean.Grind.CommRing.Mon.mult pw (m₁.mul_nc m₂)
-- Mathlib.Order.Circular
/-- The circular order obtained from "looping around" a linear order.
See note [reducible non-instances].  -/
LinearOrder.toCircularOrder : (α : Type u_1) → [LinearOrder α] → CircularOrder α
-- Mathlib.NumberTheory.Harmonic.ZetaAsymp
ZetaAsymptotics.term.eq_1 : ∀ (n : ℕ) (s : ℝ), ZetaAsymptotics.term n s = ∫ (x : ℝ) in ↑n..↑n + 1, (x - ↑n) / x ^ (s + 1)
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalSubalgebra.topologicalClosure_minimal : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : TopologicalSpace A] [inst_2 : NonUnitalSemiring A]
  [inst_3 : Module R A] [inst_4 : ContinuousConstSMul R A] [inst_5 : IsSemitopologicalSemiring A]
  {s t : NonUnitalSubalgebra R A}, s ≤ t → IsClosed ↑t → s.topologicalClosure ≤ t
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instFromJsonDeclarationParams : Lean.FromJson Lean.Lsp.DeclarationParams
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instWeaklyLocallyCompactSpaceCofiniteOfFactForallIsOpenOfCompactSpaceElem : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} [inst : (i : ι) → TopologicalSpace (R i)]
  [hAopen : Fact (∀ (i : ι), IsOpen (A i))] [∀ (i : ι), WeaklyLocallyCompactSpace (R i)]
  [hAcompact : ∀ (i : ι), CompactSpace ↑(A i)],
  WeaklyLocallyCompactSpace (RestrictedProduct (fun i => R i) (fun i => A i) Filter.cofinite)
-- Mathlib.Algebra.GroupWithZero.Action.Defs
DistribMulAction.toAddMonoidHom_apply : ∀ {M : Type u_1} (A : Type u_7) [inst : Monoid M] [inst_1 : AddMonoid A] [inst_2 : DistribMulAction M A] (x : M)
  (x_1 : A), (DistribMulAction.toAddMonoidHom A x) x_1 = x • x_1
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.ClosureState.mk.inj : ∀ {newLocalDecls localDecls newLetDecls : Array Lean.LocalDecl} {exprArgs : Array Lean.Expr}
  {newLocalDecls_1 localDecls_1 newLetDecls_1 : Array Lean.LocalDecl} {exprArgs_1 : Array Lean.Expr},
  { newLocalDecls := newLocalDecls, localDecls := localDecls, newLetDecls := newLetDecls, exprArgs := exprArgs } =
      { newLocalDecls := newLocalDecls_1, localDecls := localDecls_1, newLetDecls := newLetDecls_1,
        exprArgs := exprArgs_1 } →
    newLocalDecls = newLocalDecls_1 ∧ localDecls = localDecls_1 ∧ newLetDecls = newLetDecls_1 ∧ exprArgs = exprArgs_1
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceFinHAddNatOfNatProdIntCoreE₂CohomologicalFin : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C] {l : ℕ}
  (E : CategoryTheory.Abelian.SpectralObject C (Fin (l + 1))),
  E.HasSpectralSequence (CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin l)
-- Mathlib.Data.Rat.Cast.Order
NNRat.natCast_lt_cast : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {m : ℕ} {n : ℚ≥0},
  ↑m < ↑n ↔ ↑m < n
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₇_off_diag_nonpos : ∀ (i j : Fin 7), i ≠ j → CartanMatrix.E₇ i j ≤ 0
-- Mathlib.Combinatorics.SetFamily.Compression.Down
/-- Down-compressing a family doesn't change its size.  -/
Down.card_compression : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (𝒜 : Finset (Finset α)), (Down.compression a 𝒜).card = 𝒜.card
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.map_map : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] (N : Subgroup G) [nN : N.Normal] {I : Type u_5}
  [inst_2 : Group I] (M : Subgroup H) (O : Subgroup I) [inst_3 : M.Normal] [inst_4 : O.Normal] (f : G →* H) (g : H →* I)
  (hf : N ≤ Subgroup.comap f M) (hg : M ≤ Subgroup.comap g O) (hgf : optParam (N ≤ Subgroup.comap (g.comp f) O) ⋯)
  (x : G ⧸ N), (QuotientGroup.map M O g hg) ((QuotientGroup.map N M f hf) x) = (QuotientGroup.map N O (g.comp f) hgf) x
-- Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness
/-- Bird's equation (5)  -/
_private.Mathlib.LinearAlgebra.Matrix.Determinant.Bird.Correctness.0.BirdDet.paper_eq5 : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (A : Matrix (Fin n) (Fin n) R) {p : ℕ} (i j : Fin n),
  ∑ α ∈ BirdDet.S✝ (p + 1) i, BirdDet.bminor✝ A i j α =
    ∑ α ∈ BirdDet.S✝ (p + 1) i, BirdDet.pminor✝ A α * A i j -
      ∑ α ∈ BirdDet.S✝ (p + 1) i, ∑ t, BirdDet.bminor✝ A i (α t) (t.removeNth α) * A (α t) j
-- Mathlib.GroupTheory.Subgroup.Center
AddSubgroup.center_le_normalizer : ∀ {G : Type u_1} [inst : AddGroup G] (s : Set G), AddSubgroup.center G ≤ AddSubgroup.normalizer s
-- Mathlib.Algebra.Free
FreeAddMagma.instTraversable.eq_1 : FreeAddMagma.instTraversable = { toFunctor := FreeAddMagma.instMonad.toFunctor, traverse := @FreeAddMagma.traverse }
-- Mathlib.Analysis.Normed.Field.Basic
NormedField.mk : {α : Type u_5} →
  [toNorm : Norm α] →
    [toField : Field α] →
      [toMetricSpace : MetricSpace α] →
        (∀ (x y : α), dist x y = ‖-x + y‖) → (∀ (a b : α), ‖a * b‖ = ‖a‖ * ‖b‖) → NormedField α
-- Init.Data.Order.Opposite
LT.opposite_def : ∀ {α : Type u_1} {lt : LT α}, lt.opposite = { lt := fun a b => b < a }
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.prod_mul_prod_comm : ∀ {α : Type u_2} {β : Type u_3} [inst : Mul α] [inst_1 : Mul β] (s₁ s₂ : Set α) (t₁ t₂ : Set β),
  s₁ ×ˢ t₁ * s₂ ×ˢ t₂ = (s₁ * s₂) ×ˢ (t₁ * t₂)
-- Lean.Elab.InfoTree.Types
Lean.Elab.DocElabKind.role.sizeOf_spec : sizeOf Lean.Elab.DocElabKind.role = 1
-- Mathlib.LinearAlgebra.Dual.Lemmas
Subspace.finrank_add_finrank_dualCoannihilator_eq : ∀ {K : Type u_1} {V : Type u_2} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  (W : Subspace K (Module.Dual K V)),
  Module.finrank K ↥W + Module.finrank K ↥(Submodule.dualCoannihilator W) = Module.finrank K V
-- Mathlib.Analysis.AbsoluteValue.Equivalence
AbsoluteValue.isEquiv_iff_isHomeomorph : ∀ {F : Type u_1} [inst : Field F] (v w : AbsoluteValue F ℝ),
  v.IsEquiv w ↔ IsHomeomorph ⇑(WithAbs.congr v w (RingEquiv.refl F))
-- Mathlib.CategoryTheory.Limits.Indization.ParallelPair
CategoryTheory.NonemptyParallelPairPresentationAux.hf : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A B : CategoryTheory.Functor Cᵒᵖ (Type v₁)} (f g : A ⟶ B)
  (P₁ : CategoryTheory.Limits.IndObjectPresentation A) (P₂ : CategoryTheory.Limits.IndObjectPresentation B),
  f =
    (CategoryTheory.NonemptyParallelPairPresentationAux.isColimit₁ f g P₁ P₂).map
      { pt := B, ι := CategoryTheory.NonemptyParallelPairPresentationAux.ι₂ f g P₁ P₂ }
      (CategoryTheory.Functor.whiskerRight (CategoryTheory.NonemptyParallelPairPresentationAux.ϕ f g P₁ P₂)
        CategoryTheory.yoneda)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insertUnit.match_3.splitter : {n : ℕ} →
  (motive :
      Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) ×
          Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Bool →
        Sort u_1) →
    (x :
        Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) ×
          Array Std.Tactic.BVDecide.LRAT.Internal.Assignment × Bool) →
      ((units : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) →
          (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
            (foundContradiction : Bool) → motive (units, assignments, foundContradiction)) →
        motive x
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.Realize.eq_5 : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} (x : ℕ) (x_1 : α → M) (x_2 : Fin x → M)
  (f : L.BoundedFormula α (x + 1)), f.all.Realize x_1 x_2 = ∀ (x_3 : M), f.Realize x_1 (Fin.snoc x_2 x_3)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.isCycle_reverse : ∀ {V : Type u} {G : SimpleGraph V} {u : V} {p : G.Walk u u}, p.reverse.IsCycle ↔ p.IsCycle
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.integralAgainstBilinLM.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {n : ℕ∞} {K : TopologicalSpace.Compacts E} {m : MeasurableSpace E}
  [inst_3 : OpensMeasurableSpace E] {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst_4 : NormedAddCommGroup F₁]
  [inst_5 : NormedSpace 𝕜 F₁] [inst_6 : NormedSpace ℝ F₁] [inst_7 : NormedAddCommGroup F₂] [inst_8 : NormedSpace 𝕜 F₂]
  [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace 𝕜 F₃] [inst_11 : SMulCommClass ℝ 𝕜 F₁]
  [inst_12 : NormedSpace ℝ F₃] [inst_13 : SMulCommClass ℝ 𝕜 F₃] (B B_1 : F₁ →L[𝕜] F₂ →L[𝕜] F₃),
  B = B_1 →
    ∀ (μ μ_1 : MeasureTheory.Measure E),
      μ = μ_1 →
        ∀ (φ φ_1 : E → F₂),
          φ = φ_1 →
            ContDiffMapSupportedIn.integralAgainstBilinLM B μ φ =
              ContDiffMapSupportedIn.integralAgainstBilinLM B_1 μ_1 φ_1
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.HasColimits
AlgebraicGeometry.LocallyRingedSpace.instHasColimitsOfShapeDiscrete : ∀ {ι : Type v} [Small.{u, v} ι],
  CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete ι) AlgebraicGeometry.LocallyRingedSpace
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Util
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr.throwUnexpected : {α : Type} → Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr → Lean.Meta.Grind.GoalM α
-- Mathlib.Data.Seq.Defs
/-- Corecursor over pairs of `Option` values  -/
Stream'.Seq.Corec.f : {α : Type u} → {β : Type v} → (β → Option (α × β)) → Option β → Option α × Option β
-- Init.Meta
/-- `simp_all_arith` has been deprecated. It was a shorthand for `simp_all +arith +decide`.
Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
 -/
Lean.Parser.Tactic.simpAllArith : Lean.ParserDescr