mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Complex.Liouville
/-- **Liouville's theorem**: a complex differentiable bounded function is a constant.  -/
Differentiable.exists_eq_const_of_bounded : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {F : Type v} [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℂ F] {f : E → F},
  Differentiable ℂ f → Bornology.IsBounded (Set.range f) → ∃ c, f = Function.const E c
-- Mathlib.Algebra.Order.Hom.Ring
OrderRingIso.toRingEquiv : {α : Type u_6} →
  {β : Type u_7} →
    [inst : Mul α] →
      [inst_1 : Add α] → [inst_2 : Mul β] → [inst_3 : Add β] → [inst_4 : LE α] → [inst_5 : LE β] → α ≃+*o β → α ≃+* β
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.coe_mul : ∀ (z w : Complex.UnitDisc), ↑(z * w) = ↑z * ↑w
-- Mathlib.Data.QPF.Univariate.Basic
/-- destructor of a type defined by a qpf  -/
QPF.Fix.dest : {F : Type u → Type u} → [q : QPF F] → QPF.Fix F → F (QPF.Fix F)
-- Mathlib.GroupTheory.OrderOfElement
smul_eq_of_smul_le : ∀ {G : Type u_6} [inst : Group G] [Finite G] {α : Type u_7} [inst_2 : PartialOrder α] {g : G} {a : α}
  [inst_3 : MulAction G α] [CovariantClass G α HSMul.hSMul LE.le], g • a ≤ a → g • a = a
-- Mathlib.RepresentationTheory.Submodule
Representation.mem_invtSubmodule : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) {p : Submodule k V},
  p ∈ ρ.invtSubmodule ↔ ∀ (g : G), p ∈ Module.End.invtSubmodule (ρ g)
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.transvection.congr_simp : ∀ {n : Type u_1} {R : Type u₂} {inst : DecidableEq n} [inst_1 : DecidableEq n] [inst_2 : CommRing R] (i i_1 : n),
  i = i_1 →
    ∀ (j j_1 : n),
      j = j_1 →
        ∀ (c c_1 : R),
          c = c_1 →
            ∀ (a a_1 : n),
              a = a_1 →
                ∀ (a_2 a_3 : n), a_2 = a_3 → Matrix.transvection i j c a a_2 = Matrix.transvection i_1 j_1 c_1 a_1 a_3
-- Mathlib.NumberTheory.LSeries.PrimesInAP
_private.Mathlib.NumberTheory.LSeries.PrimesInAP.0.ArithmeticFunction.vonMangoldt.F'.eq_1 : ∀ (pk : Nat.Primes × ℕ), ArithmeticFunction.vonMangoldt.F'✝ pk = ArithmeticFunction.vonMangoldt.F₀✝ (↑pk.1 ^ (pk.2 + 1))
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.concat_ne_nil : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) (h : G.Adj v u), p.concat h ≠ SimpleGraph.Walk.nil
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearEquiv.congrQuadraticMap_apply : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : AddCommMonoid P]
  [inst_6 : Module R P] (e : N ≃ₗ[R] P) (Q : QuadraticMap R M N), e.congrQuadraticMap Q = (↑e).compQuadraticMap Q
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
/-- Isomorphic presheaves have isomorphic `piInters` for any cover `U`.  -/
TopCat.Presheaf.SheafConditionEqualizerProducts.piInters.isoOfIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasProducts C] →
      {X : TopCat} →
        {F : TopCat.Presheaf C X} →
          {ι : Type v'} →
            (U : ι → TopologicalSpace.Opens ↑X) →
              {G : TopCat.Presheaf C X} →
                (F ≅ G) →
                  (TopCat.Presheaf.SheafConditionEqualizerProducts.piInters F U ≅
                    TopCat.Presheaf.SheafConditionEqualizerProducts.piInters G U)
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.SimpleHandler.toHandler : Lean.Linter.MissingDocs.SimpleHandler → Lean.Linter.MissingDocs.Handler
-- Mathlib.Tactic.NormNum.NatSqrt
/-- Given the natural number literal `ex`, returns its square root as a natural number literal
and an equality proof. Panics if `ex` isn't a natural number literal.  -/
Mathlib.Meta.NormNum.proveNatSqrt : (ex : Q(ℕ)) → (ey : Q(ℕ)) × Q(«$ex».sqrt = «$ey»)
-- Mathlib.Order.Filter.Pointwise
Filter.isAddUnit_pure : ∀ {α : Type u_2} [inst : AddGroup α] (a : α), IsAddUnit (pure a)
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
VectorPrebundle.IsContMDiff.mk : ∀ {𝕜 : Type u_1} {B : Type u_2} {F : Type u_4} {E : B → Type u_6} [inst : NontriviallyNormedField 𝕜] {EB : Type u_7}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_3 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B]
  [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)] [inst_8 : NormedAddCommGroup F]
  [inst_9 : NormedSpace 𝕜 F] [inst_10 : (x : B) → TopologicalSpace (E x)] {a : VectorPrebundle 𝕜 F E} {n : WithTop ℕ∞},
  (∀ e ∈ a.pretrivializationAtlas,
      ∀ e' ∈ a.pretrivializationAtlas,
        ∃ f,
          ContMDiffOn IB (modelWithCornersSelf 𝕜 (F →L[𝕜] F)) n f (e.baseSet ∩ e'.baseSet) ∧
            ∀ b ∈ e.baseSet ∩ e'.baseSet, ∀ (v : F), (f b) v = (↑e' ⟨b, e.symm b v⟩).2) →
    VectorPrebundle.IsContMDiff IB a n
