mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
/-- A finite measure can be interpreted as a measure.  -/
MeasureTheory.FiniteMeasure.instCoe : {Ω : Type u_1} → [inst : MeasurableSpace Ω] → Coe (MeasureTheory.FiniteMeasure Ω) (MeasureTheory.Measure Ω)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMonObj.lift_comp_zero_left_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddMonObj B] (f : A ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
  (g : A ⟶ B) {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift
        (CategoryTheory.CategoryStruct.comp f CategoryTheory.AddMonObj.zero) g)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp g h
-- Mathlib.Algebra.GroupWithZero.Range
/-- When the *domain* is itself a group with zero, the `valueMonoid` and the `valueGroup` coincide.  -/
MonoidWithZeroHom.valueMonoid_eq_valueGroup : ∀ {A : Type u_1} {B : Type u_2} [inst : GroupWithZero A] [inst_1 : GroupWithZero B] {f : A →*₀ B},
  f.valueMonoid = f.valueGroup.toSubmonoid
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.coe_comp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B] [inst_6 : Algebra R C]
  [inst_7 : CoalgebraStruct R A] [inst_8 : CoalgebraStruct R B] [inst_9 : CoalgebraStruct R C] (φ₁ : B →ₐc[R] C)
  (φ₂ : A →ₐc[R] B), ⇑(φ₁.comp φ₂) = ⇑φ₁ ∘ ⇑φ₂
-- Init.Data.Option.Monadic
Option.forM_none : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} [inst : Monad m] (f : α → m PUnit.{u_1 + 1}), forM none f = pure PUnit.unit
-- Mathlib.Analysis.RCLike.Basic
/-- The `ℝ → K` coercion, as an algebra map.  -/
RCLike.ofRealAm : {K : Type u_1} → [inst : RCLike K] → ℝ →ₐ[ℝ] K
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
ContinuousLinearEquiv.arrowCongr_symm : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {G : Type u_4} {H : Type u_5} [inst : AddCommGroup E]
  [inst_1 : AddCommGroup F] [inst_2 : AddCommGroup G] [inst_3 : AddCommGroup H] [inst_4 : NormedField 𝕜]
  [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 F] [inst_7 : Module 𝕜 G] [inst_8 : Module 𝕜 H] [inst_9 : TopologicalSpace E]
  [inst_10 : TopologicalSpace F] [inst_11 : TopologicalSpace G] [inst_12 : TopologicalSpace H]
  [inst_13 : IsTopologicalAddGroup G] [inst_14 : IsTopologicalAddGroup H] [inst_15 : ContinuousConstSMul 𝕜 G]
  [inst_16 : ContinuousConstSMul 𝕜 H] (e₁ : E ≃L[𝕜] F) (e₂ : H ≃L[𝕜] G),
  (e₁.arrowCongr e₂).symm = e₁.symm.arrowCongr e₂.symm
-- Mathlib.Topology.Order.OrderClosed
Dense.exists_ge' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {s : Set α},
  Dense s → (∀ (x : α), IsTop x → x ∈ s) → ∀ (x : α), ∃ y ∈ s, x ≤ y
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.length_toList : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (p : Equiv.Perm α) (x : α),
  (p.toList x).length = (p.cycleOf x).support.card
-- Mathlib.Data.NNReal.Defs
Real.coe_toNNReal : ∀ (r : ℝ), 0 ≤ r → ↑r.toNNReal = r
-- Mathlib.LinearAlgebra.Dimension.Subsingleton
/-- See `rank_subsingleton` that assumes `Subsingleton R` instead.  -/
rank_subsingleton' : ∀ (R : Type u_1) (M : Type u_2) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Nontrivial R]
  [Subsingleton M], Module.rank R M = 0
-- Std.Data.DTreeMap.Raw.Basic
/-- Support for the `for` loop construct in `do` blocks. Iteration happens in ascending order.  -/
Std.DTreeMap.Raw.forIn : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} →
        {m : Type w → Type w₂} → [Monad m] → ((a : α) → β a → δ → m (ForInStep δ)) → δ → Std.DTreeMap.Raw α β cmp → m δ
