mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Creates
/-- any limit cone can be lifted to a cone above  -/
CategoryTheory.CreatesLimit.lifts : {C : Type u₁} →
  {inst : CategoryTheory.Category.{v₁, u₁} C} →
    {D : Type u₂} →
      {inst_1 : CategoryTheory.Category.{v₂, u₂} D} →
        {J : Type w} →
          {inst_2 : CategoryTheory.Category.{w', w} J} →
            {K : CategoryTheory.Functor J C} →
              {F : CategoryTheory.Functor C D} →
                [self : CategoryTheory.CreatesLimit K F] →
                  (c : CategoryTheory.Limits.Cone (K.comp F)) →
                    CategoryTheory.Limits.IsLimit c → CategoryTheory.LiftableCone K F c
-- Mathlib.Computability.TuringMachine.PostTuringMachine
/-- The current state of the tape: current symbol, left and right parts.  -/
Turing.TM0.Cfg.Tape : {Γ : Type u_1} → {Λ : Type u_2} → [inst : Inhabited Γ] → Turing.TM0.Cfg Γ Λ → Turing.Tape Γ
-- Mathlib.Order.Directed
directed_of₃ : ∀ {α : Type u_1} (r : α → α → Prop) [IsDirected α r] [IsTrans α r] (a b c : α), ∃ d, r a d ∧ r b d ∧ r c d
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow_null : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} [inst_1 : DecidablePred fun x => x ∈ I] {m : ℕ} {x : A},
  x ∉ I → DividedPowers.OfInvertibleFactorial.dpow I m x = 0
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instMul : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → Mul (CauSeq β abv)
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerLeft_mapComp'_inv_comp_mapComp'₀₁₃_inv_assoc : ∀ {B : Type u₁} {C : Type u₂} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  [inst_2 : CategoryTheory.Bicategory C] (F : CategoryTheory.Pseudofunctor B C) {b₀ b₁ b₂ b₃ : B} (f₀₁ : b₀ ⟶ b₁)
  (f₁₂ : b₁ ⟶ b₂) (f₂₃ : b₂ ⟶ b₃) (f₀₂ : b₀ ⟶ b₂) (f₁₃ : b₁ ⟶ b₃) (f : b₀ ⟶ b₃)
  (h₀₂ : CategoryTheory.CategoryStruct.comp f₀₁ f₁₂ = f₀₂) (h₁₃ : CategoryTheory.CategoryStruct.comp f₁₂ f₂₃ = f₁₃)
  (hf : CategoryTheory.CategoryStruct.comp f₀₁ f₁₃ = f) {Z : F.obj b₀ ⟶ F.obj b₃} (h : F.map f ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (F.map f₀₁) (F.mapComp' f₁₂ f₂₃ f₁₃ h₁₃).inv)
      (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₁ f₁₃ f hf).inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f₀₁) (F.map f₁₂) (F.map f₂₃)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (F.mapComp' f₀₁ f₁₂ f₀₂ h₀₂).inv (F.map f₂₃))
        (CategoryTheory.CategoryStruct.comp (F.mapComp' f₀₂ f₂₃ f ⋯).inv h))
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.LeftHomologyData.homologyIso_hom_comp_leftHomologyIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology] (h : S.LeftHomologyData) {Z : C}
  (h_1 : S.leftHomology ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.homologyIso.hom (CategoryTheory.CategoryStruct.comp h.leftHomologyIso.inv h_1) =
    CategoryTheory.CategoryStruct.comp S.leftHomologyIso.inv h_1
-- Lean.DocString.Parser
Lean.Doc.Parser.instReprInList : Repr Lean.Doc.Parser.InList
-- Init.Data.UInt.Lemmas
UInt16.lt_irrefl : ∀ (a : UInt16), ¬a < a
-- Mathlib.RingTheory.MvPowerSeries.Rename
/-- Implementation detail for `killCompl`. Use `MvPowerSeries.killCompl` instead.  -/
MvPowerSeries.killComplFun : {σ : Type u_1} → {τ : Type u_2} → {R : Type u_4} → [CommSemiring R] → (σ ↪ τ) → MvPowerSeries τ R → MvPowerSeries σ R
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfp_id : Ordinal.nfp id = id
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.instSubsingleton : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} [Subsingleton R], Subsingleton W'.CoordinateRing
-- Init.Data.BitVec.Bootstrap
/-- Prove equality of bitvectors in terms of nat operations.  -/
BitVec.eq_of_toNat_eq : ∀ {n : ℕ} {x y : BitVec n}, x.toNat = y.toNat → x = y
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.is_id : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (f : MvPolynomial σ R →+* MvPolynomial σ R),
  f.comp MvPolynomial.C = MvPolynomial.C →
    (∀ (n : σ), f (MvPolynomial.X n) = MvPolynomial.X n) → ∀ (p : MvPolynomial σ R), f p = p
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.MeasurePreserving.mul_left : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Mul G] [MeasurableMul G] (μ : MeasureTheory.Measure G)
  [μ.IsMulLeftInvariant] (g : G) {X : Type u_3} [inst_4 : MeasurableSpace X] {μ' : MeasureTheory.Measure X} {f : X → G},
  MeasureTheory.MeasurePreserving f μ' μ → MeasureTheory.MeasurePreserving (fun x => g * f x) μ' μ
-- Mathlib.RingTheory.WittVector.Defs
WittVector.mul_coeff : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (x y : WittVector p R) (n : ℕ),
  (x * y).coeff n = WittVector.peval (WittVector.wittMul p n) ![x.coeff, y.coeff]
-- Mathlib.Data.Nat.Fib.Basic
/-- **Alias** of `Nat.fastFibAux_bit_true`. -/
Nat.fast_fib_aux_bit_tt : ∀ (n : ℕ),
  (Nat.bit true n).fastFibAux =
    have p := n.fastFibAux;
    (p.2 ^ 2 + p.1 ^ 2, p.2 * (2 * p.1 + p.2))
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instFaithfulSMulForallOfNontrivial : ∀ {M : Type u_1} {β : Type u_2} {α : Type u_3} [inst : SMul M α] [FaithfulSMul M α] [Nontrivial β],
  FaithfulSMul Mᵈᵐᵃ (α → β)
-- Mathlib.Order.Filter.Extr
IsMinOn.comp_mapsTo : ∀ {α : Type u} {β : Type v} {δ : Type x} [inst : Preorder β] {f : α → β} {s : Set α} {a : α} {t : Set δ} {g : δ → α}
  {b : δ}, IsMinOn f s a → Set.MapsTo g t s → g b = a → IsMinOn (f ∘ g) t b
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.get_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k : α} (not_mem : k ∉ m₂) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).get k h' = m₁.get k ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Basic
HasFDerivWithinAt.isBigOTVS_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} [ContinuousAdd F] [ContinuousSMul 𝕜 F],
  HasFDerivWithinAt f f' s x → (fun x_1 => f x_1 - f x) =O[𝕜; nhdsWithin x s] fun x_1 => x_1 - x
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
ThreeAPFree.addRothNumber_eq : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s : Finset α}, ThreeAPFree ↑s → addRothNumber s = s.card
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- In a `p ^ (k + 1)`-th cyclotomic extension of `ℚ `, we have that `ζ` is not congruent to an
integer modulo `p` if `p ^ (k  + 1) ≠ 2`.  -/
IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_pow_ne_two : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  p ^ (k + 1) ≠ 2 → ¬∃ n, ↑p ∣ hζ.toInteger - ↑n
-- Mathlib.Order.Atoms
/-- **Alias** of the reverse direction of `covBy_top_iff`. -/
IsCoatom.covBy_top : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, IsCoatom a → a ⋖ ⊤
-- Mathlib.MeasureTheory.OuterMeasure.OfFunction
MeasureTheory.OuterMeasure.comap_ofFunction : ∀ {α : Type u_1} {m : Set α → ENNReal} {m_empty : m ∅ = 0} {β : Type u_2} (f : β → α),
  Monotone m ∨ Function.Surjective f →
    (MeasureTheory.OuterMeasure.comap f) (MeasureTheory.OuterMeasure.ofFunction m m_empty) =
      MeasureTheory.OuterMeasure.ofFunction (fun s => m (f '' s)) ⋯
