mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Convenient.Category
/-- The functor `ContinuousGeneratedByCat X ⥤ TopCat` which sends a
topological space `Y` in the category `ContinuousGeneratedByCat X` to
the topological space `WithGeneratedByTopology X Y`.  -/
ContinuousGeneratedByCat.toTopCat : {ι : Type t} →
  (X : ι → Type u) →
    [inst : (i : ι) → TopologicalSpace (X i)] → CategoryTheory.Functor (ContinuousGeneratedByCat X) TopCat
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `J` is `u`-small, the forgetful functor from `GrpCat.{u}` preserves limits of shape `J`.  -/
GrpCat.forget_preservesLimitsOfShape : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] [Small.{u, v} J],
  CategoryTheory.Limits.PreservesLimitsOfShape J (CategoryTheory.forget GrpCat)
-- Mathlib.Data.WSeq.Defs
/-- Split the sequence at position `n` into a finite initial segment
and the weak sequence tail  -/
Stream'.WSeq.splitAt : {α : Type u} → Stream'.WSeq α → ℕ → Computation (List α × Stream'.WSeq α)
-- Mathlib.CategoryTheory.Monad.Equalizer
/-- This is the Beck fork. It is a split equalizer, in particular an equalizer.  -/
CategoryTheory.Comonad.beckFork : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {T : CategoryTheory.Comonad C} → (X : T.Coalgebra) → CategoryTheory.Limits.Fork (T.map X.a) (T.δ.app X.A)
-- Mathlib.Algebra.Group.Defs
negSucc_zsmul : ∀ {G : Type u_2} [inst : SubNegMonoid G] (a : G) (n : ℕ), Int.negSucc n • a = -((n + 1) • a)
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.formatWeekdayShort : Std.Time.DateFormatSymbols → Std.Time.Weekday → String
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.S.nat.inj : ∀ {n n_1 : ℕ}, Mathlib.Deriving.Encodable.S.nat✝ n = Mathlib.Deriving.Encodable.S.nat✝ n_1 → n = n_1
-- Lean.Data.Lsp.Extra
Lean.Lsp.instToJsonDependencyBuildMode : Lean.ToJson Lean.Lsp.DependencyBuildMode
-- Mathlib.Algebra.Module.CharacterModule
/-- Any linear map `L : A → B⋆` induces a character in `(A ⊗ B)⋆` by `a ⊗ b ↦ L a b`.
 -/
CharacterModule.uncurry : {R : Type uR} →
  [inst : CommRing R] →
    {A : Type uA} →
      [inst_1 : AddCommGroup A] →
        {B : Type uB} →
          [inst_2 : AddCommGroup B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] → (A →ₗ[R] CharacterModule B) →ₗ[R] CharacterModule (TensorProduct R A B)
-- Lean.Compiler.LCNF.Types
/-- `uint32` is a 32-bit unsigned integer.
 -/
Lean.Compiler.LCNF.ImpureType.uint32 : Lean.Expr
-- Init.Data.SInt.Basic
/-- Converts a 64-bit signed integer to a natural number, mapping all negative numbers to `0`.

Use `Int64.toBitVec` to obtain the two's complement representation.
 -/
Int64.toNatClampNeg : Int64 → ℕ
-- Mathlib.Algebra.Group.Graph
MonoidHom.mgraph_eq_mrange_prod : ∀ {G : Type u_1} {H : Type u_2} [inst : Monoid G] [inst_1 : Monoid H] (f : G →* H),
  f.mgraph = MonoidHom.mrange ((MonoidHom.id G).prod f)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Misc
/-- Let `M` be a `(n+1) × (n+1)` matrix. Assume that all columns, but the `j₀`-column, sums to zero.
Then its determinant is, up to sign, the sum of the `j₀`-column times the determinant of the
matrix obtained by deleting any row and the `j₀`-column.  -/
Matrix.det_eq_sum_column_mul_submatrix_succAbove_succAbove_det : ∀ {R : Type u_1} [inst : CommRing R] {n : ℕ} (M : Matrix (Fin (n + 1)) (Fin (n + 1)) R) (i₀ j₀ : Fin (n + 1)),
  (∀ (j : Fin (n + 1)), j ≠ j₀ → ∑ i, M i j = 0) →
    M.det = ((-1) ^ (↑i₀ + ↑j₀) * ∑ i, M i j₀) * (M.submatrix i₀.succAbove j₀.succAbove).det
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.finite_div : ∀ {α : Type u_2} [inst : Group α] {s t : Set α}, (s / t).Finite ↔ s.Finite ∧ t.Finite ∨ s = ∅ ∨ t = ∅
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
HomologicalComplex.restrictionCyclesIso_hom_iCycles : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsRelIff] (j k : ι) (hk : c.next j = k) {j' k' : ι'}
  (hj' : e.f j = j') (hk' : e.f k = k') (hk'' : c'.next j' = k') [inst_3 : K.HasHomology j']
  [inst_4 : (K.restriction e).HasHomology j],
  CategoryTheory.CategoryStruct.comp (K.restrictionCyclesIso e j k hk hj' hk' hk'').hom (K.iCycles j') =
    CategoryTheory.CategoryStruct.comp ((K.restriction e).iCycles j) (K.restrictionXIso e hj').hom
-- Init.Data.Iterators.Basic
Std.Iter.IsPlausibleIndirectSuccessorOf.below.cons_right : ∀ {α β : Type w} [inst : Std.Iterator α Id β] {a : Std.Iter β}
  {motive : (a_1 : Std.Iter β) → a.IsPlausibleIndirectSuccessorOf a_1 → Prop} {it' it : Std.Iter β}
  (h' : a.IsPlausibleIndirectSuccessorOf it') (h : it'.IsPlausibleSuccessorOf it),
  Std.Iter.IsPlausibleIndirectSuccessorOf.below h' → motive it' h' → Std.Iter.IsPlausibleIndirectSuccessorOf.below ⋯
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.IsStableUnderShiftBy.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C} {A : Type u_2}
  [inst_1 : AddMonoid A] [inst_2 : CategoryTheory.HasShift C A] {a : A}, P ≤ P.shift a → P.IsStableUnderShiftBy a
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.sub_toGerm : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace γ]
  [inst_2 : AddGroup γ] [inst_3 : IsTopologicalAddGroup γ] (f g : α →ₘ[μ] γ), (f - g).toGerm = f.toGerm - g.toGerm
-- Mathlib.Topology.MetricSpace.Pseudo.Constructions
dist_prod_same_left : ∀ {α : Type u_1} {β : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {x : α} {y₁ y₂ : β},
  dist (x, y₁) (x, y₂) = dist y₁ y₂
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.toArray_iter : ∀ {γ : Type u} {α β : Type v} {s : Std.Slice γ} [inst : Std.ToIterator (Std.Slice γ) Id α β]
  [inst_1 : Std.Iterator α Id β] [Std.Iterators.Finite α Id], s.iter.toArray = s.toArray
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.cylinder_I₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F),
  (CategoryTheory.PreOneHypercover.cylinder f g).I₀ = ((i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i))
-- Mathlib.GroupTheory.Nilpotent
_private.Mathlib.GroupTheory.Nilpotent.0.Subgroup.comap_center_subst : ∀ {G : Type u_1} [inst : Group G] {H₁ H₂ : Subgroup G} [inst_1 : H₁.Normal] [inst_2 : H₂.Normal],
  H₁ = H₂ →
    Subgroup.comap (QuotientGroup.mk' H₁) (Subgroup.center (G ⧸ H₁)) =
      Subgroup.comap (QuotientGroup.mk' H₂) (Subgroup.center (G ⧸ H₂))
-- Std.Data.HashMap.Raw
/-- Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.  -/
Std.HashMap.Raw.getThenInsertIfNew? : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Std.HashMap.Raw α β → α → β → Option β × Std.HashMap.Raw α β
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.yoneda'_obj_obj : ∀ (α : Type u), (CategoryTheory.yoneda'.obj α).obj = CategoryTheory.yoneda.obj α
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `continuous_add_const`. -/
continuous_add_right : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Add M] [SeparatelyContinuousAdd M] (m : M),
  Continuous fun x => x + m
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- The equivalence between a topological group `G` and `Gᵐᵒᵖ` as a uniform equivalence when `G`
is equipped with the right uniformity and `Gᵐᵒᵖ` with the left uniformity.  -/
MulOpposite.opUniformEquivRight : (G : Type u_2) → [inst : Group G] → [inst_1 : TopologicalSpace G] → [inst_2 : IsTopologicalGroup G] → G ≃ᵤ Gᵐᵒᵖ
-- Mathlib.Topology.Order
isOpen_coinduced : ∀ {α : Type u_1} {β : Type u_2} {t : TopologicalSpace α} {s : Set β} {f : α → β}, IsOpen s ↔ IsOpen (f ⁻¹' s)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_eq_some_getKeyD_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, t.contains a = true → t.getKey? a = some (t.getKeyD a fallback)
-- Init.System.IOError
IO.Error.fopenErrorToString : String → String → UInt32 → Option String → String
-- Mathlib.Analysis.Calculus.FDeriv.Add
hasFDerivWithinAt_sub_const_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {s : Set E} (c : F), HasFDerivWithinAt (fun x => f x - c) f' s x ↔ HasFDerivWithinAt f f' s x
-- Mathlib.Order.KrullDimension
LTSeries.withLength.congr_simp : ∀ (α : Type u_1) [inst : Preorder α] [inst_1 : InfiniteDimensionalOrder α] (n n_1 : ℕ),
  n = n_1 → LTSeries.withLength α n = LTSeries.withLength α n_1
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingHom.coe_coe_ringHom : ∀ {α : Type u_2} {β : Type u_3} [inst : NonAssocSemiring α] [inst_1 : Preorder α] [inst_2 : NonAssocSemiring β]
  [inst_3 : Preorder β] (f : α →+*o β), ⇑↑f = ⇑f
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.Homotopy.compRight_h₁ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} {φ₁ φ₂ : S₁ ⟶ S₂} (h : CategoryTheory.ShortComplex.Homotopy φ₁ φ₂)
  (ψ : S₂ ⟶ S₃), (h.compRight ψ).h₁ = CategoryTheory.CategoryStruct.comp h.h₁ ψ.τ₁
-- Mathlib.ModelTheory.Bundled
FirstOrder.Language.Theory.ModelType.defaultExpansion_struc : ∀ {L : FirstOrder.Language} {T : L.Theory} {L' : FirstOrder.Language} {φ : L →ᴸ L'} (h : φ.Injective)
  [inst : (n : ℕ) → (f : L'.Functions n) → Decidable (f ∈ Set.range fun f => φ.onFunction f)]
  [inst_1 : (n : ℕ) → (r : L'.Relations n) → Decidable (r ∈ Set.range fun r => φ.onRelation r)] (M : T.ModelType)
  [inst_2 : Inhabited ↑M], (FirstOrder.Language.Theory.ModelType.defaultExpansion h M).struc = φ.defaultExpansion ↑M
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.isSingular_aleph_omega0 : (Cardinal.aleph Ordinal.omega0).IsSingular
-- Mathlib.Analysis.Normed.Ring.Finite
IsOfFinOrder.norm_eq_one : ∀ {α : Type u_1} [inst : NormedRing α] [NormMulClass α] [NormOneClass α] {a : α}, IsOfFinOrder a → ‖a‖ = 1
-- Batteries.Data.Nat.Lemmas
Nat.recAuxOn_zero : ∀ {motive : ℕ → Sort u_1} (zero : motive 0) (succ : (n : ℕ) → motive n → motive (n + 1)),
  Nat.recAuxOn 0 zero succ = zero
-- Std.Time.Format.Modifier
Std.Time.Modifier.n.sizeOf_spec : ∀ (presentation : Std.Time.Number), sizeOf (Std.Time.Modifier.n presentation) = 1 + sizeOf presentation
-- Mathlib.Probability.ConditionalProbability
ProbabilityTheory.cond.eq_1 : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} (μ : MeasureTheory.Measure Ω) (s : Set Ω), μ[|s] = (μ s)⁻¹ • μ.restrict s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_int_mul_two_pi_sub : ∀ (x : ℂ) (n : ℤ), Complex.cos (↑n * (2 * ↑Real.pi) - x) = Complex.cos x
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.hom_inv_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E F : CategoryTheory.PreZeroHypercover S} (e : E ≅ F)
  (i : E.I₀), CategoryTheory.CategoryStruct.comp (e.hom.h₀ i) (e.inv.h₀ (e.hom.s₀ i)) = CategoryTheory.eqToHom ⋯
-- Mathlib.Data.Rat.Floor
/-- This variant of `ceil_def` uses the `Int.ceil` (for any `FloorRing`) rather than `Rat.ceil`.
 -/
Rat.ceil_def' : ∀ (q : ℚ), ⌈q⌉ = -(-q.num / ↑q.den)
-- Mathlib.Order.CompleteLattice.Basic
iInf_insert : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {s : Set β} {b : β},
  ⨅ x ∈ insert b s, f x = f b ⊓ ⨅ x ∈ s, f x
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.ExtendScalars.map'_comp : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S) {M₁ M₂ M₃ : ModuleCat R}
  (l₁₂ : M₁ ⟶ M₂) (l₂₃ : M₂ ⟶ M₃),
  ModuleCat.ExtendScalars.map' f (CategoryTheory.CategoryStruct.comp l₁₂ l₂₃) =
    CategoryTheory.CategoryStruct.comp (ModuleCat.ExtendScalars.map' f l₁₂) (ModuleCat.ExtendScalars.map' f l₂₃)
-- Mathlib.Topology.Connected.CardComponents
/-- If `f : X → Y` is an open and closed map and `Y` is connected, the number of connected
components of `X` is bounded by the cardinality of the fiber of any point.  -/
IsOpenMap.enatCard_connectedComponents_le_encard_preimage_singleton : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f → IsClosedMap f → ∀ [ConnectedSpace Y] (y : Y), ENat.card (ConnectedComponents X) ≤ (f ⁻¹' {y}).encard
-- Mathlib.Data.Finsupp.Weight
Finsupp.weight_single : ∀ {σ : Type u_1} {M : Type u_2} {R : Type u_3} [inst : Semiring R] (w : σ → M) [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (s : σ) (r : R), ((Finsupp.weight w) fun₀ | s => r) = r • w s
-- Init.Data.UInt.Lemmas
USize.le_antisymm : ∀ {a b : USize}, a ≤ b → b ≤ a → a = b
-- Mathlib.FieldTheory.SeparableDegree
/-- If the field extension `E / F` is transcendental, then `Field.Emb F E` is infinite.  -/
Field.infinite_emb_of_transcendental : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] [H : Algebra.Transcendental F E],
  Infinite (Field.Emb F E)
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.IrreducibleCloseds.equivSubtype_symm_apply : ∀ {α : Type u_2} [inst : TopologicalSpace α] (a : { x // IsIrreducible x ∧ IsClosed x }),
  TopologicalSpace.IrreducibleCloseds.equivSubtype.symm a = { carrier := ↑a, isIrreducible' := ⋯, isClosed' := ⋯ }
-- Mathlib.Order.Filter.Pi
/-- The indexed product of a (possibly, infinite) family of principal filters
is generated by the finite `Set.pi` cylinders.

If the index type is finite, then the indexed product of principal filters
is a principal filter, see `pi_principal`.  -/
Filter.hasBasis_pi_principal : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : (i : ι) → Set (α i)),
  (Filter.pi fun i => Filter.principal (s i)).HasBasis Set.Finite fun x => x.pi s
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_singleton : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (μ : (i : ι) → MeasureTheory.Measure (X i))
  [hμ : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] [Countable ι] [∀ (i : ι), MeasurableSingletonClass (X i)]
  (f : (i : ι) → X i), (MeasureTheory.Measure.infinitePi μ) {f} = ∏' (i : ι), (μ i) {f i}
-- Mathlib.Algebra.Order.Star.Basic
StarRingEquivClass.instOrderIsoClass : ∀ {F : Type u_3} {R : Type u_4} {S : Type u_5} [inst : NonUnitalSemiring R] [inst_1 : PartialOrder R]
  [inst_2 : StarRing R] [StarOrderedRing R] [inst_4 : NonUnitalSemiring S] [inst_5 : PartialOrder S]
  [inst_6 : StarRing S] [StarOrderedRing S] [inst_8 : EquivLike F R S] [StarRingEquivClass F R S], OrderIsoClass F R S
-- Init.Data.Array.GetLit
Array.extLit : ∀ {α : Type u_1} {n : ℕ} (xs ys : Array α) (hsz₁ : xs.size = n) (hsz₂ : ys.size = n),
  (∀ (i : ℕ) (hi : i < n), xs.getLit i hsz₁ hi = ys.getLit i hsz₂ hi) → xs = ys
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.getEntryLE!_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited (α × β)] {k : α}, t₁.Equiv t₂ → t₁.getEntryLE! k = t₂.getEntryLE! k
-- Mathlib.Data.Set.Finite.Basic
Set.fintypeImage : {α : Type u} → {β : Type v} → [DecidableEq β] → (s : Set α) → (f : α → β) → [Fintype ↑s] → Fintype ↑(f '' s)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasProd.of_nat_of_neg_add_one : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {m m' : M} [ContinuousMul M] {f : ℤ → M},
  HasProd (fun n => f ↑n) m → HasProd (fun n => f (-(↑n + 1))) m' → HasProd f (m * m')
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.PresheafedSpace.GlueData.opensImagePreimageMap_app' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.PresheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] (i j k : D.J) (U : TopologicalSpace.Opens ↑↑(D.U i)),
  ∃ (eq :
    Opposite.op
        ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor
              (CategoryTheory.Limits.pullback.snd (D.f j i) (D.f j k))).obj
          (Opposite.unop
            (Opposite.op
              ((TopologicalSpace.Opens.map
                    (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k))
                        (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base).1
                (Opposite.unop (Opposite.op U)))))) =
      (TopologicalSpace.Opens.map (D.f j k).base).op.obj
        (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U)))),
    CategoryTheory.CategoryStruct.comp (D.opensImagePreimageMap i j U)
        ((D.f j k).c.app (Opposite.op ((TopologicalSpace.Opens.map (D.ι j).base).obj (⋯.functor.obj U)))) =
      CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k))
                (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).c.app
          (Opposite.op U))
        (CategoryTheory.CategoryStruct.comp
          (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp
            (CategoryTheory.Limits.pullback.snd (D.f j i) (D.f j k))
            (Opposite.unop
              (Opposite.op
                ((TopologicalSpace.Opens.map
                      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (D.f j i) (D.f j k))
                          (CategoryTheory.CategoryStruct.comp (D.t j i) (D.f i j))).base).1
                  (Opposite.unop (Opposite.op U))))))
          ((D.V (j, k)).presheaf.map (CategoryTheory.eqToHom eq)))
