mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Order.Field.Basic
max_div_div_right : ∀ {α : Type u_4} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {c : α},
  0 ≤ c → ∀ (a b : α), max (a / c) (b / c) = max a b / c
-- Mathlib.RingTheory.Complex
Algebra.norm_complex_eq : Algebra.norm ℝ = ↑Complex.normSq
-- Lean.DocString.Types
/-- The contents of the list item.  -/
Lean.Doc.ListItem.contents : {α : Type u} → Lean.Doc.ListItem α → Array α
-- Mathlib.AlgebraicTopology.SimplicialSet.CompStruct
SSet.Edge.InvStruct.map_inv : ∀ {X Y : SSet} {x₀ x₁ : X.obj (Opposite.op { len := 0 })} {hom : SSet.Edge x₀ x₁} (I : hom.InvStruct) (f : X ⟶ Y),
  (I.map f).inv = I.inv.map f
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
CliffordAlgebra.instSMulOfIsScalarTower : {R : Type u_3} →
  {A : Type u_4} →
    {M : Type u_5} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : CommRing A] →
            [inst_3 : Algebra R A] →
              [inst_4 : Module R M] →
                [inst_5 : Module A M] → (Q : QuadraticForm A M) → [IsScalarTower R A M] → SMul R (CliffordAlgebra Q)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedMor₂.default : Mathlib.Tactic.BicategoryLike.Mor₂
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToCodeBlock.Context.mk.injEq : ∀ (ref m returnType : Lean.Syntax) (mutableVars : Lean.Elab.Term.Do.VarSet) (insideFor : Bool)
  (ref_1 m_1 returnType_1 : Lean.Syntax) (mutableVars_1 : Lean.Elab.Term.Do.VarSet) (insideFor_1 : Bool),
  ({ ref := ref, m := m, returnType := returnType, mutableVars := mutableVars, insideFor := insideFor } =
      { ref := ref_1, m := m_1, returnType := returnType_1, mutableVars := mutableVars_1, insideFor := insideFor_1 }) =
    (ref = ref_1 ∧ m = m_1 ∧ returnType = returnType_1 ∧ mutableVars = mutableVars_1 ∧ insideFor = insideFor_1)
-- Mathlib.RingTheory.PicardGroup
Submodule.projective_of_isUnit : ∀ {R : Type u} {A : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] [FaithfulSMul R A]
  {I : Submodule R A}, IsUnit I → Module.Projective R ↥I
-- Mathlib.Analysis.InnerProductSpace.l2Space
HilbertBasis.orthonormal : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : RCLike 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] (b : HilbertBasis ι 𝕜 E), Orthonormal 𝕜 ⇑b
-- Init.Tactics
/-- `exfalso` converts a goal `⊢ tgt` into `⊢ False` by applying `False.elim`.  -/
Lean.Parser.Tactic.tacticExfalso : Lean.ParserDescr
-- Init.Data.Array.Lemmas
Array.not_any_eq_all_not : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, (!xs.any p) = xs.all fun a => !p a
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.equivAugmentedCosimplicialObject_counitIso_hom_app_right_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C]
  (X :
    CategoryTheory.Comma (CategoryTheory.Functor.const SimplexCategory)
      (CategoryTheory.Functor.id (CategoryTheory.Functor SimplexCategory C)))
  (X_1 : SimplexCategory),
  (AugmentedSimplexCategory.equivAugmentedCosimplicialObject.counitIso.hom.app X).right.app X_1 =
    CategoryTheory.CategoryStruct.id
      (match CategoryTheory.WithInitial.incl.obj X_1 with
      | CategoryTheory.WithInitial.of x => X.right.obj x
      | CategoryTheory.WithInitial.star => X.left)
-- Mathlib.CategoryTheory.UnivLE
UnivLE.ofEssSurj : CategoryTheory.uliftFunctor.{u, v}.EssSurj → UnivLE.{max u v, v}
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instMonoid.eq_1 : ∀ {α : Type u_1} [inst : Monoid α],
  Lex.instMonoid =
    { toSemigroup := Lex.instSemigroup, toOne := Lex.instOne, one_mul := ⋯, mul_one := ⋯, toNPow := NPow.ofPow,
      npow_zero := ⋯, npow_succ := ⋯ }
