mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Computability.PartrecCode
/-- Proof that `Nat.Partrec.Code.ofNatCode` is the inverse of `Nat.Partrec.Code.encodeCode`  -/
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.encode_ofNatCode : ∀ (n : ℕ), (Nat.Partrec.Code.ofNatCode n).encodeCode = n
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelAddMonoid.mk : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : Preorder α] [toIsOrderedAddMonoid : IsOrderedAddMonoid α],
  (∀ (a b c : α), a + b ≤ a + c → b ≤ c) → (∀ (a b c : α), b + a ≤ c + a → b ≤ c) → IsOrderedCancelAddMonoid α
-- Mathlib.Algebra.Order.Group.Equiv
symm_ofLexMulEquiv : ∀ (α : Type u_1) [inst : Mul α], (ofLexMulEquiv α).symm = toLexMulEquiv α
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.piIsoPi_hom_apply : ∀ {ι : Type v} (α : ι → TopCat) (i : ι) (x : ↑(∏ᶜ α)),
  (CategoryTheory.ConcreteCategory.hom (TopCat.piIsoPi α).hom) x i =
    (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.Pi.π α i)) x
-- Mathlib.Algebra.Module.Equiv.Basic
AddEquiv.toNatLinearEquiv_symm : ∀ {M : Type u_5} {M₂ : Type u_7} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid M₂] (e : M ≃+ M₂),
  e.symm.toNatLinearEquiv = e.toNatLinearEquiv.symm
-- Mathlib.RingTheory.Finiteness.Finsupp
/-- The linear map from `Hom(M,N)^(ι)` to `Hom(M,N^(ι))`. This is the `Finsupp` version of
the forward direction of `LinearEquiv.linearMapPi`.  -/
LinearMap.finsuppLinearMap : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {ι : Type u_4} →
        (S : Type u_5) →
          [inst : Semiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid N] →
                [inst_3 : Module R M] →
                  [inst_4 : Module R N] →
                    [inst_5 : Semiring S] →
                      [inst_6 : Module S N] → [inst_7 : SMulCommClass R S N] → (ι →₀ M →ₗ[R] N) →ₗ[S] M →ₗ[R] ι →₀ N
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.IsFlat.mk : ∀ {α : Type u_2} {M : Matroid α} {F : Set α},
  (∀ ⦃I X : Set α⦄, M.IsBasis I F → M.IsBasis I X → X ⊆ F) → F ⊆ M.E → M.IsFlat F
-- Mathlib.Analysis.Distribution.TestFunction
/-- `lineDerivCLM 𝕜 v` is the continuous `𝕜`-linear-map sending `f : 𝓓^{n}_{K}(E, F)` to
its derivative along the vector `v`, which is an element of `𝓓^{k}_{K}(E, F)`.
This only makes mathematical sense if `k + 1 ≤ n`, otherwise we define it as the zero map.

The parameters `n` and `k` are implicit as they can often be inferred from context, or
specified by a type ascription. For `n = k = ⊤`, we also provide instances of the `LineDeriv`
notation typeclass.  -/
TestFunction.lineDerivCLM : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_3} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace ℝ E] →
          {Ω : TopologicalSpace.Opens E} →
            {F : Type u_4} →
              [inst_3 : NormedAddCommGroup F] →
                [inst_4 : NormedSpace ℝ F] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    {n k : ℕ∞} →
                      [inst_6 : Algebra ℝ 𝕜] →
                        [inst_7 : IsScalarTower ℝ 𝕜 F] → E → TestFunction Ω F n →L[𝕜] TestFunction Ω F k
-- Mathlib.Analysis.InnerProductSpace.Defs
/-- Inner product defined by the `PreInnerProductSpace.Core` structure. We can't reuse
`PreInnerProductSpace.Core.toInner` because it takes `PreInnerProductSpace.Core` as an explicit
argument.  -/
InnerProductSpace.Core.toPreInner' : {𝕜 : Type u_1} →
  {F : Type u_3} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] → [inst_2 : Module 𝕜 F] → [c : PreInnerProductSpace.Core 𝕜 F] → Inner 𝕜 F
