mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.link.match_3.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (r' : Std.DTreeMap.Internal.Impl α β) →
      (szr : ℕ) →
        (k'' : α) →
          (v'' : β k'') →
            (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
              (motive :
                  Std.DTreeMap.Internal.Impl.Tree α β
                      (r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size) →
                    Sort u_3) →
                (x :
                    Std.DTreeMap.Internal.Impl.Tree α β
                      (r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size)) →
                  ((ℓ : Std.DTreeMap.Internal.Impl α β) →
                      (hℓ₁ : ℓ.Balanced) →
                        (hℓ₂ : ℓ.size = r'.size + 1 + (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').size) →
                          motive { impl := ℓ, balanced_impl := hℓ₁, size_impl := hℓ₂ }) →
                    motive x
-- Mathlib.GroupTheory.Subgroup.Centralizer
Subgroup.le_centralizer_iff_isMulCommutative : ∀ {G : Type u_1} [inst : Group G] {K : Subgroup G}, K ≤ Subgroup.centralizer ↑K ↔ IsMulCommutative ↥K
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRootMonic.monic : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] {f : Polynomial R}
  (self : IsAdjoinRootMonic S f), f.Monic
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ActionResult.stuck.sizeOf_spec : ∀ (gs : List Lean.Meta.Grind.Goal), sizeOf (Lean.Meta.Grind.ActionResult.stuck gs) = 1 + sizeOf gs
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.pow_apply : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (e : M ≃ₗ[R] M)
  (n : ℕ) (m : M), (e ^ n) m = (⇑e)^[n] m
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.Sign.minus.injEq : ∀ {v : Lean.Level} {M : Q(Type v)} (iM iM_1 : Q(Field «$M»)),
  (Mathlib.Tactic.FieldSimp.Sign.minus iM = Mathlib.Tactic.FieldSimp.Sign.minus iM_1) = (iM = iM_1)
-- Mathlib.FieldTheory.IsPerfectClosure
IsPerfectClosure.equiv_comp_equiv_eq_id : ∀ {K : Type u_1} {L : Type u_2} {M : Type u_3} [inst : CommRing K] [inst_1 : CommRing L] [inst_2 : CommRing M]
  (i : K →+* L) (j : K →+* M) (p : ℕ) [inst_3 : ExpChar M p] [inst_4 : ExpChar K p] [inst_5 : ExpChar L p]
  [inst_6 : PerfectRing L p] [inst_7 : IsPerfectClosure i p] [inst_8 : PerfectRing M p] [inst_9 : IsPerfectClosure j p],
  (IsPerfectClosure.equiv i j p).trans (IsPerfectClosure.equiv j i p) = RingEquiv.refl L
-- Mathlib.Analysis.Normed.Operator.Extend
ContinuousLinearMap.extend_eq : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} [inst : AddCommGroup E]
  [inst_1 : UniformSpace E] [inst_2 : IsUniformAddGroup E] [inst_3 : AddCommGroup F] [inst_4 : UniformSpace F]
  [inst_5 : IsUniformAddGroup F] [inst_6 : T0Space F] [inst_7 : AddCommMonoid Eₗ] [inst_8 : UniformSpace Eₗ]
  [inst_9 : ContinuousAdd Eₗ] [inst_10 : Semiring 𝕜] [inst_11 : Semiring 𝕜₂] [inst_12 : Module 𝕜 E]
  [inst_13 : Module 𝕜₂ F] [inst_14 : Module 𝕜 Eₗ] [inst_15 : ContinuousConstSMul 𝕜 Eₗ]
  [inst_16 : ContinuousConstSMul 𝕜₂ F] {σ₁₂ : 𝕜 →+* 𝕜₂} (f : E →SL[σ₁₂] F) [inst_17 : CompleteSpace F] {e : E →L[𝕜] Eₗ},
  DenseRange ⇑e → IsUniformInducing ⇑e → ∀ (x : E), (f.extend e) (e x) = f x
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- If `t : RightLift f (𝟙 c ≫ g)` is a Kan lift, then `t.ofIdComp : RightLift f g` is also
a Kan lift.  -/
CategoryTheory.Bicategory.RightLift.IsKan.ofIdComp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : b ⟶ a} →
        {g : c ⟶ a} →
          (t :
              CategoryTheory.Bicategory.RightLift f
                (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.id c) g)) →
            t.IsKan → t.ofIdComp.IsKan
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.StructuralAtom.id.inj : ∀ {e : Lean.Expr} {f : Mathlib.Tactic.BicategoryLike.Mor₁} {e_1 : Lean.Expr} {f_1 : Mathlib.Tactic.BicategoryLike.Mor₁},
  Mathlib.Tactic.BicategoryLike.StructuralAtom.id e f = Mathlib.Tactic.BicategoryLike.StructuralAtom.id e_1 f_1 →
    e = e_1 ∧ f = f_1
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- `HasFTaylorSeriesUpToOn n f p s` registers the fact that `p 0 = f` and `p (m+1)` is a
derivative of `p m` for `m < n`, and is continuous for `m ≤ n`. This is a predicate analogous to
`HasFDerivWithinAt` but for higher-order derivatives.

