mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.LocalInvariantProp.liftProp_of_locally_liftPropOn : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {G : StructureGroupoid H} {G' : StructureGroupoid H'}
  {P : (H → H') → Set H → H → Prop} {g : M → M'},
  G.LocalInvariantProp G' P →
    (∀ (x : M), ∃ u, IsOpen u ∧ x ∈ u ∧ ChartedSpace.LiftPropOn P g u) → ChartedSpace.LiftProp P g
-- Mathlib.Algebra.Category.ModuleCat.Kernels
/-- The kernel cone induced by the concrete kernel.  -/
ModuleCat.kernelCone : {R : Type u} → [inst : Ring R] → {M N : ModuleCat R} → (f : M ⟶ N) → CategoryTheory.Limits.KernelFork f
-- Mathlib.Order.Hom.Basic
OrderIso.le_symm_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {x : α} {y : β}, x ≤ e.symm y ↔ e x ≤ y
-- Mathlib.Data.Finset.Lattice.Fold
map_finset_sup : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} {ι : Type u_5} [inst : SemilatticeSup α] [inst_1 : OrderBot α]
  [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β] [inst_4 : FunLike F α β] [SupBotHomClass F α β] (f : F)
  (s : Finset ι) (g : ι → α), f (s.sup g) = s.sup (⇑f ∘ g)
-- Mathlib.RingTheory.WittVector.Basic
/-- The commutative ring structure on `𝕎 R`.  -/
WittVector.instCommRing : (p : ℕ) → (R : Type u_1) → [CommRing R] → [Fact (Nat.Prime p)] → CommRing (WittVector p R)
-- Mathlib.Topology.Maps.Basic
Topology.IsEmbedding.closure_eq_preimage_closure_image : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  Topology.IsEmbedding f → ∀ (s : Set X), closure s = f ⁻¹' closure (f '' s)
-- Mathlib.CategoryTheory.Bicategory.EqToHom
CategoryTheory.Bicategory.associator_eqToHom_hom : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {x y z t : B} (e₁ : x = y) (e₂ : y = z) (e₃ : z = t),
  (CategoryTheory.Bicategory.associator (CategoryTheory.eqToHom e₁) (CategoryTheory.eqToHom e₂)
        (CategoryTheory.eqToHom e₃)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.eqToHomTransIso e₁ e₂).inv
        (CategoryTheory.eqToHom e₃))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.eqToHomTransIso ⋯ e₃).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.eqToHomTransIso e₁ ⋯).hom
          (CategoryTheory.Bicategory.whiskerLeft (CategoryTheory.eqToHom e₁)
            (CategoryTheory.Bicategory.eqToHomTransIso e₂ e₃).hom)))
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbitRel.Quotient.nonempty_orbit : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (x : MulAction.orbitRel.Quotient G α),
  x.orbit.Nonempty
-- Mathlib.Order.Category.DistLat
DistLat.comp_apply : ∀ {X Y Z : DistLat} (f : X ⟶ Y) (g : Y ⟶ Z) (x : ↑X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.rootForm_anisotropic : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : LinearOrder R] [IsStrictOrderedRing R] [inst_6 : Module R M]
  [inst_7 : Module R N] (P : RootPairing ι R M N) [P.IsRootSystem],
  (LinearMap.BilinMap.toQuadraticMap P.RootForm).Anisotropic
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} [inst : BEq α] [inst_1 : LawfulBEq α]
  {f : (a : α) → β a → Option (γ a)} {l : List ((a : α) × β a)} {k : α} (hl : Std.Internal.List.DistinctKeys l)
  (h :
    Std.Internal.List.containsKey k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) =
      true),
  Std.Internal.List.getValueCast k (List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) l) h =
    (f k (Std.Internal.List.getValueCast k l ⋯)).get ⋯
