mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.constInsertManyIfNewUnit_list : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m₁ m₂ : Std.DHashMap.Raw α fun x => Unit},
  m₁.WF →
    m₂.WF →
      ∀ (l : List α),
        m₁.Equiv m₂ →
          (Std.DHashMap.Raw.Const.insertManyIfNewUnit m₁ l).Equiv (Std.DHashMap.Raw.Const.insertManyIfNewUnit m₂ l)
-- Mathlib.Order.PrimeIdeal
Order.Ideal.PrimePair.I_union_F : ∀ {P : Type u_1} [inst : Preorder P] (IF : Order.Ideal.PrimePair P), ↑IF.I ∪ ↑IF.F = Set.univ
-- Mathlib.Data.Rat.Defs
Rat.den_eq_one_iff : ∀ (r : ℚ), r.den = 1 ↔ ↑r.num = r
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.re_coe : ∀ (z : Complex.UnitDisc), (↑z).re = z.re
-- Mathlib.Order.Interval.Set.SuccOrder
Set.Iic.succ_eq_of_not_isMax : ∀ {J : Type u_1} [inst : PartialOrder J] [inst_1 : SuccOrder J] {j : J} {i : ↑(Set.Iic j)} (hi : ¬IsMax i),
  Order.succ i = ⟨Order.succ ↑i, ⋯⟩
-- Std.Internal.Do.Triple.SpecLemmas
_private.Std.Internal.Do.Triple.SpecLemmas.0.Std.Internal.Do.Except.wpInst.match_1.splitter : {ε : Type u_1} →
  {α : Type u_2} →
    (motive : Except ε α → Sort u_3) →
      (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((el : ε) → motive (Except.error el)) → motive x
-- Mathlib.MeasureTheory.Measure.Portmanteau
/-- One implication of the portmanteau theorem:
Weak convergence of probability measures implies that the limsup of the measures of any closed
set is at most the measure of the closed set under the limit probability measure.
 -/
MeasureTheory.ProbabilityMeasure.limsup_measure_closed_le_of_tendsto : ∀ {Ω : Type u_1} {ι : Type u_2} {L : Filter ι} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω]
  [inst_2 : OpensMeasurableSpace Ω] [HasOuterApproxClosed Ω] {μ : MeasureTheory.ProbabilityMeasure Ω}
  {μs : ι → MeasureTheory.ProbabilityMeasure Ω},
  Filter.Tendsto μs L (nhds μ) → ∀ {F : Set Ω}, IsClosed F → Filter.limsup (fun i => ↑(μs i) F) L ≤ ↑μ F
-- Mathlib.Topology.Algebra.Group.Defs
ContinuousAt.fun_neg : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Neg G]
  [ContinuousNeg G] {f : X → G} {x : X}, ContinuousAt f x → ContinuousAt (fun i => -f i) x
-- Mathlib.Data.Ordmap.Ordnode
/-- O(n). Split the elements of a tree into those satisfying, and not satisfying, a predicate.

```
partition (fun x ↦ x < 3) {1, 2, 4} = ({1, 2}, {3})
```  -/
Ordnode.partition : {α : Type u_1} → (p : α → Prop) → [DecidablePred p] → Ordnode α → Ordnode α × Ordnode α
-- Mathlib.Order.Antisymmetrization
instTransAntisymmRelLeSymmGen : {α : Type u_1} →
  [inst : Preorder α] →
    Trans (AntisymmRel fun x1 x2 => x1 ≤ x2) (Relation.SymmGen fun x1 x2 => x1 ≤ x2)
      (Relation.SymmGen fun x1 x2 => x1 ≤ x2)
-- Mathlib.RingTheory.WittVector.Identities
WittVector.coeff_p_pow : ∀ (p : ℕ) (R : Type u_1) [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] (i : ℕ), (↑p ^ i).coeff i = 1
-- Init.Data.Array.Erase
Array.eraseIdxIfInBounds_eq : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, xs.eraseIdxIfInBounds i = if h : i < xs.size then xs.eraseIdx i h else xs
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorParams.textDocument : Lean.Lsp.DocumentColorParams → Lean.Lsp.TextDocumentIdentifier
-- Mathlib.Algebra.Regular.SMul
/-- The `0` element is not `M`-regular, on a non-trivial module.  -/
IsSMulRegular.not_zero_iff : ∀ {R : Type u_1} {M : Type u_3} [inst : MonoidWithZero R] [inst_1 : Zero M] [inst_2 : MulActionWithZero R M],
  ¬IsSMulRegular M 0 ↔ Nontrivial M
