mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.Basic
/-- The Cartesian product of `C^n` functions on domains is `C^n`.  -/
ContDiffOn.prodMk : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {n : WithTop ℕ∞} {s : Set E} {f : E → F} {g : E → G},
  ContDiffOn 𝕜 n f s → ContDiffOn 𝕜 n g s → ContDiffOn 𝕜 n (fun x => (f x, g x)) s
-- Mathlib.Algebra.GroupWithZero.Hom
MonoidWithZeroHom.coe_mk : ∀ {α : Type u_2} {β : Type u_3} [inst : MulZeroOneClass α] [inst_1 : MulZeroOneClass β] (f : ZeroHom α β)
  (h1 : f.toFun 1 = 1) (hmul : ∀ (x y : α), f.toFun (x * y) = f.toFun x * f.toFun y),
  ⇑{ toZeroHom := f, map_one' := h1, map_mul' := hmul } = ⇑f
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zigzag.of_inv_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₁ j₂ j₃ : J} (f₂₁ : j₂ ⟶ j₁) (f₃₂ : j₃ ⟶ j₂),
  CategoryTheory.Zigzag j₁ j₃
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- The predicate `IsFraction` is "prelocal", in the sense that if it holds on `U` it holds on any open
subset `V` of `U`.
 -/
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isFractionPrelocal : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              TopCat.PrelocalPredicate fun x => HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.coeff_mapDomainRingEquiv : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (e : M ≃* N)
  (x : MonoidAlgebra R M), ((MonoidAlgebra.mapDomainRingEquiv R e) x).coeff = Finsupp.equivMapDomain (↑e) x.coeff
-- Mathlib.Computability.RegularExpressions
RegularExpression.matches'.eq_6 : ∀ {α : Type u_1} (P : RegularExpression α), P.star.matches' = KStar.kstar P.matches'
-- Mathlib.ModelTheory.Order
/-- The theory of partial orders.  -/
FirstOrder.Language.partialOrderTheory : (L : FirstOrder.Language) → [L.IsOrdered] → L.Theory
-- Mathlib.Topology.List
List.tendsto_cons_iff : ∀ {α : Type u_1} [inst : TopologicalSpace α] {β : Type u_3} {f : List α → β} {b : Filter β} {a : α} {l : List α},
  Filter.Tendsto f (nhds (a :: l)) b ↔ Filter.Tendsto (fun p => f (p.1 :: p.2)) (nhds a ×ˢ nhds l) b
-- Mathlib.CategoryTheory.Products.Basic
/-- The isomorphism between `(X.1, X.2)` and `X`.  -/
CategoryTheory.prod.etaIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} → [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (X : C × D) → (X.1, X.2) ≅ X
-- Mathlib.Topology.EMetricSpace.VariationOnFromTo
variationOnFromTo.nonneg_of_le : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] (f : α → E) (s : Set α)
  {a b : α}, a ≤ b → 0 ≤ variationOnFromTo f s a b
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
CategoryTheory.OverPresheafAux.unitAuxAux_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A F : CategoryTheory.Functor Cᵒᵖ (Type v)} (η : F ⟶ A)
  (X : Cᵒᵖ),
  (CategoryTheory.OverPresheafAux.unitAuxAux η).inv.app X =
    TypeCat.ofHom (CategoryTheory.OverPresheafAux.unitBackward η (Opposite.unop X))
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.contract_comm : ∀ {α : Type u_1} (M : Matroid α) (C₁ C₂ : Set α), (M.contract C₁).contract C₂ = (M.contract C₂).contract C₁
-- Init.Data.Vector.MapIdx
Vector.mapFinIdxM.map.eq_1 : ∀ {n : ℕ} {α : Type u} {β : Type v} {m : Type v → Type w} [inst : Monad m] (xs : Vector α n)
  (f : (i : ℕ) → α → i < n → m β) (j : ℕ) (inv_2 : 0 + j = n) (ys : Vector β (n - 0)),
  Vector.mapFinIdxM.map xs f 0 j inv_2 ys = pure (Vector.cast ⋯ ys)
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.snd_isOpenEmbedding_of_left : ∀ {X Y S : TopCat} {f : X ⟶ S},
  Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f) →
    ∀ (g : Y ⟶ S),
      Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.snd f g))
