mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.uniformity_def : ∀ {α : Type u_1} [inst : UniformSpace α],
  uniformity (TopologicalSpace.Compacts α) =
    Filter.comap (Prod.map SetLike.coe SetLike.coe) ((uniformity α).lift' hausdorffEntourage)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
IsCyclotomicExtension.Rat.natAbs_discr : ∀ (n : ℕ) (K : Type u) [inst : Field K] [inst_1 : CharZero K] [hn : NeZero n] [hK : IsCyclotomicExtension {n} ℚ K],
  (NumberField.discr K).natAbs = n ^ n.totient / ∏ p ∈ n.primeFactors, p ^ (n.totient / (p - 1))
-- Mathlib.LinearAlgebra.Projection
Submodule.ker_projection : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  (hpq : IsCompl p q), (p.projection q hpq).ker = q
-- Mathlib.Analysis.Calculus.FDeriv.Const
differentiableOn_one : ∀ {𝕜 : 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] {s : Set E} [inst_7 : One F], DifferentiableOn 𝕜 1 s
-- Mathlib.Algebra.PresentedMonoid.Basic
PresentedAddMonoid.inductionOn₃ : ∀ {α₁ : Type u_2} {α₂ : Type u_3} {α₃ : Type u_4} {rels₁ : FreeAddMonoid α₁ → FreeAddMonoid α₁ → Prop}
  {rels₂ : FreeAddMonoid α₂ → FreeAddMonoid α₂ → Prop} {rels₃ : FreeAddMonoid α₃ → FreeAddMonoid α₃ → Prop}
  {δ : PresentedAddMonoid rels₁ → PresentedAddMonoid rels₂ → PresentedAddMonoid rels₃ → Prop}
  (q₁ : PresentedAddMonoid rels₁) (q₂ : PresentedAddMonoid rels₂) (q₃ : PresentedAddMonoid rels₃),
  (∀ (a : FreeAddMonoid α₁) (b : FreeAddMonoid α₂) (c : FreeAddMonoid α₃),
      δ ((PresentedAddMonoid.mk rels₁) a) ((PresentedAddMonoid.mk rels₂) b) ((PresentedAddMonoid.mk rels₃) c)) →
    δ q₁ q₂ q₃
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
CategoryTheory.IsSplitCoequalizer.asCofork_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {h : Y ⟶ Z}
  (t : CategoryTheory.IsSplitCoequalizer f g h), t.asCofork.pt = Z
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_ofBitVec : ∀ (b : BitVec 16), { toBitVec := b }.toUInt8 = { toBitVec := BitVec.setWidth 8 b }
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- Coercion of a `BoundedContinuousFunction` is a `MonoidHom`. Similar to `MonoidHom.coeFn`.  -/
BoundedContinuousFunction.coeFnMonoidHom : {α : Type u} →
  {R : Type u_2} →
    [inst : TopologicalSpace α] →
      [inst_1 : PseudoMetricSpace R] →
        [inst_2 : Monoid R] →
          [inst_3 : BoundedMul R] → [inst_4 : ContinuousMul R] → BoundedContinuousFunction α R →* α → R
-- Mathlib.Analysis.Calculus.ContDiffHolder.Pointwise
ContinuousLinearEquiv.contDiffPointwiseHolderAt_left_comp : ∀ {E : Type u_1} {F : Type u_2} {G : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G] [inst_5 : NormedSpace ℝ G]
  {k : ℕ} {α : ↑unitInterval} {f : E → F} {a : E} (g : F ≃L[ℝ] G),
  ContDiffPointwiseHolderAt k α (⇑g ∘ f) a ↔ ContDiffPointwiseHolderAt k α f a
-- Init.Data.Range.Polymorphic.Nat
Std.instHasRcoIntersectionNat_3 : Std.Rco.HasRcoIntersection ℕ
-- Init.Data.SInt.Lemmas
Int8.toInt64_ne_minValue : ∀ (a : Int8), a.toInt64 ≠ Int64.minValue
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.retraction.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f f_1 : Y ⟶ X) (e_f : f = f_1)
  [hf : CategoryTheory.IsSplitMono f], CategoryTheory.retraction f = CategoryTheory.retraction f_1
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.Arrow.Hom.add_left : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [inst_1 : CategoryTheory.Preadditive T]
  {u v : CategoryTheory.Arrow T} (α β : u ⟶ v),
  CategoryTheory.Arrow.Hom.left (α + β) = CategoryTheory.Arrow.Hom.left α + CategoryTheory.Arrow.Hom.left β
