mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Subcanonical
CategoryTheory.GrothendieckTopology.uliftYonedaEquiv_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  [inst_1 : J.Subcanonical] {X : C} {F G : CategoryTheory.Sheaf J (Type (max v v'))}
  (α : (CategoryTheory.GrothendieckTopology.uliftYoneda.{v', v, u} J).obj X ⟶ F) (β : F ⟶ G),
  J.uliftYonedaEquiv (CategoryTheory.CategoryStruct.comp α β) =
    (CategoryTheory.ConcreteCategory.hom (β.hom.app (Opposite.op X))) (J.uliftYonedaEquiv α)
-- Std.Data.ExtTreeMap.Basic
/-- Returns the `n`-th smallest key, or `none` if `n` is at least `t.size`.  -/
Std.ExtTreeMap.keyAtIdx? : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeMap α β cmp → ℕ → Option α
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.P_add_Q : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C} (q : ℕ),
  AlgebraicTopology.DoldKan.P q + AlgebraicTopology.DoldKan.Q q =
    CategoryTheory.CategoryStruct.id (AlgebraicTopology.AlternatingFaceMapComplex.obj X)
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.nat_trans_naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) (f : F' ⟶ G.toFunctor) {U V : C} (i : U ⟶ V) (x : F'.obj U),
  ↑((CategoryTheory.ConcreteCategory.hom (f.app V)) ((CategoryTheory.ConcreteCategory.hom (F'.map i)) x)) =
    (CategoryTheory.ConcreteCategory.hom (F.map i)) ↑((CategoryTheory.ConcreteCategory.hom (f.app U)) x)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `sum_apply`. -/
ContinuousLinearMap.sum_apply : ∀ {F : Type u_8} {α : Type u_9} {β : Type u_10} {ι : Type u_11} [inst : FunLike F α β] [inst_1 : AddCommMonoid β]
  [inst_2 : AddCommMonoid F] [IsZeroApply F α β] [IsAddApply F α β] (s : Finset ι) (f : ι → F) (x : α),
  (∑ i ∈ s, f i) x = ∑ i ∈ s, (f i) x
-- Mathlib.Data.Stream.Defs
/-- Use a state monad to generate a stream through corecursion  -/
Stream'.corecState : {σ α : Type u_1} → StateM σ α → σ → Stream' α
-- Lean.Elab.Tactic.Grind.Config
Lean.Elab.Tactic.elabCutsatConfig : Lean.Syntax → optParam Lean.Grind.CutsatConfig { } → optParam Bool true → Lean.Elab.Tactic.TacticM Lean.Grind.Config
-- Mathlib.CategoryTheory.Category.TwoP
TwoP.swapEquiv_symm : TwoP.swapEquiv.symm = TwoP.swapEquiv
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- For any path `p` from `x₀` to `x₁`, we have a homotopy from the constant path based at `x₀` to
`p.trans p.symm`.  -/
Path.Homotopy.reflTransSymm : {X : Type u_1} → [inst : TopologicalSpace X] → {x₀ x₁ : X} → (p : Path x₀ x₁) → (Path.refl x₀).Homotopy (p.trans p.symm)
-- Mathlib.CategoryTheory.MorphismProperty.OfObjectProperty
CategoryTheory.MorphismProperty.monotone_ofObjectProperty_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.ObjectProperty C}
  (Q : CategoryTheory.ObjectProperty C) {P' : CategoryTheory.ObjectProperty C},
  P ≤ P' → CategoryTheory.MorphismProperty.ofObjectProperty P Q ≤ CategoryTheory.MorphismProperty.ofObjectProperty P' Q
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
neg_lt_iff_pos_add' : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b : α}, -a < b ↔ 0 < a + b
-- Mathlib.Analysis.SpecialFunctions.Integrals.Basic
integral_mul_cpow_one_add_sq : ∀ {a b : ℝ} {t : ℂ},
  t ≠ -1 →
    ∫ (x : ℝ) in a..b, ↑x * (1 + ↑x ^ 2) ^ t =
      (1 + ↑b ^ 2) ^ (t + 1) / (2 * (t + 1)) - (1 + ↑a ^ 2) ^ (t + 1) / (2 * (t + 1))
-- Mathlib.Data.Sym.Sym2
Sym2.other_invol : ∀ {α : Type u_1} {a : α} {z : Sym2 α} (ha : a ∈ z) (hb : Sym2.Mem.other ha ∈ z), Sym2.Mem.other hb = a
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.whiskerRight_id_symm_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp f h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight f (CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom h))
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cochain.fromSingleEquiv.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q n : ℤ} (h : p + n = q),
  CochainComplex.HomComplex.Cochain.fromSingleEquiv h =
    {
      toFun := fun α =>
        CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf (ComplexShape.up ℤ) p X).inv (α.v p q h),
      invFun := fun f => CochainComplex.HomComplex.Cochain.fromSingleMk f h, left_inv := ⋯, right_inv := ⋯,
      map_add' := ⋯ }
-- Init.Data.String.Termination
String.Slice.Pos.remainingBytes_copy : ∀ {s : String.Slice} {p : s.Pos}, p.copy.remainingBytes = p.remainingBytes
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.iConvexComb_id' : ∀ {R : Type u_1} {M : Type u_3} [inst : PartialOrder R] [inst_1 : Semiring R] [inst_2 : IsStrictOrderedRing R]
  [inst_3 : Convexity.ConvexSpace R M] (w : Convexity.StdSimplex R M),
  (Convexity.iConvexComb w fun x => x) = Convexity.sConvexComb w
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.cancelDen.injEq : ∀ (c : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr) (val : ℤ) (x n : Lean.Grind.Linarith.Var)
  (c_1 : Lean.Meta.Grind.Arith.Linear.RingDiseqCnstr) (val_1 : ℤ) (x_1 n_1 : Lean.Grind.Linarith.Var),
  (Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.cancelDen c val x n =
      Lean.Meta.Grind.Arith.Linear.RingDiseqCnstrProof.cancelDen c_1 val_1 x_1 n_1) =
    (c = c_1 ∧ val = val_1 ∧ x = x_1 ∧ n = n_1)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasOfPostcompPropertyMin : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W P Q : CategoryTheory.MorphismProperty C)
  [P.HasOfPostcompProperty W] [Q.HasOfPostcompProperty W], (P ⊓ Q).HasOfPostcompProperty W
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.refl_mul : ∀ {R : Type u_1} {E : Type u_5} [inst : Semiring R] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module R E]
  (e : E ≃ₗᵢ[R] E), LinearIsometryEquiv.refl R E * e = e
-- Init.Sym.Simp.SimprocDSL
/-- Recursive simplifier discharge. Calls the full simplifier to prove side conditions.  -/
Lean.Parser.Sym.Simp.dischSelf : Lean.ParserDescr
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.copy_eq : ∀ {X : Type u_1} [inst : MetricSpace X] (D : Delone.DeloneSet X) (carrier : Set X)
  (packingRadius coveringRadius : NNReal) (h_carrier : carrier = D.carrier)
  (h_packing : packingRadius = D.packingRadius) (h_covering : coveringRadius = D.coveringRadius),
  D.copy carrier packingRadius coveringRadius h_carrier h_packing h_covering = D
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.of_forall_getElem?_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp], t₁.WF → t₂.WF → (∀ (k : α), t₁[k]? = t₂[k]?) → t₁.Equiv t₂
-- Mathlib.GroupTheory.Torsion
/-- The `p`-primary component is the subgroup of elements `g` such that `g ^ p ^ k = 1`
for some `k`. For prime `p`, these are exactly the elements of `p`-power order.  -/
CommGroup.primaryComponent : (G : Type u_1) → [inst : CommGroup G] → ℕ → Subgroup G
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_dvd : ∀ {K : Type u} [inst : Field K] {x : RatFunc K} {p : Polynomial K},
  p ≠ 0 →
    (x.num ∣ p ↔ ∃ q, q ≠ 0 ∧ x = (algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q)
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Derivation.tensorProductTo.congr_simp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (D D_1 : Derivation R S M), D = D_1 → D.tensorProductTo = D_1.tensorProductTo
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- Composition of continuous linear maps.  -/
ContinuousLinearMap.«term_∘L_» : Lean.TrailingParserDescr
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesAt.compContinuousLinearMap : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {u : E →L[𝕜] F} {f : F → G}
  {pf : FormalMultilinearSeries 𝕜 F G} {x : E},
  HasFPowerSeriesAt f pf (u x) → HasFPowerSeriesAt (f ∘ ⇑u) (pf.compContinuousLinearMap u) x
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.Basic
MeasureTheory.charFun_map_add_const : ∀ {E : Type u_3} [inst : MeasurableSpace E] {μ : MeasureTheory.Measure E} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace ℝ E] [BorelSpace E] (r t : E),
  MeasureTheory.charFun (MeasureTheory.Measure.map (fun x => x + r) μ) t =
    MeasureTheory.charFun μ t * Complex.exp (↑(inner ℝ r t) * Complex.I)
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.equivMvPolynomial_symm_X_1 : ∀ {R : Type u_1} [inst : CommSemiring R],
  (Polynomial.Bivariate.equivMvPolynomial R).symm (MvPolynomial.X 1) = Polynomial.X
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.size_eq_match_roc : ∀ {α : Type u} {r : Std.Rio α} [inst : Std.PRange.Least? α] [inst_1 : LT α] [inst_2 : DecidableLT α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.Rxo.HasSize α] [Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [Std.Rxo.IsAlwaysFinite α] [Std.Rxo.LawfulHasSize α],
  r.size =
    match Std.PRange.least? with
    | none => 0
    | some next => if next < r.upper then (next<...r.upper).size + 1 else 0
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NFBelow.below : {motive : (a : ONote) → (a_1 : Ordinal.{0}) → a.NFBelow a_1 → Prop} →
  {a : ONote} → {a_1 : Ordinal.{0}} → a.NFBelow a_1 → Prop
-- Mathlib.GroupTheory.Torsion
CommMonoid.torsion.eq_1 : ∀ (G : Type u_1) [inst : CommMonoid G],
  CommMonoid.torsion G = { carrier := {x | IsOfFinOrder x}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.Algebra.Divisibility.Basic
dvd_of_mul_right_dvd : ∀ {α : Type u_1} [inst : Semigroup α] {a b c : α}, a * b ∣ c → a ∣ c
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.forIn_filterMap : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {n : Type w → Type w''} {β₂ : Type w} [inst_1 : Monad n] [LawfulMonad n]
  [Std.Iterators.Finite α Id] [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {it : Std.Iter β}
  {f : β → Option β₂} {init : γ} {g : β₂ → γ → n (ForInStep γ)},
  forIn (Std.Iter.filterMap f it) init g =
    forIn it init fun out acc =>
      match f out with
      | some c => g c acc
      | none => pure (ForInStep.yield acc)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.containsThenInsert_fst : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.containsThenInsert k).1 = t.contains k
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_inter! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β},
        Std.DTreeMap.Internal.Impl.Const.getD (m₁.inter! m₂) k fallback =
          if Std.DTreeMap.Internal.Impl.contains k m₂ = true then Std.DTreeMap.Internal.Impl.Const.getD m₁ k fallback
          else fallback
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.hom_ext₁_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {F G : CategoryTheory.ComposableArrows C 1}
  {φ φ' : F ⟶ G},
  φ = φ' ↔
    CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 =
        CategoryTheory.ComposableArrows.app' φ' 0 CategoryTheory.ComposableArrows.homMk₁._proof_4 ∧
      CategoryTheory.ComposableArrows.app' φ 1 CategoryTheory.ComposableArrows.homMk₁._proof_5 =
        CategoryTheory.ComposableArrows.app' φ' 1 CategoryTheory.ComposableArrows.homMk₁._proof_5
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- Implementation of `SheafConditionPairwiseIntersections.coneEquiv`.  -/
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverseObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        (F : TopCat.Presheaf C X) →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U) →
                CategoryTheory.Limits.Cone ((CategoryTheory.Pairwise.diagram U).op.comp F)
-- Mathlib.MeasureTheory.Function.LocallyIntegrable
MeasureTheory.integrableOn_Iic_iff_integrableAtFilter_atBot : ∀ {X : Type u_1} {ε : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X] [inst_2 : TopologicalSpace ε]
  [inst_3 : ContinuousENorm ε] {f : X → ε} {μ : MeasureTheory.Measure X} [TopologicalSpace.PseudoMetrizableSpace ε]
  {a : X} [inst_5 : LinearOrder X] [CompactIccSpace X],
  MeasureTheory.IntegrableOn f (Set.Iic a) μ ↔
    MeasureTheory.IntegrableAtFilter f Filter.atBot μ ∧ MeasureTheory.LocallyIntegrableOn f (Set.Iic a) μ
-- Mathlib.Algebra.GroupWithZero.Hom
/-- The identity map from a `MonoidWithZero` to itself.  -/
MonoidWithZeroHom.id : (α : Type u_7) → [inst : MulZeroOneClass α] → α →*₀ α
-- Mathlib.Topology.Homotopy.HSpaces
Path.delayReflLeft.eq_1 : ∀ {X : Type u} [inst : TopologicalSpace X] {x y : X} (θ : ↑unitInterval) (γ : Path x y),
  Path.delayReflLeft θ γ = (Path.delayReflRight θ γ.symm).symm
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.swap_C_C : ∀ {R : Type u_1} [inst : CommSemiring R] (r : R),
  Polynomial.Bivariate.swap (Polynomial.C (Polynomial.C r)) = Polynomial.C (Polynomial.C r)
-- Mathlib.CategoryTheory.Abelian.Injective.Resolution
CategoryTheory.InjectiveResolution.comp_descHomotopyZeroOne : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {Y Z : C}
  {I : CategoryTheory.InjectiveResolution Y} {J : CategoryTheory.InjectiveResolution Z} (f : I.cocomplex ⟶ J.cocomplex)
  (comm : CategoryTheory.CategoryStruct.comp I.ι f = 0),
  CategoryTheory.CategoryStruct.comp (I.cocomplex.d 1 2)
      (CategoryTheory.InjectiveResolution.descHomotopyZeroOne f comm) =
    f.f 1 -
      CategoryTheory.CategoryStruct.comp (CategoryTheory.InjectiveResolution.descHomotopyZeroZero f comm)
        (J.cocomplex.d 0 1)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MCasesPat.brecOn.go : {motive_1 : Lean.Parser.Tactic.MCasesPat → Sort u} →
  {motive_2 : List Lean.Parser.Tactic.MCasesPat → Sort u} →
    (t : Lean.Parser.Tactic.MCasesPat) →
      ((t : Lean.Parser.Tactic.MCasesPat) → t.below → motive_1 t) →
        ((t : List Lean.Parser.Tactic.MCasesPat) → Lean.Parser.Tactic.MCasesPat.below_1 t → motive_2 t) →
          motive_1 t ×' t.below
-- Mathlib.Data.ZMod.ValMinAbs
ZMod.valMinAbs_zero : ∀ (n : ℕ), ZMod.valMinAbs 0 = 0
-- Mathlib.Analysis.InnerProductSpace.GramSchmidtOrtho
/-- Given an indexed family `f : ι → E` of vectors in an inner product space `E`, for which the
size of the index set is the dimension of `E`, produce an orthonormal basis for `E` which agrees
with the orthonormal set produced by the Gram-Schmidt orthonormalization process on the elements of
`ι` for which this process gives a nonzero number.  -/
InnerProductSpace.gramSchmidtOrthonormalBasis : {𝕜 : Type u_1} →
  {E : Type u_2} →
    [inst : RCLike 𝕜] →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          {ι : Type u_3} →
            [inst_3 : LinearOrder ι] →
              [LocallyFiniteOrderBot ι] →
                [WellFoundedLT ι] →
                  [inst_6 : Fintype ι] →
                    [FiniteDimensional 𝕜 E] → Module.finrank 𝕜 E = Fintype.card ι → (ι → E) → OrthonormalBasis ι 𝕜 E
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
/-- `Field` instance  -/
Lean.Meta.Grind.Arith.Linear.Struct.fieldInst? : Lean.Meta.Grind.Arith.Linear.Struct → Option Lean.Expr
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
/-- Real coefficient of the monomial.  -/
Tactic.ComputeAsymptotics.Monomial.coef : Tactic.ComputeAsymptotics.Monomial → ℝ
-- Mathlib.Algebra.Star.Pi
Pi.conj_apply : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → CommSemiring (α i)] [inst_1 : (i : ι) → StarRing (α i)]
  (f : (i : ι) → α i) (i : ι), (starRingEnd ((i : ι) → α i)) f i = (starRingEnd (α i)) (f i)
-- Mathlib.Algebra.Order.Module.Defs
posSMulMono_iff_posSMulReflectLT : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : LinearOrder β] [inst_3 : Zero α],
  PosSMulMono α β ↔ PosSMulReflectLT α β
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.toAddSubmonoid_strictMono : ∀ {R : Type u} [inst : NonAssocSemiring R], StrictMono Subsemiring.toAddSubmonoid
-- Mathlib.Data.List.Rotate
/-- List of all cyclic permutations of `l`.
The `cyclicPermutations` of a nonempty list `l` will always contain `List.length l` elements.
This implies that under certain conditions, there are duplicates in `List.cyclicPermutations l`.
The `n`th entry is equal to `l.rotate n`, proven in `List.get_cyclicPermutations`.
The proof that every cyclic permutant of `l` is in the list is `List.mem_cyclicPermutations_iff`.

```
     cyclicPermutations [1, 2, 3, 2, 4] =
       [[1, 2, 3, 2, 4], [2, 3, 2, 4, 1], [3, 2, 4, 1, 2],
        [2, 4, 1, 2, 3], [4, 1, 2, 3, 2]]
```  -/
List.cyclicPermutations : {α : Type u} → List α → List (List α)
-- Std.Data.DTreeMap.Raw.Lemmas
/-- This is a restatement of `mem_of_mem_insertIfNew` that is written to exactly match the
proof obligation in the statement of `get_insertIfNew`.  -/
Std.DTreeMap.Raw.mem_of_mem_insertIfNew' : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α} {v : β k}, a ∈ t.insertIfNew k v → ¬(cmp k a = Ordering.eq ∧ k ∉ t) → a ∈ t
-- Mathlib.Order.CompleteLattice.Basic
iSup_univ : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α}, ⨆ x ∈ Set.univ, f x = ⨆ x, f x
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.instPreorder : {α : Type u_1} → [Preorder α] → Preorder (WithZero α)
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.RealizeConstKey.constName : Lean.Environment.RealizeConstKey✝ → Lean.Name
-- Mathlib.CategoryTheory.Pi.Monoidal
CategoryTheory.Pi.instIsMonoidalForallPi : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)]
  [inst_1 : (i : I) → CategoryTheory.MonoidalCategory (C i)] {D : I → Type u₂}
  [inst_2 : (i : I) → CategoryTheory.Category.{v₂, u₂} (D i)] [inst_3 : (i : I) → CategoryTheory.MonoidalCategory (D i)]
  {F G : (i : I) → CategoryTheory.Functor (D i) (C i)} [inst_4 : (i : I) → (F i).LaxMonoidal]
  [inst_5 : (i : I) → (G i).LaxMonoidal] (τ : (i : I) → F i ⟶ G i)
  [∀ (i : I), CategoryTheory.NatTrans.IsMonoidal (τ i)],
  CategoryTheory.NatTrans.IsMonoidal (CategoryTheory.NatTrans.pi τ)