-- Mathlib.Analysis.Normed.Order.UpperLower
IsLowerSet.cthickening' : ∀ {α : Type u_1} [inst : NormedCommGroup α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s : Set α},
  IsLowerSet s → ∀ (ε : ℝ), IsLowerSet (Metric.cthickening ε s)
-- Mathlib.RingTheory.DedekindDomain.Factorization
/-- **Alias** of `Ideal.map_algebraMap_eq_finsetProd_pow`.

---

If `p` is a maximal ideal, then the lift of `p` in an extension is the product of the primes
over `p` to the power the ramification index.
 -/
Ideal.map_algebraMap_eq_finset_prod_pow : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : Algebra S R] [inst_4 : Algebra.IsIntegral S R] [inst_5 : IsDomain S] [inst_6 : Module.IsTorsionFree S R]
  {p : Ideal S} [inst_7 : p.IsMaximal],
  p ≠ 0 → Ideal.map (algebraMap S R) p = ∏ P ∈ (p.primesOver R).toFinset, P ^ P.ramificationIdx S
-- Mathlib.CategoryTheory.Galois.Decomposition
/-- The trivial case if `X` is connected.  -/
_private.Mathlib.CategoryTheory.Galois.Decomposition.0.CategoryTheory.PreGaloisCategory.has_decomp_connected_components_aux_conn : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (X : C) [CategoryTheory.PreGaloisCategory.IsConnected X],
  ∃ ι f g x, (∀ (i : ι), CategoryTheory.PreGaloisCategory.IsConnected (f i)) ∧ Finite ι
-- Mathlib.Analysis.RCLike.Inner
RCLike.wInner_nonneg : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : Fintype ι] [inst_1 : RCLike 𝕜] {w : ι → ℝ} {f g : ι → 𝕜},
  0 ≤ w → 0 ≤ f → 0 ≤ g → 0 ≤ ⟪f, g⟫_[𝕜, w]
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- **Alias** of the reverse direction of `Equiv.Perm.isCycleOn_one`. -/
Set.Subsingleton.isCycleOn_one : ∀ {α : Type u_2} {s : Set α}, s.Subsingleton → Equiv.Perm.IsCycleOn 1 s
-- Mathlib.Algebra.Group.PNatPowAssoc
/-- Exponent one is identity.  -/
PNatPowAssoc.ppow_one : ∀ {M : Type u_2} {inst : Mul M} {inst_1 : Pow M ℕ+} [self : PNatPowAssoc M] (x : M), x ^ 1 = x
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.setOfPred_isNonloop_eq : ∀ {α : Type u_1} (M : Matroid α), {e | M.IsNonloop e} = M.E \ M.loops
-- Mathlib.Algebra.Torsor.Defs
Equiv.coe_constSDiv : ∀ {G : Type u_1} {P : Type u_2} [inst : Group G] [inst_1 : Torsor G P] (p : P), ⇑(Equiv.constSDiv p) = fun x => p /ₛ x
-- Init.Core
/-- If two values are equal in a quotient, then they are related by its equivalence relation.
 -/
Quotient.exact : ∀ {α : Sort u} {s : Setoid α} {a b : α}, ⟦a⟧ = ⟦b⟧ → a ≈ b
-- Mathlib.Order.Hom.WithTopBot
/-- The coercion `α → WithBot α` bundled as monotone map.  -/
WithBot.coeOrderHom : {α : Type u_4} → [inst : Preorder α] → α ↪o WithBot α
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.Equiv.toArray_eq : ∀ {m : Type u_1 → Type u_2} {α₁ β α₂ : Type u_1} [inst : Monad m] [inst_1 : LawfulMonad m]
  [inst_2 : Std.Iterator α₁ m β] [inst_3 : Std.Iterator α₂ m β] [Std.Iterators.Finite α₁ m] [Std.Iterators.Finite α₂ m]
  {ita : Std.IterM m β} {itb : Std.IterM m β}, ita.Equiv itb → ita.toArray = itb.toArray
-- Mathlib.Combinatorics.Additive.ApproximateSubgroup
IsApproximateAddSubgroup.of_small_tripling : ∀ {G : Type u_1} [inst : AddGroup G] {K : ℝ} [inst_1 : DecidableEq G] {A : Finset G},
  0 ∈ A → -A = A → ↑(3 • A).card ≤ K * ↑A.card → IsApproximateAddSubgroup (K ^ 3) (2 • ↑A)
