mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.String.Lemmas.Pattern.Split.Basic
_private.Init.Data.String.Lemmas.Pattern.Split.Basic.0.String.Slice.Pattern.Model.toList_splitToSubslice_eq_splitFromSteps : ∀ {ρ : Type} {pat : ρ} {σ : String.Slice → Type} [inst : String.Slice.Pattern.ToForwardSearcher pat σ]
  [inst_1 : (s : String.Slice) → Std.Iterator (σ s) Id (String.Slice.Pattern.SearchStep s)]
  [∀ (s : String.Slice), Std.Iterators.Finite (σ s) Id] (s : String.Slice),
  (s.splitToSubslice pat).toList =
    String.Slice.Pattern.Model.splitFromSteps✝ s.startPos
      (String.Slice.Pattern.ToForwardSearcher.toSearcher pat s).toList
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
HasProd.pow : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : β → α} {a : α}
  {L : SummationFilter β} [ContinuousMul α], HasProd f a L → ∀ (n : ℕ), HasProd (fun x => f x ^ n) (a ^ n) L
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.div : ∀ {f g : ℝ → ℝ},
  AkraBazziRecurrence.GrowsPolynomially f →
    AkraBazziRecurrence.GrowsPolynomially g → AkraBazziRecurrence.GrowsPolynomially fun x => f x / g x
-- Mathlib.Algebra.Group.Defs
inv_mul_cancel_left : ∀ {G : Type u_1} [inst : Group G] (a b : G), a⁻¹ * (a * b) = b
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- `homEquiv'` is the dual of `homEquiv`, which we need for `to_dual`.
Please avoid using this directly.  -/
CategoryTheory.Adjunction.homEquiv' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} → (G ⊣ F) → (X : C) → (Y : D) → (Y ⟶ F.obj X) ≃ (G.obj Y ⟶ X)
-- Mathlib.LinearAlgebra.CrossProduct
/-- Cyclic permutations preserve the triple product. See also `triple_product_eq_det`.  -/
triple_product_permutation : ∀ {R : Type u_1} [inst : CommRing R] (u v w : Fin 3 → R), u ⬝ᵥ (crossProduct v) w = v ⬝ᵥ (crossProduct w) u
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolution.uniqueUpToIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  {F G : CategoryTheory.Functor C V} (h h' : CategoryTheory.MonoidalCategory.DayConvolution F G),
  h.uniqueUpToIso h' =
    (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G).leftKanExtensionUnique
      (CategoryTheory.MonoidalCategory.DayConvolution.unit F G)
      (CategoryTheory.MonoidalCategory.DayConvolution.convolution F G)
      (CategoryTheory.MonoidalCategory.DayConvolution.unit F G)
-- Init.Data.Range.Polymorphic.RangeIterator
_private.Init.Data.Range.Polymorphic.RangeIterator.0.Std.Rxc.Iterator.step.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α] (it : Std.Iter α),
  Std.Rxc.Iterator.step it =
    match it.internalState.next with
    | none => Std.IterStep.done
    | some next =>
      if next ≤ it.internalState.upperBound then
        Std.IterStep.yield
          { internalState := { next := Std.PRange.succ? next, upperBound := it.internalState.upperBound } } next
      else Std.IterStep.done
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.Equiv.mk_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  {ρ : ContRepresentation R G V} {σ : ContRepresentation R G W} {e : V ≃L[R] W}
  (he : ∀ (g : G), ↑e ∘SL ρ g = σ g ∘SL ↑e) (v : V), (ContRepresentation.Equiv.mk e he) v = e v
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- A nonsingular Jacobian point on a Weierstrass curve `W`.  -/
WeierstrassCurve.Jacobian.Point : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → Type r
-- Mathlib.LinearAlgebra.SesquilinearForm.Basic
LinearMap.nondegenerate_congr_iff : ∀ {R : Type u_1} {M : Type u_5} {Mₗ₁ : Type u_9} {Mₗ₁' : Type u_10} {Mₗ₂ : Type u_11} {Mₗ₂' : Type u_12}
  [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : AddCommMonoid Mₗ₁]
  [inst_4 : AddCommMonoid Mₗ₂] [inst_5 : AddCommMonoid Mₗ₁'] [inst_6 : AddCommMonoid Mₗ₂'] [inst_7 : Module R Mₗ₁]
  [inst_8 : Module R Mₗ₂] [inst_9 : Module R Mₗ₁'] [inst_10 : Module R Mₗ₂'] {B : Mₗ₁ →ₗ[R] Mₗ₂ →ₗ[R] M}
  (e₁ : Mₗ₁ ≃ₗ[R] Mₗ₁') (e₂ : Mₗ₂ ≃ₗ[R] Mₗ₂'),
  ((e₁.arrowCongr (e₂.arrowCongr (LinearEquiv.refl R M))) B).Nondegenerate ↔ B.Nondegenerate