-- Mathlib.Analysis.Normed.Operator.NNNorm
ContinuousLinearMap.sSup_unitClosedBall_eq_nnnorm : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_4} {F : Type u_5} [inst : NormedAddCommGroup E]
  [inst_1 : SeminormedAddCommGroup F] [inst_2 : DenselyNormedField 𝕜] [inst_3 : NontriviallyNormedField 𝕜₂]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} [inst_6 : RingHomIsometric σ₁₂]
  (f : E →SL[σ₁₂] F), sSup ((fun x => ‖f x‖₊) '' Metric.closedBall 0 1) = ‖f‖₊
-- Std.Data.Internal.List.Associative
Std.Internal.List.maxKey?_le_maxKey?_insertEntryIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [inst_1 : Std.TransOrd α] [inst_2 : BEq α] [inst_3 : Std.LawfulBEqOrd α]
  {k : α} {v : β k} {l : List ((a : α) × β a)} (hd : Std.Internal.List.DistinctKeys l) {km kmi : α},
  Std.Internal.List.maxKey? l = some km →
    (Std.Internal.List.maxKey? (Std.Internal.List.insertEntryIfNew k v l)).get ⋯ = kmi → (compare km kmi).isLE = true
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp}
  [inst : Std.TransCmp cmp] {f : α → β → Option γ} {k : α} {g : k ∈ Std.TreeMap.Raw.filterMap f t} (h : t.WF),
  (Std.TreeMap.Raw.filterMap f t)[k] = (f (t.getKey k ⋯) t[k]).get ⋯