-- Mathlib.RingTheory.Ideal.Operations
Ideal.mem_radical_iff : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R} {r : R}, r ∈ I.radical ↔ ∃ n, r ^ n ∈ I
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- See `MulAction.isBlock_subgroup'` for a version that works for the right action of a group on
itself.  -/
MulAction.isBlock_subgroup : ∀ {G : Type u_1} [inst : Group G] {S : Type u_3} {H : Type u_4} [inst_1 : Group H] [inst_2 : SetLike S H]
  [SubgroupClass S H] {s : S} [inst_4 : MulAction G H] [IsScalarTower G H H], MulAction.IsBlock G ↑s
-- Mathlib.Order.Monotone.Defs
Function.monotone_eval : ∀ {ι : Type u} {α : ι → Type v} [inst : (i : ι) → Preorder (α i)] (i : ι), Monotone (Function.eval i)
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.integral_norm_prod_left : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} [inst_2 : NormedAddCommGroup E] [MeasureTheory.SFinite ν]
  ⦃f : α × β → E⦄,
  MeasureTheory.Integrable f (μ.prod ν) → MeasureTheory.Integrable (fun x => ∫ (y : β), ‖f (x, y)‖ ∂ν) μ
-- Init.Data.Iterators.Lemmas.Basic
/-- Induction principle for finite iterators: One can define a function `f` that maps every
iterator `it` to an element of `motive it` by defining `f it` in terms of the values of `f` on
the plausible successors of `it'.
 -/
Std.Iter.inductSteps : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    [Std.Iterators.Finite α Id] →
      (motive : Std.Iter β → Sort x) →
        ((it : Std.Iter β) →
            ({it' : Std.Iter β} → {out : β} → it.IsPlausibleStep (Std.IterStep.yield it' out) → motive it') →
              ({it' : Std.Iter β} → it.IsPlausibleStep (Std.IterStep.skip it') → motive it') → motive it) →
          (it : Std.Iter β) → motive it
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
AffineSubspace.coe_prod : ∀ {k : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring k] [inst_1 : AddCommGroup V]
  [inst_2 : Module k V] [inst_3 : AddTorsor V P] [inst_4 : AddCommGroup W] [inst_5 : Module k W]
  [inst_6 : AddTorsor W Q] (s : AffineSubspace k P) (t : AffineSubspace k Q), ↑(s.prod t) = ↑s ×ˢ ↑t
-- Mathlib.Algebra.Order.Ring.IsNonarchimedean
/-- Given a nonarchimedean function `α → R`, a function `g : β → α` and a nonempty multiset
`s : Multiset β`, we can always find `b : β` belonging to `s` such that
`f (t.sum g) ≤ f (g b)` .  -/
IsNonarchimedean.multiset_image_add_of_nonempty : ∀ {R : Type u_1} [inst : LinearOrder R] {α : Type u_2} {β : Type u_3} [inst_1 : AddCommMonoid α] [Nonempty β]
  {f : α → R}, IsNonarchimedean f → ∀ (g : β → α) {s : Multiset β}, s ≠ 0 → ∃ b ∈ s, f (Multiset.map g s).sum ≤ f (g b)
-- Mathlib.Algebra.Module.SpanRank
/-- Constructs a generating set with cardinality equal to the `spanFinrank` of the submodule when
the submodule is finitely generated.  -/
Submodule.FG.exists_span_set_encard_eq_spanFinrank : ∀ {R : Type u_1} {M : Type u} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {p : Submodule R M},
  p.FG → ∃ s, s.encard = ↑p.spanFinrank ∧ Submodule.span R s = p
-- Mathlib.GroupTheory.Nilpotent
/-- The `n+1`st term of the upper central series `H i` has underlying set equal to the `x` such
that `⁅x,G⁆ ⊆ H n`.  -/
Subgroup.mem_upperCentralSeries_succ_iff : ∀ {G : Type u_1} [inst : Group G] {n : ℕ} {x : G},
  x ∈ Subgroup.upperCentralSeries G (n + 1) ↔ ∀ (y : G), ⁅x, y⁆ ∈ Subgroup.upperCentralSeries G n
-- Mathlib.Topology.Category.Profinite.Basic
/-- (Implementation) The object part of the `connectedComponents` functor from compact Hausdorff spaces
to Profinite spaces, given by quotienting a space by its connected components.  -/
CompHaus.toProfiniteObj : CompHaus → Profinite
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- Transfer preservation of limits along an equivalence in the shape.  -/
CategoryTheory.Limits.preservesLimitsOfShape_of_equiv : ∀ {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] {J' : Type w₂}
  [inst_3 : CategoryTheory.Category.{w₂', w₂} J'] (e : J ≌ J') (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesLimitsOfShape J F], CategoryTheory.Limits.PreservesLimitsOfShape J' F
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ιMulti_succ_curryLeft : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {n : ℕ} (m : M),
  (ExteriorAlgebra.ιMulti R n.succ).curryLeft m =
    (LinearMap.mulLeft R ((ExteriorAlgebra.ι R) m)).compAlternatingMap (ExteriorAlgebra.ιMulti R n)
-- Mathlib.Topology.UnitInterval
unitInterval.nonneg : ∀ (x : ↑unitInterval), 0 ≤ ↑x
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
/-- Use the more general `hasLimit` lemma instead, see also
`hasPointwiseLeftDerivedFunctorAt_iff`  -/
CategoryTheory.Functor.HasPointwiseLeftDerivedFunctorAt.hasLimit' : ∀ {C : Type u₁} {H : Type u₃} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₃, u₃} H}
  {F : CategoryTheory.Functor C H} {W : CategoryTheory.MorphismProperty C} {X : C}
  [self : F.HasPointwiseLeftDerivedFunctorAt W X], W.Q.HasPointwiseRightKanExtensionAt F (W.Q.obj X)
-- Mathlib.CategoryTheory.Category.Factorisation
/-- The right commuting triangle of the factorization morphism.  -/
CategoryTheory.Factorisation.Hom.h_π_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {d e : CategoryTheory.Factorisation f}
  (self : d.Hom e) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.h (CategoryTheory.CategoryStruct.comp e.π h) =
    CategoryTheory.CategoryStruct.comp d.π h
-- Mathlib.Order.Filter.Partial
/-- Generic "limit of a partial function" predicate. `PTendsto r l₁ l₂` asserts that for every
`l₂`-neighborhood `a`, the `p`-core of `a` is an `l₁`-neighborhood. One generalization of
`Filter.Tendsto` to partial function.  -/
Filter.PTendsto : {α : Type u} → {β : Type v} → (α →. β) → Filter α → Filter β → Prop
-- Mathlib.Algebra.Group.Int.Units
Int.isUnit_ne_iff_eq_neg : ∀ {u v : ℤ}, IsUnit u → IsUnit v → (u ≠ v ↔ u = -v)
-- Mathlib.CategoryTheory.Limits.Lattice
/-- The colimit of a functor from a finite diagram into a `SemilatticeSup` with `OrderBot`
is the supremum of the objects in the image.
 -/
CategoryTheory.Limits.CompleteLattice.finite_colimit_eq_finset_univ_sup : ∀ {α : Type u} {J : Type w} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.FinCategory J]
  [inst_2 : SemilatticeSup α] [inst_3 : OrderBot α] (F : CategoryTheory.Functor J α),
  CategoryTheory.Limits.colimit F = Finset.univ.sup F.obj
-- Init.Data.UInt.Lemmas
UInt16.mod_def : ∀ (a b : UInt16), a % b = { toBitVec := a.toBitVec % b.toBitVec }
-- Mathlib.NumberTheory.Height.Basic
Height.mulHeight.eq_1 : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} (x : ι → K),
  Height.mulHeight x =
    if x = 0 then 1
    else
      (Multiset.map (fun v => ⨆ i, v (x i)) Height.AdmissibleAbsValues.archAbsVal).prod *
        ∏ᶠ (v : ↑Height.AdmissibleAbsValues.nonarchAbsVal), ⨆ i, ↑v (x i)
-- Mathlib.Geometry.Manifold.IsManifold.Basic
IsManifold.instLEInftyCastWithTopENat : ∀ (n : ℕ), ENat.LEInfty ↑n
-- Mathlib.GroupTheory.Index
AddSubgroup.not_finiteIndex_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, ¬H.FiniteIndex ↔ H.index = 0
-- Init.Data.SInt.Bitwise
Int32.or_assoc : ∀ (a b c : Int32), a ||| b ||| c = a ||| (b ||| c)
-- Init.Data.Range.Polymorphic.Stream
Std.PRange.instToStreamRciIterIteratorOfUpwardEnumerable : {α : Type u_1} → [Std.PRange.UpwardEnumerable α] → Std.ToStream (Std.Rci α) (Std.Iter α)
-- Mathlib.Data.Complex.Basic
Complex.neg_re : ∀ (z : ℂ), (-z).re = -z.re
-- Mathlib.Order.OrderIsoNat
Nat.orderEmbeddingOfSet_apply : ∀ {s : Set ℕ} [inst : Infinite ↑s] [inst_1 : DecidablePred fun x => x ∈ s] {n : ℕ},
  (Nat.orderEmbeddingOfSet s) n = ↑(Nat.Subtype.ofNat s n)
-- Mathlib.Order.Defs.Unbundled
refl : ∀ {α : Sort u_1} {r : α → α → Prop} [Std.Refl r] (a : α), r a a
-- Mathlib.SetTheory.Cardinal.Free
/-- A commutative ring can be constructed on any non-empty type.

See also `Infinite.nonempty_field`.  -/
nonempty_commRing : ∀ (α : Type u) [Nonempty α], Nonempty (CommRing α)
-- Mathlib.Analysis.Complex.Basic
Complex.im_eq_zero_iff_isSelfAdjoint : ∀ (x : ℂ), x.im = 0 ↔ IsSelfAdjoint x
-- Mathlib.Data.Nat.Choose.Multinomial
Nat.multinomial.eq_1 : ∀ {α : Type u_1} (s : Finset α) (f : α → ℕ), Nat.multinomial s f = (∑ i ∈ s, f i).factorial / ∏ i ∈ s, (f i).factorial
-- Mathlib.CategoryTheory.WithTerminal.Cone
/-- The extension of a functor to over categories behaves well with compositions.  -/
CategoryTheory.WithTerminal.liftFromOverComp : {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] →
            {X : C} →
              {K : CategoryTheory.Functor J (CategoryTheory.Over X)} →
                {F : CategoryTheory.Functor C D} →
                  CategoryTheory.WithTerminal.liftFromOver.obj (K.comp (CategoryTheory.Over.post F)) ≅
                    (CategoryTheory.WithTerminal.liftFromOver.obj K).comp F
-- Batteries.Tactic.HelpCmd
/-- The command `#help cats` shows all syntax categories that have been defined in the
current environment.
Each syntax has a format like:
```
category command [Lean.Parser.initFn✝]
```
The name of the syntax category in this case is `command`, and `Lean.Parser.initFn✝` is the
name of the declaration that introduced it. (It is often an anonymous declaration like this,
but you can click to go to the definition.) It also shows the doc string if available.

