mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.map_over_assoc : ∀ {n : Type u} {S T : AlgebraicGeometry.Scheme} (f : S ⟶ T) {Z : AlgebraicGeometry.Scheme} (h : T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.map n f)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace n T ↘ T) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace n S ↘ S) (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.natDegree_cubic : ∀ {R : Type u} {a b c d : R} [inst : Semiring R],
  a ≠ 0 →
    (Polynomial.C a * Polynomial.X ^ 3 + Polynomial.C b * Polynomial.X ^ 2 + Polynomial.C c * Polynomial.X +
          Polynomial.C d).natDegree =
      3
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.InjectiveInfo.mk.sizeOf_spec : ∀ (us : List Lean.Level) (α β h : Lean.Expr) (inv? : Option (Lean.Expr × Lean.Expr)),
  sizeOf { us := us, α := α, β := β, h := h, inv? := inv? } =
    1 + sizeOf us + sizeOf α + sizeOf β + sizeOf h + sizeOf inv?
-- Mathlib.Order.LiminfLimsup
Filter.limsInf_le_limsInf_of_le : ∀ {α : Type u_1} [inst : ConditionallyCompleteLattice α] {f g : Filter α},
  g ≤ f →
    autoParam (Filter.IsBounded (fun x1 x2 => x1 ≥ x2) f) Filter.limsInf_le_limsInf_of_le._auto_1 →
      autoParam (Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) g) Filter.limsInf_le_limsInf_of_le._auto_3 →
        f.limsInf ≤ g.limsInf
-- Init.Data.Array.Basic
/-- Returns the last element of an array, or `none` if the array is empty.

See `Array.back!` for the version that panics if the array is empty, or `Array.back` for the version
that requires a proof the array is non-empty.
 -/
Array.back? : {α : Type u} → Array α → Option α
-- Mathlib.Order.Antisymmetrization
antisymmRel_comm : ∀ {α : Type u_1} {a b : α} {r : α → α → Prop}, AntisymmRel r a b ↔ AntisymmRel r b a
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- **Alias** of `Topology.RelCWComplex.finite_of_finiteDimensional_finiteType`. -/
Topology.CWComplex.finite_of_finiteDimensional_finiteType : ∀ {X : Type u_1} [inst : TopologicalSpace X] (C : Set X) {D : Set X} [inst_1 : Topology.RelCWComplex C D]
  [Topology.RelCWComplex.FiniteDimensional C] [Topology.RelCWComplex.FiniteType C], Topology.RelCWComplex.Finite C
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.IsStrongLimit.isSuccPrelimit : ∀ {c : Cardinal.{u_1}}, c.IsStrongLimit → Order.IsSuccPrelimit c
-- Mathlib.Algebra.Homology.HomotopyCategory.KInjective
CochainComplex.isKInjective_shift_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (L : CochainComplex C ℤ) (n : ℤ),
  ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj L).IsKInjective ↔ L.IsKInjective
-- Mathlib.Algebra.Ring.Hom.Defs
RingHomClass.toMonoidHomClass : ∀ {F : Type u_5} {α : outParam (Type u_6)} {β : outParam (Type u_7)} {inst : NonAssocSemiring α}
  {inst_1 : NonAssocSemiring β} {inst_2 : FunLike F α β} [self : RingHomClass F α β], MonoidHomClass F α β
-- Mathlib.Topology.DenseEmbedding
/-- The product of two dense inducings is a dense inducing  -/
IsDenseInducing.prodMap : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] [inst_3 : TopologicalSpace δ] {e₁ : α → β} {e₂ : γ → δ},
  IsDenseInducing e₁ → IsDenseInducing e₂ → IsDenseInducing (Prod.map e₁ e₂)
-- Mathlib.GroupTheory.RegularWreathProduct
/-- The encoding of the Sylow `p`-subgroups of `Perm α` as an iterated wreath product.  -/
Sylow.mulEquivIteratedWreathProduct : (p : ℕ) →
  [hp : Fact (Nat.Prime p)] →
    (n : ℕ) →
      (α : Type u_3) →
        [Finite α] →
          Nat.card α = p ^ n →
            (G : Type u_4) →
              [inst : Group G] →
                [Finite G] → Nat.card G = p → (P : Sylow p (Equiv.Perm α)) → ↥↑P ≃* IteratedWreathProduct G n
