mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.CompleteField
LinearOrderedField.cutMap_bddAbove : ∀ {α : Type u_2} (β : Type u_3) [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : LinearOrder β] [IsStrictOrderedRing β] [Archimedean α] (a : α), BddAbove (LinearOrderedField.cutMap β a)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringLeft₃_obj_obj_obj_obj_obj_obj_map : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {D₁ : Type u_4} {D₂ : Type u_5} {D₃ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} D₁]
  [inst_4 : CategoryTheory.Category.{v_5, u_5} D₂] [inst_5 : CategoryTheory.Category.{v_6, u_6} D₃] (E : Type u_7)
  [inst_6 : CategoryTheory.Category.{v_7, u_7} E] (F₁ : CategoryTheory.Functor C₁ D₁)
  (F₂ : CategoryTheory.Functor C₂ D₂) (F₃ : CategoryTheory.Functor C₃ D₃)
  (X : CategoryTheory.Functor D₁ (CategoryTheory.Functor D₂ (CategoryTheory.Functor D₃ E))) (X_1 : C₁) (X_2 : C₂)
  {X_3 Y : C₃} (f : X_3 ⟶ Y),
  (((((((CategoryTheory.Functor.whiskeringLeft₃ E).obj F₁).obj F₂).obj F₃).obj X).obj X_1).obj X_2).map f =
    ((X.obj (F₁.obj X_1)).obj (F₂.obj X_2)).map (F₃.map f)
-- Mathlib.Algebra.Homology.HomologicalComplexBiprod
HomologicalComplex.instHasBinaryBiproduct : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {c : ComplexShape ι} (K L : HomologicalComplex C c)
  [∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (L.X i)], CategoryTheory.Limits.HasBinaryBiproduct K L
-- Mathlib.Order.Comparable
compRel_swap : ∀ {α : Type u_1} (r : α → α → Prop), CompRel (Function.swap r) = CompRel r
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.instCoeOutSieve : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} → {J : CategoryTheory.GrothendieckTopology C} → CoeOut (J.Cover X) (CategoryTheory.Sieve X)
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.sum_chartAt_inr : ∀ {H : Type u} {M : Type u_2} {M' : Type u_3} [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace M'] [cm : ChartedSpace H M] [cm' : ChartedSpace H M'] (x' : M'),
  chartAt H (Sum.inr x') = (chartAt H x').lift_openEmbedding ⋯
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Metric
measurableSet_eball : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α] {x : α}
  {ε : ENNReal}, MeasurableSet (Metric.eball x ε)
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `locallyLipschitz_inv_iff`. -/
LocallyLipschitz.of_inv : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {f : α → E},
  LocallyLipschitz f⁻¹ → LocallyLipschitz f
-- Mathlib.CategoryTheory.Widesubcategory
CategoryTheory.WideSubcategory.category : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (P : CategoryTheory.MorphismProperty C) →
      [inst_1 : P.IsMultiplicative] → CategoryTheory.Category.{v₁, u₁} (CategoryTheory.WideSubcategory P)
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Counting
_private.Mathlib.Combinatorics.SimpleGraph.Triangle.Counting.0.SimpleGraph.card_interedges_badVertices_le : ∀ {α : Type u_1} (G : SimpleGraph α) [inst : DecidableRel G.Adj] {ε : ℝ} {s t : Finset α},
  ↑(Rel.interedges G.Adj (SimpleGraph.badVertices✝ G ε s t) t).card ≤
    ↑(SimpleGraph.badVertices✝ G ε s t).card * ↑t.card * (↑(G.edgeDensity s t) - ε)
-- Mathlib.Algebra.Algebra.Hom.Rat
AlgHom.toRingHom_toRatAlgHom : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] [inst_2 : Algebra ℚ R] [inst_3 : Algebra ℚ S]
  (f : R →ₐ[ℚ] S), (↑f).toRatAlgHom = f
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.instCommMonoidWithZero : {α : Type u_1} → [CommMonoid α] → CommMonoidWithZero (WithZero α)
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.leftHomologyπNatTrans_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasKernels C] [inst_3 : CategoryTheory.Limits.HasCokernels C]
  (S : CategoryTheory.ShortComplex C), (CategoryTheory.ShortComplex.leftHomologyπNatTrans C).app S = S.leftHomologyπ
