mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.instEtaleUniversalCoprimeFactorizationRing : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (m k : ℕ) (hn : n = m + k) (p : Polynomial.MonicDegreeEq R n),
  Algebra.Etale R (Polynomial.UniversalCoprimeFactorizationRing m k hn p)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.filterMap_equiv_map : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {f : α → β → γ}, (Std.TreeMap.filterMap (fun k v => some (f k v)) t).Equiv (Std.TreeMap.map f t)
-- Lean.Util.Trace
Lean.TraceState.mk.injEq : ∀ (tid : UInt64) (traces : Lean.PersistentArray Lean.TraceElem) (tid_1 : UInt64)
  (traces_1 : Lean.PersistentArray Lean.TraceElem),
  ({ tid := tid, traces := traces } = { tid := tid_1, traces := traces_1 }) = (tid = tid_1 ∧ traces = traces_1)
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.Adj.symm : ∀ {V : Type u} {G : SimpleGraph V} {u v : V}, G.Adj u v → G.Adj v u
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.AbsolutelyContinuous.smul : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_4} {N : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N] {R : Type u_6}
  [inst_4 : Semiring R] [inst_5 : DistribMulAction R M] [inst_6 : ContinuousConstSMul R M] {r : R}
  {v : MeasureTheory.VectorMeasure α M} {w : MeasureTheory.VectorMeasure α N},
  v.AbsolutelyContinuous w → (r • v).AbsolutelyContinuous w
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.fieldEquivOfAlgEquivHom.congr_simp : ∀ {A : Type u_8} {B : Type u_9} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (K : Type u_10)
  (L : Type u_11) [inst_3 : Field K] [inst_4 : Field L] [inst_5 : Algebra A K] [inst_6 : Algebra B L]
  [inst_7 : IsFractionRing A K] [inst_8 : IsFractionRing B L] [inst_9 : Algebra A L] [inst_10 : IsScalarTower A B L]
  [inst_11 : Algebra K L] [inst_12 : IsScalarTower A K L],
  IsFractionRing.fieldEquivOfAlgEquivHom K L = IsFractionRing.fieldEquivOfAlgEquivHom K L
-- Mathlib.Algebra.Opposites
AddOpposite.instInhabited : {α : Type u_1} → [Inhabited α] → Inhabited αᵃᵒᵖ
-- Lean.Parser
Lean.PrettyPrinter.Formatter.ident.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Algebra.Polynomial.Basic
/-- **Alias** of `Polynomial.support_binomial_subset`. -/
Polynomial.support_binomial' : ∀ {R : Type u} [inst : Semiring R] (k m : ℕ) (x y : R),
  (Polynomial.C x * Polynomial.X ^ k + Polynomial.C y * Polynomial.X ^ m).support ⊆ {k, m}