-- Mathlib.NumberTheory.Height.Projectivization
Projectivization.logHeight_nonneg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2} [inst_2 : Finite ι]
  (x : Projectivization K (ι → K)), 0 ≤ x.logHeight
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalClear : Lean.Elab.Tactic.Tactic
-- Init.Data.Vector.Algebra
Vector.getElem_neg : ∀ {α : Type u_1} {n : ℕ} [inst : Neg α] (xs : Vector α n) (i : ℕ) (h : i < n), (-xs)[i] = -xs[i]
-- Mathlib.Data.Multiset.UnionInter
Multiset.disjoint_add_left : ∀ {α : Type u_1} {s t u : Multiset α}, Disjoint (s + t) u ↔ Disjoint s u ∧ Disjoint t u
-- Aesop.RuleTac.Descr
Aesop.RuleTacDescr.tacticStx : Lean.Syntax → Aesop.RuleTacDescr
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.getTerm : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → Aesop.Frontend.RuleConfig → m Lean.Term
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.ReflexiveCofork.app_one_eq_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C}
  (G : CategoryTheory.Limits.ReflexiveCofork F), G.ι.app CategoryTheory.Limits.WalkingReflexivePair.zero = G.π
-- Mathlib.GroupTheory.OreLocalization.Basic
OreLocalization.instSMul : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} → [inst_2 : MulAction R X] → SMul (OreLocalization S R) (OreLocalization S X)
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.extend_of_mem_I : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (F : f₀.Homotopy f₁) {t : ℝ} (ht : t ∈ unitInterval), F.extend t = F.curry ⟨t, ht⟩
-- Lean.Widget.Commands
Lean.Widget.addWidgetSpec : Lean.ParserDescr
-- Init.Meta.Defs
/-- Converts a substring to the Lean compiler's representation of names. The resulting name is
hierarchical, and the string is split at the dots (`'.'`).

