mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_injective : Function.Injective Complex.UnitClosedDisc.coe
-- Mathlib.Data.SetLike.Basic
/-- The order induced from a `SetLike` instance by inclusion.

An order defined as `.ofSetLike` will automatically make available an instance
of `IsConcreteLE`.
 -/
LE.ofSetLike : (A : Type u_1) → (B : Type u_2) → [SetLike A B] → LE A
-- Lean.Meta.Sym.Apply
/-- Applies a backward rule to a goal, returning new subgoals.

1. Unifies the goal type with the rule's pattern
2. Assigns the goal metavariable to the theorem application
3. Returns new goals for unassigned arguments (per `resultPos`)

Returns `.failed` if unification fails, or if an instance argument could not be synthesized.
 -/
Lean.Meta.Sym.BackwardRule.apply : Lean.MVarId → Lean.Meta.Sym.BackwardRule → Lean.Meta.Sym.SymM Lean.Meta.Sym.ApplyResult
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- There is an equivalence between the set of edges incident to a given
vertex and the set of vertices adjacent to the vertex.  -/
SimpleGraph.incidenceSetEquivNeighborSet : {V : Type u} → (G : SimpleGraph V) → [DecidableEq V] → (v : V) → ↑(G.incidenceSet v) ≃ ↑(G.neighborSet v)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isNormal_add_right : ∀ (a : Ordinal.{u_4}), Order.IsNormal fun x => a + x
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
/-- This is the key identity satisfied by `σ`.  -/
CategoryTheory.NonPreadditiveAbelian.σ_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp CategoryTheory.NonPreadditiveAbelian.σ f =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f f) CategoryTheory.NonPreadditiveAbelian.σ
-- Init.Data.Vector.OfFn
_private.Init.Data.Vector.OfFn.0.Vector.ofFnM.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] (f : Fin n → m α),
  Vector.ofFnM f = Vector.ofFnM.go✝ f 0 ⋯ (Array.emptyWithCapacity n) ⋯
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.instInhabitedTransition.default : Std.Time.TimeZone.Transition
-- Mathlib.Topology.MetricSpace.Dilation
/-- A dilation maps spheres to spheres and scales the radius by `ratio f`.  -/
Dilation.mapsTo_sphere : ∀ {α : Type u_1} {β : Type u_2} {F : Type u_4} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β]
  [inst_2 : FunLike F α β] [inst_3 : DilationClass F α β] (f : F) (x : α) (r' : ℝ),
  Set.MapsTo (⇑f) (Metric.sphere x r') (Metric.sphere (f x) (↑(Dilation.ratio f) * r'))
-- Mathlib.Order.Filter.Prod
Filter.le_prod_map_fst_snd : ∀ {α : Type u_1} {β : Type u_2} {f : Filter (α × β)}, f ≤ Filter.map Prod.fst f ×ˢ Filter.map Prod.snd f
-- Mathlib.RingTheory.Derivation.Basic
Derivation.map_one_eq_zero : ∀ {R : Type u_1} {A : Type u_2} {M : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring A]
  [inst_2 : AddCommMonoid M] [inst_3 : Algebra R A] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M),
  D 1 = 0
-- Mathlib.Order.WithBot
WithTop.map_comp_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β) (g : β → γ),
  WithTop.map g ∘ WithTop.map f = WithTop.map (g ∘ f)
-- Std.Tactic.BVDecide.Normalize.Canonicalize
Std.Tactic.BVDecide.Normalize.Bool.decide_eq_true : ∀ (a : Bool), decide (a = true) = a
-- Mathlib.Order.Lattice
sup_sup_distrib_right : ∀ {α : Type u} [inst : SemilatticeSup α] (a b c : α), a ⊔ b ⊔ c = a ⊔ c ⊔ (b ⊔ c)
-- Mathlib.CategoryTheory.Abelian.Exact
CategoryTheory.ShortComplex.exact_iff_exact_coimage_π : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C),
  S.Exact ↔
    { X₁ := S.X₁, X₂ := S.X₂, X₃ := CategoryTheory.Abelian.coimage S.g, f := S.f,
        g := CategoryTheory.Abelian.coimage.π S.g, zero := ⋯ }.Exact
