mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Category
CategoryTheory.MonoidalCategory.rightUnitor_tensor_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X Y : C),
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y)).hom =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator X Y (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).hom)
-- Mathlib.MeasureTheory.Measure.Decomposition.IntegralRNDeriv
/-- For `f` a convex function on `Ici 0`, if `f ((μ ⊗ₘ κ).rnDeriv (ν ⊗ₘ η) (a, b))` is integrable,
then `f (μ.rnDeriv ν a)` is integrable.  -/
ConvexOn.integrable_apply_rnDeriv_of_integrable_compProd : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} {μ ν : MeasureTheory.Measure 𝓧} {𝓨 : Type u_2} {m𝓨 : MeasurableSpace 𝓨}
  {κ η : ProbabilityTheory.Kernel 𝓧 𝓨} {f : ℝ → ℝ} [MeasureTheory.IsFiniteMeasure μ] [MeasureTheory.IsFiniteMeasure ν]
  [ProbabilityTheory.IsMarkovKernel κ] [ProbabilityTheory.IsMarkovKernel η],
  MeasureTheory.StronglyMeasurable f →
    ConvexOn ℝ (Set.Ici 0) f →
      ContinuousWithinAt f (Set.Ici 0) 0 →
        MeasureTheory.Integrable (fun p => f ((μ.compProd κ).rnDeriv (ν.compProd η) p).toReal) (ν.compProd η) →
          (μ.compProd κ).AbsolutelyContinuous (μ.compProd η) →
            MeasureTheory.Integrable (fun a => f (μ.rnDeriv ν a).toReal) ν
