mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- Assume that `w.Completion` forms an algebra over `v.Completion` with continuous scalar action,
such that `IsScalarTower K v.Completion w.Completion`.
If `w.embedding : L →+* ℂ` extends `v.embedding : K →+* ℂ`, then the corresponding embeddings
to completions are also extensions.  -/
NumberField.InfinitePlace.Completion.liesOver_extensionEmbedding : ∀ {K : Type u_1} [inst : Field K] {L : Type u_2} [inst_1 : Field L] [inst_2 : Algebra K L]
  (w : NumberField.InfinitePlace L) (v : NumberField.InfinitePlace K) [inst_3 : Algebra v.Completion w.Completion]
  [IsScalarTower K v.Completion w.Completion] [ContinuousSMul v.Completion w.Completion]
  [NumberField.ComplexEmbedding.LiesOver w.embedding v.embedding],
  NumberField.ComplexEmbedding.LiesOver (NumberField.InfinitePlace.Completion.extensionEmbedding w)
    (NumberField.InfinitePlace.Completion.extensionEmbedding v)
-- Mathlib.AlgebraicGeometry.Morphisms.SurjectiveOnStalks
AlgebraicGeometry.SurjectiveOnStalks.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.SurjectiveOnStalks (CategoryTheory.CategoryStruct.comp f g)],
  AlgebraicGeometry.SurjectiveOnStalks f
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
CategoryTheory.Limits.PreservesLimit.mk : ∀ {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},
  (∀ {c : CategoryTheory.Limits.Cone K} (hc : CategoryTheory.Limits.IsLimit c),
      Nonempty (CategoryTheory.Limits.IsLimit (F.mapCone c))) →
    CategoryTheory.Limits.PreservesLimit K F
-- Init.Data.SInt.Bitwise
Int32.xor_assoc : ∀ (a b c : Int32), a ^^^ b ^^^ c = a ^^^ (b ^^^ c)
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.sub : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : HasContDiffBump E] {c : E}
  (f : ContDiffBump c) (x : E), ↑f (c - x) = ↑f (c + x)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getKeyLE!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.Equiv t₂ → t₁.getKeyLE! k = t₂.getKeyLE! k
-- Init.Omega.Int
Lean.Omega.Int.ofNat_min : ∀ (a b : ℕ), ↑(min a b) = min ↑a ↑b
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey!_maxKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  [inst_4 : Inhabited α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    l.isEmpty = false →
      ∀ {fallback : α},
        Std.Internal.List.getKey! (Std.Internal.List.maxKeyD l fallback) l = Std.Internal.List.maxKeyD l fallback
-- Mathlib.Order.Circular
OrderDual.circularPartialOrder : (α : Type u_1) → [CircularPartialOrder α] → CircularPartialOrder αᵒᵈ
-- Mathlib.CategoryTheory.CofilteredSystem
CategoryTheory.Functor.eventualRange_mapsTo : ∀ {J : Type u} [inst : CategoryTheory.Category.{v_1, u} J] (F : CategoryTheory.Functor J (Type v)) {i j : J}
  [CategoryTheory.IsCofilteredOrEmpty J] (f : j ⟶ i),
  Set.MapsTo (⇑(CategoryTheory.ConcreteCategory.hom (F.map f))) (F.eventualRange j) (F.eventualRange i)
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.HasColimit.ι_isoOfEquivalence_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  {C : Type u} [inst_2 : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] {G : CategoryTheory.Functor K C}
  [inst_4 : CategoryTheory.Limits.HasColimit G] (e : J ≌ K) (w : e.functor.comp G ≅ F) (k : K),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι G k)
      (CategoryTheory.Limits.HasColimit.isoOfEquivalence e w).inv =
    CategoryTheory.CategoryStruct.comp (G.map (e.counitInv.app k))
      (CategoryTheory.CategoryStruct.comp (w.hom.app (e.inverse.obj k))
        (CategoryTheory.Limits.colimit.ι F (e.inverse.obj k)))