-- Init.Data.Ord.Basic
List.isGE_compare_nil_left : ∀ {α : Type u_1} [inst : Ord α] {xs : List α}, (compare [] xs).isGE = true ↔ xs = []
-- Mathlib.Combinatorics.Graph.Maps
Graph.IsSpanningSubgraph.map : ∀ {α : Type u_1} {α' : Type u_2} {β : Type u_4} {G H : Graph α β} (f : α → α'), G ≤s H → Graph.map f G ≤s Graph.map f H
-- Init.Data.Fin.Lemmas
Fin.succ_cast_eq : ∀ {n n' : ℕ} (i : Fin n) (h : n = n'), (Fin.cast h i).succ = Fin.cast ⋯ i.succ
-- Mathlib.Algebra.Order.ToIntervalMod
iUnion_Icc_zsmul : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [IsOrderedAddMonoid α] [Archimedean α] {p : α},
  0 < p → ⋃ n, Set.Icc (n • p) ((n + 1) • p) = Set.univ
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.norm_eq_norm_adjoin : ∀ {L : Type u_6} (K : Type u_7) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (x : L),
  (Algebra.norm K) x = (Algebra.norm K) (IntermediateField.AdjoinSimple.gen K x) ^ Module.finrank (↥K⟮x⟯) L
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
/-- The characterization of weak convergence of probability measures by the usual (defining)
condition that the integrals of every continuous bounded function are continuous.  -/
MeasureTheory.ProbabilityMeasure.continuous_iff_forall_continuous_integral : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {X : Type u_2} [inst_3 : TopologicalSpace X] {μs : X → MeasureTheory.ProbabilityMeasure Ω},
  Continuous μs ↔ ∀ (f : BoundedContinuousFunction Ω ℝ), Continuous fun x => ∫ (ω : Ω), f ω ∂↑(μs x)
-- Mathlib.NumberTheory.RatFunc.Ostrowski
RatFunc.valuation_eq_valuation_uniformizingPolynomial_pow_of_valuation_X_le_one : ∀ {K : Type u_1} {Γ : Type u_2} [inst : Field K] [inst_1 : LinearOrderedCommGroupWithZero Γ]
  {v : Valuation (RatFunc K) Γ} [inst_2 : v.IsNontrivial] [inst_3 : Valuation.IsTrivialOn K v] (hle : v RatFunc.X ≤ 1)
  {p : Polynomial K},
  p ≠ 0 →
    v ((algebraMap (Polynomial K) (RatFunc K)) p) =
      v
        (↑(RatFunc.uniformizingPolynomial hle) ^
          (Associates.mk (RatFunc.valuationIdeal hle).asIdeal).count (Associates.mk (Ideal.span {p})).factors)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Basic
NumberField.InfinitePlace.fintype : {K : Type u_1} → [inst : Field K] → [NumberField K] → Fintype (NumberField.InfinitePlace K)
-- Mathlib.LinearAlgebra.Multilinear.Basic
/-- In the specific case of multilinear maps on spaces indexed by `Fin (n+1)`, where one can build
an element of `∀ (i : Fin (n+1)), M i` using `cons`, one can express directly the additivity of a
multilinear map along the first variable.  -/
MultilinearMap.cons_add : ∀ {R : Type uR} {n : ℕ} {M : Fin n.succ → Type v} {M₂ : Type v₂} [inst : Semiring R]
  [inst_1 : (i : Fin n.succ) → AddCommMonoid (M i)] [inst_2 : AddCommMonoid M₂]
  [inst_3 : (i : Fin n.succ) → Module R (M i)] [inst_4 : Module R M₂] (f : MultilinearMap R M M₂)
  (m : (i : Fin n) → M i.succ) (x y : M 0), f (Fin.cons (x + y) m) = f (Fin.cons x m) + f (Fin.cons y m)
-- Batteries.Data.BinomialHeap.Basic
_private.Batteries.Data.BinomialHeap.Basic.0.Batteries.BinomialHeap.Imp.Heap.merge.match_1.splitter : {α : Type u_1} →
  (motive : α × Batteries.BinomialHeap.Imp.HeapNode α → Sort u_2) →
    (x : α × Batteries.BinomialHeap.Imp.HeapNode α) →
      ((a : α) → (n : Batteries.BinomialHeap.Imp.HeapNode α) → motive (a, n)) → motive x
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_one : ∀ {w i : ℕ}, (1#w).getLsbD i = (decide (0 < w) && decide (i = 0))
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.fold_eq_foldl_toArray : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashSet.Raw α} {δ : Type v} {f : δ → α → δ} {init : δ},
  m.WF → Std.HashSet.Raw.fold (fun d a => f d a) init m = Array.foldl f init m.toArray