-- Batteries.Control.LawfulMonadState
liftM_set : ∀ {σ : Type u_1} {m : Type u_1 → Type u_2} {n : Type u_1 → Type u_3} [inst : MonadStateOf σ m] [inst_1 : MonadLift m n]
  (s : σ), liftM (set s) = set s
-- Lean.Server.Requests
Lean.Server.RequestError.fileChanged : Lean.Server.RequestError
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.isometry_vertical_line : ∀ (a : ℝ), Isometry fun y => { coe := { re := a, im := Real.exp y }, coe_im_pos := ⋯ }
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.toEquiv_injective : ∀ {R : Type u_1} {S : Type u_6} {M : Type u_7} {M₂ : Type u_9} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] {modM : Module R M} {modM₂ : Module S M₂} {σ : R →+* S}
  {σ' : S →+* R} [inst_4 : RingHomInvPair σ σ'] [inst_5 : RingHomInvPair σ' σ], Function.Injective LinearEquiv.toEquiv
-- Lean.Data.Lsp.Basic
Lean.Lsp.ResolveSupport.properties : Lean.Lsp.ResolveSupport → Array String
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.supDegree_sum_lt : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {D : A → B} {ι : Type u_7} {s : Finset ι} {f : ι → AddMonoidAlgebra R A},
  s.Nonempty →
    ∀ {b : B}, (∀ i ∈ s, AddMonoidAlgebra.supDegree D (f i) < b) → AddMonoidAlgebra.supDegree D (∑ i ∈ s, f i) < b
-- Mathlib.Topology.MetricSpace.Gluing
Metric.toGlueL_isometry : ∀ {X : Type u} {Y : Type v} {Z : Type w} [inst : Nonempty Z] [inst_1 : MetricSpace Z] [inst_2 : MetricSpace X]
  [inst_3 : MetricSpace Y] {Φ : Z → X} {Ψ : Z → Y} (hΦ : Isometry Φ) (hΨ : Isometry Ψ), Isometry (Metric.toGlueL hΦ hΨ)
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.support_erase : ∀ {R : Type u_1} [inst : Semiring R] {p : SkewPolynomial R} (n : ℕ),
  (SkewPolynomial.erase n p).support = p.support.erase n
-- Init.Data.AC
Lean.Data.AC.Context.var : {α : Sort u_1} → (ctx : Lean.Data.AC.Context α) → ℕ → Lean.Data.AC.Variable ctx.op
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernel_map_comp_cokernelComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f : X ⟶ Y) {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D)
  [inst_4 : G.PreservesZeroMorphisms] {X' Y' : C} [inst_5 : CategoryTheory.Limits.HasCokernel f]
  [inst_6 : CategoryTheory.Limits.HasCokernel (G.map f)] (g : X' ⟶ Y') [inst_7 : CategoryTheory.Limits.HasCokernel g]
  [inst_8 : CategoryTheory.Limits.HasCokernel (G.map g)] (p : X ⟶ X') (q : Y ⟶ Y')
  (hpq : CategoryTheory.CategoryStruct.comp f q = CategoryTheory.CategoryStruct.comp p g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯)
      (CategoryTheory.Limits.cokernelComparison g G) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.cokernelComparison f G)
      (G.map (CategoryTheory.Limits.cokernel.map f g p q hpq))
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Defs
Matrix.SpecialLinearGroup.coe_GLPos_neg : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R] [inst_5 : Fact (Even (Fintype.card n))] (g : Matrix.SpecialLinearGroup n R),
  Matrix.SpecialLinearGroup.toGLPos (-g) = -Matrix.SpecialLinearGroup.toGLPos g
