mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtTarget.iff_of_forall_pullbackSnd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {R : CategoryTheory.Presieve Y},
  R ∈ K.coverings Y →
    ∀ {f : X ⟶ Y},
      P f ↔
        ∀ {U : C} (g : U ⟶ Y) [inst_2 : CategoryTheory.Limits.HasPullback f g],
          R g → P (CategoryTheory.Limits.pullback.snd f g)
-- Mathlib.Tactic.Ring.PNat
Mathlib.Tactic.Ring.instCSLiftValPNatNatHPow : ∀ {n : ℕ+} {n' k : ℕ} [h1 : Mathlib.Tactic.Ring.CSLiftVal n n'], Mathlib.Tactic.Ring.CSLiftVal (n ^ k) (n' ^ k)
-- Mathlib.CategoryTheory.Localization.StructuredArrow
/-- The bijection `StructuredArrow (L.obj X) L ≃ StructuredArrow (L'.obj X) L'`
when `L` and `L'` are two localization functors for the same class of morphisms.  -/
CategoryTheory.Localization.structuredArrowEquiv : {C : Type u_1} →
  {D : Type u_2} →
    {D' : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} D'] →
            (W : CategoryTheory.MorphismProperty C) →
              (L : CategoryTheory.Functor C D) →
                (L' : CategoryTheory.Functor C D') →
                  [L.IsLocalization W] →
                    [L'.IsLocalization W] →
                      {X : C} →
                        CategoryTheory.StructuredArrow (L.obj X) L ≃ CategoryTheory.StructuredArrow (L'.obj X) L'
-- Lean.Server.FileWorker.Utils
/-- Per-version diagnostics state, protected by a mutex.  -/
Lean.Server.FileWorker.EditableDocumentCore.diagnosticsMutex : Lean.Server.FileWorker.EditableDocumentCore → Std.Mutex Lean.Server.FileWorker.DiagnosticsState
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.toWord_zero : ∀ {α : Type u_1} [inst : DecidableEq α], FreeAddGroup.toWord 0 = []
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYonedaObjObjEquiv_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X X' : C}
  {Y : Cᵒᵖ} (f : (CategoryTheory.shrinkYoneda.{w, v, u}.obj X).obj Y) (g : X ⟶ X'),
  CategoryTheory.shrinkYonedaObjObjEquiv
      ((CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYoneda.{w, v, u}.map g).app Y)) f) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.shrinkYonedaObjObjEquiv f) g
-- Mathlib.Topology.Order.AtTopBotIxx
/-- A family of open intervals bounded by diverging limits is locally finite.  -/
locallyFinite_Ioo_of_tendsto : ∀ {X : Type u_1} [inst : LinearOrder X] [inst_1 : TopologicalSpace X] [OrderTopology X] {α : Type u_2}
  [inst_3 : LinearOrder α] [LocallyFiniteOrder α] [NoMaxOrder X] [NoMinOrder X] {l u : α → X},
  Filter.Tendsto l Filter.atTop Filter.atTop →
    Filter.Tendsto u Filter.atBot Filter.atBot → LocallyFinite fun n => Set.Ioo (l n) (u n)
-- Std.Do.SPred.SPred
Std.Do.SPred.conjunction_nil : ∀ {σs : List (Type u)}, Std.Do.SPred.conjunction [] = ⌜True⌝
-- Mathlib.Computability.Ackermann
ack_one : ∀ (n : ℕ), ack 1 n = n + 2
-- Mathlib.Analysis.Calculus.FDeriv.Congr
HasStrictFDerivAt.congr_of_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {f' : E →L[𝕜] F} {x : E},
  HasStrictFDerivAt f f' x → f =ᶠ[nhds x] f₁ → HasStrictFDerivAt f₁ f' x
-- Lean.Parser.Term
/-- Useful for syntax quotations. Note that generic patterns such as `` `(matchExprAltExpr| | ... => $rhs) `` should also
work with other `rhsParser`s (of arity 1).  -/
Lean.Parser.Term.matchExprAltExpr : Lean.Parser.Parser
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
/-- A well-founded linear order is conditionally complete, with a bottom element.  -/
WellFoundedLT.conditionallyCompleteLinearOrderBot : (α : Type u_5) →
  [i₁ : LinearOrder α] → [i₂ : OrderBot α] → [h : WellFoundedLT α] → ConditionallyCompleteLinearOrderBot α
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.pos_real_re : ∀ (x : { x // 0 < x }) (z : UpperHalfPlane), (x • z).re = ↑x * z.re
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
IsGaloisGroup.subgroup : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] (H : Subgroup G) [hGKL : IsGaloisGroup G K L],
  IsGaloisGroup (↥H) (↥(FixedPoints.intermediateField ↥H)) L
-- Mathlib.Algebra.Module.Submodule.EqLocus
LinearMap.eqLocus_eq_top : ∀ {R : Type u_1} {R₂ : Type u_2} {M : Type u_3} {M₂ : Type u_4} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {τ₁₂ : R →+* R₂}
  {f g : M →ₛₗ[τ₁₂] M₂}, f.eqLocus g = ⊤ ↔ f = g
-- Mathlib.Data.Int.Cast.Lemmas
RingHom.Int.subsingleton_ringHom : ∀ {R : Type u_5} [inst : NonAssocSemiring R], Subsingleton (ℤ →+* R)
-- Mathlib.LinearAlgebra.RootSystem.IsValuedIn
RootPairing.isValuedIn_iff : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (S : Type u_6)
  [inst_5 : CommRing S] [inst_6 : Algebra S R], P.IsValuedIn S ↔ ∀ (i j : ι), ∃ s, (algebraMap S R) s = P.pairing i j
-- Std.Data.TreeSet.Basic
Std.TreeSet.instBEq : {α : Type u} → {cmp : α → α → Ordering} → BEq (Std.TreeSet α cmp)
-- Lean.CoreM
Lean.DeclNameGenerator.idx : Lean.DeclNameGenerator → ℕ
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mem_closedBallSubgroup_iff : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a : M}
  {c : MulArchimedeanClass M}, a ∈ c.closedBallSubgroup ↔ c ≤ MulArchimedeanClass.mk a
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.foldM_filterMap : ∀ {α β γ δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad n]
  [LawfulMonad n] [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → Option γ}
  {g : δ → γ → n δ} {init : δ} {it : Std.Iter β},
  Std.Iter.foldM g init (Std.Iter.filterMap f it) =
    Std.Iter.foldM
      (fun d b =>
        match f b with
        | some c => g d c
        | x => pure d)
      init it
-- Mathlib.Analysis.Normed.Module.Multilinear.Curry
/-- A continuous multilinear map with variables indexed by `ι ⊕ ι'` defines a continuous
multilinear map with variables indexed by `ι` taking values in the space of continuous multilinear
maps with variables indexed by `ι'`.  -/
ContinuousMultilinearMap.currySum : {𝕜 : Type u} →
  {ι : Type v} →
    {ι' : Type v'} →
      {G : Type wG} →
        {G' : Type wG'} →
          [Fintype ι] →
            [Fintype ι'] →
              [inst : NontriviallyNormedField 𝕜] →
                [inst_1 : NormedAddCommGroup G] →
                  [inst_2 : NormedSpace 𝕜 G] →
                    [inst_3 : NormedAddCommGroup G'] →
                      [inst_4 : NormedSpace 𝕜 G'] →
                        ContinuousMultilinearMap 𝕜 (fun x => G) G' →
                          ContinuousMultilinearMap 𝕜 (fun x => G) (ContinuousMultilinearMap 𝕜 (fun x => G) G')
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.State.dsimpCache : Lean.Meta.Simp.State → Lean.ExprStructMap Lean.Expr
-- Mathlib.CategoryTheory.Limits.Shapes.IsTerminal
/-- From a functor `F : J ⥤ C`, given a terminal object of `J`, show the cocone
`coconeOfDiagramTerminal` is a colimit.  -/
CategoryTheory.Limits.colimitOfDiagramTerminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} J] →
        {X : J} →
          (tX : CategoryTheory.Limits.IsTerminal X) →
            (F : CategoryTheory.Functor J C) →
              CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfDiagramTerminal tX F)
-- Mathlib.Data.W.Constructions
_private.Mathlib.Data.W.Constructions.0.WType.ofList.match_1.eq_2 : ∀ (γ : Type u_1) (motive : List γ → Sort u_2) (hd : γ) (tl : List γ) (h_1 : Unit → motive [])
  (h_2 : (hd : γ) → (tl : List γ) → motive (hd :: tl)),
  (match hd :: tl with
    | [] => h_1 ()
    | hd :: tl => h_2 hd tl) =
    h_2 hd tl
-- Mathlib.Analysis.Normed.Module.MStructure
IsLprojection.Subtype.distribLattice : {X : Type u_1} →
  [inst : NormedAddCommGroup X] →
    {M : Type u_2} →
      [inst_1 : Ring M] → [inst_2 : Module M X] → [FaithfulSMul M X] → DistribLattice { P // IsLprojection X P }
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.IsMultiplicative.natCast : ∀ {R : Type u_1} {f : ArithmeticFunction ℕ} [inst : Semiring R], f.IsMultiplicative → (↑f).IsMultiplicative
-- Mathlib.MeasureTheory.Function.L1Space.HasFiniteIntegral
MeasureTheory.hasFiniteIntegral_enorm_iff : ∀ {α : Type u_1} {ε : Type u_4} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : ENorm ε] (f : α → ε),
  MeasureTheory.HasFiniteIntegral (fun x => ‖f x‖ₑ) μ ↔ MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.ext_iff : ∀ {E : Type u_3} [inst : AddGroup E] {p q : AddGroupNorm E}, p = q ↔ ∀ (x : E), p x = q x
-- Init.Data.UInt.Lemmas
UInt8.toBitVec_ofNatLT : ∀ {n : ℕ} (hn : n < UInt8.size), (UInt8.ofNatLT n hn).toBitVec = n#'hn
-- Mathlib.Algebra.Order.Ring.Ordering.Defs
/-- The support of a ring preordering `P` in a commutative ring `R` is
the set of elements `x` in `R` such that both `x` and `-x` lie in `P`.
 -/
RingPreordering.supportAddSubgroup : {R : Type u_1} → [inst : CommRing R] → RingPreordering R → AddSubgroup R
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.coe_map : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  {P' : Type u_3} [inst_3 : CommRing P'] [inst_4 : Algebra R P'] (g : P →ₐ[R] P') (I : FractionalIdeal S P),
  ↑(FractionalIdeal.map g I) = Submodule.map g.toLinearMap ↑I
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.isCentralScalar : ∀ {R : Type u_1} {R₃ : Type u_3} {S₃ : Type u_5} [inst : Semiring R] [inst_1 : Semiring R₃] [inst_2 : Semiring S₃]
  {M : Type u_6} [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid M] [inst_5 : Module R M] {M₃ : Type u_8}
  [inst_6 : TopologicalSpace M₃] [inst_7 : AddCommMonoid M₃] [inst_8 : Module R₃ M₃] [inst_9 : Module S₃ M₃]
  [inst_10 : SMulCommClass R₃ S₃ M₃] [inst_11 : ContinuousConstSMul S₃ M₃] {σ₁₃ : R →+* R₃} [inst_12 : Module S₃ᵐᵒᵖ M₃]
  [inst_13 : IsCentralScalar S₃ M₃], IsCentralScalar S₃ (M →SL[σ₁₃] M₃)
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
/-- The sum of a locally finite collection of sections is `C^k` iff each section is.  -/
ContMDiff.sum_section_of_locallyFinite : ∀ {𝕜 : 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] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {ι : Type u_7} {t : ι → (x : M) → V x},
  (LocallyFinite fun i => {x | t i x ≠ 0}) →
    (∀ (i : ι), ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, t i x⟩) →
      ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, ∑' (i : ι), t i x⟩
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
MDifferentiableAt.comp_of_eq : ∀ {𝕜 : 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'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {g : M' → M''} {y : M'}, MDiffAt g y → MDiffAt f x → f x = y → MDiffAt (g ∘ f) x
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- Bounded continuous functions taking values in a complete space form a complete space.  -/
BoundedContinuousFunction.instCompleteSpace : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : PseudoMetricSpace β] [CompleteSpace β],
  CompleteSpace (BoundedContinuousFunction α β)
-- Mathlib.Topology.Algebra.InfiniteSum.DiscreteConvolution
DiscreteConvolution.mem_mulFiber : ∀ {M : Type u_1} [inst : Monoid M] {x : M} {ab : M × M}, ab ∈ DiscreteConvolution.mulFiber x ↔ ab.1 * ab.2 = x
-- Mathlib.Algebra.Homology.Augment
ChainComplex.augment_X_succ : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  (C : ChainComplex V ℕ) {X : V} (f : C.X 0 ⟶ X) (w : CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0) (i : ℕ),
  (C.augment f w).X (i + 1) = C.X i
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
/-- The coherent sheaf condition can be checked after precomposing with the equivalence.
 -/
CategoryTheory.Equivalence.precoherent_isSheaf_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Precoherent C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D) (F : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology C) F ↔
    CategoryTheory.Presheaf.IsSheaf (CategoryTheory.coherentTopology D) (e.inverse.op.comp F)
-- Mathlib.Topology.WithTopology
WithTopology.instPartialOrder : {X : Type u_1} → (t : TopologicalSpace X) → [PartialOrder X] → PartialOrder (WithTopology X t)
-- Mathlib.Geometry.Manifold.VectorField.LieBracket
VectorField.mlieBracket_self : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {V : (x : M) → TangentSpace I x},
  VectorField.mlieBracket I V V = 0
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_vadd : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [inst : VAdd M G] (n : M) (a : G), ↑(n +ᵥ a) = n +ᵥ ↑a
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.instStarModuleId : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E], StarModule 𝕜 (E →ₗ[𝕜] E)
-- Mathlib.Order.PiLex
Pi.Lex.isStrictOrder : ∀ {ι : Type u_1} {β : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (a : ι) → PartialOrder (β a)],
  IsStrictOrder (Lex ((i : ι) → β i)) fun x1 x2 => x1 < x2
-- Init.Data.SInt.Lemmas
Int64.ofIntClamp_int32ToInt : ∀ (x : Int32), Int64.ofIntClamp x.toInt = x.toInt64
-- Mathlib.Analysis.RCLike.Lemmas
RCLike.finrank_le_two : ∀ (K : Type u_1) [inst : RCLike K], Module.finrank ℝ K ≤ 2
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_vsub_right_image : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {s t : Set β}, ⋃ a ∈ t, (fun x => x -ᵥ a) '' s = s -ᵥ t
-- Std.Http.Protocol.H1
/-- Returns total payload bytes currently buffered in `writer.userData`.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.bufferedUserDataBytes : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Writer dir → ℕ
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquivClass.mk : ∀ {F : Type u_9} {A : outParam (Type u_10)} {B : outParam (Type u_11)} [inst : Add A] [inst_1 : Add B]
  [inst_2 : EquivLike F A B], (∀ (f : F) (a b : A), f (a + b) = f a + f b) → AddEquivClass F A B
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
/-- An induction principle for `C(s, 𝕜)₀`.  -/
ContinuousMapZero.induction_on : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {s : Set 𝕜} [inst_1 : Fact (0 ∈ s)] {p : ContinuousMapZero (↑s) 𝕜 → Prop},
  p 0 →
    p (ContinuousMapZero.id s) →
      p (star (ContinuousMapZero.id s)) →
        (∀ (f g : ContinuousMapZero (↑s) 𝕜), p f → p g → p (f + g)) →
          (∀ (f g : ContinuousMapZero (↑s) 𝕜), p f → p g → p (f * g)) →
            (∀ (r : 𝕜) (f : ContinuousMapZero (↑s) 𝕜), p f → p (r • f)) →
              ((∀ f ∈ NonUnitalStarAlgebra.adjoin 𝕜 {ContinuousMapZero.id s}, p f) →
                  ∀ (f : ContinuousMapZero (↑s) 𝕜), p f) →
                ∀ (f : ContinuousMapZero (↑s) 𝕜), p f
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.MonObj.tensorObj.instTensorObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : C} [inst_3 : CategoryTheory.MonObj M]
  [inst_4 : CategoryTheory.MonObj N],
  CategoryTheory.MonObj.tensorObj.instTensorObj =
    {
      one :=
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).inv
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.one CategoryTheory.MonObj.one),
      mul :=
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.tensorμ M N M N)
          (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.MonObj.mul CategoryTheory.MonObj.mul),
      one_mul := ⋯, mul_one := ⋯, mul_assoc := ⋯ }