-- Mathlib.CategoryTheory.Triangulated.Functor
/-- `F.mapTriangle` commutes with the inverse of the rotation of triangles.  -/
CategoryTheory.Functor.mapTriangleInvRotateIso : {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] →
        [inst_2 : CategoryTheory.HasShift C ℤ] →
          [inst_3 : CategoryTheory.HasShift D ℤ] →
            (F : CategoryTheory.Functor C D) →
              [inst_4 : F.CommShift ℤ] →
                [inst_5 : CategoryTheory.Preadditive C] →
                  [inst_6 : CategoryTheory.Preadditive D] →
                    [F.Additive] →
                      F.mapTriangle.comp (CategoryTheory.Pretriangulated.invRotate D) ≅
                        (CategoryTheory.Pretriangulated.invRotate C).comp F.mapTriangle
-- Mathlib.CategoryTheory.RegularCategory.Basic
CategoryTheory.Regular.instHasCoequalizerFstSnd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Regular C] {X Y : C} (f : X ⟶ Y),
  CategoryTheory.Limits.HasCoequalizer (CategoryTheory.Limits.pullback.fst f f) (CategoryTheory.Limits.pullback.snd f f)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_union_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h₁ : m₁.WF)
  (h₂ : m₂.WF) {k : α},
  Std.DTreeMap.Internal.Impl.contains k (m₁.union m₂ ⋯ ⋯) = true ↔
    Std.DTreeMap.Internal.Impl.contains k m₁ = true ∨ Std.DTreeMap.Internal.Impl.contains k m₂ = true
-- Mathlib.Order.CompleteBooleanAlgebra
Pi.instCompletelyDistribLattice : {ι : Type u_1} →
  {π : ι → Type u_2} → [(i : ι) → CompletelyDistribLattice (π i)] → CompletelyDistribLattice ((i : ι) → π i)
-- Mathlib.Topology.Order.PartialSups
ContinuousOn.partialSups : ∀ {L : Type u_1} [inst : SemilatticeSup L] [inst_1 : TopologicalSpace L] [ContinuousSup L] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : ℕ → X → L} {n : ℕ} {s : Set X},
  (∀ k ≤ n, ContinuousOn (f k) s) → ContinuousOn ((partialSups f) n) s