-- Batteries.Data.String.Lemmas
String.data_join : ∀ (ss : List String), (String.join ss).toList = (List.map String.toList ss).flatten
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.continuousWithinAt : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) {S : Set A} {a : A}, ContinuousWithinAt (⇑e) S a
-- Mathlib.Combinatorics.Quiver.Arborescence
/-- The root of the arborescence.  -/
Quiver.Arborescence.root : {V : Type u} → {inst : Quiver V} → [self : Quiver.Arborescence V] → V
-- Mathlib.Algebra.GroupWithZero.Associated
Associated.dvdNotUnit_left : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] {p q r : M}, DvdNotUnit p r → Associated p q → DvdNotUnit q r
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- If `t : Cocone F` is a colimit cocone, then `t.op : Cone F.op` is a limit cone.
 -/
CategoryTheory.Limits.IsColimit.op : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          {t : CategoryTheory.Limits.Cocone F} → CategoryTheory.Limits.IsColimit t → CategoryTheory.Limits.IsLimit t.op
-- Mathlib.Data.List.Basic
List.mem_pair : ∀ {α : Type u} {a b c : α}, a ∈ [b, c] ↔ a = b ∨ a = c
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- Two morphisms into a universal `S`-costructured arrow are equal if their image under `S` are
equal after postcomposing the universal arrow.  -/
CategoryTheory.CostructuredArrow.IsUniversal.hom_ext : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D} {f : CategoryTheory.CostructuredArrow S T} (h : f.IsUniversal) {c : C}
  {η η' : c ⟶ f.left},
  CategoryTheory.CategoryStruct.comp (S.map η) f.hom = CategoryTheory.CategoryStruct.comp (S.map η') f.hom → η = η'
-- Init.Tactics
/-- `next => tac` focuses on the next goal and solves it using `tac`, or else fails.
`next x₁ ... xₙ => tac` additionally renames the `n` most recent hypotheses with
inaccessible names to the given names.
 -/
Lean.Parser.Tactic.«tacticNext_=>_» : Lean.ParserDescr
-- Mathlib.Analysis.Polynomial.MahlerMeasure
/-- If the leading coefficient of a polynomial has norm at least 1, then its Mahler measure
is at least 1. This holds in particular for nonzero polynomials with integer coefficients,
since their leading coefficient is a nonzero integer.  -/
Polynomial.one_le_mahlerMeasure_of_one_le_norm_leadingCoeff : ∀ {p : Polynomial ℂ}, 1 ≤ ‖p.leadingCoeff‖ → 1 ≤ p.mahlerMeasure
-- Mathlib.RingTheory.SimpleModule.Isotypic
eq_isotypicComponent_of_le : ∀ {R : Type u_2} {M : Type u} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S c : Submodule R M},
  c ∈ isotypicComponents R M → ∀ [IsSimpleModule R ↥S], S ≤ c → c = isotypicComponent R M ↥S
-- Mathlib.NumberTheory.SumTwoSquares
/-- If the integer `n` is a sum of two squares of coprime integers,
then `-1` is a square modulo `n`.  -/
ZMod.isSquare_neg_one_of_eq_sq_add_sq_of_isCoprime : ∀ {n x y : ℤ}, n = x ^ 2 + y ^ 2 → IsCoprime x y → IsSquare (-1)
-- Mathlib.Algebra.MvPolynomial.Nilpotent
MvPolynomial.instIsLocalHomRingHomC : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R], IsLocalHom MvPolynomial.C
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The obvious homotopy from `nullHomotopicMap K` to zero.  -/
HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopy : {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] → Homotopy (HomologicalComplex.cylinder.πCompι₀Homotopy.nullHomotopicMap K) 0
-- Mathlib.AlgebraicGeometry.Cover.QuasiCompact
/-- [Stacks Tag 022D](https://stacks.math.columbia.edu/tag/022D) ((2)) -/
AlgebraicGeometry.QuasiCompactCover.instBindScheme : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : CategoryTheory.PreZeroHypercover X) [AlgebraicGeometry.QuasiCompactCover 𝒰]
  (f : (x : 𝒰.I₀) → CategoryTheory.PreZeroHypercover (𝒰.X x)) [∀ (x : 𝒰.I₀), AlgebraicGeometry.QuasiCompactCover (f x)],
  AlgebraicGeometry.QuasiCompactCover (𝒰.bind f)
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableUniformly.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] (f : ι → β → α) [inst_1 : UniformSpace α],
  SummableUniformly f = Summable (⇑UniformFun.ofFun ∘ f)
