mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.symm_refl : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_5} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_9}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {n : WithTop ℕ∞},
  (Diffeomorph.refl I M n).symm = Diffeomorph.refl I M n
-- Mathlib.CategoryTheory.Shift.SingleFunctors
CategoryTheory.SingleFunctors.evaluation_map : ∀ (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] {A : Type u_5} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift D A] (a : A) {x x_1 : CategoryTheory.SingleFunctors C D A} (φ : x ⟶ x_1),
  (CategoryTheory.SingleFunctors.evaluation C D a).map φ = φ.hom a
-- Mathlib.Algebra.FreeMonoid.Basic
/-- An induction principle on free monoids, with cases for `0`, `FreeAddMonoid.of` and `+`.  -/
FreeAddMonoid.inductionOn : ∀ {α : Type u_1} {motive : FreeAddMonoid α → Prop} (z : FreeAddMonoid α),
  motive 0 →
    (∀ (x : α), motive (FreeAddMonoid.of x)) →
      (∀ (x y : FreeAddMonoid α), motive x → motive y → motive (x + y)) → motive z
-- Init.Data.String.Basic
String.Pos.ofSlice_le_ofSlice_iff : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {q r : (s.slice p₀ p₁ h).Pos},
  String.Pos.ofSlice q ≤ String.Pos.ofSlice r ↔ q ≤ r
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.addMonoid : {α : Type u} → [AddMonoid α] → AddMonoid (WithBot α)
-- Mathlib.RingTheory.Algebraic.Integral
/-- If `x : K` is algebraic over some ring `R`, then a nonzero `R`-multiple of it is contained
in the integral closure of `R` in `K`.  -/
IsAlgebraic.exists_smul_eq : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] {K : Type u_4} [inst_2 : CommRing K]
  [inst_3 : Algebra S K] [inst_4 : Algebra R K] [IsIntegralClosure S R K] {x : K},
  IsAlgebraic R x → ∃ r s, r ≠ 0 ∧ r • x = (algebraMap S K) s
-- Mathlib.Algebra.Homology.SpectralObject.Page
/-- The monomorphism `E^{n₁}(f₁, f₂, f₃) ⟶ opZ^{n₁}(f₂, f₃) ⟶ `.  -/
CategoryTheory.Abelian.SpectralObject.ιE : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          (X : CategoryTheory.Abelian.SpectralObject C ι) →
            {i j k l : ι} →
              (f₁ : i ⟶ j) →
                (f₂ : j ⟶ k) →
                  (f₃ : k ⟶ l) →
                    (n₀ n₁ n₂ : ℤ) →
                      (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.ιE._auto_1) →
                        (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.ιE._auto_3) →
                          X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂ ⟶ X.opcycles f₂ f₃ n₁
-- Mathlib.Topology.Instances.Int
Int.ball_eq_Ioo : ∀ (x : ℤ) (r : ℝ), Metric.ball x r = Set.Ioo ⌊↑x - r⌋ ⌈↑x + r⌉
-- Mathlib.CategoryTheory.Limits.FinallySmall
/-- A category is `InitiallySmall.{w}` if there is an initial functor from a `w`-small category.  -/
CategoryTheory.InitiallySmall : (J : Type u) → [CategoryTheory.Category.{v, u} J] → Prop
-- Mathlib.CategoryTheory.WithTerminal.Basic
/-- The pseudofunctor from `Cat` to `Cat` defined with `WithTerminal`.  -/
CategoryTheory.WithTerminal.pseudofunctor : CategoryTheory.Pseudofunctor CategoryTheory.Cat CategoryTheory.Cat
-- Mathlib.CategoryTheory.Presentable.EssentiallyLarge
CategoryTheory.ObjectProperty.IsCardinalFilteredGenerator.essentiallyLarge_top : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {κ : Cardinal.{w}} [inst_1 : Fact κ.IsRegular]
  [CategoryTheory.LocallySmall.{w, v, u} C] {P : CategoryTheory.ObjectProperty C}
  [CategoryTheory.ObjectProperty.EssentiallySmall.{w, v, u} P],
  P.IsCardinalFilteredGenerator κ → CategoryTheory.ObjectProperty.EssentiallySmall.{w + 1, v, u} ⊤
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- `ContinuousLinearMap.toSpanSingleton` as a linear equivalence. See
`ContinuousLinearMap.toSpanSingletonLIE` for the isometric version
and `ContinuousLinearMap.toSpanSingletonCLE` for the continuous version.  -/
ContinuousLinearMap.toSpanSingletonLE : (R : Type u_1) →
  (S : Type u_2) →
    (M : Type u_3) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R M] →
              [inst_4 : Module S M] →
                [inst_5 : SMulCommClass R S M] →
                  [inst_6 : TopologicalSpace M] →
                    [inst_7 : ContinuousAdd M] →
                      [inst_8 : ContinuousConstSMul S M] →
                        [inst_9 : TopologicalSpace R] → [ContinuousSMul R M] → M ≃ₗ[S] R →L[R] M