-- Mathlib.Analysis.Normed.Algebra.GelfandMazur
/-- The key step in the proof: if `a` and `b` are real numbers minimizing `‖φ x (a, b)‖`,
and the minimal value is strictly positive, then the function `(s, t) ↦ ‖φ x (s, t)‖`
is constant.  -/
_private.Mathlib.Analysis.Normed.Algebra.GelfandMazur.0.NormedAlgebra.Real.norm_φ_eq_norm_φ_of_isMinOn : ∀ {F : Type u_1} [inst : NormedRing F] [inst_1 : NormedAlgebra ℝ F] [NormOneClass F] [NormMulClass F] {x : F}
  {z : ℝ × ℝ},
  IsMinOn (fun x_1 => ‖NormedAlgebra.Real.φ✝ x x_1‖) Set.univ z →
    ‖NormedAlgebra.Real.φ✝ x z‖ ≠ 0 → ∀ (w : ℝ × ℝ), ‖NormedAlgebra.Real.φ✝ x w‖ = ‖NormedAlgebra.Real.φ✝ x z‖
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.measurable_of_not_zero_le_restrict : ∀ {α : Type u_1} {m : MeasurableSpace α} {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] (v : MeasureTheory.VectorMeasure α M) {i : Set α},
  ¬MeasureTheory.VectorMeasure.restrict 0 i ≤ v.restrict i → MeasurableSet i
-- Init.Data.Vector.Int
Vector.sum_reverse_int : ∀ {n : ℕ} (xs : Vector ℤ n), xs.reverse.sum = xs.sum
-- Lean.Meta.Tactic.Grind.Types
/-- State for the `GrindM` monad.  -/
Lean.Meta.Grind.State : Type
-- Mathlib.AlgebraicGeometry.PointsPi
/-- If `V` is a locally closed subscheme of `Spec (Π Rᵢ)` containing `∐ Spec Rᵢ`, then
`V = Spec (Π Rᵢ)`.  -/
AlgebraicGeometry.isIso_of_comp_eq_sigmaSpec : ∀ {ι : Type u} (R : ι → CommRingCat) {V : AlgebraicGeometry.Scheme} (f : (∐ fun i => AlgebraicGeometry.Spec (R i)) ⟶ V)
  (g : V ⟶ AlgebraicGeometry.Spec (CommRingCat.of ((i : ι) → ↑(R i)))) [AlgebraicGeometry.IsImmersion g]
  [CompactSpace ↥V], CategoryTheory.CategoryStruct.comp f g = AlgebraicGeometry.sigmaSpec R → CategoryTheory.IsIso g
-- Lean.Elab.DeclNameGen
_private.Lean.Elab.DeclNameGen.0.Lean.Elab.Command.NameGen.mkBaseNameCore.visit'.match_3.eq_1 : ∀ (motive : Lean.Expr → Sort u_1) (name : Lean.Name) (us : List Lean.Level)
  (h_1 : (name : Lean.Name) → (us : List Lean.Level) → motive (Lean.Expr.const name us))
  (h_2 : (f x : Lean.Expr) → motive (f.app x))
  (h_3 :
    (binderName : Lean.Name) →
      (ty body : Lean.Expr) → (binderInfo : Lean.BinderInfo) → motive (Lean.Expr.forallE binderName ty body binderInfo))
  (h_4 : Unit → motive (Lean.Expr.sort Lean.Level.zero)) (h_5 : (a : Lean.Level) → motive (Lean.Expr.sort a.succ))
  (h_6 : (u : Lean.Level) → motive (Lean.Expr.sort u)) (h_7 : (x : Lean.Expr) → motive x),
  (match Lean.Expr.const name us with
    | Lean.Expr.const name us => h_1 name us
    | f.app x => h_2 f x
    | Lean.Expr.forallE binderName ty body binderInfo => h_3 binderName ty body binderInfo
    | Lean.Expr.sort Lean.Level.zero => h_4 ()
    | Lean.Expr.sort a.succ => h_5 a
    | Lean.Expr.sort u => h_6 u
    | x => h_7 x) =
    h_1 name us
-- Init.Data.Order.Ord
/-- A typeclass for types with an oriented comparison function: flipping the arguments amounts to
applying `Ordering.swap` to the return value.
 -/