-- Init.GetElem
Array.instLawfulGetElemNatLtSize : ∀ {α : Type u_1}, LawfulGetElem (Array α) ℕ α fun xs i => i < xs.size
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- Check if one of the imports `imports` to `mainModule` is forbidden by `forbiddenImportDirs`;
if so, return an error describing how the import transitively arises.  -/
_private.Mathlib.Tactic.Linter.DirectoryDependency.0.Mathlib.Linter.checkBlocklist : Lean.Environment → Lean.Name → Array Lean.Name → Option Lean.MessageData
-- Mathlib.Data.Int.ModEq
Int.modEq_add_mul_modulus_iff : ∀ {n a b c : ℤ}, a ≡ b + c * n [ZMOD n] ↔ a ≡ b [ZMOD n]
-- Mathlib.CategoryTheory.Sites.Pretopology
/-- The trivial pretopology induces the trivial Grothendieck topology.  -/
CategoryTheory.Pretopology.toGrothendieck_bot : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C],
  ⊥.toGrothendieck = ⊥
-- Lean.DocString.Formatter
_private.Lean.DocString.Formatter.0.Lean.Doc.Parser.formatMetadata : Lean.PrettyPrinter.Formatter
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Append
Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget.lhs : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {combined : ℕ} → (self : Std.Tactic.BVDecide.BVExpr.bitblast.AppendTarget aig combined) → aig.RefVec self.lw
-- Mathlib.Topology.Sober
isGenericPoint_iff_forall_closed : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {S : Set α},
  IsClosed S → x ∈ S → (IsGenericPoint x S ↔ ∀ (Z : Set α), IsClosed Z → x ∈ Z → S ⊆ Z)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- The inner product of a linear combination of a set of orthonormal vectors with one of those