-- Init.Data.SInt.Lemmas
Int64.ofBitVec_le_iff_sle : ∀ (a b : BitVec 64), Int64.ofBitVec a ≤ Int64.ofBitVec b ↔ a.sle b = true
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.invVeblen₂_epsilon : ∀ {o : Ordinal.{u}}, o < o.epsilon → o.epsilon.invVeblen₂ = o
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatIso.unop_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ},
  CategoryTheory.NatIso.unop F.leftUnitor =
    F.unop.leftUnitor.symm ≪≫
      CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.unopId C).symm F.unop ≪≫
        ((CategoryTheory.Functor.id Cᵒᵖ).unopComp F).symm
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.funLike : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid A] →
          [inst_2 : Module R A] →
            [inst_3 : AddCommMonoid B] →
              [inst_4 : Module R B] →
                [inst_5 : CoalgebraStruct R A] → [inst_6 : CoalgebraStruct R B] → FunLike (A →ₗc[R] B) A B
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
/-- The valuation less-than relation, defined as `x <ᵥ y ↔ ¬ y ≤ᵥ x`.  -/
ValuativeRel.«term_<ᵥ_» : Lean.TrailingParserDescr
-- Mathlib.Geometry.Manifold.Sheaf.LocallyRingedSpace
/-- Viewing a manifold as a locally ringed space commutes with restriction to open subsets.  -/
ChartedSpace.restrictLocallyRingedSpaceIso : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {EM : Type u_1} →
      [inst_1 : NormedAddCommGroup EM] →
        [inst_2 : NormedSpace 𝕜 EM] →
          {HM : Type u_2} →
            [inst_3 : TopologicalSpace HM] →
              {IM : ModelWithCorners 𝕜 EM HM} →
                {M : Type u} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace HM M] →
                      (U : TopologicalSpace.Opens M) →
                        (ChartedSpace.locallyRingedSpace IM M).restrict ⋯ ≅ ChartedSpace.locallyRingedSpace IM ↥U
-- Mathlib.Data.Matrix.Diagonal
Matrix.instAddCommGroupWithOne : {n : Type u_3} → {α : Type v} → [DecidableEq n] → [AddCommGroupWithOne α] → AddCommGroupWithOne (Matrix n n α)
-- Mathlib.CategoryTheory.EffectiveEpi.Enough
/-- The morphism `F.obj p ⟶ X`  -/
CategoryTheory.Functor.EffectivePresentation.f : {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] →
        {F : CategoryTheory.Functor C D} → {X : D} → (self : F.EffectivePresentation X) → F.obj self.p ⟶ X
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.IsUnmixed.isReal_iff_isReal : ∀ (K : Type u_3) {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] {φ : L →+* ℂ},
  NumberField.ComplexEmbedding.IsUnmixed K φ →
    (NumberField.ComplexEmbedding.IsReal (φ.comp (algebraMap K L)) ↔ NumberField.ComplexEmbedding.IsReal φ)
-- Mathlib.Analysis.Calculus.FDeriv.Const
fderiv_one : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : One F], fderiv 𝕜 1 = 0
-- Mathlib.CategoryTheory.Subobject.Types
Types.monoOverEquivalenceSet_inverse_map : ∀ (α : Type u) {s t : Set α} (b : s ⟶ t),
  (Types.monoOverEquivalenceSet α).inverse.map b = CategoryTheory.MonoOver.homMk (TypeCat.ofHom fun w => ⟨↑w, ⋯⟩) ⋯
-- Mathlib.Tactic.Convert
/-- `ac_change t` on a goal `⊢ t'` changes the goal to `⊢ t` and adds new goals for proving the equality
`t' = t` using congruence, then tries proving these goals by associativity and commutativity. The
goals are created like `congr!` would.
In other words, `ac_change t` is like `convert_to t` followed by `ac_refl`.

Like `refine e`, any holes (`?_` or `?x`) in `t` that are not solved by unification are converted
into new goals, using the hole's name, if any, as the goal case name.
Like `congr!`, `convert_to` introduces variables while applying congruence rules. These can be
pattern-matched, like `rintro` would, using the `with` keyword.