-- Init.System.FilePath
System.instDecidableEqFilePath : DecidableEq System.FilePath
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_addNat_Ico : ∀ {n : ℕ} (m : ℕ) (i j : Fin n),
  Finset.image (fun x => x.addNat m) (Finset.Ico i j) = Finset.Ico (i.addNat m) (j.addNat m)
-- Mathlib.Data.Finset.Union
Finset.fold_disjiUnion : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {op : β → β → β} [hc : Std.Commutative op] [ha : Std.Associative op]
  {ι : Type u_4} {s : Finset ι} {t : ι → Finset α} {b : ι → β} {b₀ : β} (h : (↑s).PairwiseDisjoint t),
  Finset.fold op (Finset.fold op b₀ b s) f (s.disjiUnion t h) =
    Finset.fold op b₀ (fun i => Finset.fold op (b i) f (t i)) s
-- Mathlib.Analysis.MeanInequalitiesPow
Real.rpow_add_rpow_le : ∀ {p q a b : ℝ}, 0 ≤ a → 0 ≤ b → 0 < p → p ≤ q → (a ^ q + b ^ q) ^ (1 / q) ≤ (a ^ p + b ^ p) ^ (1 / p)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get!_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α] {l : List α}
  {k k' : α},
  cmp k k' = Ordering.eq →
    k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertMany l).get! k' = k
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.Nat.isSemilinearSet_inter_of_isLinearSet : ∀ {ι : Type u_3} [Finite ι] {s₁ s₂ : Set (ι → ℕ)}, IsLinearSet s₁ → IsLinearSet s₂ → IsSemilinearSet (s₁ ∩ s₂)
-- Mathlib.Combinatorics.HalesJewett
/-- A variant of the **extended Hales-Jewett theorem** `exists_mono_in_high_dimension` where the
returned type is some `Fin n` instead of a general fintype.  -/
Combinatorics.Subspace.exists_mono_in_high_dimension_fin : ∀ (α : Type u_5) (κ : Type u_6) (η : Type u_7) [Finite α] [Finite κ] [Finite η],
  ∃ n, ∀ (C : (Fin n → α) → κ), ∃ l, Combinatorics.Subspace.IsMono C l
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.del.sizeOf_spec : ∀ (x : Lean.IR.VarId) (b : Lean.IR.FnBody), sizeOf (Lean.IR.FnBody.del x b) = 1 + sizeOf x + sizeOf b
-- Std.Net.Addr
Std.Net.SocketAddressV4.port : Std.Net.SocketAddressV4 → UInt16
-- Mathlib.Algebra.Ring.BooleanRing
toBoolRing_symm_eq : ∀ {α : Type u_1}, toBoolRing.symm = ofBoolRing
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- Let `F : C₀ ⥤ C` be a dense subsite and `data : ∀ X, F.OneHypercoverDenseData J₀ J X`
be a family. Let `G₀` be a sheaf on `C₀`. Let `f : F.obj X₀ ⟶ X`.
This is the canonical morphism
`presheafObj data G₀ X ⟶ G₀.obj.obj (op X₀)` (where `presheafObj data G₀ X`
is the value on `X` of the extension to `C` of the sheaf `G₀`,
see `OneHypercoverDenseData.essSurj.presheaf` and
`OneHypercoverDenseData.essSurj.isSheaf`).  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.restriction : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  [CategoryTheory.Functor.IsDenseSubsite J₀ J F] →
                    (data : (X : C) → F.OneHypercoverDenseData J₀ J X) →
                      [inst_4 : CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] →
                        (G₀ : CategoryTheory.Sheaf J₀ A) →
                          {X : C} →
                            {X₀ : C₀} →
                              (F.obj X₀ ⟶ X) →
                                (CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObj data G₀ X ⟶
                                  G₀.obj.obj (Opposite.op X₀))
