mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Grade
/-- Lifts a graded order along a strictly monotone function.  -/
GradeBoundedOrder.liftLeft : {𝕆 : Type u_1} →
  {ℙ : Type u_2} →
    {α : Type u_3} →
      [inst : Preorder 𝕆] →
        [inst_1 : Preorder ℙ] →
          [inst_2 : Preorder α] →
            [GradeBoundedOrder 𝕆 α] →
              (f : 𝕆 → ℙ) →
                StrictMono f →
                  (∀ (a b : 𝕆), a ⋖ b → f a ⋖ f b) →
                    (∀ (a : 𝕆), IsMin a → IsMin (f a)) → (∀ (a : 𝕆), IsMax a → IsMax (f a)) → GradeBoundedOrder ℙ α
-- Mathlib.Analysis.Normed.Affine.AddTorsor
nndist_midpoint_midpoint_le : ∀ {V : Type u_1} [inst : SeminormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] (p₁ p₂ p₃ p₄ : V),
  nndist (midpoint ℝ p₁ p₂) (midpoint ℝ p₃ p₄) ≤ (nndist p₁ p₃ + nndist p₂ p₄) / 2
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_modifyKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (k : α) (f : β k → β k)
  (l : List ((a : α) × β a)), (Std.Internal.List.modifyKey k f l).length = l.length
-- Mathlib.Analysis.Normed.Order.Hom.Basic
/-- Constructs a `NormedAddCommGroup` structure from an `AddGroupNormClass` on an
`AddCommGroup`.  -/
AddGroupNormClass.toNormedAddCommGroup : {F : Type u_1} →
  {α : Type u_2} →
    [inst : FunLike F α ℝ] → [inst_1 : AddCommGroup α] → [AddGroupNormClass F α ℝ] → F → NormedAddCommGroup α
-- Mathlib.MeasureTheory.Function.LpOrder
MeasureTheory.MemLp.inf : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : ENNReal}
  [inst : NormedAddCommGroup E] [inst_1 : Lattice E] [HasSolidNorm E] [IsOrderedAddMonoid E] {f g : α → E},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp g p μ → MeasureTheory.MemLp (f ⊓ g) p μ
-- Mathlib.CategoryTheory.SmallObject.Iteration.Nonempty
CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem_obj : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {Φ : CategoryTheory.SmallObject.SuccStruct C}
  {J : Type u} [inst_1 : LinearOrder J] [inst_2 : OrderBot J] [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J]
  [inst_5 : CategoryTheory.Limits.HasIterationOfShape J C] {j : J} (iter : (i : J) → i < j → Φ.Iteration i)
  (i : ↑(Set.Iio j)),
  (CategoryTheory.SmallObject.SuccStruct.Iteration.mkOfLimit.inductiveSystem iter).obj i = (iter ↑i ⋯).F.obj ⟨↑i, ⋯⟩
-- Mathlib.RingTheory.Extension.Cotangent.Basic
LinearEquiv.baseChange.eq_1 : ∀ (R : Type u_1) (A : Type u_2) (M : Type u_4) (N : Type u_5) [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R N] (e : M ≃ₗ[R] N),
  LinearEquiv.baseChange R A M N e = TensorProduct.AlgebraTensorModule.congr (LinearEquiv.refl A A) e
-- Mathlib.Tactic.Simps.Basic
/-- The `simps` attribute.  -/
simpsAttr : Lean.ParametricAttribute (Array Lean.Name)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.AbelianImages
/-- If a functor preserves kernels and cokernels, it preserves abelian coimages.  -/
CategoryTheory.Abelian.PreservesCoimage.iso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] →
            (F : CategoryTheory.Functor C D) →
              [F.PreservesZeroMorphisms] →
                {X Y : C} →
                  (f : X ⟶ Y) →
                    [inst_5 : CategoryTheory.Limits.HasKernel f] →
                      [inst_6 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] →
                        [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f 0) F] →
                          [CategoryTheory.Limits.PreservesColimit
                                (CategoryTheory.Limits.parallelPair (CategoryTheory.Limits.kernel.ι f) 0) F] →
                            [inst_9 : CategoryTheory.Limits.HasKernel (F.map f)] →
                              [inst_10 : CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι (F.map f))] →
                                F.obj (CategoryTheory.Abelian.coimage f) ≅ CategoryTheory.Abelian.coimage (F.map f)