* `ac_change! t` uses default transparency, rather than reducible, when solving side goals.
* `ac_change t using n`, where `n` is a positive numeral, controls the depth with which congruence
  is applied. For example, if the main goal is `⊢ Prime ((a * b + 1) + c)`,
  then `ac_change Prime ((1 + a * b) + c) using 2` solves the side goals, and
  `ac_change Prime ((1 + a * b) + c) using 3` (or more) results in two (impossible) goals
  `⊢ 1 = a * b` and `⊢ a * b = 1`.
  The default value for `n` is 1.

Example:
```lean
example (a b c d e f g N : ℕ) : (a + b) + (c + d) + (e + f) + g ≤ N := by
  ac_change a + d + e + f + c + g + b ≤ _
  -- ⊢ a + d + e + f + c + g + b ≤ N
```
 -/
Mathlib.Tactic.acChange : Lean.ParserDescr
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.instOverClass : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → {X : C} → CategoryTheory.OverClass X X
-- Mathlib.Topology.MetricSpace.Holder
HolderWith.holderOnWith : ∀ {X : Type u_1} {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] {C r : NNReal}
  {f : X → Y}, HolderWith C r f → ∀ (s : Set X), HolderOnWith C r f s
-- Mathlib.Data.ZMod.Basic
ZMod.val_mul' : ∀ {m n : ZMod 0}, (m * n).val = m.val * n.val
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.lift.eq_1 : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} {φ : ↥A ≃* ↥B} {H : Type u_2} [inst_1 : Group H] (f : G →* H)
  (x : H) (hx : ∀ (a : ↥A), x * f ↑a = f ↑(φ a) * x),
  HNNExtension.lift f x hx = (HNNExtension.con G A B φ).lift (Monoid.Coprod.lift f ((zpowersHom H) x)) ⋯
-- Mathlib.LinearAlgebra.FreeModule.PID
Submodule.basisOfPid_bot : ∀ {R : Type u_2} [inst : CommRing R] {M : Type u_3} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : IsPrincipalIdealRing R] [inst_4 : IsDomain R] {ι : Type u_4} [inst_5 : Finite ι] (b : Module.Basis ι R M),
  Submodule.basisOfPid b ⊥ = ⟨0, Module.Basis.empty ↥⊥⟩
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGT?_eq_map : ∀ {α : Type u} {β : Type v} [inst : Ord α] {t : Std.DTreeMap.Internal.Impl α fun x => β} {k : α},
  Std.DTreeMap.Internal.Impl.Const.getEntryGT? k t =
    Option.map (fun x => (x.fst, x.snd)) (Std.DTreeMap.Internal.Impl.getEntryGT? k t)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
CategoryTheory.Functor.biprodComparison_fst_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor C D) (X Y : C) [inst_4 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)] {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.biprodComparison X Y)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.biprod.fst) h
-- Mathlib.Algebra.Order.Group.Opposite
MulOpposite.op_le_op : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, MulOpposite.op a ≤ MulOpposite.op b ↔ a ≤ b
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.isUniformInducing_toCompletion : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R),
  IsUniformInducing IsDedekindDomain.HeightOneSpectrum.adicCompletion.toCompletion
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.instSMulCommClassElemRootSet : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommRing S] [inst_3 : Algebra S R]
  (G : Type u_1) (H : Type u_2) [inst_4 : Monoid G] [inst_5 : MulSemiringAction G R] [inst_6 : SMulCommClass G S R]
  [inst_7 : Monoid H] [inst_8 : MulSemiringAction H R] [inst_9 : SMulCommClass H S R] [SMulCommClass G H R]
  (f : Polynomial S), SMulCommClass G H ↑(f.rootSet R)