-- Mathlib.Topology.Order.MonotoneConvergence
Pi.supConvergenceClass : ∀ {ι : Type u_3} {α : ι → Type u_4} [inst : (i : ι) → Preorder (α i)] [inst_1 : (i : ι) → TopologicalSpace (α i)]
  [∀ (i : ι), SupConvergenceClass (α i)], SupConvergenceClass ((i : ι) → α i)
-- Mathlib.MeasureTheory.Measure.SeparableMeasure
MeasureTheory.instIsSeparableNullMeasurableSpaceCompletion : ∀ {X : Type u_1} [m : MeasurableSpace X] (μ : MeasureTheory.Measure X) [hμ : MeasureTheory.IsSeparable μ],
  MeasureTheory.IsSeparable μ.completion
-- Mathlib.Algebra.Group.Subgroup.Ker
AddSubgroup.map_eq_range_iff : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] {f : G →+ N} {H : AddSubgroup G},
  AddSubgroup.map f H = f.range ↔ Codisjoint H f.ker
-- Mathlib.Order.Max
IsBot.eq_1 : ∀ {α : Type u_1} [inst : LE α] (a : α), IsBot a = ∀ (b : α), a ≤ b
-- Mathlib.Algebra.Order.Module.Defs
smul_le_smul_iff_of_pos_right : ∀ {α : Type u_1} {β : Type u_2} {a₁ a₂ : α} {b : β} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β]
  [inst_3 : Zero β] [SMulPosMono α β] [SMulPosReflectLE α β], 0 < b → (a₁ • b ≤ a₂ • b ↔ a₁ ≤ a₂)
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.fst_equivOfRightInverse : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_3} [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {M₂ : Type u_4} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommGroup M₂] [inst_6 : Module R M₂]
  [inst_7 : IsTopologicalAddGroup M] (f₁ : M →L[R] M₂) (f₂ : M₂ →L[R] M) (h : Function.RightInverse ⇑f₂ ⇑f₁) (x : M),
  ((ContinuousLinearEquiv.equivOfRightInverse f₁ f₂ h) x).1 = f₁ x
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanIndex.multiforkEquivPiForkOfIsLimit_counitIso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MulticospanShape}
  (I : CategoryTheory.Limits.MulticospanIndex J C) {c : CategoryTheory.Limits.Fan I.left}
  (hc : CategoryTheory.Limits.IsLimit c) {d : CategoryTheory.Limits.Fan I.right} (hd : CategoryTheory.Limits.IsLimit d),
  (I.multiforkEquivPiForkOfIsLimit hc hd).counitIso =
    CategoryTheory.NatIso.ofComponents
      (fun K =>
        CategoryTheory.Limits.Fork.ext
          (CategoryTheory.Iso.refl (((I.ofPiForkFunctor hd).comp (I.toPiForkFunctor hc hd)).obj K).pt) ⋯)
      ⋯
-- Mathlib.RingTheory.HahnSeries.HEval
HahnSeries.SummableFamily.support_powerSeriesFamily_subset : ∀ {Γ : Type u_1} {R : Type u_3} {V : Type u_4} [inst : AddCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : CommRing R] [inst_4 : CommRing V] [inst_5 : Algebra R V]
  {x : HahnSeries Γ V} (a b : PowerSeries R) (g : Γ),
  ((HahnSeries.SummableFamily.powerSeriesFamily x (a * b)).coeff g).support ⊆
    Finset.image (fun i => i.1 + i.2)
      (((HahnSeries.SummableFamily.powerSeriesFamily x a).mul (HahnSeries.SummableFamily.powerSeriesFamily x b)).coeff
          g).support