-- Mathlib.FieldTheory.AbsoluteGaloisGroup
Field.absoluteGaloisGroup.commutator_closure_isNormal : ∀ (K : Type u_1) [inst : Field K], (commutator (Field.absoluteGaloisGroup K)).topologicalClosure.Normal
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.Spec.map_eq_id : ∀ {R : CommRingCat} {ϕ : R ⟶ R},
  AlgebraicGeometry.Spec.map ϕ = CategoryTheory.CategoryStruct.id (AlgebraicGeometry.Spec R) ↔
    ϕ = CategoryTheory.CategoryStruct.id R
-- Mathlib.Algebra.Homology.TotalComplexShift
HomologicalComplex₂.ι_totalShift₁Iso_inv_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : HomologicalComplex₂ C (ComplexShape.up ℤ) (ComplexShape.up ℤ)) (x : ℤ) [inst_2 : K.HasTotal (ComplexShape.up ℤ)]
  (a b n : ℤ) (h : a + b = n) (a' n' : ℤ) (ha' : a' + b = n') (hn' : n' = n + x),
  CategoryTheory.CategoryStruct.comp (K.ιTotal (ComplexShape.up ℤ) a' b n' ha')
      (CategoryTheory.CategoryStruct.comp
        (CochainComplex.shiftFunctorObjXIso (K.total (ComplexShape.up ℤ)) x n n' hn').inv
        ((K.totalShift₁Iso x).inv.f n)) =
    CategoryTheory.CategoryStruct.comp (K.shiftFunctor₁XXIso a x a' ⋯ b).inv
      (((HomologicalComplex₂.shiftFunctor₁ C x).obj K).ιTotal (ComplexShape.up ℤ) a b n h)
-- Mathlib.Algebra.Order.Invertible
invOf_nonpos : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a : R} [inst_3 : Invertible a],
  ⅟a ≤ 0 ↔ a ≤ 0
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_div : ∀ {K : Type u} [inst : Field K] (p q : Polynomial K),
  ((algebraMap (Polynomial K) (RatFunc K)) p / (algebraMap (Polynomial K) (RatFunc K)) q).num =
    Polynomial.C (q / gcd p q).leadingCoeff⁻¹ * (p / gcd p q)
-- Batteries.Lean.Meta.UnusedNames
Lean.Name.MatchUpToIndexSuffix.exactMatch.sizeOf_spec : sizeOf Lean.Name.MatchUpToIndexSuffix.exactMatch = 1
-- Mathlib.Algebra.Order.GroupWithZero.Basic
/-- **Alias** of the reverse direction of `inv_nonneg`. -/
inv_nonneg_of_nonneg : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}, 0 ≤ a → 0 ≤ a⁻¹
-- Mathlib.GroupTheory.QuotientGroup.Finite
Group.fintypeOfKerLeRange.eq_1 : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : Group F] [inst_1 : Group G] [inst_2 : Group H]
  [inst_3 : Fintype F] [inst_4 : Fintype H] (f : F →* G) (g : G →* H) (h : g.ker ≤ f.range),
  Group.fintypeOfKerLeRange f g h = Fintype.ofEquiv ((G ⧸ g.ker) × ↥g.ker) Subgroup.groupEquivQuotientProdSubgroup.symm
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.insert.match_3.splitter : (motive : Ordering → Sort u_1) →
  (x : Ordering) → (Unit → motive Ordering.lt) → (Unit → motive Ordering.gt) → (Unit → motive Ordering.eq) → motive x
-- Mathlib.Order.Hom.Lex
/-- `Equiv.prodAssoc` promoted to an order isomorphism of lexicographic products.  -/
Prod.Lex.prodLexAssoc : (α : Type u_4) →
  (β : Type u_5) →
    (γ : Type u_6) →
      [inst : Preorder α] →
        [inst_1 : Preorder β] → [inst_2 : Preorder γ] → Lex (Lex (α × β) × γ) ≃o Lex (α × Lex (β × γ))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Basic