-- Mathlib.RingTheory.DividedPowers.Basic
DividedPowers.dpow_zero : ∀ {A : Type u_1} [inst : CommSemiring A] {I : Ideal A} (self : DividedPowers I) {x : A}, x ∈ I → self.dpow 0 x = 1
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.algEquivOpMop_symm_apply_coe : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S : Subalgebra R A) (a : (↥S.op)ᵐᵒᵖ), ↑(S.algEquivOpMop.symm a) = MulOpposite.unop ↑(MulOpposite.unop a)
-- Mathlib.Data.QPF.Multivariate.Constructions.Quot
/-- If `F` is a QPF then `G` is a QPF as well. Can be used to
construct `MvQPF` instances by transporting them across
surjective functions  -/
MvQPF.quotientQPF : {n : ℕ} →
  {F : TypeVec.{u} n → Type u} →
    [q : MvQPF F] →
      {G : TypeVec.{u} n → Type u} →
        [inst : MvFunctor G] →
          {FG_abs : {α : TypeVec.{u} n} → F α → G α} →
            {FG_repr : {α : TypeVec.{u} n} → G α → F α} →
              (∀ {α : TypeVec.{u} n} (x : G α), FG_abs (FG_repr x) = x) →
                (∀ {α β : TypeVec.{u} n} (f : α.Arrow β) (x : F α),
                    FG_abs (MvFunctor.map f x) = MvFunctor.map f (FG_abs x)) →
                  MvQPF G
-- Mathlib.GroupTheory.Perm.Fin
Fin.cycleIcc_zero_eq_cycleRange : ∀ {n : ℕ} (i : Fin n) [inst : NeZero n], Fin.cycleIcc 0 i = i.cycleRange
-- Mathlib.CategoryTheory.Action.Basic
Action.FunctorCategoryEquivalence.unitIso_hom_app_hom : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {G : Type u_2} [inst_1 : Monoid G] (X : Action V G),
  (Action.FunctorCategoryEquivalence.unitIso.hom.app X).hom = CategoryTheory.CategoryStruct.id X.V
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- Constructor for functors from the homotopy category.  -/
SSet.Truncated.HomotopyCategory.lift : {V : SSet.Truncated 2} →
  {D : Type u_1} →
    [inst : CategoryTheory.Category.{v_1, u_1} D] →
      (obj : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 }) → D) →
        (map :
            {x y : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })} →
              SSet.Truncated.Edge x y → (obj x ⟶ obj y)) →
          (∀ (x : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })),
              map (SSet.Truncated.Edge.id x) = CategoryTheory.CategoryStruct.id (obj x)) →
            (∀ {x₀ x₁ x₂ : V.obj (Opposite.op { obj := { len := 0 }, property := SSet.OneTruncation₂._proof_1 })}
                {e₀₁ : SSet.Truncated.Edge x₀ x₁} {e₁₂ : SSet.Truncated.Edge x₁ x₂} {e₀₂ : SSet.Truncated.Edge x₀ x₂}
                (x : e₀₁.CompStruct e₁₂ e₀₂), CategoryTheory.CategoryStruct.comp (map e₀₁) (map e₁₂) = map e₀₂) →
              CategoryTheory.Functor V.HomotopyCategory D
-- Lean.LibrarySuggestions.Basic
Lean.LibrarySuggestions.Suggestion.mk.injEq : ∀ (name : Lean.Name) (score : Float) (flag : Option String) (name_1 : Lean.Name) (score_1 : Float)
  (flag_1 : Option String),
  ({ name := name, score := score, flag := flag } = { name := name_1, score := score_1, flag := flag_1 }) =
    (name = name_1 ∧ score = score_1 ∧ flag = flag_1)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.functorPushforward_functorPullback_overForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X}
  (S : CategoryTheory.Sieve Y.left),
  CategoryTheory.Sieve.functorPushforward (CategoryTheory.Over.forget X)
      (CategoryTheory.Sieve.functorPullback (CategoryTheory.Over.forget X) S) =
    S
-- Mathlib.Data.Nat.Factorial.NatCast
/-- If `A` is an algebra over a characteristic-zero (semi)field, then `n!` is a unit.  -/
IsUnit.natCast_factorial_of_algebra : ∀ {A : Type u_1} [inst : Semiring A] (K : Type u_2) [inst_1 : Semifield K] [CharZero K] [Algebra K A] (n : ℕ),
  IsUnit ↑n.factorial
