mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.map_toSpecMvPoly : ∀ {n : Type u} {S T : AlgebraicGeometry.Scheme} (f : S ⟶ T),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.map n f)
      (AlgebraicGeometry.AffineSpace.toSpecMvPoly n T) =
    AlgebraicGeometry.AffineSpace.toSpecMvPoly n S
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctor.id_map₂ : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
  (CategoryTheory.StrictlyUnitaryLaxFunctor.id B).map₂ η = η
-- Mathlib.Topology.Sheaves.LocalPredicate
TopCat.LocalPredicate.mk.inj : ∀ {X : TopCat} {T : ↑X → Type u_1} {toPrelocalPredicate : TopCat.PrelocalPredicate T}
  {locality :
    ∀ {U : TopologicalSpace.Opens ↑X} (f : (x : ↥U) → T ↑x),
      (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, toPrelocalPredicate.pred fun x => f (i x)) → toPrelocalPredicate.pred f}
  {toPrelocalPredicate_1 : TopCat.PrelocalPredicate T}
  {locality_1 :
    ∀ {U : TopologicalSpace.Opens ↑X} (f : (x : ↥U) → T ↑x),
      (∀ (x : ↥U), ∃ V, ∃ (_ : ↑x ∈ V), ∃ i, toPrelocalPredicate_1.pred fun x => f (i x)) →
        toPrelocalPredicate_1.pred f},
  { toPrelocalPredicate := toPrelocalPredicate, locality := locality } =
      { toPrelocalPredicate := toPrelocalPredicate_1, locality := locality_1 } →
    toPrelocalPredicate = toPrelocalPredicate_1
-- Mathlib.Algebra.Lie.AdjointAction.Derivation
LieDerivation.ad_apply_apply : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (a a_1 : L),
  ((LieDerivation.ad R L) a) a_1 = ⁅a, a_1⁆
-- Mathlib.Dynamics.Transitive
AddAction.isTopologicallyTransitive_iff : ∀ (M : Type u_1) {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : AddMonoid M] [inst_2 : AddAction M α],
  AddAction.IsTopologicallyTransitive M α ↔
    ∀ {U V : Set α}, IsOpen U → U.Nonempty → IsOpen V → V.Nonempty → ∃ m, ((m +ᵥ U) ∩ V).Nonempty
-- Init.Data.SInt.Basic
/-- Converts 32-bit signed integers to word-sized signed integers that denote the same number. This
conversion is lossless, because `ISize` is either `Int32` or `Int64`.

This function is overridden at runtime with an efficient implementation.
 -/
Int32.toISize : Int32 → ISize
-- Batteries.Classes.Order
Std.LawfulLECmp.ne_lt_iff_ge : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x y : α} [inst : LE α] [Std.LawfulLECmp cmp], cmp x y ≠ Ordering.lt ↔ y ≤ x
-- Lean.Data.Lsp.Window
Lean.Lsp.instToJsonShowMessageRequestParams : Lean.ToJson Lean.Lsp.ShowMessageRequestParams
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.Lp.simpleFunc.toSimpleFunc_indicatorConst : ∀ {α : Type u_1} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (c : E),
  ⇑(MeasureTheory.Lp.simpleFunc.toSimpleFunc (MeasureTheory.Lp.simpleFunc.indicatorConst p hs hμs c)) =ᵐ[μ]
    ⇑(MeasureTheory.SimpleFunc.piecewise s hs (MeasureTheory.SimpleFunc.const α c) (MeasureTheory.SimpleFunc.const α 0))
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor_obj_obj_obj : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] (W : CategoryTheory.MorphismProperty C) (D : Type uD)
  [inst_1 : CategoryTheory.Category.{uD', uD} D] (X : CategoryTheory.Functor W.Localization D) (X_1 : C),
  ((CategoryTheory.Localization.Construction.WhiskeringLeftEquivalence.functor W D).obj X).obj.obj X_1 =
    X.obj (W.Q.obj X_1)
-- Lean.Util.LeanOptions
Lean.instCoeStringLeanOptionValue : Coe String Lean.LeanOptionValue
-- Mathlib.CategoryTheory.Functor.Category
CategoryTheory.NatTrans.exchange : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {F G H : CategoryTheory.Functor C D}
  {I J K : CategoryTheory.Functor D E} (α : F ⟶ G) (β : G ⟶ H) (γ : I ⟶ J) (δ : J ⟶ K),
  CategoryTheory.CategoryStruct.comp α β ◫ CategoryTheory.CategoryStruct.comp γ δ =
    CategoryTheory.CategoryStruct.comp (α ◫ γ) (β ◫ δ)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
Submodule.starProjection_bot : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E],
  ⊥.starProjection = 0
-- Mathlib.CategoryTheory.Localization.Construction
CategoryTheory.Localization.Construction.NatTransExtension.app.eq_1 : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] {W : CategoryTheory.MorphismProperty C} {D : Type uD}
  [inst_1 : CategoryTheory.Category.{uD', uD} D] {F₁ F₂ : CategoryTheory.Functor W.Localization D}
  (τ : W.Q.comp F₁ ⟶ W.Q.comp F₂) (X : W.Localization),
  CategoryTheory.Localization.Construction.NatTransExtension.app τ X =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.Localization.Construction.objEquiv W).invFun X))
        (CategoryTheory.eqToHom ⋯))