SimpleGraph.Walk.length_darts : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v), p.darts.length = p.length
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Zarankiewicz
/-- `zarankiewicz m n s t` is at most `x` if and only if every
`completeBipartiteGraph α β`-free bipartite graph `G` has at most `x` edges.  -/
SimpleGraph.zarankiewicz_le_iff_of_nonneg : ∀ {m n s t : ℕ} {V : Type u_1} {W : Type u_2} {α : Type u_3} {β : Type u_4} [inst : Fintype V] [inst_1 : Fintype W]
  [inst_2 : Fintype α] [inst_3 : Fintype β] {R : Type u_5} [inst_4 : Semiring R] [inst_5 : LinearOrder R]
  [FloorSemiring R],
  Fintype.card V = m →
    Fintype.card W = n →
      Fintype.card α = s →
        Fintype.card β = t →
          ∀ {x : R},
            0 ≤ x →
              (↑(SimpleGraph.zarankiewicz m n s t) ≤ x ↔
                ∀ ⦃G : SimpleGraph (V ⊕ W)⦄ [inst_7 : DecidableRel G.Adj],
                  G ≤ completeBipartiteGraph V W → (completeBipartiteGraph α β).Free G → ↑G.edgeFinset.card ≤ x)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_inter : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveInv α] (s t : Finset α), (s ∩ t)⁻¹ = s⁻¹ ∩ t⁻¹
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- Reinterpret an additive homomorphism as an `ℕ`-linear map.  -/
AddMonoidHom.toNatLinearMap : {M : Type u_8} → {M₂ : Type u_10} → [inst : AddCommMonoid M] → [inst_1 : AddCommMonoid M₂] → (M →+ M₂) → M →ₗ[ℕ] M₂
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
AlgebraicGeometry.Scheme.Cover.mkOfCovers_I₀ : ∀ {X : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} (J : Type u_1)
  (obj : J → AlgebraicGeometry.Scheme) (map : (j : J) → obj j ⟶ X) (covers : ∀ (x : ↥X), ∃ j y, (map j) y = x)
  (map_prop : autoParam (∀ (j : J), P (map j)) AlgebraicGeometry.Scheme.Cover.mkOfCovers._auto_1),
  (AlgebraicGeometry.Scheme.Cover.mkOfCovers J obj map covers map_prop).I₀ = J
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
instCategoryProfiniteGrp : CategoryTheory.Category.{u_1, u_1 + 1} ProfiniteGrp.{u_1}
-- Mathlib.Combinatorics.Young.SemistandardTableau
/-- `entry` is required to be zero for all pairs `(i, j) ∉ μ`.  -/
SemistandardYoungTableau.zeros' : ∀ {μ : YoungDiagram} (self : SemistandardYoungTableau μ) {i j : ℕ}, (i, j) ∉ μ → self.entry i j = 0
-- ProofWidgets.Component.Basic
ProofWidgets.InteractiveMessageProps.mk.inj : ∀ {msg msg_1 : Lean.Server.WithRpcRef Lean.MessageData}, { msg := msg } = { msg := msg_1 } → msg = msg_1
-- Mathlib.Order.KrullDimension
Order.krullDim_nonneg_iff : ∀ {α : Type u_1} [inst : Preorder α], 0 ≤ Order.krullDim α ↔ Nonempty α
-- Mathlib.Computability.RecursiveIn
/-- If a function is partial recursive, then it is recursive in every partial function.  -/
Nat.Partrec.recursiveIn : ∀ {f : ℕ →. ℕ} {O : Set (ℕ →. ℕ)}, Nat.Partrec f → Nat.RecursiveIn O f
-- Mathlib.Algebra.Category.ModuleCat.Stalk
/-- Given a cofiltered diagram of rings `R`, and a module `M` over `R`,
this is the `colim R`-module structure of `colim M`.  -/
CategoryTheory.Limits.IsColimit.module : {C : Type u_1} →
  [inst : CategoryTheory.SmallCategory C] →
    [CategoryTheory.IsFiltered C] →
      (R : CategoryTheory.Functor C RingCat) →
        (M : CategoryTheory.Functor C Ab) →
          [inst_2 : (i : C) → Module ↑(R.obj i) ↑(M.obj i)] →
            (∀ {i j : C} (f : i ⟶ j) (r : ↑(R.obj i)) (m : ↑(M.obj i)),
                (CategoryTheory.ConcreteCategory.hom (M.map f)) (r • m) =
                  (CategoryTheory.ConcreteCategory.hom (R.map f)) r •
                    (CategoryTheory.ConcreteCategory.hom (M.map f)) m) →
              {cR : CategoryTheory.Limits.Cocone R} →
                CategoryTheory.Limits.IsColimit cR →
                  {cM : CategoryTheory.Limits.Cocone M} → CategoryTheory.Limits.IsColimit cM → Module ↑cR.pt ↑cM.pt
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.insertₘ.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (v v_1 : β k),
  v = v_1 →
    ∀ (l l_1 : Std.DTreeMap.Internal.Impl α β) (e_l : l = l_1) (h : l.Balanced),
      Std.DTreeMap.Internal.Impl.insertₘ k v l h = Std.DTreeMap.Internal.Impl.insertₘ k v_1 l_1 ⋯
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.notMem_support_iff : ∀ {X : Type u_1} (x : X) (a : FreeAbelianGroup X), x ∉ a.support ↔ (FreeAbelianGroup.coeff x) a = 0
-- Mathlib.Topology.MetricSpace.Polish
TopologicalSpace.Opens.CompleteCopy.dist_eq : ∀ {α : Type u_1} [inst : MetricSpace α] {s : TopologicalSpace.Opens α} (x y : s.CompleteCopy),
  dist x y = dist ↑x ↑y + |1 / Metric.infDist (↑x) (↑s)ᶜ - 1 / Metric.infDist (↑y) (↑s)ᶜ|