-- Mathlib.Algebra.Torsor.Basic
/-- Subtracting two points from the same point produces equal results
if and only if those points are equal.  -/
sdiv_right_cancel_iff : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [T : Torsor G P] {p₁ p₂ p : P}, p /ₛ p₁ = p /ₛ p₂ ↔ p₁ = p₂
-- Mathlib.Data.Nat.Factorial.Basic
Nat.add_descFactorial_eq_ascFactorial : ∀ (n k : ℕ), (n + k).descFactorial k = (n + 1).ascFactorial k
-- Mathlib.CategoryTheory.Category.Quiv
CategoryTheory.Prefunctor.of_toQuivHom : ∀ {C D : Type} [inst : Quiver C] [inst_1 : Quiver D] (F : C ⥤q D),
  CategoryTheory.Prefunctor.ofQuivHom (CategoryTheory.Prefunctor.toQuivHom F) = F
-- Mathlib.MeasureTheory.Integral.Prod
MeasureTheory.Integrable.comp_fst : ∀ {α : Type u_1} {β : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ : MeasureTheory.Measure α} [inst_2 : NormedAddCommGroup E] {f : α → E},
  MeasureTheory.Integrable f μ →
    ∀ (ν : MeasureTheory.Measure β) [MeasureTheory.IsFiniteMeasure ν],
      MeasureTheory.Integrable (fun x => f x.1) (μ.prod ν)
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.cylinder.congr_simp : ∀ {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 f_1 : E.Hom F),
  f = f_1 →
    ∀ (g g_1 : E.Hom F),
      g = g_1 → CategoryTheory.PreOneHypercover.cylinder f g = CategoryTheory.PreOneHypercover.cylinder f_1 g_1
-- Batteries.Data.List.Basic
List.rotate'.eq_def : ∀ {α : Type u_1} (x : List α) (x_1 : ℕ),
  x.rotate' x_1 =
    match x, x_1 with
    | [], x => []
    | l, 0 => l
    | a :: l, n.succ => (l ++ [a]).rotate' n