-- Mathlib.RingTheory.Perfectoid.FontaineTheta
WittVector.ghostComponent.eq_1 : ∀ {p : ℕ} {R : Type u_1} [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] (n : ℕ),
  WittVector.ghostComponent n = (Pi.evalRingHom (fun a => R) n).comp WittVector.ghostMap
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithInitial.coconeLift.match_1.eq_1 : ∀ {J : Type u_1} (motive : CategoryTheory.WithInitial J → Sort u_2) (a : J)
  (h_1 : (a : J) → motive (CategoryTheory.WithInitial.of a)) (h_2 : Unit → motive CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.of a with
    | CategoryTheory.WithInitial.of a => h_1 a
    | CategoryTheory.WithInitial.star => h_2 ()) =
    h_1 a
-- Mathlib.RingTheory.Localization.Basic
/-- The localization of `R` at `M` as a quotient type is isomorphic to any other localization.  -/
Localization.algEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      (S : Type u_2) →
        [inst_1 : CommSemiring S] → [inst_2 : Algebra R S] → [IsLocalization M S] → Localization M ≃ₐ[R] S
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- Given an exact short complex `S` and a colimit cokernel cofork `cc` for `S.f`, this is the
right homology data for `S` with `Q := cc.pt` and `H := 0`.  -/
CategoryTheory.ShortComplex.Exact.rightHomologyDataOfIsColimitCokernelCofork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} →
        S.Exact →
          [CategoryTheory.Limits.HasZeroObject C] →
            (cc : CategoryTheory.Limits.CokernelCofork S.f) → CategoryTheory.Limits.IsColimit cc → S.RightHomologyData
-- Mathlib.Combinatorics.Matroid.Map
/-- The pullback of a matroid on `β` by a function `f : α → β` to a matroid on `α`.
Elements with the same (nonloop) image are parallel and the ground set is `f ⁻¹' M.E`.
The matroids `M.comap f` and `M ↾ range f` have isomorphic simplifications;
the preimage of each nonloop of `M ↾ range f` is a parallel class.  -/
Matroid.comap : {α : Type u_1} → {β : Type u_2} → Matroid β → (α → β) → Matroid α
-- Mathlib.Logic.Basic
/-- `Classical.byContradiction'` is equivalent to lean's axiom `Classical.choice`.  -/
Classical.choice_of_byContradiction' : {α : Sort u_2} → ((¬∀ (a : α), False) → α) → Nonempty α → α
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.getKeyD_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Bool} {k fallback : α},
  (Std.ExtDTreeMap.filter f t).getKeyD k fallback =
    ((t.getKey? k).pfilter fun x h' => f x (Std.ExtDTreeMap.Const.get t x ⋯)).getD fallback
-- Lean.PrettyPrinter.Parenthesizer
Lean.PrettyPrinter.Parenthesizer.State.trailCat : Lean.PrettyPrinter.Parenthesizer.State → Lean.Name
-- Mathlib.Topology.Semicontinuity.Basic
/-- An intersection of sublevel sets of a lower semicontinuous function
on a compact set is empty if and only if a finite sub-intersection is already empty.  -/
LowerSemicontinuousOn.inter_biInter_preimage_Iic_eq_empty_iff_exists_finset : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {γ : Type u_4} [inst_1 : LinearOrder γ] {ι : Type u_5}
  {f : ι → α → γ},
  IsCompact s →
    ∀ {I : Set ι} {c : γ},
      (∀ i ∈ I, LowerSemicontinuousOn (f i) s) →
        (s ∩ ⋂ i ∈ I, f i ⁻¹' Set.Iic c = ∅ ↔ ∃ u, ∀ x ∈ s, ∃ i ∈ u, c < f (↑i) x)
-- Mathlib.Order.Interval.Set.Fin
Fin.image_succ_Ioi : ∀ {n : ℕ} (i : Fin n), Fin.succ '' Set.Ioi i = Set.Ioi i.succ
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instCategory : {X : AlgebraicGeometry.Scheme} → CategoryTheory.Category.{u, u + 1} X.Modules
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} (not_mem : k ∉ m₁) {h' : k ∈ m₁ ∪ m₂}, (m₁ ∪ m₂).getKey k h' = m₂.getKey k ⋯
-- Mathlib.GroupTheory.GroupExtension.Defs
AddGroupExtension.Splitting.instFunLike.eq_1 : ∀ {N : Type u_1} {E : Type u_2} {G : Type u_3} [inst : AddGroup N] [inst_1 : AddGroup E] [inst_2 : AddGroup G]
  (S : AddGroupExtension N E G),
  AddGroupExtension.Splitting.instFunLike S = { coe := fun s => (↑s.toAddMonoidHom).toFun, coe_injective := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.eval_polynomialX_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  P 2 ≠ 0 →
    (MvPolynomial.eval P) W.polynomialX / P 2 ^ 4 =
      Polynomial.evalEval (P 0 / P 2 ^ 2) (P 1 / P 2 ^ 3) W.toAffine.polynomialX
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.ToIntThms.mkResult : Lean.Meta.Grind.Arith.Cutsat.ToIntThms →
  (Lean.Expr → Lean.Expr → Lean.Expr) →
    Lean.Expr →
      Lean.Expr →
        Lean.Expr → Lean.Expr → Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Lean.Expr × Lean.Expr)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.multicoforkEquivSigmaCofork_inverse_obj_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right]
  (a :
    CategoryTheory.Limits.Cofork
      (I.fstSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right))
        (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left)))
      (I.sndSigmaMapOfIsColimit (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right))
        (CategoryTheory.Limits.colimit.isColimit (CategoryTheory.Discrete.functor I.left))))
  (x : CategoryTheory.Limits.WalkingMultispan J),
  (I.multicoforkEquivSigmaCofork.inverse.obj a).ι.app x =
    match x with
    | CategoryTheory.Limits.WalkingMultispan.left a_1 =>
      CategoryTheory.CategoryStruct.comp (I.fst a_1)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Limits.Cofan.inj
            (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) (J.fst a_1))
          a.π)
    | CategoryTheory.Limits.WalkingMultispan.right a_1 =>
      CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.Cofan.inj
          (CategoryTheory.Limits.colimit.cocone (CategoryTheory.Discrete.functor I.right)) a_1)
        a.π