-- Mathlib.Analysis.Normed.Module.Connected
Metric.isPreconnected_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [NormedSpace ℝ E] {x : E} {r : ℝ}, IsPreconnected (Metric.ball x r)
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- The tautological 1-hypercover induced by `S : J.Cover X`. Its index type `I₀`
is given by `S.Arrow` (i.e. all the morphisms in the sieve `S`), while `I₁` is given
by all possible pullback cones.  -/
CategoryTheory.GrothendieckTopology.Cover.oneHypercover : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} → {X : C} → J.Cover X → J.OneHypercover X
-- Mathlib.Data.Prod.TProd
List.TProd.elim'.eq_1 : ∀ {ι : Type u} {α : ι → Type v} {l : List ι} [inst : DecidableEq ι] (h : ∀ (i : ι), i ∈ l) (v : List.TProd α l) (i : ι),
  List.TProd.elim' h v i = v.elim ⋯
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.instFinitePolynomialAEval' : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (φ : M →ₗ[R] M)
  [Module.Finite R M], Module.Finite (Polynomial R) (Module.AEval' φ)
-- Mathlib.Util.Notation3
/-- The key `app.const` or `app` with a specific arity.  -/
Mathlib.Notation3.DelabKey.app : Option Lean.Name → ℕ → Mathlib.Notation3.DelabKey
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sin_nonpos_of_nonpos_of_neg_pi_le : ∀ {x : ℝ}, x ≤ 0 → -Real.pi ≤ x → Real.sin x ≤ 0
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_ofNatLT : ∀ {n : ℕ} (hn : n < USize.size) (h : System.Platform.numBits = 64), (USize.ofNatLT n hn).toBitVec64 h = n#'⋯
-- Mathlib.NumberTheory.ClassNumber.AdmissibleAbsoluteValue
/-- Any large enough family of vectors in `R^n` has a pair of elements
whose remainders are close together, pointwise.  -/
AbsoluteValue.IsAdmissible.exists_approx_aux : ∀ {R : Type u_1} [inst : EuclideanDomain R] {abv : AbsoluteValue R ℤ} (n : ℕ) (h : abv.IsAdmissible) {ε : ℝ},
  0 < ε →
    ∀ {b : R},
      b ≠ 0 →
        ∀ (A : Fin (h.card ε ^ n).succ → Fin n → R),
          ∃ i₀ i₁, i₀ ≠ i₁ ∧ ∀ (k : Fin n), ↑(abv (A i₁ k % b - A i₀ k % b)) < abv b • ε
-- Init.Data.Array.Int
Array.sum_div_length_le_max_of_max?_eq_some_int : ∀ {x : ℤ} {xs : Array ℤ}, xs.max? = some x → xs.sum / ↑xs.size ≤ x
-- Lean.Parser.Extension
Lean.Parser.registerAlias : Lean.Name →
  Lean.Name →
    Lean.Parser.ParserAliasValue →
      optParam (Option Lean.SyntaxNodeKind) none → optParam Lean.Parser.ParserAliasInfo { } → IO Unit
-- Init.Data.Vector.DecidableEq
Vector.isEqv_self : ∀ {α : Type u_1} {n : ℕ} [inst : DecidableEq α] (xs : Vector α n), (xs.isEqv xs fun x1 x2 => decide (x1 = x2)) = true
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_insertIfNew : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {fallback v : β},
  Std.ExtDHashMap.Const.getD (m.insertIfNew k v) a fallback =
    if (k == a) = true ∧ k ∉ m then v else Std.ExtDHashMap.Const.getD m a fallback
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- If `E` is a spectral sequence, and `r = r'`, this is the
isomorphism `(E.page r).X pq ≅ (E.page r').X pq`.  -/
CategoryTheory.SpectralSequence.pageXIsoOfEq : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {κ : Type u_2} →
        {c : ℤ → ComplexShape κ} →
          {r₀ : ℤ} →
            (E : CategoryTheory.SpectralSequence C c r₀) →
              (pq : κ) →
                (r r' : ℤ) →
                  (h : autoParam (r = r') CategoryTheory.SpectralSequence.pageXIsoOfEq._auto_1) →
                    (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.pageXIsoOfEq._auto_3) →
                      (E.page r ⋯).X pq ≅ (E.page r' ⋯).X pq
-- Mathlib.Algebra.Group.Prod
/-- Given monoids `M`, `N`, the natural projection homomorphism from `M × N` to `M`.  -/
MonoidHom.fst : (M : Type u_3) → (N : Type u_4) → [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M × N →* M
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueueEntry : Type
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.Basic
MeasureTheory.condExp_add : ∀ {α : Type u_1} {E : Type u_3} {m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → E}
  [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E],
  MeasureTheory.Integrable f μ →
    MeasureTheory.Integrable g μ → ∀ (m : MeasurableSpace α), μ[f + g | m] =ᵐ[μ] μ[f | m] + μ[g | m]
-- Mathlib.Probability.Kernel.Disintegration.CDFToKernel
ProbabilityTheory.IsRatCondKernelCDFAux.mono' : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {f : α × β → ℚ → ℝ}
  {κ : ProbabilityTheory.Kernel α (β × ℝ)} {ν : ProbabilityTheory.Kernel α β},
  ProbabilityTheory.IsRatCondKernelCDFAux f κ ν → ∀ (a : α) {q r : ℚ}, q ≤ r → ∀ᵐ (c : β) ∂ν a, f (a, c) q ≤ f (a, c) r
-- Mathlib.Data.List.Basic
List.instSingletonList : {α : Type u} → Singleton α (List α)
-- Init.Data.UInt.Lemmas
UInt8.ofNatTruncate_toNat : ∀ (n : UInt8), UInt8.ofNatClamp n.toNat = n
-- Lean.ToExpr
Lean.instToExprLiteral : Lean.ToExpr Lean.Literal
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.Pos.skip?_cast : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat]
  [inst_1 : String.Slice.Pattern.ForwardPattern pat] [String.Slice.Pattern.Model.LawfulForwardPatternModel pat]
  {s t : String.Slice} (hst : s.copy = t.copy) {pos : s.Pos},
  (pos.cast hst).skip? pat = Option.map (fun x => x.cast hst) (pos.skip? pat)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.edist_eq_card : ∀ {ι : Type u_2} {β : ι → Type u_4} [inst : Fintype ι] [inst_1 : (i : ι) → EDist (β i)] (f g : PiLp 0 β),
  edist f g = ↑⋯.toFinset.card
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.insertMany_list_eq_empty_iff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l : List α}, m.insertMany l = ∅ ↔ m = ∅ ∧ l = []
-- Mathlib.NumberTheory.Height.Projectivization
/-- The multiplicative height of a point on a finite-dimensional projective space over `K`
with a given basis.  -/
Projectivization.mulHeight : {K : Type u_1} →
  [inst : Field K] → [Height.AdmissibleAbsValues K] → {ι : Type u_2} → [Finite ι] → Projectivization K (ι → K) → ℝ
-- Init.Data.List.Lemmas
List.forall_mem_replicate : ∀ {α : Type u_1} {p : α → Prop} {a : α} {n : ℕ}, (∀ b ∈ List.replicate n a, p b) ↔ n = 0 ∨ p a
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `tsub_add_eq_add_tsub` for the equality.  -/
add_tsub_le_tsub_add : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b c : α}
  [AddLeftMono α], a + b - c ≤ a - c + b
-- Mathlib.CategoryTheory.Monoidal.Center
/-- Construct an isomorphism in the Drinfeld center from
a morphism whose underlying morphism is an isomorphism.
 -/
CategoryTheory.Center.isoMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {X Y : CategoryTheory.Center C} → (f : X ⟶ Y) → [CategoryTheory.IsIso f.f] → X ≅ Y
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.one_rel : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} (y : ↥S), (Localization.r S) 1 (↑y, y)
-- Mathlib.Geometry.Manifold.IsManifold.InteriorBoundary
Diffeomorph.boundarylessManifold : ∀ {𝕜 : 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'}
  {N : Type u_7} [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace H' N] {n : WithTop ℕ∞},
  n ≠ 0 → ∀ (Φ : Diffeomorph I I' M N n) [BoundarylessManifold I M], BoundarylessManifold I' N
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.degree_add_eq_right_of_lt : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f g : MvPolynomial σ R},
  m.toSyn (m.degree f) < m.toSyn (m.degree g) → m.degree (f + g) = m.degree g
-- Lean.Server.FileWorker.SemanticHighlighting
_private.Lean.Server.FileWorker.SemanticHighlighting.0.Lean.Server.FileWorker.collectVersoTokens.tok : Lean.Syntax → Lean.Lsp.SemanticTokenType → StateM (Array Lean.Server.FileWorker.LeanSemanticToken) Unit
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem_toArray_roo : ∀ {m n i : ℕ} (_h : i < (m<...n).toArray.size), (m<...n).toArray[i] = m + 1 + i
-- Mathlib.Data.Setoid.Basic
/-- Given a function `f : α → β`, an equivalence relation `r` on `β` induces an equivalence
relation on `α` defined by '`x ≈ y` iff `f(x)` is related to `f(y)` by `r`'.

See note [reducible non-instances].  -/
Setoid.comap : {α : Type u_1} → {β : Type u_2} → (α → β) → Setoid β → Setoid α
-- Mathlib.Analysis.Convex.Strong
UniformConcaveOn.concaveOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {φ : ℝ → ℝ} {s : Set E} {f : E → ℝ},
  UniformConcaveOn s φ f → 0 ≤ φ → ConcaveOn ℝ s f
-- Init.Data.UInt.Bitwise
UInt64.not_eq_neg_sub : ∀ (a : UInt64), ~~~a = -a - 1
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
Algebra.IsIntegral.adjoin : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {S : Set A},
  (∀ x ∈ S, IsIntegral R x) → Algebra.IsIntegral R ↥(Algebra.adjoin R S)
-- Mathlib.Data.Multiset.UnionInter
Multiset.instUnion : {α : Type u_1} → [DecidableEq α] → Union (Multiset α)
-- Mathlib.Order.InitialSeg
PrincipalSeg.isMin_apply_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder β] {a : α} [inst_1 : PartialOrder α] (f : α <i β),
  IsMin (f.toRelEmbedding a) ↔ IsMin a
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.NatTrans.mapHomologicalComplex_id : ∀ {ι : Type u_1} {W₁ : Type u_3} {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] (c : ComplexShape ι) (F : CategoryTheory.Functor W₁ W₂)
  [inst_4 : F.PreservesZeroMorphisms],
  CategoryTheory.NatTrans.mapHomologicalComplex (CategoryTheory.CategoryStruct.id F) c =
    CategoryTheory.CategoryStruct.id (F.mapHomologicalComplex c)
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- **Alias** of `TypeCat.symm_of_symmetricRelation`.

---

An internal symmetric relation in the category of types gives rise to a standard symmetric
relation.  -/
TypeCat.symmetric_of_symmetricRelation : ∀ {X R : Type w} {p₁ p₂ : R ⟶ X} (e : CategoryTheory.SymmetricRelation p₁ p₂), Std.Symm (TypeCat.Rel.ofPair p₁ p₂)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.congr_symm_tprod : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {t : ι → Type u_11} [inst_3 : (i : ι) → AddCommMonoid (t i)]
  [inst_4 : (i : ι) → Module R (t i)] (f : (i : ι) → s i ≃ₗ[R] t i) (p : (i : ι) → t i),
  (PiTensorProduct.congr f).symm ((PiTensorProduct.tprod R) p) = ⨂ₜ[R] (i : ι), (f i).symm (p i)
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_compL_smulLeftCLM : ∀ {𝕜 : Type u_2} {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NontriviallyNormedField 𝕜]
  [inst_5 : NormedAlgebra ℝ 𝕜] [inst_6 : NormedSpace 𝕜 F] {g₁ g₂ : E → 𝕜},
  Function.HasTemperateGrowth g₁ →
    Function.HasTemperateGrowth g₂ →
      SchwartzMap.smulLeftCLM F g₁ ∘SL SchwartzMap.smulLeftCLM F g₂ = SchwartzMap.smulLeftCLM F (g₁ * g₂)
-- Mathlib.Order.Basic
le_of_forall_lt_imp_ne : ∀ {α : Type u_2} [inst : LinearOrder α] {a b : α}, (∀ c < a, c ≠ b) → a ≤ b
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.setIntegral_eq_tsum : ∀ {G : Type u_1} {α : Type u_3} {E : Type u_5} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α]
  [inst_3 : NormedAddCommGroup E] {s : Set α} {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α]
  [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G] [inst_7 : NormedSpace ℝ E],
  MeasureTheory.IsFundamentalDomain G s μ →
    ∀ {f : α → E} {t : Set α},
      MeasureTheory.IntegrableOn f t μ → ∫ (x : α) in t, f x ∂μ = ∑' (g : G), ∫ (x : α) in t ∩ g • s, f x ∂μ
-- Mathlib.Algebra.GroupWithZero.Basic
mul_eq_zero_of_ne_zero_imp_eq_zero : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] {a b : M₀}, (a ≠ 0 → b = 0) → a * b = 0
-- Mathlib.Combinatorics.Enumerative.Partition.Basic
/-- The finset of those partitions in which every part is odd and used at most once.  -/
Nat.Partition.oddDistincts : (n : ℕ) → Finset n.Partition
-- Lean.Elab.SetOption
_private.Lean.Elab.SetOption.0.Lean.Elab.elabSetOption.setOption : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadOptions m] →
      [Lean.MonadError m] → Lean.Name → Lean.OptionDecl → Lean.DataValue → m (Lean.Options × Lean.OptionDecl)