-- Init.PropLemmas
Exists.imp' : ∀ {α : Sort u_2} {p : α → Prop} {β : Sort u_1} {q : β → Prop} (f : α → β),
  (∀ (a : α), p a → q (f a)) → (∃ a, p a) → ∃ b, q b
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.AddSubMap
WeierstrassCurve.Affine.Point.sym2x_zero_some : ∀ {R : Type u_1} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {x y : R} (h : W'.Nonsingular x y),
  WeierstrassCurve.Affine.Point.sym2x 0 (WeierstrassCurve.Affine.Point.some x y h) = ![x, 1, 0]
-- Mathlib.GroupTheory.Commutator.Basic
AddSubgroup.addCommutator_characteristic : ∀ {G : Type u_1} [inst : AddGroup G] (H₁ H₂ : AddSubgroup G) [h₁ : H₁.Characteristic] [h₂ : H₂.Characteristic],
  ⁅H₁, H₂⁆.Characteristic
-- Lean.Elab.DocString
/-- Converts the syntax of a documentation argument into a suitable value.
 -/
Lean.Doc.DocArg.ofSyntax : Lean.TSyntax `arg_val → Lean.Elab.TermElabM Lean.Doc.DocArg
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.one_left : ∀ {o : Ordinal.{u_1}}, o ≠ 0 → Ordinal.CNF 1 o = [(0, o)]
-- Mathlib.Geometry.Manifold.ContMDiff.Basic
ContMDiffAt.subtypeVal_comp_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] {E' : Type u_5} [inst_5 : NormedAddCommGroup E'] [inst_6 : NormedSpace 𝕜 E']
  {H' : Type u_6} [inst_7 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'} {M' : Type u_7}
  [inst_8 : TopologicalSpace M'] [inst_9 : ChartedSpace H M] [inst_10 : ChartedSpace H' M']
  (U : TopologicalSpace.Opens M') (f : M → ↥U) (x : M),
  ContMDiffAt I I' (↑⊤) (Subtype.val ∘ f) x ↔ ContMDiffAt I I' (↑⊤) f x
-- Lean.Meta.Match.Basic
Lean.Meta.Match.MatcherResult.counterExamples : Lean.Meta.Match.MatcherResult → Array Lean.Meta.Match.CounterExample
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.proj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (S : CategoryTheory.Functor C D) (T : D) (X : CategoryTheory.Comma S (CategoryTheory.Functor.fromPUnit T)),
  (CategoryTheory.CostructuredArrow.proj S T).obj X = X.left
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
/-- Bijection between a subsemiring `S` and `MulOpposite` of its opposite.  -/
Subsemiring.ringEquivOpMop : {R : Type u_2} → [inst : NonAssocSemiring R] → (S : Subsemiring R) → ↥S ≃+* (↥S.op)ᵐᵒᵖ
-- Mathlib.Algebra.ContinuedFractions.Translations
GenContFract.convs'Aux_succ_some : ∀ {K : Type u_1} [inst : DivisionRing K] {s : Stream'.Seq (GenContFract.Pair K)} {p : GenContFract.Pair K},
  s.head = some p → ∀ (n : ℕ), GenContFract.convs'Aux s (n + 1) = p.a / (p.b + GenContFract.convs'Aux s.tail n)
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.ε_def : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] (i : I),
  CategoryTheory.Functor.LaxMonoidal.ε (CategoryTheory.Pi.eval C i) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategoryStruct.tensorUnit (C i))
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Functor
AlgebraicGeometry.Proj.isLocallyFraction_comapStructureSheafFun : ∀ {A : Type u_1} {B : Type u_2} {σ : Type u_4} {τ : Type u_5} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : CommRing B] [inst_4 : SetLike τ B] [inst_5 : AddSubgroupClass τ B]
  {𝒜 : ℕ → σ} {ℬ : ℕ → τ} [inst_6 : GradedRing 𝒜] [inst_7 : GradedRing ℬ] (f : 𝒜 →+*ᵍ ℬ)
  (hf : HomogeneousIdeal.irrelevant ℬ ≤ HomogeneousIdeal.map f (HomogeneousIdeal.irrelevant 𝒜))
  (U : TopologicalSpace.Opens (ProjectiveSpectrum 𝒜)) (V : TopologicalSpace.Opens (ProjectiveSpectrum ℬ))
  (hUV : V.carrier ⊆ ⇑(AlgebraicGeometry.ProjectiveSpectrum.comap f hf) ⁻¹' U.carrier)
  (s : (x : ↥U) → HomogeneousLocalization.AtPrime 𝒜 (↑x).asHomogeneousIdeal.toSubmodule),
  (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction 𝒜).pred s →
    (AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction ℬ).pred
      (AlgebraicGeometry.Proj.comapStructureSheafFun f hf U V hUV s)
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
/-- The pullback over the terminal object is the product  -/
isProductOfIsTerminalIsPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {W X Y Z : C} →
      (f : X ⟶ Z) →
        (g : Y ⟶ Z) →
          (h : W ⟶ X) →
            (k : W ⟶ Y) →
              (H₁ : CategoryTheory.Limits.IsTerminal Z) →
                CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.PullbackCone.mk h k ⋯) →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk h k)
-- Mathlib.Data.Stream.Init
Stream'.ext : ∀ {α : Type u} {s₁ s₂ : Stream' α}, (∀ (n : ℕ), s₁.get n = s₂.get n) → s₁ = s₂
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.initialMul_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasStrictInitialObjects C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (X : C) [inst_3 : CategoryTheory.Limits.HasBinaryProduct (⊥_ C) X],
  (CategoryTheory.Limits.initialMul X).hom = CategoryTheory.Limits.prod.fst
-- Mathlib.CategoryTheory.MorphismProperty.LocalEpi
/-- A morphism `f` is a local epimorphism wrt. the object property `P`
if it satisfies left cancellation for morphisms with codomain in `P`.  -/
CategoryTheory.ObjectProperty.localEpi : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.ObjectProperty C → CategoryTheory.MorphismProperty C
-- Mathlib.RingTheory.Extension.Cotangent.BaseChange
Algebra.tensorH1CotangentOfFlat_tmul : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Module.Flat R T] (t : T) (x : Algebra.H1Cotangent R S),
  (Algebra.tensorH1CotangentOfFlat R S T) (t ⊗ₜ[R] x) = t • (Algebra.H1Cotangent.map R T S (TensorProduct R T S)) x
-- Init.Prelude
/-- The opaque methods that are available to `MacroM`.  -/
Lean.Macro.Methods : Type
-- Mathlib.Data.Fintype.EquivFin
/-- See `Infinite.exists_superset_card_eq` for a version that, for an `s : Finset α`,
provides a superset `t : Finset α`, `s ⊆ t` such that `#t` is fixed.  -/
Infinite.exists_subset_card_eq : ∀ (α : Type u_4) [Infinite α] (n : ℕ), ∃ s, s.card = n
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.NoAccidental.mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)},
  (∀ ⦃a a' : α⦄ ⦃b b' : β⦄ ⦃c c' : γ⦄, (a', b, c) ∈ t → (a, b', c) ∈ t → (a, b, c') ∈ t → a = a' ∨ b = b' ∨ c = c') →
    SimpleGraph.TripartiteFromTriangles.NoAccidental t
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instHasColimitsOfShapeDiscreteIndOfFinite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type v} [Finite α]
  [CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C],
  CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) (CategoryTheory.Ind C)
