mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.EMetricSpace.BoundedVariation
LipschitzOnWith.locallyBoundedVariationOn : ∀ {E : Type u_2} [inst : PseudoEMetricSpace E] {f : ℝ → E} {C : NNReal} {s : Set ℝ},
  LipschitzOnWith C f s → LocallyBoundedVariationOn f s
-- Mathlib.Topology.ContinuousMap.Bounded.Basic
/-- The indicator function of a clopen set, as a bounded continuous function.  -/
BoundedContinuousFunction.indicator : {α : Type u} → [inst : TopologicalSpace α] → (s : Set α) → IsClopen s → BoundedContinuousFunction α ℝ
-- Mathlib.Topology.Algebra.Monoid
/-- If multiplication is separately continuous in `α`, then it also is in `αᵐᵒᵖ`.  -/
MulOpposite.instSeparatelyContinuousMul : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : Mul α] [SeparatelyContinuousMul α], SeparatelyContinuousMul αᵐᵒᵖ
-- Init.Prelude
/-- Unsigned 8-bit integers.

This type has special support in the compiler so it can be represented by an unboxed 8-bit value
rather than wrapping a `BitVec 8`.
 -/
UInt8 : Type
-- Mathlib.Algebra.Group.Hom.Instances
AddMonoidHom.compl₂_apply : ∀ {M : Type uM} {N : Type uN} {P : Type uP} {Q : Type uQ} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddZeroClass Q] (f : M →+ N →+ P) (g : Q →+ N) (m : M) (q : Q),
  ((f.compl₂ g) m) q = (f m) (g q)
-- Mathlib.Combinatorics.SimpleGraph.Cayley
SimpleGraph.addCayley_monotone : ∀ {M : Type u_1} [inst : Add M], Monotone fun x => SimpleGraph.addCayley x
-- Mathlib.Analysis.Calculus.FDeriv.Mul
/-- Eta-expanded form of `HasFDerivAt.smul` -/
HasFDerivAt.fun_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {x : E} {𝕜' : Type u_5} [inst_5 : NormedRing 𝕜'] [inst_6 : NormedAlgebra 𝕜 𝕜'] [inst_7 : Module 𝕜' F]
  [inst_8 : IsBoundedSMul 𝕜' F] [inst_9 : IsScalarTower 𝕜 𝕜' F] {c : E → 𝕜'} {c' : E →L[𝕜] 𝕜'},
  HasFDerivAt c c' x → HasFDerivAt f f' x → HasFDerivAt (fun i => c i • f i) (c x • f' + c'.smulRight (f x)) x
-- Init.Data.Order.Ord
Std.OrientedCmp.isLE_antisymm : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.OrientedCmp cmp] {a b : α},
  (cmp a b).isLE = true → (cmp b a).isLE = true → cmp a b = Ordering.eq