-- Mathlib.Analysis.Normed.Group.Basic
enorm_div_rev : ∀ {E : Type u_8} [inst : SeminormedGroup E] (a b : E), ‖a / b‖ₑ = ‖b / a‖ₑ
-- Mathlib.RingTheory.Noetherian.Defs
IsNoetherian.mk : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  (∀ (s : Submodule R M), s.FG) → IsNoetherian R M
-- Batteries.Recycling.MonadSatisfying.Array
_private.Batteries.Recycling.MonadSatisfying.Array.0.Array.forIn'.loop.match_3.eq_1 : ∀ {α : Type u_1} (as : Array α) (motive : (i : ℕ) → i ≤ as.size → Sort u_2) (x : 0 ≤ as.size)
  (h_1 : (x : 0 ≤ as.size) → motive 0 x) (h_2 : (i : ℕ) → (h : i + 1 ≤ as.size) → motive i.succ h),
  (match 0, x with
    | 0, x => h_1 x
    | i.succ, h => h_2 i h) =
    h_1 x
-- Init.Grind.AC
Lean.Grind.AC.eq_simp_lhs_ac : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {inst₁ : Std.Associative ctx.op} {inst₂ : Std.Commutative ctx.op}
  (c lhs₁ rhs₁ lhs₂ rhs₂ lhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_ac_cert c lhs₁ rhs₁ lhs₂ lhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ = Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂' = Lean.Grind.AC.Seq.denote ctx rhs₂
-- Mathlib.Order.Lattice
MonotoneOn.map_sup : ∀ {α : Type u} {β : Type v} {f : α → β} {s : Set α} {x y : α} [inst : LinearOrder α] [inst_1 : SemilatticeSup β],
  MonotoneOn f s → x ∈ s → y ∈ s → f (max x y) = f x ⊔ f y
-- Init.Data.SInt.Lemmas
Int16.neg_ofNat : ∀ {n : ℕ}, -Int16.ofNat n = Int16.ofInt (-↑n)
-- Std.Sat.AIG.If
Std.Sat.AIG.RefVec.ite.go_denote_mem_prefix : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {inv : Bool} {w : ℕ} (aig : Std.Sat.AIG α)
  (curr : ℕ) (hcurr : curr ≤ w) (discr : aig.Ref) (lhs rhs : aig.RefVec w) (s : aig.RefVec curr) (start : ℕ)
  (hstart : start < aig.decls.size),
  ⟦assign,
      { aig := (Std.Sat.AIG.RefVec.ite.go aig curr hcurr discr lhs rhs s).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.neg : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [Neg α] → Neg (Matrix m n α)
-- Init.Data.Vector.Range
Vector.range_succ : ∀ {n : ℕ}, Vector.range n.succ = Vector.range n ++ #v[n]
-- Mathlib.CategoryTheory.Limits.Types.Products
/-- The product type `X × Y` forms a cone for the binary product of `X` and `Y`.  -/
CategoryTheory.Limits.Types.binaryProductCone : (X Y : Type u) → CategoryTheory.Limits.BinaryFan X Y
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Completion
/-- Given a normed group hom `V ⟶ W`, this defines the associated morphism
from the completion of `V` to the completion of `W`.
The difference from the definition obtained from the functoriality of completion is in that the
map sending a morphism `f` to the associated morphism of completions is itself additive.  -/
SemiNormedGrp.completion.mapHom : (V W : SemiNormedGrp) → (V ⟶ W) →+ (SemiNormedGrp.completion.obj V ⟶ SemiNormedGrp.completion.obj W)
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- The Coxeter matrix of type F₄.

The corresponding Coxeter-Dynkin diagram is:
```
             4
    o --- o --- o --- o
```
 -/
CoxeterMatrix.F₄ : CoxeterMatrix (Fin 4)
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_toUSize : ∀ (n : UInt16), n.toUSize.toBitVec = BitVec.setWidth System.Platform.numBits n.toBitVec
-- Mathlib.Analysis.Convex.Basic
convex_empty : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E], Convex 𝕜 ∅
-- Mathlib.Algebra.Group.Subgroup.Finite
Fintype.card_coeSort_mrange : ∀ {M : Type u_4} {N : Type u_5} [inst : Monoid M] [inst_1 : Monoid N] [inst_2 : Fintype M] [inst_3 : DecidableEq N]
  {f : M →* N}, Function.Injective ⇑f → Fintype.card ↥(MonoidHom.mrange f) = Fintype.card M
-- Mathlib.InformationTheory.Hamming
Hamming.instNormOfZero : {ι : Type u_2} →
  {β : ι → Type u_3} → [Fintype ι] → [(i : ι) → DecidableEq (β i)] → [(i : ι) → Zero (β i)] → Norm (Hamming β)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueD_filter_not_contains_map_fst : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l₁ l₂ : List ((_ : α) × β)} {k : α} {fallback : β},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getValueD k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback =
      if Std.Internal.List.containsKey k l₂ = true then fallback else Std.Internal.List.getValueD k l₁ fallback
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.findD : {α : Type u_1} → {β : Type u_2} → {x : BEq α} → {x_1 : Hashable α} → Lean.PersistentHashMap α β → α → β → β
-- Mathlib.Analysis.Normed.Lp.lpSpace
Memℓp.mono : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f : (i : α) → E i}
  {g : α → ℝ}, Memℓp g p → (∀ (i : α), ‖f i‖ ≤ g i) → Memℓp f p