-- Mathlib.Order.Fin.Tuple
RelIso.mk.congr_simp : ∀ {α : Type u_5} {β : Type u_6} {r : α → α → Prop} {s : β → β → Prop} (toEquiv toEquiv_1 : α ≃ β)
  (e_toEquiv : toEquiv = toEquiv_1) (map_rel_iff' : ∀ {a b : α}, s (toEquiv a) (toEquiv b) ↔ r a b),
  { toEquiv := toEquiv, map_rel_iff' := map_rel_iff' } = { toEquiv := toEquiv_1, map_rel_iff' := ⋯ }
-- Init.Data.UInt.Bitwise
UInt64.zero_shiftRight : ∀ {a : UInt64}, 0 >>> a = 0
-- Init.Grind.ToIntLemmas
Lean.Grind.ToInt.div_congr : ∀ {α : Type u_1} {i : Lean.Grind.IntInterval} [inst : Lean.Grind.ToInt α i] [inst_1 : Div α] [Lean.Grind.ToInt.Div α i]
  {a b : α} {a' b' : ℤ}, ↑a = a' → ↑b = b' → ↑(a / b) = a' / b'
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.indexAt : {R : Type u_1} →
  {B : Type u_2} →
    {F : Type u_3} →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] → [inst_3 : TopologicalSpace B] → {ι : Type u_5} → VectorBundleCore R B F ι → B → ι
-- Mathlib.Geometry.Euclidean.Simplex
Affine.Triangle.acuteAngled_iff_angle_lt : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {t : Affine.Triangle ℝ P},
  Affine.Simplex.AcuteAngled t ↔
    EuclideanGeometry.angle (t.points 0) (t.points 1) (t.points 2) < Real.pi / 2 ∧
      EuclideanGeometry.angle (t.points 1) (t.points 2) (t.points 0) < Real.pi / 2 ∧
        EuclideanGeometry.angle (t.points 2) (t.points 0) (t.points 1) < Real.pi / 2
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁.eq_1 : ∀ {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.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)],
  CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst (hf₁.fst' f₂) (hf₁.fst' f₃)) (hf₁.fst' f₂)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_insertEntry : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l : List ((a : α) × β a)} {k a : α}
  {fallback : β a} {v : β k},
  Std.Internal.List.getValueCastD a (Std.Internal.List.insertEntry k v l) fallback =
    if h : (k == a) = true then cast ⋯ v else Std.Internal.List.getValueCastD a l fallback
-- Mathlib.RingTheory.Congruence.Hom
RingCon.comapQuotientEquivOfSurj_mk : ∀ {M : Type u_1} {N : Type u_2} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring N] (c : RingCon M) {f : N →+* M}
  (hf : Function.Surjective ⇑f) {d : RingCon N} (hcd : d = c.comap f) (x : N),
  (c.comapQuotientEquivOfSurj f hf hcd) ↑x = ↑(f x)
-- Lean.Elab.ConfigEval.DeriveEvalExpr
Lean.Elab.ConfigEval.EvalExpr.withSimpleEvalExpr : {α : Type} → Lean.Name → (String → Array Lean.Expr → Lean.MetaM α) → Lean.Expr → Lean.MetaM α
-- Lean.Meta.Tactic.Ext
Lean.Meta.Ext.instInhabitedExtTheorems.default : Lean.Meta.Ext.ExtTheorems
-- Mathlib.Algebra.Module.Submodule.Lattice
Submodule.add_mem_sup : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {S T : Submodule R M} {s t : M}, s ∈ S → t ∈ T → s + t ∈ S ⊔ T
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.hom_inv_id_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C),
  CategoryTheory.CategoryStruct.comp (α.hom.app X) (α.inv.app X) = CategoryTheory.CategoryStruct.id (F.obj X)
-- Init.Data.String.Length
Nat.repeat.eq_1 : ∀ {α : Type u} (f : α → α) (x : α), Nat.repeat f 0 x = x
-- Mathlib.Algebra.Free
FreeSemigroup.pure_seq : ∀ {α β : Type u} {f : α → β} {x : FreeSemigroup α}, pure f <*> x = f <$> x
-- Mathlib.Order.Filter.Defs
Filter.instFunctor : Functor Filter
-- Init.Data.Slice.Lemmas
Std.Slice.Internal.foldl_iter : ∀ {γ : Type u} {α β : Type v} {δ : Type u_1} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  [inst_2 : Std.IteratorLoop α Id Id] {s : Std.Slice γ} {init : δ} {f : δ → β → δ},
  Std.Iter.fold f init (Std.Slice.Internal.iter s) = Std.Slice.foldl f init s