-- Mathlib.Algebra.Group.Subgroup.Basic
MulEquiv.normal_map_iff : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] {f : G ≃* G'} {H : Subgroup G},
  (Subgroup.map (↑f) H).Normal ↔ H.Normal
-- Mathlib.Data.Nat.Bits
Nat.div2_two : Nat.div2 2 = 1
-- Mathlib.Order.WithBot
WithBot.instOrderBot.eq_1 : ∀ {α : Type u_1} [inst : LE α], WithBot.instOrderBot = { toBot := WithBot.bot, bot_le := ⋯ }
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instFromJsonCodeActionLiteralSupport : Lean.FromJson Lean.Lsp.CodeActionLiteralSupport
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddCommMagma : {M : Type u_1} →
  [inst : TopologicalSpace M] → [inst_1 : AddCommMagma M] → [ContinuousAdd M] → AddCommMagma (SeparationQuotient M)
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.instBEqInlayHintTextEdit : BEq Lean.Elab.InlayHintTextEdit
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.image_log_Ioc : ∀ {a b : ℝ}, 0 < a → a ≤ b → Real.log '' Set.Ioc a b = Set.Ioc (Real.log a) (Real.log b)
-- Std.Data.DTreeMap.Internal.Ordered
Std.DTreeMap.Internal.Impl.Ordered.right : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {sz : ℕ} {k : α} {v : β k} {l r : Std.DTreeMap.Internal.Impl α β},
  (Std.DTreeMap.Internal.Impl.inner sz k v l r).Ordered → r.Ordered
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
IsUniformGroup.mk' : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : Group α],
  (UniformContinuous fun p => p.1 * p.2) → (UniformContinuous fun p => p⁻¹) → IsUniformGroup α
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueSums.toIsCancelAdd : ∀ {G : Type u} [inst : Add G] [UniqueSums G], IsCancelAdd G
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- The canonical isomorphism between the domains of two strongly Cartesian morphisms lying over
isomorphic objects.  -/
CategoryTheory.Functor.IsStronglyCartesian.domainIsoOfBaseIso : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        (p : CategoryTheory.Functor 𝒳 𝒮) →
          {R R' S : 𝒮} →
            {a a' b : 𝒳} →
              {f : R ⟶ S} →
                {f' : R' ⟶ S} →
                  {g : R' ≅ R} →
                    f' = CategoryTheory.CategoryStruct.comp g.hom f →
                      (φ : a ⟶ b) → (φ' : a' ⟶ b) → [p.IsStronglyCartesian f φ] → [p.IsStronglyCartesian f' φ'] → a' ≅ a
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.mem_insertMany_list : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k : α},
  k ∈ Std.DHashMap.Const.insertMany m l ↔ k ∈ m ∨ (List.map Prod.fst l).contains k = true
-- Std.Tactic.BVDecide.LRAT.Internal.CNF
Std.Tactic.BVDecide.LRAT.Internal.Formula.limplies_insert : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ] [inst_2 : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ]
  {c : β} {f : σ}, Std.Tactic.BVDecide.LRAT.Internal.Limplies α (Std.Tactic.BVDecide.LRAT.Internal.Formula.insert f c) f
-- Lean.Parser.Term
Lean.Parser.Termination.terminationBy.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.VectorBundle.Constructions
Bundle.Trivialization.pullback_linear : ∀ (𝕜 : Type u_2) {B : Type u_3} {F : Type u_4} {E : B → Type u_5} {B' : Type u_6} [inst : TopologicalSpace B']
  [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_2 : NontriviallyNormedField 𝕜]
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] [inst_5 : TopologicalSpace B]
  [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)] {K : Type u_7} [inst_8 : FunLike K B' B]
  [inst_9 : ContinuousMapClass K B' B] (e : Bundle.Trivialization F Bundle.TotalSpace.proj)
  [Bundle.Trivialization.IsLinear 𝕜 e] (f : K), Bundle.Trivialization.IsLinear 𝕜 (e.pullback f)
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.preprocessOutParam : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Algebra.CubicDiscriminant
Cubic.splits_iff_roots_eq_three : ∀ {F : Type u_3} {K : Type u_4} {P : Cubic F} [inst : Field F] [inst_1 : Field K] {φ : F →+* K},
  P.a ≠ 0 → ((Polynomial.map φ P.toPoly).Splits ↔ ∃ x y z, (Cubic.map φ P).roots = {x, y, z})
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.continuous_restrictScalars : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [ContinuousSMul 𝕜 E] {𝕜' : Type u_5}
  [inst_9 : NontriviallyNormedField 𝕜'] [inst_10 : NormedAlgebra 𝕜' 𝕜] [inst_11 : Module 𝕜' E]
  [inst_12 : IsScalarTower 𝕜' 𝕜 E] [inst_13 : Module 𝕜' F] [inst_14 : IsScalarTower 𝕜' 𝕜 F],
  Continuous (ContinuousAlternatingMap.restrictScalars 𝕜')
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_lt_top_iff_lintegral_rpow_enorm_lt_top : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} [inst : ENorm ε]
  {f : α → ε}, p ≠ 0 → p ≠ ⊤ → (MeasureTheory.eLpNorm f p μ < ⊤ ↔ ∫⁻ (a : α), ‖f a‖ₑ ^ p.toReal ∂μ < ⊤)
-- Mathlib.GroupTheory.Torsion
/-- Elements of the `p`-primary component have order `p^n` for some `n`.  -/
CommMonoid.primaryComponent.exists_orderOf_eq_prime_pow : ∀ {G : Type u_1} [inst : CommMonoid G] {p : ℕ} [hp : Fact (Nat.Prime p)] (g : ↥(CommMonoid.primaryComponent G p)),
  ∃ n, orderOf g = p ^ n
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.Monadic.isPlausibleOutput_iff : ∀ {α : Type u} {a : α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  {it : Std.IterM Id α}, it.IsPlausibleOutput a ↔ it.internalState.next = some a ∧ a ≤ it.internalState.upperBound
-- Mathlib.Algebra.Module.PID
/-- A finitely generated torsion module over a PID is isomorphic to a direct sum of some
`R ⧸ R ∙ (p i ^ e i)` where the `p i ^ e i` are prime powers.  -/
Module.equiv_directSum_of_isTorsion : ∀ {R : Type u} [inst : CommRing R] [IsPrincipalIdealRing R] {M : Type v} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [IsDomain R] [h' : Module.Finite R M],
  Module.IsTorsion R M →
    ∃ ι x p, ∃ (_ : ∀ (i : ι), Irreducible (p i)), ∃ e, Nonempty (M ≃ₗ[R] DirectSum ι fun i => R ⧸ R ∙ p i ^ e i)
-- Mathlib.Algebra.Ring.Basic
inv_neg : ∀ {R : Type u_1} [inst : DivisionMonoid R] [inst_1 : HasDistribNeg R] {a : R}, (-a)⁻¹ = -a⁻¹
-- Mathlib.Algebra.Order.BigOperators.GroupWithZero.Finset
/-- A finite product of nonnegative antitone functions is antitone. See also
`Antitone.finsetProd'` for the case of an ordered commutative multiplicative monoid.  -/
Antitone.finsetProd : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommMonoidWithZero R] [inst_1 : Preorder R] [ZeroLEOneClass R] [PosMulMono R]
  {s : Finset ι} {γ : Type u_4} [inst_4 : Preorder γ] {f : ι → γ → R},
  (∀ i ∈ s, Antitone (f i)) → (∀ i ∈ s, ∀ (x : γ), 0 ≤ f i x) → Antitone fun x => ∏ i ∈ s, f i x
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.mapComp_inv_app : ∀ {I : Type w₁} (C : I → Type u₁) [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {J : Type w₂} {K : Type w₃}
  (f : K → J) (g : J → I) (X : (i : K) × (fun i => C (g (f i))) i),
  (CategoryTheory.Sigma.mapComp C f g).inv.app X = CategoryTheory.CategoryStruct.id ⟨g (f X.fst), X.snd⟩
-- Mathlib.Combinatorics.Quiver.Subquiver
Quiver.Total.mk.injEq : ∀ {V : Type u} [inst : Quiver V] (left right : V) (hom : left ⟶ right) (left_1 right_1 : V) (hom_1 : left_1 ⟶ right_1),
  ({ left := left, right := right, hom := hom } = { left := left_1, right := right_1, hom := hom_1 }) =
    (left = left_1 ∧ right = right_1 ∧ hom ≍ hom_1)
-- Mathlib.Algebra.Algebra.RestrictScalars
/-- If we put an `R`-algebra structure on a semiring `S`, we get a natural equivalence from the
category of `S`-modules to the category of representations of the algebra `S` (over `R`). The type
synonym `RestrictScalars` is essentially this equivalence.

Warning: use this type synonym judiciously! Consider an example where we want to construct an
`R`-linear map from `M` to `S`, given:
```lean
variable (R S M : Type*)
variable [CommSemiring R] [Semiring S] [Algebra R S] [AddCommMonoid M] [Module S M]
```
With the assumptions above we can't directly state our map as we have no `Module R M` structure, but
`RestrictScalars` permits it to be written as:
```lean
-- an `R`-module structure on `M` is provided by `RestrictScalars` which is compatible
example : RestrictScalars R S M →ₗ[R] S := sorry
```
However, it is usually better just to add this extra structure as an argument:
```lean
-- an `R`-module structure on `M` and proof of its compatibility is provided by the user
example [Module R M] [IsScalarTower R S M] : M →ₗ[R] S := sorry
```
The advantage of the second approach is that it defers the duty of providing the missing typeclasses
`[Module R M] [IsScalarTower R S M]`. If some concrete `M` naturally carries these (as is often
the case) then we have avoided `RestrictScalars` entirely. If not, we can pass
`RestrictScalars R S M` later on instead of `M`.

Note that this means we almost always want to state definitions and lemmas in the language of
`IsScalarTower` rather than `RestrictScalars`.

An example of when one might want to use `RestrictScalars` would be if one has a vector space
over a field of characteristic zero and wishes to make use of the `ℚ`-algebra structure.  -/
RestrictScalars : Type u_5 → Type u_6 → Type u_7 → Type u_7
-- Init.Data.Int.Order
Int.neg_of_mul_neg_left : ∀ {a b : ℤ}, a * b < 0 → 0 < b → a < 0
-- Mathlib.Algebra.Group.Semiconj.Defs
/-- The relation “there exists an element that semiconjugates `a` to `b`” on a semigroup
is transitive.  -/
SemiconjBy.isTrans : ∀ {S : Type u_1} [inst : Semigroup S], IsTrans S fun a b => ∃ c, SemiconjBy c a b
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem_toArray_rco : ∀ {m n i : ℕ} (_h : i < (m...n).toArray.size), (m...n).toArray[i] = m + i
-- Mathlib.Order.ModularLattice
IsModularLattice.complementedLattice_Ici : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {a : α} [inst_2 : BoundedOrder α] [ComplementedLattice α],
  ComplementedLattice ↑(Set.Ici a)
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instNonUnitalCommRing : {R : Type u_1} → [NonUnitalCommRing R] → NonUnitalCommRing Rᵃᵒᵖ
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The homotopy between `cylinder.ι₀ K` and `cylinder.ι₁ K`.  -/
HomologicalComplex.cylinder.homotopy₀₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasCylinder] →
                  (∀ (j : ι), ∃ i, c.Rel i j) →
                    Homotopy (HomologicalComplex.cylinder.ι₀ K) (HomologicalComplex.cylinder.ι₁ K)
-- Lean.Expr
Lean.MVarIdMap : Type → Type
-- Std.Internal.Do.Order.Heyting
/-- Pointwise characterization of Heyting implication on function lattices.  -/
Lean.Order.himp_apply : ∀ {σ : Type v} {β : Type u} [inst : Lean.Order.CompleteLattice β] (a b : σ → β) (s : σ),
  Lean.Order.himp a b s = Lean.Order.himp (a s) (b s)
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
ContinuousMultilinearMap.compContinuousLinearMapLRight_apply : ∀ {𝕜 : Type u} {ι : Type v} {E : ι → Type wE} {E₁ : ι → Type wE₁} {G : Type wG} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)]
  [inst_3 : (i : ι) → SeminormedAddCommGroup (E₁ i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (E₁ i)]
  [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] [inst_7 : Fintype ι]
  (g : ContinuousMultilinearMap 𝕜 E₁ G) (f : (i : ι) → E i →L[𝕜] E₁ i),
  g.compContinuousLinearMapLRight f = g.compContinuousLinearMap f
-- Init.Data.UInt.Lemmas
UInt32.le_iff_toBitVec_le : ∀ {a b : UInt32}, a ≤ b ↔ a.toBitVec ≤ b.toBitVec
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.submatrix : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  {M : Matrix n n R}, M.PosDef → ∀ {e : m → n}, Function.Injective e → (M.submatrix e e).PosDef
-- Std.Http.Data.Status
/-- A proposition stating that `s` is a valid HTTP reason phrase: every character passes
`Char.reasonPhraseChar` per RFC 9110 §15.

Reference: https://httpwg.org/specs/rfc9110.html#reason.phrase
 -/
Std.Http.IsValidReasonPhrase : String → Prop
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.cos_int_mul_two_pi_add_pi : ∀ (n : ℤ), Complex.cos (↑n * (2 * ↑Real.pi) + ↑Real.pi) = -1
-- Mathlib.Topology.NhdsWithin
mem_nhdsWithin_subtype : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} {a : { x // x ∈ s }} {t u : Set { x // x ∈ s }},
  t ∈ nhdsWithin a u ↔ t ∈ Filter.comap Subtype.val (nhdsWithin (↑a) (Subtype.val '' u))
-- Std.Data.TreeSet.Raw.Basic
/-- Two tree sets are equivalent in the sense of Equiv iff all the values are equal.  -/
Std.TreeSet.Raw.«term_~m_» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monoidal.Limits.HasLimits
CategoryTheory.MonoidalCategory.Limits.HasColimit.whiskerLeft_isoOfNatIso_ι_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {J : Type u₁}
  [inst_2 : CategoryTheory.Category.{v₁, u₁} J] {F G : CategoryTheory.Functor J C}
  [inst_3 : CategoryTheory.Limits.HasColimit F] [inst_4 : CategoryTheory.Limits.HasColimit G] (w : F ≅ G) (j : J)
  {Q Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Q (CategoryTheory.Limits.colimit G) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.colimit.ι F j))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.HasColimit.isoOfNatIso w).hom) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (w.hom.app j))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Q (CategoryTheory.Limits.colimit.ι G j)) h)