-- Std.Do.Triple.SpecLemmas
tryCatchThe.eq_1 : ∀ (ε : Type u) {m : Type v → Type w} [inst : MonadExceptOf ε m] {α : Type v} (x : m α) (handle : ε → m α),
  tryCatchThe ε x handle = MonadExceptOf.tryCatch x handle
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
/-- The dual submodule of a submodule with respect to a bilinear form.  -/
LinearMap.BilinForm.dualSubmodule : {R : Type u_1} →
  {S : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : Field S] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Algebra R S] →
              [inst_4 : Module R M] →
                [inst_5 : Module S M] → [IsScalarTower R S M] → LinearMap.BilinForm S M → Submodule R M → Submodule R M
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.iSup₂_lintegral_le : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {ι : Sort u_4} {ι' : ι → Sort u_5}
  (f : (i : ι) → ι' i → α → ENNReal), ⨆ i, ⨆ j, ∫⁻ (a : α), f i j a ∂μ ≤ ∫⁻ (a : α), ⨆ i, ⨆ j, f i j a ∂μ
-- Mathlib.Geometry.Manifold.VectorBundle.Riemannian
instIsContMDiffRiemannianBundleOfTopWithTopENat : ∀ {EB : Type u_1} [inst : NormedAddCommGroup EB] [inst_1 : NormedSpace ℝ EB] {HB : Type u_2}
  [inst_2 : TopologicalSpace HB] {IB : ModelWithCorners ℝ EB HB} {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]
  {a : WithTop ℕ∞} [IsContMDiffRiemannianBundle IB ⊤ F E], IsContMDiffRiemannianBundle IB a F E
-- Mathlib.CategoryTheory.Monoidal.Rigid.Basic
CategoryTheory.tensorRightHomEquiv_whiskerLeft_comp_evaluation : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  [inst_2 : CategoryTheory.HasRightDual X] [inst_3 : CategoryTheory.HasRightDual Y] (f : X ⟶ Y),
  (CategoryTheory.tensorRightHomEquiv Yᘁ X Xᘁ (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Yᘁ f) (ε_ Y Yᘁ)) =
    CategoryTheory.CategoryStruct.comp (fᘁ) (CategoryTheory.MonoidalCategoryStruct.leftUnitor Xᘁ).inv
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
spectralValueTerms.eq_1 : ∀ {R : Type u_1} [inst : SeminormedRing R] (p : Polynomial R) (n : ℕ),
  spectralValueTerms p n = if n < p.natDegree then ‖p.coeff n‖ ^ (1 / (↑p.natDegree - ↑n)) else 0
-- Init.Data.UInt.Bitwise
UInt16.xor_left_inj : ∀ {a b : UInt16} (c : UInt16), a ^^^ c = b ^^^ c ↔ a = b
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- If two continuous `R`-alternating maps from `R` are equal on 1, then they are equal.

This is the alternating version of `ContinuousLinearMap.ext_ring`.  -/
ContinuousAlternatingMap.ext_ring : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [Finite ι] [inst_5 : TopologicalSpace R] ⦃f g : R [⋀^ι]→L[R] M⦄,
  ((f fun x => 1) = g fun x => 1) → f = g
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mem_localTrivAsPartialEquiv_source : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι) (p : Z.TotalSpace),
  p ∈ (Z.localTrivAsPartialEquiv i).source ↔ p.proj ∈ Z.baseSet i
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- Given a point `Φ` of a site `(C, J)`, `X : C` and `x : Φ.fiber.obj X`, this
is the canonical map `P.obj (op X) ⟶ Φ.presheafFiber.obj P`.  -/
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber : {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.HasColimitsOfSize.{w, w, v', u'} A] →
              (X : C) →
                Φ.fiber.obj X → (P : CategoryTheory.Functor Cᵒᵖ A) → P.obj (Opposite.op X) ⟶ Φ.presheafFiber.obj P
-- Mathlib.Algebra.Tropical.Basic
Tropical.rightInverse_trop : ∀ {R : Type u}, Function.RightInverse Tropical.trop Tropical.untrop
-- Mathlib.Geometry.RingedSpace.SheafedSpace
AlgebraicGeometry.SheafedSpace.restrictTopIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : AlgebraicGeometry.SheafedSpace C),
  X.restrictTopIso.inv = CategoryTheory.InducedCategory.homMk X.toRestrictTop
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.instMonoFunctorTypeHomOfLe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  {G G' : CategoryTheory.Subfunctor F} (h : G ≤ G'), CategoryTheory.Mono (CategoryTheory.Subfunctor.homOfLe h)
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.P_idem_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q : ℕ) {Z : ChainComplex C ℕ}
  (h : AlgebraicTopology.AlternatingFaceMapComplex.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.P q)
      (CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.P q) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicTopology.DoldKan.P q) h