-- Lean.ReducibilityAttrs
Lean.ReducibilityStatus.reducible : Lean.ReducibilityStatus
-- Mathlib.Data.Finsupp.Basic
Finsupp.filter_eq_self_iff : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (p : α → Prop) [inst_1 : DecidablePred p] (f : α →₀ M),
  Finsupp.filter p f = f ↔ ∀ (x : α), f x ≠ 0 → p x
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instSMulWithZero : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : Zero β] →
          {R : Type u_2} →
            [inst_3 : Zero R] →
              [inst_4 : SMulWithZero R β] → [ContinuousConstSMul R β] → SMulWithZero R (ZeroAtInftyContinuousMap α β)
-- Mathlib.Order.BourbakiWitt
/-- `cSup` is an upper bound of the nonempty chain  -/
ChainCompletePartialOrder.le_cSup : ∀ {α : Type u_4} [self : ChainCompletePartialOrder α] (c : NonemptyChain α),
  ∀ x ∈ c.carrier, x ≤ ChainCompletePartialOrder.cSup c
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.discrete_isNormal : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C], CategoryTheory.Subgroupoid.discrete.IsNormal
-- Mathlib.Order.Hom.Basic
/-- An order isomorphism is an equivalence such that `a ≤ b ↔ (f a) ≤ (f b)`.
This definition is an abbreviation of `RelIso (≤) (≤)`.  -/
OrderIso : (α : Type u_6) → (β : Type u_7) → [LE α] → [LE β] → Type (max u_6 u_7)
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.AffineOpenCover.openCover_I₀ : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.AffineOpenCover), 𝒰.openCover.I₀ = 𝒰.I₀
-- Mathlib.MeasureTheory.Measure.EverywherePos
/-- The everywhere positive subset of a set is obtained by removing an open set.  -/
MeasureTheory.Measure.exists_isOpen_everywherePosSubset_eq_sdiff : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α) (s : Set α),
  ∃ u, IsOpen u ∧ μ.everywherePosSubset s = s \ u
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instAddAction.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {M : Type u_5} [inst : AddMonoid M] [inst_1 : AddAction M β],
  Filter.Germ.instAddAction = { toVAdd := Filter.Germ.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Data.Set.Image
Set.preimage_range_inter : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {s : Set β}, f ⁻¹' (Set.range f ∩ s) = f ⁻¹' s
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.im_zero : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} [inst : Zero R], QuaternionAlgebra.im 0 = 0
-- Mathlib.Combinatorics.SimpleGraph.Sum
/-- Get coloring of `G` from coloring of `G ⊕g H`  -/
SimpleGraph.Coloring.sumLeft : {V : Type u_3} →
  {W : Type u_5} → {γ : Type u_7} → {G : SimpleGraph V} → {H : SimpleGraph W} → (G ⊕g H).Coloring γ → G.Coloring γ
-- Mathlib.NumberTheory.RamificationInertia.Ramification
/-- **Alias** of `Ideal.ramificationIdx'_eq_find`. -/
Ideal.ramificationIdx_eq_find : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  [inst_3 : DecidablePred fun n => ∀ (k : ℕ), Ideal.map (algebraMap R S) p ≤ P ^ k → k ≤ n]
  (h : ∃ n, ∀ (k : ℕ), Ideal.map (algebraMap R S) p ≤ P ^ k → k ≤ n), p.ramificationIdx' P = Nat.find h
-- Mathlib.Order.Filter.NAry
Filter.map_uncurry_prod : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} (m : α → β → γ) (f : Filter α) (g : Filter β),
  Filter.map (Function.uncurry m) (f ×ˢ g) = Filter.map₂ m f g
