mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.SmallObject.WellOrderInductionData
CategoryTheory.Functor.WellOrderInductionData.Extension.map_limit : ∀ {J : Type u} [inst : LinearOrder J] [inst_1 : SuccOrder J] {F : CategoryTheory.Functor Jᵒᵖ (Type v)}
  {d : F.WellOrderInductionData} [inst_2 : OrderBot J] {val₀ : F.obj (Opposite.op ⊥)} {j : J}
  (self : d.Extension val₀ j) (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j),
  (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE hij).op)) self.val =
    d.lift i hi
      ⟨fun x =>
        match x with
        | Opposite.op ⟨k, hk⟩ => (CategoryTheory.ConcreteCategory.hom (F.map (CategoryTheory.homOfLE ⋯).op)) self.val,
        ⋯⟩
-- Batteries.Control.LawfulMonadState
LawfulMonadStateOf.set_bind_map_get : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} [inst : Monad m] [inst_1 : MonadStateOf σ m] [LawfulMonadStateOf σ m]
  {α : Type u_1} (f : σ → α) (s : σ),
  (do
      set s
      f <$> get) =
    do
    set s
    pure (f s)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.AffineScheme.instIsEquivalenceOppositeCommRingCatOpRightOpΓ : AlgebraicGeometry.AffineScheme.Γ.rightOp.op.IsEquivalence
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapLeftIso_unitIso_inv_app_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (R : CategoryTheory.Functor B T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {L₁ L₂ : CategoryTheory.Functor A T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : L₁ ≅ L₂) (X : CategoryTheory.MorphismProperty.Comma L₁ R P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapLeftIso R e).unitIso.inv.app X).left =
    CategoryTheory.CategoryStruct.id X.left
-- Mathlib.Data.Complex.Basic
Complex.ofReal_nnratCast : ∀ (q : ℚ≥0), ↑↑q = ↑q
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- `PreservesColimitsOfSize.{v u} F` means that `F` sends all colimit cocones over any
diagram `J ⥤ C` to colimit cocones, where `J : Type u` with `[Category.{v} J]`.  -/
CategoryTheory.Limits.PreservesColimitsOfSize : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor C D → Prop
-- Mathlib.Algebra.Group.Subgroup.Basic
Group.conjugates_subset_normal : ∀ {G : Type u_1} [inst : Group G] {N : Subgroup G} [tn : N.Normal] {a : G}, a ∈ N → conjugatesOf a ⊆ ↑N
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.inv_zero' : ∀ (K : Type u_3) [inst : Field K] {R₁ : Type u_4} [inst_1 : CommRing R₁] [inst_2 : IsDomain R₁] [inst_3 : Algebra R₁ K]
  [inst_4 : IsFractionRing R₁ K], 0⁻¹ = 0
-- Mathlib.Algebra.Star.SelfAdjoint
/-- **Alias** of the forward direction of `Pi.isSelfAdjoint`. -/
IsSelfAdjoint.apply : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Star (α i)] {f : (i : ι) → α i},
  IsSelfAdjoint f → ∀ (i : ι), IsSelfAdjoint (f i)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.RightExactFunctor.forget_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : C ⥤ᵣ D), (CategoryTheory.RightExactFunctor.forget C D).obj F = F.obj
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.ext_of_ring_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : CoalgebraStruct R A] {f g : R →ₐc[R] A}, f = g ↔ f 1 = g 1
-- Lean.Util.InstantiateLevelParams
/-- Instantiate universe level parameters names `paramNames` with `lvls` in `e`.
If the two lists have different length, the smallest one is used.
 -/
Lean.Expr.instantiateLevelParams : Lean.Expr → List Lean.Name → List Lean.Level → Lean.Expr
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.addDeclCheck : Lean.Environment →
  USize → USize → Lean.Declaration → Option IO.CancelToken → Except Lean.Kernel.Exception Lean.Environment
-- Mathlib.RingTheory.LaurentSeries
RatFunc.coe_X : ∀ {F : Type u} [inst : Field F], (algebraMap (RatFunc F) (LaurentSeries F)) RatFunc.X = (HahnSeries.single 1) 1
-- Mathlib.Topology.Order.LowerUpperTopology
/-- Type synonym for a preorder equipped with the lower set topology.  -/
Topology.WithLower : Type u_1 → Type u_1
-- Lean.Meta.TryThis
Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax.injEq : ∀ {kind : Lean.SyntaxNodeKind} (a : Lean.TSyntax kind) (kind_1 : Lean.SyntaxNodeKind) (a_1 : Lean.TSyntax kind_1),
  (Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax a = Lean.Meta.Tactic.TryThis.SuggestionText.tsyntax a_1) =
    (kind = kind_1 ∧ a ≍ a_1)