-- Mathlib.CategoryTheory.Action.Concrete
Action.FintypeCat.toEndHom_trivial_of_mem : ∀ {G : Type u_1} [inst : Group G] {N : Subgroup G} [inst_1 : Fintype (G ⧸ N)] [inst_2 : N.Normal] {n : G},
  n ∈ N →
    (Action.FintypeCat.toEndHom N) n =
      CategoryTheory.CategoryStruct.id (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)))
-- Std.Data.ExtHashSet.Basic
Std.ExtHashSet.instSingletonOfEquivBEqOfLawfulHashable : {α : Type u} → {x : BEq α} → {x_1 : Hashable α} → [EquivBEq α] → [LawfulHashable α] → Singleton α (Std.ExtHashSet α)
-- Std.Sat.AIG.RefVecOperator.Zip
Std.Sat.AIG.RefVec.LawfulZipOperator.instMkOrCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α], Std.Sat.AIG.RefVec.LawfulZipOperator α Std.Sat.AIG.mkOrCached
-- Init.Data.UInt.Lemmas
UInt32.toFin_ofNatTruncate_of_le : ∀ {n : ℕ}, UInt32.size ≤ n → (UInt32.ofNatClamp n).toFin = ⟨UInt32.size - 1, UInt32.toFin_ofNatClamp_of_le._proof_1⟩
-- Init.Data.Int.DivMod.Lemmas
Int.bmod.eq_1 : ∀ (x : ℤ) (m : ℕ), x.bmod m = if x % ↑m < (↑m + 1) / 2 then x % ↑m else x % ↑m - ↑m
-- Mathlib.Algebra.Order.Group.Synonym
toLex_eq_one : ∀ {α : Type u_1} [inst : One α] {a : α}, toLex a = 1 ↔ a = 1
-- Mathlib.Algebra.Group.Equiv.Defs
MulEquiv.coe_monoidHom_trans : ∀ {M : Type u_4} {N : Type u_5} {P : Type u_6} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : MulOneClass P]
  (e₁ : M ≃* N) (e₂ : N ≃* P), ↑(e₁.trans e₂) = (↑e₂).comp ↑e₁
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.ext_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  {f g : A →A[R] B}, f = g ↔ ∀ (x : A), f x = g x
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is twice differentiable on an open convex set `D ⊆ ℝ` and
`f''` is nonpositive on `D`, then `f` is concave on `D`.  -/
concaveOn_of_deriv2_nonpos' : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      DifferentiableOn ℝ f D → DifferentiableOn ℝ (deriv f) D → (∀ x ∈ D, deriv^[2] f x ≤ 0) → ConcaveOn ℝ D f
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.cramer_is_linear : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α),
  IsLinearMap α A.cramerMap
-- Mathlib.Analysis.Normed.Group.AddTorsor
/-- A `SeminormedAddCommGroup` is a `NormedAddTorsor` over itself.  -/
SeminormedAddCommGroup.toNormedAddTorsor : {V : Type u_2} → [inst : SeminormedAddCommGroup V] → NormedAddTorsor V V
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.X_pow_mul : ∀ {R : Type u_1} [inst : Semiring R] {p : SkewPolynomial R} [inst_1 : MulSemiringAction (Multiplicative ℕ) R] {n : ℕ},
  SkewPolynomial.X ^ n * p =
    (p.sum fun a b => (SkewPolynomial.monomial a) ((⇑SkewPolynomial.φ)^[n] b)) * SkewPolynomial.X ^ n
-- Mathlib.Algebra.Polynomial.Coeff
Polynomial.coeff_monomial_mul : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R) (n d : ℕ) (r : R),
  ((Polynomial.monomial n) r * p).coeff (d + n) = r * p.coeff d