-- Batteries.Recycling.RBTree.Basic
RBTree.RBSet.instMembership : {α : Type u_1} → {cmp : α → α → Ordering} → Membership α (RBTree.RBSet α cmp)
-- Lean.Parser.Types
Lean.Parser.SyntaxStack.back : Lean.Parser.SyntaxStack → Lean.Syntax
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.lift_symm_apply : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (F : MonoidAlgebra R M →ₐ[R] A) (m : M),
  ((MonoidAlgebra.lift R A M).symm F) m = F (MonoidAlgebra.single m 1)
-- Init.Data.Int.Order
Int.sign_eq_neg_one_of_neg : ∀ {a : ℤ}, a < 0 → a.sign = -1
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.mk.sizeOf_spec : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  {ρ : Representation A G V} {σ : Representation A G W} [inst_6 : SizeOf A] [inst_7 : SizeOf G] [inst_8 : SizeOf V]
  [inst_9 : SizeOf W] (toLinearMap : V →ₗ[A] W) (isIntertwining' : ∀ (g : G), toLinearMap ∘ₗ ρ g = σ g ∘ₗ toLinearMap),
  sizeOf { toLinearMap := toLinearMap, isIntertwining' := isIntertwining' } = 1 + sizeOf toLinearMap
-- Mathlib.Topology.Algebra.Support
HasCompactMulSupport.mul : ∀ {α : Type u_2} {β : Type u_4} [inst : TopologicalSpace α] [inst_1 : MulOneClass β] {f f' : α → β},
  HasCompactMulSupport f → HasCompactMulSupport f' → HasCompactMulSupport (f * f')
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mdifferentiableWithinAt_univ : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M},
  MDiffAt[Set.univ] f x ↔ MDiffAt f x
-- Mathlib.Analysis.Convex.Strong
/-- A function `f` from a real normed space is uniformly convex with modulus `φ` if
`f (t • x + (1 - t) • y) ≤ t • f x + (1 - t) • f y - t * (1 - t) * φ ‖x - y‖` for all `t ∈ [0, 1]`.

`φ` is usually taken to be a monotone function such that `φ r = 0 ↔ r = 0`.  -/
UniformConvexOn : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℝ E] → Set E → (ℝ → ℝ) → (E → ℝ) → Prop
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.balanceₘ.match_1.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (l : Std.DTreeMap.Internal.Impl α β) →
      (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.size > Std.DTreeMap.Internal.delta * l.size → Sort u_3) →
        (r : Std.DTreeMap.Internal.Impl α β) →
          (h : r.size > Std.DTreeMap.Internal.delta * l.size) →
            ((h : Std.DTreeMap.Internal.Impl.leaf.size > Std.DTreeMap.Internal.delta * l.size) →
                motive Std.DTreeMap.Internal.Impl.leaf h) →
              ((size : ℕ) →
                  (rk : α) →
                    (rv : β rk) →
                      (rl rr : Std.DTreeMap.Internal.Impl α β) →
                        (h :
                            (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr).size >
                              Std.DTreeMap.Internal.delta * l.size) →
                          motive (Std.DTreeMap.Internal.Impl.inner size rk rv rl rr) h) →
                motive r h
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.RupAddSound.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.confirmRupHint.match_1.eq_3 : ∀ {n : ℕ}
  (motive : Std.Tactic.BVDecide.LRAT.Internal.ReduceResult (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) → Sort u_1)
  (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) (b : Bool)
  (h_1 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth)
  (h_2 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty)
  (h_3 :
    (l : Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
      (b : Bool) → motive (Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b)))
  (h_4 : Unit → motive Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit),
  (match Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) with
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.encounteredBoth => h_1 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToEmpty => h_2 ()
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToUnit (l, b) => h_3 l b
    | Std.Tactic.BVDecide.LRAT.Internal.ReduceResult.reducedToNonunit => h_4 ()) =
    h_3 l b
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetRing.isSetSemiring : ∀ {α : Type u_1} {C : Set (Set α)}, MeasureTheory.IsSetRing C → MeasureTheory.IsSetSemiring C
-- Std.Data.Internal.List.Associative
Std.Internal.List.DistinctKeys_impl_Pairwise_distinct : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l → List.Pairwise (fun a b => (a.fst == b.fst) = false) l
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.RefVec.getD : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → {len : ℕ} → aig.RefVec len → ℕ → aig.Ref → aig.Ref
-- Init.Data.Array.Erase
Array.set_getElem_succ_eraseIdx_succ : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} (h : i + 1 < xs.size),
  (xs.eraseIdx (i + 1) h).set i xs[i + 1] ⋯ = xs.eraseIdx i ⋯