The form `#help cats id` will show only syntax categories that begin with `id`.
 -/
Batteries.Tactic.«command#help_Cats___» : Lean.ParserDescr
-- Mathlib.Algebra.Ring.IsFormallyReal
AddSubsemigroup.mem_sumNonzeroSq : ∀ {R : Type u_1} [inst : AddMonoid R] [inst_1 : Mul R] {s : R}, s ∈ AddSubsemigroup.sumNonzeroSq R ↔ IsSumNonzeroSq s
-- Aesop.Script.GoalWithMVars
Aesop.GoalWithMVars.mvars : Aesop.GoalWithMVars → Std.HashSet Lean.MVarId
-- Mathlib.Algebra.Group.Hom.Defs
AddMonoid.End.instMonoid.eq_1 : ∀ (M : Type u_4) [inst : AddZero M],
  AddMonoid.End.instMonoid M =
    { mul := AddMonoidHom.comp, mul_assoc := ⋯, one := AddMonoidHom.id M, one_mul := ⋯, mul_one := ⋯,
      npow := fun n f => AddMonoidHom.copy (npowRec n f) (⇑f)^[n] ⋯, npow_zero := ⋯, npow_succ := ⋯ }
-- Std.Time.Zoned.Database.TzIf
_private.Std.Time.Zoned.Database.TzIf.0.Std.Time.TimeZone.TZif.parseTZifV2 : Std.Internal.Parsec.ByteArray.Parser (Option Std.Time.TimeZone.TZif.TZifV2)
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.callHierarchyProvider : Lean.Lsp.ServerCapabilities → Bool
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_zero_left : ∀ {ι : Type u_1} {𝕜 : Type u_3} {E : ι → Type u_4} [inst : Fintype ι] [inst_1 : RCLike 𝕜]
  [inst_2 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_3 : (i : ι) → InnerProductSpace 𝕜 (E i)] (w : ι → ℝ)
  (g : (i : ι) → E i), ⟪0, g⟫_[𝕜, w] = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_mul_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Mul α] {s t : Finset α}, (s * t).card ≤ s.card * t.card