Notice that `p` does not sum up to `f` on the diagonal (`FormalMultilinearSeries.sum`), even if
`f` is analytic and `n = ∞`: an additional `1/m!` factor on the `m`th term is necessary for that.  -/
HasFTaylorSeriesUpToOn : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type uE} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type uF} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → WithTop ℕ∞ → (E → F) → (E → FormalMultilinearSeries 𝕜 E F) → Set E → Prop
-- Mathlib.Topology.LocalAtTarget
TopologicalSpace.IsOpenCover.isClosedMap_iff_restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {ι : Type u_3}
  {U : ι → TopologicalSpace.Opens β},
  TopologicalSpace.IsOpenCover U → (IsClosedMap f ↔ ∀ (i : ι), IsClosedMap ((U i).carrier.restrictPreimage f))
-- Mathlib.Order.Basic
/-- **Alias** of `lt_of_le_of_lt`. -/
LE.le.trans_lt : ∀ {α : Type u_1} [inst : Preorder α] {a b c : α}, a ≤ b → b < c → a < c
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.Mon.instCartesianMonoidalCategory.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.Mon.instCartesianMonoidalCategory =
    { toMonoidalCategory := CategoryTheory.Mon.monMonoidal,
      isTerminalTensorUnit :=
        CategoryTheory.Limits.IsTerminal.ofUniqueHom
          (fun M => { hom := CategoryTheory.SemiCartesianMonoidalCategory.toUnit M.X, isMonHom_hom := ⋯ }) ⋯,
      fst := fun M N => { hom := CategoryTheory.SemiCartesianMonoidalCategory.fst M.X N.X, isMonHom_hom := ⋯ },
      snd := fun M N => { hom := CategoryTheory.SemiCartesianMonoidalCategory.snd M.X N.X, isMonHom_hom := ⋯ },
      fst_def := ⋯, snd_def := ⋯,
      tensorProductIsBinaryProduct := fun M N =>
        CategoryTheory.Limits.BinaryFan.IsLimit.mk
          (CategoryTheory.Limits.BinaryFan.mk
            { hom := CategoryTheory.SemiCartesianMonoidalCategory.fst M.X N.X, isMonHom_hom := ⋯ }
            { hom := CategoryTheory.SemiCartesianMonoidalCategory.snd M.X N.X, isMonHom_hom := ⋯ })
          (fun {T} f g => { hom := CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom, isMonHom_hom := ⋯ }) ⋯ ⋯
          ⋯ }
-- Mathlib.Analysis.Analytic.Constructions
analyticAt_inverse_one_add : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [HasSummableGeomSeries A] [Nontrivial A], AnalyticAt 𝕜 (fun x => Ring.inverse (1 + x)) 0
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.op_mono_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X),
  CategoryTheory.Mono f.op ↔ CategoryTheory.Epi f
