mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.Equiv.rfl : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp}, t.Equiv t
-- Mathlib.Algebra.Order.Monoid.Submonoid
/-- A submonoid of an ordered cancellative monoid is an ordered cancellative monoid.  -/
Submonoid.toIsOrderedCancelMonoid : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] (S : Submonoid M),
  IsOrderedCancelMonoid ↥S
-- Mathlib.Combinatorics.Graph.Basic
/-- If some edge `e` is incident to `x`, then `x ∈ V`.  -/
Graph.left_mem_of_isLink : ∀ {α : Type u_3} {β : Type u_4} (self : Graph α β) ⦃e : β⦄ ⦃x y : α⦄, self.IsLink e x y → x ∈ self.vertexSet
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instMulOneClass.eq_1 : ∀ {α : Type u_1} [inst : MulOneClass α],
  Colex.instMulOneClass = { toOne := Colex.instOne, toMul := Colex.instMul, one_mul := ⋯, mul_one := ⋯ }
-- Lean.LocalContext
Lean.LocalContext.foldl : {β : Type u_1} → Lean.LocalContext → (β → Lean.LocalDecl → β) → β → optParam ℕ 0 → β
-- Mathlib.Order.RelClasses
/-- **Alias** of `ssubset_iff_subset_not_superset`.

---

Set notation form of `lt_iff_le_not_ge` -/
ssubset_iff_subset_not_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b : α}, a ⊂ b ↔ a ⊆ b ∧ ¬b ⊆ a
-- Mathlib.RingTheory.Extension.Basic
Algebra.Extension.Cotangent.ker_mk : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Extension R S), Algebra.Extension.Cotangent.mk.ker = P.ker • ⊤
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop.0.Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastCpopTree : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {assign : α → Bool} (aig : Std.Sat.AIG α) (len : ℕ)
  (l : aig.RefVec (len * w)) (h : 0 < len) (bv : BitVec (len * w)),
  (∀ (idx : ℕ) (hidx : idx < len * w), ⟦assign, { aig := aig, ref := l.get idx hidx }⟧ = bv.getLsbD idx) →
    ∀ (idx : ℕ) (hidx : idx < w),
      ⟦assign,
          { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree aig { len := len, x := l, h := h }).aig,
            ref :=
              (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree aig { len := len, x := l, h := h }).vec.get idx
                hidx }⟧ =
        bv.cpopTree.getLsbD idx
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.piEquiv_apply : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} [inst : Semiring R] [inst_1 : (i : ι) → AddCommMonoid (M₁ i)]
  [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : (i : ι) → TopologicalSpace (M₁ i)] {ι' : Type u_1} {M' : ι' → Type u_2}
  [inst_4 : (i : ι') → AddCommMonoid (M' i)] [inst_5 : (i : ι') → TopologicalSpace (M' i)]
  [inst_6 : (i : ι') → Module R (M' i)] (f : (i : ι') → ContinuousMultilinearMap R M₁ (M' i)),
  ContinuousMultilinearMap.piEquiv f = ContinuousMultilinearMap.pi f
-- Mathlib.Analysis.Convex.Deriv
ConcaveOn.antitoneOn_slope_gt : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜} {x : 𝕜},
  ConcaveOn 𝕜 s f → x ∈ s → AntitoneOn (slope f x) {y | y ∈ s ∧ x < y}
-- Mathlib.Combinatorics.SimpleGraph.Maps
/-- Given an injective function, there is an embedding from a graph into the mapped graph.  -/
SimpleGraph.Embedding.map : {V : Type u_1} → {W : Type u_2} → (f : V ↪ W) → (G : SimpleGraph V) → G ↪g SimpleGraph.map (⇑f) G
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.skeletalFunctor.coe_map : ∀ {Δ₁ Δ₂ : SimplexCategory} (f : Δ₁ ⟶ Δ₂),
  LinOrd.Hom.hom (SimplexCategory.skeletalFunctor.map f).hom = SimplexCategory.Hom.toOrderHom f