-- Mathlib.CategoryTheory.Sites.MayerVietorisSquare
/-- Constructor for Mayer-Vietoris squares taking as an input
a pullback square `sq` such that `sq.f₂₄` and `sq.f₃₄` are two monomorphisms
which form a covering of `S.X₄`.  -/
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.mk_of_isPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] →
        (sq : CategoryTheory.Square C) →
          [CategoryTheory.Mono sq.f₂₄] →
            [CategoryTheory.Mono sq.f₃₄] →
              sq.IsPullback → CategoryTheory.Sieve.ofTwoArrows sq.f₂₄ sq.f₃₄ ∈ J sq.X₄ → J.MayerVietorisSquare
-- Mathlib.Analysis.SpecialFunctions.Complex.Arctan
/-- We can combine the logs in `log (1 + z * I) + -log (1 - z * I)` into one.
This is only used in `hasSum_arctan`.  -/
Complex.hasSum_arctan_aux : ∀ {z : ℂ},
  ‖z‖ < 1 →
    Complex.log (1 + z * Complex.I) + -Complex.log (1 - z * Complex.I) =
      Complex.log ((1 + z * Complex.I) / (1 - z * Complex.I))
-- Mathlib.Topology.Algebra.UniformConvergence
UniformOnFun.hasBasis_nhds_zero : ∀ {α : Type u_1} {G : Type u_2} [inst : AddGroup G] [inst_1 : UniformSpace G] [IsUniformAddGroup G] (𝔖 : Set (Set α)),
  𝔖.Nonempty →
    DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 →
      (nhds 0).HasBasis (fun SV => SV.1 ∈ 𝔖 ∧ SV.2 ∈ nhds 0) fun SV => {f | ∀ x ∈ SV.1, f x ∈ SV.2}
-- Mathlib.CategoryTheory.Functor.OfSequence
CategoryTheory.Functor.OfSequence.map_id : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : ℕ → C} (f : (n : ℕ) → X n ⟶ X (n + 1)) (i : ℕ),
  CategoryTheory.Functor.OfSequence.map f i i ⋯ = CategoryTheory.CategoryStruct.id (X i)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RciSliceData.mk.sizeOf_spec : ∀ {α : Type u} [inst : Ord α] [inst_1 : SizeOf α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit)
  (range : Std.Rci α), sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Init.Data.Int.Order