-- Aesop.Saturate
Aesop.SaturateM.Context.mk.injEq : ∀ (options options_1 : Aesop.Options'), ({ options := options } = { options := options_1 }) = (options = options_1)
-- Mathlib.Data.List.Cycle
Cycle.forall_eq_of_chain : ∀ {α : Type u_1} {r : α → α → Prop} {s : Cycle α} [IsTrans α r] [Std.Antisymm r],
  Cycle.Chain r s → ∀ {a b : α}, a ∈ s → b ∈ s → a = b
-- Init.Data.Array.Lemmas
Array.foldr.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → β → β) (init : β) (as : Array α) (start stop : ℕ),
  Array.foldr f init as start stop = (Array.foldrM (fun x1 x2 => pure (f x1 x2)) init as start stop).run
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.AffineCover.cover_X : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.AffineCover P X) (j : 𝒰.I₀), 𝒰.cover.X j = AlgebraicGeometry.Spec (𝒰.X j)
-- Init.Data.List.Sort.Impl
List.MergeSort.Internal.mergeSort_eq_mergeSortTR : @List.mergeSort = @List.MergeSort.Internal.mergeSortTR
-- Init.Data.Nat.Lemmas
Nat.mul_mod_mod : ∀ (m n l : ℕ), m * (n % l) % l = m * n % l
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.separatingLeft_iff_det_ne_zero : ∀ {R : Type u_1} {M₁ : Type u_6} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [IsDomain R] [inst_4 : AddCommMonoid M₁] [inst_5 : Module R M₁] (b : Module.Basis m R M₁) {B : M₁ →ₗ[R] M₁ →ₗ[R] R},
  B.SeparatingLeft ↔ ((LinearMap.toMatrix₂ b b) B).det ≠ 0
-- Init.SimpLemmas
instLawfulIdentityBoolOrFalse : Std.LawfulIdentity (fun x1 x2 => x1 || x2) false
-- Mathlib.Analysis.Normed.Operator.Extend
LinearEquiv.extendOfIsometry_symm_apply : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6} [inst : NormedField 𝕜]
  [inst_1 : NormedField 𝕜₂] [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : Module 𝕜₂ F] [inst_6 : NormedAddCommGroup Eₗ] [inst_7 : NormedSpace 𝕜 Eₗ] [inst_8 : CompleteSpace Eₗ]
  [inst_9 : NormedAddCommGroup Fₗ] [inst_10 : NormedSpace 𝕜₂ Fₗ] [inst_11 : CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_12 : RingHomInvPair σ₁₂ σ₂₁] [inst_13 : RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F)
  (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (h_dense₁ : DenseRange ⇑e₁) (h_dense₂ : DenseRange ⇑e₂)
  (h_norm : ∀ (x : E), ‖e₂ (f x)‖ = ‖e₁ x‖) (x : Fₗ),
  (f.extendOfIsometry e₁ e₂ h_dense₁ h_dense₂ h_norm).symm x = ((e₁ ∘ₛₗ ↑f.symm).extendOfNorm e₂) x
-- Mathlib.Analysis.Convex.Function
ConcaveOn.left_le_of_le_right'' : ∀ {𝕜 : Type u_1} {β : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommMonoid β] [inst_4 : LinearOrder β] [IsOrderedCancelAddMonoid β] [inst_6 : Module 𝕜 β]
  [PosSMulStrictMono 𝕜 β] {x y z : 𝕜} {s : Set 𝕜} {f : 𝕜 → β},
  ConcaveOn 𝕜 s f → x ∈ s → z ∈ s → x ≤ y → y < z → f y ≤ f z → f x ≤ f y
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.comp_id : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] (f : M₁ →SL[σ₁₂] M₂),
  f ∘SL ContinuousLinearMap.id R₁ M₁ = f
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsSeparating.of_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  P.IsSeparating → ∀ {Q : CategoryTheory.ObjectProperty C}, P ≤ Q → Q.IsSeparating
-- Mathlib.AlgebraicGeometry.Morphisms.Preimmersion
AlgebraicGeometry.IsPreimmersion.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [toSurjectiveOnStalks : AlgebraicGeometry.SurjectiveOnStalks f],
  Topology.IsEmbedding ⇑f → AlgebraicGeometry.IsPreimmersion f
