mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.mono_binaryCofanSum_inr : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C}
  (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl))
  (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc : CategoryTheory.Limits.IsColimit c)
  (hc₁ : CategoryTheory.Limits.IsColimit c₁) (hc₂ : CategoryTheory.Limits.IsColimit c₂)
  [CategoryTheory.Limits.MonoCoprod C],
  CategoryTheory.Mono (CategoryTheory.Limits.MonoCoprod.binaryCofanSum c c₁ c₂ hc₁ hc₂).inr
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits_obj : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C)) [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C]
  (j : J), (CategoryTheory.Limits.DiagramOfCones.mkOfHasLimits F).obj j = CategoryTheory.Limits.limit.cone (F.obj j)
-- Mathlib.RingTheory.Filtration
Ideal.Filtration.instBot : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommRing R] → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → {I : Ideal R} → Bot (I.Filtration M)
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
/-- Geometric progressions of length three are reflected under `2`-Freiman homomorphisms.  -/
IsMulFreimanHom.threeGPFree : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoid α] [inst_1 : CommMonoid β] {s : Set α} {t : Set β} {f : α → β},
  IsMulFreimanHom 2 s t f → Set.InjOn f s → ThreeGPFree t → ThreeGPFree s
-- Mathlib.Probability.Distributions.Pareto
ProbabilityTheory.isProbabilityMeasure_paretoMeasure : ∀ {t r : ℝ}, 0 < t → 0 < r → MeasureTheory.IsProbabilityMeasure (ProbabilityTheory.paretoMeasure t r)
-- Mathlib.LinearAlgebra.Finsupp.Defs
Finsupp.mapDomain.coe_linearEquiv : ∀ {α : Type u_1} (M : Type u_2) (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {α' : Type u_9} (f : α ≃ α'), ⇑(Finsupp.mapDomain.linearEquiv M R f) = Finsupp.mapDomain ⇑f
-- Mathlib.Analysis.Meromorphic.Order
/-- A meromorphic function converges to a nonzero limit iff its order is zero.  -/
tendsto_ne_zero_iff_meromorphicOrderAt_eq_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f x → ((∃ c, c ≠ 0 ∧ Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds c)) ↔ meromorphicOrderAt f x = 0)
-- Mathlib.Order.Bounds.Basic
isLUB_congr : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α} {a : α}, upperBounds s = upperBounds t → (IsLUB s a ↔ IsLUB t a)
-- Init.Data.UInt.Lemmas
UInt32.ofNat_finVal : ∀ (n : Fin UInt32.size), UInt32.ofNat ↑n = UInt32.ofFin n
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.trans_refl_restr' : ∀ {α : Type u_1} {β : Type u_2} (e : PartialEquiv α β) (s : Set β),
  e.trans ((PartialEquiv.refl β).restr s) = e.restr (e.source ∩ ↑e ⁻¹' s)
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.diff.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (l : List α) (h_1 : (l : List α) → motive l [])
  (h_2 : (l₁ : List α) → (a : α) → (l₂ : List α) → motive l₁ (a :: l₂)),
  (match l, [] with
    | l, [] => h_1 l
    | l₁, a :: l₂ => h_2 l₁ a l₂) =
    h_1 l
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.instSubsingletonHom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C) [∀ (x y : C), Subsingleton (x ⟶ y)]
  (x y : CategoryTheory.Quotient r), Subsingleton (x ⟶ y)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.comp_add_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M X Y : C} [inst_2 : CategoryTheory.AddMonObj M] (f : X ⟶ Y) (g₁ g₂ : Y ⟶ M) {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (g₁ + g₂) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp f g₁ + CategoryTheory.CategoryStruct.comp f g₂) h
-- Mathlib.GroupTheory.PGroup
/-- **Alias** of the forward direction of `IsPGroup.iff_orderOf`. -/
IsPGroup.exists_orderOf_eq_pow : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] [Fact (Nat.Prime p)], IsPGroup p G → ∀ (g : G), ∃ k, orderOf g = p ^ k
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
/-- For any valuation `v` compatible with the valuative relation on `R`, the open `r`-ball
around zero `{x | v.restrict x < r}` is closed in the valuative topology.  -/
Valuation.isClosed_ball : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] {v : Valuation R Γ₀} [v.Compatible]
  (r : (MonoidWithZeroHom.ofClass v).ValueGroup₀), IsClosed {x | v.restrict x < r}
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.Iic_add_Iic_subset : ∀ {α : Type u_1} [inst : Add α] [inst_1 : Preorder α] [AddLeftMono α] [AddRightMono α] (a b : α),
  Set.Iic a + Set.Iic b ⊆ Set.Iic (a + b)
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instAddLeftCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddLeftCancelSemigroup α],
  OrderDual.instAddLeftCancelSemigroup = { toAddSemigroup := OrderDual.instAddSemigroup, toIsLeftCancelAdd := ⋯ }