-- Mathlib.CategoryTheory.Limits.Weighted.HasWeightedLimit
CategoryTheory.Functor.weightedLimObjMap_π_assoc : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  (W : CategoryTheory.Functor J (Type w)) {F₁ F₂ : CategoryTheory.Functor J C}
  [inst_2 : CategoryTheory.Limits.HasWeightedLimit W F₁] [inst_3 : CategoryTheory.Limits.HasWeightedLimit W F₂]
  (f : F₁ ⟶ F₂) ⦃j : J⦄ (x : W.obj j) {Z : C} (h : F₂.obj j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (W.weightedLimObjMap f)
      (CategoryTheory.CategoryStruct.comp (W.weightedLimObjObjπ F₂ x) h) =
    CategoryTheory.CategoryStruct.comp (W.weightedLimObjObjπ F₁ x) (CategoryTheory.CategoryStruct.comp (f.app j) h)
-- Init.Data.SInt.Lemmas
UInt16.toInt16_neg : ∀ (a : UInt16), (-a).toInt16 = -a.toInt16
-- Lean.Meta.Tactic.FunIndInfo
Lean.Meta.FunIndParamKind.noConfusionType : Sort v✝ → Lean.Meta.FunIndParamKind → Lean.Meta.FunIndParamKind → Sort v✝
-- Aesop.Stats.Basic
Aesop.GoalKind : Type
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.norm_eq_of_associated : ∀ {d : ℤ}, d ≤ 0 → ∀ {x y : ℤ√d}, Associated x y → x.norm = y.norm
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- See also `Finset.prod_ite_zero`.  -/
Finset.prod_ite_one : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (s : Finset ι) (p : ι → Prop) [inst_1 : DecidablePred p],
  (∀ i ∈ s, ∀ j ∈ s, p i → p j → i = j) → ∀ (a : M), (∏ i ∈ s, if p i then a else 1) = if ∃ i ∈ s, p i then a else 1
-- Mathlib.GroupTheory.FreeAbelianGroup
FreeAbelianGroup.liftMonoid_coe : ∀ {α : Type u} {R : Type u_2} [inst : Monoid α] [inst_1 : Ring R] (f : α →* R),
  ⇑(FreeAbelianGroup.liftMonoid f) = ⇑(FreeAbelianGroup.lift ⇑f)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ofIsInitialLeft_inl : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)) {X₁ Y₁ : C₁} (f₁ : X₁ ⟶ Y₁) {X₂ Y₂ : C₂} (f₂ : X₂ ⟶ Y₂)
  [inst_3 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.flip.obj X₂)]
  [inst_4 : CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) (F.flip.obj Y₂)]
  (h : CategoryTheory.Limits.IsInitial X₁),
  (CategoryTheory.Functor.PushoutObjObj.ofIsInitialLeft F f₁ f₂ h).inl =
    CategoryTheory.CategoryStruct.id ((F.obj Y₁).obj X₂)
-- Mathlib.Analysis.SpecialFunctions.Pow.Asymptotics
Asymptotics.IsBigO.sqrt : ∀ {α : Type u_1} {l : Filter α} {f g : α → ℝ}, f =O[l] g → 0 ≤ᶠ[l] g → (fun x => √(f x)) =O[l] fun x => √(g x)
-- Mathlib.NumberTheory.ModularForms.QExpansion
ModularForm.qExpansion_add : ∀ {F : Type u_1} [inst : FunLike F UpperHalfPlane ℂ] {Γ : Subgroup (GL (Fin 2) ℝ)} {h : ℝ} {G : Type u_2}
  [inst_1 : FunLike G UpperHalfPlane ℂ],
  0 < h →
    h ∈ Γ.strictPeriods →
      ∀ {a b : ℤ} (f : F) [ModularFormClass F Γ a] (g : G) [ModularFormClass G Γ b],
        UpperHalfPlane.qExpansion h (⇑f + ⇑g) = UpperHalfPlane.qExpansion h ⇑f + UpperHalfPlane.qExpansion h ⇑g
