mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
DerivedCategory.mem_distTriang_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (T : CategoryTheory.Pretriangulated.Triangle (DerivedCategory C)),
  T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles ↔
    ∃ X Y f, Nonempty (T ≅ DerivedCategory.Q.mapTriangle.obj (CochainComplex.mappingCone.triangle f))
-- Mathlib.Data.NNReal.Defs
NNReal.coe_ne_one : ∀ {r : NNReal}, ↑r ≠ 1 ↔ r ≠ 1
-- Lean.Elab.Import
Lean.Elab.HeaderSyntax : Type
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsClosure
CategoryTheory.ObjectProperty.colimitsClosure.below.of_colimitPresentation : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {α : Type t}
  {J : α → Type u'} [inst_1 : (a : α) → CategoryTheory.Category.{v', u'} (J a)]
  {motive : (a : C) → P.colimitsClosure J a → Prop} {X : C} {a : α}
  (pres : CategoryTheory.Limits.ColimitPresentation (J a) X) (h : ∀ (j : J a), P.colimitsClosure J (pres.diag.obj j)),
  (∀ (j : J a), CategoryTheory.ObjectProperty.colimitsClosure.below ⋯) →
    (∀ (j : J a), motive (pres.diag.obj j) ⋯) → CategoryTheory.ObjectProperty.colimitsClosure.below ⋯
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCompletionItemKind : Lean.ToJson Lean.Lsp.CompletionItemKind
-- Mathlib.Computability.NFA
/-- `M.Path` represents a concrete path through the NFA from a start state to an end state
for a particular word.

Note that due to the non-deterministic nature of the automata, there can be more than one `Path`
for a given word.

Also note that this is `Type` and not a `Prop`, so that we can speak about the properties
of a particular `Path`, such as the set of states visited along the way (defined as `Path.supp`).  -/
NFA.Path : {α : Type u} → {σ : Type v} → NFA α σ → σ → σ → List α → Type (max u v)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey?_ofList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k : α}, (List.map Prod.fst l).contains k = false → (Std.DHashMap.Raw.Const.ofList l).getKey? k = none
-- Mathlib.Data.Nat.Factorization.Basic
Nat.ordProj_self_pow : ∀ {p k : ℕ}, Nat.Prime p → p ^ (p ^ k).factorization p = p ^ k
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight_one : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {ι : Type u_2}, Height.logHeight 1 = 0
-- Mathlib.GroupTheory.GroupAction.FixedPoints
/-- If a set `s : Set α` is in `fixedBy (Set α) g`, then all points of `s` will stay in `s` after being
moved by `g`.
 -/