-- Mathlib.FieldTheory.Finite.Basic
ZMod.orderOf_dvd_card_sub_one : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {a : ZMod p}, a ≠ 0 → orderOf a ∣ p - 1
-- Batteries.Recycling.RBTree.Basic
/-- `O(n log n)`. Build a tree from an unsorted list by inserting them one at a time.  -/
RBTree.RBMap.ofList : {α : Type u} → {β : Type v} → List (α × β) → (cmp : α → α → Ordering) → RBTree.RBMap α β cmp
-- Init.Data.Array.Lemmas
Array.back?_pop : ∀ {α : Type u_1} {xs : Array α}, xs.pop.back? = if xs.size ≤ 1 then none else xs[xs.size - 2]?
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.prod_mono : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  ⦃s₁ s₂ : NonUnitalSubsemiring R⦄, s₁ ≤ s₂ → ∀ ⦃t₁ t₂ : NonUnitalSubsemiring S⦄, t₁ ≤ t₂ → s₁.prod t₁ ≤ s₂.prod t₂
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_non_aestronglyMeasurable : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ},
  ¬MeasureTheory.AEStronglyMeasurable f (μ.restrict (Set.uIoc a b)) → ∫ (x : ℝ) in a..b, f x ∂μ = 0
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instIsUniformGroup : ∀ {G : Type u_1} [inst : Group G] [inst_1 : UniformSpace G] [inst_2 : IsUniformGroup G],
  IsUniformGroup (SeparationQuotient G)
-- Mathlib.Topology.Maps.Strict.Basic
/-- **Alias** of `IsOpenMap.isStrictMap`.

---

A open continuous map is a strict map.  -/
Topology.IsOpenMap.isStrictMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsOpenMap f → Continuous f → Topology.IsStrictMap f
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.edges_cycleBypass_sublist_edges : ∀ {V : Type u} {G : SimpleGraph V} {v : V} [inst : DecidableEq V] (w : G.Walk v v), w.cycleBypass.edges.Sublist w.edges
-- Init.System.ST
ST.Prim.Ref.set : {σ α : Type} → ST.Ref σ α → α → ST σ Unit
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.eventually_ne_atTop : ∀ {α : Type u_3} [inst : Preorder α] [NoTopOrder α] (a : α), ∀ᶠ (x : α) in Filter.atTop, x ≠ a
-- Init.Data.Iterators.Basic
Std.IterStep.skip.inj : ∀ {α : Sort u_1} {β : Sort u_2} {it it_1 : α}, Std.IterStep.skip it = Std.IterStep.skip it_1 → it = it_1
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.or : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p q : α → Prop},
  Measurable p → Measurable q → Measurable fun a => p a ∨ q a