vectors picks out the coefficient of that vector.  -/
Orthonormal.inner_right_sum : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E},
  Orthonormal 𝕜 v → ∀ (l : ι → 𝕜) {s : Finset ι} {i : ι}, i ∈ s → inner 𝕜 (v i) (∑ i ∈ s, l i • v i) = l i
-- Lean.Declaration
Lean.ConstantInfo.inductiveVal! : Lean.ConstantInfo → Lean.InductiveVal
-- Mathlib.Tactic.DuplicateDecls
_private.Mathlib.Tactic.DuplicateDecls.0.Mathlib.Tactic.DuplicateDecls.instMaxModuleKey : Max Mathlib.Tactic.DuplicateDecls.ModuleKey✝
-- Mathlib.CategoryTheory.Comma.Final
/-- Let `A` and `B` be cofiltered categories, `L : A ⥤ T` be initial and `R : B ⥤ T`. Then, the
comma category `Comma L R` is cofiltered.  -/
CategoryTheory.Comma.isCofiltered_of_initial : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [CategoryTheory.IsCofiltered A] [CategoryTheory.IsCofiltered B] [L.Initial],
  CategoryTheory.IsCofiltered (CategoryTheory.Comma L R)
-- Mathlib.LinearAlgebra.Determinant
/-- If there exists a two-sided inverse `M'` for `M` (indexed differently),
then `det (N * M) = det (M * N)`.  -/
Matrix.det_comm' : ∀ {A : Type u_5} [inst : CommRing A] {m : Type u_6} {n : Type u_7} [inst_1 : Fintype m] [inst_2 : Fintype n]
  [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] {M : Matrix n m A} {N M' : Matrix m n A},
  M * M' = 1 → M' * M = 1 → (M * N).det = (N * M).det
-- Init.Data.String.Slice
/-- Checks whether a slice only consists of matches of the pattern `pat`.

Short-circuits at the first pattern mis-match.

This function is generic over all currently supported patterns.

Examples:

* `"brown".toSlice.all Char.isLower = true`

* `"brown and orange".toSlice.all Char.isLower = false`

* `"aaaaaa".toSlice.all 'a' = true`

* `"aaaaaa".toSlice.all "aa" = true`

* `"aaaaaaa".toSlice.all "aa" = false`
 -/
String.Slice.all : {ρ : Type} → String.Slice → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → Bool
-- Mathlib.Data.Countable.Small
Countable.toSmall : ∀ (α : Type v) [Countable α], Small.{w, v} α
-- Mathlib.Topology.Homotopy.HSpaces
/-- `qRight` is analogous to the function `Q` defined on p. 475 of [serre1951] that helps proving
continuity of `delayReflRight`.  -/
unitInterval.qRight : ↑unitInterval × ↑unitInterval → ↑unitInterval
-- Mathlib.AlgebraicGeometry.Restrict
AlgebraicGeometry.ΓRestrictAlgebra : {X : AlgebraicGeometry.Scheme} →
  (U : X.Opens) → Algebra ↑(X.presheaf.obj (Opposite.op ⊤)) ↑((↑U).presheaf.obj (Opposite.op ⊤))
-- Mathlib.RingTheory.TwoSidedIdeal.Lattice
TwoSidedIdeal.coe_top : ∀ (R : Type u_1) [inst : NonUnitalNonAssocRing R], ↑⊤ = Set.univ
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.nndist_single_same : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] (i : ι) (a b : 𝕜),
  nndist (EuclideanSpace.single i a) (EuclideanSpace.single i b) = nndist a b