-- Mathlib.Analysis.Complex.ExponentialBounds
Real.exp_one_gt_d9 : 2.7182818283 < Real.exp 1
-- Std.Http.Data.Method
/-- Create a workspace resource.
Source: https://www.rfc-editor.org/rfc/rfc3253#section-6.3
 -/
Std.Http.Method.mkworkspace : Std.Http.Method
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.get!_insert_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t.WF → ∀ {k : α} {v : β}, Std.DTreeMap.Raw.Const.get! (t.insert k v) k = v
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trTape_mk' : ∀ {Γ : Type u_1} {n : ℕ} {enc : Γ → List.Vector Bool n} [inst : Inhabited Γ]
  (enc0 : enc default = List.Vector.replicate n false) (L R : Turing.ListBlank Γ),
  Turing.TM1to1.trTape enc0 (Turing.Tape.mk' L R) = Turing.TM1to1.trTape' enc0 L R
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instMulActionWithZeroOfContinuousConstSMul : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : Zero β] →
          {R : Type u_5} →
            [inst_3 : MonoidWithZero R] →
              [inst_4 : MulActionWithZero R β] →
                [ContinuousConstSMul R β] → MulActionWithZero R (CompactlySupportedContinuousMap α β)
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.IsClosedUnderColimitsOfShape.inverseImage : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] (J : Type u') [inst_2 : CategoryTheory.Category.{v', u'} J]
  (P : CategoryTheory.ObjectProperty D) (F : CategoryTheory.Functor C D) [P.IsClosedUnderColimitsOfShape J]
  [CategoryTheory.Limits.PreservesColimitsOfShape J F], (P.inverseImage F).IsClosedUnderColimitsOfShape J
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.Basic
CategoryTheory.Abelian.Ext.comp_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y Z : C} {n : ℕ} (α : CategoryTheory.Abelian.Ext X Y n) {m : ℕ}
  (β₁ β₂ : CategoryTheory.Abelian.Ext Y Z m) {p : ℕ} (h : n + m = p), α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