-- Mathlib.Data.List.Iterate
List.mem_iterate : ∀ {α : Type u_1} {f : α → α} {a : α} {n : ℕ} {b : α}, b ∈ List.iterate f a n ↔ ∃ m < n, b = f^[m] a
-- Mathlib.Data.Finset.Card
Finset.card_disjUnion : ∀ {α : Type u_1} (s t : Finset α) (h : Disjoint s t), (s.disjUnion t h).card = s.card + t.card
-- Mathlib.Data.Set.Defs
/-- The subset relation on sets. `s ⊆ t` means that all elements of `s` are elements of `t`.

Note that you should **not** use this definition directly, but instead write `s ⊆ t`.  -/
Set.Subset : {α : Type u} → Set α → Set α → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.End
/-- If all bifunctors `Jᵒᵖ ⥤ J ⥤ C` have a coend, then the construction
`F ↦ coend F` defines a functor `(Jᵒᵖ ⥤ J ⥤ C) ⥤ C`.  -/
CategoryTheory.Limits.coendFunctor : (J : Type u) →
  [inst : CategoryTheory.Category.{v, u} J] →
    (C : Type u') →
      [inst_1 : CategoryTheory.Category.{v', u'} C] →
        [∀ (F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)), CategoryTheory.Limits.HasCoend F] →
          CategoryTheory.Functor (CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)) C