-- Mathlib.Computability.TuringMachine.Tape
_private.Mathlib.Computability.TuringMachine.Tape.0.Turing.Tape.move.match_1.eq_1 : ∀ {Γ : Type u_1} [inst : Inhabited Γ] (motive : Turing.Dir → Turing.Tape Γ → Sort u_2) (a : Γ)
  (L R : Turing.ListBlank Γ)
  (h_1 : (a : Γ) → (L R : Turing.ListBlank Γ) → motive Turing.Dir.left { head := a, left := L, right := R })
  (h_2 : (a : Γ) → (L R : Turing.ListBlank Γ) → motive Turing.Dir.right { head := a, left := L, right := R }),
  (match Turing.Dir.left, { head := a, left := L, right := R } with
    | Turing.Dir.left, { head := a, left := L, right := R } => h_1 a L R
    | Turing.Dir.right, { head := a, left := L, right := R } => h_2 a L R) =
    h_1 a L R
-- Mathlib.CategoryTheory.Monoidal.Preadditive
CategoryTheory.rightDistributor_inv_comp_biproduct_π : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalPreadditive C]
  [inst_4 : CategoryTheory.Limits.HasFiniteBiproducts C] {J : Type} [inst_5 : Finite J] (f : J → C) (X : C) (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.rightDistributor f X).inv
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Limits.biproduct.π f j) X) =
    CategoryTheory.Limits.biproduct.π (fun j => CategoryTheory.MonoidalCategoryStruct.tensorObj (f j) X) j
-- Init.Data.Fin.Basic
Fin.instMul : {n : ℕ} → Mul (Fin n)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.quotientBot_apply : ∀ {G : Type u} [inst : Group G] (a : G ⧸ (MonoidHom.id G).ker),
  QuotientGroup.quotientBot a = (QuotientGroup.kerLift (MonoidHom.id G)) a
-- Mathlib.Data.Finset.Image
Equiv.finsetCongr_apply : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Finset α), e.finsetCongr s = Finset.map e.toEmbedding s
-- Batteries.Data.PairingHeap
Batteries.PairingHeapImp.Heap.size.eq_2 : ∀ {α : Type u_1} (a : α) (c s : Batteries.PairingHeapImp.Heap α),
  (Batteries.PairingHeapImp.Heap.node a c s).size = c.size + 1 + s.size
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKeyD_alter_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] [Inhabited α],
  t.WF →
    ∀ {k fallback : α} {f : Option (β k) → Option (β k)},
      (t.alter k f).getKeyD k fallback = if (f (t.get? k)).isSome = true then k else fallback
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.below.wf : ∀ {α : Type u} [inst : Ord α] {motive : {β : α → Type v} → (a : Std.DTreeMap.Internal.Impl α β) → a.WF → Prop}
  {x : α → Type v} {t : Std.DTreeMap.Internal.Impl α x} (a : t.Balanced) (a_1 : ∀ [Std.TransOrd α], t.Ordered),
  Std.DTreeMap.Internal.Impl.WF.below ⋯
-- Mathlib.Algebra.Order.Module.Pointwise
smul_lowerBounds_subset_lowerBounds_smul_of_nonneg : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero α]
  [PosSMulMono α β] {a : α} {s : Set β}, 0 ≤ a → a • lowerBounds s ⊆ lowerBounds (a • s)
-- Mathlib.Probability.Kernel.Composition.CompProd
ProbabilityTheory.Kernel.setLIntegral_compProd : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} (κ : ProbabilityTheory.Kernel α β) [ProbabilityTheory.IsSFiniteKernel κ]
  (η : ProbabilityTheory.Kernel (α × β) γ) [ProbabilityTheory.IsSFiniteKernel η] (a : α) {f : β × γ → ENNReal},
  Measurable f →
    ∀ {s : Set β} {t : Set γ},
      MeasurableSet s →
        MeasurableSet t →
          ∫⁻ (z : β × γ) in s ×ˢ t, f z ∂(κ.compProd η) a = ∫⁻ (x : β) in s, ∫⁻ (y : γ) in t, f (x, y) ∂η (a, x) ∂κ a
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.keys_perm : ∀ {α : Type u} {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β}, m₁.Equiv m₂ → m₁.keys.Perm m₂.keys
-- Mathlib.RingTheory.Coprime.Basic
IsRelPrime.neg_neg_iff : ∀ {R : Type u_1} [inst : CommRing R] (x y : R), IsRelPrime (-x) (-y) ↔ IsRelPrime x y
-- Init.Data.Array.MapIdx
Array.mapFinIdx_ne_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β}, xs.mapFinIdx f ≠ #[] ↔ xs ≠ #[]
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
MeasureTheory.HaveLebesgueDecomposition.mconv : ∀ {G : Type u_3} [inst : Group G] {mG : MeasurableSpace G} [MeasurableMul₂ G] [MeasurableInv G]
  {μ : MeasureTheory.Measure G} [μ.IsMulLeftInvariant] [MeasureTheory.SFinite μ] {ν₁ ν₂ : MeasureTheory.Measure G}
  [ν₁.HaveLebesgueDecomposition μ] [ν₂.HaveLebesgueDecomposition μ],
  ν₁.AbsolutelyContinuous μ → ν₂.AbsolutelyContinuous μ → (ν₁.mconv ν₂).HaveLebesgueDecomposition μ
