mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.liminf_add_le : ∀ {α : Type u_3} {f : Filter α} {u v : α → EReal},
  Filter.limsup u f ≠ ⊥ ∨ Filter.liminf v f ≠ ⊤ →
    Filter.limsup u f ≠ ⊤ ∨ Filter.liminf v f ≠ ⊥ → Filter.liminf (u + v) f ≤ Filter.limsup u f + Filter.liminf v f
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_nonpos : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] {x : K},
  x ≤ 0 → ArchimedeanClass.stdPart x ≤ 0
-- Mathlib.Topology.Homeomorph.Defs
Homeomorph.comp_continuous_iff' : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (h : X ≃ₜ Y) {f : Y → Z}, Continuous (f ∘ ⇑h) ↔ Continuous f
-- Init.Meta
Lean.Parser.Tactic.simpAllKind : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCore.inj : ∀ {e : Lean.Expr} {lhs rhs : Lean.Meta.Grind.Arith.Linear.LinExpr} {e_1 : Lean.Expr}
  {lhs_1 rhs_1 : Lean.Meta.Grind.Arith.Linear.LinExpr},
  Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCore e lhs rhs =
      Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.notCore e_1 lhs_1 rhs_1 →
    e = e_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C),
  (CategoryTheory.BraidedCategory.tensorLeftIsoTensorRight X).hom.app Y = (β_ X Y).hom
-- Mathlib.Topology.UniformSpace.Completion
/-- Space of Cauchy filters

This is essentially the completion of a uniform space. The embeddings are the neighbourhood filters.
This space is not minimal, the separated uniform space (i.e. quotiented on the intersection of all
entourages) is necessary for this.
 -/