-- Mathlib.RingTheory.Ideal.Operations
IsCoprime.sup_eq : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R}, IsCoprime I J → I ⊔ J = ⊤
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `monovaryOn_iff_mul_rearrangement`.

---

Two functions monovary iff the rearrangement inequality holds.  -/
MonovaryOn.mul_add_mul_le_mul_add_mul : ∀ {ι : Type u_1} {α : Type u_2} [inst : Ring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {f g : ι → α}
  {s : Set ι}, MonovaryOn f g s → ∀ ⦃i : ι⦄, i ∈ s → ∀ ⦃j : ι⦄, j ∈ s → f i * g j + f j * g i ≤ f i * g i + f j * g j
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- Additive subgroup closure of a set is monotone in its argument: if `h ⊆ k`,
then `closure h ≤ closure k`  -/
AddSubgroup.closure_mono : ∀ {G : Type u_1} [inst : AddGroup G] ⦃h k : Set G⦄, h ⊆ k → AddSubgroup.closure h ≤ AddSubgroup.closure k
-- Mathlib.Algebra.Group.Defs
mul_div_cancel_right : ∀ {G : Type u_1} [inst : Group G] (a b : G), a * b / b = a
-- Mathlib.Algebra.Algebra.Unitization
Unitization.addEquiv_apply : ∀ (R : Type u_3) (A : Type u_4) [inst : Add R] [inst_1 : Add A] (self : Unitization R A),
  (Unitization.addEquiv R A) self = self.toProd
-- Mathlib.Topology.Algebra.Module.TopDualPairing
/-- The `topDualPairing` is a continuous perfect pairing for finite-dimensional
Hausdorff spaces over complete nontrivially normed fields.  -/
topDualPairing_isContPerfPair : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] {E : Type u_2} [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : TopologicalSpace E] [IsTopologicalAddGroup E] [ContinuousSMul 𝕜 E]
  [FiniteDimensional 𝕜 E] [T2Space E], (topDualPairing 𝕜 E).IsContPerfPair
-- Mathlib.MeasureTheory.Group.Arithmetic
aemeasurable_inv_iff : ∀ {α : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {G : Type u_4} [inst : InvolutiveInv G]
  [inst_1 : MeasurableSpace G] [MeasurableInv G] {f : α → G}, AEMeasurable (fun x => (f x)⁻¹) μ ↔ AEMeasurable f μ
-- Mathlib.CategoryTheory.Galois.Topology
CategoryTheory.PreGaloisCategory.aut_discreteTopology : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) (X : C),
  DiscreteTopology (CategoryTheory.Aut (F.obj X))
-- Mathlib.Tactic.Linter.DirectoryDependency
/-- The `directoryDependency` linter detects imports between directories that are supposed to be
independent. If this is the case, it emits a warning.
 -/
Mathlib.Linter.linter.directoryDependency : Lean.Option Bool
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput.aig : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {old : Std.Sat.AIG α} →
        {w : ℕ} → Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput old w → Std.Sat.AIG α
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.mkTermElabAttributeUnsafe : Lean.Name → IO (Lean.KeyedDeclsAttribute Lean.Elab.Term.TermElab)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_map : ∀ {S : Type u} [inst : Semiring S] {T : Type v} [inst_1 : Semiring T] (f : S →+* T) (n : ℕ),
  Polynomial.map f (ascPochhammer S n) = ascPochhammer T n