-- Mathlib.Algebra.Homology.Embedding.TruncGE
HomologicalComplex.truncGE'Map_id : ∀ {ι : 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'],
  HomologicalComplex.truncGE'Map (CategoryTheory.CategoryStruct.id K) e =
    CategoryTheory.CategoryStruct.id (K.truncGE' e)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
_private.Init.Data.Iterators.Lemmas.Consumers.Loop.0.Std.Iter.forIn'_eq_match_step.match_3.eq_3 : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] {it : Std.Iter β} (motive : it.Step → Sort u_2)
  (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.Iter β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.Iter β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Init.Data.Array.MapIdx
Array.mapIdx_eq_zipIdx_map : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : ℕ → α → β},
  Array.mapIdx f xs =
    Array.map
      (fun x =>
        match x with
        | (a, i) => f i a)
      xs.zipIdx
-- Init.Data.List.BasicAux
/-- Returns the element at the provided index, counting from `0`. Returns `fallback` if the index is out
of bounds.

To return an `Option` depending on whether the index is in bounds, use `as[i]?`. To panic if the
index is out of bounds, use `as[i]!`.

Examples:
 * `["spring", "summer", "fall", "winter"].getD 2 "never" = "fall"`
 * `["spring", "summer", "fall", "winter"].getD 0 "never" = "spring"`
 * `["spring", "summer", "fall", "winter"].getD 4 "never" = "never"`
 -/
List.getD : {α : Type u_1} → List α → ℕ → α → α
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.Scheme.Hom.finite_appTop : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsAffine Y] [AlgebraicGeometry.IsFinite f],
  (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.appTop f)).Finite
-- Init.Data.Array.Find
Array.idxOf_le_size : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {xs : Array α} {a : α}, Array.idxOf a xs ≤ xs.size
-- Mathlib.Algebra.Module.Lattice
Module.Basis.extendOfIsLattice_apply : ∀ {R : Type u_1} [inst : CommRing R] (K : Type u_2) [inst_1 : Field K] [inst_2 : Algebra R K] {V : Type u_3}
  [inst_3 : AddCommGroup V] [inst_4 : Module K V] [inst_5 : Module R V] [inst_6 : IsScalarTower R K V]
  [inst_7 : IsFractionRing R K] {κ : Type u_4} {M : Submodule R V} [inst_8 : Submodule.IsLattice K M]
  (b : Module.Basis κ R ↥M) (k : κ), (Module.Basis.extendOfIsLattice K b) k = ↑(b k)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.inl_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y Z : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryCoproduct W X] [inst_2 : CategoryTheory.Limits.HasBinaryCoproduct Y Z]
  (f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C} (h : Y ⨿ Z ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coprod.map f g) h) =
    CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.coprod.inl h)
-- Mathlib.Topology.Compactness.CountablyCompact
/-- A topological space is countably compact if every countably generated proper filter has a
cluster point.  -/
CountablyCompactSpace : (E : Type u_4) → [TopologicalSpace E] → Prop
-- Mathlib.Algebra.Order.Sub.Defs
tsub_tsub_tsub_le_tsub : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftMono α], c - a - (c - b) ≤ b - a
-- Mathlib.Data.Rat.Cast.Order
NNRat.natCast_le_cast : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {m : ℕ} {n : ℚ≥0},
  ↑m ≤ ↑n ↔ ↑m ≤ n
-- Init.Data.UInt.Lemmas
UInt32.sub_lt : ∀ {a b : UInt32}, 0 < b → b ≤ a → a - b < a
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKeyD_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, (t₁ \ t₂).getKeyD k fallback = if k ∈ t₂ then fallback else t₁.getKeyD k fallback
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.isToIntTerm : Lean.Expr → Lean.Meta.Grind.GoalM Bool
-- Mathlib.Data.Set.Restrict
Set.MapsTo.range_restrict : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (s : Set α) (t : Set β) (h : Set.MapsTo f s t),
  Set.range (Set.MapsTo.restrict f s t h) = Subtype.val ⁻¹' f '' s