-- Mathlib.CategoryTheory.Action.Monoidal
Action.diagonalSuccIsoTensorTrivial_inv_hom_apply : ∀ {G : Type u} [inst : Group G] {n : ℕ} (g : G) (f : Fin n → G),
  (CategoryTheory.ConcreteCategory.hom (Action.diagonalSuccIsoTensorTrivial G n).inv.hom) (g, f) = g • Fin.partialProd f
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roi.isEmpty_iff_forall_not_mem : ∀ {α : Type u} {r : Std.Roi α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxi.HasSize α] [Std.Rxi.LawfulHasSize α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [Std.Rxi.IsAlwaysFinite α] [Std.PRange.LawfulUpwardEnumerable α], r.isEmpty = true ↔ ∀ (a : α), a ∉ r
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.isCycleOn_support_cycleOf : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] (f : Equiv.Perm α) (x : α),
  f.IsCycleOn ↑(f.cycleOf x).support
-- Mathlib.CategoryTheory.IsConnected
/-- If any functor to a discrete category is constant on objects, J is connected.
The converse of `any_functor_const_on_obj`.
 -/
CategoryTheory.IsPreconnected.of_any_functor_const_on_obj : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J],
  (∀ {α : Type u₁} (F : CategoryTheory.Functor J (CategoryTheory.Discrete α)) (j j' : J), F.obj j = F.obj j') →
    CategoryTheory.IsPreconnected J
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.hasCokernels : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  CategoryTheory.Limits.HasCokernels D
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
/-- `RingHom.comap` of an isomorphism of rings as an equivalence of their prime spectra.  -/
PrimeSpectrum.comapEquiv : {R : Type u} →
  {S : Type v} → [inst : CommSemiring R] → [inst_1 : CommSemiring S] → R ≃+* S → PrimeSpectrum R ≃o PrimeSpectrum S
-- Init.PropLemmas
And.imp_left : ∀ {a b c : Prop}, (a → b) → a ∧ c → b ∧ c
-- Mathlib.AlgebraicGeometry.Morphisms.WeaklyEtale
AlgebraicGeometry.WeaklyEtale.mk : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  autoParam (AlgebraicGeometry.Flat f) AlgebraicGeometry.WeaklyEtale.flat._autoParam →
    autoParam (AlgebraicGeometry.Flat (CategoryTheory.Limits.pullback.diagonal f))
        AlgebraicGeometry.WeaklyEtale.flat_diagonal._autoParam →
      AlgebraicGeometry.WeaklyEtale f
-- Mathlib.LinearAlgebra.Reflection
/-- A formula for $(r_1 r_2)^m x$, where $m$ is an integer. This is the special case of
`Module.reflection_mul_reflection_zpow_apply` with $z = x$.  -/
Module.reflection_mul_reflection_zpow_apply_self : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x y : M}
  {f g : Module.Dual R M} (hf : f x = 2) (hg : g y = 2) (m : ℤ) (t : optParam R (f y * g x - 2)),
  autoParam (t = f y * g x - 2) Module.reflection_mul_reflection_zpow_apply_self._auto_1 →
    ((Module.reflection hf * Module.reflection hg) ^ m) x =
      (Polynomial.eval t (Polynomial.Chebyshev.S R m) + Polynomial.eval t (Polynomial.Chebyshev.S R (m - 1))) • x +
        (Polynomial.eval t (Polynomial.Chebyshev.S R (m - 1)) * -g x) • y