-- Mathlib.Analysis.SpecialFunctions.Gamma.Basic
Complex.tendsto_partialGamma : ∀ {s : ℂ}, 0 < s.re → Filter.Tendsto (fun X => s.partialGamma X) Filter.atTop (nhds s.GammaIntegral)
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
CategoryTheory.isCardinalFiltered_pi : ∀ {ι : Type u'} (J : ι → Type u) [inst : (i : ι) → CategoryTheory.Category.{v, u} (J i)] (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [∀ (i : ι), CategoryTheory.IsCardinalFiltered (J i) κ],
  CategoryTheory.IsCardinalFiltered ((i : ι) → J i) κ
-- Init.Data.Nat.Div.Lemmas
Nat.mod_mod_of_dvd' : ∀ {a b c : ℕ}, b ∣ c → a % b % c = a % b
-- Init.Data.Array.MapIdx
List.mapFinIdxM.go.congr_simp : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Monad m] (as : List α)
  (f f_1 : (i : ℕ) → α → i < as.length → m β),
  f = f_1 →
    ∀ (bs bs_1 : List α) (e_bs : bs = bs_1) (acc acc_1 : Array β) (e_acc : acc = acc_1)
      (a : bs.length + acc.size = as.length), List.mapFinIdxM.go as f bs acc a = List.mapFinIdxM.go as f_1 bs_1 acc_1 ⋯
-- Init.Data.Iterators.Lemmas.Producers.List
List.toListRev_iter : ∀ {β : Type w} {l : List β}, l.iter.toListRev = l.reverse
-- Mathlib.AlgebraicGeometry.RelativeGluing
AlgebraicGeometry.Scheme.Cover.RelativeGluingData.preimage_toBase_eq_range_ι : ∀ {S : AlgebraicGeometry.Scheme} {𝒰 : S.OpenCover} [inst : CategoryTheory.Category.{u_2, u_1} 𝒰.I₀]
  [inst_1 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰] (d : AlgebraicGeometry.Scheme.Cover.RelativeGluingData 𝒰)
  [inst_2 : Small.{u, u_1} 𝒰.I₀] [inst_3 : Quiver.IsThin 𝒰.I₀] (i : 𝒰.I₀),
  ⇑d.toBase ⁻¹' Set.range ⇑(𝒰.f i) = Set.range ⇑(CategoryTheory.Limits.colimit.ι d.functor i)
-- Mathlib.Algebra.BigOperators.Fin
/-- A sum of a function `f : Fin (n + 1) → M` over all `Fin (n + 1)` is the sum of
`f x`, for some `x : Fin (n + 1)` plus the remaining sum  -/
Fin.sum_univ_succAbove : ∀ {M : Type u_2} [inst : AddCommMonoid M] {n : ℕ} (f : Fin (n + 1) → M) (x : Fin (n + 1)),
  ∑ i, f i = f x + ∑ i, f (x.succAbove i)