Std.OrientedOrd : (α : Type u) → [Ord α] → Prop
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.subRight_apply : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddRightMono α] (a b : α), (OrderIso.subRight a) b = b - a
-- Mathlib.Analysis.Convex.Extreme
IsExtreme.extremePoints_subset_extremePoints : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A B : Set E}, IsExtreme 𝕜 A B → Set.extremePoints 𝕜 B ⊆ Set.extremePoints 𝕜 A
-- Mathlib.RingTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.inertiaDeg_smul`. -/
Ideal.inertiaDeg'_smul : ∀ (R : Type u_1) {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (q : Ideal S)
  {G : Type u_4} [inst_3 : Group G] [inst_4 : MulSemiringAction G S] [SMulCommClass G R S] (g : G),
  (g • q).inertiaDeg R = q.inertiaDeg R
-- Mathlib.Order.Minimal
exists_maximal_of_wellFoundedGT : ∀ {α : Type u_2} [inst : Preorder α] [WellFoundedGT α] (P : α → Prop), (∃ a, P a) → ∃ a, Maximal P a
-- Init.Data.UInt.Bitwise
UInt16.toFin_or : ∀ (a b : UInt16), (a ||| b).toFin = a.toFin ||| b.toFin
-- Lean.Elab.ConfigEval.Instances
Lean.Elab.ConfigEval.EvalExpr.instOption : {α : Type} → [Lean.Elab.ConfigEval.EvalExpr α] → Lean.Elab.ConfigEval.EvalExpr (Option α)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_smul : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {A : Type u_8} [inst_1 : SMulZeroClass A R] (a : A)
  (x : MonoidAlgebra R M), (a • x).coeff = a • x.coeff
-- Mathlib.LinearAlgebra.Matrix.ToLin
Module.Basis.end_repr_symm_apply : ∀ {R : Type u_1} {M : Type u_2} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Fintype ι] [inst_4 : DecidableEq ι] (b : Module.Basis ι R M) (a : ι × ι →₀ R),
  b.end.repr.symm a = (Matrix.toLin b b) ((Finsupp.linearCombination R ⇑(Matrix.stdBasis R ι ι)) a)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
/-- the morphism in the opposite direction between right adjoints  -/
CategoryTheory.Bicategory.Adj.Hom₂.τr : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : CategoryTheory.Bicategory.Adj B} → {α β : a ⟶ b} → CategoryTheory.Bicategory.Adj.Hom₂ α β → (β.r ⟶ α.r)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.cos_arccos : ∀ {x : ℝ}, -1 ≤ x → x ≤ 1 → Real.cos (Real.arccos x) = x
-- Aesop.RuleSet.Member
Aesop.GlobalRuleSetMember.base : Aesop.BaseRuleSetMember → Aesop.GlobalRuleSetMember
-- Init.Data.Order.Lemmas
Std.instTransLtOfLeOfLawfulOrderLT : {α : Type u} →
  [inst : LT α] →
    [inst_1 : LE α] →
      [Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2] →
        [Std.LawfulOrderLT α] → Trans (fun x1 x2 => x1 < x2) (fun x1 x2 => x1 < x2) fun x1 x2 => x1 < x2
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.contains_of_contains_filter : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [EquivBEq α] [LawfulHashable α]
  {f : (a : α) → β a → Bool} {k : α}, (Std.DHashMap.filter f m).contains k = true → m.contains k = true
-- Init.Data.BitVec.Lemmas
BitVec.ofFin_toFin : ∀ {w : ℕ} (x : BitVec w), { toFin := x.toFin } = x
-- Mathlib.Data.Finmap
/-- Look up the value associated to a key in a map.  -/
Finmap.lookup : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → Finmap β → Option (β a)
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_sub_right : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y z : F), inner 𝕜 x (y - z) = inner 𝕜 x y - inner 𝕜 x z
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reflect_add : ∀ {R : Type u_1} [inst : Semiring R] (f g : Polynomial R) (N : ℕ),
  Polynomial.reflect N (f + g) = Polynomial.reflect N f + Polynomial.reflect N g
-- Batteries.Data.Array.Match
_private.Batteries.Data.Array.Match.0.Array.Matcher.modifyStep.match_1.eq_3 : ∀ {α σ : Type u_1} {n : Type u_1 → Type u_2} [inst : BEq α] (m : Array.Matcher α) [inst_1 : Std.Iterator σ n α]
  (it : Std.IterM n σ) (motive : it.internalState.inner.Step → Sort u_3) (it' : Std.IterM n α) (x : α)
  (property : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' x))
  (h_1 : (property : it.internalState.inner.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩)
  (h_2 :
    (it' : Std.IterM n α) →
      (property : it.internalState.inner.IsPlausibleStep (Std.IterStep.skip it')) →
        motive ⟨Std.IterStep.skip it', property⟩)
  (h_3 :
    (it' : Std.IterM n α) →
      (x : α) →
        (property : it.internalState.inner.IsPlausibleStep (Std.IterStep.yield it' x)) →
          motive ⟨Std.IterStep.yield it' x, property⟩),
  (match ⟨Std.IterStep.yield it' x, property⟩ with
    | ⟨Std.IterStep.done, property⟩ => h_1 property
    | ⟨Std.IterStep.skip it', property⟩ => h_2 it' property
    | ⟨Std.IterStep.yield it' x, property⟩ => h_3 it' x property) =
    h_3 it' x property
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.botEquiv_def : ∀ {F : Type u_1} [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (x : F),
  (IntermediateField.botEquiv F E) ((algebraMap F ↥⊥) x) = x
-- Mathlib.Data.Finsupp.NeLocus
Finsupp.zipWith_neLocus_eq_left : ∀ {α : Type u_1} {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : DecidableEq α] [inst_1 : DecidableEq N]
  [inst_2 : Zero M] [inst_3 : DecidableEq P] [inst_4 : Zero P] [inst_5 : Zero N] {F : M → N → P} (F0 : F 0 0 = 0)
  (f : α →₀ M) (g₁ g₂ : α →₀ N),
  (∀ (f : M), Function.Injective fun g => F f g) →
    (Finsupp.zipWith F F0 f g₁).neLocus (Finsupp.zipWith F F0 f g₂) = g₁.neLocus g₂
-- Init.Data.Array.Basic
Array.reverse.termination : ∀ {i j : ℕ}, i < j → j - 1 - (i + 1) < j - i
-- Std.Do.Triple.Basic
Std.Do.Triple.pure : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {P : Std.Do.SPred ps.args} [inst : Monad m]
  [inst_1 : Std.Do.WPMonad m ps] {α : Type u} {Q : Std.Do.PostCond α ps} (a : α), (P ⊢ₛ Q.1 a) → ⦃P⦄ pure a ⦃Q⦄
-- Mathlib.Algebra.Group.Subgroup.Pointwise
/-- The action on a subgroup corresponding to applying the action to every element.

This is available as an instance in the `Pointwise` locale.  -/
Subgroup.pointwiseMulAction : {α : Type u_1} →
  {G : Type u_2} → [inst : Group G] → [inst_1 : Monoid α] → [MulDistribMulAction α G] → MulAction α (Subgroup G)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
Filter.EventuallyEq.contMDiffAt_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f f₁ : M → M'} {x : M}
  {n : WithTop ℕ∞}, f₁ =ᶠ[nhds x] f → (ContMDiffAt I I' n f₁ x ↔ ContMDiffAt I I' n f x)
-- Mathlib.Data.NNReal.Defs
NNReal.orderIsoIccZeroCoe_apply_coe_coe : ∀ (a : NNReal) (b : ↑(Set.Icc 0 ↑a)), ↑↑(a.orderIsoIccZeroCoe b) = ↑b
-- Mathlib.Algebra.Field.Defs
Rat.smulDivisionRing : {K : Type u_1} → [DivisionRing K] → SMul ℚ K
-- Lean.Elab.Match
/-- The `Bool` context is true iff we are inside of an "inaccessible" pattern.  -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.ToDepElimPattern.savePatternInfo.go : Lean.Expr → ReaderT Bool Lean.Elab.TermElabM Lean.Expr
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.cokernel_π_comp_cokernelToAbelianCoimage_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {Z : C} (h : CategoryTheory.Abelian.coimage S.g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.π S.f)
      (CategoryTheory.CategoryStruct.comp S.cokernelToAbelianCoimage h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Abelian.coimage.π S.g) h
-- Mathlib.Topology.MetricSpace.Basic
PseudoEMetricSpace.replaceEDist_eq : ∀ {X : Type u_2} (m : PseudoEMetricSpace X) (d : X → X → ENNReal) (hd : d = edist), m.replaceEDist d hd = m
-- Init.Data.SInt.Bitwise
ISize.not_not : ∀ {a : ISize}, ~~~~~~a = a
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.roiIterator : {α : Type u_1} → {β : α → Type u_2} → [Ord α] → Std.DTreeMap.Internal.Impl α β → α → Std.Iter ((a : α) × β a)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_alter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      (t.alter k f).getKey? k' =
        if cmp k k' = Ordering.eq then if (f t[k]?).isSome = true then some k else none else t.getKey? k'
-- Init.Sym.Lemmas
Lean.Sym.Rat.eq_eq_false : ∀ (a b : ℚ), decide (a = b) = false → (a = b) = False
-- Std.Data.HashSet.Lemmas
Std.HashSet.size_ofList_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α},
  (Std.HashSet.ofList l).size ≤ l.length
-- Mathlib.LinearAlgebra.AffineSpace.Restrict
AffineMap.restrict.coe_apply : ∀ {k : Type u_1} {V₁ : Type u_2} {P₁ : Type u_3} {V₂ : Type u_4} {P₂ : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : Module k V₁] [inst_4 : Module k V₂]
  [inst_5 : AddTorsor V₁ P₁] [inst_6 : AddTorsor V₂ P₂] (φ : P₁ →ᵃ[k] P₂) {E : AffineSubspace k P₁}
  {F : AffineSubspace k P₂} [inst_7 : Nonempty ↥E] [inst_8 : Nonempty ↥F] (hEF : AffineSubspace.map φ E ≤ F) (x : ↥E),
  ↑((φ.restrict hEF) x) = φ ↑x
-- Mathlib.Data.Num.Lemmas
Num.succ_to_nat : ∀ (n : Num), ↑n.succ = ↑n + 1
-- Mathlib.NumberTheory.ZetaValues
bernoulliFun_endpoints_eq_of_ne_one : ∀ {k : ℕ}, k ≠ 1 → bernoulliFun k 1 = bernoulliFun k 0
-- Std.Data.TreeSet.Raw.Basic
/-- Computes the intersection of the given tree sets.

This function always iterates through the smaller set.
 -/
Std.TreeSet.Raw.inter : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → Std.TreeSet.Raw α cmp → Std.TreeSet.Raw α cmp
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.centerCongr_symm_apply_coe : ∀ {R : Type u} {S : Type v} [inst : NonAssocSemiring R] [inst_1 : NonAssocSemiring S] (e : R ≃+* S)
  (s : ↥(Subsemigroup.center S)), ↑((Subsemiring.centerCongr e).symm s) = e.symm ↑s
-- Mathlib.Analysis.Convex.Slope
/-- A function `f : 𝕜 → 𝕜` is convex iff for any three points `x < y < z` the slope of the secant
line of `f` on `[x, y]` is less than the slope of the secant line of `f` on `[y, z]`.  -/
convexOn_iff_slope_mono_adjacent : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  ConvexOn 𝕜 s f ↔
    Convex 𝕜 s ∧ ∀ ⦃x y z : 𝕜⦄, x ∈ s → z ∈ s → x < y → y < z → (f y - f x) / (y - x) ≤ (f z - f y) / (z - y)
-- Mathlib.Combinatorics.Additive.VerySmallDoubling
_private.Mathlib.Combinatorics.Additive.VerySmallDoubling.0.Finset.IsAtom.isFragment : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {K : ℝ} {A S : Finset G},
  Finset.IsAtom✝ K S A → Finset.IsFragment✝ K S A
-- Mathlib.Algebra.Regular.SMul
IsSMulRegular.natAbs_iff : ∀ {M : Type u_3} [inst : SubtractionMonoid M] {n : ℤ}, IsSMulRegular M n.natAbs ↔ IsSMulRegular M n
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.PromiseCheckedResult.mk.injEq : ∀ (mainEnv asyncEnv : Lean.Environment) (checkedEnvPromise : IO.Promise Lean.Kernel.Environment)
  (mainEnv_1 asyncEnv_1 : Lean.Environment) (checkedEnvPromise_1 : IO.Promise Lean.Kernel.Environment),
  ({ mainEnv := mainEnv, asyncEnv := asyncEnv, checkedEnvPromise := checkedEnvPromise } =
      { mainEnv := mainEnv_1, asyncEnv := asyncEnv_1, checkedEnvPromise := checkedEnvPromise_1 }) =
    (mainEnv = mainEnv_1 ∧ asyncEnv = asyncEnv_1 ∧ checkedEnvPromise = checkedEnvPromise_1)
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.isLittleOTVS_neg_right : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F} [ContinuousNeg F],
  f =o[𝕜; l] (-g) ↔ f =o[𝕜; l] g
-- Mathlib.CategoryTheory.Abelian.Basic
/-- In an abelian category, the pullback of an epimorphism is an epimorphism.  -/
CategoryTheory.Abelian.epi_pullback_of_epi_g : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.Limits.HasPullbacks C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z) [CategoryTheory.Epi g],
  CategoryTheory.Epi (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.CategoryTheory.LiftingProperties.ParametrizedAdjunction
CategoryTheory.ParametrizedAdjunction.arrowHomEquiv_apply_right_fst : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)}
  {G : CategoryTheory.Functor C₁ᵒᵖ (CategoryTheory.Functor C₃ C₂)} (adj₂ : F ⊣₂ G) {X₁ Y₁ : C₁} {f₁ : X₁ ⟶ Y₁}
  {X₂ Y₂ : C₂} {f₂ : X₂ ⟶ Y₂} {X₃ Y₃ : C₃} {f₃ : X₃ ⟶ Y₃} (sq₁₂ : F.PushoutObjObj f₁ f₂) (sq₁₃ : G.PullbackObjObj f₁ f₃)
  (α : CategoryTheory.Arrow.mk sq₁₂.ι ⟶ CategoryTheory.Arrow.mk f₃),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Arrow.Hom.right ((adj₂.arrowHomEquiv sq₁₂ sq₁₃) α)) sq₁₃.fst =
    adj₂.homEquiv (CategoryTheory.CategoryStruct.comp sq₁₂.inr (CategoryTheory.Arrow.Hom.left α))
-- Mathlib.Algebra.Ring.Hom.Defs
/-- `NonUnitalRingHomClass F α β` states that `F` is a type of non-unital (semi)ring
homomorphisms. You should extend this class when you extend `NonUnitalRingHom`.  -/
NonUnitalRingHomClass : (F : Type u_5) →
  (α : outParam (Type u_6)) →
    (β : outParam (Type u_7)) → [NonUnitalNonAssocSemiring α] → [NonUnitalNonAssocSemiring β] → [FunLike F α β] → Prop
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubAddAction.ofFixingAddSubgroup_insert_map.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : AddGroup M] [inst_1 : AddAction M α] (a : α)
  (s : Set ↥(SubAddAction.ofStabilizer M a)),
  SubAddAction.ofFixingAddSubgroup_insert_map a s =
    { toFun := fun x => (fun hx hx' => ⟨⟨↑x, hx⟩, hx'⟩) ⋯ ⋯, map_vadd' := ⋯ }