-- Mathlib.LinearAlgebra.LinearIndependent.Basic
linearIndepOn_union_iff : ∀ {ι : Type u'} {R : Type u_2} {s : Set ι} {M : Type u_4} {v : ι → M} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] {t : Set ι},
  Disjoint s t →
    (LinearIndepOn R v (s ∪ t) ↔
      LinearIndepOn R v s ∧ LinearIndepOn R v t ∧ Disjoint (Submodule.span R (v '' s)) (Submodule.span R (v '' t)))
-- Mathlib.Control.ULift
PLift.bind_up : ∀ {α : Sort u} {β : Sort v} (a : α) (f : α → PLift β), { down := a }.bind f = f a
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestMatchAt_of_get_eq : ∀ {c : Char} {s : String.Slice} {pos : s.Pos} {h : pos ≠ s.endPos},
  pos.get h = c → String.Slice.Pattern.Model.IsLongestMatchAt c pos (pos.next h)
-- Mathlib.CategoryTheory.Comma.Arrow
/-- Extensionality lemma for functors `C ⥤ D` which uses as an assumption
that the induced maps `Arrow C → Arrow D` coincide.  -/
CategoryTheory.Arrow.functor_ext : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F G : CategoryTheory.Functor C D},
  (∀ ⦃X Y : C⦄ (f : X ⟶ Y), F.mapArrow.obj (CategoryTheory.Arrow.mk f) = G.mapArrow.obj (CategoryTheory.Arrow.mk f)) →
    F = G
-- Mathlib.CategoryTheory.Galois.Prorepresentability
CategoryTheory.PreGaloisCategory.endEquivAutGalois_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] [inst_1 : CategoryTheory.GaloisCategory C]
  (F : CategoryTheory.Functor C FintypeCat) [inst_2 : CategoryTheory.PreGaloisCategory.FiberFunctor F]
  (f : CategoryTheory.End F) (A : CategoryTheory.PreGaloisCategory.PointedGaloisObject F),
  (CategoryTheory.ConcreteCategory.hom
        (F.map
          ((CategoryTheory.PreGaloisCategory.AutGalois.π F A)
              ((CategoryTheory.PreGaloisCategory.endEquivAutGalois F) f)).hom))
      A.pt =
    (CategoryTheory.ConcreteCategory.hom (f.app A.obj)) A.pt
-- Mathlib.Order.Disjoint
Codisjoint.out : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α},
  Codisjoint a b → ∀ (x : α), a ≤ x → b ≤ x → x = ⊤
-- Mathlib.NumberTheory.LSeries.AbstractFuncEq
WeakFEPair.mk.inj : ∀ {E : Type u_1} {inst : NormedAddCommGroup E} {inst_1 : NormedSpace ℂ E} {f g : ℝ → E} {k : ℝ} {ε : ℂ} {f₀ g₀ : E}
  {hf_int : MeasureTheory.LocallyIntegrableOn f (Set.Ioi 0) MeasureTheory.volume}
  {hg_int : MeasureTheory.LocallyIntegrableOn g (Set.Ioi 0) MeasureTheory.volume} {hk : 0 < k} {hε : ε ≠ 0}
  {h_feq : ∀ x ∈ Set.Ioi 0, f (1 / x) = (ε * ↑(x ^ k)) • g x}
  {hf_top : ∀ (r : ℝ), (fun x => f x - f₀) =O[Filter.atTop] fun x => x ^ r}
  {hg_top : ∀ (r : ℝ), (fun x => g x - g₀) =O[Filter.atTop] fun x => x ^ r} {f_1 g_1 : ℝ → E} {k_1 : ℝ} {ε_1 : ℂ}
  {f₀_1 g₀_1 : E} {hf_int_1 : MeasureTheory.LocallyIntegrableOn f_1 (Set.Ioi 0) MeasureTheory.volume}
  {hg_int_1 : MeasureTheory.LocallyIntegrableOn g_1 (Set.Ioi 0) MeasureTheory.volume} {hk_1 : 0 < k_1} {hε_1 : ε_1 ≠ 0}
  {h_feq_1 : ∀ x ∈ Set.Ioi 0, f_1 (1 / x) = (ε_1 * ↑(x ^ k_1)) • g_1 x}
  {hf_top_1 : ∀ (r : ℝ), (fun x => f_1 x - f₀_1) =O[Filter.atTop] fun x => x ^ r}
  {hg_top_1 : ∀ (r : ℝ), (fun x => g_1 x - g₀_1) =O[Filter.atTop] fun x => x ^ r},
  { f := f, g := g, k := k, ε := ε, f₀ := f₀, g₀ := g₀, hf_int := hf_int, hg_int := hg_int, hk := hk, hε := hε,
        h_feq := h_feq, hf_top := hf_top, hg_top := hg_top } =
      { f := f_1, g := g_1, k := k_1, ε := ε_1, f₀ := f₀_1, g₀ := g₀_1, hf_int := hf_int_1, hg_int := hg_int_1,
        hk := hk_1, hε := hε_1, h_feq := h_feq_1, hf_top := hf_top_1, hg_top := hg_top_1 } →
    f = f_1 ∧ g = g_1 ∧ k = k_1 ∧ ε = ε_1 ∧ f₀ = f₀_1 ∧ g₀ = g₀_1
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.mul_le_left : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {x y : ↑(Set.Icc 0 1)},
  x * y ≤ x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackProdFstIsoProd_hom_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : X ⟶ Y) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct Y Z] [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Z]
  [inst_3 : CategoryTheory.Limits.HasPullback f CategoryTheory.Limits.prod.fst] {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackProdFstIsoProd f Z).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.fst h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f CategoryTheory.Limits.prod.fst) h