CauchyFilter : (α : Type u) → [UniformSpace α] → Type u
-- Mathlib.Algebra.Order.Group.Cone
GroupCone.instSetLike.eq_1 : ∀ (G : Type u_1) [inst : CommGroup G], GroupCone.instSetLike G = { coe := fun C => C.carrier, coe_injective := ⋯ }
-- Lean.ErrorExplanation
/-- Returns `true` if there exists an error explanation named `name`.  -/
Lean.hasErrorExplanation : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → m Bool
-- Init.Data.BitVec.Lemmas
BitVec.zero_sle_eq_not_msb : ∀ {w : ℕ} {x : BitVec w}, (0#w).sle x = !x.msb
-- Mathlib.Data.Nat.PSub
Nat.psub.eq_1 : ∀ (m : ℕ), m.psub 0 = some m
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.coeff_single_of_ne : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {a b : Γ} {r : R},
  b ≠ a → ((HahnSeries.single a) r).coeff b = 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- If `c` is a colimit cocone for a functor `F : C ⥤ H` and `α : F ⟶ L ⋙ F'` is the unit of any
left Kan extension `F' : D ⥤ H` of `F` along `L : C ⥤ D`, then `coconeOfIsLeftKanExtension α c` is
a colimit cocone, too.  -/
CategoryTheory.Functor.isColimitCoconeOfIsLeftKanExtension : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} →
                {F : CategoryTheory.Functor C H} →
                  (α : F ⟶ L.comp F') →
                    [inst_3 : F'.IsLeftKanExtension α] →
                      {c : CategoryTheory.Limits.Cocone F} →
                        CategoryTheory.Limits.IsColimit c →
                          CategoryTheory.Limits.IsColimit (F'.coconeOfIsLeftKanExtension α c)
-- Mathlib.Data.Nat.Cast.SetInterval
Nat.range_cast_int : Set.range Nat.cast = Set.Ici 0
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
/-- Affine isomorphisms between the domains and codomains of two spaces of affine maps give a
bijection between the two function spaces.

See `AffineEquiv.arrowCongr` and `AffineEquiv.arrowCongrₗ` for the affine and linear versions of
this bijection.  -/
AffineEquiv.arrowCongrEquiv : {k : Type u_1} →
  {P₁ : Type u_2} →
    {P₂ : Type u_3} →
      {P₃ : Type u_4} →
        {P₄ : Type u_5} →
          {V₁ : Type u_6} →
            {V₂ : Type u_7} →
              {V₃ : Type u_8} →
                {V₄ : Type u_9} →
                  [inst : Ring k] →
                    [inst_1 : AddCommGroup V₁] →
                      [inst_2 : AddCommGroup V₂] →
                        [inst_3 : AddCommGroup V₃] →
                          [inst_4 : AddCommGroup V₄] →
                            [inst_5 : Module k V₁] →
                              [inst_6 : Module k V₂] →
                                [inst_7 : Module k V₃] →
                                  [inst_8 : Module k V₄] →
                                    [inst_9 : AddTorsor V₁ P₁] →
                                      [inst_10 : AddTorsor V₂ P₂] →
                                        [inst_11 : AddTorsor V₃ P₃] →
                                          [inst_12 : AddTorsor V₄ P₄] →
                                            (P₁ ≃ᵃ[k] P₂) → (P₃ ≃ᵃ[k] P₄) → (P₁ →ᵃ[k] P₃) ≃ (P₂ →ᵃ[k] P₄)
-- Std.Http.Server.Connection
/-- The processing machine for HTTP/1.1.
 -/
Std.Http.Server.Connection.machine : {α : Type} → Std.Http.Server.Connection α → Std.Http.Protocol.H1.Machine Std.Http.Protocol.H1.Direction.receiving
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toList_eq_toListModel : ∀ {α : Type u} {β : α → Type v} {t : Std.DTreeMap.Internal.Impl α β}, t.toList = t.toListModel
-- Lean.Elab.Tactic.Simp
/-- Position for the `only` child syntax in the `simp` tactic.  -/
Lean.Elab.Tactic.simpOnlyPos : ℕ
-- Mathlib.Order.Interval.Finset.Defs
Set.finite_Ici : ∀ {α : Type u_1} [inst : Preorder α] [LocallyFiniteOrderTop α] (a : α), (Set.Ici a).Finite
-- Mathlib.Algebra.Category.Ring.Basic
/-- This unification hint helps with problems of the form `(forget ?C).obj R =?= carrier R'`.  -/
SemiRingCat.forget_obj_eq_coe : SemiRingCat → SemiRingCat → Prop
-- Lean.Elab.App
Lean.Elab.Term.ElabElim.M : Type → Type
-- Mathlib.Algebra.Ring.Periodic
Function.Antiperiodic.sub : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {c₁ c₂ : α} [inst : AddGroup α] [inst_1 : InvolutiveNeg β],
  Function.Antiperiodic f c₁ → Function.Antiperiodic f c₂ → Function.Periodic f (c₁ - c₂)
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanIso.mul_eq_mul : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {A : Set α} {B : Set β} {f : α → β},
  IsMulFreimanIso 2 A B f → ∀ {a b c d : α}, a ∈ A → b ∈ A → c ∈ A → d ∈ A → (f a * f b = f c * f d ↔ a * b = c * d)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
add_neg_le_add_neg_iff : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c d : α}, a + -b ≤ c + -d ↔ a + d ≤ c + b
-- Init.Data.List.MinMax
_private.Init.Data.List.MinMax.0.List.head.match_1.eq_1 : ∀ {α : Type u_1} (motive : (x : List α) → x ≠ [] → Sort u_2) (a : α) (tail : List α) (x : a :: tail ≠ [])
  (h_1 : (a : α) → (tail : List α) → (x : a :: tail ≠ []) → motive (a :: tail) x),
  (match a :: tail, x with
    | a :: tail, x => h_1 a tail x) =
    h_1 a tail x
-- Mathlib.Topology.LocallyConstant.Basic
LocallyConstant.indicator.eq_1 : ∀ {X : Type u_1} [inst : TopologicalSpace X] {R : Type u_5} [inst_1 : Zero R] {U : Set X} (f : LocallyConstant X R)
  (hU : IsClopen U), f.indicator hU = { toFun := U.indicator ⇑f, isLocallyConstant := ⋯ }
-- Init.Data.UInt.Bitwise
UInt64.toUInt8_not : ∀ (a : UInt64), (~~~a).toUInt8 = ~~~a.toUInt8
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.idemFst_compl : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β] {p : ENNReal},
  1 - WithLp.idemFst = WithLp.idemSnd
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
/-- This is a `HasPullback` variant of `CategoryTheory.IsPullback.paste_twist_right`  -/
CategoryTheory.IsPullback.map_fst_comp_fst_snd_comp_fst : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z U S : C} (f : X ⟶ S) (g : Y ⟶ S) (i : Z ⟶ S)
  [inst_1 : CategoryTheory.Limits.HasPullback i g] (h : U ⟶ CategoryTheory.Limits.pullback i g)
  [inst_2 : CategoryTheory.Limits.HasPullback f g]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.snd f g)
      (CategoryTheory.CategoryStruct.comp h (CategoryTheory.Limits.pullback.snd i g))]
  [inst_4 : CategoryTheory.Limits.HasPullback f i],
  CategoryTheory.IsPullback
    (CategoryTheory.Limits.pullback.map (CategoryTheory.Limits.pullback.snd f g)
      (CategoryTheory.CategoryStruct.comp h (CategoryTheory.Limits.pullback.snd i g)) f i
      (CategoryTheory.Limits.pullback.fst f g)
      (CategoryTheory.CategoryStruct.comp h (CategoryTheory.Limits.pullback.fst i g)) g ⋯ ⋯)
    (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.snd f g)
      (CategoryTheory.CategoryStruct.comp h (CategoryTheory.Limits.pullback.snd i g)))
    (CategoryTheory.Limits.pullback.snd f i)
    (CategoryTheory.CategoryStruct.comp h (CategoryTheory.Limits.pullback.fst i g))