-- Mathlib.Order.RelIso.Basic
RelIso.symm_symm : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (e : r ≃r s), e.symm.symm = e
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get!_empty : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α] {a : α}, ∅.get! a = default
-- Lean.Meta.Sym.Simp.SimpM
Lean.Meta.Sym.Simp.instInhabitedResult : Inhabited Lean.Meta.Sym.Simp.Result
-- Mathlib.Data.Finset.Insert
/-- `cons a s h` is the set `{a} ∪ s` containing `a` and the elements of `s`. It is the same as
`insert a s` when it is defined, but unlike `insert a s` it does not require `DecidableEq α`,
and the union is guaranteed to be disjoint.  -/
Finset.cons : {α : Type u_1} → (a : α) → (s : Finset α) → a ∉ s → Finset α
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Unit.RocSliceData.mk.sizeOf_spec : ∀ {α : Type u} [inst : Ord α] [inst_1 : SizeOf α] (treeMap : Std.DTreeMap.Internal.Impl α fun x => Unit)
  (range : Std.Roc α), sizeOf { treeMap := treeMap, range := range } = 1 + sizeOf treeMap + sizeOf range
-- Init.Grind.Ring.Basic
/-- Scalar multiplication by natural numbers is consistent with scalar multiplication by integers.  -/
Lean.Grind.Ring.zsmul_natCast_eq_nsmul : ∀ {α : Type u} [self : Lean.Grind.Ring α] (n : ℕ) (a : α), ↑n • a = n • a
-- Lean.Elab.Do.Basic
Lean.Elab.Do.DoElemContKind.duplicable : Lean.Elab.Do.DoElemContKind
-- Mathlib.RepresentationTheory.Subrepresentation
Subrepresentation.coe_inf : ∀ {A : Type u_1} {G : Type u_2} {W : Type u_3} [inst : Semiring A] [inst_1 : Monoid G] [inst_2 : AddCommMonoid W]
  [inst_3 : Module A W] {ρ : Representation A G W} (ρ₁ ρ₂ : Subrepresentation ρ), ↑(ρ₁ ⊓ ρ₂) = ↑ρ₁ ∩ ↑ρ₂