MulAction.set_mem_fixedBy_iff : ∀ {α : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (s : Set α) (g : G),
  s ∈ MulAction.fixedBy (Set α) g ↔ ∀ (x : α), g • x ∈ s ↔ x ∈ s
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandParsedSnapshot.brecOn_2.eq : ∀ {motive_1 : Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  {motive_2 : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) → Sort u}
  {motive_3 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  {motive_4 : Task Lean.Language.Lean.CommandParsedSnapshot → Sort u}
  (t : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)
  (F_1 : (t : Lean.Language.Lean.CommandParsedSnapshot) → t.below → motive_1 t)
  (F_2 :
    (t : Option (Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot)) →
      Lean.Language.Lean.CommandParsedSnapshot.below_1 t → motive_2 t)
  (F_3 :
    (t : Lean.Language.SnapshotTask Lean.Language.Lean.CommandParsedSnapshot) →
      Lean.Language.Lean.CommandParsedSnapshot.below_2 t → motive_3 t)
  (F_4 :
    (t : Task Lean.Language.Lean.CommandParsedSnapshot) →
      Lean.Language.Lean.CommandParsedSnapshot.below_3 t → motive_4 t),
  Lean.Language.Lean.CommandParsedSnapshot.brecOn_2 t F_1 F_2 F_3 F_4 =
    F_3 t (Lean.Language.Lean.CommandParsedSnapshot.brecOn_2.go t F_1 F_2 F_3 F_4).2
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.map_opShiftFunctorEquivalence_counitIso_hom_app_unop_assoc : ∀ {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] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ] (X : Cᵒᵖ) (n : ℤ)
  {Z : D}
  (h :
    F.obj
        (Opposite.unop
          ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).functor.obj
            ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).inverse.obj X))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (F.map ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence C n).counitIso.hom.app X).unop) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Pretriangulated.opShiftFunctorEquivalence D n).counitIso.hom.app
          (Opposite.op (F.obj (Opposite.unop X)))).unop
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor Dᵒᵖ n).map
            ((CategoryTheory.Functor.commShiftIso F n).inv.app (Opposite.unop X)).op).unop
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Functor.commShiftIso F.op n).hom.app
              (Opposite.op ((CategoryTheory.shiftFunctor C n).obj (Opposite.unop X)))).unop
          h))
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.foldlM_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} {δ : Type w} {m : Type w → Type w'}
  [Std.TransCmp cmp] [inst : Monad m] [LawfulMonad m] {f : δ → α → m δ} {init : δ},
  t₁.Equiv t₂ → Std.TreeSet.foldlM f init t₁ = Std.TreeSet.foldlM f init t₂
-- Mathlib.CategoryTheory.Adjunction.Basic
CategoryTheory.Adjunction.CoreHomEquiv.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (homEquiv : (X : C) → (Y : D) → (F.obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) →
              autoParam
                  (∀ {X' X : C} {Y : D} (f : X' ⟶ X) (g : X ⟶ G.obj Y),
                    (homEquiv X' Y).symm (CategoryTheory.CategoryStruct.comp f g) =
                      CategoryTheory.CategoryStruct.comp (F.map f) ((homEquiv X Y).symm g))
                  CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_left_symm._autoParam →
                autoParam
                    (∀ {X : C} {Y Y' : D} (f : F.obj X ⟶ Y) (g : Y ⟶ Y'),
                      (homEquiv X Y') (CategoryTheory.CategoryStruct.comp f g) =
                        CategoryTheory.CategoryStruct.comp ((homEquiv X Y) f) (G.map g))
                    CategoryTheory.Adjunction.CoreHomEquiv.homEquiv_naturality_right._autoParam →
                  CategoryTheory.Adjunction.CoreHomEquiv F G
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_self_le_mul_self_of_le_of_neg_le : ∀ {R : Type u} [inst : Ring R] [inst_1 : LinearOrder R] {a b : R} [MulPosMono R] [PosMulMono R] [AddLeftMono R],
  a ≤ b → -a ≤ b → a * a ≤ b * b
-- Lean.Elab.BindersUtil
/-- Determines the local declaration kind of a binder using its name.

Names that begin with `__` are implementation details (`.implDetail`).
 -/
Lean.LocalDeclKind.ofBinderName : Lean.Name → Lean.LocalDeclKind
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
/-- The homology of the differentials on a page of the spectral sequence identifies
to the objects on the next page.  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyIso' : {C : Type u_1} →
  {ι : Type u_2} →
    {κ : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Abelian C] →
          [inst_2 : Preorder ι] →
            (X : CategoryTheory.Abelian.SpectralObject C ι) →
              {c : ℤ → ComplexShape κ} →
                {r₀ : ℤ} →
                  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) →
                    (r r' : ℤ) →
                      (hrr' : r + 1 = r') →
                        (hr : r₀ ≤ r) →
                          (pq pq' pq'' : κ) →
                            (c r).prev pq' = pq →
                              (c r).next pq' = pq'' →
                                (i₀' i₀ i₁ i₂ i₃ i₃' : ι) →
                                  i₀' = data.i₀ r' pq' ⋯ →
                                    i₀ = data.i₀ r pq' ⋯ →
                                      i₁ = data.i₁ pq' →
                                        i₂ = data.i₂ pq' →
                                          i₃ = data.i₃ r pq' ⋯ →
                                            i₃' = data.i₃ r' pq' ⋯ →
                                              (n₀ n₁ n₂ : ℤ) →
                                                n₁ = data.deg pq' →
                                                  [X.HasSpectralSequence data] →
                                                    autoParam (n₀ + 1 = n₁)
                                                        CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyIso'._auto_1 →
                                                      autoParam (n₁ + 1 = n₂)
                                                          CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyIso'._auto_3 →
                                                        (((CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X
                                                                  data r hr).sc'
                                                              pq pq' pq'').homology ≅
                                                          (CategoryTheory.Abelian.SpectralObject.SpectralSequence.page X
                                                                data r' ⋯).X
                                                            pq')
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.coe_circle_smul : ∀ (z : Circle) (w : Complex.UnitDisc), ↑(z • w) = ↑z * ↑w
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.SymmetricRelation.toJointlyMono₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X}
  (self : CategoryTheory.SymmetricRelation p₁ p₂), CategoryTheory.JointlyMono₂ p₁ p₂
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instCommMonoid : {M : Type u_1} → [inst : CommMonoid M] → CommMonoid (Associates M)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_of_getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k k' : α}, t.getKey? k = some k' → k' ∈ t
-- Init.Data.Int.DivMod.Lemmas
Int.dvd_self_sub_fmod : ∀ {x m : ℤ}, m ∣ x - x.fmod m
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.derivationQuotKerTotal_apply : ∀ (R : Type u) (S : Type v) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (x : S),
  (KaehlerDifferential.derivationQuotKerTotal R S) x = (KaehlerDifferential.kerTotal R S).mkQ fun₀ | x => 1
-- Mathlib.CategoryTheory.Filtered.Small
CategoryTheory.IsCofiltered.small_fullSubcategory_cofilteredClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.IsCofilteredOrEmpty C] {α : Type w}
  (f : α → C), Small.{max v w, u} (CategoryTheory.IsCofiltered.cofilteredClosure f).FullSubcategory
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.acExt : Lean.Meta.Grind.SolverExtension Lean.Meta.Grind.AC.State
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.mono_ac : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}
  {f : α → β},
  ν.AbsolutelyContinuous μ → MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable f ν
-- Mathlib.NumberTheory.Divisors
Nat.properDivisors_prime_pow : ∀ {p : ℕ} (pp : Nat.Prime p) (k : ℕ),
  (p ^ k).properDivisors = Finset.map { toFun := fun x => p ^ x, inj' := ⋯ } (Finset.range k)
-- Mathlib.Algebra.Module.ZLattice.Basic
ZSpan.ceil_eq_self_of_mem : ∀ {E : Type u_1} {ι : Type u_2} {K : Type u_3} [inst : NormedField K] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace K E] (b : Module.Basis ι K E) [inst_3 : LinearOrder K] [inst_4 : IsStrictOrderedRing K]
  [inst_5 : FloorRing K] [inst_6 : Fintype ι], ∀ m ∈ Submodule.span ℤ (Set.range ⇑b), ↑(ZSpan.ceil b m) = m
-- Mathlib.RingTheory.Etale.Basic
RingHom.FormallyEtale.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
  f.FormallyEtale = Algebra.FormallyEtale R S
-- Mathlib.Data.Real.Basic
Real.instAddLeftCancelSemigroup : AddLeftCancelSemigroup ℝ
-- Mathlib.RingTheory.Localization.Away.Basic
/-- Localizing the localization of `R` at `x` at the image of `y` is the same as localizing
`R` at `y * x`. See `IsLocalization.Away.mul'` for the `x * y` version.  -/
IsLocalization.Away.mul : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (T : Type u_5)
  [inst_3 : CommSemiring T] [inst_4 : Algebra S T] [inst_5 : Algebra R T] [IsScalarTower R S T] (x y : R)
  [IsLocalization.Away x S] [IsLocalization.Away ((algebraMap R S) y) T], IsLocalization.Away (y * x) T
-- Mathlib.Geometry.Euclidean.Altitude
/-- The direction of an altitude.  -/
Affine.Simplex.direction_altitude : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) (i : Fin (n + 1)),
  (s.altitude i).direction = (vectorSpan ℝ (s.points '' {i}ᶜ))ᗮ ⊓ vectorSpan ℝ (Set.range s.points)
-- Mathlib.CategoryTheory.Monad.Adjunction
/-- Given an adjunction `L ⊣ R`, if `L ⋙ R` is isomorphic to the identity functor, then `L` is
fully faithful.
 -/
CategoryTheory.Adjunction.fullyFaithfulLOfCompIsoId : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {L : CategoryTheory.Functor C D} →
          {R : CategoryTheory.Functor D C} → (L ⊣ R) → (L.comp R ≅ CategoryTheory.Functor.id C) → L.FullyFaithful
-- Mathlib.Data.Finset.Lattice.Fold
Finset.isGLB_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : OrderTop α] {s : Finset β} {f : β → α},
  IsGLB (f '' ↑s) (s.inf f)
-- Init.Data.UInt.Lemmas
USize.toUInt8_toUInt16 : ∀ (n : USize), n.toUInt16.toUInt8 = n.toUInt8
-- Mathlib.Topology.Algebra.Constructions
/-- An auxiliary lemma that can be used to prove that coercion `Mˣ → M` is a topological embedding.
Use `Units.isEmbedding_val₀`, `Units.isEmbedding_val`, or `toUnits_homeomorph` instead.  -/
Units.isEmbedding_val_mk' : ∀ {M : Type u_4} [inst : Monoid M] [inst_1 : TopologicalSpace M] {f : M → M},
  ContinuousOn f {x | IsUnit x} → (∀ (u : Mˣ), f ↑u = ↑u⁻¹) → Topology.IsEmbedding Units.val
-- Init.Data.UInt.Lemmas
Nat.toUInt8_eq : ∀ {n : ℕ}, n.toUInt8 = UInt8.ofNat n
-- Mathlib.Analysis.Calculus.FDeriv.Add
differentiable_neg_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},
  Differentiable 𝕜 (-f) ↔ Differentiable 𝕜 f
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.homotopyCofiber.desc_f' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} {F G K : HomologicalComplex C c} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ]
  [inst_3 : DecidableRel c.Rel] (α : G ⟶ K) (hα : Homotopy (CategoryTheory.CategoryStruct.comp φ α) 0) (j : ι),
  ¬c.Rel j (c.next j) →
    (HomologicalComplex.homotopyCofiber.desc φ α hα).f j =
      CategoryTheory.CategoryStruct.comp (HomologicalComplex.homotopyCofiber.sndX φ j) (α.f j)
-- Mathlib.Order.Filter.Cofinite
/-- If `l ≥ Filter.cofinite` is a countably generated filter, then `l.ker` is cocountable.  -/
Filter.countable_compl_ker : ∀ {α : Type u_2} {l : Filter α} [l.IsCountablyGenerated], Filter.cofinite ≤ l → l.kerᶜ.Countable
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_of_mem_insertMany_list : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k : α}, k ∈ m.insertMany l → (List.map Prod.fst l).contains k = false → k ∈ m
-- Lean.Expr
Lean.Expr.app.inj : ∀ {fn arg fn_1 arg_1 : Lean.Expr}, fn.app arg = fn_1.app arg_1 → fn = fn_1 ∧ arg = arg_1
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.linear_toAffineMap : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (e : P₁ ≃ᵃ[k] P₂), (↑e).linear = ↑e.linear
-- Mathlib.Probability.Kernel.Composition.Comp
ProbabilityTheory.Kernel.comp_id : ∀ {β : Type u_2} {γ : Type u_3} {mβ : MeasurableSpace β} {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel β γ),
  κ.comp ProbabilityTheory.Kernel.id = κ
-- Mathlib.Topology.Order.IsLUB
IsGLB.exists_seq_strictAnti_tendsto_of_notMem : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {t : Set α} {x : α}
  [(nhds x).IsCountablyGenerated],
  IsGLB t x →
    x ∉ t →
      t.Nonempty →
        ∃ u, StrictAnti u ∧ (∀ (n : ℕ), x < u n) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t
-- Mathlib.GroupTheory.GroupAction.Basic
MulAction.stabilizerEquivStabilizer_trans : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] {g h k : G} {a b c : α} (hg : b = g • a)
  (hh : c = h • b) (hk : c = k • a),
  k = h * g →
    (MulAction.stabilizerEquivStabilizer hg).trans (MulAction.stabilizerEquivStabilizer hh) =
      MulAction.stabilizerEquivStabilizer hk