-- Mathlib.Tactic.Algebraize
_private.Mathlib.Tactic.Algebraize.0.Mathlib.Tactic.Algebraize.elabAlgebraizeConfig.evalConfigItem : Lean.Elab.ConfigEval.EvalConfigItem Mathlib.Tactic.Algebraize.Config
-- Mathlib.Algebra.Group.Subgroup.Basic
AddMonoidHom.eq_liftOfRightInverse : ∀ {G₁ : Type u_5} {G₂ : Type u_6} {G₃ : Type u_7} [inst : AddGroup G₁] [inst_1 : AddGroup G₂] [inst_2 : AddGroup G₃]
  (f : G₁ →+ G₂) (f_neg : G₂ → G₁) (hf : Function.RightInverse f_neg ⇑f) (g : G₁ →+ G₃) (hg : f.ker ≤ g.ker)
  (h : G₂ →+ G₃), h.comp f = g → h = (f.liftOfRightInverse f_neg hf) ⟨g, hg⟩
-- Lean.Expr
Lean.Expr.app.injEq : ∀ (fn arg fn_1 arg_1 : Lean.Expr), (fn.app arg = fn_1.app arg_1) = (fn = fn_1 ∧ arg = arg_1)
-- Mathlib.Analysis.Meromorphic.TrailingCoefficient
/-- If `f` is analytic and does not vanish at `x`, then the trailing coefficient of `f` at `x` is `f x`.
 -/
AnalyticAt.meromorphicTrailingCoeffAt_of_ne_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, AnalyticAt 𝕜 f x → f x ≠ 0 → meromorphicTrailingCoeffAt f x = f x
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
/-- Version of `bialgHom_ext` where both assumptions are written as equalities of bundled homs.  -/
MonoidAlgebra.bialgHom_ext' : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_4} {M : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Bialgebra R A] [inst_4 : Bialgebra R B] [inst_5 : Monoid M]
  ⦃φ₁ φ₂ : MonoidAlgebra A M →ₐc[R] B⦄,
  (↑φ₁).comp (MonoidAlgebra.of A M) = (↑φ₂).comp (MonoidAlgebra.of A M) →
    (↑φ₁).comp MonoidAlgebra.singleOneAlgHom = (↑φ₂).comp MonoidAlgebra.singleOneAlgHom → φ₁ = φ₂
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
SimplexCategoryGenRel.eq_or_len_le_of_P_δ : ∀ {x y : SimplexCategoryGenRel} {f : x ⟶ y},
  SimplexCategoryGenRel.P_δ f → (∃ (h : x = y), f = CategoryTheory.eqToHom h) ∨ x.len < y.len
-- Mathlib.Analysis.RCLike.Basic
RCLike.real_smul_ofReal : ∀ {K : Type u_1} [inst : RCLike K] (r x : ℝ), r • ↑x = ↑r * ↑x
-- Mathlib.Topology.Algebra.Algebra
ContinuousLinearMap.toSpanSingleton_one_eq_algebraMapCLM : ∀ (R : Type u_1) (A : Type u) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : TopologicalSpace R] [inst_4 : TopologicalSpace A] [inst_5 : ContinuousSMul R A],
  ContinuousLinearMap.toSpanSingleton R 1 = algebraMapCLM R A