-- Lean.Meta.Tactic.Grind.CheckResult
Lean.Meta.Grind.CheckResult.closed.sizeOf_spec : sizeOf Lean.Meta.Grind.CheckResult.closed = 1
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.coequalizer.condition_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] (f g : X ⟶ Y)
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] {Z : C} (h : CategoryTheory.Limits.coequalizer f g ⟶ Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) h) =
    CategoryTheory.CategoryStruct.comp g
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) h)
-- Init.Data.String.Basic
ByteArray.utf8Decode?.go : (b : ByteArray) → (i : ℕ) → Array Char → i ≤ b.size → Option (Array Char)
-- Std.Data.DHashMap.Internal.Model
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.Raw₀.getₘ : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      [LawfulBEq α] →
        [inst_2 : Hashable α] → (m : Std.DHashMap.Internal.Raw₀ α β) → (a : α) → m.containsₘ a = true → β a
-- Mathlib.Data.Fin.SuccPredOrder
Fin.orderSucc_eq : ∀ {n : ℕ}, Order.succ = fun i => Fin.lastCases (Fin.last n) Fin.succ i
-- Mathlib.CategoryTheory.Limits.Cones
/-- A map from the vertex of a cocone naturally induces a cocone by composition.  -/
CategoryTheory.Limits.Cocone.extensions : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (c : CategoryTheory.Limits.Cocone F) →
            (CategoryTheory.coyoneda.obj (Opposite.op c.pt)).comp CategoryTheory.uliftFunctor.{u₁, v₃} ⟶ F.cocones
