mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.Modules.Tilde
/-- Given a presentation of a module `M`, we may construct an associated presentation of `M^~`.  -/
AlgebraicGeometry.presentationTilde : {R : CommRingCat} →
  (M : ModuleCat ↑R) →
    (s : Set ↑M) →
      Submodule.span (↑R) s = ⊤ →
        (t : Set (↑s →₀ ↑R)) →
          Submodule.span (↑R) t = (Finsupp.linearCombination (↑R) Subtype.val).ker →
            SheafOfModules.Presentation (AlgebraicGeometry.tilde M)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
hasSum_nat_add_iff' : ∀ {G : Type u_2} [inst : AddCommGroup G] {g : G} [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G}
  (k : ℕ), HasSum (fun n => f (n + k)) (g - ∑ i ∈ Finset.range k, f i) ↔ HasSum f g
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.symm_eq_on_of_inter_eq_of_eqOn : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} {e' : PartialEquiv α β},
  e.IsImage s t →
    e.source ∩ s = e'.source ∩ s → Set.EqOn (↑e) (↑e') (e.source ∩ s) → Set.EqOn (↑e.symm) (↑e'.symm) (e.target ∩ t)
-- Init.Data.Iterators.Consumers.Monadic.Partial
/-- A wrapper around an iterator that provides partial consumers. See `IterM.allowNontermination`.
 -/
Std.IterM.Partial : {α : Type w} → (Type w → Type w') → Type w → Type w
-- Mathlib.Order.WithBot
WithBot.coe_le : ∀ {α : Type u_1} {a b : α} [inst : LE α] {o : Option α}, b ∈ o → (↑a ≤ o ↔ a ≤ b)
-- Lean.Meta.Tactic.Grind.Arith.CommRing.Types
Lean.Meta.Grind.Arith.CommRing.EqCnstr : Type
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
/-- The `Cardinal` rank function is submodular.  -/
Matroid.cRk_inter_add_cRk_union_le : ∀ {α : Type u} (M : Matroid α) [M.InvariantCardinalRank] (X Y : Set α),
  M.cRk (X ∩ Y) + M.cRk (X ∪ Y) ≤ M.cRk X + M.cRk Y
-- Qq.Macro
/-- Maps free variables in the new context to levels in the old context (of type Level)  -/
Qq.Impl.UnquoteState.levelBackSubst : Qq.Impl.UnquoteState → Std.HashMap Lean.Level Lean.Expr
-- Mathlib.Algebra.Order.Ring.Cone
RingCone.coe_set_mk : ∀ {R : Type u_1} [inst : Ring R] {toSubsemiring : Subsemiring R}
  (eq_zero_of_mem_of_neg_mem : ∀ {a : R}, a ∈ toSubsemiring.carrier → -a ∈ toSubsemiring.carrier → a = 0),
  ↑{ toSubsemiring := toSubsemiring, eq_zero_of_mem_of_neg_mem' := eq_zero_of_mem_of_neg_mem } = ↑toSubsemiring
-- Mathlib.GroupTheory.Coprod.Basic
AddEquiv.coprodCongr.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {M' : Type u_3} {N' : Type u_4} [inst : AddZeroClass M] [inst_1 : AddZeroClass N]
  [inst_2 : AddZeroClass M'] [inst_3 : AddZeroClass N'] (e : M ≃+ N) (e' : M' ≃+ N'),
  e.coprodCongr e' = (AddMonoid.Coprod.map ↑e ↑e').toAddEquiv (AddMonoid.Coprod.map ↑e.symm ↑e'.symm) ⋯ ⋯
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get!_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [inst : LawfulBEq α] {k : α}
  [inst_1 : Inhabited (β k)], k ∉ m₁ → (m₁ ∪ m₂).get! k = m₂.get! k
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.covering_iff_covers_id : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} (J : CategoryTheory.GrothendieckTopology C)
  (S : CategoryTheory.Sieve X), S ∈ J X ↔ J.Covers S (CategoryTheory.CategoryStruct.id X)
-- Init.Data.UInt.Lemmas
UInt16.toUInt32_toUSize : ∀ (n : UInt16), n.toUSize.toUInt32 = n.toUInt32
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforwardCongr_symm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] {φ ψ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R} (e : φ = ψ),
  (SheafOfModules.pushforwardCongr e).symm = SheafOfModules.pushforwardCongr ⋯
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.toListModel_modify : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α] [inst_3 : BEq α]
  [inst_4 : Std.LawfulBEqOrd α] {t : Std.DTreeMap.Internal.Impl α β} {a : α} {f : β a → β a},
  t.Balanced →
    t.Ordered →
      (Std.DTreeMap.Internal.Impl.modify a f t).toListModel.Perm (Std.Internal.List.modifyKey a f t.toListModel)
-- Mathlib.MeasureTheory.Measure.Regular
/-- Outer regular measures are determined by values on open sets.  -/
MeasureTheory.Measure.OuterRegular.ext_isOpen : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  {ν : MeasureTheory.Measure α} [μ.OuterRegular] [ν.OuterRegular], (∀ (U : Set α), IsOpen U → μ U = ν U) → μ = ν
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.sectionsMap_coe : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M N : PresheafOfModules R} (f : M ⟶ N) (s : M.sections) (X : Cᵒᵖ),
  ↑(PresheafOfModules.sectionsMap f s) X = (CategoryTheory.ConcreteCategory.hom (f.app X)) (↑s X)