-- Mathlib.CategoryTheory.Abelian.SerreClass.MorphismProperty
CategoryTheory.ObjectProperty.instIsStableUnderCobaseChangeEpiModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.epiModSerre.IsStableUnderCobaseChange
-- Mathlib.Algebra.Group.Subgroup.Ker
MonoidHom.decidableMemKer : {G : Type u_1} →
  [inst : Group G] →
    {M : Type u_7} → [inst_1 : MulOneClass M] → [DecidableEq M] → (f : G →* M) → DecidablePred fun x => x ∈ f.ker
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
/-- `Matrix.conjTranspose` as an `AddEquiv`  -/
Matrix.conjTransposeAddEquiv : (m : Type u_2) → (n : Type u_3) → (α : Type v) → [inst : AddMonoid α] → [StarAddMonoid α] → Matrix m n α ≃+ Matrix n m α
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shiftFunctorAdd_assoc_hom_app_assoc : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (a₁ a₂ a₃ : A) (X : C) {Z : C}
  (h :
    (CategoryTheory.shiftFunctor C a₃).obj
        ((CategoryTheory.shiftFunctor C a₂).obj ((CategoryTheory.shiftFunctor C a₁).obj X)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd C (a₁ + a₂) a₃).hom.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor C a₃).map ((CategoryTheory.shiftFunctorAdd C a₁ a₂).hom.app X)) h) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C a₁ (a₂ + a₃) (a₁ + a₂ + a₃) ⋯).hom.app X)
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctorAdd C a₂ a₃).hom.app ((CategoryTheory.shiftFunctor C a₁).obj X)) h)
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
/-- **Alias** of the forward direction of `Set.finite_neg`. -/
Set.Finite.of_neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {s : Set α}, (-s).Finite → s.Finite
-- Mathlib.Algebra.Group.Action.Defs
instSMulCommClassOfIsScalarTower : ∀ {R : Type u_9} {M : Type u_10} [inst : CommMonoid M] [inst_1 : SMul R M] [IsScalarTower R M M], SMulCommClass R M M
-- Mathlib.CategoryTheory.Quotient
CategoryTheory.Quotient.essSurj_functor : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (r : HomRel C),
  (CategoryTheory.Quotient.functor r).EssSurj
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.isNormal_deriv : ∀ (f : Ordinal.{u_1} → Ordinal.{u_1}), Order.IsNormal (Ordinal.deriv f)
-- Mathlib.Algebra.Group.Units.Defs
/-- See `isUnit_iff_exists` for a similar lemma with one existential.  -/
isUnit_iff_exists_and_exists : ∀ {M : Type u_1} [inst : Monoid M] {a : M}, IsUnit a ↔ (∃ b, a * b = 1) ∧ ∃ c, c * a = 1
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.div_def : ∀ {K : Type u_1} [inst : CommRing K] [inst_1 : IsDomain K] (x x_1 : RatFunc K),
  x.div x_1 =
    match x, x_1 with
    | { toFractionRing := p }, { toFractionRing := q } => { toFractionRing := p / q }
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.changeFormEquiv_symm : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q Q' : QuadraticForm R M} {B : LinearMap.BilinForm R M} (h : LinearMap.BilinMap.toQuadraticMap B = Q' - Q),
  (CliffordAlgebra.changeFormEquiv h).symm = CliffordAlgebra.changeFormEquiv ⋯