-- Mathlib.Topology.UniformSpace.UniformConvergenceTopology
UniformFun.phi : (α : Type u_5) → (β : Type u_6) → (UniformFun α β × UniformFun α β) × α → β × β
-- Mathlib.Algebra.Homology.DerivedCategory.DerivabilityStructureInjectives
HomotopyCategory.homotopyOfEq.congr_simp : ∀ {ι : Type u_2} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (f g : C ⟶ D)
  (w : (HomotopyCategory.quotient V c).map f = (HomotopyCategory.quotient V c).map g),
  HomotopyCategory.homotopyOfEq f g w = HomotopyCategory.homotopyOfEq f g w
-- Mathlib.Data.Set.Finite.Basic
Set.finite_singleton : ∀ {α : Type u} (a : α), {a}.Finite
-- Mathlib.Order.Bounded
Set.unbounded_gt_inter_gt : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] [NoMinOrder α] (a : α),
  Set.Unbounded (fun x1 x2 => x1 > x2) (s ∩ {b | b < a}) ↔ Set.Unbounded (fun x1 x2 => x1 > x2) s
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.matchExpr.inj : ∀ {ref : Lean.Syntax} {«meta» : Bool} {discr : Lean.Syntax}
  {alts : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)} {elseBranch : Lean.Elab.Term.Do.Code}
  {ref_1 : Lean.Syntax} {meta_1 : Bool} {discr_1 : Lean.Syntax}
  {alts_1 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)} {elseBranch_1 : Lean.Elab.Term.Do.Code},
  Lean.Elab.Term.Do.Code.matchExpr ref «meta» discr alts elseBranch =
      Lean.Elab.Term.Do.Code.matchExpr ref_1 meta_1 discr_1 alts_1 elseBranch_1 →
    ref = ref_1 ∧ «meta» = meta_1 ∧ discr = discr_1 ∧ alts = alts_1 ∧ elseBranch = elseBranch_1
-- Mathlib.Algebra.Ring.CompTypeclasses
RingHom.surjective : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] (σ : R₁ →+* R₂) [t : RingHomSurjective σ],
  Function.Surjective ⇑σ
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsInitial.isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasZeroMorphisms C] {X : C}
  (hX : CategoryTheory.Limits.IsInitial X), CategoryTheory.Limits.IsZero X
-- Mathlib.Algebra.GroupWithZero.Action.Defs
DistribSMul.toSMulZeroClass : {M : Type u_12} → {A : Type u_13} → {inst : AddZeroClass A} → [self : DistribSMul M A] → SMulZeroClass M A
-- Mathlib.Topology.Category.CompactlyGenerated
/-- Construct an isomorphism from a homeomorphism.  -/
CompactlyGenerated.isoOfHomeo : {X Y : CompactlyGenerated} → ↑X.toTop ≃ₜ ↑Y.toTop → (X ≅ Y)
-- Aesop.Stats.Basic
Aesop.RuleStatsTotals.instEmptyCollection : EmptyCollection Aesop.RuleStatsTotals
-- Lean.Elab.PreDefinition.WF.Fix
_private.Lean.Elab.PreDefinition.WF.Fix.0.Lean.Elab.WF.replaceRecApps : Lean.Name → ℕ → Lean.Expr → Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Mathlib.GroupTheory.OrderOfElement
pow_mod_card : ∀ {G : Type u_1} [inst : Group G] [inst_1 : Fintype G] (a : G) (n : ℕ), a ^ (n % Fintype.card G) = a ^ n
-- Init.Data.SInt.Lemmas
ISize.ofInt_lt_iff_lt : ∀ {a b : ℤ},
  ISize.minValue.toInt ≤ a →
    a ≤ ISize.maxValue.toInt →
      ISize.minValue.toInt ≤ b → b ≤ ISize.maxValue.toInt → (ISize.ofInt a < ISize.ofInt b ↔ a < b)