-- Mathlib.Algebra.Category.ModuleCat.Semi
SemimoduleCat.hom_inv_apply : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R} (e : M ≅ N) (x : ↑N),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) x) = x
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEπ_coe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ), t.eTruncGEπ (WithBotTop.coe n) = t.truncGEπ n
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- `AddMonoidAlgebra.lift` as a `MulEquiv`.  -/
AddMonoidAlgebra.liftMulEquiv : (R : Type u_1) →
  (A : Type u_3) →
    (M : Type u_8) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddMonoid M] → (Multiplicative M →* A) ≃* WithConv (AddMonoidAlgebra R M →ₐ[R] A)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.opcyclesIsoSc'.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j k : ι) (hi : c.prev j = i) (hk : c.next j = k)
  [inst_2 : K.HasHomology j] [inst_3 : (K.sc' i j k).HasHomology],
  K.opcyclesIsoSc' i j k hi hk = CategoryTheory.ShortComplex.opcyclesMapIso (K.isoSc' i j k hi hk)
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with subtraction.  -/
ContDiffAt.laplacian_sub_nhds : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f₁ f₂ : E → F} {x : E},
  ContDiffAt ℝ 2 f₁ x →
    ContDiffAt ℝ 2 f₂ x → Laplacian.laplacian (f₁ - f₂) =ᶠ[nhds x] Laplacian.laplacian f₁ - Laplacian.laplacian f₂
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- If `AddCommMonoid` homs `g : M →+ P, l : P →+ A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`.  -/
AddSubmonoid.LocalizationMap.map_map : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} {T : AddSubmonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : AddCommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5} [inst_4 : AddCommMonoid A]
  {U : AddSubmonoid A} {R : Type u_6} [inst_5 : AddCommMonoid R] (j : U.LocalizationMap R) {l : P →+ A}
  (hl : ∀ (w : ↥T), l ↑w ∈ U) (x : N), (k.map hl j) ((f.map hy k) x) = (f.map ⋯ j) x
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.image_subset_compact_of_isVonNBounded : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NontriviallyNormedField 𝕜₁] [inst_1 : SeminormedRing 𝕜₂] {σ₁₂ : 𝕜₁ →+* 𝕜₂}
  {M₁ : Type u_3} {M₂ : Type u_4} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁]
  [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂] [inst_6 : Module 𝕜₁ M₁] [inst_7 : Module 𝕜₂ M₂]
  [ContinuousConstSMul 𝕜₂ M₂] {f : M₁ →ₛₗ[σ₁₂] M₂},
  IsCompactOperator ⇑f → ∀ {S : Set M₁}, Bornology.IsVonNBounded 𝕜₁ S → ∃ K, IsCompact K ∧ ⇑f '' S ⊆ K
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.dual_symm_apply_toFun : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β] (f : sInfHom αᵒᵈ βᵒᵈ) (a : α),
  (sSupHom.dual.symm f) a = (⇑OrderDual.ofDual ∘ ⇑f ∘ ⇑OrderDual.toDual) a