-- Mathlib.Dynamics.Circle.RotationNumber.TranslationNumber
CircleDeg1Lift.units_apply_inv_apply : ∀ (f : CircleDeg1Liftˣ) (x : ℝ), ↑f (↑f⁻¹ x) = x
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
Std.DHashMap.Internal.AssocList.getCastD.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] (a : α) (fallback fallback_1 : β a),
  fallback = fallback_1 →
    ∀ (a_1 a_2 : Std.DHashMap.Internal.AssocList α β),
      a_1 = a_2 →
        Std.DHashMap.Internal.AssocList.getCastD a fallback a_1 =
          Std.DHashMap.Internal.AssocList.getCastD a fallback_1 a_2
-- Mathlib.Algebra.Group.Ideal
AddSemigroupIdeal.closure_mono : ∀ {M : Type u_1} [inst : Add M] {s t : Set M}, s ⊆ t → AddSemigroupIdeal.closure s ≤ AddSemigroupIdeal.closure t
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.splitUpper_le : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ}, I.splitUpper i x ≤ ↑I
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder_foldl_mem_of_mem : ∀ {n : ℕ} {acc : Option (Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool)}
  {ls : List (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))}
  {map : Std.HashMap (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) Bool},
  List.foldl Std.Tactic.BVDecide.LRAT.Internal.DefaultClause.ofArray.folder acc ls = some map → ∀ l ∈ ls, l ∈ map.toList
-- Mathlib.Data.Matrix.Mul
Matrix.one_vecMul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype m] (A : Matrix m n α),
  Matrix.vecMul 1 A = ∑ i, A i
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.map_nhds_eq : ∀ {𝕜 : 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) (x : H),
  Filter.map (↑I) (nhds x) = nhdsWithin (↑I x) (Set.range ↑I)
-- Init.Data.BitVec.Lemmas
BitVec.toFin_xor : ∀ {v : ℕ} (x y : BitVec v), (x ^^^ y).toFin = x.toFin ^^^ y.toFin
-- Mathlib.Data.Finsupp.Lex
Finsupp.instLTColex : {α : Type u_1} → {N : Type u_2} → [inst : Zero N] → [LT α] → [LT N] → LT (Colex (α →₀ N))
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.unop_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S : CategoryTheory.ShortComplex Cᵒᵖ} (h : S.HomologyData), h.unop.right = h.left.unop
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.instLattice : {X : TopCat} → (x : ↑X) → Lattice (TopologicalSpace.OpenNhds x)
-- Init.Meta.Defs
_private.Init.Meta.Defs.0.Lean.Name.beq.eq_2 : ∀ (p₁ : Lean.Name) (s₁ : String) (p₂ : Lean.Name) (s₂ : String), (p₁.str s₁).beq (p₂.str s₂) = (s₁ == s₂ && p₁.beq p₂)
-- Mathlib.NumberTheory.FLT.Basic
/-- To prove Fermat Last Theorem in any semiring that is a `NormalizedGCDMonoid` one can assume
that the `gcd` of `{a, b, c}` is `1`.  -/
fermatLastTheoremWith_of_fermatLastTheoremWith_coprime : ∀ {n : ℕ} {R : Type u_2} [inst : CommSemiring R] [IsDomain R] [inst_2 : DecidableEq R] [inst_3 : NormalizedGCDMonoid R],
  (∀ (a b c : R), a ≠ 0 → b ≠ 0 → c ≠ 0 → {a, b, c}.gcd id = 1 → a ^ n + b ^ n ≠ c ^ n) → FermatLastTheoremWith R n