-- Lean.Data.Json.FromToJson.Basic
Lean.instFromJsonProd : {α : Type u} → {β : Type v} → [Lean.FromJson α] → [Lean.FromJson β] → Lean.FromJson (α × β)
-- Mathlib.Logic.Basic
heq_iff_exists_eq_cast : ∀ {α β : Sort u} {a : α} {b : β}, a ≍ b ↔ ∃ (h : β = α), a = cast h b
-- Mathlib.RingTheory.Nilpotent.Lemmas
Module.End.isNilpotent.restrict : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {f : M →ₗ[R] M}
  {p : Submodule R M} (hf : Set.MapsTo ⇑f ↑p ↑p), IsNilpotent f → IsNilpotent (f.restrict hf)
-- Mathlib.ModelTheory.Algebra.Ring.Basic
FirstOrder.Ring.neg_def : ∀ (α : Type u_2) (t : FirstOrder.Language.ring.Term α), -t = FirstOrder.Ring.negFunc.apply₁ t
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Icc_union_Ico_eq_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α}, a ≤ b → b < c → Set.Icc a b ∪ Set.Ico b c = Set.Ico a c
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
/-- Given a homomorphism from a subgraph to `F`, construct its restriction to a sub-subgraph.  -/
SimpleGraph.FinsubgraphHom.restrict : {V : Type u} →
  {W : Type v} →
    {G : SimpleGraph V} →
      {F : SimpleGraph W} →
        {G' G'' : G.Finsubgraph} → G'' ≤ G' → SimpleGraph.FinsubgraphHom G' F → SimpleGraph.FinsubgraphHom G'' F
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.coe_eq_coe : ∀ {X : Type u_1} {x y : X}, ↑x = ↑y ↔ x = y
-- Mathlib.Topology.Algebra.FilterBasis
/-- The topology associated to a ring filter basis.
It has the given basis as a basis of neighborhoods of zero.  -/
RingFilterBasis.topology : {R : Type u} → [inst : Ring R] → RingFilterBasis R → TopologicalSpace R
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem?_toList_rcc_eq_some_iff : ∀ {k m n : ℤ} {i : ℕ}, (m...=n).toList[i]? = some k ↔ i < (n + 1 - m).toNat ∧ m + ↑i = k