-- Mathlib.Tactic.NormNum.NatFib
Mathlib.Meta.NormNum.isFibAux_zero : Mathlib.Meta.NormNum.IsFibAux 0 0 1
-- Mathlib.Logic.Denumerable
_private.Mathlib.Logic.Denumerable.0.Nat.Subtype.ofNat.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Init.Data.Vector.Count
Vector.countP_flatten : ∀ {α : Type u_1} {p : α → Bool} {m n : ℕ} {xss : Vector (Vector α m) n},
  Vector.countP p xss.flatten = (Vector.map (Vector.countP p) xss).sum
-- Init.Data.List.Nat.Sum
List.sum_replicate_nat : ∀ {n a : ℕ}, (List.replicate n a).sum = n * a
-- Mathlib.FieldTheory.RatFunc.Luroth
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.swap_Φ_natDegree_eq_θ_natDegree : ∀ {K : Type u_1} [inst : Field K] {E : IntermediateField K (RatFunc K)},
  E ≠ ⊥ → (Polynomial.Bivariate.swap (RatFunc.Luroth.Φ✝ E)).natDegree = (RatFunc.Luroth.θ✝ E).natDegree
-- Mathlib.Algebra.QuaternionBasis
QuaternionAlgebra.Basis.i_mul_i : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {c₁ c₂ c₃ : R}
  (self : QuaternionAlgebra.Basis A c₁ c₂ c₃), self.i * self.i = c₁ • 1 + c₂ • self.i