-- Mathlib.Analysis.InnerProductSpace.Defs
InnerProductSpace.Core.inner_neg_left : ∀ {𝕜 : Type u_1} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [c : PreInnerProductSpace.Core 𝕜 F] (x y : F), inner 𝕜 (-x) y = -inner 𝕜 x y
-- Mathlib.CategoryTheory.Sites.Whiskering
CategoryTheory.sheafCompose_map_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  (F : CategoryTheory.Functor A B) [inst_3 : J.HasSheafCompose F] {X Y : CategoryTheory.Sheaf J A} (f : X ⟶ Y),
  ((CategoryTheory.sheafCompose J F).map f).hom = CategoryTheory.Functor.whiskerRight f.hom F
-- Mathlib.Data.Finsupp.SMulWithZero
Finsupp.instSMulWithZero : {α : Type u_1} →
  {M : Type u_5} → {R : Type u_11} → [inst : Zero R] → [inst_1 : Zero M] → [SMulWithZero R M] → SMulWithZero R (α →₀ M)
-- Lean.Parser.Term
Lean.Parser.Term.fromTerm : Lean.Parser.Parser
-- Mathlib.CategoryTheory.Limits.Cones
/-- The triangle consisting of the two natural transformations and `hom` commutes  -/
CategoryTheory.Limits.ConeMorphism.w : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {A B : CategoryTheory.Limits.Cone F} (self : CategoryTheory.Limits.ConeMorphism A B)
  (j : J), CategoryTheory.CategoryStruct.comp self.hom (B.π.app j) = A.π.app j