-- Mathlib.Data.Finset.Prod
Finset.product_subset_product_left : ∀ {α : Type u_1} {β : Type u_2} {s s' : Finset α} {t : Finset β}, s ⊆ s' → s ×ˢ t ⊆ s' ×ˢ t
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.congrLeftₗ_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {Z : Type u_6} (R : Type u_7)
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid Z] [inst_4 : Module R Z] (e : X ≃ₜ Y) (g : LocallyConstant X Z) (a : Y),
  ((LocallyConstant.congrLeftₗ R e) g) a = g (e.symm a)
-- Mathlib.Data.Finsupp.Antidiagonal
/-- The antidiagonal of `s : α →₀ ℕ` is the finset of all pairs `(t₁, t₂) : (α →₀ ℕ) × (α →₀ ℕ)`
such that `t₁ + t₂ = s`.  -/
Finsupp.instHasAntidiagonal : {α : Type u} → [DecidableEq α] → Finset.HasAntidiagonal (α →₀ ℕ)
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
/-- The function `Complex.exp` is complex analytic.  -/
analyticWithinAt_cexp : ∀ {s : Set ℂ} {x : ℂ}, AnalyticWithinAt ℂ Complex.exp s x
-- Init.Data.Nat.Lemmas
Nat.div_eq_self : ∀ {m n : ℕ}, m / n = m ↔ m = 0 ∨ n = 1
-- Mathlib.Algebra.Group.Submonoid.MulAction
AddSubmonoid.addAction.eq_1 : ∀ {M' : Type u_1} {α : Type u_2} [inst : AddMonoid M'] [inst_1 : AddAction M' α] (S : AddSubmonoid M'),
  S.addAction = inferInstance
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The integral `PowerBasis` of `𝓞 K` given by a primitive root of unity, where `K` is an `n`-th
cyclotomic extension of `ℚ`.  -/
IsPrimitiveRoot.integralPowerBasis : {n : ℕ} →
  {K : Type u} →
    [inst : Field K] →
      {ζ : K} →
        [NeZero n] →
          [inst_2 : CharZero K] →
            [IsCyclotomicExtension {n} ℚ K] → IsPrimitiveRoot ζ n → PowerBasis ℤ (NumberField.RingOfIntegers K)
-- Mathlib.Tactic.NormNum.Irrational
_private.Mathlib.Tactic.NormNum.Irrational.0.Mathlib.Meta.NormNum.not_power_nat_pow_of_bounds : ∀ {n k p q : ℕ}, 0 < q → p.Coprime q → k ^ q < n → n < (k + 1) ^ q → ∀ (m : ℕ), n ^ p ≠ m ^ q
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.C.eq_def : ∀ (R : Type u_1) [inst : CommRing R] (x : ℤ),
  Polynomial.Chebyshev.C R x =
    match x with
    | 0 => 2
    | 1 => Polynomial.X
    | Int.ofNat n.succ.succ => Polynomial.X * Polynomial.Chebyshev.C R (↑n + 1) - Polynomial.Chebyshev.C R ↑n
    | Int.negSucc n => Polynomial.X * Polynomial.Chebyshev.C R (-↑n) - Polynomial.Chebyshev.C R (-↑n + 1)
-- Mathlib.Data.Set.MemPartition
/-- The set in `memPartition f n` to which `a : α` belongs.  -/
memPartitionSet : {α : Type u_1} → (ℕ → Set α) → ℕ → α → Set α
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp},
  t₁.Equiv t₂ → ∀ (f : α → Bool), (Std.TreeSet.filter f t₁).Equiv (Std.TreeSet.filter f t₂)
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- Continuous injection to functions from the reproducing kernel Hilbert space `H` to functions
from the domain `X` to the Hilbert space `V`  -/
RKHS.coeCLM : (𝕜 : outParam (Type u_1)) →
  {H : Type u_2} →
    {X : outParam (Type u_3)} →
      {V : outParam (Type u_4)} →
        {inst : RCLike 𝕜} →
          {inst_1 : NormedAddCommGroup V} →
            {inst_2 : InnerProductSpace 𝕜 V} →
              {inst_3 : NormedAddCommGroup H} → {inst_4 : InnerProductSpace 𝕜 H} → [self : RKHS 𝕜 H X V] → H →L[𝕜] X → V
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.smeval.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid S] [inst_2 : SMulWithZero R S]
  [inst_3 : Monoid S] (f : LaurentPolynomial R) (x : Sˣ), f.smeval x = f.coeff.sum fun n r => r • ↑(x ^ n)
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Iic_of_antitoneOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Iic a) →
    AntitoneOn f (Set.Iic a) → Filter.Tendsto f Filter.atBot Filter.atTop → f '' Set.Iic a = Set.Ici (f a)