`"a.b".toRawSubstring.toName` is the name `a.b`, not `«a.b»`. For the latter, use
`Name.mkSimple ∘ Substring.Raw.toString`.
-- TODO: deprecate old name
 -/
Substring.Raw.toName : Substring.Raw → Lean.Name
-- Mathlib.Data.Num.Bitwise
/-- `SNum.czAdd a b n` is `n + a - b` (where `a` and `b` should be read as either 0 or 1).
This is useful to implement the carry system in `cAdd`.  -/
SNum.czAdd : Bool → Bool → SNum → SNum
-- Mathlib.LinearAlgebra.Matrix.Charpoly.FiniteField
ZMod.charpoly_pow_card : ∀ {n : Type u_1} [inst : DecidableEq n] [inst_1 : Fintype n] {p : ℕ} [inst_2 : Fact (Nat.Prime p)]
  (M : Matrix n n (ZMod p)), (M ^ p).charpoly = M.charpoly
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.instModuleResidueFieldOfAlgebra : (R : Type u_1) →
  [inst : CommRing R] →
    [inst_1 : IsLocalRing R] →
      {R₀ : Type u_4} → [inst_2 : CommRing R₀] → [Algebra R₀ R] → Module R₀ (IsLocalRing.ResidueField R)
-- Lean.Elab.Do.Basic
/-- Match a monad application `m α`, returning `MonadInfo` for `m` and `α`.  -/
Lean.Elab.Do.DoOps.splitMonadApp? : Lean.Elab.Do.DoOps → Lean.Expr → Lean.Elab.TermElabM (Option (Lean.Elab.Do.MonadInfo × Lean.Expr))
-- Mathlib.CategoryTheory.Elements
CategoryTheory.Functor.Elements.initialOfRepresentableBy_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor Cᵒᵖ (Type u_1)} {X : C}
  (h : F.RepresentableBy X), (CategoryTheory.Functor.Elements.initialOfRepresentableBy h).fst = Opposite.op X
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.π_comp_H0Iso_hom : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G),
  CategoryTheory.CategoryStruct.comp (groupCohomology.π A 0) (groupCohomology.H0Iso A).hom =
    (groupCohomology.cocyclesIso₀ A).hom