-- Mathlib.Control.Bifunctor
Bifunctor.comp_fst : ∀ {F : Type u₀ → Type u₁ → Type u₂} [inst : Bifunctor F] [LawfulBifunctor F] {α₀ α₁ α₂ : Type u₀} {β : Type u₁}
  (f : α₀ → α₁) (f' : α₁ → α₂) (x : F α₀ β), Bifunctor.fst f' (Bifunctor.fst f x) = Bifunctor.fst (f' ∘ f) x
-- Init.Data.Dyadic.Basic
/-- Rounds a dyadic rational `x` down to the greatest dyadic number with precision at most `prec`
which is less than or equal to `x`.
 -/
Dyadic.roundDown : Dyadic → ℤ → Dyadic
-- Mathlib.CategoryTheory.Limits.Presheaf
CategoryTheory.Presheaf.instUniqueHomLeftExtensionOppositeOpObjFunctorTypeUliftYonedaMkUliftYonedaMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          (X : C) →
            (Y : F.op.LeftExtension (CategoryTheory.uliftYoneda.{max w v₂, v₁, u₁}.obj X)) →
              Unique
                (CategoryTheory.Functor.LeftExtension.mk (CategoryTheory.uliftYoneda.{max w v₁, v₂, u₂}.obj (F.obj X))
                    (CategoryTheory.uliftYonedaMap F X) ⟶
                  Y)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of a strictly antitone function and an antitone function is
strictly antitone.  -/
StrictAnti.add_antitone : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} [AddLeftMono α]
  [AddRightStrictMono α], StrictAnti f → Antitone g → StrictAnti fun x => f x + g x
-- Mathlib.Order.Hom.Bounded
BoundedOrderHom.instBoundedOrderHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β], BoundedOrderHomClass (BoundedOrderHom α β) α β
-- Mathlib.Order.WellFoundedSet
Set.IsWF.min_eq_of_le : ∀ {α : Type u_2} [inst : PartialOrder α] {s : Set α} {a : α} (hs : s.IsWF) (ha : a ∈ s), (∀ b ∈ s, a ≤ b) → hs.min ⋯ = a
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_mul_eq : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  {ab ∈ A ×ˢ B | ab.1 * ab.2 = x}.card = A.convolution B x
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- Construct the simple graph induced by the given relation. It
symmetrizes the relation and makes it irreflexive.  -/
SimpleGraph.fromRel : {V : Type u} → (V → V → Prop) → SimpleGraph V
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k fallback : α},
  k ∉ t₁ → (t₁ \ t₂).getKeyD k fallback = fallback
-- Mathlib.Tactic.Order
/-- `order` solves the main goal if it can be derived from the local hypotheses and the axioms of
`Preorder`, `PartialOrder` or `LinearOrder`. Also supports `⊤`, `⊥` and lattice operations.

This tactic fails if it cannot prove the main goal.

* `order [e₁, ..., eₙ]` uses the terms `e₁`, ... `eₙ` as hypotheses, in addition to the local
  context.
* `order only [e₁, ..., eₙ]` uses only the terms `e₁`, ... `eₙ` as hypotheses (ignoring the local
  context).
 -/
Mathlib.Tactic.Order.tacticOrder_ : Lean.ParserDescr
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.union_sub_inter_subset_union : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Sub α] {s₁ s₂ t₁ t₂ : Finset α},
  s₁ ∪ s₂ - t₁ ∩ t₂ ⊆ s₁ - t₁ ∪ (s₂ - t₂)
-- Mathlib.Data.List.Infix
List.IsInfix.flatten : ∀ {α : Type u_1} {l₁ l₂ : List (List α)}, l₁ <:+: l₂ → l₁.flatten <:+: l₂.flatten
-- Mathlib.NumberTheory.Height.MvPolynomial
Height.mulHeight_sym2_le : ∀ (K : Type u_4) [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K],
  ∃ C > 0,
    ∀ (a b c d : K),
      Height.mulHeight ![a * c, a * d + b * c, b * d] ≤ C * Height.mulHeight ![a, b] * Height.mulHeight ![c, d]
-- Init.Data.UInt.Bitwise
instIdempotentOpUInt32HAnd : Std.IdempotentOp fun x1 x2 => x1 &&& x2
-- Mathlib.NumberTheory.LSeries.RiemannZeta
/-- The Riemann zeta function `ζ(s)`.  -/
riemannZeta : ℂ → ℂ
-- Mathlib.Data.Nat.Choose.Factorization
/-- Contrapositive form of `Nat.factorization_centralBinom_eq_zero_of_two_mul_lt`  -/
Nat.le_two_mul_of_factorization_centralBinom_pos : ∀ {p n : ℕ}, 0 < n.centralBinom.factorization p → p ≤ 2 * n
-- Mathlib.Algebra.Module.Submodule.Lattice
/-- An additive submonoid is equivalent to a ℕ-submodule.  -/
AddSubmonoid.toNatSubmodule : {M : Type u_3} → [inst : AddCommMonoid M] → AddSubmonoid M ≃o Submodule ℕ M
-- Mathlib.CategoryTheory.Limits.Final.Type
CategoryTheory.Functor.bijective_colimitTypePrecomp : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (P : CategoryTheory.Functor D (Type w)) [F.Final],
  Function.Bijective (F.colimitTypePrecomp P)