-- Mathlib.FieldTheory.IntermediateField.Basic
AlgHom.fieldRange_toSubalgebra : ∀ {K : Type u_1} {L : Type u_2} {L' : Type u_3} [inst : Field K] [inst_1 : Field L] [inst_2 : Field L']
  [inst_3 : Algebra K L] [inst_4 : Algebra K L'] (f : L →ₐ[K] L'), f.fieldRange.toSubalgebra = f.range
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.Hom.mk : {R : Type u} → [inst : CommRing R] → {A B : CommHopfAlgCat R} → (↑A →ₐc[R] ↑B) → A.Hom B
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.Indep.ssubset_ground : ∀ {α : Type u_1} {M : Matroid α} {I : Set α} [h : M✶.RankPos], M.Indep I → I ⊂ M.E
-- Lean.Log
/-- The `MonadLog` interface for logging error messages.
 -/
Lean.MonadLog : (Type → Type) → Type
-- Init.Data.List.Zip
List.zipWithAll_replicate : ∀ {α : Type u_1} {β : Type u_2} {α_1 : Type u_3} {f : Option α → Option β → α_1} {a : α} {b : β} {n : ℕ},
  List.zipWithAll f (List.replicate n a) (List.replicate n b) = List.replicate n (f (some a) (some b))
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.mul_omega0 : ∀ {a : Ordinal.{u}}, 0 < a → a < Ordinal.omega0 → a * Ordinal.omega0 = Ordinal.omega0
-- Mathlib.Algebra.Order.Monoid.Defs
one_le_mul_self_iff : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : LinearOrder α] [IsOrderedMonoid α] {a : α}, 1 ≤ a * a ↔ 1 ≤ a
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instIsRightCancelAdd : ∀ {α : Type u_1} [inst : Add α] [IsLeftCancelAdd α], IsRightCancelAdd αᵃᵒᵖ
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag_one : ∀ {m : Type u_2} {o : Type u_4} {α : Type u_12} [inst : Zero α] [inst_1 : DecidableEq o] [inst_2 : DecidableEq m]
  [inst_3 : One α], Matrix.blockDiag 1 = 1
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.coe_nsmul : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] (r : ℕ)
  (f : NormedAddGroupHom V₁ V₂), ⇑(r • f) = r • ⇑f
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.mem_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.LawfulEqCmp cmp] [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, k ∈ t.toList ↔ k ∈ t
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedTheoremGuard : Inhabited Lean.Meta.Grind.TheoremGuard
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileSystemWatcher.change : ℕ
-- Mathlib.FieldTheory.Minpoly.ConjRootClass
ConjRootClass.rootSet_minpoly_eq_carrier : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [Algebra.IsAlgebraic K L]
  (c : ConjRootClass K L), c.minpoly.rootSet L = c.carrier
-- Aesop.Tree.Data.ForwardRuleMatches
/-- Get the safe rules corresponding to the safe rule matches.  -/
Aesop.ForwardRuleMatches.safeRules : Aesop.ForwardRuleMatches → Array Aesop.SafeRule
-- Lean.Meta.MatchUtil
/-- Return `some (α, lhs)` if `e` is of the form `@Eq α lhs rhs` or `@HEq α lhs β rhs`
 -/
Lean.Meta.matchEqHEqLHS? : Lean.Expr → Lean.MetaM (Option (Lean.Expr × Lean.Expr))
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between a vector and a positive multiple of a vector.  -/
InnerProductGeometry.angle_smul_right_of_pos : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V) {r : ℝ},
  0 < r → InnerProductGeometry.angle x (r • y) = InnerProductGeometry.angle x y
-- Mathlib.LinearAlgebra.Span.Basic
/-- If `R` is "smaller" ring than `S` then the span by `R` is smaller than the span by `S`.  -/
Submodule.span_le_restrictScalars : ∀ (R : Type u_1) {M : Type u_4} (S : Type u_7) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (s : Set M) [inst_3 : Semiring S] [inst_4 : SMul R S] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M],
  Submodule.span R s ≤ Submodule.restrictScalars R (Submodule.span S s)