-- Mathlib.Data.Finset.Card
Finset.le_card_iff_exists_subset_card : ∀ {α : Type u_1} {s : Finset α} {n : ℕ}, n ≤ s.card ↔ ∃ t ⊆ s, t.card = n
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.start_mem_verts_toSubgraph : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), u ∈ p.toSubgraph.verts
-- Mathlib.GroupTheory.Congruence.Defs
Con.quot_mk_eq_coe : ∀ {M : Type u_4} [inst : Mul M] (c : Con M) (x : M), Quot.mk (⇑c) x = ↑x
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.instReprPolyCnstr_lean : Repr Nat.Internal.Linear.PolyCnstr
-- Mathlib.Lean.Expr.Basic
/-- Construct the term of type `α` for a given natural number
(doing typeclass search for the `OfNat` instance required).  -/
Lean.Expr.ofNat : Lean.Expr → ℕ → Lean.MetaM Lean.Expr
-- Lean.Elab.InfoTree.Types
Lean.Elab.FVarAliasInfo.mk.injEq : ∀ (userName : Lean.Name) (id baseId : Lean.FVarId) (userName_1 : Lean.Name) (id_1 baseId_1 : Lean.FVarId),
  ({ userName := userName, id := id, baseId := baseId } = { userName := userName_1, id := id_1, baseId := baseId_1 }) =
    (userName = userName_1 ∧ id = id_1 ∧ baseId = baseId_1)
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.ext_iff : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] {e e' : A ≃ₗc[R] B}, e = e' ↔ ∀ (x : A), e x = e' x
-- Init.Data.Range.Polymorphic.PRange
/-- The intersection operator.  -/
Std.Roi.HasRcoIntersection.intersection : {α : Type w} → [self : Std.Roi.HasRcoIntersection α] → Std.Roi α → Std.Rco α → Std.Rco α
-- Mathlib.Topology.ContinuousOn
ContinuousWithinAt.union : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s t : Set α}
  {x : α}, ContinuousWithinAt f s x → ContinuousWithinAt f t x → ContinuousWithinAt f (s ∪ t) x