-- Mathlib.Topology.Bornology.Real
NNReal.instOrderTopology : OrderTopology NNReal
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso_inv_app : ∀ {X Y : SSet.Truncated 2}
  (x : X.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 }))
  (y : Y.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Edge.tensor._proof_1 })),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.functorCompInverseIso X Y).inv.app
      (SSet.Truncated.HomotopyCategory.mk (x, y)) =
    CategoryTheory.CategoryStruct.id
      ((CategoryTheory.Functor.id (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y).HomotopyCategory).obj
        (SSet.Truncated.HomotopyCategory.mk (x, y)))
-- Mathlib.NumberTheory.LegendreSymbol.QuadraticChar.Basic
/-- The quadratic character is multiplicative.  -/
quadraticCharFun_mul : ∀ {F : Type u_1} [inst : Field F] [inst_1 : Fintype F] [inst_2 : DecidableEq F] (a b : F),
  quadraticCharFun F (a * b) = quadraticCharFun F a * quadraticCharFun F b
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.inf_toSubmodule : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S T : Subalgebra R A),
  Subalgebra.toSubmodule (S ⊓ T) = Subalgebra.toSubmodule S ⊓ Subalgebra.toSubmodule T
-- Mathlib.GroupTheory.GroupAction.Primitive
AddAction.IsPreprimitive.of_subsingleton : ∀ {G : Type u_1} {X : Type u_2} [inst : VAdd G X] [Nonempty G] [Subsingleton X], AddAction.IsPreprimitive G X
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_trans : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b c : E} {ω : E → E →L[𝕜] F}
  {γab : Path a b} {γbc : Path b c},
  CurveIntegrable ω γab →
    CurveIntegrable ω γbc → ∫ᶜ (x : E) in γab.trans γbc, ω x = ∫ᶜ (x : E) in γab, ω x + ∫ᶜ (x : E) in γbc, ω x