-- Mathlib.AlgebraicGeometry.Morphisms.FormallyUnramified
AlgebraicGeometry.FormallyUnramified.instIsStableUnderCompositionScheme : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.FormallyUnramified
-- Mathlib.Algebra.Group.Basic
div_eq_mul_one_div : ∀ {G : Type u_3} [inst : DivInvMonoid G] (a b : G), a / b = a * (1 / b)
-- Init.Data.UInt.Lemmas
UInt64.ofNat_lt_iff : ∀ {n : UInt64} {m : ℕ}, m < UInt64.size → (UInt64.ofNat m < n ↔ m < n.toNat)
-- Mathlib.CategoryTheory.Localization.Bifunctor
CategoryTheory.Localization.lift₂NatTrans.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D₁ : Type u_3} {D₂ : Type u_4} {E : Type u_5}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D₁] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₂]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} E] (L₁ : CategoryTheory.Functor C₁ D₁)
  (L₂ : CategoryTheory.Functor C₂ D₂) (W₁ : CategoryTheory.MorphismProperty C₁)
  (W₂ : CategoryTheory.MorphismProperty C₂) [inst_5 : L₁.IsLocalization W₁] [inst_6 : L₂.IsLocalization W₂]
  [inst_7 : W₁.ContainsIdentities] [inst_8 : W₂.ContainsIdentities]
  (F₁ F₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ E))
  (F₁' F₂' : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ E))
  [inst_9 : CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₁ F₁']
  [inst_10 : CategoryTheory.Localization.Lifting₂ L₁ L₂ W₁ W₂ F₂ F₂'] (τ τ_1 : F₁ ⟶ F₂),
  τ = τ_1 →
    CategoryTheory.Localization.lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' τ =
      CategoryTheory.Localization.lift₂NatTrans L₁ L₂ W₁ W₂ F₁ F₂ F₁' F₂' τ_1
-- Mathlib.Algebra.Group.Action.Defs
smul_assoc : ∀ {α : Type u_5} {M : Type u_9} {N : Type u_10} [inst : SMul M N] [inst_1 : SMul N α] [inst_2 : SMul M α]
  [IsScalarTower M N α] (x : M) (y : N) (z : α), (x • y) • z = x • y • z
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.next_eq' : ∀ {ι : Type u_1} (c : ComplexShape ι) {i j : ι}, c.Rel i j → c.next i = j
-- Mathlib.Order.Completion
DedekindCut.ext_iff : ∀ {α : Type u_1} [inst : Preorder α] {A B : DedekindCut α}, A = B ↔ A.left = B.left
-- Init.Data.UInt.Bitwise
instAssociativeUInt16HOr : Std.Associative fun x1 x2 => x1 ||| x2
-- Mathlib.Tactic.Simproc.ExistsAndEq
ExistsAndEq.GoTo.left.sizeOf_spec : sizeOf ExistsAndEq.GoTo.left = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_erase : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {k a : α}, (m.erase k).contains a = (!k == a && m.contains a)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.LocallyFree
SheafOfModules.IsLocallyFree.exists_isLocallyFreeData : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} {inst_1 : ∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat}
  {inst_2 : ∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat} {M : SheafOfModules R}
  [self : M.IsLocallyFree], ∃ q, q.IsLocallyFreeData
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The underlying type of the colimit of a diagram in `CommRingCat`.
 -/
CommRingCat.Colimits.ColimitType : {J : Type v} → [inst : CategoryTheory.SmallCategory J] → CategoryTheory.Functor J CommRingCat → Type v
-- Mathlib.CategoryTheory.GradedObject.Unitor
CategoryTheory.GradedObject.mapBifunctorLeftUnitor_naturality_assoc : ∀ {C : Type u_1} {D : Type u_2} {I : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : Zero I] [inst_3 : DecidableEq I]
  [inst_4 : CategoryTheory.Limits.HasInitial C] (F : CategoryTheory.Functor C (CategoryTheory.Functor D D)) (X : C)
  (e : F.obj X ≅ CategoryTheory.Functor.id D)
  [inst_5 : ∀ (Y : D), CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C) (F.flip.obj Y)]
  (p : I × J → J) (hp : ∀ (j : J), p (0, j) = j) {Y Y' : CategoryTheory.GradedObject J D} (φ : Y ⟶ Y')
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
          Y).HasMap
      p]
  [inst_7 :
    (((CategoryTheory.GradedObject.mapBifunctor F I J).obj ((CategoryTheory.GradedObject.single₀ I).obj X)).obj
          Y').HasMap
      p]
  {Z : CategoryTheory.GradedObject J D} (h : Y' ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GradedObject.mapBifunctorMapMap F p
        (CategoryTheory.CategoryStruct.id ((CategoryTheory.GradedObject.single₀ I).obj X)) φ)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y').hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.GradedObject.mapBifunctorLeftUnitor F X e p hp Y).hom
      (CategoryTheory.CategoryStruct.comp φ h)
-- Mathlib.RingTheory.Polynomial.Basic
Polynomial.Monic.geom_sum' : ∀ {R : Type u} [inst : Semiring R] {P : Polynomial R},
  P.Monic → 0 < P.degree → ∀ {n : ℕ}, n ≠ 0 → (∑ i ∈ Finset.range n, P ^ i).Monic
-- Mathlib.Topology.Algebra.Module.LocallyConvex
/-- A `LocallyConvexSpace` is a topological semimodule over an ordered semiring in which convex
neighborhoods of a point form a neighborhood basis at that point.  -/
LocallyConvexSpace : (𝕜 : Type u_1) →
  (E : Type u_2) →
    [inst : Semiring 𝕜] → [PartialOrder 𝕜] → [inst_2 : AddCommMonoid E] → [Module 𝕜 E] → [TopologicalSpace E] → Prop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintClientCapabilities : Type
-- Std.Http.Data.Status
Std.Http.Status.resetContent.sizeOf_spec : sizeOf Std.Http.Status.resetContent = 1
-- Init.Data.String.Basic
/-- Returns the character at position `p` of a string. Panics if `p` is not a valid position.

See `String.pos?` and `String.Pos.get` for a safer alternative.

This function is overridden with an efficient implementation in runtime code. See
`String.utf8GetAux` for the reference implementation.

This is a legacy function. The recommended alternative is `String.Pos.get`, combined with
`String.pos!` or another means of obtaining a `String.Pos`.

Examples
* `"abc".get! ⟨1⟩ = 'b'`
 -/
String.Pos.Raw.get! : String → String.Pos.Raw → Char
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.AEStronglyMeasurable.of_comp_snd : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} {X : Type u_4} [inst_2 : TopologicalSpace X] {f : β → X} [MeasureTheory.SFinite ν],
  MeasureTheory.AEStronglyMeasurable (fun x => f x.2) (μ.prod ν) → μ ≠ 0 → MeasureTheory.AEStronglyMeasurable f ν