-- Mathlib.Order.OmegaCompletePartialOrder
OmegaCompletePartialOrder.ContinuousHom.ωScottContinuous_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : OmegaCompletePartialOrder α]
  [inst_1 : OmegaCompletePartialOrder β] [inst_2 : OmegaCompletePartialOrder γ] {f : α → β →𝒄 γ},
  OmegaCompletePartialOrder.ωScottContinuous f →
    ∀ {g : α → β},
      OmegaCompletePartialOrder.ωScottContinuous g → OmegaCompletePartialOrder.ωScottContinuous fun x => (f x) (g x)
-- Mathlib.Analysis.InnerProductSpace.TwoDim
/-- The area form is invariant under pullback by a positively-oriented isometric automorphism.  -/
Orientation.areaForm_comp_linearIsometryEquiv : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (φ : E ≃ₗᵢ[ℝ] E),
  0 < LinearMap.det ↑φ.toLinearEquiv → ∀ (x y : E), (o.areaForm (φ x)) (φ y) = (o.areaForm x) y
-- Mathlib.Tactic.Translate.TagUnfoldBoundary
_private.Mathlib.Tactic.Translate.TagUnfoldBoundary.0.Mathlib.Tactic.Translate.CastKind.unfoldFun.sizeOf_spec : sizeOf Mathlib.Tactic.Translate.CastKind.unfoldFun✝ = 1
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
MonCat.FilteredColimits.colimitOne.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] (F : CategoryTheory.Functor J MonCat)
  [inst_1 : CategoryTheory.IsFiltered J],
  MonCat.FilteredColimits.colimitOne F = { one := MonCat.FilteredColimits.M.mk F ⟨⋯.some, 1⟩ }
-- Mathlib.GroupTheory.OrderOfElement
Commute.orderOf_mul_dvd_mul_orderOf : ∀ {G : Type u_1} [inst : Monoid G] {x y : G}, Commute x y → orderOf (x * y) ∣ orderOf x * orderOf y
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.addLinearEquiv_apply_snd : ∀ {m n : ℕ} {R : Type u_2} [inst : Ring R] (f : ↥(Polynomial.degreeLT R (m + n))),
  ↑((Polynomial.degreeLT.addLinearEquiv R m n) f).2 = ↑f /ₘ Polynomial.X ^ m