-- Mathlib.Topology.Semicontinuity.Defs
UpperHemicontinuous.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace γ]
  [inst_2 : TopologicalSpace β] {f : α → Set β} {g : γ → α},
  UpperHemicontinuous f → Continuous g → UpperHemicontinuous (f ∘ g)
-- Mathlib.Data.List.Sort
List.sortedLT_iff_strictMono_get : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], l.SortedLT ↔ StrictMono l.get
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.map_comp_residue : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] (f : R →+* S) [inst_4 : IsLocalHom f],
  (IsLocalRing.ResidueField.map f).comp (IsLocalRing.residue R) = (IsLocalRing.residue S).comp f
-- Mathlib.Data.Subtype
Subtype.coe_injective : ∀ {α : Sort u_1} {p : α → Prop}, Function.Injective fun a => ↑a
-- Init.Core
Std.RightIdentity.mk : ∀ {α : Sort u} {β : Sort u_1} {op : α → β → α} {o : outParam β}, Std.RightIdentity op o
-- Batteries.Data.List.Lemmas
List.diff_erase : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] (l₁ l₂ : List α) (a : α), (l₁.diff l₂).erase a = (l₁.erase a).diff l₂
-- Mathlib.Order.Antisymmetrization
/-- Get a representative from the antisymmetrization.  -/
ofAntisymmetrization : {α : Type u_1} → (r : α → α → Prop) → [inst : IsPreorder α r] → Antisymmetrization α r → α
-- Mathlib.MeasureTheory.Measure.MeasureSpace
AEMeasurable.nullMeasurable : ∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {f : α → β}, AEMeasurable f μ → MeasureTheory.NullMeasurable f μ
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.ext_norm_arg_iff : ∀ {x y : ℂ}, x = y ↔ ‖x‖ = ‖y‖ ∧ x.arg = y.arg
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.AreEqualizedByLocalization.mk : ∀ {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] (W : CategoryTheory.MorphismProperty C) {X Y : C} (f g : X ⟶ Y)
  (L : CategoryTheory.Functor C D) [L.IsLocalization W],
  L.map f = L.map g → CategoryTheory.AreEqualizedByLocalization W f g