-- Mathlib.Algebra.Homology.HomotopyFiber
/-- The second projection `K.pathObject ⟶ K`.  -/
HomologicalComplex.pathObject.π₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {α : Type u_2} →
        {c : ComplexShape α} →
          (K : HomologicalComplex C c) →
            [inst_2 : DecidableRel c.Rel] →
              [inst_3 : ∀ (i : α), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] →
                [inst_4 : K.HasPathObject] → K.pathObject ⟶ K
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUInfo.speed : Std.Internal.UV.System.CPUInfo → UInt64
-- Mathlib.Algebra.Group.Hom.Basic
zsmulAddGroupHom_apply : ∀ {α : Type u_1} [inst : SubtractionCommMonoid α] (n : ℤ) (x : α), (zsmulAddGroupHom n) x = n • x
-- Lean.PrivateName
_private.Lean.PrivateName.0.Lean.privateToUserNameAux : Lean.Name → Lean.Name
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
zmodAddEquivOfGenerator_apply_one : ∀ {G : Type u_2} [inst : AddGroup G] {g : G} (hg : ∀ (x : G), x ∈ AddSubgroup.zmultiples g) {n : ℕ}
  (hn : Nat.card G = n), (zmodAddEquivOfGenerator hg hn) 1 = g
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.Comma.mapRightIso_functor_obj_left : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] {B : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] {T : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} T]
  (L : CategoryTheory.Functor A T) {P : CategoryTheory.MorphismProperty T} {Q : CategoryTheory.MorphismProperty A}
  {W : CategoryTheory.MorphismProperty B} [inst_3 : Q.IsMultiplicative] [inst_4 : W.IsMultiplicative]
  {R₁ R₂ : CategoryTheory.Functor B T} [inst_5 : P.RespectsIso] [inst_6 : Q.RespectsIso] [inst_7 : W.RespectsIso]
  (e : R₁ ≅ R₂) (X : CategoryTheory.MorphismProperty.Comma L R₁ P Q W),
  ((CategoryTheory.MorphismProperty.Comma.mapRightIso L e).functor.obj X).left = X.left
-- Mathlib.Algebra.Module.LocalizedModule.Basic
/-- If `(M', f)` and `(M'', g)` both satisfy universal property of localized module, then `M', M''`
are isomorphic as `R`-module
 -/
IsLocalizedModule.linearEquiv : {R : Type u_1} →
  [inst : CommSemiring R] →
    (S : Submonoid R) →
      {M : Type u_2} →
        {M' : Type u_3} →
          {M'' : Type u_4} →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid M'] →
                [inst_3 : AddCommMonoid M''] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module R M'] →
                      [inst_6 : Module R M''] →
                        (f : M →ₗ[R] M') →
                          (g : M →ₗ[R] M'') → [IsLocalizedModule S f] → [IsLocalizedModule S g] → M' ≃ₗ[R] M''
-- Mathlib.LinearAlgebra.QuadraticForm.Isometry
/-- There is a zero map from any module with the zero form.  -/
QuadraticMap.Isometry.instZeroOfNat : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {N : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid N] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] → [inst_6 : Module R N] → {Q₂ : QuadraticMap R M₂ N} → Zero (0 →qᵢ Q₂)
-- Mathlib.Topology.MetricSpace.Thickening
Metric.thickening_subset_interior_cthickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α),
  Metric.thickening δ E ⊆ interior (Metric.cthickening δ E)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.mem_alter_of_beq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : Option β → Option β},
  (k == k') = true → (k' ∈ Std.ExtDHashMap.Const.alter m k f ↔ (f (Std.ExtDHashMap.Const.get? m k)).isSome = true)