-- Lean.Environment
Lean.saveModuleData : System.FilePath → Lean.Name → Lean.ModuleData → IO Unit
-- Mathlib.Analysis.Fourier.Convolution
/-- The convolution on Schwartz functions is equal to the convolution on functions.  -/
SchwartzMap.convolution_apply : ∀ {E : Type u_3} {F₁ : Type u_5} {F₂ : Type u_6} {F₃ : Type u_7} [inst : NormedAddCommGroup E]
  [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E] [inst_3 : MeasurableSpace E] [inst_4 : BorelSpace E]
  [inst_5 : NormedAddCommGroup F₁] [inst_6 : NormedSpace ℂ F₁] [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace ℂ F₂] [inst_9 : NormedAddCommGroup F₃] [inst_10 : NormedSpace ℂ F₃] [CompleteSpace F₃]
  [CompleteSpace F₁] [CompleteSpace F₂] (B : F₁ →L[ℂ] F₂ →L[ℂ] F₃) (f : SchwartzMap E F₁) (g : SchwartzMap E F₂)
  (x : E), (((SchwartzMap.convolution B) f) g) x = MeasureTheory.convolution (⇑f) (⇑g) B MeasureTheory.volume x
-- Mathlib.Analysis.Normed.Group.Quotient
Subgroup.quotientIsometryEquivOfEq.eq_1 : ∀ {M : Type u_1} [inst : SeminormedCommGroup M] {S T : Subgroup M} (h : S = T),
  Subgroup.quotientIsometryEquivOfEq h = { toEquiv := Subgroup.quotientEquivOfEq h, isometry_toFun := ⋯ }
-- Init.Core
instDecidableEqPUnit : DecidableEq PUnit.{u_1}
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.AB5StarOfSize_shrink : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasCofilteredLimitsOfSize.{max w w₂, max w' w₂', v, u} C]
  [CategoryTheory.AB5StarOfSize.{max w w₂, max w' w₂', v, u} C], CategoryTheory.AB5StarOfSize.{w, w', v, u} C
-- Mathlib.Analysis.Analytic.ChangeOrigin
FormalMultilinearSeries.radius_le_radius_derivSeries : ∀ {𝕜 : 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]
  (p : FormalMultilinearSeries 𝕜 E F), p.radius ≤ p.derivSeries.radius
-- Mathlib.Geometry.Convex.Cone.Basic
/-- The empty convex cone is generating iff the module is a subsingleton.  -/
ConvexCone.isGenerating_bot_iff : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M], ⊥.IsGenerating ↔ Subsingleton M
-- Mathlib.Analysis.Calculus.Deriv.Pow
derivWithin_fun_pow' : ∀ {𝕜 : Type u_1} {𝔸 : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing 𝔸] [inst_2 : NormedAlgebra 𝕜 𝔸]
  {f : 𝕜 → 𝔸} {x : 𝕜} {s : Set 𝕜},
  DifferentiableWithinAt 𝕜 f s x →
    ∀ (n : ℕ),
      derivWithin (fun x => f x ^ n) s x = ∑ i ∈ Finset.range n, f x ^ (n.pred - i) * derivWithin f s x * f x ^ i