-- Mathlib.CategoryTheory.Shift.Localization
CategoryTheory.Functor.commShiftOfLocalization.iso_inv_app_assoc : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (L : CategoryTheory.Functor C D)
  (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W] {A : Type w} [inst_4 : AddMonoid A]
  [inst_5 : CategoryTheory.HasShift C A] (F : CategoryTheory.Functor C E) (F' : CategoryTheory.Functor D E)
  [inst_6 : CategoryTheory.Localization.Lifting L W F F'] [inst_7 : CategoryTheory.HasShift D A]
  [inst_8 : CategoryTheory.HasShift E A] [inst_9 : L.CommShift A] [inst_10 : F.CommShift A] (a : A) (X : C) {Z : E}
  (h : F'.obj ((CategoryTheory.shiftFunctor D a).obj (L.obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftOfLocalization.iso L W F F' a).inv.app (L.obj X))
      h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.shiftFunctor E a).map ((CategoryTheory.Localization.Lifting.iso L W F F').hom.app X))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F a).inv.app X)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.Localization.Lifting.iso L W F F').inv.app ((CategoryTheory.shiftFunctor C a).obj X))
          (CategoryTheory.CategoryStruct.comp (F'.map ((CategoryTheory.Functor.commShiftIso L a).hom.app X)) h)))
-- Mathlib.Analysis.Convex.Continuous
ConcaveOn.continuousOn_Ico : ∀ {f : ℝ → ℝ} {y z : ℝ}, ConcaveOn ℝ (Set.Ico y z) f → ContinuousWithinAt f (Set.Ici y) y → ContinuousOn f (Set.Ico y z)
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
CategoryTheory.Limits.terminal.strict_hom_ext_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasStrictTerminalObjects C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C] {A : C} {f g : ⊤_ C ⟶ A}, f = g ↔ True
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
/-- Eta-expanded form of `TendstoUniformly.mul` -/
TendstoUniformly.fun_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3}
  {l : Filter ι} {f f' : ι → β → α} {g g' : β → α},
  TendstoUniformly f g l →
    TendstoUniformly f' g' l → TendstoUniformly (fun i i_1 => f i i_1 * f' i i_1) (fun i => g i * g' i) l
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.findSomeM?.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) →
    (__do_lift : Option β) →
      ((b : β) → motive (some b)) → ((x : Option β) → (∀ (b : β), x = some b → False) → motive x) → motive __do_lift
-- Init.Data.String.Lemmas.FindPos
String.posGT_le_iff : ∀ {s : String} {p : String.Pos.Raw} {h : p < s.rawEndPos} {q : s.Pos}, s.posGT p h ≤ q ↔ p < q.offset
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.isDynCoverOf_empty : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X} {s : Set X} {n : ℕ}, Dynamics.IsDynCoverOf T ∅ U n s
-- Mathlib.NumberTheory.NumberField.House
/-- `newBasis K` defines a reindexed basis of the ring of integers of `K`,
adjusted by the inverse of the equivalence `equivReindex`.  -/
_private.Mathlib.NumberTheory.NumberField.House.0.NumberField.house.newBasis : (K : Type u_1) → [inst : Field K] → [NumberField K] → Module.Basis (K →+* ℂ) ℤ (NumberField.RingOfIntegers K)
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
/-- Alternative constructor for `IndObjectPresentation` taking a cocone instead of its defining
natural transformation.  -/
CategoryTheory.Limits.IndObjectPresentation.ofCocone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type v} →
      [inst_1 : CategoryTheory.SmallCategory I] →
        [CategoryTheory.IsFiltered I] →
          {F : CategoryTheory.Functor I C} →
            (c : CategoryTheory.Limits.Cocone (F.comp CategoryTheory.yoneda)) →
              CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IndObjectPresentation c.pt
-- Mathlib.Algebra.Divisibility.Hom
MonoidHom.map_dvd : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] (f : M →* N) {a b : M}, a ∣ b → f a ∣ f b
-- Mathlib.RingTheory.Coalgebra.GroupLike
isGroupLikeElem_self : ∀ {R : Type u_2} [inst : CommSemiring R] {r : R}, IsGroupLikeElem R r ↔ r = 1
-- Mathlib.Order.Interval.Finset.Defs
WithTop.insertTop.eq_1 : ∀ {α : Type u_1},
  WithTop.insertTop =
    OrderEmbedding.ofMapLEIff (fun s => Finset.cons ⊤ (Finset.map Function.Embedding.coeWithTop s) ⋯) ⋯