-- Mathlib.Analysis.Normed.Group.Pointwise
Bornology.IsBounded.inv : ∀ {E : Type u_1} [inst : SeminormedGroup E] {s : Set E}, Bornology.IsBounded s → Bornology.IsBounded s⁻¹
-- Aesop.Util.EqualUpToIds
Aesop.EqualUpToIds.GoalContext.mk.injEq : ∀ (lctx₁ : Lean.LocalContext) (localInstances₁ : Lean.LocalInstances) (lctx₂ : Lean.LocalContext)
  (localInstances₂ : Lean.LocalInstances) (equalFVarIds : Std.HashMap Lean.FVarId Lean.FVarId)
  (lctx₁_1 : Lean.LocalContext) (localInstances₁_1 : Lean.LocalInstances) (lctx₂_1 : Lean.LocalContext)
  (localInstances₂_1 : Lean.LocalInstances) (equalFVarIds_1 : Std.HashMap Lean.FVarId Lean.FVarId),
  ({ lctx₁ := lctx₁, localInstances₁ := localInstances₁, lctx₂ := lctx₂, localInstances₂ := localInstances₂,
        equalFVarIds := equalFVarIds } =
      { lctx₁ := lctx₁_1, localInstances₁ := localInstances₁_1, lctx₂ := lctx₂_1, localInstances₂ := localInstances₂_1,
        equalFVarIds := equalFVarIds_1 }) =
    (lctx₁ = lctx₁_1 ∧
      localInstances₁ = localInstances₁_1 ∧
        lctx₂ = lctx₂_1 ∧ localInstances₂ = localInstances₂_1 ∧ equalFVarIds = equalFVarIds_1)
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Problem.mk.inj : ∀ {assumptions : Array Lean.Elab.Tactic.Omega.Proof} {numVars : ℕ}
  {constraints : Std.HashMap Lean.Omega.Coeffs Lean.Elab.Tactic.Omega.Fact} {equalities : Std.HashSet Lean.Omega.Coeffs}
  {eliminations : List (Lean.Elab.Tactic.Omega.Fact × ℕ × ℤ)} {possible : Bool}
  {proveFalse? : Option Lean.Elab.Tactic.Omega.Proof}
  {proveFalse?_spec :
    autoParam ((possible || proveFalse?.isSome) = true) Lean.Elab.Tactic.Omega.Problem.proveFalse?_spec._autoParam}
  {explanation? : Thunk String} {assumptions_1 : Array Lean.Elab.Tactic.Omega.Proof} {numVars_1 : ℕ}
  {constraints_1 : Std.HashMap Lean.Omega.Coeffs Lean.Elab.Tactic.Omega.Fact}
  {equalities_1 : Std.HashSet Lean.Omega.Coeffs} {eliminations_1 : List (Lean.Elab.Tactic.Omega.Fact × ℕ × ℤ)}
  {possible_1 : Bool} {proveFalse?_1 : Option Lean.Elab.Tactic.Omega.Proof}
  {proveFalse?_spec_1 :
    autoParam ((possible_1 || proveFalse?_1.isSome) = true) Lean.Elab.Tactic.Omega.Problem.proveFalse?_spec._autoParam}
  {explanation?_1 : Thunk String},
  { assumptions := assumptions, numVars := numVars, constraints := constraints, equalities := equalities,
        eliminations := eliminations, possible := possible, proveFalse? := proveFalse?,
        proveFalse?_spec := proveFalse?_spec, explanation? := explanation? } =
      { assumptions := assumptions_1, numVars := numVars_1, constraints := constraints_1, equalities := equalities_1,
        eliminations := eliminations_1, possible := possible_1, proveFalse? := proveFalse?_1,
        proveFalse?_spec := proveFalse?_spec_1, explanation? := explanation?_1 } →
    assumptions = assumptions_1 ∧
      numVars = numVars_1 ∧
        constraints = constraints_1 ∧
          equalities = equalities_1 ∧
            eliminations = eliminations_1 ∧
              possible = possible_1 ∧ proveFalse? = proveFalse?_1 ∧ explanation? = explanation?_1
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.Reachable.dist_triangle_right : ∀ {V : Type u_1} {G : SimpleGraph V} {v w : V}, G.Reachable v w → ∀ (u : V), G.dist u w ≤ G.dist u v + G.dist v w
-- Mathlib.Algebra.Order.Floor.Defs
/-- `FloorSemiring.floor a` computes the greatest natural `n` such that `(n : α) ≤ a`.  -/
FloorSemiring.floor : {α : Type u_4} → {inst : Semiring α} → {inst_1 : PartialOrder α} → [self : FloorSemiring α] → α → ℕ
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_extendDomain : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {β : Type u_2} [inst_2 : Fintype β]
  [inst_3 : DecidableEq β] {p : β → Prop} [inst_4 : DecidablePred p] (f : α ≃ Subtype p) {g : Equiv.Perm α},
  (g.extendDomain f).cycleType = g.cycleType
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKeyLE?_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp] {k : α},
  t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyLE? k = t₂.getKeyLE? k