-- Init.Data.Nat.Dvd
Nat.mod_mod_of_dvd : ∀ {c b : ℕ} (a : ℕ), c ∣ b → a % b % c = a % c
-- Init.System.ST
EST.tryCatch : {ε σ α : Type} → EST ε σ α → (ε → EST ε σ α) → EST ε σ α
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the reverse direction of `monovary_inv₀`. -/
Monovary.inv₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [inst_3 : Semifield β] [inst_4 : LinearOrder β] [IsStrictOrderedRing β] {f : ι → α} {g : ι → β},
  StrongLT 0 f → StrongLT 0 g → Monovary f g → Monovary f⁻¹ g⁻¹
-- Mathlib.Algebra.WithConv
WithConv.ofConv_bijective : ∀ {A : Type u_2}, Function.Bijective WithConv.ofConv
-- Mathlib.Geometry.Convex.Cone.Pointed
PointedCone.ext : ∀ {R : Type u_1} {E : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : Module R E] {C₁ C₂ : PointedCone R E}, (∀ (x : E), x ∈ C₁ ↔ x ∈ C₂) → C₁ = C₂
-- Init.Data.String.Basic
String.Slice.Pos.sliceTo_ofSliceTo : ∀ {s : String.Slice} {p₀ : s.Pos} {p : (s.sliceTo p₀).Pos}, p₀.sliceTo (String.Slice.Pos.ofSliceTo p) ⋯ = p
-- Init.Data.Range.Polymorphic.PRange
Std.instDecidableEqRoo : {α : Type u_1} → [DecidableEq α] → DecidableEq (Std.Roo α)
-- Lean.Elab.PreDefinition.PartialFixpoint.Eqns
Lean.Elab.PartialFixpoint.EqnInfo.type : Lean.Elab.PartialFixpoint.EqnInfo → Lean.Expr
-- Mathlib.Analysis.Analytic.Composition
FormalMultilinearSeries.compContinuousLinearMap_applyComposition : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} [inst : CommRing 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : AddCommGroup G] [inst_4 : Module 𝕜 E] [inst_5 : Module 𝕜 F] [inst_6 : Module 𝕜 G]
  [inst_7 : TopologicalSpace E] [inst_8 : TopologicalSpace F] [inst_9 : TopologicalSpace G]
  [inst_10 : IsTopologicalAddGroup E] [inst_11 : ContinuousConstSMul 𝕜 E] [inst_12 : IsTopologicalAddGroup F]
  [inst_13 : ContinuousConstSMul 𝕜 F] [inst_14 : IsTopologicalAddGroup G] [inst_15 : ContinuousConstSMul 𝕜 G] {n : ℕ}
  (p : FormalMultilinearSeries 𝕜 F G) (f : E →L[𝕜] F) (c : Composition n) (v : Fin n → E),
  (p.compContinuousLinearMap f).applyComposition c v = p.applyComposition c (⇑f ∘ v)
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.ext_iff : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {X : CategoryTheory.SimplicialObject.Augmented C}
  {x y : X.ExtraDegeneracy}, x = y ↔ x.s' = y.s' ∧ x.s = y.s
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.list_prod_mem : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S : Subalgebra R A)
  {L : List A}, (∀ x ∈ L, x ∈ S) → L.prod ∈ S
-- Mathlib.Order.Hom.Lex
/-- `Equiv.prodCongr` promoted to an order isomorphism between lexicographic products.  -/
Prod.Lex.prodLexCongr : {α : Type u_4} →
  {β : Type u_5} →
    {γ : Type u_6} →
      {δ : Type u_7} →
        [inst : Preorder α] →
          [inst_1 : Preorder β] →
            [inst_2 : Preorder γ] → [inst_3 : Preorder δ] → α ≃o β → γ ≃o δ → Lex (α × γ) ≃o Lex (β × δ)
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
/-- Let `x` be a submonoid of `A`, then `NumDenSameDeg 𝒜 x` is a structure with a numerator and a
denominator with same grading such that the denominator is contained in `x`.
 -/
HomogeneousLocalization.NumDenSameDeg : {ι : Type u_1} →
  {A : Type u_2} → {σ : Type u_3} → [inst : CommRing A] → [SetLike σ A] → (ι → σ) → Submonoid A → Type (max u_1 u_2)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Cokleisli.Adjunction.toCokleisli_obj_of : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (U : CategoryTheory.Comonad C) (X : C),
  ((CategoryTheory.Cokleisli.Adjunction.toCokleisli U).obj X).of = X