-- Lean.Meta.Instances
_private.Lean.Meta.Instances.0.Lean.Meta.computeSynthOrder.getSemiOutParamPositionsOf : Lean.Expr → Lean.MetaM (Array ℕ)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} (h : k ∈ Std.ExtDTreeMap.filterMap f t),
  (f (t.getKey k ⋯) (Std.ExtDTreeMap.Const.get t k ⋯)).isSome = true
-- Mathlib.GroupTheory.Submonoid.Center
AddSubmonoid.center_pi : ∀ {ι : Type u_2} {M : ι → Type u_3} [inst : (i : ι) → AddZeroClass (M i)],
  AddSubmonoid.center ((i : ι) → M i) = AddSubmonoid.pi Set.univ fun i => AddSubmonoid.center (M i)
-- Mathlib.RingTheory.Ideal.Maps
Ideal.map_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {T : Type u_3} [inst_2 : Semiring T] {I : Ideal R}
  (f : R →+* S) (g : S →+* T), Ideal.map g (Ideal.map f I) = Ideal.map (g.comp f) I
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coprod_inl_inr : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace M]
  [inst_2 : TopologicalSpace N] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : ContinuousAdd M]
  [inst_6 : AddCommMonoid N] [inst_7 : Module R N] [inst_8 : ContinuousAdd N],
  (ContinuousLinearMap.inl R M N).coprod (ContinuousLinearMap.inr R M N) = ContinuousLinearMap.id R (M × N)
-- Init.Data.Int.Order
Int.nonneg_of_mul_nonpos_left : ∀ {a b : ℤ}, a * b ≤ 0 → b < 0 → 0 ≤ a
-- Mathlib.Data.ZMod.Basic
/-- The coercions are respectively `Int.cast`, `ZMod.cast`, and `ZMod.cast`.  -/
ZMod.intCast_comp_cast : ∀ {n : ℕ} (R : Type u_1) [inst : Ring R], Int.cast ∘ ZMod.cast = ZMod.cast
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.notInLink : Lean.Doc.Parser.InlineCtxt → Lean.Parser.ParserFn
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
OrderedFinpartition.extendMiddle_length : ∀ {n : ℕ} (c : OrderedFinpartition n) (k : Fin c.length), (c.extendMiddle k).length = c.length
-- Mathlib.MeasureTheory.Measure.Trim
MeasureTheory.ae_eq_of_ae_eq_trim : ∀ {α : Type u_1} {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_3} {hm : m ≤ m0} {f₁ f₂ : α → E},
  f₁ =ᵐ[μ.trim hm] f₂ → f₁ =ᵐ[μ] f₂
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.coe_toEquiv : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (f : M ≃+ N), ⇑↑f = ⇑f
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Signature.mk.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {name : Lean.Name} {levelParams : List Lean.Name} {type : Lean.Expr}
  {params : Array (Lean.Compiler.LCNF.Param pu)} {safe : Bool} {name_1 : Lean.Name} {levelParams_1 : List Lean.Name}
  {type_1 : Lean.Expr} {params_1 : Array (Lean.Compiler.LCNF.Param pu)} {safe_1 : Bool},
  { name := name, levelParams := levelParams, type := type, params := params, safe := safe } =
      { name := name_1, levelParams := levelParams_1, type := type_1, params := params_1, safe := safe_1 } →
    name = name_1 ∧ levelParams = levelParams_1 ∧ type = type_1 ∧ params = params_1 ∧ safe = safe_1
-- Mathlib.Analysis.Convex.Between
affineSegment_const_vadd_image : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] (x y : P) (v : V),
  (fun x => v +ᵥ x) '' affineSegment R x y = affineSegment R (v +ᵥ x) (v +ᵥ y)