-- Mathlib.Data.Analysis.Filter
Filter.Realizer.mem_sets : ∀ {α : Type u_1} {f : Filter α} (F : f.Realizer) {a : Set α}, a ∈ f ↔ ∃ b, F.F.f b ⊆ a
-- Mathlib.Topology.EMetricSpace.Defs
/-- Two points coincide if their distance is `< ε` for all positive ε  -/
eq_of_forall_edist_le : ∀ {γ : Type w} [inst : EMetricSpace γ] {x y : γ}, (∀ ε > 0, edist x y ≤ ε) → x = y
-- Mathlib.NumberTheory.FLT.Three
/-- We have that `λ ^ (3*S.multiplicity-2)` divides `S.a + S.b`.  -/
_private.Mathlib.NumberTheory.FLT.Three.0.FermatLastTheoremForThreeGen.Solution.lambda_pow_dvd_a_add_b : ∀ {K : Type u_1} [inst : Field K] {ζ : K} {hζ : IsPrimitiveRoot ζ 3} (S : FermatLastTheoremForThreeGen.Solution✝ hζ)
  [inst_1 : NumberField K] [IsCyclotomicExtension {3} ℚ K],
  (hζ.toInteger - 1) ^ (3 * FermatLastTheoremForThreeGen.Solution.multiplicity✝ S - 2) ∣
    FermatLastTheoremForThreeGen.Solution'.a✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S) +
      FermatLastTheoremForThreeGen.Solution'.b✝ (FermatLastTheoremForThreeGen.Solution.toSolution'✝ S)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
exists_maximal_algebraicIndependent : ∀ {R : Type u_2} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] (s t : Set A),
  s ⊆ t → AlgebraicIndepOn R id s → ∃ u, s ⊆ u ∧ Maximal (fun x => AlgebraicIndepOn R id x ∧ x ⊆ t) u
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The union of all closed cells equals `C`. Use `RelCWComplex.union` instead.  -/
Topology.RelCWComplex.union' : ∀ {X : Type u} {inst : TopologicalSpace X} {C : Set X} {D : outParam (Set X)} [self : Topology.RelCWComplex C D],
  D ∪ ⋃ n, ⋃ j, ↑(Topology.RelCWComplex.map n j) '' Metric.closedBall 0 1 = C
-- Mathlib.Data.Rat.Defs
Rat.natCast_div_eq_divInt : ∀ (n d : ℕ), ↑n / ↑d = Rat.divInt ↑n ↑d
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Atom.mk.injEq : ∀ (e : Lean.Expr) (src tgt : Mathlib.Tactic.BicategoryLike.Mor₁) (e_1 : Lean.Expr)
  (src_1 tgt_1 : Mathlib.Tactic.BicategoryLike.Mor₁),
  ({ e := e, src := src, tgt := tgt } = { e := e_1, src := src_1, tgt := tgt_1 }) =
    (e = e_1 ∧ src = src_1 ∧ tgt = tgt_1)
-- Init.Prelude
/-- Gets the end position information from a `SourceInfo`, if available.
If `canonicalOnly` is true, then `.synthetic` syntax with `canonical := false`
will also return `none`.
 -/
Lean.SourceInfo.getTailPos? : Lean.SourceInfo → optParam Bool false → Option String.Pos.Raw
-- Mathlib.Analysis.SpecificLimits.Normed
/-- `v (1 / (1 + a ^n))` tends to `1` for all `v : AbsoluteValue R S` for fields `R` and `S`,
provided `v a < 1`.  -/
AbsoluteValue.tendsto_div_one_add_pow_nhds_one : ∀ {R : Type u_2} {S : Type u_3} [inst : Field R] [inst_1 : Field S] [inst_2 : LinearOrder S]
  [inst_3 : TopologicalSpace S] [IsStrictOrderedRing S] [Archimedean S] [_i : OrderTopology S] {v : AbsoluteValue R S}
  {a : R}, v a < 1 → Filter.Tendsto (fun n => v (1 / (1 + a ^ n))) Filter.atTop (nhds 1)