-- Mathlib.CategoryTheory.Bicategory.Kan.Adjunction
/-- An absolute left Kan extension of the identity along `f` is a right adjoint to `f`.
The unit of this adjunction is given by the unit of the Kan extension.  -/
CategoryTheory.Bicategory.LeftExtension.IsAbsKan.adjunction : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b : B} →
      {f : a ⟶ b} →
        (t : CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.id a)) →
          t.IsAbsKan → CategoryTheory.Bicategory.Adjunction f t.extension
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.exact : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp},
  Std.ExtDTreeMap.mk t₁ = Std.ExtDTreeMap.mk t₂ → t₁.Equiv t₂
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffAt_finprod : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : CommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffMul I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x₀ : M} {f : ι → M → G},
  (LocallyFinite fun i => Function.mulSupport (f i)) →
    (∀ (i : ι), ContMDiffAt I' I n (f i) x₀) → ContMDiffAt I' I n (fun x => ∏ᶠ (i : ι), f i x) x₀
-- Init.Data.Int.Lemmas
Int.instCommutativeHAdd : Std.Commutative fun x1 x2 => x1 + x2
-- Mathlib.Topology.MetricSpace.Pseudo.Pi
/-- A closed ball in a product space is a product of closed balls. See also `closedBall_pi'`
for a version assuming `Nonempty β` instead of `0 ≤ r`.  -/
closedBall_pi : ∀ {β : Type u_2} {X : β → Type u_3} [inst : Fintype β] [inst_1 : (b : β) → PseudoMetricSpace (X b)] (x : (b : β) → X b)
  {r : ℝ}, 0 ≤ r → Metric.closedBall x r = Set.univ.pi fun b => Metric.closedBall (x b) r
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- SubAddAction on the complement of an invariant subset  -/
SubAddAction.instCompl : {R : Type u} → {M : Type v} → [inst : AddGroup R] → [inst_1 : AddAction R M] → Compl (SubAddAction R M)
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- The natural equivalence between `PiLp p β` and `β default`,
for any index type `ι` with a unique element.  -/
PiLp.equivOfUnique : (p : ENNReal) →
  (𝕜 : Type u_1) →
    {ι : Type u_2} →
      (β : ι → Type u_4) →
        [inst : Semiring 𝕜] →
          [inst_1 : (i : ι) → AddCommGroup (β i)] →
            [inst_2 : (i : ι) → Module 𝕜 (β i)] →
              [inst_3 : (i : ι) → TopologicalSpace (β i)] → [inst_4 : Unique ι] → PiLp p β ≃L[𝕜] β default
-- Std.Sat.AIG.CachedGates
/-- Create an xor gate in the input AIG. This uses the builtin cache to enable automated subterm
sharing.
 -/
Std.Sat.AIG.mkXorCached : {α : Type} →
  [inst : Hashable α] → [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α
-- Mathlib.Logic.IsEmpty.Defs
IsEmpty.forall_iff : ∀ {α : Sort u} [IsEmpty α] {p : α → Prop}, (∀ (a : α), p a) ↔ True
-- Lean.Elab.InfoTree.Types
Lean.Elab.CommandContextInfo.openDecls : Lean.Elab.CommandContextInfo → List Lean.OpenDecl
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.nontrivial_dual_iff : ∀ (K : Type uK) {V : Type uV} [inst : CommSemiring K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [Module.Projective K V], Nontrivial (Module.Dual K V) ↔ Nontrivial V
-- Mathlib.Topology.MetricSpace.Gluing
Metric.Sum.dist_eq : ∀ {X : Type u} {Y : Type v} [inst : MetricSpace X] [inst_1 : MetricSpace Y] {x y : X ⊕ Y},
  dist x y = Metric.Sum.dist x y
-- Mathlib.Algebra.Order.Group.Synonym
toLex_eq_zero : ∀ {α : Type u_1} [inst : Zero α] {a : α}, toLex a = 0 ↔ a = 0
-- Mathlib.Algebra.Group.Defs
/-- Addition is commutative in a commutative additive magma.  -/
AddCommMonoid.add_comm : ∀ {M : Type u} [self : AddCommMonoid M] (a b : M), a + b = b + a
-- Mathlib.Probability.Kernel.Composition.CompNotation
MeasureTheory.Measure.id_comp : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}, μ.bind ⇑ProbabilityTheory.Kernel.id = μ
-- Mathlib.Topology.Category.TopCat.Basic
/-- The type of morphisms in `TopCat`.  -/
TopCat.Hom : TopCat → TopCat → Type u