-- Aesop.Forward.RuleInfo
Aesop.instBEqSlot : BEq Aesop.Slot
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.map_reindex_assoc : ∀ {n₁ n₂ : Type u} (i : n₁ → n₂) {S T : AlgebraicGeometry.Scheme} (f : S ⟶ T) {Z : AlgebraicGeometry.Scheme}
  (h : AlgebraicGeometry.AffineSpace n₁ T ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.map n₂ f)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.reindex i T) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.reindex i S)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.map n₁ f) h)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.instAddGroup.eq_1 : ∀ {α : Type u},
  FreeAddGroup.instAddGroup =
    { toAdd := FreeAddGroup.instAdd, add_assoc := ⋯, toZero := FreeAddGroup.instZero, zero_add := ⋯, add_zero := ⋯,
      nsmul := nsmulRecAuto, nsmul_zero := ⋯, nsmul_succ := ⋯, toNeg := FreeAddGroup.instNeg, sub := SubNegMonoid.sub',
      zsmul := zsmulRec, sub_eq_add_neg := ⋯, zsmul_zero' := ⋯, zsmul_succ' := ⋯, zsmul_neg' := ⋯, neg_add_cancel := ⋯ }
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.lift_add : ∀ (a b : Cardinal.{u}), Cardinal.lift.{v, u} (a + b) = Cardinal.lift.{v, u} a + Cardinal.lift.{v, u} b
-- Lean.Parser.Term
/-- Configuration options for tactics, commands, and other elaborators.  -/
Lean.Parser.Term.optConfig : Lean.Parser.Parser
-- Mathlib.MeasureTheory.Constructions.Polish.Basic
/-- If one Polish topology on a type refines another, they have the same Borel sets.  -/
MeasureTheory.borel_eq_borel_of_le : ∀ {γ : Type u_3} {t t' : TopologicalSpace γ}, PolishSpace γ → PolishSpace γ → t ≤ t' → borel γ = borel γ
-- Mathlib.NumberTheory.Modular
/-- The points on the fundamental domain that aren't on the bottom "arc"
are in the closure of the open fundamental domain.
 -/
_private.Mathlib.NumberTheory.Modular.0.ModularGroup.mem_closure_of_one_lt_norm : ∀ {x : UpperHalfPlane}, 1 < ‖↑x‖ → |x.re| ≤ 1 / 2 → x ∈ closure ModularGroup.fdo
-- Mathlib.Algebra.Group.Subgroup.Map
Subgroup.comap_toSubmonoid : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (e : G ≃* N) (s : Subgroup N),
  (Subgroup.comap (↑e) s).toSubmonoid = Submonoid.comap e.toMonoidHom s.toSubmonoid
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.isEmpty_alter_eq_isEmpty_erase : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  {f : Option (β k) → Option (β k)}, (m.alter k f).isEmpty = ((m.erase k).isEmpty && (f (m.get? k)).isNone)
-- Mathlib.CategoryTheory.Bicategory.Yoneda
CategoryTheory.Bicategory.yoneda_mapComp_inv_as_app_toNatTrans_app : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} (f : a ⟶ b) (g : b ⟶ c) (a_1 : Bᵒᵖ)
  (X : ↑(CategoryTheory.Cat.of (Opposite.unop a_1 ⟶ a))),
  ((CategoryTheory.Bicategory.yoneda.mapComp f g).inv.as.app a_1).toNatTrans.app X =
    (CategoryTheory.Bicategory.associator X f g).hom
-- Mathlib.GroupTheory.Submonoid.Centralizer
AddSubmonoid.centralizer.eq_1 : ∀ {M : Type u_1} (S : Set M) [inst : AddMonoid M],
  AddSubmonoid.centralizer S = { carrier := S.addCentralizer, add_mem' := ⋯, zero_mem' := ⋯ }
-- Mathlib.CategoryTheory.Sites.Coherent.ExtensiveSheaves
CategoryTheory.Presieve.Extensive.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : C} {R : CategoryTheory.Presieve X},
  (∃ α,
      ∃ (_ : Finite α),
        ∃ Z π,
          R = CategoryTheory.Presieve.ofArrows Z π ∧
            Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk X π))) →
    R.Extensive