-- Lean.Parser.Command
/-- Prints the axioms used by a declaration, directly or indirectly.
Please consult [the reference manual](https://lean-lang.org/doc/reference/4.33.0/find/?domain=Verso.Genre.Manual.section&name=validating-proofs) to understand the significance of the output.  -/
Lean.Parser.Command.printAxioms : Lean.Parser.Parser
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.inter.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m₁ m₂ : Std.DHashMap.Raw α β),
  m₁.inter m₂ =
    if h₁ : 0 < m₁.buckets.size then
      if h₂ : 0 < m₂.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.inter ⟨m₁, h₁⟩ ⟨m₂, h₂⟩) else m₁
    else m₂
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.lt_opow_of_log_lt : ∀ {b x c : Ordinal.{u_1}}, 1 < b → Ordinal.log b x < c → x < b ^ c
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.toList_getLast? : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j : ι} (w : Monoid.CoprodI.NeWord M i j),
  w.toList.getLast? = some ⟨j, w.last⟩
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.not_mem_diff_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → k ∉ t₁ \ t₂
-- Init.Data.String.Lemmas.FindPos
String.Slice.posLE_eq_pos : ∀ {s : String.Slice} {p : String.Pos.Raw} (h : String.Pos.Raw.IsValidForSlice s p), s.posLE p = s.pos p h
-- Mathlib.Topology.Sets.Closeds
/-- The map `IrreducibleCloseds.map` is injective when `f` is inducing.
This relies on the property of embeddings that a closed set in the domain is the preimage
of the closure of its image.  -/
TopologicalSpace.IrreducibleCloseds.map_injective_of_isInducing : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : β → α}
  (hf : Topology.IsInducing f), Function.Injective (TopologicalSpace.IrreducibleCloseds.map f ⋯)
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.C_mul_monomial : ∀ {R : Type u} {σ : Type u_1} {a a' : R} {s : σ →₀ ℕ} [inst : CommSemiring R],
  MvPolynomial.C a * (MvPolynomial.monomial s) a' = (MvPolynomial.monomial s) (a * a')
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
_private.Mathlib.Analysis.Distribution.SchwartzSpace.Basic.0.SchwartzMap.decay_neg_aux : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (k n : ℕ) (f : SchwartzMap E F) (x : E),
  ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (-⇑f) x‖ = ‖x‖ ^ k * ‖iteratedFDeriv ℝ n (⇑f) x‖
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Cpop
Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget.w : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {outWidth : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.blastExtractAndExtendTarget aig outWidth → ℕ
-- Mathlib.Algebra.Module.Submodule.Range
LinearMap.range_id : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  LinearMap.id.range = ⊤
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
/-- Number of "steps": simplification and superposition.  -/
Lean.Meta.Grind.Arith.CommRing.CommRing.steps : Lean.Meta.Grind.Arith.CommRing.CommRing → ℕ
-- Mathlib.RingTheory.NonUnitalSubring.Defs
NonUnitalSubring.ext_iff : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {S T : NonUnitalSubring R}, S = T ↔ ∀ (x : R), x ∈ S ↔ x ∈ T
-- Mathlib.Order.Circular.ZMod
Int.sbtw_iff : ∀ {a b c : ℤ}, sbtw a b c ↔ a < b ∧ b < c ∨ b < c ∧ c < a ∨ c < a ∧ a < b
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.prod_range_succ' : ∀ {M : Type u_4} [inst : CommMonoid M] (f : ℕ → M) (n : ℕ),
  ∏ k ∈ Finset.range (n + 1), f k = (∏ k ∈ Finset.range n, f (k + 1)) * f 0
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Equivalence.unitIso_hom_app_tensor_comp_inverse_map_δ_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D] (e : C ≌ D)
  [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal] [e.IsMonoidal] (X Y : C),
  CategoryTheory.CategoryStruct.comp (e.unitIso.hom.app (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y))
      (e.inverse.map (CategoryTheory.Functor.OplaxMonoidal.δ e.functor X Y)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom (e.unitIso.hom.app X) (e.unitIso.hom.app Y))
      (CategoryTheory.Functor.LaxMonoidal.μ e.inverse (e.functor.obj X) (e.functor.obj Y))