-- Mathlib.Algebra.Order.Module.Defs
smul_nonneg_of_nonpos_of_nonpos : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Ring α] [inst_1 : PartialOrder α] [inst_2 : AddCommGroup β]
  [inst_3 : PartialOrder β] [IsOrderedAddMonoid β] [inst_5 : Module α β] [SMulPosMono α β], a ≤ 0 → b ≤ 0 → 0 ≤ a • b
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C} {h₁ h₂ : CategoryTheory.AddGrpObj X}, h₁ = h₂ ↔ h₁.toAddMonObj = h₂.toAddMonObj
-- Init.Tactics
/-- The `let` tactic is for adding definitions to the local context of the main goal.
The definition can be unfolded, unlike definitions introduced by `have`.

* `let x : t := e` adds the definition `x : t := e` if `e` is a term of type `t`.
* `let x := e` uses the type of `e` for `t`.
* `let : t := e` and `let := e` use `this` for the name of the hypothesis.
* `let pat := e` for a pattern `pat` is equivalent to `match e with | pat => _`,
  where `_` stands for the tactics that follow this one.
  It is convenient for types that let only one applicable constructor.
  For example, given `p : α × β × γ`, `let ⟨x, y, z⟩ := p` produces the
  local variables `x : α`, `y : β`, and `z : γ`.