-- Mathlib.Order.Comparable
instTransCompRelLeAntisymmRel : {α : Type u_1} →
  [inst : Preorder α] →
    Trans (CompRel fun x1 x2 => x1 ≤ x2) (AntisymmRel fun x1 x2 => x1 ≤ x2) (CompRel fun x1 x2 => x1 ≤ x2)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.one_power : ∀ {a : Cardinal.{u_1}}, 1 ^ a = 1
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegrable_smul_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E} {ω : E → E →L[𝕜] F}
  {γ : Path a b} {𝕝 : Type u_4} [inst_5 : RCLike 𝕝] [inst_6 : NormedSpace 𝕝 F] [inst_7 : SMulCommClass 𝕜 𝕝 F] {c : 𝕝},
  CurveIntegrable (c • ω) γ ↔ c = 0 ∨ CurveIntegrable ω γ
-- Init.Data.Nat.Bitwise.Lemmas
Nat.testBit.eq_1 : ∀ (m n : ℕ), m.testBit n = (1 &&& m >>> n != 0)
-- Mathlib.Control.Fold
Monoid.foldlM.get.eq_1 : ∀ {m : Type u → Type u} [inst : Monad m] {α : Type u} (x : Monoid.foldlM m α), x.get = MulOpposite.unop x
-- Mathlib.CategoryTheory.Action
/-- An object of the action category given by M ↻ X corresponds to an element of X.  -/
CategoryTheory.ActionCategory.objEquiv : (M : Type u_1) → [inst : Monoid M] → (X : Type u) → [inst_1 : MulAction M X] → X ≃ CategoryTheory.ActionCategory M X
-- Mathlib.Algebra.Group.Subsemigroup.Defs
AddSubsemigroup.mk.inj : ∀ {M : Type u_3} {inst : Add M} {carrier : Set M} {add_mem' : ∀ {a b : M}, a ∈ carrier → b ∈ carrier → a + b ∈ carrier}
  {carrier_1 : Set M} {add_mem'_1 : ∀ {a b : M}, a ∈ carrier_1 → b ∈ carrier_1 → a + b ∈ carrier_1},
  { carrier := carrier, add_mem' := add_mem' } = { carrier := carrier_1, add_mem' := add_mem'_1 } → carrier = carrier_1
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The objects on the pages of a spectral sequence attached to a spectral object `X`
identifies an object `X.E`.  -/
CategoryTheory.Abelian.SpectralObject.spectralSequencePageXIso : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    [inst_3 : X.HasSpectralSequence data] →
                      (r : ℤ) →
                        (hr : r₀ ≤ r) →
                          (pq : κ) →
                            (i₀ i₁ i₂ i₃ : ι) →
                              (h₀ : i₀ = data.i₀ r pq ⋯) →
                                (h₁ : i₁ = data.i₁ pq) →
                                  (h₂ : i₂ = data.i₂ pq) →
                                    (h₃ : i₃ = data.i₃ r pq ⋯) →
                                      (n₀ n₁ n₂ : ℤ) →
                                        n₁ = data.deg pq →
                                          (hn₁ :
                                              autoParam (n₀ + 1 = n₁)
                                                CategoryTheory.Abelian.SpectralObject.spectralSequencePageXIso._auto_1) →
                                            (hn₂ :
                                                autoParam (n₁ + 1 = n₂)
                                                  CategoryTheory.Abelian.SpectralObject.spectralSequencePageXIso._auto_3) →
                                              ((X.spectralSequence data).page r ⋯).X pq ≅
                                                X.E (CategoryTheory.homOfLE ⋯) (CategoryTheory.homOfLE ⋯)
                                                  (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ ⋯ ⋯
-- Mathlib.Algebra.Category.BoolRing
BoolAlg.hasForgetToBoolRing_forget₂_map : ∀ {X Y : BoolAlg} (f : X ⟶ Y), CategoryTheory.HasForget₂.forget₂.map f = BoolRing.ofHom (BoolAlg.Hom.hom f).asBoolRing
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.Char
Char.reduceGE : Lean.Meta.Simp.Simproc
-- Mathlib.GroupTheory.Exponent
addOrderOf_eq_two_iff : ∀ {G : Type u} [inst : AddMonoid G], AddMonoid.exponent G = 2 → ∀ {x : G}, addOrderOf x = 2 ↔ x ≠ 0
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.toSpanSingleton.congr_simp : ∀ (R₁ : Type u_1) [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] [inst_4 : TopologicalSpace R₁] [inst_5 : ContinuousSMul R₁ M₁] (x x_1 : M₁),
  x = x_1 → ContinuousLinearMap.toSpanSingleton R₁ x = ContinuousLinearMap.toSpanSingleton R₁ x_1
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Ico_add_Ioc_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [AddLeftStrictMono α]
  [AddRightStrictMono α] [inst_5 : LocallyFiniteOrder α] (a b c d : α),
  Finset.Ico a b + Finset.Ioc c d ⊆ Finset.Ioo (a + c) (b + d)
-- Mathlib.NumberTheory.LSeries.Convergence
LSeriesSummable.abscissaOfAbsConv_le : ∀ {f : ℕ → ℂ} {s : ℂ}, LSeriesSummable f s → LSeries.abscissaOfAbsConv f ≤ ↑s.re
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.powerlt.eq_1 : ∀ (a b : Cardinal.{u}), a ^< b = ⨆ c, a ^ ↑c
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
/-- The (limit) multifork with point `presheafObjπ data G₀ X` for
the diagram given by `G₀` and `data X`.  -/
CategoryTheory.Functor.OneHypercoverDenseData.essSurj.presheafObjMultifork : {C₀ : Type u₀} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v₀, u₀} C₀] →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor C₀ C} →
          {J₀ : CategoryTheory.GrothendieckTopology C₀} →
            {J : CategoryTheory.GrothendieckTopology C} →
              {A : Type u'} →
                [inst_2 : CategoryTheory.Category.{v', u'} A] →
                  (data : (X : C) → F.OneHypercoverDenseData J₀ J X) →
                    [CategoryTheory.Limits.HasLimitsOfSize.{w, w, v', u'} A] →
                      (G₀ : CategoryTheory.Sheaf J₀ A) →
                        (X : C) → CategoryTheory.Limits.Multifork ((data X).multicospanIndex G₀.obj)
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_pow_left_dvd_pow_gcd : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : GCDMonoid α] {a b : α} {k : ℕ}, gcd (a ^ k) b ∣ gcd a b ^ k
-- Mathlib.Data.Set.Image
Set.range_const_subset : ∀ {α : Type u_1} {ι : Sort u_4} {c : α}, (Set.range fun x => c) ⊆ {c}
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.preconnectedSpace : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β}
  [PreconnectedSpace α], IsDenseInducing i → PreconnectedSpace β