-- Mathlib.Data.Finsupp.MonomialOrder.DegLex
ofDegLex_add : ∀ {α : Type u_1} [inst : AddCommMonoid α] (a b : DegLex α), ofDegLex (a + b) = ofDegLex a + ofDegLex b
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.Monoidal.id_tensorHom : ∀ {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] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : W.IsMonoidal]
  [inst_4 : L.IsLocalization W] {unit : D} (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit)
  (X : CategoryTheory.LocalizedMonoidal L W ε) {Y₁ Y₂ : CategoryTheory.LocalizedMonoidal L W ε} (f : Y₁ ⟶ Y₂),
  CategoryTheory.MonoidalCategoryStruct.tensorHom (CategoryTheory.CategoryStruct.id X) f =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.Triangle.isZero₂_of_isZero₁₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    CategoryTheory.Limits.IsZero T.obj₁ → CategoryTheory.Limits.IsZero T.obj₃ → CategoryTheory.Limits.IsZero T.obj₂
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isCompact_isOpen_iff : ∀ {R : Type u} [inst : CommSemiring R] {s : Set (PrimeSpectrum R)},
  IsCompact s ∧ IsOpen s ↔ ∃ t, (PrimeSpectrum.zeroLocus ↑t)ᶜ = s
-- Mathlib.GroupTheory.Subgroup.Center
Subgroup.centerCharacteristic : ∀ {G : Type u_1} [inst : Group G], (Subgroup.center G).Characteristic
-- Mathlib.Algebra.Group.Graph
AddMonoidHom.mem_graph : ∀ {G : Type u_1} {H : Type u_2} [inst : AddGroup G] [inst_1 : AddGroup H] {f : G →+ H} {x : G × H},
  x ∈ f.graph ↔ f x.1 = x.2
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpL1CLM_smul : ∀ {α : Type u_1} {F' : Type u_3} {𝕜 : Type u_6} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F']
  [inst_2 : NormedSpace 𝕜 F'] [inst_3 : NormedSpace ℝ F'] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {hm : m ≤ m0} [inst_4 : MeasureTheory.SigmaFinite (μ.trim hm)] [inst_5 : CompleteSpace F'] (c : 𝕜)
  (f : ↥(MeasureTheory.Lp F' 1 μ)),
  (MeasureTheory.condExpL1CLM F' hm μ) (c • f) = c • (MeasureTheory.condExpL1CLM F' hm μ) f
-- Lean.Server.CodeActions.Provider
/-- The cursor is between tactics, and the nearest enclosing range is a tactic sequence.
Code actions will insert tactics at index `insertIdx` into the syntax
(which is a nullNode of `tactic;*` inside a `tacticSeqBracketed` or `tacticSeq1Indented`).  -/
Lean.CodeAction.FindTacticResult.tacticSeq : Bool → ℕ → Lean.Syntax.Stack → Lean.CodeAction.FindTacticResult
-- Lean.DocString.Types
Lean.Doc.instBEqInline.beq : {i : Type u_1} → [BEq i] → Lean.Doc.Inline i → Lean.Doc.Inline i → Bool
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.instInhabited : {k : Type u_1} →
  {V1 : Type u_2} →
    {P1 : Type u_3} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V1] → [inst_2 : Module k V1] → [inst_3 : AddTorsor V1 P1] → Inhabited (P1 →ᵃ[k] P1)
-- Mathlib.Order.Filter.Basic
Filter.frequently_top : ∀ {α : Type u} {p : α → Prop}, (∃ᶠ (x : α) in ⊤, p x) ↔ ∃ x, p x
-- Lean.Elab.Do.Basic
Lean.Elab.Do.Context.mk.sizeOf_spec : ∀ (monadInfo : Lean.Elab.Do.MonadInfo) (mutVars : Array Lean.Elab.Do.MutVar)
  (mutVarDefs : Std.HashMap Lean.Name Lean.Elab.Do.MutVar) (doBlockResultType : Lean.Expr)
  (contInfo : Lean.Elab.Do.ContInfoRef) (deadCode : Lean.Elab.Do.CodeLiveness) (ops : Lean.Elab.Do.DoOpsRef),
  sizeOf
      { monadInfo := monadInfo, mutVars := mutVars, mutVarDefs := mutVarDefs, doBlockResultType := doBlockResultType,
        contInfo := contInfo, deadCode := deadCode, ops := ops } =
    1 + sizeOf monadInfo + sizeOf mutVars + sizeOf mutVarDefs + sizeOf doBlockResultType + sizeOf contInfo +
        sizeOf deadCode +
      sizeOf ops
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
groupHomology.chainsMap_f_2_comp_chainsIso₂_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k G}
  {B : Rep.{u, u, u} k H} (f : G →* H) (φ : A ⟶ Rep.res f B) {Z : ModuleCat k} (h : ModuleCat.of k (H × H →₀ ↑B) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((groupHomology.chainsMap f φ).f 2)
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₂ B).hom h) =
    CategoryTheory.CategoryStruct.comp (groupHomology.chainsIso₂ A).hom
      (CategoryTheory.CategoryStruct.comp (groupHomology.chainsMap₂ f φ) h)
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScottHausdorff.isClosed_iff_dirSupClosed : ∀ {α : Type u_1} {s : Set α} [inst : Preorder α] [t : TopologicalSpace α] [Topology.IsScottHausdorff α Set.univ],
  IsClosed s ↔ DirSupClosed s
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.mem_subgroupGalEquivSubgroupChar_symm_iff : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K] (R : Type u_2) [inst_3 : CommRing R]
  [inst_4 : HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)] (σ : Gal(K/ℚ)) (Y : Subgroup (DirichletCharacter R n)),
  σ ∈ (IsCyclotomicExtension.Rat.subgroupGalEquivSubgroupChar n K R).symm (OrderDual.toDual Y) ↔
    ∀ χ ∈ Y, χ ↑((IsCyclotomicExtension.Rat.galEquivZMod n K) σ) = 1