Int.sign_negSucc : ∀ (x : ℕ), (Int.negSucc x).sign = -1
-- Mathlib.LinearAlgebra.Dual.Defs
LinearEquiv.dualMap_trans : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : Module R M₁] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M₂] {M₃ : Type u_4} [inst_5 : AddCommMonoid M₃]
  [inst_6 : Module R M₃] (f : M₁ ≃ₗ[R] M₂) (g : M₂ ≃ₗ[R] M₃), g.dualMap ≪≫ₗ f.dualMap = (f ≪≫ₗ g).dualMap
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.sum_filter_count_eq_countP : ∀ {ι : Type u_1} [inst : DecidableEq ι] (p : ι → Prop) [inst_1 : DecidablePred p] (l : List ι),
  ∑ x ∈ l.toFinset with p x, List.count x l = List.countP (fun b => decide (p b)) l
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict
/-- The homeomorphism `spectrum S a ≃ₜ spectrum R a` induced by `SpectrumRestricts a f`.  -/
SpectrumRestricts.homeomorph : {R : Type u_1} →
  {S : Type u_2} →
    {A : Type u_3} →
      [inst : Semifield R] →
        [inst_1 : Semifield S] →
          [inst_2 : Ring A] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra R A] →
                [inst_5 : Algebra S A] →
                  [IsScalarTower R S A] →
                    [inst_7 : TopologicalSpace R] →
                      [inst_8 : TopologicalSpace S] →
                        [ContinuousSMul R S] →
                          {a : A} → {f : C(S, R)} → SpectrumRestricts a ⇑f → ↑(spectrum S a) ≃ₜ ↑(spectrum R a)
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.Sheaf.Hom.mono_iff_presheaf_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [(CategoryTheory.forget D).ReflectsIsomorphisms] {F G : CategoryTheory.Sheaf J D} (f : F ⟶ G),
  CategoryTheory.Mono f ↔ CategoryTheory.Mono f.hom
-- Mathlib.Topology.MetricSpace.Polish
/-- A Polish space is a topological space with second countable topology, that can be endowed
with a metric for which it is complete.

To endow a Polish space with a complete metric space structure, do
`letI := upgradeIsCompletelyMetrizable α`.
 -/
PolishSpace : (α : Type u_3) → [h : TopologicalSpace α] → Prop
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- Converse to the mean value inequality: if `f` is `C`-lipschitz
on a neighborhood of `x₀` then its derivative at `x₀` has norm bounded by `C`. This version
only assumes that `‖f x - f x₀‖ ≤ C * ‖x - x₀‖` in a neighborhood of `x`.  -/
norm_fderiv_le_of_lip' : ∀ (𝕜 : 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}
  {x₀ : E} {C : ℝ}, 0 ≤ C → (∀ᶠ (x : E) in nhds x₀, ‖f x - f x₀‖ ≤ C * ‖x - x₀‖) → ‖fderiv 𝕜 f x₀‖ ≤ C
-- Mathlib.Data.Finset.Powerset
/-- The `n`-element subsets of `t` containing `s` are exactly the `(n - s.card)`-element
subsets of `t \ s`, unioned with `s`.  -/
Finset.filter_powersetCard_subset : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α) (n : ℕ),
  s ⊆ t →
    s.card ≤ n →
      {x ∈ Finset.powersetCard n t | s ⊆ x} = Finset.image (fun x => x ∪ s) (Finset.powersetCard (n - s.card) (t \ s))
-- Mathlib.MeasureTheory.Integral.Prod
/-- A version of *Fubini theorem* for continuous functions with compact support: one may swap
the order of integration with respect to locally finite measures. One does not assume that the
measures are σ-finite, contrary to the usual Fubini theorem.  -/
MeasureTheory.integral_integral_swap_of_hasCompactSupport : ∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {X : Type u_5} {Y : Type u_6}
  [inst_2 : TopologicalSpace X] [inst_3 : TopologicalSpace Y] [inst_4 : MeasurableSpace X] [inst_5 : MeasurableSpace Y]
  [OpensMeasurableSpace X] [OpensMeasurableSpace Y] {f : X → Y → E},
  Continuous (Function.uncurry f) →
    HasCompactSupport (Function.uncurry f) →
      ∀ {μ : MeasureTheory.Measure X} {ν : MeasureTheory.Measure Y} [MeasureTheory.IsFiniteMeasureOnCompacts μ]
        [MeasureTheory.IsFiniteMeasureOnCompacts ν],
        ∫ (x : X), ∫ (y : Y), f x y ∂ν ∂μ = ∫ (y : Y), ∫ (x : X), f x y ∂μ ∂ν
-- Mathlib.Computability.Language
/-- The subtraction of two languages is their difference.  -/
Language.instSub : {α : Type u_1} → Sub (Language α)
-- Mathlib.Algebra.Group.Action.Defs
smul_one_smul : ∀ {α : Type u_5} {M : Type u_9} (N : Type u_10) [inst : Monoid N] [inst_1 : SMul M N] [inst_2 : MulAction N α]
  [inst_3 : SMul M α] [IsScalarTower M N α] (x : M) (y : α), (x • 1) • y = x • y