* The syntax `let (eq := h) pat := e` is equivalent to `match h : e with | pat => _`,
  which adds the equation `h : e = pat` to the local context.

The tactic supports all the same syntax variants and options as the `let` term.

## Properties and relations

* Unlike `have`, it is possible to unfold definitions introduced using `let`, using tactics
  such as `simp`, `dsimp`, `unfold`, and `subst`.
* The `clear_value` tactic turns a `let` definition into a `have` definition after the fact.
  The tactic might fail if the local context depends on the value of the variable.
* The `let` tactic is preferred for data (non-propositions).
* Sometimes `have` is used for non-propositions to ensure that the variable is never unfolded,
  which may be important for performance reasons.
 -/
Lean.Parser.Tactic.tacticLet__ : Lean.ParserDescr
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.map : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop} (j j' : J) (f : j ⟶ j')
  (x : ↑(F.obj j)), RingCat.Colimits.Relation.below ⋯
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.leadingCoeff_add_eq_right : ∀ {R : Type u_3} [inst : AddMonoid R] {Γ : Type u_8} [inst_1 : LinearOrder Γ] {x y : HahnSeries Γ R},
  y.orderTop < x.orderTop → (x + y).leadingCoeff = y.leadingCoeff
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMono.splitEpi.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : Y ⟶ X} (se : CategoryTheory.SplitMono f),
  se.splitEpi = { section_ := f, id := ⋯ }
-- Init.Grind.Ring.Basic
Lean.Grind.IsCharP.intCast_emod : ∀ (p : ℕ) {α : Type u} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α p] (x : ℤ), ↑(x % ↑p) = ↑x