-- Init.Data.Vector.Attach
Vector.pmap_eq_pmapImpl : @Vector.pmap = @Vector.pmapImpl
-- Mathlib.Topology.EMetricSpace.Weak
Option.edist_none_some : ∀ {α : Type u} [t : TopologicalSpace α] [m : WeakPseudoEMetricSpace α] {a : α}, edist none (some a) = ⊤
-- Mathlib.Analysis.Calculus.FDeriv.Measurable
/-- The set of right differentiability points of a function taking values in a complete space is
Borel-measurable.  -/
measurableSet_of_differentiableWithinAt_Ioi : ∀ {F : Type u_1} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] (f : ℝ → F) [CompleteSpace F],
  MeasurableSet {x | DifferentiableWithinAt ℝ f (Set.Ioi x) x}
-- Mathlib.SetTheory.ZFC.Basic
ZFSet.nonempty_coe : ∀ {x : ZFSet.{u}}, (↑x).Nonempty ↔ x.Nonempty
-- Std.Sync.StreamMap
_private.Std.Sync.StreamMap.0.Std.StreamMap.streams : {α β : Type} → Std.StreamMap α β → Array (α × Std.Async.Selector β × IO Unit)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.coreS.injEq : ∀ (a b : Lean.Expr) (sa sb : Lean.Meta.Grind.Arith.CommRing.SemiringExpr)
  (ra rb : Lean.Meta.Grind.Arith.CommRing.RingExpr) (a_1 b_1 : Lean.Expr)
  (sa_1 sb_1 : Lean.Meta.Grind.Arith.CommRing.SemiringExpr) (ra_1 rb_1 : Lean.Meta.Grind.Arith.CommRing.RingExpr),
  (Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.coreS a b sa sb ra rb =
      Lean.Meta.Grind.Arith.CommRing.EqCnstrProof.coreS a_1 b_1 sa_1 sb_1 ra_1 rb_1) =
    (a = a_1 ∧ b = b_1 ∧ sa = sa_1 ∧ sb = sb_1 ∧ ra = ra_1 ∧ rb = rb_1)
-- Init.Data.String.Lemmas.Splits
_private.Init.Data.String.Lemmas.Splits.0.String.Slice.Pos.Splits.rotateRight.eq_1 : ∀ {s : String.Slice} {p : s.Pos} {t₁ t₂ t₃ : String} (h : p.Splits t₁ (t₂ ++ t₃)),
  h.rotateRight = s.pos (p.offset.increaseBy t₂.utf8ByteSize) ⋯
-- Mathlib.MeasureTheory.Measure.Prokhorov
/-- The set of finite measures of mass at most `C` supported on a given compact set `K` is
compact.  -/
isCompact_setOfPred_finiteMeasure_le_of_isCompact : ∀ {E : Type u_1} [inst : MeasurableSpace E] [inst_1 : TopologicalSpace E] [T2Space E] [inst_3 : BorelSpace E]
  (C : NNReal) {K : Set E}, IsCompact K → IsCompact {μ | μ.mass ≤ C ∧ μ Kᶜ = 0}
-- Mathlib.Logic.Hydra
Relation.cutExpand_add_left : ∀ {α : Type u_1} {r : α → α → Prop} {t u : Multiset α} (s : Multiset α),
  Relation.CutExpand r (s + t) (s + u) ↔ Relation.CutExpand r t u
-- Mathlib.Topology.UniformSpace.UniformConvergence
UniformCauchySeqOn.prod' : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_4} [inst : UniformSpace β] {F : ι → α → β} {s : Set α} {p : Filter ι}
  {β' : Type u_5} [inst_1 : UniformSpace β'] {F' : ι → α → β'},
  UniformCauchySeqOn F p s → UniformCauchySeqOn F' p s → UniformCauchySeqOn (fun i a => (F i a, F' i a)) p s
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.unitsModPrincipalUnitsEquivResidueFieldUnits_comp_quotientGroup_mk_apply : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) (x : ↥A.unitGroup),
  A.unitsModPrincipalUnitsEquivResidueFieldUnits.toMonoidHom ↑x = A.unitGroupToResidueFieldUnits x