-- Mathlib.NumberTheory.Height.MvPolynomial
_private.Mathlib.NumberTheory.Height.MvPolynomial.0.Height.mulHeight_eval_ge_aux : ∀ {K : Type u_6} [inst : Field K] {ι : Type u_7} {ι' : Type u_8} [inst_1 : Fintype ι'] {M N : ℕ}
  {q : ι × ι' → MvPolynomial ι K} [IsEmpty ι'] (p : ι' → MvPolynomial ι K) {x : ι → K},
  (∀ (k : ι), ∑ j, (MvPolynomial.eval x) (q (k, j)) * (MvPolynomial.eval x) (p j) = x k ^ (M + N)) → x = 0
-- Mathlib.Topology.LocallyFinsupp
Function.locallyFinsuppWithin.instAddGroup : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : AddGroup Y] → AddGroup (Function.locallyFinsuppWithin U Y)
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Multipliable.tprod_comm' : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] [ContinuousMul α]
  [T3Space α] {f : β → γ → α},
  Multipliable (Function.uncurry f) →
    (∀ (b : β), Multipliable (f b)) →
      (∀ (c : γ), Multipliable fun b => f b c) → ∏' (c : γ) (b : β), f b c = ∏' (b : β) (c : γ), f b c
-- Mathlib.Order.WithBot
WithBot.decidableEq.eq_1 : ∀ {α : Type u_1} [inst : DecidableEq α], WithBot.decidableEq = WithBot.decidableEq._aux_1
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.coe_fst : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {x : Z}, x ∈ e.source → (↑e x).1 = proj x
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.IsUnramified.isUnmixed : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K]
  {w : NumberField.InfinitePlace K},
  NumberField.InfinitePlace.IsUnramified k w → NumberField.ComplexEmbedding.IsUnmixed k w.embedding