-- Mathlib.Algebra.Module.Injective
Module.Injective.of_ringEquiv : ∀ {R : Type u} [inst : Ring R] [Small.{v, u} R] {S : Type u'} [inst_2 : Ring S] {M : Type v} {N : Type v'}
  [inst_3 : AddCommGroup M] [inst_4 : AddCommGroup N] [inst_5 : Module R M] [inst_6 : Module S N] (e₁ : R ≃+* S)
  (e₂ : M ≃ₛₗ[↑e₁] N) [inj : Module.Injective R M], Module.Injective S N
-- Std.Http.Data.Request
Std.Http.Request.Head.mk.sizeOf_spec : ∀ (method : Std.Http.Method) (version : Std.Http.Version) (uri : Std.Http.RequestTarget) (headers : Std.Http.Headers),
  sizeOf { method := method, version := version, uri := uri, headers := headers } =
    1 + sizeOf method + sizeOf version + sizeOf uri + sizeOf headers
-- Mathlib.Combinatorics.Graph.Simple
/-- A loopless graph is one where the ends of every edge are distinct.  -/
Graph.Loopless : {α : Type u_1} → {β : Type u_2} → Graph α β → Prop
-- Mathlib.CategoryTheory.IsConnected
/-- If there is a zigzag from `j₁` to `j₂`, then there is a zigzag from `F j₁` to
`F j₂` as long as `F` is a prefunctor.
 -/
CategoryTheory.zigzag_prefunctor_obj_of_zigzag : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {K : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} K]
  (F : J ⥤q K) {j₁ j₂ : J}, CategoryTheory.Zigzag j₁ j₂ → CategoryTheory.Zigzag (F.obj j₁) (F.obj j₂)
-- Mathlib.RingTheory.Etale.QuasiFinite
Ideal.fiberIsoOfBijectiveResidueField.congr_simp : ∀ {R : Type u_1} {R' : Type u_2} {S : Type u_3} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : CommRing S]
  [inst_3 : Algebra R R'] [inst_4 : Algebra R S] {p : Ideal R} {q : Ideal R'} [inst_5 : p.IsPrime] [inst_6 : q.IsPrime]
  [inst_7 : q.LiesOver p] (H : Function.Bijective ⇑(Ideal.ResidueField.mapₐ p q (Algebra.ofId R R') ⋯)),
  Ideal.fiberIsoOfBijectiveResidueField H = Ideal.fiberIsoOfBijectiveResidueField H
-- Init.Data.Range.Polymorphic.Iterators
/-- Internal function that constructs an iterator for a closed range `lo...*`.
This is an internal function.
Use `Rcc.iter` instead, which requires
importing `Std.Data.Iterators`.
 -/
Std.Rci.Internal.iter : {α : Type u} → [Std.PRange.UpwardEnumerable α] → Std.Rci α → Std.Iter α
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_add_infinitePos : ∀ {x y : ℝ*}, x.InfinitePos → y.InfinitePos → (x + y).InfinitePos
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.Iio_add_one_eq_Iic_of_not_isMax : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrderBot α] [inst_3 : Add α]
  [SuccAddOrder α] {b : α}, ¬IsMax b → Finset.Iio (b + 1) = Finset.Iic b
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.piEquivPiSubtypeProd_apply : ∀ {δ' : Type u_5} (π : δ' → Type u_6) [inst : (x : δ') → MeasurableSpace (π x)] (p : δ' → Prop)
  [inst_1 : DecidablePred p], ⇑(MeasurableEquiv.piEquivPiSubtypeProd π p) = fun f => (fun x => f ↑x, fun x => f ↑x)
-- Init.Data.List.Zip
List.zip_map : ∀ {α : Type u_1} {γ : Type u_2} {β : Type u_3} {δ : Type u_4} {f : α → γ} {g : β → δ} {l₁ : List α} {l₂ : List β},
  (List.map f l₁).zip (List.map g l₂) = List.map (Prod.map f g) (l₁.zip l₂)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstr.brecOn.go : {motive_1 : Lean.Meta.Grind.Arith.Linear.EqCnstr → Sort u} →
  {motive_2 : Lean.Meta.Grind.Arith.Linear.EqCnstrProof → Sort u} →
    {motive_3 : Lean.Meta.Grind.Arith.Linear.IneqCnstr → Sort u} →
      {motive_4 : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof → Sort u} →
        {motive_5 : Lean.Meta.Grind.Arith.Linear.DiseqCnstr → Sort u} →
          {motive_6 : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof → Sort u} →
            {motive_7 : Lean.Meta.Grind.Arith.Linear.UnsatProof → Sort u} →
              (t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) →
                ((t : Lean.Meta.Grind.Arith.Linear.EqCnstr) → t.below → motive_1 t) →
                  ((t : Lean.Meta.Grind.Arith.Linear.EqCnstrProof) → t.below → motive_2 t) →
                    ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstr) → t.below → motive_3 t) →
                      ((t : Lean.Meta.Grind.Arith.Linear.IneqCnstrProof) → t.below → motive_4 t) →
                        ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstr) → t.below → motive_5 t) →
                          ((t : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof) → t.below → motive_6 t) →
                            ((t : Lean.Meta.Grind.Arith.Linear.UnsatProof) → t.below → motive_7 t) →
                              motive_5 t ×' t.below