-- Init.Data.Array.MinMax
Array.max_eq_iff : ∀ {α : Type u_1} {a : α} [inst : Max α] [inst_1 : LE α] {xs : Array α} [Std.IsLinearOrder α] [Std.LawfulOrderMax α]
  (h : xs ≠ #[]), xs.max h = a ↔ a ∈ xs ∧ ∀ b ∈ xs, b ≤ a
-- Mathlib.Logic.Equiv.PartialEquiv
/-- `EqOnSource` is an equivalence relation. This instance provides the `≈` notation between two
`PartialEquiv`s.  -/
PartialEquiv.eqOnSourceSetoid : {α : Type u_1} → {β : Type u_2} → Setoid (PartialEquiv α β)
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_prodMap' : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [Module.Free R M] [Module.Finite R M] [Module.Free R N]
  [Module.Finite R N] (f : M →ₗ[R] M) (g : N →ₗ[R] N),
  (LinearMap.trace R (M × N)) (f.prodMap g) = (LinearMap.trace R M) f + (LinearMap.trace R N) g
-- Mathlib.Analysis.Normed.Operator.Bilinear
ContinuousLinearMap.bilinearRestrictScalars_eq_restrictScalarsL_comp_restrictScalars : ∀ {𝕜 : Type u_1} {E : Type u_4} {F : Type u_6} {G : Type u_8} {𝕜' : Type u_11} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] [inst_3 : SeminormedAddCommGroup E]
  [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜' E] [inst_6 : IsScalarTower 𝕜 𝕜' E]
  [inst_7 : SeminormedAddCommGroup F] [inst_8 : NormedSpace 𝕜 F] [inst_9 : NormedSpace 𝕜' F]
  [inst_10 : IsScalarTower 𝕜 𝕜' F] [inst_11 : SeminormedAddCommGroup G] [inst_12 : NormedSpace 𝕜 G]
  [inst_13 : NormedSpace 𝕜' G] [inst_14 : IsScalarTower 𝕜 𝕜' G] (B : E →L[𝕜'] F →L[𝕜'] G),
  ContinuousLinearMap.bilinearRestrictScalars 𝕜 B =
    ContinuousLinearMap.restrictScalarsL 𝕜' F G 𝕜 𝕜 ∘SL ContinuousLinearMap.restrictScalars 𝕜 B
-- Mathlib.Topology.Sheaves.SheafCondition.UniqueGluing
TopCat.Sheaf.eq_of_locally_eq₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : C → C → Type u_2} {CC : C → Type u_3}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [CategoryTheory.Limits.HasLimitsOfSize.{x, x, v_1, u_1} C] [(CategoryTheory.forget C).ReflectsIsomorphisms]
  [CategoryTheory.Limits.PreservesLimitsOfSize.{x, x, v_1, u_3, u_1, u_3 + 1} (CategoryTheory.forget C)] {X : TopCat}
  (F : TopCat.Sheaf C X) {U₁ U₂ V : TopologicalSpace.Opens ↑X} (i₁ : U₁ ⟶ V) (i₂ : U₂ ⟶ V),
  V ≤ U₁ ⊔ U₂ →
    ∀ (s t : CategoryTheory.ToType (F.obj.obj (Opposite.op V))),
      (CategoryTheory.ConcreteCategory.hom (F.obj.map i₁.op)) s =
          (CategoryTheory.ConcreteCategory.hom (F.obj.map i₁.op)) t →
        (CategoryTheory.ConcreteCategory.hom (F.obj.map i₂.op)) s =
            (CategoryTheory.ConcreteCategory.hom (F.obj.map i₂.op)) t →
          s = t
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.instPartialOrder.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : Bot α] [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β],
  SupBotHom.instPartialOrder = PartialOrder.lift DFunLike.coe ⋯
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
/-- The identity on the whole space as an open partial homeomorphism.  -/
OpenPartialHomeomorph.refl : (X : Type u_7) → [inst : TopologicalSpace X] → OpenPartialHomeomorph X X
-- Mathlib.CategoryTheory.Adjunction.Triple
CategoryTheory.Adjunction.Triple.rightToLeft_app_adj₂_unit_app : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  {H : CategoryTheory.Functor C D} (t : CategoryTheory.Adjunction.Triple F G H) [inst_2 : G.Full] [inst_3 : G.Faithful]
  (X : C),
  CategoryTheory.CategoryStruct.comp (t.rightToLeft.app X) (t.adj₂.unit.app (F.obj X)) = H.map (t.adj₁.unit.app X)
-- Mathlib.Algebra.Category.Ring.Under.Property
CommRingCat.Under.hasFiniteLimits : ∀ {Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => Q) →
    (RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => Q) →
      (RingHom.HasEqualizers fun {R S} [CommRing R] [CommRing S] => Q) →
        ∀ (R : CommRingCat),
          CategoryTheory.Limits.HasFiniteLimits
            ((RingHom.toMorphismProperty fun {R S} [CommRing R] [CommRing S] => Q).Under ⊤ R)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.riiIterator : {α : Type u_1} → {β : α → Type u_2} → Std.DTreeMap.Internal.Impl α β → Std.Iter ((a : α) × β a)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.inl_v_fst_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (p : ℤ),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCocone.inl φ).v p p ⋯)
      ((CochainComplex.mappingCocone.fst φ).f p) =
    CategoryTheory.CategoryStruct.id (K.X p)
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.trim_le_trim_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] {m₁ m₂ : MeasureTheory.OuterMeasure α},
  m₁.trim ≤ m₂.trim ↔ ∀ (s : Set α), MeasurableSet s → m₁ s ≤ m₂ s