-- Mathlib.CategoryTheory.Triangulated.TStructure.Heart
CategoryTheory.Triangulated.TStructure.instIsLEObjιHeartOfNatInt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (H : Type u') [inst_6 : CategoryTheory.Category.{v', u'} H]
  [inst_7 : CategoryTheory.Preadditive H] [inst_8 : t.Heart H] (X : H), t.IsLE (t.ιHeart.obj X) 0
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
/-- A multiplicative morphism property `W` has left calculus of fractions if
any right fraction can be turned into a left fraction and that two morphisms
that can be equalized by precomposition with a morphism in `W` can also
be equalized by postcomposition with a morphism in `W`.  -/
CategoryTheory.MorphismProperty.HasLeftCalculusOfFractions : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.MorphismProperty C → Prop
-- Mathlib.Algebra.Homology.ComplexShapeSigns
TotalComplexShapeSymmetry.σ_ε₂ : ∀ {I₁ : Type u_1} {I₂ : Type u_2} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  {c₁₂ : ComplexShape I₁₂} {inst : TotalComplexShape c₁ c₂ c₁₂} {inst_1 : TotalComplexShape c₂ c₁ c₁₂}
  [self : TotalComplexShapeSymmetry c₁ c₂ c₁₂] (i₁ : I₁) {i₂ i₂' : I₂},
  c₂.Rel i₂ i₂' →
    TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂ * c₁.ε₂ c₂ c₁₂ (i₁, i₂) =
      c₂.ε₁ c₁ c₁₂ (i₂, i₁) * TotalComplexShapeSymmetry.σ c₁ c₂ c₁₂ i₁ i₂'
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.liftRingHom.congr_simp : ∀ {L : Type u_2} {R : Type u_3} [inst : Field L] [inst_1 : CommRing R] (φ φ_1 : Polynomial R →+* L) (e_φ : φ = φ_1)
  (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors L)),
  RatFunc.liftRingHom φ hφ = RatFunc.liftRingHom φ_1 ⋯
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.foldM_eq_forIn : ∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'}
  [inst_2 : Monad m] [inst_3 : Std.IteratorLoop α Id m] {f : γ → β → m γ} {init : γ} {it : Std.Iter β},
  Std.Iter.foldM f init it = forIn it init fun x acc => ForInStep.yield <$> f acc x
-- Mathlib.Order.Hom.Basic
/-- The preorder structure of `α →o β` is pointwise inequality: `f ≤ g ↔ ∀ a, f a ≤ g a`.  -/
OrderHom.instPreorder : {α : Type u_2} → {β : Type u_3} → [inst : Preorder α] → [inst_1 : Preorder β] → Preorder (α →o β)
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.mono : ∀ {X Z : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Z) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f],
  CategoryTheory.Mono f
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair_inverse_map : ∀ {X Y : CategoryTheory.Limits.WalkingParallelPair} (h : X ⟶ Y),
  CategoryTheory.Limits.walkingParallelFamilyEquivWalkingParallelPair.inverse.map h =
    CategoryTheory.Limits.parallelPair.parallelPairHom
      (CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := true })
      (CategoryTheory.Limits.WalkingParallelFamily.Hom.line { down := false }) h
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalLeftAction.monoidalOppositeLeftAction_actionObj : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c : Cᴹᵒᵖ) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d =
    CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c.unmop
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.radius_ne_top_iff : ∀ {α : Type u_1} {G : SimpleGraph α} [Nonempty α] [Finite α], G.radius ≠ ⊤ ↔ G.Connected
-- Lean.Setup
Lean.ModuleHeader.mk : Array Lean.Import → Bool → Lean.ModuleHeader
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
/-- Bijection between `MulOpposite` of a subsemiring `S` and its opposite.  -/
Subsemiring.mopRingEquivOp : {R : Type u_2} → [inst : NonAssocSemiring R] → (S : Subsemiring R) → (↥S)ᵐᵒᵖ ≃+* ↥S.op
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.hom_ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {W : C}
  {φ₁ φ₂ : W ⟶ CategoryTheory.ChosenPullbacksAlong.pullbackObj f g},
  φ₁ = φ₂ ↔
    CategoryTheory.CategoryStruct.comp φ₁ (CategoryTheory.ChosenPullbacksAlong.fst f g) =
        CategoryTheory.CategoryStruct.comp φ₂ (CategoryTheory.ChosenPullbacksAlong.fst f g) ∧
      CategoryTheory.CategoryStruct.comp φ₁ (CategoryTheory.ChosenPullbacksAlong.snd f g) =
        CategoryTheory.CategoryStruct.comp φ₂ (CategoryTheory.ChosenPullbacksAlong.snd f g)