-- Mathlib.Combinatorics.SimpleGraph.Copy
/-- A simple graph contains itself.  -/
SimpleGraph.IsContained.refl : ∀ {V : Type u_1} (G : SimpleGraph V), G.IsContained G
-- Init.Data.UInt.Lemmas
UInt64.toBitVec_toUInt16 : ∀ (n : UInt64), n.toUInt16.toBitVec = BitVec.setWidth 16 n.toBitVec
-- Mathlib.AlgebraicTopology.SimplicialSet.StdSimplex
/-- The functor `stdSimplex : SimplexCategory ⥤ SSet` is fully faithful.  -/
SSet.stdSimplex.fullyFaithful : CategoryTheory.Functor.FullyFaithful SSet.stdSimplex
-- Lean.Parser.Term
/-- Syntax for `.{u, ...}` itself. Generally the `explicitUniv` trailing parser suffices.
However, for `e |>.x.{u} a1 a2 a3` notation we need to be able to express explicit universes in the
middle of the syntax.  -/
Lean.Parser.Term.explicitUnivSuffix : Lean.Parser.Parser
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.keys_insertIfNew_perm : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [inst : BEq α] [Std.TransCmp cmp]
  [Std.LawfulBEqCmp cmp] {k : α} {v : β k}, (t.insertIfNew k v).keys.Perm (if k ∈ t then t.keys else k :: t.keys)
-- Mathlib.CategoryTheory.EqToHom
CategoryTheory.eqToHom.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {X Y : C} (p : X = Y),
  CategoryTheory.eqToHom p = CategoryTheory.eqToHom p
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The `v`-adic absolute value satisfies the ultrametric inequality.  -/
NumberField.HeightOneSpectrum.adicAbv_add_le_max : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (x y : K),
  (NumberField.HeightOneSpectrum.adicAbv K v) (x + y) ≤
    max ((NumberField.HeightOneSpectrum.adicAbv K v) x) ((NumberField.HeightOneSpectrum.adicAbv K v) y)
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.inclusion.congr_simp : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N N' : LieSubmodule R L M} (h : N ≤ N'),
  LieSubmodule.inclusion h = LieSubmodule.inclusion h
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
ContinuousMultilinearMap.fin0_apply_enorm : ∀ {𝕜 : Type u} {G : Type wG} {G' : Type wG'} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup G]
  [inst_2 : NormedSpace 𝕜 G] [inst_3 : NormedAddCommGroup G'] [inst_4 : NormedSpace 𝕜 G'] (f : G [×0]→L[𝕜] G')
  {x : Fin 0 → G}, ‖f x‖ₑ = ‖f‖ₑ
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.forget₂_commRingCat_map : ∀ {R : Type u} [inst : CommRing R] {A B : CommAlgCat R} (f : A ⟶ B),
  (CategoryTheory.forget₂ (CommAlgCat R) CommRingCat).map f = CommRingCat.ofHom ↑(CommAlgCat.Hom.hom f)
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.ulift_I₀ : ∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X), 𝒰.ulift.I₀ = ↥X
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.dropEndWhile_eq_self_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [String.Slice.Pattern.Model.StrictPatternModel pat] [inst_2 : String.Slice.Pattern.BackwardPattern pat]
  [String.Slice.Pattern.Model.LawfulBackwardPatternModel pat] {s : String.Slice},
  s.dropEndWhile pat = s ↔ s.endsWith pat = false
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instZero : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] → [Nonempty ι] → [(i : ι) → Zero (G i)] → Zero (DirectLimit G f)
-- Mathlib.Algebra.Order.Group.Cone
AddGroupCone.instSetLike.eq_1 : ∀ (G : Type u_1) [inst : AddCommGroup G], AddGroupCone.instSetLike G = { coe := fun C => C.carrier, coe_injective := ⋯ }
-- Init.Data.SInt.Lemmas
Int32.toInt_maxValue : Int32.maxValue.toInt = 2 ^ 31 - 1
-- Init.Grind.FieldNormNum
_private.Init.Grind.FieldNormNum.0.Lean.Grind.Field.NormNum.dvd_helper₁ : ∀ {z : ℤ} {n : ℕ}, ↑(z.natAbs.gcd n) ∣ z
-- Mathlib.GroupTheory.GroupExtension.Basic
/-- `N`-conjugacy is symmetric.  -/
AddGroupExtension.IsAddConj.symm : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  (S : AddGroupExtension N E G) {s₁ s₂ : S.Splitting}, S.IsAddConj s₁ s₂ → S.IsAddConj s₂ s₁
-- Mathlib.Analysis.Convex.Basic
/-- See `Convex.semilinear_image` for a version for semilinear maps, but requiring that `𝕜` be a
linear order, instead of just a partial order.  -/
Convex.linear_image : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid F] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] {s : Set E},
  Convex 𝕜 s → ∀ (f : E →ₗ[𝕜] F), Convex 𝕜 (⇑f '' s)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.zeroLocus_iInf_of_nonempty : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} {ι : Type u_1} (I : ι → Ideal ↑(X.presheaf.obj (Opposite.op U)))
  [Finite ι] [Nonempty ι], X.zeroLocus ↑(⨅ i, I i) = ⋃ i, X.zeroLocus ↑(I i)