-- Mathlib.CategoryTheory.Pi.Basic
/-- A product of categories indexed by `Option J` identifies to a binary product.  -/
CategoryTheory.Pi.optionEquivalence : {J : Type w₁} →
  (C' : Option J → Type u₁) →
    [inst : (i : Option J) → CategoryTheory.Category.{v₁, u₁} (C' i)] →
      ((i : Option J) → C' i) ≌ C' none × ((j : J) → C' (some j))
-- Mathlib.Order.OrderDual
/-- **Alias** of the reverse direction of `OrderDual.ofDual_lt_ofDual`. -/
LT.lt.ofDual : ∀ {α : Type u_1} [inst : LT α] {a b : αᵒᵈ}, b < a → OrderDual.ofDual a < OrderDual.ofDual b
-- Mathlib.Logic.Unique
Unique.subsingleton_unique : ∀ {α : Sort u_1}, Subsingleton (Unique α)
-- Init.Data.ByteArray.Basic
/-- Finds the index of the first byte in `a` for which `p` returns `true`. If no byte
in `a` satisfies `p`, then the result is `none`.

The index is returned along with a proof that it is a valid index in the array.
 -/
ByteArray.findFinIdx? : (a : ByteArray) → (UInt8 → Bool) → optParam ℕ 0 → Option (Fin a.size)
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteArchimedeanClass.min_le_mk_add : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {a b : M} (ha : a ≠ 0)
  (hb : b ≠ 0) (hab : a + b ≠ 0),
  min (FiniteArchimedeanClass.mk a ha) (FiniteArchimedeanClass.mk b hb) ≤ FiniteArchimedeanClass.mk (a + b) hab
-- Init.Data.String.Lemmas.Basic
String.toByteArray_copy_slice : ∀ {s : String} {p₁ p₂ : s.Pos} {h : p₁ ≤ p₂},
  (s.slice p₁ p₂ h).copy.toByteArray = s.toByteArray.extract p₁.offset.byteIdx p₂.offset.byteIdx
-- Init.Data.List.Monadic
/-- We can express a for loop over a list which always yields as a fold.  -/
List.forIn'_yield_eq_foldlM : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {β γ : Type u_1} [inst : Monad m] [LawfulMonad m] {l : List α}
  (f : (a : α) → a ∈ l → β → m γ) (g : (a : α) → a ∈ l → β → γ → β) (init : β),
  (forIn' l init fun a m_1 b => (fun c => ForInStep.yield (g a m_1 b c)) <$> f a m_1 b) =
    List.foldlM
      (fun b x =>
        match x with
        | ⟨a, m_1⟩ => g a m_1 b <$> f a m_1 b)
      init l.attach
-- Mathlib.Algebra.Notation.Indicator
Set.mulIndicator_univ : ∀ {α : Type u_1} {M : Type u_3} [inst : One M] (f : α → M), Set.univ.mulIndicator f = f
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.inl_injective : ∀ {R : Type u} {M : Type v} [inst : Zero M], Function.Injective TrivSqZeroExt.inl
-- Init.Data.List.Nat.Modify
List.getElem_modify : ∀ {α : Type u_1} (f : α → α) (i : ℕ) (l : List α) (j : ℕ) (h : j < (l.modify i f).length),
  (l.modify i f)[j] = if i = j then f l[j] else l[j]
-- Batteries.Data.List.Lemmas
List.countBefore_cons_succ_of_beq : ∀ {α : Type u_1} {x : α} {xs : List α} {i : ℕ} {a : α} [inst : BEq α],
  (a == x) = true → List.countBefore x (a :: xs) (i + 1) = List.countBefore x xs i + 1
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoElemContKind.nonDuplicable.sizeOf_spec : sizeOf Lean.Elab.Do.DoElemContKind.nonDuplicable = 1
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Basic
/-- The direction of the sup of two affine subspaces with a common point is the sup of the two
directions.  -/
AffineSubspace.direction_sup_eq_sup_direction : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {s₁ s₂ : AffineSubspace k P} {p : P},
  p ∈ s₁ → p ∈ s₂ → (s₁ ⊔ s₂).direction = s₁.direction ⊔ s₂.direction
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coneOfIsSplitMono_pt : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f : X ⟶ Y) [inst_1 : CategoryTheory.IsSplitMono f],
  (CategoryTheory.Limits.coneOfIsSplitMono f).pt = X
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.inv_mul_cancel : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : DivisionRing β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] {x : CauSeq.Completion.Cauchy abv},
  x ≠ 0 → x⁻¹ * x = 1
-- Mathlib.Data.Finsupp.Basic
Finsupp.mapDomain_apply' : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : AddCommMonoid M] (S : Set α) {f : α → β} (x : α →₀ M),
  ↑x.support ⊆ S → Set.InjOn f S → ∀ {a : α}, a ∈ S → (Finsupp.mapDomain f x) (f a) = x a
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.isEmpty_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α],
  m₁.Equiv m₂ → m₁.isEmpty = m₂.isEmpty
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.find_parent_1 : ∀ (self : Batteries.UnionFind) (x : Fin self.size), (self.find x).fst.parent ↑x = self.rootD ↑x
-- Mathlib.Algebra.Order.AddGroupWithTop
LinearOrderedAddCommGroupWithTop.toSubNegMonoid : {α : Type u_3} → [self : LinearOrderedAddCommGroupWithTop α] → SubNegMonoid α
-- Mathlib.LinearAlgebra.Dual.Lemmas
Module.dual_finite : ∀ {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Finite R M] [Module.Projective R M], Module.Finite R (Module.Dual R M)
-- Mathlib.Data.W.Constructions
WType.ofList.eq_2 : ∀ (γ : Type u) (hd : γ) (tl : List γ),
  WType.ofList γ (hd :: tl) = WType.mk (WType.Listα.cons hd) fun x => WType.ofList γ tl
-- Mathlib.Analysis.Normed.Group.Uniform
/-- **Alias** of the forward direction of `locallyLipschitz_neg_iff`. -/
LocallyLipschitz.of_neg : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedAddCommGroup E] [inst_1 : PseudoEMetricSpace α] {f : α → E},
  LocallyLipschitz (-f) → LocallyLipschitz f
-- Mathlib.RepresentationTheory.Continuous.Basic
ContRepresentation.coind.congr_simp : ∀ {R : Type u_1} {V : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : TopologicalSpace V]
  [inst_3 : IsTopologicalAddGroup V] [inst_4 : Module R V] {G : Type u_7} {H : Type u_8} [inst_5 : Group G]
  [inst_6 : TopologicalSpace G] [inst_7 : TopologicalSpace R] [inst_8 : ContinuousSMul R V] [inst_9 : Group H]
  [inst_10 : TopologicalSpace H] (φ : G →ₜ* H) [inst_11 : IsTopologicalGroup H] (π : ContRepresentation R G V),
  ContRepresentation.coind φ π = ContRepresentation.coind φ π
-- Mathlib.Order.InitialSeg
/-- Every initial segment embedding into a well order can be turned into an isomorphism if
surjective, or into a principal segment embedding if not.  -/
InitialSeg.principalSumRelIso : {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} → {s : β → β → Prop} → [IsWellOrder β s] → InitialSeg r s → PrincipalSeg r s ⊕ (r ≃r s)
-- Init.Tactics
/-- `with_unfolding_none tacs` executes `tacs` using the `.none` transparency setting.
In this setting no definitions are unfolded.
 -/
Lean.Parser.Tactic.withUnfoldingNone : Lean.ParserDescr
-- Lean.Environment
Lean.AsyncConstantInfo.isUnsafe : Lean.AsyncConstantInfo → Bool
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBMap.toStream_toList : ∀ {α : Type u_1} {β : Type u_2} {cmp : α → α → Ordering} {t : RBTree.RBMap α β cmp}, (Std.toStream t).toList = t.toList
-- Mathlib.Data.EReal.Inv
_private.Mathlib.Data.EReal.Inv.0.EReal.exists_mul_left_lt : ∀ {a b c : EReal}, a ≠ 0 ∨ b ≠ ⊤ → a ≠ ⊤ ∨ 0 < b → a * b < c → ∃ a' ∈ Set.Ioo a ⊤, a' * b < c
-- Std.Data.TreeSet.Slice
Std.TreeSet.instSliceableRccSlice : {α : Type u} →
  (cmp : autoParam (α → α → Ordering) Std.TreeSet.instSliceableRccSlice._auto_1) →
    Std.Rcc.Sliceable (Std.TreeSet α cmp) α (Std.DTreeMap.Internal.Unit.RccSlice α)
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.combine.go.match_1.eq_4 : ∀ (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Sort u_1) (k₁ : ℤ) (m₁ : Lean.Grind.CommRing.Mon)
  (p₁ : Lean.Grind.CommRing.Poly) (k₂ : ℤ) (m₂ : Lean.Grind.CommRing.Mon) (p₂ : Lean.Grind.CommRing.Poly)
  (h_1 : (k₁ k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_2 :
    (k₁ k₂ : ℤ) →
      (m₂ : Lean.Grind.CommRing.Mon) →
        (p₂ : Lean.Grind.CommRing.Poly) →
          motive (Lean.Grind.CommRing.Poly.num k₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂))
  (h_3 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) → motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.num k₂))
  (h_4 :
    (k₁ : ℤ) →
      (m₁ : Lean.Grind.CommRing.Mon) →
        (p₁ : Lean.Grind.CommRing.Poly) →
          (k₂ : ℤ) →
            (m₂ : Lean.Grind.CommRing.Mon) →
              (p₂ : Lean.Grind.CommRing.Poly) →
                motive (Lean.Grind.CommRing.Poly.add k₁ m₁ p₁) (Lean.Grind.CommRing.Poly.add k₂ m₂ p₂)),
  (match Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ with
    | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.num k₂ => h_1 k₁ k₂
    | Lean.Grind.CommRing.Poly.num k₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_2 k₁ k₂ m₂ p₂
    | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.num k₂ => h_3 k₁ m₁ p₁ k₂
    | Lean.Grind.CommRing.Poly.add k₁ m₁ p₁, Lean.Grind.CommRing.Poly.add k₂ m₂ p₂ => h_4 k₁ m₁ p₁ k₂ m₂ p₂) =
    h_4 k₁ m₁ p₁ k₂ m₂ p₂
-- Mathlib.Algebra.Module.Torsion.Free
smul_eq_zero_iff_left : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {m : M}
  [Module.IsTorsionFree R M] [IsCancelMulZero R], m ≠ 0 → (r • m = 0 ↔ r = 0)
-- Mathlib.Computability.Partrec
Computable.subtype_mk : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {f : α → β} {p : β → Prop}
  [inst_2 : DecidablePred p] {h : ∀ (a : α), p (f a)} (hp : PrimrecPred p), Computable f → Computable fun a => ⟨f a, ⋯⟩
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.tryCatch_ExceptT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α ε : Type u} {x : ExceptT ε m α} {h : ε → ExceptT ε m α}
  [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps] (Q : Std.Do.PostCond α (Std.Do.PostShape.except ε ps)),
  ⦃(Std.Do.wp x).apply (Q.1, fun e => (Std.Do.wp (h e)).apply Q, Q.2.2)⦄ MonadExceptOf.tryCatch x h ⦃Q⦄
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
QuadraticModuleCat.toIsometry_whiskerLeft : ∀ {R : Type u} [inst : CommRing R] [inst_1 : Invertible 2] (L : QuadraticModuleCat R) {M N : QuadraticModuleCat R}
  (f : M ⟶ N),
  QuadraticModuleCat.Hom.toIsometry (CategoryTheory.MonoidalCategoryStruct.whiskerLeft L f) =
    (QuadraticMap.Isometry.id L.form).tmul (QuadraticModuleCat.Hom.toIsometry f)