-- Mathlib.RingTheory.DedekindDomain.IntegralClosure
/-- Send a set of `x`s in a finite extension `L` of the fraction field of `R`
to `(y : R) • x ∈ integralClosure R L`.  -/
exists_integral_multiples : ∀ (A : Type u_1) (K : Type u_2) [inst : CommRing A] [inst_1 : Field K] [inst_2 : Algebra A K] [IsFractionRing A K]
  {L : Type u_3} [inst_4 : Field L] [inst_5 : Algebra K L] [inst_6 : Algebra A L] [IsScalarTower A K L]
  [FiniteDimensional K L] [IsDomain A] (s : Finset L), ∃ y, y ≠ 0 ∧ ∀ x ∈ s, IsIntegral A (y • x)
-- Mathlib.Geometry.Manifold.Instances.Real
IccLeftChart_symm_apply_of_le : ∀ {x y : ℝ} [hxy : Fact (x < y)] {z : EuclideanHalfSpace 1} (hz : (↑z).ofLp 0 ≤ y - x),
  ↑(IccLeftChart x y).symm z = ⟨(↑z).ofLp 0 + x, ⋯⟩
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- **Alias** of `ContinuousLinearMap.postcompUniformConvergenceCLM`.

---

Post-composition by a *fixed* continuous linear map as a continuous linear map for the uniform
convergence topology.  -/
ContinuousLinearMap.postcomp_uniformConvergenceCLM : {𝕜₁ : Type u_6} →
  {𝕜₂ : Type u_7} →
    {𝕜₃ : Type u_8} →
      [inst : NormedField 𝕜₁] →
        [inst_1 : NormedField 𝕜₂] →
          [inst_2 : NormedField 𝕜₃] →
            {σ : 𝕜₁ →+* 𝕜₂} →
              {τ : 𝕜₂ →+* 𝕜₃} →
                {ρ : 𝕜₁ →+* 𝕜₃} →
                  [RingHomCompTriple σ τ ρ] →
                    {E : Type u_9} →
                      {F : Type u_10} →
                        {G : Type u_11} →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : Module 𝕜₁ E] →
                              [inst_6 : AddCommGroup F] →
                                [inst_7 : Module 𝕜₂ F] →
                                  [inst_8 : AddCommGroup G] →
                                    [inst_9 : Module 𝕜₃ G] →
                                      [inst_10 : TopologicalSpace E] →
                                        [inst_11 : TopologicalSpace F] →
                                          [inst_12 : TopologicalSpace G] →
                                            (𝔖 : Set (Set E)) →
                                              [inst_13 : IsTopologicalAddGroup F] →
                                                [inst_14 : IsTopologicalAddGroup G] →
                                                  [inst_15 : ContinuousConstSMul 𝕜₃ G] →
                                                    [inst_16 : ContinuousConstSMul 𝕜₂ F] →
                                                      (F →SL[τ] G) →
                                                        UniformConvergenceCLM σ F 𝔖 →SL[τ] UniformConvergenceCLM ρ G 𝔖