-- Lean.Expr
_private.Lean.Expr.0.Lean.intEqPred : Lean.Expr
-- Mathlib.Algebra.Star.Basic
mem_of_star_mem : ∀ {S : Type u_1} {R : Type u_2} [inst : InvolutiveStar R] [inst_1 : SetLike S R] [StarMemClass S R] {s : S} {r : R},
  star r ∈ s → r ∈ s
-- Mathlib.Topology.Subpath
/-- The subpath of `γ` from `t` to `t` is just the constant path at `γ t`.  -/
Path.subpath_self : ∀ {X : Type u_1} [inst : TopologicalSpace X] {a b : X} (γ : Path a b) (t : ↑unitInterval),
  γ.subpath t t = Path.refl (γ t)
-- Mathlib.Order.Heyting.Hom
BiheytingHomClass.toHeytingHomClass : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : BiheytingAlgebra α]
  {x : BiheytingAlgebra β} [BiheytingHomClass F α β], HeytingHomClass F α β
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.add_mem : ∀ {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid M]
  [inst_3 : SMul R M] (C : ConvexCone R M) ⦃x : M⦄, x ∈ C → ∀ ⦃y : M⦄, y ∈ C → x + y ∈ C
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.filter_tag : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.TaggedPrepartition I) (p : BoxIntegral.Box ι → Prop),
  (π.filter p).tag = π.tag
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.instInhabited : {R : Type u} → [inst : NonAssocRing R] → Inhabited (Subring R)
-- Mathlib.Analysis.Normed.Ring.Basic
MulOpposite.instNormedRing : {α : Type u_2} → [NormedRing α] → NormedRing αᵐᵒᵖ
-- Mathlib.Algebra.Ring.Submonoid.Pointwise
AddSubmonoid.mul_le : ∀ {R : Type u_2} [inst : NonUnitalNonAssocSemiring R] {M N P : AddSubmonoid R}, M * N ≤ P ↔ ∀ m ∈ M, ∀ n ∈ N, m * n ∈ P
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.rankMax_push : ∀ {m : Batteries.UnionFind}, m.push.rankMax = m.rankMax
-- Mathlib.ModelTheory.Definability
FirstOrder.Language.DefinableSet.instSetLike : {L : FirstOrder.Language} →
  {M : Type w} → [inst : L.Structure M] → {A : Set M} → {α : Type u₁} → SetLike (L.DefinableSet A α) (α → M)