-- Mathlib.MeasureTheory.Measure.Haar.Extension
/-- If `φ : A →* B` and `ψ : B →* C` define a short exact sequence of topological groups, then we
can define a Haar measure on `B` induced by the Haar measures on `A` and `C`.  -/
TopologicalGroup.IsSES.inducedMeasure : {A : Type u_1} →
  {B : Type u_2} →
    {C : Type u_3} →
      [inst : Group A] →
        [inst_1 : Group B] →
          [inst_2 : Group C] →
            [inst_3 : TopologicalSpace A] →
              [inst_4 : TopologicalSpace B] →
                [inst_5 : TopologicalSpace C] →
                  {φ : A →* B} →
                    {ψ : B →* C} →
                      TopologicalGroup.IsSES φ ψ →
                        [IsTopologicalGroup A] →
                          [IsTopologicalGroup B] →
                            [inst_8 : MeasurableSpace A] →
                              [BorelSpace A] →
                                (μA : MeasureTheory.Measure A) →
                                  [hμA : μA.IsHaarMeasure] →
                                    [IsTopologicalGroup C] →
                                      [LocallyCompactSpace B] →
                                        [inst : MeasurableSpace C] →
                                          [BorelSpace C] →
                                            (μC : MeasureTheory.Measure C) →
                                              [hμC : μC.IsHaarMeasure] →
                                                [T2Space B] →
                                                  [inst : MeasurableSpace B] → [BorelSpace B] → MeasureTheory.Measure B
-- Std.Data.DTreeMap.Internal.WF.Lemmas
/-- Internal implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.SameKeys.leaf : ∀ {α : Type u} {β : α → Type v} {β' : α → Type u_1},
  Std.DTreeMap.Internal.Impl.leaf.SameKeys Std.DTreeMap.Internal.Impl.leaf
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.le_floor_map_map_zero : ∀ (f g : CircleDeg1Lift), ⌊f 0⌋ + ⌊g 0⌋ ≤ ⌊f (g 0)⌋
-- Init.Data.UInt.Lemmas
UInt32.toUInt8_div : ∀ (a b : UInt32), a < 256 → b < 256 → (a / b).toUInt8 = a.toUInt8 / b.toUInt8
-- Init.Data.Vector.Range
Vector.getElem?_range' : ∀ {start size step i : ℕ}, (Vector.range' start size step)[i]? = if i < size then some (start + step * i) else none
-- Std.Time.Zoned.Database.Basic
Std.Time.Database.mk : {α : Type} → (α → String → IO Std.Time.TimeZone.ZoneRules) → (α → IO Std.Time.TimeZone.ZoneRules) → Std.Time.Database α
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.id_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (x : E.I₀),
  (CategoryTheory.CategoryStruct.id E).h₀ x = CategoryTheory.CategoryStruct.id (E.X x)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure.below.of_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)]
  {motive : (a : C) → P.colimitsClosure J a → Prop} {X Y : C} (e : X ≅ Y) (hX : P.colimitsClosure J X),
  CategoryTheory.ObjectProperty.colimitsClosure.below hX →
    motive X hX → CategoryTheory.ObjectProperty.colimitsClosure.below ⋯
-- Std.Data.ExtDHashMap.Basic
Std.ExtDHashMap.instInsertSigmaOfEquivBEqOfLawfulHashable : {α : Type u} →
  {β : α → Type v} →
    {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Insert ((a : α) × β a) (Std.ExtDHashMap α β)
-- Mathlib.AlgebraicTopology.ModelCategory.FundamentalLemma
/-- The map `LeftHomotopyClass X Y → (L.obj X ⟶ L.obj Y)` when `L` is
a localization functor with respect to `weakEquivalences C`.  -/
HomotopicalAlgebra.leftHomotopyClassToHom : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] →
      {H : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} H] →
          (L : CategoryTheory.Functor C H) →
            [L.IsLocalization (HomotopicalAlgebra.weakEquivalences C)] →
              {X Y : C} → HomotopicalAlgebra.LeftHomotopyClass X Y → (L.obj X ⟶ L.obj Y)