-- Mathlib.CategoryTheory.Localization.HasLocalization
/-- the category structure.  -/
CategoryTheory.MorphismProperty.HasLocalization.hD : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {W : CategoryTheory.MorphismProperty C} →
      [self : W.HasLocalization] → CategoryTheory.Category.{w, u} (CategoryTheory.MorphismProperty.HasLocalization.D W)
-- Mathlib.Algebra.Ring.NonZeroDivisors
mul_cancel_right_mem_nonZeroDivisorsRight : ∀ {R : Type u_1} [inst : Ring R] {x y r : R}, r ∈ nonZeroDivisorsRight R → (x * r = y * r ↔ x = y)
-- Mathlib.Data.TypeVec
TypeVec.splitFun_comp : ∀ {n : ℕ} {α₀ : TypeVec.{u_1} (n + 1)} {α₁ : TypeVec.{u_2} (n + 1)} {α₂ : TypeVec.{u_3} (n + 1)}
  (f₀ : α₀.drop.Arrow α₁.drop) (f₁ : α₁.drop.Arrow α₂.drop) (g₀ : α₀.last → α₁.last) (g₁ : α₁.last → α₂.last),
  TypeVec.splitFun (TypeVec.comp f₁ f₀) (g₁ ∘ g₀) = TypeVec.comp (TypeVec.splitFun f₁ g₁) (TypeVec.splitFun f₀ g₀)
-- Lean.LocalContext
_private.Lean.LocalContext.0.Lean.LocalContext.popTailNoneAux : Lean.PArray (Option Lean.LocalDecl) → Lean.PArray (Option Lean.LocalDecl)
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Oplax.OplaxTrans.Modification η θ) {a b : B}
  {a' : C} (f : a ⟶ b) (g : G.obj b ⟶ a'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (F.map f) (CategoryTheory.Bicategory.whiskerRight (Γ.app b) g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (θ.app b) g).inv
        (CategoryTheory.Bicategory.whiskerRight (θ.naturality f) g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (η.app b) g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) g)
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (Γ.app a) (G.map f)) g))
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.frontier_setOfPred_re_le`. -/
Complex.frontier_setOf_re_le : ∀ (a : ℝ), frontier {z | z.re ≤ a} = {z | z.re = a}
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- Given a closed subgroup `H` of an additive topological group `G`, the right
action of `H` on `G` is proper. Note that the corresponding statement for the left action can be
proven by `inferInstance`.  -/
instProperVAddSubtypeAddOppositeMemAddSubgroupOpOfIsTopologicalAddGroupOfIsClosedCoe : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {H : AddSubgroup G}
  [H_closed : IsClosed ↑H], ProperVAdd (↥H.op) G
-- Mathlib.MeasureTheory.Measure.Typeclasses.NullSingletonClass
MeasureTheory.uIoc_ae_eq_interval : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.NullSingletonClass μ]
  [inst : LinearOrder α] {a b : α}, Set.uIoc a b =ᵐ[μ] Set.uIcc a b
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropSuffix?_eq_dropSuffix?_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.dropSuffix? pat = s.toSlice.dropSuffix? pat
-- Mathlib.Data.EReal.Operations
EReal.bot_mul_bot : ⊥ * ⊥ = ⊤
-- Mathlib.Algebra.Tropical.Basic
Tropical.instInhabited : {R : Type u} → [Inhabited R] → Inhabited (Tropical R)
-- Mathlib.Algebra.Category.Ring.Basic
/-- The category of semirings.  -/
SemiRingCat : Type (u + 1)
-- Mathlib.CategoryTheory.Limits.Constructions.BinaryProducts
inr_coprodIsoPushout_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasPushouts C] (X Y : C) [inst_3 : CategoryTheory.Limits.HasBinaryCoproduct X Y],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pushout.inr (CategoryTheory.Limits.initial.to X) (CategoryTheory.Limits.initial.to Y))
      (coprodIsoPushout X Y).inv =
    CategoryTheory.Limits.coprod.inr
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.mem_sSup_of_directedOn : ∀ {R : Type u} [inst : NonUnitalNonAssocSemiring R] {S : Set (NonUnitalSubsemiring R)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ∀ {x : R}, x ∈ sSup S ↔ ∃ s ∈ S, x ∈ s
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.preimage_vadd_closedEBall`. -/
EMetric.preimage_vadd_closedBall : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : AddGroup G] [inst_2 : AddAction G X]
  [IsIsometricVAdd G X] (c : G) (x : X) (r : ENNReal),
  (fun x => c +ᵥ x) ⁻¹' Metric.closedEBall x r = Metric.closedEBall (-c +ᵥ x) r
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- The natural coercion of `A` into `𝓜(𝕜, A)` given by sending `a : A` to the pair of linear
maps `Lₐ Rₐ : A →L[𝕜] A` given by left- and right-multiplication by `a`, respectively.