-- Mathlib.Topology.UniformSpace.Completion
UniformSpace.Completion.uniformContinuous_completionSeparationQuotientEquiv_symm : ∀ {α : Type u_1} [inst : UniformSpace α],
  UniformContinuous ⇑(UniformSpace.Completion.completionSeparationQuotientEquiv α).symm
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
/-- `homₚ` needs to be compatible with the boundary maps.  -/
TopPair.HomologyPretheory.Hom.w : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (self : HP.Hom HP') (i j : ι),
  CategoryTheory.CategoryStruct.comp (HP.δ i j) (TopPair.proj₂.whiskerLeft (self.hom j)) =
    CategoryTheory.CategoryStruct.comp (self.homₚ i) (HP'.δ i j)
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- The neighbor set of `v ∈ s` in `G.between s sᶜ` excludes the vertices in `s` adjacent to `v`
in `G`.  -/
SimpleGraph.neighborSet_subset_between_union : ∀ {V : Type u_1} {v : V} {G : SimpleGraph V} {s : Set V},
  v ∈ s → G.neighborSet v ⊆ (SimpleGraph.between s sᶜ G).neighborSet v ∪ s
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftUnshift_smul : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {R : Type u_1}
  [inst_2 : Ring R] [inst_3 : CategoryTheory.Linear R C] {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ)
  (hn : n + a = n') (x : R), (x • γ).leftUnshift n hn = x • γ.leftUnshift n hn
-- Mathlib.Order.KonigLemma
/-- A formulation of Kőnig's infinity lemma, useful in applications.
Given a sequence `α 0, α 1, ...` of nonempty types with `α 0` finite,
and a well-behaved family of projections `π : α j → α i` for all `i ≤ j`,
if each term in each `α i` is the projection of only finitely many terms in `α (i+1)`,
then we can find a sequence `(f 0 : α 0), (f 1 : α 1), ...`
where `f i` is the projection of `f j` for all `i ≤ j`.

In a typical application, the `α i` are function types with increasingly large domains,
and `π hij (f : α j)` is the restriction of the domain of `f` to that of `α i`.
In this case, the sequence given by the lemma is essentially a function whose domain
is the limit of the `α i`.

See also `nonempty_sections_of_finite_cofiltered_system`.  -/
exists_seq_forall_proj_of_forall_finite : ∀ {α : ℕ → Type u_1} [Finite (α 0)] [∀ (i : ℕ), Nonempty (α i)] (π : {i j : ℕ} → i ≤ j → α j → α i),
  (∀ ⦃i : ℕ⦄ (a : α i), π ⋯ a = a) →
    (∀ ⦃i j k : ℕ⦄ (hij : i ≤ j) (hjk : j ≤ k) (a : α k), π hij (π hjk a) = π ⋯ a) →
      (∀ (i : ℕ) (a : α i), {b | π ⋯ b = a}.Finite) → ∃ f, ∀ ⦃i j : ℕ⦄ (hij : i ≤ j), π hij (f j) = f i
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₀_apply : ∀ {X : TopCat} (x : ↑X), (CategoryTheory.ConcreteCategory.hom TopCat.ι₀) x = (x, 0)
-- Mathlib.Data.Vector.Basic
List.Vector.instTraversableFlipNat : {n : ℕ} → Traversable (flip List.Vector n)
-- Mathlib.CategoryTheory.Adjunction.Evaluation
/-- The left adjoint of evaluation.  -/
CategoryTheory.evaluationLeftAdjoint : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        [∀ (a b : C), CategoryTheory.Limits.HasCoproductsOfShape (a ⟶ b) D] →
          C → CategoryTheory.Functor D (CategoryTheory.Functor C D)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.instPowNat : {X : AlgebraicGeometry.Scheme} → Pow X.IdealSheafData ℕ
-- Mathlib.Combinatorics.SimpleGraph.Partition
SimpleGraph.Partition.mk : {V : Type u} →
  {G : SimpleGraph V} →
    (parts : Set (Set V)) → Setoid.IsPartition parts → (∀ s ∈ parts, IsAntichain G.Adj s) → G.Partition
-- Mathlib.ModelTheory.Basic
/-- The identity equivalence from a structure to itself.  -/
FirstOrder.Language.Equiv.refl : (L : FirstOrder.Language) → (M : Type w) → [inst : L.Structure M] → L.Equiv M M
-- Mathlib.Data.NNReal.Defs
NNReal.val_eq_coe : ∀ (n : NNReal), ↑n = ↑n
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Colimits
PresheafOfModules.hasColimit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} {J : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} J] (F : CategoryTheory.Functor J (PresheafOfModules R))
  [∀ {X Y : Cᵒᵖ} (f : X ⟶ Y),
      CategoryTheory.Limits.PreservesColimit (F.comp (PresheafOfModules.evaluation R Y))
        (ModuleCat.restrictScalars (RingCat.Hom.hom (R.map f)))]
  [∀ (X : Cᵒᵖ), CategoryTheory.Limits.HasColimit (F.comp (PresheafOfModules.evaluation R X))],
  CategoryTheory.Limits.HasColimit F
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.instSliceableRccSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.instSliceableRccSlice._auto_1) →
      Std.Rcc.Sliceable (Std.TreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.Const.RccSlice α β)
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
IsLeftRegular.mem_nonZeroDivisorsLeft : ∀ {M₀ : Type u_2} [inst : MonoidWithZero M₀] {r : M₀}, IsLeftRegular r → r ∈ nonZeroDivisorsLeft M₀
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
instInhabitedArithmeticFunction : (R : Type u_1) → [inst : Zero R] → Inhabited (ArithmeticFunction R)
-- Mathlib.Geometry.Manifold.ContMDiffMap
/-- Bundled `n` times continuously differentiable maps,
denoted as `C^n(I, M; I', M')` and `C^n(I, M; k)` (when the target is a normed space `k` with
the trivial model) in the `Manifold` namespace.  -/
Manifold.«termC^_⟮_,_;_⟯» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Cones
/-- If `F` and `G` are naturally isomorphic functors, then they have equivalent categories of
cocones.
 -/