-- Mathlib.Data.List.Permutation
List.map_map_permutationsAux2 : ∀ {α : Type u_1} {α' : Type u_3} (g : α → α') (t : α) (ts ys : List α),
  List.map (List.map g) (List.permutationsAux2 t ts [] ys id).2 =
    (List.permutationsAux2 (g t) (List.map g ts) [] (List.map g ys) id).2
-- Mathlib.Order.Basic
update_le_self_iff : ∀ {ι : Type u_1} {π : ι → Type u_4} [inst : DecidableEq ι] [inst_1 : (i : ι) → Preorder (π i)] {x : (i : ι) → π i}
  {i : ι} {a : π i}, Function.update x i a ≤ x ↔ a ≤ x i
-- Lean.Data.PersistentHashSet
Lean.PersistentHashSet.forIn : {α : Type u_1} →
  {m : Type u_2 → Type u_3} →
    {σ : Type u_2} →
      {x : BEq α} → {x_1 : Hashable α} → [Monad m] → Lean.PersistentHashSet α → σ → (α → σ → m (ForInStep σ)) → m σ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : β},
  Std.DTreeMap.Const.getD (t₁ ∩ t₂) k fallback = if k ∈ t₂ then Std.DTreeMap.Const.getD t₁ k fallback else fallback
-- Lean.Util.CollectLevelParams
Lean.CollectLevelParams.instInhabitedState : Inhabited Lean.CollectLevelParams.State
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.eq_of_empty : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Zero β] [IsEmpty α]
  (f g : CompactlySupportedContinuousMap α β), f = g
-- Mathlib.Geometry.Convex.ConvexSpace.AffineMap
Convexity.ConvexSpace.AffineMap.comp_id : ∀ {R : Type u_1} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R] {X : Type u_2}
  {Y : Type u_3} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y]
  (f : Convexity.ConvexSpace.AffineMap R X Y), f.comp (Convexity.ConvexSpace.AffineMap.id X) = f
-- Init.Data.UInt.Lemmas
UInt16.ofFin_div : ∀ (a b : Fin UInt16.size), UInt16.ofFin (a / b) = UInt16.ofFin a / UInt16.ofFin b
-- Mathlib.RingTheory.Spectrum.Prime.FreeLocus
Module.basicOpen_subset_freeLocus_iff : ∀ {R : Type uR} {M : Type uM} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.FinitePresentation R M] {f : R},
  ↑(PrimeSpectrum.basicOpen f) ⊆ Module.freeLocus R M ↔
    Module.Projective (Localization.Away f) (LocalizedModule.Away f M)
-- Mathlib.Topology.Sheaves.Presheaf
TopologicalSpace.Opens.mapIso.congr_simp : ∀ {X Y : TopCat} (f g : X ⟶ Y) (h : f = g), TopologicalSpace.Opens.mapIso f g h = TopologicalSpace.Opens.mapIso f g h
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeSet α cmp) (e_t : t = t_1)
  (a a_1 : α) (e_a : a = a_1) (h : a ∈ t), t.get a h = t_1.get a_1 ⋯