-- Aesop.Rule.Name
_private.Aesop.Rule.Name.0.Aesop.RuleName.Json : Type
-- Init.Data.Option.Lemmas
Option.dite_none_left_eq_some : ∀ {β : Type u_1} {a : β} {p : Prop} {x : Decidable p} {b : ¬p → Option β},
  (if h : p then none else b h) = some a ↔ ∃ (h : ¬p), b h = some a
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
/-- Given a trifunctor `F : C₁ ⥤ C₂ ⥤ C₃ ⥤ C₄`, a map `p : I₁ × I₂ × I₃ → J`, and
graded objects `X₁ : GradedObject I₁ C₁`, `X₂ : GradedObject I₂ C₂` and `X₃ : GradedObject I₃ C₃`,
this is the `J`-graded object sending `j` to the coproduct of
`((F.obj (X₁ i₁)).obj (X₂ i₂)).obj (X₃ i₃)` for `p ⟨i₁, i₂, i₃⟩ = j`.  -/
CategoryTheory.GradedObject.mapTrifunctorMapFunctorObj : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    {C₃ : Type u_3} →
      {C₄ : Type u_4} →
        [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
          [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
            [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃] →
              [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄] →
                (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₄))) →
                  {I₁ : Type u_7} →
                    {I₂ : Type u_8} →
                      {I₃ : Type u_9} →
                        {J : Type u_10} →
                          (p : I₁ × I₂ × I₃ → J) →
                            (X₁ : CategoryTheory.GradedObject I₁ C₁) →
                              [∀ (X₂ : CategoryTheory.GradedObject I₂ C₂) (X₃ : CategoryTheory.GradedObject I₃ C₃),
                                    ((((CategoryTheory.GradedObject.mapTrifunctor F I₁ I₂ I₃).obj X₁).obj X₂).obj
                                          X₃).HasMap
                                      p] →
                                CategoryTheory.Functor (CategoryTheory.GradedObject I₂ C₂)
                                  (CategoryTheory.Functor (CategoryTheory.GradedObject I₃ C₃)
                                    (CategoryTheory.GradedObject J C₄))
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.ofLEMk_comp_ofMkLEMk_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} (X : CategoryTheory.Subobject B) (f : A₁ ⟶ B)
  [inst_1 : CategoryTheory.Mono f] (g : A₂ ⟶ B) [inst_2 : CategoryTheory.Mono g]
  (h₁ : X ≤ CategoryTheory.Subobject.mk f) (h₂ : CategoryTheory.Subobject.mk f ≤ CategoryTheory.Subobject.mk g) {Z : C}
  (h : A₂ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.ofLEMk f h₁)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Subobject.ofMkLEMk f g h₂) h) =
    CategoryTheory.CategoryStruct.comp (X.ofLEMk g ⋯) h
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.ExcenterExists.sSameSide_excenter_point_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {signs : Finset (Fin (n + 1))},
  s.ExcenterExists signs →
    ∀ {i : Fin (n + 1)},
      (affineSpan ℝ (Set.range (s.faceOpposite i).points)).SSameSide (s.excenter signs) (s.points i) ↔
        0 < s.excenterWeights signs i
-- Mathlib.AlgebraicGeometry.AffineSpace
/-- `𝔸(n; S)` is functorial w.r.t. `S`.  -/
AlgebraicGeometry.AffineSpace.map : (n : Type u) →
  {S T : AlgebraicGeometry.Scheme} → (S ⟶ T) → (AlgebraicGeometry.AffineSpace n S ⟶ AlgebraicGeometry.AffineSpace n T)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.isColimitCoconeWithTop`.

---

If `J : CardinalDirectedPoset κ` and `κ'` is any regular cardinal,
then `J.withTop` is the `κ'`-filtered colimit of its subsets that are of
cardinality `< κ'` and contain `⊤`.  -/
CategoryTheory.CardinalFilteredPoset.isColimitCoconeWithTop : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    (J : CategoryTheory.CardinalDirectedPoset κ) →
      (κ' : Cardinal.{u}) → [inst_1 : Fact κ'.IsRegular] → CategoryTheory.Limits.IsColimit (J.coconeWithTop κ')
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instInhabitedPosition : Inhabited Lean.Lsp.Position
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.extend_eq : ∀ {α : Type u_2} {P : α → Prop} (m : (s : α) → P s → ENNReal) {s : α} (h : P s), MeasureTheory.extend m s = m s h
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.fromOpcycles_H_map_twoδ₁Toδ₀_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (fg : i ⟶ k)
  (h : CategoryTheory.CategoryStruct.comp f g = fg) (n : ℤ) {Z : C}
  (h_1 : (X.H n).obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.fromOpcycles f g fg h n)
      (CategoryTheory.CategoryStruct.comp ((X.H n).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀ f g fg h)) h_1) =
    CategoryTheory.CategoryStruct.comp 0 h_1