-- Mathlib.Data.Set.Finite.Basic
Set.finite_option : ∀ {α : Type u} {s : Set (Option α)}, s.Finite ↔ {x | some x ∈ s}.Finite
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.mem_skeletonOfMono_obj_iff_of_nonDegenerate : ∀ {X Y : SSet} (i : X ⟶ Y) {d : ℕ} (x : ↑(Y.nonDegenerate d)) (n : ℕ),
  ↑x ∈ ((SSet.skeletonOfMono i) n).obj (Opposite.op { len := d }) ↔
    ↑x ∈ Set.range ⇑(CategoryTheory.ConcreteCategory.hom (i.app (Opposite.op { len := d }))) ∨ d < n
-- Mathlib.Algebra.Order.Group.Synonym
isLeftRegular_ofDual : ∀ {α : Type u_1} [inst : Monoid α] {a : αᵒᵈ}, IsLeftRegular (OrderDual.ofDual a) ↔ IsLeftRegular a
-- Mathlib.Algebra.Group.Equiv.Opposite
AddEquiv.opOp_apply : ∀ (M : Type u_3) [inst : Add M] (a : M), (AddEquiv.opOp M) a = AddOpposite.op (AddOpposite.op a)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.instDecidableEq : {k : Type u_1} →
  {G : Type u_2} → [inst : AddCommMonoid k] → [DecidableEq G] → [DecidableEq k] → DecidableEq (SkewMonoidAlgebra k G)
-- Mathlib.RingTheory.Localization.BaseChange
/-- `A[M⁻¹] ⊗[R] S` is the localization of `A ⊗[R] S` at `M`.  -/
IsLocalization.tensorProduct_tensorProduct : ∀ (R : Type u_7) (S : Type u_8) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {A : Type u_9}
  [inst_3 : CommSemiring A] [inst_4 : Algebra R A] (M : Submonoid A) (B : Type u_10) [inst_5 : CommSemiring B]
  [inst_6 : Algebra R B] [inst_7 : Algebra A B] [inst_8 : IsScalarTower R A B] [IsLocalization M B]
  [inst_10 : Algebra (TensorProduct R A S) (TensorProduct R B S)]
  [IsScalarTower A (TensorProduct R A S) (TensorProduct R B S)],
  (algebraMap (TensorProduct R A S) (TensorProduct R B S)).comp Algebra.TensorProduct.includeRight.toRingHom =
      Algebra.TensorProduct.includeRight.toRingHom →
    IsLocalization (Algebra.algebraMapSubmonoid (TensorProduct R A S) M) (TensorProduct R B S)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.length_eq : ∀ {α : Type u} {β : α → Type v} {l : Std.DHashMap.Internal.AssocList α β}, l.length = l.toList.length