-- Mathlib.Computability.Primrec.List
/-- `List.modifyHead` with a function depending on external data is primitive recursive.  -/
Primrec.list_modifyHead' : ∀ {α : Type u_1} {β : Type u_2} [inst : Primcodable α] [inst_1 : Primcodable β] {g : β → α → α},
  Primrec₂ g → Primrec₂ fun l b => List.modifyHead (g b) l
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.SimpleFunc.setToL1S_neg : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {T : Set α → E →L[ℝ] F},
  (∀ (s : Set α), MeasurableSet s → μ s = 0 → T s = 0) →
    MeasureTheory.FinMeasAdditive μ T →
      ∀ (f : ↥(α →₁ₛ[μ] E)), MeasureTheory.L1.SimpleFunc.setToL1S T (-f) = -MeasureTheory.L1.SimpleFunc.setToL1S T f
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the numerator of the second left fraction  -/
CategoryTheory.MorphismProperty.LeftFraction₃.f' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.LeftFraction₃ X Y) → X ⟶ self.Y'
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- The `Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_left`
for commutative rings.  -/
Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat_left : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N → ∀ [Nontrivial R] [Module.Flat R ↥M] (a b : ↥(M ⊓ N)), ¬LinearIndependent R ![a, b]
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.monomial_mul_X : ∀ {R : Type u} [inst : Semiring R] (n : ℕ) (r : R),
  (Polynomial.monomial n) r * Polynomial.X = (Polynomial.monomial (n + 1)) r