-- Init.Internal.Order.Basic
Lean.Order.instMonoBindStateRefT' : ∀ {m : Type → Type} {ω σ : Type} [inst : Monad m] [inst_1 : (α : Type) → Lean.Order.PartialOrder (m α)]
  [Lean.Order.MonoBind m], Lean.Order.MonoBind (StateRefT' ω σ m)
-- Lean.Meta.HaveTelescope
Lean.Meta.HaveTelescopeInfo.mk.sizeOf_spec : ∀ (haveInfo : Array Lean.Meta.HaveInfo) (bodyDeps bodyTypeDeps : Std.HashSet ℕ) (body bodyType : Lean.Expr)
  (level : Lean.Level),
  sizeOf
      { haveInfo := haveInfo, bodyDeps := bodyDeps, bodyTypeDeps := bodyTypeDeps, body := body, bodyType := bodyType,
        level := level } =
    1 + sizeOf haveInfo + sizeOf bodyDeps + sizeOf bodyTypeDeps + sizeOf body + sizeOf bodyType + sizeOf level
-- Mathlib.Topology.Inseparable
Inseparable.specializes' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y : X}, Inseparable x y → y ⤳ x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_antisymm : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} {p₁ p₂ : G.Walk u v}, p₁.IsSubwalk p₂ → p₂.IsSubwalk p₁ → p₁ = p₂
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.comap_normalClosure : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (s : Set N) (f : G ≃* N),
  Subgroup.normalClosure (⇑f ⁻¹' s) = Subgroup.comap (↑f) (Subgroup.normalClosure s)
-- Mathlib.Topology.MetricSpace.HolderNorm
nnHolderNorm.eq_1 : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (r : NNReal) (f : X → Y),
  nnHolderNorm r f = (eHolderNorm r f).toNNReal
-- Mathlib.Algebra.Ring.BooleanRing
_private.Mathlib.Algebra.Ring.BooleanRing.0.of_boolalg_symmDiff_aux : ∀ {α : Type u_1} [inst : BooleanRing α] (a b : α), (a + b + a * b) * (1 + a * b) = a + b
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- **Alias** of `CategoryTheory.HasSubobjectClassifier.unique`.

---

`χ m` is the only map for which the associated square
is a pullback square.
 -/
CategoryTheory.HasClassifier.unique : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasSubobjectClassifier C] {U X : C}
  (m : U ⟶ X) [inst_2 : CategoryTheory.Mono m] (χ' : X ⟶ CategoryTheory.HasSubobjectClassifier.Ω C),
  CategoryTheory.IsPullback m (⋯.some.χ₀ U) χ' (CategoryTheory.HasSubobjectClassifier.truth C) →
    χ' = CategoryTheory.HasSubobjectClassifier.χ m
-- Std.Time.Duration
/-- Checks if the duration is zero seconds and zero nanoseconds.
 -/
Std.Time.Duration.isZero : Std.Time.Duration → Bool
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
MeasureTheory.isFiniteMeasure_sfiniteSeq : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [h : MeasureTheory.SFinite μ] (n : ℕ),
  MeasureTheory.IsFiniteMeasure (MeasureTheory.sfiniteSeq μ n)
-- Mathlib.Data.Nat.Prime.Defs
Nat.prime_seven : Nat.Prime 7
-- Init.Data.String.Lemmas.IsEmpty
String.isEmpty_iff : ∀ {s : String}, s.isEmpty = true ↔ s = ""
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.sub_subset_sub_left : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s t₁ t₂ : Finset α}, t₁ ⊆ t₂ → s - t₁ ⊆ s - t₂
-- Lean.ResolveName
Lean.MonadResolveName.mk : {m : Type → Type} → m Lean.Name → m (List Lean.OpenDecl) → Lean.MonadResolveName m
-- Mathlib.Algebra.Star.SelfAdjoint
skewAdjoint.conjugate : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : StarRing R] {x : R},
  x ∈ skewAdjoint R → ∀ (z : R), z * x * star z ∈ skewAdjoint R
-- Mathlib.Data.ENNReal.Inv
OrderIso.invENNReal_apply : ∀ (a : ENNReal), OrderIso.invENNReal a = (OrderDual.toDual a)⁻¹
-- Mathlib.Tactic.NormNum.Basic
/-- Helper function to synthesize a typed `DivisionSemiring α` expression.  -/
Mathlib.Meta.NormNum.inferDivisionSemiring : {u : Lean.Level} → (α : Q(Type u)) → Lean.MetaM Q(DivisionSemiring «$α»)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.isSelfAdjoint_toLinearMap_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] (T : E →L[𝕜] E),
  have this := ⋯;
  IsSelfAdjoint ↑T ↔ IsSelfAdjoint T
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- The right homology map data associated to the zero morphism between two short complexes.  -/
CategoryTheory.ShortComplex.RightHomologyMapData.zero : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S₁ S₂ : CategoryTheory.ShortComplex C} →
        (h₁ : S₁.RightHomologyData) →
          (h₂ : S₂.RightHomologyData) → CategoryTheory.ShortComplex.RightHomologyMapData 0 h₁ h₂
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.cons.hcongr_7 : ∀ (V V' : Type u),
  V = V' →
    ∀ (G : SimpleGraph V) (G' : SimpleGraph V'),
      G ≍ G' →
        ∀ (u : V) (u' : V'),
          u ≍ u' →
            ∀ (v : V) (v' : V'),
              v ≍ v' →
                ∀ (w : V) (w' : V'),
                  w ≍ w' →
                    ∀ (h : G.Adj u v) (h' : G'.Adj u' v'),
                      h ≍ h' →
                        ∀ (p : G.Walk v w) (p' : G'.Walk v' w'),
                          p ≍ p' → SimpleGraph.Walk.cons h p ≍ SimpleGraph.Walk.cons h' p'
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k a : α}
  {v : β k} {h₁ : a ∈ m.insertIfNew k v},
  (m.insertIfNew k v).get a h₁ = if h₂ : (k == a) = true ∧ k ∉ m then cast ⋯ v else m.get a ⋯