-- Mathlib.CategoryTheory.Monad.Limits
/-- Any comonadic functor creates colimits.  -/
CategoryTheory.comonadicCreatesColimits : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (R : CategoryTheory.Functor D C) →
          [CategoryTheory.ComonadicLeftAdjoint R] → CategoryTheory.CreatesColimitsOfSize.{v, u, v₂, v₁, u₂, u₁} R
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.beq_iff_equiv : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α] [inst_3 : (k : α) → BEq (β k)] [∀ (k : α), LawfulBEq (β k)],
  m₁.WF → m₂.WF → ((m₁ == m₂) = true ↔ m₁.Equiv m₂)
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedParentSet.default : Lean.Meta.Grind.ParentSet
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.ElementarilyEquivalent.infinite_iff : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N],
  L.ElementarilyEquivalent M N → (Infinite M ↔ Infinite N)
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Expr.denoteN.eq_def : ∀ {α : Type u_1} [inst : Lean.Grind.NatModule α] (ctx : Lean.Grind.Linarith.Context α) (x : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Expr.denoteN ctx x =
    match x with
    | a.sub b => 0
    | a.neg => 0
    | Lean.Grind.Linarith.Expr.intMul k a => 0
    | Lean.Grind.Linarith.Expr.zero => 0
    | Lean.Grind.Linarith.Expr.var v => Lean.Grind.Linarith.Var.denote ctx v
    | a.add b => Lean.Grind.Linarith.Expr.denoteN ctx a + Lean.Grind.Linarith.Expr.denoteN ctx b
    | Lean.Grind.Linarith.Expr.natMul k a => k • Lean.Grind.Linarith.Expr.denoteN ctx a
-- Std.Data.ExtDHashMap.Lemmas
/-- Simpler variant of `get?_filterMap` when `LawfulBEq` is available.  -/
Std.ExtDHashMap.Const.get?_filterMap' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : LawfulBEq α] {f : α → β → Option γ} {k : α},
  Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.filterMap f m) k = (Std.ExtDHashMap.Const.get? m k).bind (f k)
-- Mathlib.Order.Atoms
sSup_atoms_le_eq : ∀ {α : Type u_4} [inst : CompleteLattice α] [IsAtomistic α] (b : α), sSup {a | IsAtom a ∧ a ≤ b} = b
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidIso.instOrderIsoClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : Add β],
  OrderIsoClass (α ≃+o β) α β
-- Mathlib.Algebra.MonoidAlgebra.Opposite
MonoidAlgebra.opRingEquiv_apply : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : Mul M] (a : (MonoidAlgebra R M)ᵐᵒᵖ),
  MonoidAlgebra.opRingEquiv a =
    (MonoidAlgebra.mapAddEquiv Mᵐᵒᵖ MulOpposite.opAddEquiv)
      ((MonoidAlgebra.mapDomainAddEquiv R MulOpposite.opEquiv) (MulOpposite.unop a))
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_symm_sub : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommGroup M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubgroupClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] (x y : DirectSum ι fun i => ↥(ℳ i)),
  (DirectSum.decompose ℳ).symm (x - y) = (DirectSum.decompose ℳ).symm x - (DirectSum.decompose ℳ).symm y
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.updateRIn_rOut : ∀ {E : Type uE} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type uH} [inst_2 : TopologicalSpace H]
  {I : ModelWithCorners ℝ E H} {M : Type uM} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M] {c : M}
  (f : SmoothBumpFunction I c) (r : ℝ) (hr : r ∈ Set.Ioo 0 f.rOut), (f.updateRIn r hr).rOut = f.rOut
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.mk.sizeOf_spec : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : SizeOf G] (toAddSubgroup : AddSubgroup G)
  (isOpen' : IsOpen toAddSubgroup.carrier),
  sizeOf { toAddSubgroup := toAddSubgroup, isOpen' := isOpen' } = 1 + sizeOf toAddSubgroup + sizeOf isOpen'
-- Mathlib.Algebra.Quaternion
Quaternion.re_zero : ∀ {R : Type u_3} [inst : CommRing R], QuaternionAlgebra.re 0 = 0
-- Mathlib.Algebra.Module.LinearMap.End
LinearMap.smulRightₗ_apply_apply : ∀ {R : Type u_1} {M : Type u_4} {M₂ : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M] [inst_4 : Module R M₂] (f : M₂ →ₗ[R] R) (x : M) (y : M₂),
  ((LinearMap.smulRightₗ f) x) y = f y • x
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
CFC.one_le : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] {a : A},
  (∀ x ∈ spectrum R a, 1 ≤ x) → autoParam (p a) CFC.one_le._auto_1 → 1 ≤ a