-- Mathlib.CategoryTheory.Types.Basic
/-- **Alias** of `Equiv.toIso_inv_hom_apply`. -/
Equiv.toIso_inv : ∀ {X Y : Type u} (e : X ≃ Y) (x : Y), (CategoryTheory.ConcreteCategory.hom e.toIso.inv) x = e.symm x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_filterMap! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  [inst : Std.TransOrd α] [inst_1 : Inhabited γ] {f : α → β → Option γ} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.filterMap! f t) k =
    ((Std.DTreeMap.Internal.Impl.Const.get? t k).pbind fun x h' => f (t.getKey k ⋯) x).get!
-- Init.Data.Int.Order
Int.neg_of_mul_pos_right : ∀ {a b : ℤ}, 0 < a * b → a < 0 → b < 0
-- Batteries.Recycling.RBTree.Basic
/-- `O(log n)`. Find the value corresponding to key `k`, or return `v₀` if it is not in the map.  -/
RBTree.RBMap.findD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → α → β → β
-- Mathlib.Algebra.Homology.AlternatingConst
ComplexShape.down_nat_odd_add : ∀ {i j : ℕ}, (ComplexShape.down ℕ).Rel i j → Odd (i + j)
-- Mathlib.LinearAlgebra.FreeModule.Finite.Quotient
/-- We can write the quotient by a submodule of full rank over a PID as a product of quotients
by principal ideals.
 -/
Submodule.quotientEquivPiSpan : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : IsDomain R] →
              [inst_4 : IsPrincipalIdealRing R] →
                [inst_5 : Finite ι] →
                  (N : Submodule R M) →
                    (b : Module.Basis ι R M) →
                      (h : Module.finrank R ↥N = Module.finrank R M) →
                        (M ⧸ N) ≃ₗ[R] (i : ι) → R ⧸ Ideal.span {Submodule.smithNormalFormCoeffs b h i}
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
/-- One can reformulate smoothness on a set as continuity on this set, and smoothness in any
extended chart.  -/
mdifferentiableOn_iff : ∀ {𝕜 : 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'} {s : Set M}
  [IsManifold I 1 M] [IsManifold I' 1 M'],
  MDiff[s] f ↔
    ContinuousOn f s ∧
      ∀ (x : M) (y : M'),
        DifferentiableOn 𝕜 (↑(extChartAt I' y) ∘ f ∘ ↑(extChartAt I x).symm)
          ((extChartAt I x).target ∩ ↑(extChartAt I x).symm ⁻¹' (s ∩ f ⁻¹' (extChartAt I' y).source))
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.foldlM_eq_foldlM_toList : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Monad m] [LawfulMonad m] {f : δ → α → β → m δ} {init : δ},
  Std.TreeMap.foldlM f init t = List.foldlM (fun a b => f a b.1 b.2) init t.toList
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.SpaceResult.mk.sizeOf_spec : ∀ (foundLine foundFlattenedHardLine : Bool) (space : ℕ),
  sizeOf { foundLine := foundLine, foundFlattenedHardLine := foundFlattenedHardLine, space := space } =
    1 + sizeOf foundLine + sizeOf foundFlattenedHardLine + sizeOf space
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.zero_prod_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Zero β], 0 ×ˢ 0 = 0
-- Mathlib.Algebra.Group.Pointwise.Set.BigOperators
Set.image_multiset_prod : ∀ {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : FunLike F α β] [inst_1 : CommMonoid α] [inst_2 : CommMonoid β]
  [MonoidHomClass F α β] (f : F) (m : Multiset (Set α)), ⇑f '' m.prod = (Multiset.map (fun s => ⇑f '' s) m).prod
-- Lean.Data.Lsp.Basic
Lean.Lsp.MarkupContent.mk : Lean.Lsp.MarkupKind → String → Lean.Lsp.MarkupContent
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.op_tensorUnit : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C],
  Opposite.op (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) =
    CategoryTheory.MonoidalCategoryStruct.tensorUnit Cᵒᵖ
-- Init.Data.List.Lemmas
List.any_append : ∀ {α : Type u_1} {f : α → Bool} {xs ys : List α}, (xs ++ ys).any f = (xs.any f || ys.any f)
-- Batteries.Tactic.Lint.Simp
/-- A linter for simp lemmas whose lhs is not in simp-normal form, and which hence never fire.  -/
Batteries.Tactic.Lint.simpNF : Batteries.Tactic.Lint.Linter
-- Batteries.Data.List.Perm
List.subperm_cons_diff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a : α} {l₁ l₂ : List α}, ((a :: l₁).diff l₂).Subperm (a :: l₁.diff l₂)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
SSet.Truncated.instCategoryHomotopyCategory : (V : SSet.Truncated 2) → CategoryTheory.Category.{u_1, u_1} V.HomotopyCategory
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
IsDedekindDomain.FiniteAdeleRing.instIsTopologicalRing : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K], IsTopologicalRing (IsDedekindDomain.FiniteAdeleRing R K)
-- Mathlib.Order.Sublocale
Sublocale.mk.inj : ∀ {X : Type u_2} {inst : Order.Frame X} {carrier : Set X} {sInf_mem' : ∀ s ⊆ carrier, sInf s ∈ carrier}
  {himp_mem' : ∀ (a b : X), b ∈ carrier → a ⇨ b ∈ carrier} {carrier_1 : Set X}
  {sInf_mem'_1 : ∀ s ⊆ carrier_1, sInf s ∈ carrier_1} {himp_mem'_1 : ∀ (a b : X), b ∈ carrier_1 → a ⇨ b ∈ carrier_1},
  { carrier := carrier, sInf_mem' := sInf_mem', himp_mem' := himp_mem' } =
      { carrier := carrier_1, sInf_mem' := sInf_mem'_1, himp_mem' := himp_mem'_1 } →
    carrier = carrier_1
-- Mathlib.Condensed.Module
/-- The free condensed abelian group on a condensed set.  -/
Condensed.freeAb : CategoryTheory.Functor CondensedSet CondensedAb
-- Mathlib.GroupTheory.Congruence.BigOperators
AddCon.coe_finsetSum : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] (c : AddCon M) (s : Finset ι) (f : ι → M),
  ↑(s.sum f) = ∑ i ∈ s, ↑(f i)
-- Mathlib.Order.RelClasses
isTrans_gt : ∀ {α : Type u} [inst : Preorder α], IsTrans α fun a a_1 => a_1 < a
-- Mathlib.LinearAlgebra.Determinant
Algebra.det_lsmul : ∀ {R : Type u_5} {S : Type u_6} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] [Module.Free R S] (x : R),
  LinearMap.det ((Algebra.lsmul R R S) x) = x ^ Module.finrank R S
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.insertManyIfNewUnit_nil : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp}, t.insertManyIfNewUnit [] = t
-- Mathlib.Topology.Defs.Basic
/-- An open quotient map is an open map `f : X → Y` which is both an open map and a quotient map.
Equivalently, it is a surjective continuous open map.
We use the latter characterization as a definition.