-- Mathlib.Algebra.Order.Group.PosPart
leOnePart_inv : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : Group α] (a : α), a⁻¹⁻ᵐ = a⁺ᵐ
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.castNum.match_1.eq_1 : ∀ (motive : Num → Sort u_1) (h_1 : Unit → motive Num.zero) (h_2 : (p : PosNum) → motive (Num.pos p)),
  (match Num.zero with
    | Num.zero => h_1 ()
    | Num.pos p => h_2 p) =
    h_1 ()
-- Mathlib.Data.Fin.Tuple.Basic
Fin.le_insertNth_iff : ∀ {n : ℕ} {α : Fin (n + 1) → Type u_3} [inst : (i : Fin (n + 1)) → Preorder (α i)] {i : Fin (n + 1)} {x : α i}
  {p : (j : Fin n) → α (i.succAbove j)} {q : (j : Fin (n + 1)) → α j},
  q ≤ i.insertNth x p ↔ q i ≤ x ∧ (fun j => q (i.succAbove j)) ≤ p
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.hausdorffMeasure_homothety_preimage : ∀ {𝕜 : Type u_4} {E : Type u_5} {P : Type u_6} [inst : NormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : MeasurableSpace P] [inst_4 : MetricSpace P] [inst_5 : NormedAddTorsor E P]
  [inst_6 : BorelSpace P] {d : ℝ},
  0 ≤ d →
    ∀ (x : P) {c : 𝕜},
      c ≠ 0 →
        ∀ (s : Set P),
          (MeasureTheory.Measure.hausdorffMeasure d) (⇑(AffineMap.homothety x c) ⁻¹' s) =
            ‖c‖₊⁻¹ ^ d • (MeasureTheory.Measure.hausdorffMeasure d) s