-- Mathlib.Data.Nat.Factorization.PrimePow
/-- An equivalent definition for prime powers: `n` is a prime power iff there is a unique prime
dividing it.  -/
isPrimePow_iff_unique_prime_dvd : ∀ {n : ℕ}, IsPrimePow n ↔ ∃! p, Nat.Prime p ∧ p ∣ n
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degreeOf_X_pow_of_ne : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {i j : σ} (k : ℕ),
  i ≠ j → MvPolynomial.degreeOf i (MvPolynomial.X j ^ k) = 0
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.h₀_f_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (self : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂) {Z : C}
  (h : S₂.X₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.h₀ (CategoryTheory.CategoryStruct.comp S₂.f h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_cancelVar : ∀ {α : Type u_1} [inst : Lean.Grind.CommRing α] (ctx : Lean.Grind.CommRing.Context α) (p : Lean.Grind.CommRing.Poly)
  (c : ℤ) (x : Lean.Grind.CommRing.Var),
  c ≠ 0 →
    ↑c * Lean.Grind.CommRing.Var.denote ctx x = 1 →
      Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.cancelVar c x p) =
        Lean.Grind.CommRing.Poly.denote ctx p
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Ric.toArray_iter : ∀ {α : Type u_1} [inst : Std.PRange.Least? α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] [inst_5 : Std.Rxc.IsAlwaysFinite α]
  [inst_6 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Ric α}, r.iter.toArray = r.toArray
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote_norm : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote ctx p.norm = Int.Internal.Linear.Poly.denote ctx p
-- Mathlib.NumberTheory.Pell
Pell.Solution₁.x_inv : ∀ {d : ℤ} (a : Pell.Solution₁ d), a⁻¹.x = a.x
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_le_zero_iff : ∀ {x : ENNReal}, x.log ≤ 0 ↔ x ≤ 1
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.MorphismProperty.transfiniteCompositionsOfShape_le_llp_rlp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (J : Type w)
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J] [inst_4 : WellFoundedLT J],
  W.transfiniteCompositionsOfShape J ≤ W.rlp.llp
-- Lean.Meta.Tactic.Simp.SimpTheorems
Lean.Meta.SimpEntry.toUnfoldThms.inj : ∀ {a : Lean.Name} {a_1 : Array Lean.Name} {a_2 : Lean.Name} {a_3 : Array Lean.Name},
  Lean.Meta.SimpEntry.toUnfoldThms a a_1 = Lean.Meta.SimpEntry.toUnfoldThms a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.braiding_inv_tensorUnit_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X : C),
  (β_ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) X).inv =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).hom
      (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).inv
-- Mathlib.Tactic.TermCongr
/-- The left-hand side of the congruence result.  -/
Mathlib.Tactic.TermCongr.CongrResult.lhs : Mathlib.Tactic.TermCongr.CongrResult → Lean.Expr
-- Mathlib.CategoryTheory.Iso
CategoryTheory.IsIso.hom_inv_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) [I : CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.inv f) = CategoryTheory.CategoryStruct.id X
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
/-- Given a colimit cocone over the underlying modules, equipping the cocone point with
the coinduced topology gives a colimit cocone in `TopModuleCat R`.  -/
TopModuleCat.isColimit : {R : Type u} →
  [inst : Ring R] →
    [inst_1 : TopologicalSpace R] →
      {J : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_1, u_2} J] →
          {F : CategoryTheory.Functor J (TopModuleCat R)} →
            {c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget₂ (TopModuleCat R) (ModuleCat R)))} →
              CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsColimit (TopModuleCat.ofCocone c)
-- Mathlib.Analysis.SpecialFunctions.Gaussian.GaussianIntegral
integrable_exp_neg_mul_sq : ∀ {b : ℝ}, 0 < b → MeasureTheory.Integrable (fun x => Real.exp (-b * x ^ 2)) MeasureTheory.volume
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left_symm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  {P Q : CategoryTheory.Functor Cᵒᵖ A} {M : A} [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (f : P ⟶ Q) (g : Q ⟶ Φ.skyscraperPresheaf M) {Z : A} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv.symm (CategoryTheory.CategoryStruct.comp f g)) h =
    CategoryTheory.CategoryStruct.comp (Φ.presheafFiber.map f)
      (CategoryTheory.CategoryStruct.comp (Φ.skyscraperPresheafHomEquiv.symm g) h)
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.tensor_eq_tensor : ∀ {C : Type u} {X Y : CategoryTheory.FreeMonoidalCategory C},
  X.tensor Y = CategoryTheory.MonoidalCategoryStruct.tensorObj X Y
-- Lean.Elab.PreDefinition.Structural.IndGroupInfo
Lean.Elab.Structural.instReprIndGroupInst.repr : Lean.Elab.Structural.IndGroupInst → ℕ → Std.Format
-- Mathlib.Algebra.Order.Floor.Defs
Int.floor_int : Int.floor = id