-- Init.System.IO
/-- The contents of the buffer.  -/
IO.FS.Stream.Buffer.data : IO.FS.Stream.Buffer → ByteArray
-- Mathlib.Analysis.Normed.Group.Basic
NormedGroup.nhds_one_basis_norm_lt : ∀ {E : Type u_5} [inst : SeminormedGroup E], (nhds 1).HasBasis (fun ε => 0 < ε) fun ε => {y | ‖y‖ < ε}
-- Init.Data.BitVec.Bootstrap
BitVec.setWidth.eq_1 : ∀ {w : ℕ} (v : ℕ) (x : BitVec w),
  BitVec.setWidth v x = if h : w ≤ v then BitVec.setWidth' h x else BitVec.ofNat v x.toNat
-- Mathlib.NumberTheory.LegendreSymbol.GaussEisensteinLemmas
ZMod.div_eq_filter_card : ∀ {a b c : ℕ}, 0 < b → a / b ≤ c → a / b = {x ∈ Finset.Ico 1 c.succ | x * b ≤ a}.card
-- Mathlib.Data.Rel
Function.graph_injective : ∀ {α : Type u_1} {β : Type u_2}, Function.Injective Function.graph
-- Lean.Parser.Extension
_private.Lean.Parser.Extension.0.Lean.Parser.compileParserDescr.visit : Lean.Parser.ParserCategories → Lean.ParserDescr → Lean.ImportM Lean.Parser.Parser
-- Mathlib.RingTheory.Coalgebra.GroupLike
GroupLike.valEquiv_apply_coe : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (a : GroupLike R A), ↑(GroupLike.valEquiv a) = ↑a
-- Mathlib.MeasureTheory.Integral.RieszMarkovKakutani.NNReal
CompactlySupportedContinuousMap.integralLinearMap.congr_simp : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] [inst_2 : OpensMeasurableSpace X]
  (μ μ_1 : MeasureTheory.Measure X) (e_μ : μ = μ_1) [inst_3 : MeasureTheory.IsFiniteMeasureOnCompacts μ],
  CompactlySupportedContinuousMap.integralLinearMap μ = CompactlySupportedContinuousMap.integralLinearMap μ_1
-- Mathlib.NumberTheory.Padics.Hensel
hensels_lemma : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2 →
    ∃ z,
      (Polynomial.aeval z) F = 0 ∧
        ‖z - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ∧
          ‖(Polynomial.aeval z) (Polynomial.derivative F)‖ = ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ∧
            ∀ (z' : ℤ_[p]),
              (Polynomial.aeval z') F = 0 → ‖z' - a‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ → z' = z
-- Mathlib.Geometry.Manifold.LocalDiffeomorph
PartialDiffeomorph.contMDiffOn : ∀ {𝕜 : 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] {H₁ : Type u_5}
  [inst_5 : TopologicalSpace H₁] {H₂ : Type u_6} [inst_6 : TopologicalSpace H₂] {I : ModelWithCorners 𝕜 E H₁}
  {J : ModelWithCorners 𝕜 F H₂} {M : Type u_8} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H₁ M] {N : Type u_9}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H₂ N] {n : WithTop ℕ∞} (Φ : PartialDiffeomorph I J M N n),
  ContMDiffOn I J n (↑Φ.toPartialEquiv) Φ.source