-- Init.SimpLemmas
and_iff_left_iff_imp : ∀ {a b : Prop}, (a ∧ b ↔ a) ↔ a → b
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
Measurable.imp : ∀ {α : Type u_1} [inst : MeasurableSpace α] {p q : α → Prop},
  Measurable p → Measurable q → Measurable fun a => p a → q a
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.separatingLeft_toMatrix₂'_iff : ∀ {R : Type u_1} {n : Type u_11} {m : Type u_12} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] {B : (m → R) →ₗ[R] (n → R) →ₗ[R] R},
  ((LinearMap.toMatrix₂' R) B).SeparatingLeft ↔ B.SeparatingLeft
-- Init.Data.Option.Basic
/-- Runs the monadic action `f` on `o`'s value, if any, and returns the result, or  `none` if there is
no value.

From the perspective of `Option` as a collection with at most one element, the monadic the function
is applied to the element if present, and the final result is empty if either the initial or the
resulting collections are empty.
 -/
Option.bindM : {m : Type u_1 → Type u_2} → {α : Type u_3} → {β : Type u_1} → [Pure m] → (α → m (Option β)) → Option α → m (Option β)
-- Mathlib.Probability.ProductMeasure
MeasureTheory.Measure.infinitePi_dirac : ∀ {ι : Type u_1} {X : ι → Type u_2} {mX : (i : ι) → MeasurableSpace (X i)} (f : (i : ι) → X i),
  (MeasureTheory.Measure.infinitePi fun i => MeasureTheory.Measure.dirac (f i)) = MeasureTheory.Measure.dirac f
-- Mathlib.Combinatorics.Additive.Corner.Defs
/-- A convenient restatement of corner-freeness in terms of an ambient product set.  -/
isCornerFree_iff : ∀ {G : Type u_1} [inst : AddCommMonoid G] {A : Set (G × G)} {s : Set G},
  A ⊆ s ×ˢ s →
    (IsCornerFree A ↔
      ∀ ⦃x₁ : G⦄,
        x₁ ∈ s → ∀ ⦃y₁ : G⦄, y₁ ∈ s → ∀ ⦃x₂ : G⦄, x₂ ∈ s → ∀ ⦃y₂ : G⦄, y₂ ∈ s → IsCorner A x₁ y₁ x₂ y₂ → x₁ = x₂)
-- Mathlib.RepresentationTheory.Intertwining
/-- Underlying linear isomorphism of an equivalence of representations.  -/
Representation.Equiv.toLinearEquiv : {A : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Semiring A] →
          [inst_1 : Monoid G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : AddCommMonoid W] →
                [inst_4 : Module A V] →
                  [inst_5 : Module A W] →
                    {ρ : Representation A G V} → {σ : Representation A G W} → ρ.Equiv σ → V ≃ₗ[A] W
-- Mathlib.Data.Nat.Factorial.Basic
Nat.one_ascFactorial : ∀ (k : ℕ), Nat.ascFactorial 1 k = k.factorial