-- Mathlib.Order.Cofinal
isCofinal_range_of_strictMono : ∀ {α : Type u_1} [inst : LinearOrder α] [WellFoundedLT α] {f : α → α}, StrictMono f → IsCofinal (Set.range f)
-- Mathlib.Data.Multiset.MapFold
/-- `foldl f H b s` is the lift of the list operation `foldl f b l`,
which folds `f` over the multiset. It is well defined when `f` is right-commutative,
that is, `f (f b a₁) a₂ = f (f b a₂) a₁`.  -/
Multiset.foldl : {α : Type u_1} → {β : Type v} → (f : β → α → β) → [RightCommutative f] → β → Multiset α → β
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.natCoe_one : ∀ {R : Type u_1} [inst : AddMonoidWithOne R], ↑1 = 1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.size_alter_eq_sub_one : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      k ∈ t →
        (f (Std.DTreeMap.Raw.Const.get? t k)).isNone = true → (Std.DTreeMap.Raw.Const.alter t k f).size = t.size - 1
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_add_le : ∀ (r s : ENNReal), ⌈r + s⌉ₑ ≤ ⌈r⌉ₑ + ⌈s⌉ₑ
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.functor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (S : CategoryTheory.Sieve X) (Y : Cᵒᵖ),
  S.functor.obj Y = { g // S.arrows g }
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.mk'_sub : ∀ {R : Type u_1} [inst : CommRing R] {M : Submonoid R} (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S] (x₁ x₂ : R) (y₁ y₂ : ↥M),
  IsLocalization.mk' S (x₁ * ↑y₂ - x₂ * ↑y₁) (y₁ * y₂) = IsLocalization.mk' S x₁ y₁ - IsLocalization.mk' S x₂ y₂
-- Mathlib.Analysis.Convex.Between
/-- Lift a `Wbtw` predicate from one ring to another along a scalar tower.  -/
Wbtw.lift : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [ZeroLEOneClass R] {R' : Type u_6} [inst_6 : Ring R']
  [inst_7 : PartialOrder R'] [inst_8 : Module R' V] [inst_9 : Module R' R] [IsScalarTower R' R V] [SMulPosMono R' R]
  {x y z : P}, Wbtw R' x y z → Wbtw R x y z
-- Mathlib.Data.TypeVec
_private.Mathlib.Data.TypeVec.0.TypeVec.subtypeVal.match_1.eq_1 : ∀ (motive : (x : ℕ) → (x_1 : TypeVec.{u_1} x) → x_1.Arrow (TypeVec.repeat x Prop) → Fin2 x → Sort u_2) (n : ℕ)
  (x : TypeVec.{u_1} n.succ) (x_1 : x.Arrow (TypeVec.repeat n.succ Prop)) (i : Fin2 n)
  (h_1 :
    (n : ℕ) →
      (x : TypeVec.{u_1} n.succ) →
        (x_2 : x.Arrow (TypeVec.repeat n.succ Prop)) → (i : Fin2 n) → motive n.succ x x_2 i.fs)
  (h_2 :
    (n : ℕ) → (x : TypeVec.{u_1} n.succ) → (x_2 : x.Arrow (TypeVec.repeat n.succ Prop)) → motive n.succ x x_2 Fin2.fz),
  (match n.succ, x, x_1, i.fs with
    | n.succ, x, x_2, i.fs => h_1 n x x_2 i
    | n.succ, x, x_2, Fin2.fz => h_2 n x x_2) =
    h_1 n x x_1 i
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefIdent.instFromJson : Lean.FromJson Lean.Lsp.RefIdent
-- Mathlib.LinearAlgebra.Matrix.WithConv
instCommRingWithConvMatrix : {m : Type u_1} → {n : Type u_2} → {α : Type u_3} → [CommRing α] → CommRing (WithConv (Matrix m n α))
-- Mathlib.Data.Finsupp.Weight
Finsupp.le_degree : ∀ {σ : Type u_1} {R : Type u_5} [inst : AddCommMonoid R] [inst_1 : PartialOrder R] [CanonicallyOrderedAdd R] (s : σ)
  (f : σ →₀ R), f s ≤ Finsupp.degree f
-- Std.Internal.Do.WP.Basic
Std.Internal.Do.WP.wp_consequence_econs : ∀ {Pred : Type u_1} {EPred : Type u_2} {Prog : Type u} {Value : Type v} [inst : Std.Internal.Do.Assertion Pred]
  [inst_1 : Std.Internal.Do.Assertion EPred] [inst_2 : Std.Internal.Do.WP Prog Value Pred EPred] (x : Prog)
  (post post' : Value → Pred) (epost epost' : EPred),
  Lean.Order.PartialOrder.rel post post' →
    Lean.Order.PartialOrder.rel epost epost' →
      Lean.Order.PartialOrder.rel (Std.Internal.Do.wp x post epost) (Std.Internal.Do.wp x post' epost')
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Formula.iExs.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u'} (β : Type v') [inst : Finite β] (φ : L.Formula (α ⊕ β)),
  FirstOrder.Language.Formula.iExs β φ =
    (FirstOrder.Language.BoundedFormula.relabel (fun a => Sum.map id (⇑(Classical.choice ⋯)) a) φ).exs
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.Perm.sum_eq : ∀ {M : Type u_4} [inst : AddCommMonoid M] {l₁ l₂ : List M}, l₁.Perm l₂ → l₁.sum = l₂.sum
-- Mathlib.Geometry.Convex.Hull
Convexity.subset_convexHull_self : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {s : Set X}, s ⊆ (Convexity.convexHull R) s
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.Balanced.setBlack : ∀ {α : Type u_1} {t : RBTree.RBNode α} {c : RBTree.RBColor} {n : ℕ},
  t.Balanced c n → ∃ n', t.setBlack.Balanced RBTree.RBColor.black n'
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (t t_1 : Std.TreeMap.Raw α β cmp) (e_t : t = t_1) (a a_1 : α)
  (e_a : a = a_1) (h : a ∈ t), t.getKey a h = t_1.getKey a_1 ⋯
-- Mathlib.LinearAlgebra.AffineSpace.Pointwise
AffineSubspace.smul_span : ∀ {M : Type u_1} {k : Type u_2} {V : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : DistribSMul M V] [inst_4 : SMulCommClass M k V] (a : M) (s : Set V),
  a • affineSpan k s = affineSpan k (a • s)
-- Mathlib.CategoryTheory.Functor.Basic
/-- Notation for composition of functors.  -/
CategoryTheory.«term_⋙_» : Lean.TrailingParserDescr
-- Std.Time.Time.Unit.Nanosecond
Std.Time.Nanosecond.instDecidableLeOrdinal : {x y : Std.Time.Nanosecond.Ordinal} → Decidable (x ≤ y)
-- Mathlib.Geometry.Convex.Star
Convexity.IsStarConvexSet.univ : ∀ {R : Type u_1} {X : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R X] {x : X}, Convexity.IsStarConvexSet R x Set.univ
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.equiv_iff_keys_unit_perm : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m₁ m₂ : Std.DHashMap.Raw α fun x => Unit}, m₁.Equiv m₂ ↔ m₁.keys.Perm m₂.keys
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.toFinset_inter : ∀ {α : Type u} {s t : Set α} [inst : DecidableEq α] (hs : s.Finite) (ht : t.Finite) (h : (s ∩ t).Finite),
  h.toFinset = hs.toFinset ∩ ht.toFinset