-- Mathlib.Data.Nat.Factorial.DoubleFactorial
_private.Mathlib.Data.Nat.Factorial.DoubleFactorial.0.Nat.doubleFactorial.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1) (h_3 : (k : ℕ) → motive k.succ.succ),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | k.succ.succ => h_3 k) =
    h_1 ()
-- Mathlib.SetTheory.ZFC.Basic
/-- `Insert x y` is the set `{x} ∪ y`  -/
ZFSet.Insert : ZFSet.{u_1} → ZFSet.{u_1} → ZFSet.{u_1}
-- Mathlib.Order.Atoms
CompleteLattice.isAtomistic_iff : ∀ {α : Type u_4} [inst : CompleteLattice α], IsAtomistic α ↔ ∀ (b : α), ∃ s, b = sSup s ∧ ∀ a ∈ s, IsAtom a
-- Init.Data.Option.Attach
Option.unattach_eq_some_iff : ∀ {α : Type u_1} {p : α → Prop} {o : Option { x // p x }} {x : α}, o.unattach = some x ↔ ∃ (h : p x), o = some ⟨x, h⟩
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
_private.Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol.0.ZMod.χ₈.match_1.eq_2 : ∀ (motive : ZMod 8 → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 2) (h_3 : Unit → motive 4)
  (h_4 : Unit → motive 6) (h_5 : Unit → motive 1) (h_6 : Unit → motive 7) (h_7 : Unit → motive 3)
  (h_8 : Unit → motive 5),
  (match 2 with
    | 0 => h_1 ()
    | 2 => h_2 ()
    | 4 => h_3 ()
    | 6 => h_4 ()
    | 1 => h_5 ()
    | 7 => h_6 ()
    | 3 => h_7 ()
    | 5 => h_8 ()) =
    h_2 ()
-- Mathlib.Topology.Irreducible
closure_image_preimage_of_isPreirreducible : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f : Y → X),
  IsOpenMap f → ∀ (s : Set X), (f ⁻¹' s).Nonempty → IsPreirreducible s → IsClosed s → closure (f '' f ⁻¹' s) = s
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- An initial object in the opposite category is terminal in the original category.  -/
CategoryTheory.Limits.IsInitial.unop : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : Cᵒᵖ} → CategoryTheory.Limits.IsInitial X → CategoryTheory.Limits.IsTerminal (Opposite.unop X)
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- A triangle in `C` is a sextuple `(X,Y,Z,f,g,h)` where `X,Y,Z` are objects of `C`,
and `f : X ⟶ Y`, `g : Y ⟶ Z`, `h : Z ⟶ X⟦1⟧` are morphisms in `C`.  -/
CategoryTheory.Pretriangulated.Triangle : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.HasShift C ℤ] → Type (max u v)
-- Mathlib.Data.Fin.VecNotation
Matrix.vecAlt1.eq_1 : ∀ {α : Type u} {m n : ℕ} (hm : m = n + n) (v : Fin m → α) (k : Fin n), Matrix.vecAlt1 hm v k = v ⟨↑k + ↑k + 1, ⋯⟩
-- Mathlib.Topology.Algebra.Monoid.Defs
instSeparatelyContinuousMulOfContinuousMul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [ContinuousMul M], SeparatelyContinuousMul M
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.instFunLike : {Γ : Type u_1} →
  {R : Type u_3} →
    {α : Type u_5} →
      [inst : PartialOrder Γ] →
        [inst_1 : AddCommMonoid R] → FunLike (HahnSeries.SummableFamily Γ R α) α (HahnSeries Γ R)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaGrp_obj_map_shrinkYonedaGrpObjObjEquiv_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] {M : CategoryTheory.Grp C} {Y Y' : Cᵒᵖ} (g : Y ⟶ Y')
  (f : Opposite.unop Y ⟶ M.X),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYonedaGrp.{w, v, u}.obj M).map g))
      (CategoryTheory.shrinkYonedaGrpObjObjEquiv.symm f) =
    CategoryTheory.shrinkYonedaGrpObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp g.unop f)
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleMap
circleMap_zero_div : ∀ (R₁ R₂ θ₁ θ₂ : ℝ), circleMap 0 R₁ θ₁ / circleMap 0 R₂ θ₂ = circleMap 0 (R₁ / R₂) (θ₁ - θ₂)
-- Batteries.Data.PairingHeap
_private.Batteries.Data.PairingHeap.0.Batteries.PairingHeapImp.Heap.size.match_1.eq_2 : ∀ {α : Type u_1} (motive : Batteries.PairingHeapImp.Heap α → Sort u_2) (a : α) (c s : Batteries.PairingHeapImp.Heap α)
  (h_1 : Unit → motive Batteries.PairingHeapImp.Heap.nil)
  (h_2 : (a : α) → (c s : Batteries.PairingHeapImp.Heap α) → motive (Batteries.PairingHeapImp.Heap.node a c s)),
  (match Batteries.PairingHeapImp.Heap.node a c s with
    | Batteries.PairingHeapImp.Heap.nil => h_1 ()
    | Batteries.PairingHeapImp.Heap.node a c s => h_2 a c s) =
    h_2 a c s