CategoryTheory.Limits.Cocone.precomposeEquivalence : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} → (F ≅ G) → (CategoryTheory.Limits.Cocone F ≌ CategoryTheory.Limits.Cocone G)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.div_one : ∀ (a : Ordinal.{u_4}), a / 1 = a
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.jacobian_reindex : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) {ι' : Type u_1} {σ' : Type u_2} (e : ι' ≃ ι) (f : σ' ≃ σ)
  [inst_3 : Finite σ] [inst_4 : Finite σ'], (P.reindex e f).jacobian = P.jacobian
-- Lean.Parser.Syntax
Lean.Parser.syntaxParser.formatter : optParam ℕ 0 → Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.ContainsIdentities.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C},
  (∀ (X : C), W (CategoryTheory.CategoryStruct.id X)) → W.ContainsIdentities
-- Mathlib.CategoryTheory.Comma.Arrow
/-- Create an isomorphism between arrows,
by providing isomorphisms between the domains and codomains,
and a proof that the square commutes.  -/
CategoryTheory.Arrow.isoMk : {T : Type u} →
  [inst : CategoryTheory.Category.{v, u} T] →
    {f g : CategoryTheory.Arrow T} →
      (l : f.left ≅ g.left) →
        (r : f.right ≅ g.right) →
          autoParam (CategoryTheory.CategoryStruct.comp l.hom g.hom = CategoryTheory.CategoryStruct.comp f.hom r.hom)
              CategoryTheory.Arrow.isoMk._auto_1 →
            (f ≅ g)