Many important quotient maps are open quotient maps, including

- the quotient map from a topological space to its quotient by the action of a group;
- the quotient map from a topological group to its quotient by a normal subgroup;
- the quotient map from a topological space to its separation quotient.

Contrary to general quotient maps,
the category of open quotient maps is closed under `Prod.map`.
 -/
IsOpenQuotientMap : {X : Type u} → {Y : Type v} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.Rel.below.mul_right : ∀ {R : Type u} {X : Type v} [inst : CommRing R]
  {motive : (a a_1 : FreeNonUnitalNonAssocAlgebra R X) → FreeLieAlgebra.Rel R X a a_1 → Prop}
  {a b : FreeNonUnitalNonAssocAlgebra R X} (c : FreeNonUnitalNonAssocAlgebra R X) (a_1 : FreeLieAlgebra.Rel R X a b),
  FreeLieAlgebra.Rel.below a_1 → motive a b a_1 → FreeLieAlgebra.Rel.below ⋯
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {v : β k} {fallback : α},
      (t.insertIfNew k v).minKeyD fallback = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instInhabitedCompletionItemKind : Inhabited Lean.Lsp.CompletionItemKind
-- Lean.Elab.PreDefinition.Basic
Lean.Elab.PreDefinition.kind : Lean.Elab.PreDefinition → Lean.Elab.DefKind
-- Mathlib.Algebra.IsPrimePow
isPrimePow_nat_iff : ∀ (n : ℕ), IsPrimePow n ↔ ∃ p k, Nat.Prime p ∧ 0 < k ∧ p ^ k = n
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
Finset.aestronglyMeasurable_sum : ∀ {α : Type u_1} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {M : Type u_5} [inst : AddCommMonoid M]
  [inst_1 : TopologicalSpace M] [ContinuousAdd M] {ι : Type u_6} {f : ι → α → M} (s : Finset ι),
  (∀ i ∈ s, MeasureTheory.AEStronglyMeasurable (f i) μ) → MeasureTheory.AEStronglyMeasurable (∑ i ∈ s, f i) μ
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go.eq_def : ∀ {α : Type u} {β : Type v} [inst : Ord α] (k : α) (best : Option (α × β))
  (a : Std.DTreeMap.Internal.Impl α fun x => β),
  Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go k best a =
    match a with
    | Std.DTreeMap.Internal.Impl.leaf => best
    | Std.DTreeMap.Internal.Impl.inner size ky y l r =>
      match compare k ky with
      | Ordering.lt => Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go k (some (ky, y)) l
      | Ordering.eq => some (ky, y)
      | Ordering.gt => Std.DTreeMap.Internal.Impl.Const.getEntryGE?.go k best r
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.map'_id : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : α → C}
  [inst_1 : CategoryTheory.Limits.HasProduct f] [inst_2 : CategoryTheory.Limits.HasProduct g] (p : (b : α) → f b ⟶ g b),
  CategoryTheory.Limits.Pi.map' id p = CategoryTheory.Limits.Pi.map p
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- Pigeonhole principle for measure spaces: if `∑' i, μ (s i) > μ univ`, then
one of the intersections `s i ∩ s j` is not empty.  -/
MeasureTheory.exists_nonempty_inter_of_measure_univ_lt_tsum_measure : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s : ι → Set α},
  (∀ (i : ι), MeasureTheory.NullMeasurableSet (s i) μ) →
    μ Set.univ < ∑' (i : ι), μ (s i) → ∃ i j, i ≠ j ∧ (s i ∩ s j).Nonempty