-- Mathlib.Data.Int.Bitwise
Int.shiftLeft_sub : ∀ (m : ℤ) (n : ℕ) (k : ℤ), m <<< (↑n - k) = m <<< ↑n >>> k
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get!_alter : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h : t.WF) {k k' : α} [inst_1 : Inhabited (β k')] {f : Option (β k) → Option (β k)},
  (Std.DTreeMap.Internal.Impl.alter k f t ⋯).impl.get! k' =
    if heq : compare k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).get! else t.get! k'
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.isEmpty.eq_1 : ∀ {α : Type u_1} {cmp : α → α → Ordering} (property : RBTree.RBNode.WF cmp RBTree.RBNode.nil),
  RBTree.RBSet.isEmpty ⟨RBTree.RBNode.nil, property⟩ = true
-- Mathlib.Data.Nat.Digits.Lemmas
_private.Mathlib.Data.Nat.Digits.Lemmas.0.List.alternatingSum.match_1.eq_2 : ∀ {G : Type u_1} (motive : List G → Sort u_2) (g : G) (h_1 : Unit → motive []) (h_2 : (g : G) → motive [g])
  (h_3 : (g h : G) → (t : List G) → motive (g :: h :: t)),
  (match [g] with
    | [] => h_1 ()
    | [g] => h_2 g
    | g :: h :: t => h_3 g h t) =
    h_2 g
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.mem_roots' : ∀ {R : Type u} {a : R} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R}, a ∈ p.roots ↔ p ≠ 0 ∧ p.IsRoot a