-- Init.Sym.Lemmas
Lean.Sym.Rat.eq_eq_true : ∀ (a b : ℚ), decide (a = b) = true → (a = b) = True
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CFC.sqrt_rpow : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : Ring A] [inst_2 : StarRing A] [inst_3 : TopologicalSpace A]
  [inst_4 : StarOrderedRing A] [inst_5 : Algebra ℝ A] [inst_6 : ContinuousFunctionalCalculus ℝ A IsSelfAdjoint]
  [inst_7 : NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A] [T2Space A] {a : A} {x : ℝ},
  IsUnit a → x ≠ 0 → CFC.sqrt (a ^ x) = a ^ (x / 2)
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.cosh_artanh : ∀ {x : ℝ}, x ∈ Set.Ioo (-1) 1 → Real.cosh (Real.artanh x) = 1 / √(1 - x ^ 2)
-- Init.Data.Int.LemmasAux
Int.lt_of_toNat_lt : ∀ {a b : ℤ}, a.toNat < b.toNat → a < b
-- Mathlib.CategoryTheory.Monoidal.Action.LinearFunctor
CategoryTheory.Functor.LaxLeftLinear.μₗ_naturality_right_assoc : ∀ {D : Type u_1} {D' : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} D}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D'} (F : CategoryTheory.Functor D D') {C : Type u_3}
  {inst_2 : CategoryTheory.Category.{v_3, u_3} C} {inst_3 : CategoryTheory.MonoidalCategory C}
  {inst_4 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D}
  {inst_5 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D'} [self : F.LaxLeftLinear C] (c : C) {d d' : D}
  (f : d ⟶ d') {Z : D'} (h : F.obj (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d') ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (F.map f))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d') h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.LaxLeftLinear.μₗ F c d)
      (CategoryTheory.CategoryStruct.comp
        (F.map (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c f)) h)
-- Mathlib.Algebra.Star.SelfAdjoint
selfAdjoint.val_smul : ∀ {R : Type u_1} {A : Type u_2} [inst : Star R] [inst_1 : TrivialStar R] [inst_2 : AddGroup A]
  [inst_3 : StarAddMonoid A] [inst_4 : SMul R A] [inst_5 : StarModule R A] (r : R) (x : ↥(selfAdjoint A)),
  ↑(r • x) = r • ↑x
-- Mathlib.SetTheory.Ordinal.Basic
OrderIso.ordinalType_congr : ∀ {α β : Type u_1} [inst : LinearOrder α] [inst_1 : LinearOrder β] [inst_2 : WellFoundedLT α] [inst_3 : WellFoundedLT β]
  (h : α ≃o β), (Ordinal.type fun x1 x2 => x1 < x2) = Ordinal.type fun x1 x2 => x1 < x2
-- Mathlib.Topology.UniformSpace.HeineCantor
/-- If `s` is compact and `f` is continuous at all points of `s`, then `f` is
"uniformly continuous at the set `s`", i.e. `f x` is close to `f y` whenever `x ∈ s` and `y` is
close to `x` (even if `y` is not itself in `s`, so this is a stronger assertion than
`UniformContinuousOn s`).  -/
IsCompact.uniformContinuousAt_of_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : UniformSpace β] {r : Set (β × β)} {s : Set α},
  IsCompact s →
    ∀ (f : α → β), (∀ a ∈ s, ContinuousAt f a) → r ∈ uniformity β → {x | x.1 ∈ s → (f x.1, f x.2) ∈ r} ∈ uniformity α
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.IProp.false : Mathlib.Tactic.ITauto.IProp
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.associator_inv_fst_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.SemiCartesianMonoidalCategory.fst (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
        (CategoryTheory.SemiCartesianMonoidalCategory.snd X Y)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.SemiCartesianMonoidalCategory.snd X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
      (CategoryTheory.SemiCartesianMonoidalCategory.fst Y Z)
-- Mathlib.Topology.Algebra.Group.Pointwise
IsClosed.add_closure_zero_eq : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {F : Set G},
  IsClosed F → F + closure {0} = F
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- A linear isometry preserves the inner product.  -/
LinearIsometry.inner_map_map : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {E' : Type u_7} [inst_3 : SeminormedAddCommGroup E'] [inst_4 : InnerProductSpace 𝕜 E'] (f : E →ₗᵢ[𝕜] E') (x y : E),
  inner 𝕜 (f x) (f y) = inner 𝕜 x y
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.contMDiff_diffeomorph_comp_iff : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {F : Type u_4}
  [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_5} [inst_7 : TopologicalSpace H]
  {H' : Type u_6} [inst_8 : TopologicalSpace H'] {G : Type u_7} [inst_9 : TopologicalSpace G]
  {I : ModelWithCorners 𝕜 E H} {I' : ModelWithCorners 𝕜 E' H'} {J : ModelWithCorners 𝕜 F G} {M : Type u_9}
  [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H M] {M' : Type u_10} [inst_12 : TopologicalSpace M']
  [inst_13 : ChartedSpace H' M'] {N : Type u_11} [inst_14 : TopologicalSpace N] [inst_15 : ChartedSpace G N]
  {n m : WithTop ℕ∞} (h : Diffeomorph I J M N n) {f : M' → M}, m ≤ n → (ContMDiff I' J m (⇑h ∘ f) ↔ ContMDiff I' I m f)
-- Batteries.Lean.AttributeExtra
Lean.TagAttributeExtra.mk.inj : ∀ {ext : Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet} {base : Lean.NameHashSet}
  {ext_1 : Lean.PersistentEnvExtension Lean.Name Lean.Name Lean.NameSet} {base_1 : Lean.NameHashSet},
  { ext := ext, base := base } = { ext := ext_1, base := base_1 } → ext = ext_1 ∧ base = base_1
-- Aesop.RuleTac.Tactic
Aesop.RuleTac.ruleTac : Lean.Name → Aesop.RuleTac
-- Std.Sync.Barrier
/-- Blocks the current thread until all threads have rendezvoused here.

Barriers are re-usable after all threads have rendezvoused once, and can be used continuously.

A single (arbitrary) thread will receive `true` when returning from this function, and all other
threads will receive `false`.
 -/
Std.Barrier.wait : Std.Barrier → BaseIO Bool
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.add.eq_1 : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (q₁ q₂ : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.add q₁ q₂ =
    q₁.liftOn₂ q₂
      (fun x x_1 =>
        match x with
        | (a, b) =>
          match x_1 with
          | (c, d) => Lean.Grind.Ring.OfSemiring.Q.mk (a + c, b + d))
      ⋯
-- Mathlib.RingTheory.Valuation.Extension
Valuation.HasExtension.instLiesOverSubtypeMemValuationSubringValuationSubringMaximalIdeal : ∀ {K : outParam (Type u_5)} {L : outParam (Type u_6)} {Γ₀ : outParam (Type u_7)} {Γ₁ : outParam (Type u_8)}
  [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] [inst_3 : LinearOrderedCommGroupWithZero Γ₀]
  [inst_4 : LinearOrderedCommGroupWithZero Γ₁] (vK : Valuation K Γ₀) (vL : Valuation L Γ₁)
  [inst_5 : vK.HasExtension vL],
  (IsLocalRing.maximalIdeal ↥vL.valuationSubring).LiesOver (IsLocalRing.maximalIdeal ↥vK.valuationSubring)
-- Std.Http.Protocol.H1
/-- Conditionally enqueues an event when present (`some`), otherwise leaves events
unchanged.
 -/
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.setEvent : {dir : Std.Http.Protocol.H1.Direction} →
  Std.Http.Protocol.H1.Machine dir → Option (Std.Http.Protocol.H1.Event dir) → Std.Http.Protocol.H1.Machine dir
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.instSub : {R : Type u_1} →
  {V : Type u_2} →
    {W : Type u_3} →
      {P : Type u_4} →
        [inst : Ring R] →
          [inst_1 : AddCommGroup V] →
            [inst_2 : Module R V] →
              [inst_3 : TopologicalSpace P] →
                [inst_4 : AddTorsor V P] →
                  [inst_5 : AddCommGroup W] →
                    [inst_6 : Module R W] → [inst_7 : TopologicalSpace W] → [IsTopologicalAddGroup W] → Sub (P →ᴬ[R] W)
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.ofLE_refl_apply : ∀ {X : Type u_2} [inst : TopologicalSpace X] {A : DiscreteQuotient X} (a : Quotient A.toSetoid),
  DiscreteQuotient.ofLE ⋯ a = a
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- Monomials are weighted homogeneous.  -/
MvPolynomial.isWeightedHomogeneous_monomial : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M] (w : σ → M)
  (d : σ →₀ ℕ) (r : R) {m : M},
  (Finsupp.weight w) d = m → MvPolynomial.IsWeightedHomogeneous w ((MvPolynomial.monomial d) r) m
-- Mathlib.Algebra.GroupWithZero.Units.Basic
Units.val_mk0 : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {a : G₀} (h : a ≠ 0), ↑(Units.mk0 a h) = a
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.product_add_product_comm : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : Add α] [inst_2 : Add β] [inst_3 : DecidableEq β]
  (s₁ s₂ : Finset α) (t₁ t₂ : Finset β), s₁ ×ˢ t₁ + s₂ ×ˢ t₂ = (s₁ + s₂) ×ˢ (t₁ + t₂)
-- Mathlib.Analysis.Normed.Operator.Basic
/-- Given a unit-length element `x` of a normed space `E` over a field `𝕜`, the natural linear
isometry map from `𝕜` to `E` by taking multiples of `x`.  -/
LinearIsometry.toSpanSingleton : (𝕜 : Type u_1) →
  (E : Type u_4) →
    [inst : SeminormedAddCommGroup E] →
      [inst_1 : NontriviallyNormedField 𝕜] → [inst_2 : NormedSpace 𝕜 E] → {v : E} → ‖v‖ = 1 → 𝕜 →ₗᵢ[𝕜] E
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.instInhabited : {M : Type u_4} → [inst : Add M] → Inhabited (M ≃+ M)
-- Std.Http.Data.Body.Stream
/-- Returns `true` when a consumer is currently blocked waiting for data.
 -/
Std.Http.Body.Stream.hasInterest : Std.Http.Body.Stream → Std.Async.Async Bool
-- Mathlib.Algebra.Group.WithOne.Defs
WithOne.coe_ne_one : ∀ {α : Type u} {a : α}, ↑a ≠ 1