-- Init.Data.Fin.Lemmas
Fin.cast_castAdd_left : ∀ {n n' m : ℕ} (i : Fin n') (h : n' + m = n + m), Fin.cast h (Fin.castAdd m i) = Fin.castAdd m (Fin.cast ⋯ i)
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- If `g ≫ f = 0` implies `g = 0` for all `g`, then `0 : 0 ⟶ X` is a kernel of `f`.  -/
CategoryTheory.Limits.zeroKernelOfCancelZero : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X Y : C} →
          (f : X ⟶ Y) →
            (∀ (Z : C) (g : Z ⟶ X), CategoryTheory.CategoryStruct.comp g f = 0 → g = 0) →
              CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι 0 ⋯)
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.comap_inf : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N]
  (S T : L.Substructure N) (f : L.Hom M N),
  FirstOrder.Language.Substructure.comap f (S ⊓ T) =
    FirstOrder.Language.Substructure.comap f S ⊓ FirstOrder.Language.Substructure.comap f T
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.processLevels : List Lean.Level → List Lean.Level → Lean.Meta.Sym.UnifyM✝ Bool
-- Mathlib.MeasureTheory.Integral.DominatedConvergence
intervalIntegral.continuousAt_parametric_primitive_of_dominated : ∀ {E : Type u_1} {X : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : TopologicalSpace X]
  {μ : MeasureTheory.Measure ℝ} [FirstCountableTopology X] {F : X → ℝ → E} (bound : ℝ → ℝ) (a b : ℝ) {a₀ b₀ : ℝ}
  {x₀ : X},
  (∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Set.uIoc a b))) →
    (∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ‖F x t‖ ≤ bound t) →
      IntervalIntegrable bound μ a b →
        (∀ᵐ (t : ℝ) ∂μ.restrict (Set.uIoc a b), ContinuousAt (fun x => F x t) x₀) →
          a₀ ∈ Set.Ioo a b →
            b₀ ∈ Set.Ioo a b → μ {b₀} = 0 → ContinuousAt (fun p => ∫ (t : ℝ) in a₀..p.2, F p.1 t ∂μ) (x₀, b₀)
-- Mathlib.Data.Finset.Defs
Finset.instDecidableRelSubset : {α : Type u_1} → [DecidableEq α] → DecidableRel fun x1 x2 => x1 ⊆ x2
-- Mathlib.CategoryTheory.Monoidal.Mod
/-- **Alias** of `CategoryTheory.IsModHom`.

---

A morphism in `D` is a morphism of `A`-module objects if it commutes with
the action maps  -/
CategoryTheory.IsMod_Hom : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            (A : C) →
              [inst_4 : CategoryTheory.MonObj A] →
                {M N : D} → [CategoryTheory.ModObj A M] → [CategoryTheory.ModObj A N] → (M ⟶ N) → Prop
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- `psumPart` is the product of the symmetric polynomials `psum μᵢ`,
where `μ = (μ₁, μ₂, ...)` is a partition.  -/
MvPolynomial.psumPart : (σ : Type u_5) → (R : Type u_6) → [inst : CommSemiring R] → [Fintype σ] → {n : ℕ} → n.Partition → MvPolynomial σ R
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t.WF →
    ∀ {k k' : α} [inst_1 : Inhabited (β k')] {f : Option (β k) → Option (β k)},
      (t.alter k f).get! k' =
        if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (f (t.get? k))).get! else t.get! k'
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.instIsIsoFunctorProdComparisonBifunctorNatTransOfProdComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D)
  [∀ (A B : C), CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)],
  CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans F)
-- Mathlib.SetTheory.Ordinal.Basic
_private.Mathlib.SetTheory.Ordinal.Basic.0.Ordinal.succ_le_iff' : ∀ {a b : Ordinal.{u_1}}, a + 1 ≤ b ↔ a < b
-- Mathlib.Analysis.Normed.Order.Lattice
lipschitzWith_negPart : ∀ {α : Type u_1} [inst : NormedAddCommGroup α] [inst_1 : Lattice α] [HasSolidNorm α] [IsOrderedAddMonoid α],
  LipschitzWith 1 negPart