-- Mathlib.Data.Part
/-- The map operation for `Part` just maps the value and maintains the same domain.  -/
Part.map : {α : Type u_1} → {β : Type u_2} → (α → β) → Part α → Part β
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
Continuous.sigmoid : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : E → ℝ}, Continuous f → Continuous (Real.sigmoid ∘ f)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.leftMulMatrix : ∀ {S : Type u_2} [inst : Ring S] {A : Type u_4} [inst_1 : CommRing A] [inst_2 : Algebra A S] (pb : PowerBasis A S),
  (Algebra.leftMulMatrix pb.basis) pb.gen =
    Matrix.of fun i j => if ↑j + 1 = pb.dim then -pb.minpolyGen.coeff ↑i else if ↑i = ↑j + 1 then 1 else 0
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometry.toLinearMap_inj : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} [inst_2 : SeminormedAddCommGroup E] [inst_3 : SeminormedAddCommGroup E₂] [inst_4 : Module R E]
  [inst_5 : Module R₂ E₂] {f g : E →ₛₗᵢ[σ₁₂] E₂}, f.toLinearMap = g.toLinearMap ↔ f = g
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PullbackObjObj.mapArrowRight_right : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} {f₁ : CategoryTheory.Arrow C₁}
  {f₃ f₃' : CategoryTheory.Arrow C₃} (sq₁₃ : G.PullbackObjObj f₁.hom f₃.hom) (sq₁₃' : G.PullbackObjObj f₁.hom f₃'.hom)
  (sq : f₃ ⟶ f₃'),
  (sq₁₃.mapArrowRight sq₁₃' sq).right =
    ⋯.lift
      (CategoryTheory.CategoryStruct.comp sq₁₃.fst
        ((G.obj (Opposite.op f₁.left)).map (CategoryTheory.Arrow.Hom.left sq)))
      (CategoryTheory.CategoryStruct.comp sq₁₃.snd
        ((G.obj (Opposite.op f₁.right)).map (CategoryTheory.Arrow.Hom.right sq)))
      ⋯
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.polyOfInterest.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] (n n_1 : ℕ),
  n = n_1 → WittVector.polyOfInterest p n = WittVector.polyOfInterest p_1 n_1
-- Init.Data.SInt.Lemmas
Int8.toBitVec_inj : ∀ {a b : Int8}, a.toBitVec = b.toBitVec ↔ a = b
-- Mathlib.NumberTheory.Padics.PadicVal.Defs
padicValNat.eq_zero_iff : ∀ {p n : ℕ}, padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n
-- Mathlib.Data.Seq.Computation
Computation.liftRelAux_inr_inr : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {C : Computation α → Computation β → Prop} {ca : Computation α}
  {cb : Computation β}, Computation.LiftRelAux R C (Sum.inr ca) (Sum.inr cb) = C ca cb
-- Mathlib.Condensed.Light.Monoidal
LightCondensed.instIsMonoidalFunctorOppositeLightProfiniteModuleCatWCoherentTopology : ∀ (R : Type u) [inst : CommRing R], (CategoryTheory.coherentTopology LightProfinite).W.IsMonoidal
-- Mathlib.Tactic.Module
/-- Evaluate a `Module.NF R M` object `l`, i.e. a list of pairs in `R × M`, to an element of `M`, by
forming the "linear combination" it specifies: scalar-multiply each `R` term to the corresponding
`M` term, then add them all up.  -/
Mathlib.Tactic.Module.NF.eval : {R : Type u_2} → {M : Type u_3} → [Add M] → [Zero M] → [SMul R M] → Mathlib.Tactic.Module.NF R M → M
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s_comp_π_0_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (S : CategoryTheory.SplitEpi f.hom) (n : ℕ) {Z : C} (h : f.left ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.AugmentedCechNerve.ExtraDegeneracy.s f S n)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => f.hom) 0) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => f.hom)
      (CategoryTheory.CategoryStruct.comp S.section_ h)