-- Mathlib.Order.Category.BddDistLat
_private.Mathlib.Order.Category.BddDistLat.0.BddDistLat.Hom.mk.injEq : ∀ {X Y : BddDistLat} (hom' hom'_1 : BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_eval_cast : ∀ (S : Type u) [inst : Semiring S] (n k : ℕ),
  ↑(Polynomial.eval k (ascPochhammer ℕ n)) = Polynomial.eval (↑k) (ascPochhammer S n)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.getLast?.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Lean.Meta.Sorry
Lean.Meta.SorryLabelView : Type
-- Mathlib.Order.Concept
subset_upperPolar_lowerPolar : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (t : Set β), t ⊆ upperPolar r (lowerPolar r t)
-- Batteries.Data.Fin.Lemmas
Fin.findSomeRev?_rev : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, (Fin.findSomeRev? fun x => f x.rev) = Fin.findSome? f
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianPDFReal_add : ∀ {μ : ℝ} {v : NNReal} (x y : ℝ),
  ProbabilityTheory.gaussianPDFReal μ v (x + y) = ProbabilityTheory.gaussianPDFReal (μ - y) v x
-- Init.Data.ToString.Basic
instToStringPUnit : ToString PUnit.{u + 1}
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.IsClosedImmersion.Spec_iff : ∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCat} {f : X ⟶ AlgebraicGeometry.Spec R},
  AlgebraicGeometry.IsClosedImmersion f ↔
    ∃ I e,
      f =
        CategoryTheory.CategoryStruct.comp e.hom (AlgebraicGeometry.Spec.map (CommRingCat.ofHom (Ideal.Quotient.mk I)))