-- Mathlib.Algebra.GroupWithZero.Indicator
Function.mulSupport_add_one : ∀ {ι : Type u_1} {R : Type u_5} [inst : One R] [inst_1 : AddRightCancelMonoid R] (f : ι → R),
  (Function.mulSupport fun x => f x + 1) = Function.support f
-- Mathlib.Algebra.Group.Subgroup.Finsupp
AddSubgroup.mem_closure_range_iff : ∀ {M : Type u_1} [inst : AddCommGroup M] {ι : Type u_2} {f : ι → M} {x : M},
  x ∈ AddSubgroup.closure (Set.range f) ↔ ∃ a, x = a.sum fun x1 x2 => x2 • f x1
-- Mathlib.Topology.UniformSpace.Ascoli
/-- A version of the **Arzela-Ascoli theorem**.

If an equicontinuous family of continuous functions is compact in the pointwise topology, then it
is compact in the compact open topology.  -/
ArzelaAscoli.isCompact_of_equicontinuous : ∀ {X : Type u_2} {α : Type u_3} [inst : TopologicalSpace X] [inst_1 : UniformSpace α] (S : Set C(X, α)),
  IsCompact (ContinuousMap.toFun '' S) → (Equicontinuous fun x => ⇑↑x) → IsCompact S
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.down_pure_intro : ∀ {φ : Prop}, φ → ⌜φ⌝.down
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- Supergraphs have smaller or equal extended distances to their subgraphs.  -/
SimpleGraph.edist_anti : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} {G' : SimpleGraph V}, G ≤ G' → G'.edist u v ≤ G.edist u v
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.le_maxKey?_of_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k km : α}
  (hc : k ∈ t), t.maxKey?.get ⋯ = km → (cmp k km).isLE = true
-- Mathlib.Topology.Constructions
/-- A map defined on a sigma type (a.k.a. the disjoint union of an indexed family of topological
spaces) is inducing iff its restriction to each component is inducing and each the image of each
component under `f` can be separated from the images of all other components by an open set.  -/
inducing_sigma : ∀ {X : Type u} {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] [inst_1 : TopologicalSpace X]
  {f : Sigma σ → X},
  Topology.IsInducing f ↔
    (∀ (i : ι), Topology.IsInducing (f ∘ Sigma.mk i)) ∧ ∀ (i : ι), ∃ U, IsOpen U ∧ ∀ (x : Sigma σ), f x ∈ U ↔ x.fst = i
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.baseChange_polynomialY : ∀ {R : Type r} [inst : CommRing R] (W' : WeierstrassCurve.Jacobian R) {S : Type s} [inst_1 : CommRing S] {A : Type u}
  [inst_2 : CommRing A] {B : Type v} [inst_3 : CommRing B] [inst_4 : Algebra R S] [inst_5 : Algebra R A]
  [inst_6 : Algebra S A] [IsScalarTower R S A] [inst_8 : Algebra R B] [inst_9 : Algebra S B] [IsScalarTower R S B]
  (f : A →ₐ[S] B), (W'.baseChange B).polynomialY = (MvPolynomial.map ↑f) (W'.baseChange A).polynomialY
-- Lean.Meta.Tactic.TryThis
/-- Returns a possibly modified version of `tac` that succeeds in `initialState`, prepending
`expose_names` if necessary. If `expectedType?` is non-`none`, the tactic is only considered to have
"succeeded" if the resulting goal is equal (up to `Expr` equality modulo metavariable instantiation)
to the provided type. Returns `none` if the tactic fails even with `expose_names`.

Remark: We cannot determine if a tactic requires `expose_names` merely by inspecting its syntax
(shadowed variables are delaborated without daggers) nor the underlying `Expr` used to produce it
(some inaccessible names may be implicit arguments that do not appear in the delaborated syntax).
 -/
_private.Lean.Meta.Tactic.TryThis.0.Lean.Meta.Tactic.TryThis.mkValidatedTactic : Lean.TSyntax `tactic →
  Lean.MessageData →
    Lean.Elab.Tactic.SavedState →
      optParam (Option Lean.Expr) none → Lean.Elab.Tactic.TacticM (Option (Lean.TSyntax `tactic × Lean.MessageData))