-- Mathlib.Logic.Basic
imp_congr_eq : ∀ {a b c d : Prop}, a = c → b = d → (a → b) = (c → d)
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.instMulDistribMulAction : {G : Type u_3} → [inst : Group G] → MulDistribMulAction (ConjAct G) G
-- Lean.PrettyPrinter.Delaborator.Builtins
/-- A structure that records details of a function parameter.
 -/
Lean.PrettyPrinter.Delaborator.ParamKind : Type
-- Mathlib.Topology.EMetricSpace.Weak
/-- `ℕ∞` is a weak extended metric space with its usual distance function.  -/
instWeakEMetricSpaceENat : WeakEMetricSpace ℕ∞
-- Batteries.Data.String.Lemmas
String.offsetOfPosAux_of_valid : ∀ (l m r : List Char) (n : ℕ),
  String.Pos.Raw.offsetOfPosAux (String.ofList (l ++ m ++ r)) { byteIdx := String.utf8Len l + String.utf8Len m }
      { byteIdx := String.utf8Len l } n =
    n + m.length
-- Init.Data.Int.DivMod.Lemmas
Int.lt_of_mul_lt_mul_left : ∀ {a b c : ℤ}, a * b < a * c → 0 ≤ a → b < c
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
/-- A commutative domain that is an integral algebra over a field is a field.  -/
isField_of_isIntegral_of_isField' : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [IsDomain S] [inst_3 : Algebra R S]
  [Algebra.IsIntegral R S], IsField R → IsField S