-- Mathlib.Algebra.GroupWithZero.Defs
/-- A type `M₀` is a “monoid with zero” if it is a monoid with zero element, and `0` is left
and right absorbing.  -/
MonoidWithZero : Type u → Type u
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.Subcomplex.coe_mk' : ∀ {X : Type u_1} [t : TopologicalSpace X] [inst : T2Space X] (C : Set X) {D : Set X}
  [inst_1 : Topology.RelCWComplex C D] (E : Set X) (I : (n : ℕ) → Set (Topology.RelCWComplex.cell C n))
  (closedCell_subset : ∀ (n : ℕ) (i : ↑(I n)), Topology.RelCWComplex.closedCell n ↑i ⊆ E)
  (union : D ∪ ⋃ n, ⋃ j, Topology.RelCWComplex.openCell n ↑j = E),
  ↑(Topology.RelCWComplex.Subcomplex.mk' C E I closedCell_subset union) = E
-- Mathlib.Geometry.Manifold.IsManifold.Basic
/-- If two model with corners are boundaryless, their product also is  -/
ModelWithCorners.range_eq_univ_prod : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type w} [inst_3 : TopologicalSpace H] (I : ModelWithCorners 𝕜 E H) [I.Boundaryless]
  {E' : Type v'} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E'] {H' : Type w'}
  [inst_7 : TopologicalSpace H'] (I' : ModelWithCorners 𝕜 E' H') [I'.Boundaryless], (I.prod I').Boundaryless
-- Lean.Server.References
Lean.Server.Reference.mk : Lean.Lsp.RefIdent →
  Array Lean.Lsp.RefIdent →
    Lean.Lsp.Range → Lean.Syntax → Lean.Elab.ContextInfo → Lean.Elab.Info → Bool → Lean.Server.Reference
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
AddMonoidHom.isUniformInducing_of_isInducing : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] {Hom : Type u_3}
  [inst_3 : UniformSpace β] [inst_4 : AddGroup β] [IsUniformAddGroup β] [inst_6 : FunLike Hom α β]
  [AddMonoidHomClass Hom α β] {f : Hom}, Topology.IsInducing ⇑f → IsUniformInducing ⇑f
-- Init.Data.Nat.ToString
Nat.f_eq_digitChar : ∀ {n : ℕ}, 'f' = n.digitChar ↔ n = 15
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.addCommGroup : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (p : Submodule R M) → AddCommGroup (M ⧸ p)
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.ΓSpec.adjunction_unit_app : ∀ {X : AlgebraicGeometry.Scheme}, AlgebraicGeometry.ΓSpec.adjunction.unit.app X = X.toSpecΓ
-- Mathlib.Computability.TuringMachine.ToPartrec
/-- The halting state corresponding to a `List ℕ` output value.  -/
Turing.PartrecToTM2.halt : List ℕ → Turing.PartrecToTM2.Cfg'
-- Mathlib.Topology.Sheaves.Presheaf
IsOpenMap.pullbackObjIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X Y : TopCat}
  {f : X ⟶ Y} (hf : IsOpenMap ⇑(CategoryTheory.ConcreteCategory.hom f)) (ℱ : TopCat.Presheaf C Y)
  (X_1 : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (hf.pullbackObjIso ℱ).inv.app X_1 = (TopCat.Presheaf.pullbackObjObjOfImageOpen f ℱ (Opposite.unop X_1) ⋯).inv
-- Mathlib.CategoryTheory.Shift.Adjunction
CategoryTheory.Equivalence.commShift_of_functor : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (E : C ≌ D) (A : Type u_3) [inst_2 : AddGroup A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] [inst_5 : E.functor.CommShift A],
  E.CommShift A
-- Mathlib.CategoryTheory.Monoidal.Conv
CategoryTheory.Conv.instOne : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : C} → [CategoryTheory.ComonObj M] → [CategoryTheory.MonObj N] → One (CategoryTheory.Conv M N)
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- 7.64(b) in [axler2024]  -/
LinearMap.ker_adjoint_comp_self : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F] (A : E →ₗ[𝕜] F),
  (LinearMap.adjoint A ∘ₗ A).ker = A.ker
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
seminormFromConst'.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (c : R) (f : RingSeminorm R) (x : R),
  seminormFromConst' c f x = iInf (seminormFromConst_seq c f x)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.typeParameter.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.typeParameter = 1