-- Mathlib.Order.Atoms
BooleanAlgebra.eq_iff_atom_le_iff : ∀ {α : Type u_4} [inst : BooleanAlgebra α] [IsAtomic α] {x y : α}, x = y ↔ ∀ (a : α), IsAtom a → (a ≤ x ↔ a ≤ y)
-- Mathlib.Probability.IdentDistrib
ProbabilityTheory.IdentDistrib.integrable_snd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  [inst_2 : MeasurableSpace γ] {μ : MeasureTheory.Measure α} {ν : MeasureTheory.Measure β} {f : α → γ} {g : β → γ}
  [inst_3 : NormedAddCommGroup γ] [BorelSpace γ],
  ProbabilityTheory.IdentDistrib f g μ ν → MeasureTheory.Integrable f μ → MeasureTheory.Integrable g ν
-- Lean.Meta.Closure
Lean.Meta.Closure.mkValueTypeClosureAux : Lean.Expr → Lean.Expr → Lean.Meta.Closure.ClosureM (Lean.Expr × Lean.Expr)
-- Init.Data.Nat.Dvd
Nat.zero_dvd : ∀ {n : ℕ}, 0 ∣ n ↔ n = 0
-- Init.Data.SInt.Basic
instMulInt8 : Mul Int8
-- Mathlib.Data.Finmap
Finmap.keysLookupEquiv_symm_apply_lookup : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] (f : { f // ∀ (i : α), (f.2 i).isSome = true ↔ i ∈ f.1 })
  (a : α), Finmap.lookup a (Finmap.keysLookupEquiv.symm f) = (↑f).2 a
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.single_mem_span_single : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [Nontrivial R] {m : M} {s : Set M},
  MonoidAlgebra.single m 1 ∈ Submodule.span R ((fun x => MonoidAlgebra.single x 1) '' s) ↔ m ∈ s
-- Mathlib.LinearAlgebra.LinearIndependent.BaseChange
linearIndependent_algebraMap_comp_iff : ∀ {ι : Type u_1} {ι' : Type u_2} [Finite ι'] {R : Type u_3} {S : Type u_4} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : Algebra R S] [FaithfulSMul R S] [IsDomain S] {v : ι → ι' → R},
  (LinearIndependent S fun i => ⇑(algebraMap R S) ∘ v i) ↔ LinearIndependent R v
-- Mathlib.LinearAlgebra.Matrix.InvariantBasisNumber
/-- The rank condition is left-right symmetric. Note that the strong rank condition
is not left-right symmetric, see Remark (1.32) in §1.1D of [lam_1999].  -/
MulOpposite.rankCondition_iff : ∀ {R : Type u_1} [inst : Semiring R], RankCondition Rᵐᵒᵖ ↔ RankCondition R
-- Mathlib.Combinatorics.Compactness
/-- Given a (dependent) function `g s : (a : s) → β a` for each finset `s` of `α`, provided that
each `β a` is finite, we can find another function `χ : (a : α) → β a` such that on every `s`,
there is some larger `t` such that `χ` agrees with `g t` on `s`.
Informally, we are stitching together the local functions `g s` into a global `χ` such that on
each `s`, `χ` can be expressed in terms of one of the `g`.
 -/
Finset.rado_selection_subtype : ∀ {α : Type u_1} {β : α → Type u_2} [∀ (a : α), Finite (β a)] (g : (s : Finset α) → (a : ↥s) → β ↑a),
  ∃ χ, ∀ (s : Finset α), ∃ t, ∃ (hst : s ⊆ t), ∀ (x : ↥s), χ ↑x = g t (Set.inclusion hst x)
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- The natural equivalence between continuous linear maps from `M₂` to `M₃`
and continuous 1-multilinear maps from `M₂` to `M₃`.  -/
ContinuousMultilinearMap.ofSubsingleton : (R : Type u) →
  {ι : Type v} →
    (M₂ : Type w₂) →
      (M₃ : Type w₃) →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M₂] →
            [inst_2 : AddCommMonoid M₃] →
              [inst_3 : Module R M₂] →
                [inst_4 : Module R M₃] →
                  [inst_5 : TopologicalSpace M₂] →
                    [inst_6 : TopologicalSpace M₃] →
                      [Subsingleton ι] → ι → (M₂ →L[R] M₃) ≃ ContinuousMultilinearMap R (fun x => M₂) M₃
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.lidIsometry_eq_ridIsometry : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜], TensorProduct.lidIsometry 𝕜 𝕜 = TensorProduct.ridIsometry 𝕜 𝕜
-- Mathlib.Algebra.Ring.Opposite
AddOpposite.instNatCast.eq_1 : ∀ {R : Type u_1} [inst : NatCast R], AddOpposite.instNatCast = { natCast := fun n => AddOpposite.op ↑n }
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.ofCompIso_m : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y} {Y' : C} {g : Y ⟶ Y'}
  [inst_1 : CategoryTheory.IsIso g]
  (F : CategoryTheory.Limits.MonoFactorisation (CategoryTheory.CategoryStruct.comp f g)),
  F.ofCompIso.m = CategoryTheory.CategoryStruct.comp F.m (CategoryTheory.inv g)