-- Mathlib.Topology.DenseEmbedding
IsDenseInducing.closure_range : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {i : α → β},
  IsDenseInducing i → closure (Set.range i) = Set.univ
-- Mathlib.Analysis.Convex.Mul
ConcaveOn.smul_convexOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : LinearOrder 𝕜]
  [IsStrictOrderedRing 𝕜] [inst_3 : CommRing E] [inst_4 : LinearOrder E] [IsStrictOrderedRing E]
  [inst_6 : AddCommGroup F] [inst_7 : LinearOrder F] [IsOrderedAddMonoid F] [inst_9 : AddCommGroup G]
  [inst_10 : Module 𝕜 G] [inst_11 : Module 𝕜 E] [inst_12 : Module 𝕜 F] [inst_13 : Module E F] [IsScalarTower 𝕜 E F]
  [SMulCommClass 𝕜 E F] [IsOrderedModule 𝕜 F] [IsStrictOrderedModule E F] {s : Set G} {f : G → E} {g : G → F}
  [IsOrderedModule 𝕜 E],
  ConcaveOn 𝕜 s f →
    ConvexOn 𝕜 s g →
      (∀ ⦃x : G⦄, x ∈ s → 0 ≤ f x) → (∀ ⦃x : G⦄, x ∈ s → g x ≤ 0) → MonovaryOn f g s → ConvexOn 𝕜 s (f • g)
-- Mathlib.NumberTheory.Pell
/-- If a fundamental solution exists, then `d` must be positive.  -/
Pell.IsFundamental.d_pos : ∀ {d : ℤ} {a : Pell.Solution₁ d}, Pell.IsFundamental a → 0 < d
-- Mathlib.Order.Category.HeytAlg
HeytAlg.hom_id : ∀ {X : HeytAlg}, HeytAlg.Hom.hom (CategoryTheory.CategoryStruct.id X) = HeytingHom.id ↑X
-- Mathlib.Analysis.SpecialFunctions.Sigmoid
AnalyticAt.sigmoid' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x : E},
  AnalyticAt ℝ f x → AnalyticAt ℝ (fun z => (f z).sigmoid) x
-- Mathlib.RingTheory.WittVector.Basic
WittVector.map_surjective : ∀ {p : ℕ} {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Fact (Nat.Prime p)]
  (f : R →+* S), Function.Surjective ⇑f → Function.Surjective ⇑(WittVector.map f)
-- Mathlib.Analysis.Normed.Module.FiniteDimension
lipschitzExtensionConstant_def : ∀ (E' : Type u_1) [inst : NormedAddCommGroup E'] [inst_1 : NormedSpace ℝ E'] [inst_2 : FiniteDimensional ℝ E'],
  lipschitzExtensionConstant E' =
    have A := (Module.Basis.ofVectorSpace ℝ E').equivFun.toContinuousLinearEquiv;
    max (‖↑A.symm‖₊ * ‖↑A‖₊) 1
-- Mathlib.Probability.Distributions.SetBernoulli
ProbabilityTheory.setBernoulli_empty : ∀ {ι : Type u_1} {p : ↑unitInterval} [Countable ι], ProbabilityTheory.setBernoulli ∅ p = MeasureTheory.Measure.dirac ∅
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.eval_zpow' : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (l : Mathlib.Tactic.FieldSimp.NF M) (r : ℤ),
  (l ^ r).eval = Mathlib.Tactic.FieldSimp.zpow' l.eval r
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₂ → k ∉ m₁ ∩ m₂
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_union_self`. -/
Set.diff_union_self : ∀ {α : Type u_1} {s t : Set α}, s \ t ∪ t = s ∪ t
-- Mathlib.CategoryTheory.Bicategory.Yoneda
/-- Postcomposing of `1`-morphisms seen as a functor from `a ⟶ b` to the hom-category of the
corresponding pseudofunctors.

This is an implementation detail, and `Bicategory.yoneda.map` should be preferred.  -/
CategoryTheory.Bicategory.postcomposing₂ : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (a b : B) →
      CategoryTheory.Functor (a ⟶ b) (CategoryTheory.Bicategory.yoneda₀ a ⟶ CategoryTheory.Bicategory.yoneda₀ b)