Warning: if `A = 𝕜`, then this is a coercion which is not definitionally equal to the
`algebraMap 𝕜 𝓜(𝕜, 𝕜)` coercion, but these are propositionally equal. See
`DoubleCentralizer.coe_eq_algebraMap` below.  -/
DoubleCentralizer.coe : (𝕜 : Type u_1) →
  {A : Type u_2} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : SMulCommClass 𝕜 A A] → [inst_4 : IsScalarTower 𝕜 A A] → A → DoubleCentralizer 𝕜 A
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovary_inv_left₀`. -/
Antivary.inv_left₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : LinearOrder β] {f : ι → α} {g : ι → β}, StrongLT 0 f → Antivary f g → Monovary f⁻¹ g
-- Lean.Elab.Tactic.Simp
Lean.Meta.Simp.ConfigWithOptions.config : Lean.Meta.Simp.ConfigWithOptions → Lean.Meta.Simp.Config
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyClosed
AlgebraicGeometry.Surjective.of_universallyClosed_of_isDominant : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.UniversallyClosed f] [AlgebraicGeometry.IsDominant f],
  AlgebraicGeometry.Surjective f
-- Mathlib.CategoryTheory.Opposites
CategoryTheory.NatTrans.removeRightOp_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor Cᵒᵖ D} (α : F.rightOp ⟶ G.rightOp) (X : Cᵒᵖ),
  (CategoryTheory.NatTrans.removeRightOp α).app X = (α.app (Opposite.unop X)).unop
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
UniformConvergenceCLM.nhds_zero_eq : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) {E : Type u_3}
  (F : Type u_4) [inst_2 : AddCommGroup E] [inst_3 : Module 𝕜₁ E] [inst_4 : TopologicalSpace E]
  [inst_5 : AddCommGroup F] [inst_6 : Module 𝕜₂ F] [inst_7 : TopologicalSpace F] [inst_8 : IsTopologicalAddGroup F]
  (𝔖 : Set (Set E)), nhds 0 = ⨅ s ∈ 𝔖, ⨅ t ∈ nhds 0, Filter.principal {f | Set.MapsTo (⇑f) s t}
-- Mathlib.Analysis.Calculus.ContDiff.Operations
/-- **Alias** of `fun_iteratedFDeriv_add_apply`.

---

Eta-expanded form of `iteratedFDeriv_add_apply` -/
iteratedFDeriv_add_apply' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {x : E} {i : ℕ}
  {f g : E → F},
  ContDiffAt 𝕜 (↑i) f x →
    ContDiffAt 𝕜 (↑i) g x → iteratedFDeriv 𝕜 i (fun i => f i + g i) x = iteratedFDeriv 𝕜 i f x + iteratedFDeriv 𝕜 i g x
-- Mathlib.NumberTheory.ModularForms.Derivative
Derivative.serreDerivative_mul : ∀ (k₁ k₂ : ℂ) (F G : UpperHalfPlane → ℂ),
  MDiff F →
    MDiff G →
      Derivative.serreDerivative (k₁ + k₂) (F * G) =
        Derivative.serreDerivative k₁ F * G + F * Derivative.serreDerivative k₂ G
-- Init.Data.SInt.Lemmas
Int64.toInt8_toISize : ∀ (n : Int64), n.toISize.toInt8 = n.toInt8
-- Mathlib.Probability.Kernel.Composition.MapComap
ProbabilityTheory.Kernel.instIsMarkovKernelSectROfProd : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel (α × β) γ) (a : α) [ProbabilityTheory.IsMarkovKernel κ],
  ProbabilityTheory.IsMarkovKernel (κ.sectR a)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min!_eq_head!_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.min! = t.toList.head!
-- Mathlib.Order.UpperLower.Principal
/-- Principal upper set. `Set.Ici` as an upper set. The smallest upper set containing a given
element.  -/
UpperSet.Ici : {α : Type u_1} → [inst : Preorder α] → α → UpperSet α