-- Mathlib.NumberTheory.Height.Basic
/-- The "local" version of the height bound for arbitrary sums for nonarchimedean
absolute values.  -/
Finset.max_abv_sum_one_le_of_isNonarchimedean : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : CommSemiring S] [inst_2 : LinearOrder S] [IsOrderedRing S]
  {v : AbsoluteValue R S},
  IsNonarchimedean ⇑v → ∀ {ι : Type u_3} (s : Finset ι) (x : ι → R), max (v (∑ i ∈ s, x i)) 1 ≤ ∏ i ∈ s, max (v (x i)) 1
-- Mathlib.Algebra.Group.UniqueProds.Basic
UniqueProds.instMulOpposite : ∀ {G : Type u} [inst : Mul G] [h : UniqueProds G], UniqueProds Gᵐᵒᵖ
-- Mathlib.Algebra.Group.Action.End
/-- Given an action of a group `G` on a set `α`, each `g : G` defines a permutation of `α`.  -/
MulAction.toPermHom : (G : Type u_1) → (α : Type u_5) → [inst : Group G] → [MulAction G α] → G →* Equiv.Perm α
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- Result type for `s₁.startsWith s₂`
 -/
_private.Lean.Meta.Tactic.Grind.AC.Seq.0.Lean.Grind.AC.StartsWithResult : Type
-- Std.Data.ExtTreeMap.Basic
Std.ExtTreeMap.instMembershipOfTransCmp : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Membership α (Std.ExtTreeMap α β cmp)
-- Mathlib.LinearAlgebra.Determinant
/-- On a `LinearEquiv`, the domain of `LinearMap.det` can be promoted to `Rˣ`.  -/
LinearEquiv.det : {R : Type u_1} →
  [inst : CommRing R] → {M : Type u_2} → [inst_1 : AddCommGroup M] → [inst_2 : Module R M] → (M ≃ₗ[R] M) →* Rˣ
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.of.sizeOf_spec : ∀ (carrier : Type u) [str : SeminormedAddCommGroup carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Mathlib.Algebra.Order.Monoid.Defs
IsOrderedCancelAddMonoid.of_add_lt_add_left : ∀ {α : Type u_2} [inst : AddCommMonoid α] [inst_1 : LinearOrder α],
  (∀ (a b c : α), b < c → a + b < a + c) → IsOrderedCancelAddMonoid α
-- Lean.Meta.Basic
/-- Return the level of the given universe level metavariable.
 -/
Lean.LMVarId.getLevel : Lean.LMVarId → Lean.MetaM ℕ
-- Mathlib.LinearAlgebra.Matrix.Symmetric
Matrix.isSymm_one : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : One α], Matrix.IsSymm 1
-- Mathlib.CategoryTheory.PathCategory.MorphismProperty
/-- If `W` and `W'` are morphism properties on `C` such that `W ≤ W'`, then `W.paths ≤ W'.paths`.  -/
CategoryTheory.MorphismProperty.monotone_paths : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C], Monotone CategoryTheory.MorphismProperty.paths
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.SimplicialObject.augmentedCechNerve_map_left_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 :
    ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
      CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  {X Y : CategoryTheory.Arrow C} (F : X ⟶ Y) (n : SimplexCategoryᵒᵖ),
  (CategoryTheory.SimplicialObject.augmentedCechNerve.map F).left.app n =
    CategoryTheory.Limits.WidePullback.lift
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.base fun x => X.hom)
        (CategoryTheory.Arrow.Hom.right F))
      (fun i =>
        CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.WidePullback.π (fun x => X.hom) i)
          (CategoryTheory.Arrow.Hom.left F))
      ⋯
-- Mathlib.Order.Heyting.Basic
compl_unique : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ⊓ b = ⊥ → a ⊔ b = ⊤ → aᶜ = b