-- Mathlib.Combinatorics.Graph.Basic
/-- `G.IsNonloopAt e x` means that the vertex `x` is one but not both of the ends of the edge =`e`,
or equivalently that `e` is incident with `x` but not a loop at `x` -
see `Graph.isNonloopAt_iff_inc_not_isLoopAt`.  -/
Graph.IsNonloopAt : {α : Type u_1} → {β : Type u_2} → Graph α β → β → α → Prop
-- Lean.Data.Json.Basic
Lean.Json.null.sizeOf_spec : sizeOf Lean.Json.null = 1
-- Mathlib.AlgebraicGeometry.Stalk
AlgebraicGeometry.Scheme.Spec_stalkClosedPointTo_fromSpecStalk : ∀ {X : AlgebraicGeometry.Scheme} {R : CommRingCat} [inst : IsLocalRing ↑R] (f : AlgebraicGeometry.Spec R ⟶ X),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Spec.map (AlgebraicGeometry.Scheme.stalkClosedPointTo f))
      (X.fromSpecStalk (f (IsLocalRing.closedPoint ↑R))) =
    f
-- Std.Http.Data.Body.Stream
Std.Http.Body.instCoeResponseStreamAny : Coe (Std.Http.Response Std.Http.Body.Stream) (Std.Http.Response Std.Http.Body.Any)
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.Norm.Transitivity.eval_zero_comp_det : ∀ {R : Type u_1} {S : Type u_2} {n : Type u_4} {m : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  (M : Matrix m m S) [inst_2 : DecidableEq m] [inst_3 : DecidableEq n] (k : m) [inst_4 : Fintype m] [inst_5 : Fintype n]
  (f : S →+* Matrix n n R),
  Polynomial.eval 0
      ((Matrix.comp m m n n (Polynomial R)) ((Algebra.Norm.Transitivity.cornerAddX M k).map ⇑f.polyToMatrix)).det =
    ((Matrix.comp m m n n R) (M.map ⇑f)).det
-- Mathlib.Algebra.Homology.Embedding.TruncGEHomology
HomologicalComplex.truncGE'.hasHomology_sc'_of_not_mem_boundary : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncGE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i j k : ι), c.prev j = i → c.next j = k → ¬e.BoundaryGE j → ((K.truncGE' e).sc' i j k).HasHomology
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.mulLeft_symm : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul G G] (x : G),
  (IsometryEquiv.mulLeft x).symm = IsometryEquiv.mulLeft x⁻¹
-- Mathlib.Order.JordanHolder
CompositionSeries.last_eraseLast_le : ∀ {X : Type u} [inst : Lattice X] [inst_1 : JordanHolderLattice X] (s : CompositionSeries X),
  (RelSeries.eraseLast s).last ≤ RelSeries.last s
-- Mathlib.CategoryTheory.Limits.Final
CategoryTheory.Functor.Final.colimit_pre_isIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [inst_2 : F.Final] {E : Type u₃} [inst_3 : CategoryTheory.Category.{v₃, u₃} E]
  {G : CategoryTheory.Functor D E} [inst_4 : CategoryTheory.Limits.HasColimit G],
  CategoryTheory.IsIso (CategoryTheory.Limits.colimit.pre G F)
-- Mathlib.Order.InitialSeg
PrincipalSeg.le_apply_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a : α} {b : β} [inst_1 : PartialOrder α] (f : α <i β),
  b ≤ f.toRelEmbedding a ↔ ∃ c ≤ a, f.toRelEmbedding c = b
-- Lean.DocString.Parser
Lean.Doc.Parser.InList.mk.injEq : ∀ (indentation : ℕ) (type : Lean.Doc.Parser.OrderedListType ⊕ Lean.Doc.Parser.UnorderedListType) (indentation_1 : ℕ)
  (type_1 : Lean.Doc.Parser.OrderedListType ⊕ Lean.Doc.Parser.UnorderedListType),
  ({ indentation := indentation, type := type } = { indentation := indentation_1, type := type_1 }) =
    (indentation = indentation_1 ∧ type = type_1)
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.blsub_lt_ord_lift_of_isRegular : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {c : Cardinal.{max u v}},
  c.IsRegular → Cardinal.lift.{v, u} o.card < c → (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c.ord) → o.blsub f < c.ord