-- Mathlib.Algebra.Regular.Basic
/-- Two elements `a` and `b` are add-regular if and only if both sums `a + b` and
`b + a` are add-regular.  -/
isAddRegular_add_and_add_iff : ∀ {R : Type u_1} [inst : AddSemigroup R] {a b : R},
  IsAddRegular (a + b) ∧ IsAddRegular (b + a) ↔ IsAddRegular a ∧ IsAddRegular b
-- Mathlib.Data.Multiset.Functor
Multiset.traverse_map : ∀ {G : Type u_1 → Type u_1} [inst : Applicative G] [inst_1 : CommApplicative G] {α β γ : Type u_1} (g : α → β)
  (h : β → G γ) (x : Multiset α), Multiset.traverse h (Multiset.map g x) = Multiset.traverse (h ∘ g) x
-- Mathlib.Data.Sum.Basic
Sum.update_inl_comp_inr : ∀ {α : Type u} {β : Type v} {γ : Type u_1} [inst : DecidableEq (α ⊕ β)] {f : α ⊕ β → γ} {i : α} {x : γ},
  Function.update f (Sum.inl i) x ∘ Sum.inr = f ∘ Sum.inr
-- Mathlib.Topology.Algebra.Group.Torsor
Homeomorph.coe_pointReflection : ∀ {V : Type u_4} {P : Type u_5} [inst : AddGroup V] [inst_1 : TopologicalSpace V] [inst_2 : AddTorsor V P]
  [inst_3 : TopologicalSpace P] [inst_4 : IsTopologicalAddTorsor P] (p : P),
  ⇑(Homeomorph.pointReflection p) = ⇑(Equiv.pointReflection p)
-- Mathlib.Data.Set.Function
Set.BijOn.congr : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f₁ f₂ : α → β},
  Set.BijOn f₁ s t → Set.EqOn f₁ f₂ s → Set.BijOn f₂ s t
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₄_of_isCharNeTwoNF : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsCharNeTwoNF], W.c₄ = 16 * W.a₂ ^ 2 - 48 * W.a₄
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.succ_zero : Order.succ 0 = 1
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- The indexed supremum of a function is bounded above by a uniform bound  -/
ciSup_le : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] [Nonempty ι] {f : ι → α} {c : α},
  (∀ (x : ι), f x ≤ c) → iSup f ≤ c