-- Mathlib.Algebra.Module.Projective
/-- A projective R-module has the property that maps from it lift along surjections.  -/
Module.projective_lifting_property : ∀ {R : Type u_1} [inst : Semiring R] {P : Type u_2} [inst_1 : AddCommMonoid P] [inst_2 : Module R P] {M : Type u_3}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_4} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  [h : Module.Projective R P] (f : M →ₗ[R] N) (g : P →ₗ[R] N), Function.Surjective ⇑f → ∃ h, f ∘ₗ h = g
-- Mathlib.Algebra.Colimit.Ring
/-- If the maps in the directed system are injective, then the canonical maps
from the components to the direct limits are injective.  -/
Ring.DirectLimit.of_injective : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  (f' : (i j : ι) → i ≤ j → G i →+* G j) [IsDirectedOrder ι] [DirectedSystem G fun i j h => ⇑(f' i j h)],
  (∀ (i j : ι) (hij : i ≤ j), Function.Injective ⇑(f' i j hij)) →
    ∀ (i : ι), Function.Injective ⇑(Ring.DirectLimit.of G (fun i j h => ⇑(f' i j h)) i)
-- Mathlib.LinearAlgebra.Quotient.Defs
Submodule.Quotient.isScalarTower : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S : Type u_3}
  [inst_3 : SMul S R] [inst_4 : SMul S M] [inst_5 : IsScalarTower S R M] (P : Submodule R M) (T : Type u_4)
  [inst_6 : SMul T R] [inst_7 : SMul T M] [inst_8 : IsScalarTower T R M] [inst_9 : SMul S T] [IsScalarTower S T M],
  IsScalarTower S T (M ⧸ P)
-- Mathlib.Order.Shrink
equivShrink_bot : ∀ {α : Type u_1} [inst : Small.{u, u_1} α] [inst_1 : Bot α], (equivShrink α) ⊥ = ⊥
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.sPolynomial_lt_of_degree_ne_zero_of_degree_eq : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommRing R] {f g : MvPolynomial σ R},
  m.degree f = m.degree g → m.sPolynomial f g ≠ 0 → m.toSyn (m.degree (m.sPolynomial f g)) < m.toSyn (m.degree f)
-- Mathlib.Tactic.CategoryTheory.Bicategory.PureCoherence
Mathlib.Tactic.Bicategory.instMkEqOfNaturalityBicategoryM : Mathlib.Tactic.BicategoryLike.MkEqOfNaturality Mathlib.Tactic.Bicategory.BicategoryM
-- Plausible.Random
/-- Create a new random number generator distinct from the one stored in the state  -/
Plausible.Rand.split : {m : Type → Type u_1} → {g : Type} → [RandomGen g] → [Monad m] → Plausible.RandGT g m g
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.valUnknown : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Data.Set.Semiring
SetSemiring.zero_def : ∀ {α : Type u_1}, 0 = Set.up ∅
-- Lean.Server.Requests
Lean.Server.partialLspRequestHandlerMethods : IO (Array (String × String × ℕ))
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.single_neg : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddGroup R] (a : Γ) (r : R),
  (HahnSeries.single a) (-r) = -(HahnSeries.single a) r
-- Mathlib.Algebra.DualNumber
/-- The type of dual numbers, numbers of the form $a + bε$ where $ε^2 = 0$.
`R[ε]` is notation for `DualNumber R`.  -/
DualNumber : Type u_4 → Type u_4
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.sub_right_injective_of_ne_top : ∀ {α : Type u_2} [inst : LinearOrderedAddCommGroupWithTop α] {b : α}, b ≠ ⊤ → Function.Injective fun x => b - x
-- Lean.Elab.PreDefinition.Structural.RecArgInfo
/-- position of the indices of the inductive datatype we are recursing on, among all parameters  -/
Lean.Elab.Structural.RecArgInfo.indicesPos : Lean.Elab.Structural.RecArgInfo → Array ℕ
-- Init.Data.SInt.Lemmas
ISize.toInt_div_of_ne_right : ∀ (a b : ISize), b ≠ -1 → (a / b).toInt = a.toInt.tdiv b.toInt
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_of_tendsto : ∀ {f : ℕ → ℝ} {r : ℝ}, Filter.Tendsto f Filter.atTop (nhds r) → (Hyperreal.ofSeq f).IsSt r
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.ISize.maxValueSealed_def : ISize.maxValueSealed✝ = ISize.maxValue
-- Mathlib.Analysis.Complex.Norm
Complex.abs_re_eq_norm : ∀ {z : ℂ}, |z.re| = ‖z‖ ↔ z.im = 0
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc_f : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' : κ) (i₀ i₁ i₂ i₃ i₃' : ι) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq')
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc._auto_3),
  (CategoryTheory.Abelian.SpectralObject.SpectralSequence.HomologyData.ccSc X data r r' hrr' hr pq pq' i₀ i₁ i₂ i₃ i₃'
        hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂).f =
    CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageD X data r pq pq' ⋯
-- Mathlib.Algebra.CubicDiscriminant
Cubic.of_b_eq_zero' : ∀ {R : Type u_1} {c d : R} [inst : Semiring R],
  { a := 0, b := 0, c := c, d := d }.toPoly = Polynomial.C c * Polynomial.X + Polynomial.C d
-- Std.Data.DHashMap.Internal.Raw
_private.Std.Data.DHashMap.Internal.Raw.0.Std.DHashMap.Raw.erase.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Raw α β) (a : α),
  m.erase a = if h : 0 < m.buckets.size then ↑(Std.DHashMap.Internal.Raw₀.erase ⟨m, h⟩ a) else m
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_unitOfList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l →
      k ∈ l → (Std.DTreeMap.Raw.Const.unitOfList l cmp).getKey? k' = some k