-- Lean.ToExpr
Lean.instToExprInt16 : Lean.ToExpr Int16
-- Mathlib.CategoryTheory.EquivalenceRelation
CategoryTheory.IsEquivalenceRelation.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {R X : C} {p₁ p₂ : R ⟶ X},
  Nonempty (CategoryTheory.EquivalenceRelation p₁ p₂) → CategoryTheory.IsEquivalenceRelation p₁ p₂
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_refl : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] (f : α → E) (l : Filter α), Asymptotics.IsBigOWith 1 l f f
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instFromJsonDiagnosticRelatedInformation.fromJson : Lean.Json → Except String Lean.Lsp.DiagnosticRelatedInformation
-- Mathlib.CategoryTheory.Category.Cat.Terminal
/-- Any terminal object `T : Cat.{u, u}` is isomorphic to `Cat.of (Discrete PUnit)`.  -/
CategoryTheory.Cat.isoDiscretePUnitOfIsTerminal : {T : Type u} →
  [inst : CategoryTheory.Category.{u, u} T] →
    CategoryTheory.Limits.IsTerminal (CategoryTheory.Cat.of T) →
      (CategoryTheory.Cat.of T ≅ CategoryTheory.Cat.of (CategoryTheory.Discrete PUnit.{u + 1}))