-- Mathlib.RingTheory.Perfection
PerfectionMap.lift_symm_apply : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (R : Type u₁) [inst_1 : CommSemiring R] [inst_2 : CharP R p]
  [inst_3 : PerfectRing R p] (S : Type u₂) [inst_4 : CommSemiring S] [inst_5 : CharP S p] (P : Type u₃)
  [inst_6 : CommSemiring P] [inst_7 : CharP P p] [inst_8 : PerfectRing P p] (π : P →+* S) (m : PerfectionMap p π)
  (f : R →+* P), (PerfectionMap.lift p R S P π m).symm f = π.comp f
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.orderTop : {C : Type u₁} → [inst : CategoryTheory.Category.{v₁, u₁} C] → {X : C} → OrderTop (CategoryTheory.Subobject X)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_eq_singleton : ∀ {m n : ℤ}, n = m → (m...=n).toArray = #[m]
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
IsContMDiffRiemannianBundle.of_le : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {n n' : WithTop ℕ∞} {B : Type u_3}
  [inst_3 : TopologicalSpace B] [inst_4 : ChartedSpace HB B] {F : Type u_4} [inst_5 : NormedAddCommGroup F]
  [inst_6 : NormedSpace ℝ F] {E : B → Type u_5} [inst_7 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_8 : (x : B) → NormedAddCommGroup (E x)] [inst_9 : (x : B) → InnerProductSpace ℝ (E x)]
  [inst_10 : FiberBundle F E] [inst_11 : VectorBundle ℝ F E] [h : IsContMDiffRiemannianBundle IB n F E],
  n' ≤ n → IsContMDiffRiemannianBundle IB n' F E
-- Mathlib.NumberTheory.SmoothNumbers
Nat.smoothNumbers.eq_1 : ∀ (n : ℕ), n.smoothNumbers = {m | m ≠ 0 ∧ ∀ p ∈ m.primeFactorsList, p < n}
-- Mathlib.Order.Filter.ENNReal
ENNReal.limsup_add_le : ∀ {α : Type u_1} {f : Filter α} [CountableInterFilter f] (u v : α → ENNReal),
  Filter.limsup (u + v) f ≤ Filter.limsup u f + Filter.limsup v f
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.Equivalence.unop_inverse : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (e : Cᵒᵖ ≌ Dᵒᵖ), e.unop.inverse = e.inverse.unop
-- Init.Data.Int.Order
Int.pos_of_mul_neg_left : ∀ {a b : ℤ}, a * b < 0 → b < 0 → 0 < a
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.NatIso.naturality_2 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} {X Y : C} (α : F ≅ G) (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (α.hom.app X) (CategoryTheory.CategoryStruct.comp (G.map f) (α.inv.app Y)) =
    F.map f
-- Mathlib.Geometry.Euclidean.Sphere.Power
/-- A point lies on the sphere if and only if its power with respect to
the sphere is zero.  -/
EuclideanGeometry.Sphere.power_eq_zero_iff_mem_sphere : ∀ {P : Type u_2} [inst : MetricSpace P] {s : EuclideanGeometry.Sphere P} {p : P}, 0 ≤ s.radius → (s.power p = 0 ↔ p ∈ s)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.piₗᵢ_apply : ∀ (𝕜 : Type u) {ι : Type v} (E : ι → Type wE) [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] [inst_3 : Fintype ι]
  {ι' : Type v'} [inst_4 : Fintype ι'] {E' : ι' → Type wE'} [inst_5 : (i' : ι') → NormedAddCommGroup (E' i')]
  [inst_6 : (i' : ι') → NormedSpace 𝕜 (E' i')] (a : (i : ι') → ContinuousMultilinearMap 𝕜 E (E' i)),
  (ContinuousMultilinearMap.piₗᵢ 𝕜 E) a = ContinuousMultilinearMap.pi a
-- Mathlib.CategoryTheory.Idempotents.KaroubiKaroubi
CategoryTheory.Idempotents.KaroubiKaroubi.instAdditiveKaroubiInverse : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C],
  (CategoryTheory.Idempotents.KaroubiKaroubi.inverse C).Additive
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
FractionalIdeal.inv_le_inv_iff : ∀ {A : Type u_2} {K : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : IsDedekindDomain A]
  [inst_3 : Algebra A K] [inst_4 : IsFractionRing A K] {I J : FractionalIdeal (nonZeroDivisors A) K},
  I ≠ 0 → J ≠ 0 → (I⁻¹ ≤ J⁻¹ ↔ J ≤ I)
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- A nonarchimedean seminorm on an additive group `G` is a function `f : G → ℝ` that preserves
zero, is nonarchimedean and such that `f (-x) = f x` for all `x`.  -/
NonarchAddGroupSeminorm : (G : Type u_6) → [AddGroup G] → Type u_6
-- Mathlib.Data.Int.GCD
Int.lcm_def : ∀ (i j : ℤ), i.lcm j = i.natAbs.lcm j.natAbs
-- Mathlib.Algebra.Algebra.Defs
/-- To prove two algebra structures on a fixed `[CommSemiring R] [Semiring A]` agree,
it suffices to check the `algebraMap`s agree.
 -/
Algebra.algebra_ext : ∀ {R : Type u_2} [inst : CommSemiring R] {A : Type u_3} [inst_1 : Semiring A] (P Q : Algebra R A),
  (∀ (r : R), (algebraMap R A) r = (algebraMap R A) r) → P = Q