-- Mathlib.Topology.EMetricSpace.Defs
EMetric.toUniformSpace_ofEDist : ∀ {α : Type u} [inst : EDist α] (edist_self : ∀ (x : α), edist x x = 0)
  (edist_comm : ∀ (x y : α), edist x y = edist y x) (edist_triangle : ∀ (x y z : α), edist x z ≤ edist x y + edist y z),
  PseudoEMetricSpace.toUniformSpace = uniformSpaceOfEDist edist edist_self edist_comm edist_triangle
-- Mathlib.MeasureTheory.MeasurableSpace.Prod
/-- `Prod.map` of two measurable embeddings is a measurable embedding.  -/
MeasurableEmbedding.prodMap : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {δ : Type u_6} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} {f : α → β} {g : γ → δ},
  MeasurableEmbedding g → MeasurableEmbedding f → MeasurableEmbedding (Prod.map g f)
-- Std.Internal.Do.Order.Lemmas
Std.Internal.Do.CompleteLattice.meet_le_of_le_himp_comm : ∀ {l : Type u} [inst : Lean.Order.CompleteLattice l] {P Q R : l}
  [∀ (a : l), Lean.Order.PreservesSup (Lean.Order.meet a)],
  Lean.Order.PartialOrder.rel Q (Lean.Order.himp P R) → Lean.Order.PartialOrder.rel (Lean.Order.meet P Q) R
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₆_of_isCharTwoJNeZeroNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharTwoJNeZeroNF], W.c₆ = -W.b₂ ^ 3 - 864 * W.a₆
-- Lean.Meta.Tactic.Grind.EMatch
/-- Returns "applications" in the given goal that may match `p`.
We say "applications," because we assume a constant is a zero-ary application.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.getAppsOf : Lean.Expr → Lean.Meta.Grind.GoalM (Option (List Lean.Expr))
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.Basic
basisOfPiSpaceOfLinearIndependent.congr_simp : ∀ {K : Type u} [inst : DivisionRing K] {ι : Type u_1} [inst_1 : Fintype ι] [inst_2 : Decidable (Nonempty ι)]
  {b b_1 : ι → ι → K} (e_b : b = b_1) (hb : LinearIndependent K b),
  basisOfPiSpaceOfLinearIndependent hb = basisOfPiSpaceOfLinearIndependent ⋯
-- Mathlib.Topology.Separation.Regular
/-- A `T₅` space is a `T₄` space.  -/
T5Space.toT4Space : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T5Space X], T4Space X
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zero_mem_neg_add_iff : ∀ {α : Type u_2} [inst : AddGroup α] {s t : Set α}, 0 ∈ -t + s ↔ ¬Disjoint s t
-- Mathlib.NumberTheory.Padics.PadicNumbers
PadicSeq.equiv_zero_of_val_eq_of_equiv_zero : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {f g : PadicSeq p},
  (∀ (k : ℕ), padicNorm p (↑f k) = padicNorm p (↑g k)) → f ≈ 0 → g ≈ 0
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.con.eq_1 : ∀ (L : FirstOrder.Language) {α : Type w'} (a : α), L.con a = Sum.inr a
-- Mathlib.Algebra.Star.SelfAdjoint
Pi.isSelfAdjoint : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Star (α i)] {f : (i : ι) → α i},
  IsSelfAdjoint f ↔ ∀ (i : ι), IsSelfAdjoint (f i)
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.toFun_sub : ∀ {α : Type u_1} {β : Type u_2} [inst : Sub β] (f g : UniformFun α β),
  UniformFun.toFun (f - g) = UniformFun.toFun f - UniformFun.toFun g
-- Mathlib.Algebra.Category.Ring.Limits
CommSemiRingCat.commSemiringObj : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J CommSemiRingCat) →
      (j : J) → CommSemiring ((F.comp (CategoryTheory.forget CommSemiRingCat)).obj j)