-- Mathlib.Data.Seq.Parallel
Computation.parallel_congr_lem : ∀ {α : Type u} {S T : Stream'.WSeq (Computation α)} {a : α},
  Stream'.WSeq.LiftRel Computation.Equiv S T → ((∀ s ∈ S, s.Promises a) ↔ ∀ t ∈ T, t.Promises a)
-- Mathlib.Geometry.RingedSpace.Basic
/-- The restriction of a section `f` to the basic open of `f` is a unit.  -/
AlgebraicGeometry.RingedSpace.isUnit_res_basicOpen : ∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  (f : ↑(X.presheaf.obj (Opposite.op U))),
  IsUnit ((CategoryTheory.ConcreteCategory.hom (X.presheaf.map (CategoryTheory.homOfLE ⋯).op)) f)
-- Init.Data.Int.LemmasAux
Int.min_assoc : ∀ (a b c : ℤ), min (min a b) c = min a (min b c)
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- In a flatten, dropping all the elements up to an index which is the sum of the lengths of the
first `i` sublists, is the same as taking the join after dropping the first `i` sublists.  -/
List.drop_sum_flatten : ∀ {α : Type u_2} (L : List (List α)) (i : ℕ),
  List.drop (List.take i (List.map List.length L)).sum L.flatten = (List.drop i L).flatten
-- Mathlib.Algebra.Field.Opposite
MulOpposite.unop_ratCast : ∀ {α : Type u_1} [inst : RatCast α] (q : ℚ), MulOpposite.unop ↑q = ↑q
-- Mathlib.Data.Nat.Bits
/-- `ldiff a b` performs bitwise set difference. For each corresponding
pair of bits taken as Booleans, say `aᵢ` and `bᵢ`, it applies the
Boolean operation `aᵢ ∧ ¬bᵢ` to obtain the `iᵗʰ` bit of the result.  -/
Nat.ldiff : ℕ → ℕ → ℕ
-- Mathlib.Analysis.Convex.Strict
StrictConvex.add_smul_sub_mem : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : TopologicalSpace E]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {s : Set E} {x y : E} [AddRightMono 𝕜],
  StrictConvex 𝕜 s → x ∈ s → y ∈ s → x ≠ y → ∀ {t : 𝕜}, 0 < t → t < 1 → x + t • (y - x) ∈ interior s
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} (self : CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct c p f g j) {Z : C}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) (CategoryTheory.CategoryStruct.comp self.f' h) =
    CategoryTheory.CategoryStruct.comp f h
-- Mathlib.NumberTheory.SmoothNumbers
Nat.equivProdNatFactoredNumbers_apply' : ∀ {s : Finset ℕ} {p : ℕ} (hp : Nat.Prime p) (hs : p ∉ s) (x : ℕ × ↑(Nat.factoredNumbers s)),
  ↑((Nat.equivProdNatFactoredNumbers hp hs) x) = p ^ x.1 * ↑x.2