-- Mathlib.Analysis.Calculus.LineDeriv.Basic
HasLineDerivWithinAt.congr : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {E : Type u_3} [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {f f₁ : E → F} {f' : F}
  {s : Set E} {x v : E},
  HasLineDerivWithinAt 𝕜 f f' s x v → Set.EqOn f₁ f s → f₁ x = f x → HasLineDerivWithinAt 𝕜 f₁ f' s x v
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.map_taylor : ∀ {R : Type u_2} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] (p : Polynomial R) (r : R) (f : R →+* S),
  Polynomial.map f ((Polynomial.taylor r) p) = (Polynomial.taylor (f r)) (Polynomial.map f p)
-- Mathlib.CategoryTheory.Adjunction.FullyFaithful
CategoryTheory.Adjunction.isIso_map_unit_of_isLeftAdjoint_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {R : CategoryTheory.Functor D C} (h : L ⊣ R) {E : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} E] {T : CategoryTheory.Functor C E} {S : CategoryTheory.Functor E D}
  {X : C} (adj2 : T ⊣ S.comp R) [R.Faithful] [R.Full], CategoryTheory.IsIso (T.map (h.unit.app X))
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestMatchAtChain.below : {ρ : Type} →
  {pat : ρ} →
    [inst : String.Slice.Pattern.Model.PatternModel pat] →
      {s : String.Slice} →
        {motive : (a a_1 : s.Pos) → String.Slice.Pattern.Model.IsLongestMatchAtChain pat a a_1 → Prop} →
          {a a_1 : s.Pos} → String.Slice.Pattern.Model.IsLongestMatchAtChain pat a a_1 → Prop
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.lift_comp_eqToHom : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ] {S' : 𝒮} (h : S = S'),
  p.IsHomLift (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom h)) φ
-- Init.Data.String.Lemmas.FindPos
String.Slice.Pos.prev.eq_1 : ∀ {s : String.Slice} (pos : s.Pos) (h : pos ≠ s.startPos), pos.prev h = s.posLT pos.offset ⋯
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_inv_comp_biproduct_π_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (f : J → C) (X : C) (j : J)
  {Z : C} (h : CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j) h
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Protoset.mk.sizeOf_spec : ∀ {G : Type u_1} {X : Type u_2} {ιₚ : Type u_3} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : SizeOf G]
  [inst_3 : SizeOf X] [inst_4 : SizeOf ιₚ] (tiles : ιₚ → DiscreteTiling.Prototile G X), sizeOf { tiles := tiles } = 1
-- Mathlib.Data.Real.ENatENNReal
ENat.toENNReal_zero : ↑0 = 0
-- Init.System.FilePath
/-- A relative path is one that depends on the current working directory for interpretation. Relative
paths do not start with the root directory or a drive letter.
 -/
System.FilePath.isRelative : System.FilePath → Bool
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.Term.listDecode.match_1.eq_3 : ∀ {L : FirstOrder.Language} {α : Type u_2} (motive : List (α ⊕ (i : ℕ) × L.Functions i) → Sort u_4) (n : ℕ)
  (f : L.Functions n) (l : List (α ⊕ (i : ℕ) × L.Functions i)) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (l : List (α ⊕ (i : ℕ) × L.Functions i)) → motive (Sum.inl a :: l))
  (h_3 : (n : ℕ) → (f : L.Functions n) → (l : List (α ⊕ (i : ℕ) × L.Functions i)) → motive (Sum.inr ⟨n, f⟩ :: l)),
  (match Sum.inr ⟨n, f⟩ :: l with
    | [] => h_1 ()
    | Sum.inl a :: l => h_2 a l
    | Sum.inr ⟨n, f⟩ :: l => h_3 n f l) =
    h_3 n f l
-- Mathlib.Topology.MetricSpace.HausdorffDistance
Metric.exists_mem_closure_infDist_eq_dist : ∀ {α : Type u} [inst : PseudoMetricSpace α] {s : Set α} [ProperSpace α],
  s.Nonempty → ∀ (x : α), ∃ y ∈ closure s, Metric.infDist x s = dist x y
-- Mathlib.Computability.Primrec.List
Primrec.vector_head : ∀ {α : Type u_1} [inst : Primcodable α] {n : ℕ}, Primrec List.Vector.head
-- Mathlib.RingTheory.Polynomial.ContentIdeal
Submodule.IsPrincipal.isPrimitive_iff_contentIdeal_eq_top : ∀ {R : Type u_3} [inst : CommSemiring R] {p : Polynomial R},
  Submodule.IsPrincipal p.contentIdeal → (p.IsPrimitive ↔ p.contentIdeal = ⊤)