-- Mathlib.Order.Preorder.Chain
Flag.instOrderTopSubtypeMem : {α : Type u_1} → [inst : Preorder α] → [OrderTop α] → (s : Flag α) → OrderTop ↥s
-- Mathlib.GroupTheory.Perm.Basic
Set.SurjOn.perm_pow : ∀ {α : Type u_1} {f : Equiv.Perm α} {s : Set α}, Set.SurjOn (⇑f) s s → ∀ (n : ℕ), Set.SurjOn (⇑(f ^ n)) s s
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.lift_star : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {H : ι → Type u_4} {C : Type u_5}
  {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} {f : (x x_1 : ι) → (h : x ≤ x_1) → T h}
  [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] [inst_2 : (i : ι) → FunLike (H i) (G i) C]
  [inst_3 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_4 : IsDirectedOrder ι] [inst_5 : (i : ι) → Star (G i)]
  [inst_6 : Star C] [inst_7 : ∀ (i j : ι) (h : i ≤ j), StarHomClass (T h) (G i) (G j)]
  [∀ (i : ι), StarHomClass (H i) (G i) C] (g : (i : ι) → H i)
  (h : ∀ (i j : ι) (h : i ≤ j) (x : G i), (g i) x = (g j) ((f i j h) x)) (x : DirectLimit G f),
  DirectLimit.lift f (fun x => ⇑(g x)) h (star x) = star (DirectLimit.lift f (fun x => ⇑(g x)) h x)
-- Mathlib.Algebra.Module.Torsion.Free
smul_right_inj : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {m₁ m₂ : M}
  [Module.IsTorsionFree R M] [IsCancelMulZero R], r ≠ 0 → (r • m₁ = r • m₂ ↔ m₁ = m₂)
-- Mathlib.Analysis.Distribution.ContDiffMapSupportedIn
ContDiffMapSupportedIn.seminorm_fderivLM_le : ∀ (𝕜 : Type u_1) {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F]
  [inst_6 : SMulCommClass ℝ 𝕜 F] {n k : ℕ∞} {K : TopologicalSpace.Compacts E} {i : ℕ}
  (f : ContDiffMapSupportedIn E F n K),
  (ContDiffMapSupportedIn.seminorm 𝕜 E (E →L[ℝ] F) k K i) ((ContDiffMapSupportedIn.fderivLM 𝕜 n k) f) ≤
    (ContDiffMapSupportedIn.seminorm 𝕜 E F n K (i + 1)) f
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsLongestRevMatch.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsRevMatch pat pos →
    (∀ pos' < pos, ¬String.Slice.Pattern.Model.IsRevMatch pat pos') →
      String.Slice.Pattern.Model.IsLongestRevMatch pat pos
-- Mathlib.Algebra.Order.Module.Defs
/-- A constructor for `SMulPosReflectLT` requiring you to prove `a₁ • b < a₂ • b → a₁ < a₂` only
when `0 < b`  -/
SMulPosReflectLT.of_pos : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero α] [inst_1 : Zero β] [inst_2 : SMulWithZero α β] [inst_3 : Preorder α]
  [inst_4 : PartialOrder β], (∀ (b : β), 0 < b → ∀ (a₁ a₂ : α), a₁ • b < a₂ • b → a₁ < a₂) → SMulPosReflectLT α β
-- Mathlib.Analysis.Normed.Group.Pointwise
Bornology.IsBounded.of_mul : ∀ {E : Type u_1} [inst : SeminormedGroup E] {s t : Set E},
  Bornology.IsBounded (s * t) → Bornology.IsBounded s ∨ Bornology.IsBounded t
-- Mathlib.Algebra.Algebra.Opposite
AlgEquiv.toRingEquiv_toOpposite : ∀ (R : Type u_1) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A],
  (AlgEquiv.toOpposite R A).toRingEquiv = RingEquiv.toOpposite A
-- Std.Data.HashMap.Lemmas
Std.HashMap.get_eq_getElem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} {a : α} {h : a ∈ m}, m.get a h = m[a]
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicones.ext_hom_hom : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} {c c' : CategoryTheory.Limits.Bicone F}
  (φ : c.pt ≅ c'.pt)
  (wι :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp (c.ι j) φ.hom = c'.ι j)
      CategoryTheory.Limits.Bicones.ext._auto_1)
  (wπ :
    autoParam (∀ (j : J), CategoryTheory.CategoryStruct.comp φ.hom (c'.π j) = c.π j)
      CategoryTheory.Limits.Bicones.ext._auto_3),
  (CategoryTheory.Limits.Bicones.ext φ wι wπ).hom.hom = φ.hom