-- Mathlib.Data.Fintype.Defs
/-- Elaborate set builder notation for `Finset`.

* `{x | p x}` is elaborated as `Finset.filter (fun x ↦ p x) Finset.univ` if the expected type is
  `Finset ?α`.
* `{x : α | p x}` is elaborated as `Finset.filter (fun x : α ↦ p x) Finset.univ` if the expected
  type is `Finset ?α`.
* `{x ∉ s | p x}` is elaborated as `Finset.filter (fun x ↦ p x) sᶜ` if either the expected type is
  `Finset ?α` or the expected type is not `Set ?α` and `s` has expected type `Finset ?α`.
* `{x ≠ a | p x}` is elaborated as `Finset.filter (fun x ↦ p x) {a}ᶜ` if the expected type is
  `Finset ?α`.

See also
* `Data.Set.Defs` for the `Set` builder notation elaborator that this elaborator partly overrides.
* `Data.Finset.Basic` for the `Finset` builder notation elaborator partly overriding this one for
  syntax of the form `{x ∈ s | p x}`.
* `Data.Fintype.Basic` for the `Finset` builder notation elaborator handling syntax of the form
  `{x | p x}`, `{x : α | p x}`, `{x ∉ s | p x}`, `{x ≠ a | p x}`.
* `Order.LocallyFinite.Basic` for the `Finset` builder notation elaborator handling syntax of the
  form `{x ≤ a | p x}`, `{x ≥ a | p x}`, `{x < a | p x}`, `{x > a | p x}`.
 -/
Mathlib.Meta.elabFinsetBuilderSetOf : Lean.Elab.Term.TermElab
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
AffineEquiv.midpoint_pointReflection_right : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P), midpoint R y ((AffineEquiv.pointReflection R x) y) = x
-- Mathlib.MeasureTheory.Integral.Average
MeasureTheory.measure_smul_average : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  (μ : MeasureTheory.Measure α) [MeasureTheory.IsFiniteMeasure μ] (f : α → E),
  μ.real Set.univ • ⨍ (x : α), f x ∂μ = ∫ (x : α), f x ∂μ
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.map_lt_map_iff_of_injective : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  [inst_6 : RingHomSurjective σ₁₂] {f : M →ₛₗ[σ₁₂] M₂},
  Function.Injective ⇑f → ∀ {p q : Submodule R M}, Submodule.map f p < Submodule.map f q ↔ p < q
-- Mathlib.Algebra.MonoidAlgebra.Basic
AddMonoidAlgebra.algebraMap_def : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_7} [inst : AddCommMonoid M] [inst_1 : CommSemiring R]
  [inst_2 : CommSemiring S] [inst_3 : Algebra R S],
  algebraMap (AddMonoidAlgebra R M) (AddMonoidAlgebra S M) = AddMonoidAlgebra.mapRingHom M (algebraMap R S)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.spanningCoe_inj : ∀ {V : Type u} {G : SimpleGraph V} {G₁ G₂ : G.Subgraph}, G₁.spanningCoe = G₂.spanningCoe ↔ G₁.Adj = G₂.Adj
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.CasesTypes.insert : Lean.Meta.Grind.CasesTypes → Lean.Name → Bool → Lean.Meta.Grind.CasesTypes