-- Mathlib.Algebra.Group.Defs
/-- Raising to the power of a natural number.  -/
NPow.npow : {M : Type u} → [self : NPow M] → ℕ → M → M
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_trailingCoeff : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R), p.mirror.trailingCoeff = p.leadingCoeff
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticParsedSnapshot.brecOn_3.go : {motive_1 : Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
  {motive_2 :
      Lean.Language.TransformedSnap (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
        Sort u} →
    {motive_3 : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
      {motive_4 : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
        {motive_5 : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
          {motive_6 : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) → Sort u} →
            {motive_7 : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
              {motive_8 : Task Lean.Elab.Tactic.TacticParsedSnapshot → Sort u} →
                (t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
                  ((t : Lean.Elab.Tactic.TacticParsedSnapshot) → t.below → motive_1 t) →
                    ((t :
                          Lean.Language.TransformedSnap
                            (Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot)) →
                        Lean.Elab.Tactic.TacticParsedSnapshot.below_1 t → motive_2 t) →
                      ((t : Array (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                          Lean.Elab.Tactic.TacticParsedSnapshot.below_2 t → motive_3 t) →
                        ((t : Lean.Elab.Tactic.TacticParsedSnapshotInner Lean.Elab.Tactic.TacticParsedSnapshot) →
                            Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t → motive_4 t) →
                          ((t : List (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                              Lean.Elab.Tactic.TacticParsedSnapshot.below_4 t → motive_5 t) →
                            ((t : Option (Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot)) →
                                Lean.Elab.Tactic.TacticParsedSnapshot.below_5 t → motive_6 t) →
                              ((t : Lean.Language.SnapshotTask Lean.Elab.Tactic.TacticParsedSnapshot) →
                                  Lean.Elab.Tactic.TacticParsedSnapshot.below_6 t → motive_7 t) →
                                ((t : Task Lean.Elab.Tactic.TacticParsedSnapshot) →
                                    Lean.Elab.Tactic.TacticParsedSnapshot.below_7 t → motive_8 t) →
                                  motive_4 t ×' Lean.Elab.Tactic.TacticParsedSnapshot.below_3 t
-- Mathlib.Data.Multiset.ZeroCons
Multiset.le_cons_of_notMem : ∀ {α : Type u_1} {s t : Multiset α} {a : α}, a ∉ s → (s ≤ a ::ₘ t ↔ s ≤ t)
-- Mathlib.Analysis.LocallyConvex.WeakDual
LinearMap.weakBilin_withSeminorms : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : AddCommGroup F] [inst_4 : Module 𝕜 F] (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜), WithSeminorms B.toSeminormFamily
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearMap.map_sub₂ : ∀ {R : Type u_1} {𝕜₂ : Type u_3} {𝕜₃ : Type u_4} {E : Type u_5} {F : Type u_6} {G : Type u_7} [inst : Semiring R]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] [inst_3 : AddCommGroup E] [inst_4 : Module R E]
  [inst_5 : TopologicalSpace E] [inst_6 : AddCommGroup F] [inst_7 : Module 𝕜₂ F] [inst_8 : TopologicalSpace F]
  [inst_9 : AddCommGroup G] [inst_10 : Module 𝕜₃ G] [inst_11 : TopologicalSpace G] [inst_12 : IsTopologicalAddGroup G]
  [inst_13 : ContinuousConstSMul 𝕜₃ G] {σ₁₃ : R →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃} (f : E →SL[σ₁₃] F →SL[σ₂₃] G) (x x' : E)
  (y : F), (f (x - x')) y = (f x) y - (f x') y
-- Mathlib.Data.Prod.TProd
_private.Mathlib.Data.Prod.TProd.0.Set.tprod.match_1.splitter : {ι : Type u_1} →
  {α : ι → Type u_2} →
    (motive : List ι → ((i : ι) → Set (α i)) → Sort u_3) →
      (x : List ι) →
        (x_1 : (i : ι) → Set (α i)) →
          ((x : (i : ι) → Set (α i)) → motive [] x) →
            ((i : ι) → (is : List ι) → (t : (i : ι) → Set (α i)) → motive (i :: is) t) → motive x x_1
-- Mathlib.Order.UpperLower.Principal
UpperSet.Ici_le_Ioi : ∀ {α : Type u_1} [inst : Preorder α] (a : α), UpperSet.Ici a ≤ UpperSet.Ioi a
-- Init.Data.Fin.Basic
/-- The predecessor of a non-zero element of `Fin (n+1)`, with the bound decreased.

Examples:
* `(4 : Fin 8).pred (by decide) = (3 : Fin 7)`
* `(1 : Fin 2).pred (by decide) = (0 : Fin 1)`
 -/
Fin.pred : {n : ℕ} → (i : Fin (n + 1)) → i ≠ 0 → Fin n