-- Mathlib.Data.EReal.Operations
EReal.toENNReal_add_le : ∀ {x y : EReal}, (x + y).toENNReal ≤ x.toENNReal + y.toENNReal
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonempty
/-- If a simplicial set is not nonempty, it is an initial object.  -/
SSet.isInitialOfNotNonempty : {X : SSet} → ¬X.Nonempty → CategoryTheory.Limits.IsInitial X
-- Mathlib.Logic.Equiv.Basic
/-- Convert an involutive function `f` to a permutation with `toFun = invFun = f`.  -/
Function.Involutive.toPerm : {α : Sort u_1} → (f : α → α) → Function.Involutive f → Equiv.Perm α
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.mem_valueMonoid_iff : ∀ {A : Type u_1} {B : Type u_2} [inst : MonoidWithZero A] [inst_1 : MonoidWithZero B] (f : A →*₀ B) {b : Bˣ},
  b ∈ f.valueMonoid ↔ b ∈ Units.val ⁻¹' Set.range ⇑f
-- Lean.Elab.Do.InferControlInfo
Lean.Elab.Do.instToMessageDataControlInfo : Lean.ToMessageData Lean.Elab.Do.ControlInfo
-- Lean.Data.JsonRpc
Lean.JsonRpc.MessageDirection.clientToServer.sizeOf_spec : sizeOf Lean.JsonRpc.MessageDirection.clientToServer = 1