-- Mathlib.Algebra.Order.GroupWithZero.Defs
/-- Pullback `MulPosStrictMono`.  -/
Function.Injective.mulPosStrictMono : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [MulPosStrictMono α] {β : Type u_2}
  [inst_4 : Zero β] [inst_5 : Mul β] [inst_6 : Preorder β] (f : β → α),
  f 0 = 0 → (∀ (x y : β), f (x * y) = f x * f y) → (∀ {x y : β}, f x < f y ↔ x < y) → MulPosStrictMono β
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
/-- In a `LawfulDayConvolutionMonoidalCategoryStruct`, `ι.obj (d ⊗ d' ⊗ d'')`
is a (triple) Day convolution of `(ι C V).obj d`, `(ι C V).obj d'` and
`(ι C V).obj d''`.  -/
CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.convolution₂ : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (V : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} V] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          [inst_3 : CategoryTheory.MonoidalCategory V] →
            (D : Type u₃) →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} D] →
                [inst_5 : CategoryTheory.MonoidalCategoryStruct D] →
                  [inst_6 : CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct C V D] →
                    (d d' d'' : D) →
                      CategoryTheory.MonoidalCategory.DayConvolution
                        ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d)
                        (CategoryTheory.MonoidalCategory.DayConvolution.convolution
                          ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj d')
                          ((CategoryTheory.MonoidalCategory.LawfulDayConvolutionMonoidalCategoryStruct.ι C V D).obj
                            d''))
-- Init.Data.BitVec.Lemmas
BitVec.msb_xor : ∀ {w : ℕ} {x y : BitVec w}, (x ^^^ y).msb = (x.msb ^^ y.msb)
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.MemLp.mono_measure : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {p : ENNReal} {μ ν : MeasureTheory.Measure α} {ε : Type u_7}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {f : α → ε},
  ν ≤ μ → MeasureTheory.MemLp f p μ → MeasureTheory.MemLp f p ν
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.cofan_inj_f_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {𝒜 : Type w} {f : 𝒜 → CategoryTheory.Limits.FormalCoproduct C}
  (i : 𝒜) (x : (f i).I), (((CategoryTheory.Limits.FormalCoproduct.cofan 𝒜 f).inj i).f x).snd = x
-- Mathlib.SetTheory.ZFC.Class
instEmptyCollectionClass : EmptyCollection Class.{u_1}
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelAddMonoid.le_of_add_le_add_right : ∀ {α : Type u_2} {inst : AddCommMonoid α} {inst_1 : Preorder α} [self : IsOrderedCancelAddMonoid α] (a b c : α),
  b + a ≤ c + a → b ≤ c
-- Mathlib.Analysis.Calculus.IteratedDeriv.Defs
/-- The property of being `C^n`, initially defined in terms of the Fréchet derivative, can be
reformulated in terms of the one-dimensional derivative.  -/
contDiff_iff_iteratedDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type u_2} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {n : ℕ∞},
  ContDiff 𝕜 (↑n) f ↔
    (∀ (m : ℕ), ↑m ≤ n → Continuous (iteratedDeriv m f)) ∧ ∀ (m : ℕ), ↑m < n → Differentiable 𝕜 (iteratedDeriv m f)
-- Lean.Parser.Command
Lean.Parser.Command.addDocString.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
/-- `LinearEquiv.prodComm` is isometric.  -/
QuadraticMap.IsometryEquiv.prodComm : {R : Type u_2} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      {P : Type u_7} →
        [inst : CommSemiring R] →
          [inst_1 : AddCommMonoid M₁] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid P] →
                [inst_4 : Module R M₁] →
                  [inst_5 : Module R M₂] →
                    [inst_6 : Module R P] →
                      (Q₁ : QuadraticMap R M₁ P) → (Q₂ : QuadraticMap R M₂ P) → (Q₁.prod Q₂).IsometryEquiv (Q₂.prod Q₁)
-- Mathlib.NumberTheory.Padics.MahlerBasis
/-- Explicit bound for the decay rate of the Mahler coefficients of a continuous function on `ℤ_[p]`.
This will be used to prove Mahler's theorem.
 -/