-- Mathlib.Analysis.Convex.Jensen
/-- Convex **Jensen's inequality**, `Finset.sum` version.  -/
ConvexOn.map_sum_le : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} {ι : Type u_5} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : PartialOrder β]
  [IsOrderedAddMonoid β] [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {s : Set E} {f : E → β}
  {t : Finset ι} {w : ι → 𝕜} {p : ι → E},
  ConvexOn 𝕜 s f →
    (∀ i ∈ t, 0 ≤ w i) → ∑ i ∈ t, w i = 1 → (∀ i ∈ t, p i ∈ s) → f (∑ i ∈ t, w i • p i) ≤ ∑ i ∈ t, w i • f (p i)
-- Mathlib.Topology.Separation.CompletelyRegular
isDenseEmbedding_stoneCechUnit : ∀ {X : Type u} [inst : TopologicalSpace X] [T35Space X], IsDenseEmbedding stoneCechUnit
-- Init.WF
Subrelation.accessible : ∀ {α : Sort u} {r q : α → α → Prop} {a : α}, Subrelation q r → Acc r a → Acc q a
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
ModularForm.E₄_qExpansion_coeff_one : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ⇑ModularForm.E₄) = 240
-- Mathlib.Analysis.Complex.AbelLimit
Complex.stolzCone_subset_stolzSet_aux : ∀ {s : ℝ}, 0 < s → ∃ M ε, 0 < M ∧ 0 < ε ∧ {z | 1 - ε < z.re} ∩ Complex.stolzCone s ⊆ Complex.stolzSet M
-- Mathlib.Algebra.Notation.Prod
Prod.swap_one : ∀ {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N], Prod.swap 1 = 1
-- Mathlib.Analysis.Matrix.Normed
Matrix.nnnorm_diagonal : ∀ {n : Type u_4} {α : Type u_5} [inst : Fintype n] [inst_1 : SeminormedAddCommGroup α] [inst_2 : DecidableEq n]
  (v : n → α), ‖Matrix.diagonal v‖₊ = ‖v‖₊
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
CategoryTheory.Limits.IsZero.of_full_of_faithful_of_isZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) [F.Full] [F.Faithful] (X : C),
  CategoryTheory.Limits.IsZero (F.obj X) → CategoryTheory.Limits.IsZero X
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.NeWord.append_last : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] {i j k l : ι} {w₁ : Monoid.CoprodI.NeWord M i j}
  {hne : j ≠ k} {w₂ : Monoid.CoprodI.NeWord M k l}, (w₁.append hne w₂).last = w₂.last
-- Mathlib.Algebra.Homology.ShortComplex.ConcreteCategory
CategoryTheory.ShortComplex.i_cyclesMk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [inst_3 : CategoryTheory.HasForget₂ C Ab] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : (CategoryTheory.forget₂ C Ab).Additive] [inst_6 : (CategoryTheory.forget₂ C Ab).PreservesHomology]
  (S : CategoryTheory.ShortComplex C) [inst_7 : S.HasHomology] (x₂ : ↑((CategoryTheory.forget₂ C Ab).obj S.X₂))
  (hx₂ : (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map S.g)) x₂ = 0),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.forget₂ C Ab).map S.iCycles)) (S.cyclesMk x₂ hx₂) = x₂
-- Mathlib.RingTheory.Algebraic.Integral
IsAlgebraic.of_smul : ∀ {R : Type u_1} {A : Type u_3} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {z : A} {y : R},
  y ∈ nonZeroDivisors R → IsAlgebraic R (y • z) → IsAlgebraic R z
-- Mathlib.Algebra.Group.Subgroup.Pointwise
AddSubgroup.addConj_mem_sup_of_mem_inf_normalizer_of_mem_inf : ∀ {G : Type u_2} [inst : AddGroup G] {H K : AddSubgroup G} {s : G},
  s ∈ AddSubgroup.normalizer ↑H ⊓ AddSubgroup.normalizer ↑K → ∀ g ∈ H ⊔ K, s + g + -s ∈ H ⊔ K
-- Mathlib.Order.Hom.Basic
/-- To define an order embedding from a partial order to a preorder it suffices to give a function
together with a proof that it satisfies `f a ≤ f b ↔ a ≤ b`.
 -/
OrderEmbedding.ofMapLEIff : {α : Type u_6} →
  {β : Type u_7} →
    [inst : PartialOrder α] → [inst_1 : Preorder β] → (f : α → β) → (∀ (a b : α), f a ≤ f b ↔ a ≤ b) → α ↪o β
-- Init.Data.Option.Lemmas
Option.filter_pmap : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} {p : α → Prop} {f : (a : α) → p a → β} {h : ∀ (a : α), o = some a → p a}
  {q : β → Bool}, Option.filter q (Option.pmap f o h) = Option.pmap f (o.pfilter fun a h' => q (f a ⋯)) ⋯