-- Mathlib.Data.Multiset.Filter
Multiset.mem_of_mem_filter : ∀ {α : Type u_1} {p : α → Prop} [inst : DecidablePred p] {a : α} {s : Multiset α}, a ∈ Multiset.filter p s → a ∈ s
-- Batteries.Control.Lemmas
ReaderT.run_failure : ∀ {m : Type u_1 → Type u_2} {ρ α : Type u_1} [inst : Monad m] [inst_1 : Alternative m] (ctx : ρ),
  failure.run ctx = failure
-- Mathlib.RingTheory.Polynomial.Content
Polynomial.primPart_dvd : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : NormalizedGCDMonoid R] (p : Polynomial R), p.primPart ∣ p
-- Mathlib.Topology.Closure
closure_nonempty_iff : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, (closure s).Nonempty ↔ s.Nonempty
-- Mathlib.CategoryTheory.Localization.DerivabilityStructure.OfFunctorialResolutions
CategoryTheory.LocalizerMorphism.functorialRightResolutions.localizerMorphismInv_functor : ∀ {C₁ : Type u_1} {C₂ : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} {Φ : CategoryTheory.LocalizerMorphism W₁ W₂}
  {ρ : CategoryTheory.Functor C₂ C₁} {i : CategoryTheory.Functor.id C₂ ⟶ ρ.comp Φ.functor}
  (hi : ∀ (X₂ : C₂), W₂ (i.app X₂)) (hW₁ : W₁ = W₂.inverseImage Φ.functor) [inst_2 : W₂.HasTwoOutOfThreeProperty],
  (CategoryTheory.LocalizerMorphism.functorialRightResolutions.localizerMorphismInv hi hW₁).functor = ρ
-- Mathlib.Topology.Order.OrderClosed
/-- **Alias** of the reverse direction of `bddAbove_closure`. -/
BddAbove.closure : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [ClosedIicTopology α] {s : Set α},
  BddAbove s → BddAbove (closure s)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey!_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ [inst : Inhabited α] {k k' : α} {f : β → β},
      (t.modify k f).getKey! k' = if cmp k k' = Ordering.eq then if k ∈ t then k else default else t.getKey! k'
-- Init.Data.Vector.Lemmas
Vector.foldrM_reverse : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] {xs : Vector α n} {f : α → β → m β}
  {b : β}, Vector.foldrM f b xs.reverse = Vector.foldlM (fun x y => f y x) b xs
-- Mathlib.Data.Seq.Computation
Computation.get_equiv : ∀ {α : Type u} {c₁ c₂ : Computation α}, c₁.Equiv c₂ → ∀ [inst : c₁.Terminates] [inst_1 : c₂.Terminates], c₁.get = c₂.get
-- Mathlib.CategoryTheory.Limits.Shapes.StrictInitial
/-- If `I` is initial, then `X ⨯ I` is isomorphic to it.  -/
CategoryTheory.Limits.mulIsInitial : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasStrictInitialObjects C] →
      {I : C} →
        (X : C) →
          [inst_2 : CategoryTheory.Limits.HasBinaryProduct X I] → CategoryTheory.Limits.IsInitial I → (X ⨯ I ≅ I)
-- Qq.Typ
/-- Check that a term `e : Q(α)` really has type `α`.  -/
Qq.Quoted.check : failed to pretty print expression (use 'set_option pp.rawOnError true' for raw representation)
-- Init.Data.UInt.Lemmas
UInt16.lt_trans : ∀ {a b c : UInt16}, a < b → b < c → a < c
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.minKeyD_modify_eq_minKeyD : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {fallback : α},
  (Std.DTreeMap.Const.modify t k f).minKeyD fallback = t.minKeyD fallback
-- Mathlib.Topology.Order.Lattice
TopologicalLattice.toContinuousSup : ∀ {L : Type u_1} {inst : TopologicalSpace L} {inst_1 : Lattice L} [self : TopologicalLattice L], ContinuousSup L
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.measure_smul : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : Group G] [inst_1 : MulAction G α]
  (μ : MeasureTheory.Measure α) [MeasureTheory.SMulInvariantMeasure G α μ] (c : G) (s : Set α), μ (c • s) = μ s