PadicInt.fwdDiff_iter_le_of_forall_le : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : Module ℤ_[p] E]
  [IsBoundedSMul ℤ_[p] E] [IsUltrametricDist E] {f : C(ℤ_[p], E)} {s t : ℕ},
  (∀ (x y : ℤ_[p]), ‖x - y‖ ≤ ↑p ^ (-↑t) → ‖f x - f y‖ ≤ ‖f‖ / ↑p ^ s) →
    ∀ (n : ℕ), ‖(fwdDiff 1)^[n + s * p ^ t] (⇑f) 0‖ ≤ ‖f‖ / ↑p ^ s
-- Mathlib.Computability.Ackermann
Nat.Partrec.Code.pappAck.step.eq_1 : ∀ (c : Nat.Partrec.Code),
  Nat.Partrec.Code.pappAck.step c =
    ((c.comp (Nat.Partrec.Code.const 1)).prec (c.comp (Nat.Partrec.Code.right.comp Nat.Partrec.Code.right))).curry 0
-- Mathlib.RingTheory.TensorProduct.IncludeLeftSubRight
/-- If `S` is a faithfully flat `R`-algebra, `codRestrictEqLocusPushoutCocone` is bijective.  -/
Algebra.codRestrictEqLocusPushoutCocone.bijective_of_faithfullyFlat : ∀ (R S : Type u) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.FaithfullyFlat R S],
  Function.Bijective ⇑(Algebra.codRestrictEqLocusPushoutCocone R S)
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.supportedEquivFinsupp_apply_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M) (x : ↥(AddMonoidAlgebra.supported R S s)) (a : { x // x ∈ s }),
  ((AddMonoidAlgebra.supportedEquivFinsupp s) x) a = (↑x).coeff ↑a
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
/-- Given a root-positive form associated to a root pairing with coefficients in `R` but taking
values in `S`, this is the associated `S`-bilinear form on the `S`-span of the roots.  -/
RootPairing.RootPositiveForm.posForm : {ι : Type u_1} →
  {R : Type u_2} →
    {S : Type u_3} →
      {M : Type u_4} →
        {N : Type u_5} →
          [inst : CommRing S] →
            [inst_1 : LinearOrder S] →
              [inst_2 : CommRing R] →
                [inst_3 : Algebra S R] →
                  [inst_4 : AddCommGroup M] →
                    [inst_5 : Module R M] →
                      [inst_6 : AddCommGroup N] →
                        [inst_7 : Module R N] →
                          {P : RootPairing ι R M N} →
                            [inst_8 : P.IsValuedIn S] →
                              RootPairing.RootPositiveForm S P →
                                [FaithfulSMul S R] →
                                  [inst_10 : Module S M] →
                                    [IsScalarTower S R M] →
                                      LinearMap.BilinForm S ↥(Submodule.span S (Set.range ⇑P.root))
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.eq_of_le : ∀ {ι : Type u_1} {I J₁ J₂ : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), J₁ ∈ π → J₂ ∈ π → J₁ ≤ J₂ → J₁ = J₂
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- If `y ∈ f.target` and `I y ∈ interior (range I)`,
then `I y` is an interior point of `(I ∘ f).target`.  -/
OpenPartialHomeomorph.mem_interior_extend_target : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  (f : OpenPartialHomeomorph M H) {I : ModelWithCorners 𝕜 E H} {y : H},
  y ∈ f.target → ↑I y ∈ interior (Set.range ↑I) → ↑I y ∈ interior (f.extend I).target
-- Mathlib.AlgebraicGeometry.Spec
AlgebraicGeometry.Spec_Γ_naturality_assoc : ∀ {R S : CommRingCat} (f : R ⟶ S) {Z : CommRingCat}
  (h :
    AlgebraicGeometry.LocallyRingedSpace.Γ.obj
        (Opposite.op (AlgebraicGeometry.Spec.toLocallyRingedSpace.obj (Opposite.op S))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.toSpecΓ S) h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.toSpecΓ R)
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.LocallyRingedSpace.Γ.map (AlgebraicGeometry.Spec.toLocallyRingedSpace.map f.op).op) h)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Grp
CategoryTheory.AddGrp.Hom.hom_hom_sub : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H : CategoryTheory.AddGrp C}
  [inst_3 : CategoryTheory.IsCommAddMonObj H.X] (f g : G ⟶ H), (f - g).hom.hom = f.hom.hom - g.hom.hom