-- Mathlib.Algebra.Torsor.Basic
Prod.snd_sdiv : ∀ {G : Type u_1} {G' : Type u_2} {P : Type u_3} {P' : Type u_4} [inst : Group G] [inst_1 : Group G']
  [inst_2 : Torsor G P] [inst_3 : Torsor G' P'] (p₁ p₂ : P × P'), (p₁ /ₛ p₂).2 = p₁.2 /ₛ p₂.2
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {P : CategoryTheory.ProjectiveResolution Y} {Q : CategoryTheory.ProjectiveResolution Z}
  (f f_1 : P.complex ⟶ Q.complex) (e_f : f = f_1) (comm : CategoryTheory.CategoryStruct.comp f Q.π = 0),
  CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne f comm =
    CategoryTheory.ProjectiveResolution.liftHomotopyZeroOne f_1 ⋯
-- Mathlib.Data.Matrix.Block
/-- `Matrix.blockDiag'` as an `AddMonoidHom`.  -/
Matrix.blockDiag'AddMonoidHom : {o : Type u_4} →
  (m' : o → Type u_7) →
    (n' : o → Type u_8) →
      (α : Type u_12) →
        [inst : AddZeroClass α] → Matrix ((i : o) × m' i) ((i : o) × n' i) α →+ (i : o) → Matrix (m' i) (n' i) α
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.mk' : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] (i : α → β),
  Continuous i →
    (∀ (x : β), x ∈ closure (Set.range i)) →
      (∀ (a : α), ∀ s ∈ nhds a, ∃ t ∈ nhds (i a), ∀ (b : α), i b ∈ t → b ∈ s) → IsDenseInducing i
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C_zero : ∀ (R : Type u_1) [inst : CommRing R], Polynomial.Chebyshev.C R 0 = 2
-- Mathlib.Computability.TuringMachine.StackTuringMachine
_private.Mathlib.Computability.TuringMachine.StackTuringMachine.0.Option.isSome.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → ((val : α) → motive (some val)) → (Unit → motive none) → motive x
-- Mathlib.Analysis.Convex.Quasiconvex
QuasilinearOn.eq_1 : ∀ (𝕜 : Type u_1) {E : Type u_2} {β : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : LE β] [inst_4 : SMul 𝕜 E] (s : Set E) (f : E → β),
  QuasilinearOn 𝕜 s f = (QuasiconvexOn 𝕜 s f ∧ QuasiconcaveOn 𝕜 s f)
-- Lean.Elab.MutualInductive
Lean.Elab.Command.InductiveView.ctors : Lean.Elab.Command.InductiveView → Array Lean.Elab.Command.CtorView
-- Init.Data.SInt.Lemmas
ISize.sub_nonneg_of_le : ∀ {a b : ISize}, 0 ≤ b → b ≤ a → 0 ≤ a - b
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
/-- The embedding `K →+* ℝ` associated to a real infinite place extended to `v.Completion →+* ℝ`.  -/
NumberField.InfinitePlace.Completion.extensionEmbeddingOfIsReal : {K : Type u_1} → [inst : Field K] → {v : NumberField.InfinitePlace K} → v.IsReal → v.Completion →+* ℝ
-- Mathlib.Algebra.Algebra.Hom
/-- Turn an algebra homomorphism into the corresponding multiplicative monoid homomorphism.  -/
AlgHom.toMonoidHom' : {R : Type u} →
  {A : Type v} →
    {B : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] → [inst_3 : Algebra R A] → [inst_4 : Algebra R B] → (A →ₐ[R] B) → A →* B
-- Mathlib.Combinatorics.Matroid.Map
/-- The pullback of a matroid on `β` by a function `f : α → β` to a matroid on `α`,
restricted to a ground set `E`.
The matroids `M.comapOn f E` and `M ↾ (f '' E)` have isomorphic simplifications;
elements with the same nonloop image are parallel.  -/
Matroid.comapOn : {α : Type u_1} → {β : Type u_2} → Matroid β → Set α → (α → β) → Matroid α
-- Lean.Server.Requests
Lean.Server.RequestHandler.handle : Lean.Server.RequestHandler →
  Lean.Json → Lean.Server.RequestM (Lean.Server.RequestTask Lean.Server.SerializedLspResponse)
-- Mathlib.Order.Height
Set.chainHeight_le_encard : ∀ {α : Type u_1} (s : Set α) (r : α → α → Prop), s.chainHeight r ≤ s.encard
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.toList_of_mul : ∀ {α : Type u_1} (x : α) (xs : FreeMonoid α), FreeMonoid.toList (FreeMonoid.of x * xs) = x :: FreeMonoid.toList xs
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.coequalizer_as_cokernel : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) [inst_2 : CategoryTheory.Limits.HasCokernel f],
  CategoryTheory.Limits.coequalizer.π f 0 = CategoryTheory.Limits.cokernel.π f
-- Mathlib.RepresentationTheory.Homological.FiniteCyclic
/-- Given a finite group `G` and `g : G`, this is the functor `Rep k G ⥤ ChainComplex (Rep k G) ℕ`
sending `A : Rep k G` to the periodic chain complex in `Rep k G` given by
`... ⟶ A --N--> A --(ρ(g) - 𝟙)--> A --N--> A --(ρ(g) - 𝟙)--> A ⟶ 0`
where `N` is the norm map. When `G` is generated by `g` and `A` is the left regular representation
`k[G]`, it is a projective resolution of `k` as a trivial representation.

It sends a morphism `f : A ⟶ B` to the chain morphism defined by `f` in every degree.  -/
Rep.FiniteCyclicGroup.chainComplexFunctor : (k : Type u) →
  {G : Type u} →
    [inst : CommRing k] →
      [inst_1 : CommGroup G] →
        [Fintype G] → G → CategoryTheory.Functor (Rep.{u_1, u, u} k G) (ChainComplex (Rep.{u_1, u, u} k G) ℕ)
-- Mathlib.SetTheory.ZFC.Class
Class.instWellFoundedRelation : WellFoundedRelation Class.{u_1}
-- Lean.Expr
/-- Default binder annotation, e.g. `(x : α)`  -/
Lean.BinderInfo.default : Lean.BinderInfo
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.sub_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_5} [inst : Sub A] (M N : CStarMatrix m n A) (i : m) (j : n),
  (M - N) i j = M i j - N i j
-- Mathlib.Order.BooleanAlgebra.Set
Set.compl_ne_eq_singleton : ∀ {α : Type u_1} (a : α), {x | x ≠ a}ᶜ = {a}
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.primitiveRootsPowEquiv_apply_coe : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {a b n : ℕ} (h : a * b ≡ 1 [MOD n])
  (x : ↥(primitiveRoots n R)), ↑((IsPrimitiveRoot.primitiveRootsPowEquiv h) x) = ↑x ^ a