-- Lean.Server.Completion.CompletionCollectors
/-- Given a type, try to extract relevant type names for dot notation field completion (for `s.f x₁ ... xₙ`).
We extract the type name, parent struct names, and unfold the type.
The process mimics the dot notation elaboration procedure at `App.lean`  -/
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.getDotCompletionTypeNameSet : Lean.Expr → Lean.MetaM Lean.Server.Completion.NameSetModPrivate✝
-- Mathlib.RingTheory.Trace.Quotient
Algebra.trace_quotient_mk : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Free R S]
  [Module.Finite R S] [inst_5 : IsLocalRing R] (x : S),
  (Algebra.trace (R ⧸ IsLocalRing.maximalIdeal R) (S ⧸ Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R)))
      ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) (IsLocalRing.maximalIdeal R))) x) =
    (Ideal.Quotient.mk (IsLocalRing.maximalIdeal R)) ((Algebra.trace R S) x)
-- Mathlib.RingTheory.GradedAlgebra.Homogeneous.Ideal
HomogeneousIdeal.coe_sup : ∀ {ι : Type u_1} {σ : Type u_2} {A : Type u_3} [inst : Semiring A] [inst_1 : DecidableEq ι] [inst_2 : AddMonoid ι]
  [inst_3 : SetLike σ A] [inst_4 : AddSubmonoidClass σ A] {𝒜 : ι → σ} [inst_5 : GradedRing 𝒜]
  (I J : HomogeneousIdeal 𝒜), ↑(I ⊔ J) = ↑I + ↑J
-- Lean.Server.FileSource
Lean.Lsp.FileSource.fileSource : {α : Type} → [self : Lean.Lsp.FileSource α] → α → Lean.Lsp.DocumentUri
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
instIsCyclicUnitsWithZero : ∀ (G : Type u_4) [inst : Group G] [IsCyclic G], IsCyclic (WithZero G)ˣ
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getKeyD_eq_of_contains : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : LawfulBEq α]
  {k fallback : α}, m.contains k = true → m.getKeyD k fallback = k
-- Lean.HeadIndex
/-- Hash code for a `HeadIndex` value.  -/
Lean.HeadIndex.hash : Lean.HeadIndex → UInt64
-- Mathlib.AlgebraicGeometry.IdealSheaf.Functorial
TopologicalSpace.Closeds.preimage.congr_simp : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  (s s_1 : TopologicalSpace.Closeds β),
  s = s_1 → ∀ {f f_1 : α → β} (e_f : f = f_1) (hf : Continuous f), s.preimage hf = s_1.preimage ⋯