-- Init.Data.Nat.Basic
Nat.mul_add_one : ∀ (n m : ℕ), n * (m + 1) = n * m + n
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
/-- `HasSumUniformly f g` means that
the sum `∑ i, f i b` converges uniformly (wrt `b`) to `g`.  -/
HasSumUniformly : {α : Type u_1} → {β : Type u_2} → {ι : Type u_3} → [AddCommMonoid α] → (ι → β → α) → (β → α) → [UniformSpace α] → Prop
-- Lean.Expr
_private.Lean.Expr.0.Lean.intNegFn : Lean.Expr
-- Lean.Server.Requests
Lean.Server.RequestM.bindRequestTaskCheap : {α : Type u_1} →
  {β : Type} →
    Lean.Server.RequestTask α →
      (α → Lean.Server.RequestM (Lean.Server.RequestTask β)) → Lean.Server.RequestM (Lean.Server.RequestTask β)
-- Mathlib.Algebra.Module.FinitePresentation
/-- An alternative version of `Module.FinitePresentation.exists_fin` that provides a right exact
sequence.  -/
Module.FinitePresentation.exists_fin' : ∀ (R : Type u) (M : Type u_1) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [fp : Module.FinitePresentation R M], ∃ n m f g, Function.Surjective ⇑f ∧ Function.Exact ⇑g ⇑f
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.σ_injective : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι), Function.Injective P.σ
-- Mathlib.Data.Nat.GCD.Basic
Nat.gcd_greatest : ∀ {a b d : ℕ}, d ∣ a → d ∣ b → (∀ (e : ℕ), e ∣ a → e ∣ b → e ∣ d) → d = a.gcd b
-- Mathlib.GroupTheory.QuotientGroup.Defs
/-- The congruence relation generated by a normal subgroup.  -/
QuotientGroup.con : {G : Type u_1} → [inst : Group G] → (N : Subgroup G) → [nN : N.Normal] → Con G
-- Mathlib.Algebra.Polynomial.FieldDivision
/-- The normalized factors of a polynomial over a field times its leading coefficient give
the polynomial.
 -/
Polynomial.leadingCoeff_mul_prod_normalizedFactors : ∀ {R : Type u} [inst : Field R] [inst_1 : DecidableEq R] (a : Polynomial R),
  Polynomial.C a.leadingCoeff * (UniqueFactorizationMonoid.normalizedFactors a).prod = a
-- Init.Data.Char.Basic
/-- Determines if the given integer is a valid [Unicode scalar value](https://www.unicode.org/glossary/#unicode_scalar_value).

Note that values in `[0xd800, 0xdfff]` are reserved for [UTF-16 surrogate pairs](https://en.wikipedia.org/wiki/Universal_Character_Set_characters#Surrogates).
 -/
isValidChar : UInt32 → Prop
-- Init.Data.BitVec.Lemmas
BitVec.rotateLeftAux.eq_1 : ∀ {w : ℕ} (x : BitVec w) (n : ℕ), x.rotateLeftAux n = x <<< n ||| x >>> (w - n)
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_iff_existsUnique_inv_mul_mem : ∀ {G : Type u_1} [inst : Group G] {S T : Set G}, Subgroup.IsComplement S T ↔ ∀ (g : G), ∃! s, (↑s)⁻¹ * g ∈ T
-- Mathlib.AlgebraicTopology.SimplexCategory.Rev
SimplexCategory.rev_obj : ∀ (n : SimplexCategory), SimplexCategory.rev.obj n = n
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
SimpleGraph.ofNat_hadamard_adjMatrix : ∀ (α : Type u_1) {V : Type u_2} (G : SimpleGraph V) [inst : DecidableRel G.Adj] [inst_1 : DecidableEq V]
  [inst_2 : MulZeroOneClass α] [inst_3 : NatCast α] (a : ℕ) [inst_4 : a.AtLeastTwo],
  (OfNat.ofNat a).hadamard (SimpleGraph.adjMatrix α G) = 0
-- Mathlib.Algebra.Module.Submodule.RestrictScalars
Submodule.restrictScalars_sInf : ∀ (S : Type u_1) {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Semiring S]
  [inst_3 : Module S M] [inst_4 : Module R M] [inst_5 : SMul S R] [inst_6 : IsScalarTower S R M]
  (s : Set (Submodule R M)), Submodule.restrictScalars S (sInf s) = sInf (Submodule.restrictScalars S '' s)
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.zsmul_hom : ∀ {k : Type u} {G : Type v} [inst : Semiring k] [inst_1 : Monoid G] {A B : Rep.{w, u, v} k G} (f : A ⟶ B) (n : ℤ),
  Rep.Hom.hom (n • f) = n • Rep.Hom.hom f