-- Init.ShareCommon
/-- Internally `State` is implemented as a pair `ObjectMap` and `ObjectSet`  -/
ShareCommon.StatePointed : ShareCommon.StateFactory → NonemptyType
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.instBEqFunctionTheorem.beq : Mathlib.Meta.FunProp.FunctionTheorem → Mathlib.Meta.FunProp.FunctionTheorem → Bool
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.event.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.event = 1
-- Mathlib.Order.JordanHolder
/-- Two `CompositionSeries` are equal if they have the same elements. See also `ext_fun`.  -/
CompositionSeries.ext : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] {s₁ s₂ : CompositionSeries X},
  (∀ (x : X), x ∈ s₁ ↔ x ∈ s₂) → s₁ = s₂
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₆_of_isCharThreeJNeZeroNF_of_char_three : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharThreeJNeZeroNF] [CharP R 3], W.c₆ = -W.a₂ ^ 3
-- Mathlib.Data.FinEnum
/-- transport a `FinEnum` instance across an equivalence  -/
FinEnum.ofEquiv : (α : Sort u_1) → {β : Sort u_2} → [FinEnum α] → β ≃ α → FinEnum β
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instContinuousAdd : ∀ {A : Type u_3} {E : Type u_4} [inst : AddCommGroup E] [inst_1 : UniformSpace E] [ContinuousAdd E],
  ContinuousAdd (WithCStarModule A E)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_sub : ∀ {R : Type u} [inst : Ring R] {f g : Polynomial R},
  Polynomial.derivative (f - g) = Polynomial.derivative f - Polynomial.derivative g
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass.toFriendlyOperationClass : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis} {γ : Type u_1}
  {op :
    γ →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
        Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl}
  [self : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.FriendlyOperationClass op],
  Tactic.ComputeAsymptotics.Seq.FriendlyOperationClass op
-- Mathlib.CategoryTheory.Shift.Opposite
CategoryTheory.instAdditiveOppositeShiftShiftFunctor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] (A : Type u_2) [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] [inst_3 : CategoryTheory.Preadditive C] (n : A)
  [(CategoryTheory.shiftFunctor C n).Additive],
  (CategoryTheory.shiftFunctor (CategoryTheory.OppositeShift C A) n).Additive
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.hasNeutral : Lean.Meta.Grind.AC.ACM Bool
-- Init.Data.Range.Polymorphic.UInt
UInt64.instLawfulHasSize_1 : Std.Rxo.LawfulHasSize UInt64
-- Lean.Meta.Match.AltTelescopes
_private.Lean.Meta.Match.AltTelescopes.0.Lean.Meta.Match.forallAltVarsTelescope.go : {α : Type} →
  Lean.Expr →
    Lean.Meta.Match.AltParamInfo →
      (Array Lean.Expr → Array Lean.Expr → Array Bool → Lean.Expr → Lean.MetaM α) →
        Array Lean.Expr → Array Lean.Expr → Array Bool → ℕ → Lean.Expr → Lean.MetaM α