-- Init.Data.List.Int.Sum
List.le_sum_div_length_of_min?_eq_some_int : ∀ {x : ℤ} {xs : List ℤ}, xs.min? = some x → x ≤ xs.sum / ↑xs.length
-- Mathlib.Analysis.Convex.Approximation
/-- The sequential version of `sSup_of_countable_affine_eq`.  -/
ConvexOn.sSup_of_nat_affine_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {s : Set E} {φ : E → ℝ} [inst : RCLike 𝕜] [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [inst_4 : Module 𝕜 E] [IsScalarTower ℝ 𝕜 E] [IsTopologicalAddGroup E]
  [ContinuousSMul 𝕜 E] [LocallyConvexSpace ℝ E] [HereditarilyLindelofSpace E],
  IsClosed s →
    LowerSemicontinuousOn φ s →
      ConvexOn ℝ s φ →
        ∃ l c,
          (∀ (i : ℕ), s.domRestrict (⇑RCLike.re ∘ ⇑(l i)) + Function.const (↑s) (c i) ≤ s.domRestrict φ) ∧
            ⨆ i, s.domRestrict (⇑RCLike.re ∘ ⇑(l i)) + Function.const (↑s) (c i) = s.domRestrict φ
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- Given a power series `P = u • X + O(X²)` with `u` invertible,
this is the power series `Q` such that `P(Q(X)) = X`. See `PowerSeries.subst_substInv_right`.

See also `PowerSeries.substInvOfIsUnit` for a variant using `IsUnit`.  -/
PowerSeries.substInv : {R : Type u_2} → [inst : CommRing R] → (P : PowerSeries R) → [Invertible ((PowerSeries.coeff 1) P)] → PowerSeries R
-- Mathlib.Order.FixedPoints
OrderHom.isFixedPt_gfp : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), Function.IsFixedPt (⇑f) (OrderHom.gfp f)
-- Init.Data.List.Sort.Lemmas
List.Perm.merge : ∀ {α : Type u_1} {l₁ l₂ r₁ r₂ : List α} (s₁ s₂ : α → α → Bool),
  l₁.Perm l₂ → r₁.Perm r₂ → (l₁.merge r₁ s₁).Perm (l₂.merge r₂ s₂)
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.projr_inr_apply : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K) {x : L},
  (LieAlgebra.SemiDirectSum.projr ψ) ((LieAlgebra.SemiDirectSum.inr ψ) x) = x
-- Init.Data.Nat.Lemmas
Nat.two_pow_succ : ∀ (n : ℕ), 2 ^ (n + 1) = 2 ^ n + 2 ^ n
-- Batteries.Data.List.Basic
List.dropSliceTR.go.eq_2 : ∀ {α : Type u_1} (l : List α) (m : ℕ) (a : Array α) (head : α) (xs : List α),
  List.dropSliceTR.go l m (head :: xs) 0 a = a.toListAppend (List.drop m xs)
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instAddOfAddOpposite : {M : Type u_1} → [Add Mᵃᵒᵖ] → Add Mᵈᵃᵃ
-- Init.Data.Nat.Lcm
Nat.lcm_lcm_self_left_right : ∀ (m n : ℕ), (n.lcm m).lcm m = n.lcm m
-- Mathlib.CategoryTheory.Sites.Over
/-- For `f : X ⟶ Y`, `F.over Y` viewed as a sheaf on `Over X` is isomorphic to `F.Over X`.  -/
CategoryTheory.Sheaf.pushforwardOverMapIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          (F : CategoryTheory.Sheaf J A) →
            {X Y : C} →
              (f : X ⟶ Y) →
                ((CategoryTheory.Over.map f).sheafPushforwardContinuous A (J.over X) (J.over Y)).obj (F.over Y) ≅
                  F.over X
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.isStructureInstance : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Topology.Convenient.Category
ContinuousGeneratedByCat.instFaithfulTopCatToTopCat : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)],
  (ContinuousGeneratedByCat.toTopCat X).Faithful