mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Group.Convolution
/-- Convolution of a measure μ with the dirac measure at 0 returns μ.  -/
MeasureTheory.Measure.conv_dirac_zero : ∀ {M : Type u_1} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M] (μ : MeasureTheory.Measure M)
  [MeasureTheory.SFinite μ], μ.conv (MeasureTheory.Measure.dirac 0) = μ
-- Mathlib.Topology.MetricSpace.Isometry
IsometryEquiv.symm_comp_self : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (h : α ≃ᵢ β),
  ⇑h.symm ∘ ⇑h = id
-- Init.Data.UInt.Lemmas
UInt16.ofNatClamp_bitVecToNat : ∀ (n : BitVec 16), UInt16.ofNatClamp n.toNat = { toBitVec := n }
-- Mathlib.Analysis.InnerProductSpace.Spectrum
/-- The **Spectral Theorem** for compact self-adjoint operators: the eigenspaces of a compact
self-adjoint operator have trivial orthogonal complement.  -/
ContinuousLinearMap.orthogonalComplement_iSup_eigenspaces_eq_bot : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [CompleteSpace E] {T : E →L[𝕜] E}, IsCompactOperator ⇑T → (↑T).IsSymmetric → (⨆ μ, Module.End.eigenspace (↑T) μ)ᗮ = ⊥
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
/-- Continuous multilinear maps over the ring `R`, from `∀ i, M₁ i` to `M₂` where `M₁ i` and `M₂`
are modules over `R` with a topological structure. In applications, there will be compatibility
conditions between the algebraic and the topological structures, but this is not needed for the
definition.  -/
ContinuousMultilinearMap.cont : ∀ {R : Type u} {ι : Type v} {M₁ : ι → Type w₁} {M₂ : Type w₂} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : AddCommMonoid M₂] [inst_3 : (i : ι) → Module R (M₁ i)]
  [inst_4 : Module R M₂] [inst_5 : (i : ι) → TopologicalSpace (M₁ i)] [inst_6 : TopologicalSpace M₂]
  (self : ContinuousMultilinearMap R M₁ M₂), Continuous self.toFun
-- Batteries.Data.List.Basic
/-- Fold a list from left to right as with `foldl`, but the combining function
also receives each element's index added to an optional parameter `start`
(i.e. the numbers that `f` takes as its first argument will be greater than or equal to `start` and
less than `start + l.length`).
 -/
List.foldlIdx : {α : Sort u_1} → {β : Type u_2} → (ℕ → α → β → α) → α → List β → optParam ℕ 0 → α
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.closure_eq_of_isRelational : ∀ (L : FirstOrder.Language) {M : Type w} [inst : L.Structure M] [L.IsRelational] (s : Set M),
  ↑((FirstOrder.Language.Substructure.closure L).toFun s) = s
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- When `C` has enough injectives, the object `Injective.syzygies f` is
an arbitrarily chosen injective object under `cokernel f`.
 -/
CategoryTheory.Injective.syzygies : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.EnoughInjectives C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {X Y : C} → (f : X ⟶ Y) → [CategoryTheory.Limits.HasCokernel f] → C
-- Mathlib.Tactic.NormNum.Result
/-- The result is `q : NNRat` and `proof : isNNRat x q`.  -/
Mathlib.Meta.NormNum.Result.isNNRat' : {u : Lean.Level} →
  {α : Q(Type u)} →
    {x : Q(«$α»)} →
      (inst : autoParam Q(DivisionSemiring «$α») Mathlib.Meta.NormNum.Result.isNNRat'._auto_1) →
        ℚ → (n d : Q(ℕ)) → Q(Mathlib.Meta.NormNum.IsNNRat «$x» «$n» «$d») → Mathlib.Meta.NormNum.Result x
-- Mathlib.Algebra.Category.MonCat.Basic
/-- multiplicative equivalences between `CommMonoid`s are the same as (isomorphic to) isomorphisms
in `CommMonCat`  -/
mulEquivIsoCommMonCatIso : {X Y : Type u} → [inst : CommMonoid X] → [inst_1 : CommMonoid Y] → X ≃* Y ≅ CommMonCat.of X ≅ CommMonCat.of Y
-- Aesop.Stats.Basic
Aesop.profilingRuleSelection : {m : Type → Type} → [Monad m] → [Aesop.MonadStats m] → [MonadLiftT BaseIO m] → {α : Type} → m α → m α
-- Init.Data.String.Bootstrap
/-- Constructs a singleton string that contains only the provided character.

Examples:
* `'L'.toString = "L"`
* `'"'.toString = "\""`
 -/
Char.toString : Char → String
-- Init.Core
imp_congr : ∀ {a b c d : Prop}, (a ↔ c) → (b ↔ d) → (a → b ↔ c → d)
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Localization.r_iff_exists : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {x y : M × ↥S},
  (Localization.r S) x y ↔ ∃ c, ↑c * (↑y.2 * x.1) = ↑c * (↑x.2 * y.1)
-- Mathlib.Algebra.Group.Defs
InvolutiveInv.mk : {G : Type u_2} → [toInv : Inv G] → (∀ (x : G), x⁻¹⁻¹ = x) → InvolutiveInv G
-- Mathlib.Data.Num.Lemmas
Num.cmp_swap : ∀ (m n : Num), (m.cmp n).swap = n.cmp m
-- Mathlib.Data.Nat.Digits.Lemmas
List.consFixedLengthDigits.congr_simp : ∀ {b b_1 : ℕ} (e_b : b = b_1) (hb : 1 < b) (l l_1 : ℕ),
  l = l_1 → ∀ (d d_1 : ℕ), d = d_1 → List.consFixedLengthDigits hb l d = List.consFixedLengthDigits ⋯ l_1 d_1
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsAddIndecomposable.apply_ne_zero_iff_mem_closure : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : AddCommGroup G] [inst_1 : LinearOrder S] [Finite ι]
  [inst_3 : InvolutiveNeg ι] [inst_4 : AddCommGroup S] [IsOrderedAddMonoid S] (v : ι → G) (f : G →+ S) (i : ι),
  v i ≠ 0 →
    v (-i) = -v i →
      (f (v i) ≠ 0 ↔
        v i ∈ AddSubmonoid.closure (v '' IsAddIndecomposable.baseOf v f) ∨
          -v i ∈ AddSubmonoid.closure (v '' IsAddIndecomposable.baseOf v f))
-- Init.Core
instBEqOption : {α : Type u_1} → [BEq α] → BEq (Option α)
-- Init.Data.Range.Polymorphic.Char
Char.instLawfulHasSize_1 : Std.Rxo.LawfulHasSize Char
-- Mathlib.CategoryTheory.MorphismProperty.TransfiniteComposition
CategoryTheory.MorphismProperty.transfiniteCompositions_monotone : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  Monotone CategoryTheory.MorphismProperty.transfiniteCompositions.{w, v, u}
-- Mathlib.Logic.Basic
eq_or_ne : ∀ {α : Sort u_1} (x y : α), x = y ∨ x ≠ y
-- Mathlib.Computability.Encoding
/-- Given an `Encoding` of `α` and `β`,
constructs an `Encoding` of `α × β` by concatenating the encodings,
mapping the symbols from the first encoding with `Sum.inl`
and those from the second with `Sum.inr`.
 -/
Computability.encodingProd : {α : Type u_1} →
  {β : Type u_2} →
    {Γ₁ : Type u_3} →
      {Γ₂ : Type u_4} →
        Computability.Encoding α Γ₁ → Computability.Encoding β Γ₂ → Computability.Encoding (α × β) (Γ₁ ⊕ Γ₂)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.im_star : ∀ (z : Complex.UnitClosedDisc), (star z).im = -z.im
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.minD_eq_iff_get?_eq_self_and_forall : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t.isEmpty = false → ∀ {km fallback : α}, t.minD fallback = km ↔ t.get? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getKeyD_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.DTreeMap α (fun x => Unit) cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k fallback : α},
  k ∉ t → l.contains k = false → (Std.DTreeMap.Const.insertManyIfNewUnit t l).getKeyD k fallback = fallback
-- Mathlib.Topology.Algebra.UniformConvergence
instCommGroupUniformFun.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : CommGroup β],
  instCommGroupUniformFun = { toGroup := instGroupUniformFun, mul_comm := ⋯ }
-- Mathlib.RepresentationTheory.Coinvariants
Representation.coinvariantsTprodLeftRegularLEquiv_apply : ∀ {k : Type u_6} {G : Type u_7} {V : Type u_8} [inst : CommRing k] [inst_1 : Group G] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] (ρ : Representation k G V) (x : (ρ.tprod (Representation.leftRegular k G)).Coinvariants),
  ρ.coinvariantsTprodLeftRegularLEquiv x = ρ.ofCoinvariantsTprodLeftRegular x
-- Init.Data.Int.Lemmas
Int.beq'_ne : ∀ (a b : ℤ), (a.beq' b = false) = (a ≠ b)
-- Lean.Elab.Term.TermElabM
/-- `mvarArgNames` stores the argument names associated to metavariables.
These are used in combination with `mvarErrorInfos` for throwing errors about metavariables that could not be fully instantiated.
For example when elaborating `List _`, the argument name of the placeholder will be `α`.

While elaborating an application, `mvarArgNames` is set for each metavariable argument, using the available argument name.
This may happen before or after the `mvarErrorInfos` is set for the same metavariable.

We used to store the argument names in `mvarErrorInfos`, updating the `MVarErrorInfos` to add the argument name when it is available,
but this doesn't work if the argument name is available _before_ the `mvarErrorInfos` is set for that metavariable.
 -/
Lean.Elab.Term.State.mvarArgNames : Lean.Elab.Term.State → Lean.MVarIdMap Lean.Name
-- Mathlib.Algebra.Lie.Nilpotent
LieSubmodule.lcs_le_iff : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] {N₁ N₂ : LieSubmodule R L M}
  [inst_6 : LieModule R L M] (k : ℕ), LieSubmodule.lcs k N₁ ≤ N₂ ↔ N₁ ≤ LieSubmodule.ucs k N₂
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.splitMono_retraction : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract X Y),
  h.splitMono.retraction = h.r
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKey!_diff_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [inst : Inhabited α]
  [Std.TransCmp cmp] {k : α}, k ∉ t₂ → (t₁ \ t₂).getKey! k = t₁.getKey! k
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.bind_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {T : C} (E : CategoryTheory.PreZeroHypercover T)
  (F : (i : E.I₀) → CategoryTheory.PreZeroHypercover (E.X i)) (ij : (i : E.I₀) × (F i).I₀),
  (E.bind F).X ij = (F ij.fst).X ij.snd
-- Mathlib.Order.Filter.Defs
/-- Product of filters. This is the filter generated by Cartesian products
of elements of the component filters.  -/
Filter.instSProd : {α : Type u_1} → {β : Type u_2} → SProd (Filter α) (Filter β) (Filter (α × β))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.mem_of_mem_keys : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {k : α}, k ∈ t.keys → k ∈ t
-- Mathlib.CategoryTheory.Limits.Types.Limits
CategoryTheory.Limits.Types.limit_ext : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J (Type u))
  [inst_1 : CategoryTheory.Limits.HasLimit F] (x y : CategoryTheory.Limits.limit F),
  (∀ (j : J),
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) x =
        (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.limit.π F j)) y) →
    x = y
-- Mathlib.CategoryTheory.Monoidal.ExternalProduct.Basic
/-- A version of `externalProductSwap` phrased in terms of the curried functors.  -/
CategoryTheory.MonoidalCategory.externalProductFlip : (J₁ : Type u₁) →
  (J₂ : Type u₂) →
    (C : Type u₃) →
      [inst : CategoryTheory.Category.{v₁, u₁} J₁] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} J₂] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            [inst_3 : CategoryTheory.MonoidalCategory C] →
              [CategoryTheory.BraidedCategory C] →
                (CategoryTheory.Functor.postcompose₂.obj (CategoryTheory.flipFunctor J₁ J₂ C)).obj
                    (CategoryTheory.MonoidalCategory.externalProductBifunctorCurried J₁ J₂ C) ≅
                  (CategoryTheory.MonoidalCategory.externalProductBifunctorCurried J₂ J₁ C).flip
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f + g) x = f x + g x`, `0 x = 0`, and
`(n • f) x = n • f x` is a right cancel additive monoid if `β` is a right cancel
additive monoid.  -/
FunLike.addRightCancelMonoid : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : FunLike F α β] →
        [inst_1 : Add F] →
          [inst_2 : Zero F] →
            [inst_3 : SMul ℕ F] →
              [inst_4 : AddRightCancelMonoid β] →
                [IsZeroApply F α β] → [IsAddApply F α β] → [IsSMulApply ℕ F α β] → AddRightCancelMonoid F
-- Init.Prelude
/-- `.str p s` is now the preferred form.
 -/
Lean.Name.mkStr : Lean.Name → String → Lean.Name
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.addAction'.eq_1 : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : AddMonoid R] [inst_1 : AddAction R M] [inst_2 : AddMonoid S]
  [inst_3 : VAdd S R] [inst_4 : AddAction S M] [inst_5 : VAddAssocClass S R M] (p : SubAddAction R M),
  p.addAction' = { toVAdd := p.vadd', add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Data.ENNReal.Basic
ENNReal.ofNNReal_sub_natCast : ∀ (r : NNReal) (n : ℕ), ↑(r - ↑n) = ↑r - ↑n
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isEmpty_emptyc : ∀ {α : Type u} {cmp : α → α → Ordering}, ∅.isEmpty = true
-- Lean.Elab.Syntax
/-- Sequence (aka NullNode)  -/
_private.Lean.Elab.Syntax.0.Lean.Elab.Term.toParserDescr.processSeq : Lean.Syntax → Lean.Elab.Term.ToParserDescrM (Lean.Term × ℕ)
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.isSome_minKey?_of_isSome_minKey?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.erase k).minKey?.isSome = true → t.minKey?.isSome = true
-- Init.Data.List.Basic
List.length_singleton : ∀ {α : Type u} {a : α}, [a].length = 1
-- Mathlib.Data.ENNReal.Operations
ENNReal.sub_iSup : ∀ {ι : Sort u_1} {f : ι → ENNReal} {a : ENNReal} [Nonempty ι], a ≠ ⊤ → a - ⨆ i, f i = ⨅ i, a - f i
-- Mathlib.Order.Category.NonemptyFinLinOrd
/-- The generating arrow `i ⟶ i+1` in the category `Fin n`  -/
Fin.homSucc : {n : ℕ} → (i : Fin n) → i.castSucc ⟶ i.succ
-- Mathlib.CategoryTheory.Core
CategoryTheory.CoreHom.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : CategoryTheory.Core C} (iso iso_1 : X.of ≅ Y.of),
  ({ iso := iso } = { iso := iso_1 }) = (iso = iso_1)
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.enorm_apply_le : ∀ {p : ENNReal} {ι : Type u_2} {β : ι → Type u_4} [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] (x : PiLp p β) (i : ι), ‖x.ofLp i‖ₑ ≤ ‖x‖ₑ
-- Mathlib.RepresentationTheory.Basic
/-- Given representations of `G` on `V` and `W`, there is a natural representation of `G` on the
module `V →ₗ[k] W`, where `G` acts by conjugation.
 -/
Representation.linHom : {k : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : CommSemiring k] →
          [inst_1 : Group G] →
            [inst_2 : AddCommMonoid V] →
              [inst_3 : Module k V] →
                [inst_4 : AddCommMonoid W] →
                  [inst_5 : Module k W] → Representation k G V → Representation k G W → Representation k G (V →ₗ[k] W)
-- Mathlib.Data.Rel
SetRel.preimage_inter_cod : ∀ {α : Type u_1} {β : Type u_2} (R : SetRel α β) (t : Set β), R.preimage (t ∩ R.cod) = R.preimage t
-- Aesop.Forward.State
_private.Aesop.Forward.State.0.Aesop.RuleState.update.addCompleteMatches : Aesop.RuleState →
  Array Aesop.ForwardRuleMatch → Array Aesop.ClusterState → ℕ → Array Aesop.Match → Array Aesop.ForwardRuleMatch
-- Batteries.Data.BinomialHeap.Basic
Batteries.BinomialHeap.Imp.FindMin.WF.mk.inj : ∀ {α : Type u_1} {le : α → α → Bool} {res : Batteries.BinomialHeap.Imp.FindMin α} {rank : ℕ}
  {before :
    ∀ {s : Batteries.BinomialHeap.Imp.Heap α},
      Batteries.BinomialHeap.Imp.Heap.WF le rank s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (res.before s)}
  {node : Batteries.BinomialHeap.Imp.HeapNode.WF le res.val res.node rank}
  {next : Batteries.BinomialHeap.Imp.Heap.WF le (rank + 1) res.next} {rank_1 : ℕ}
  {before_1 :
    ∀ {s : Batteries.BinomialHeap.Imp.Heap α},
      Batteries.BinomialHeap.Imp.Heap.WF le rank_1 s → Batteries.BinomialHeap.Imp.Heap.WF le 0 (res.before s)}
  {node_1 : Batteries.BinomialHeap.Imp.HeapNode.WF le res.val res.node rank_1}
  {next_1 : Batteries.BinomialHeap.Imp.Heap.WF le (rank_1 + 1) res.next},
  { rank := rank, before := before, node := node, next := next } =
      { rank := rank_1, before := before_1, node := node_1, next := next_1 } →
    rank = rank_1
-- Mathlib.Order.Filter.Cocardinal
Set.Finite.compl_mem_cocardinal : ∀ {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {s : Set α}, s.Finite → sᶜ ∈ Filter.cocardinal α hreg
-- Mathlib.Util.Delaborators
PiNotation.piNotation.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Combinatorics.Matroid.Minor.Contract
Matroid.IsBasis'.contract_indep_sdiff_iff : ∀ {α : Type u_1} {M : Matroid α} {I J X : Set α}, M.IsBasis' I X → ((M.contract X).Indep (J \ X) ↔ M.Indep (J \ X ∪ I))
-- Mathlib.Data.Matrix.Diagonal
Matrix.transpose_natCast : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : AddMonoidWithOne α] (d : ℕ), (↑d).transpose = ↑d
-- Mathlib.Logic.Equiv.Defs
/-- Quotients are congruent on equivalences under equality of their relation.
An alternative is just to use rewriting with `eq`, but then computational proofs get stuck.  -/
Quotient.congrRight : {α : Sort u} → {r r' : Setoid α} → (∀ (a₁ a₂ : α), r a₁ a₂ ↔ r' a₁ a₂) → Quotient r ≃ Quotient r'
-- Mathlib.FieldTheory.RatFunc.IntermediateField
RatFunc.adjoin_X : ∀ {K : Type u_1} [inst : Field K], K⟮RatFunc.X⟯ = ⊤
-- Mathlib.NumberTheory.MulChar.Basic
/-- The inverse of a quadratic character is itself. →  -/
MulChar.IsQuadratic.inv : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommRing R'] {χ : MulChar R R'},
  χ.IsQuadratic → χ⁻¹ = χ
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Y : CategoryTheory.Over X),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv)
      (CategoryTheory.ChosenPullbacksAlong.snd Y.hom (CategoryTheory.CategoryStruct.id X)) =
    Y.hom
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
CoassocSimps.assoc_comp_map_comm_comp_comul_comp_comul : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : Coalgebra R M] (f : M →ₗ[R] N),
  ↑(TensorProduct.assoc R M M N) ∘ₗ
      TensorProduct.map (↑(TensorProduct.comm R M M) ∘ₗ CoalgebraStruct.comul) f ∘ₗ CoalgebraStruct.comul =
    TensorProduct.map LinearMap.id (TensorProduct.map LinearMap.id f ∘ₗ ↑(TensorProduct.comm R M M)) ∘ₗ
      ↑(TensorProduct.assoc R M M M) ∘ₗ
        TensorProduct.map CoalgebraStruct.comul LinearMap.id ∘ₗ ↑(TensorProduct.comm R M M) ∘ₗ CoalgebraStruct.comul
-- Mathlib.CategoryTheory.Functor.CurryingThree
CategoryTheory.Functor.currying₃_unitIso_inv_app_app_app_app : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_4} {E : Type u_9} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_4} C₃]
  [inst_3 : CategoryTheory.Category.{v_9, u_9} E]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ E))) (X₁ : C₁) (X₂ : C₂)
  (X₃ : C₃),
  (((CategoryTheory.Functor.currying₃.unitIso.inv.app F).app X₁).app X₂).app X₃ =
    CategoryTheory.CategoryStruct.id
      (((((CategoryTheory.Functor.currying₃.functor.comp CategoryTheory.Functor.currying₃.inverse).obj F).obj X₁).obj
            X₂).obj
        X₃)
-- Init.Data.List.Sublist
List.infix_iff_prefix_suffix : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <:+: l₂ ↔ ∃ t, l₁ <+: t ∧ t <:+ l₂
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_X_sub_C : ∀ {F : Type u} [inst : Field F] (x : F), (Polynomial.X - Polynomial.C x).natSepDegree = 1
-- Init.Data.Slice.Lemmas
Std.Slice.foldlM_toList : ∀ {γ : Type u} {α β : Type v} {m : Type u_1 → Type u_2} {δ : Type u_1} [inst : Monad m]
  [inst_1 : Std.ToIterator (Std.Slice γ) Id α β] [inst_2 : Std.Iterator α Id β] [inst_3 : Std.IteratorLoop α Id m]
  [Std.LawfulIteratorLoop α Id m] [Std.Iterators.Finite α Id] [LawfulMonad m] {s : Std.Slice γ} {init : δ}
  {f : δ → β → m δ}, List.foldlM f init s.toList = Std.Slice.foldlM f init s
-- Init.Data.Int.Lemmas
Int.mul_one : ∀ (a : ℤ), a * 1 = a
-- Init.Data.String.Pattern.Basic
String.Slice.Pattern.Internal.memcmpStr : (lhs rhs : String) →
  (lstart rstart len : String.Pos.Raw) →
    len.offsetBy lstart ≤ lhs.rawEndPos → len.offsetBy rstart ≤ rhs.rawEndPos → Bool
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.monadMap_StateT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ : Type u}
  {epost : EPred} (f : {β : Type u} → m β → m β) {α : Type u} (x : StateT σ m α) (post : α → σ → Pred),
  ⦃ fun s =>
    Std.Internal.Do.wp (f (x.run s))
      (fun x =>
        match x with
        | (a, s') => post a s')
      epost ⦄
    MonadFunctor.monadMap (fun {β} => f) x ⦃ post; epost ⦄
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey?_eq_some_getKey : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α} (h' : a ∈ t), t.getKey? a = some (t.getKey a h')
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.apply_lineMap : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} {P2 : Type u_5} [inst : Ring k]
  [inst_1 : AddCommGroup V1] [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2]
  [inst_5 : Module k V2] [inst_6 : AddTorsor V2 P2] (f : P1 →ᵃ[k] P2) (p₀ p₁ : P1) (c : k),
  f ((AffineMap.lineMap p₀ p₁) c) = (AffineMap.lineMap (f p₀) (f p₁)) c
-- Mathlib.Topology.MetricSpace.IsometricSMul
Prod.isIsometricSMul'' : ∀ {M : Type u} {N : Type u_2} [inst : Mul M] [inst_1 : PseudoEMetricSpace M] [IsIsometricSMul Mᵐᵒᵖ M] [inst_3 : Mul N]
  [inst_4 : PseudoEMetricSpace N] [IsIsometricSMul Nᵐᵒᵖ N], IsIsometricSMul (M × N)ᵐᵒᵖ (M × N)
-- Mathlib.Topology.PartitionOfUnity
/-- The collection of continuous functions underlying this partition of unity  -/
PartitionOfUnity.toFun : {ι : Type u_1} →
  {X : Type u_2} → [inst : TopologicalSpace X] → {s : optParam (Set X) Set.univ} → PartitionOfUnity ι X s → ι → C(X, ℝ)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Quotient
Submodule.liftQL_apply : ∀ {R : Type u_1} {R₂ : Type u_2} [inst : Ring R] [inst_1 : Ring R₂] {σ : R →+* R₂} {M : Type u_3} {M₂ : Type u_4}
  [inst_2 : TopologicalSpace M] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : TopologicalSpace M₂]
  [inst_6 : AddCommGroup M₂] [inst_7 : Module R₂ M₂] (S : Submodule R M) (f : M →SL[σ] M₂) (h : S ≤ (↑f).ker)
  (x : M ⧸ S), (S.liftQL f h) x = (S.liftQ (↑f) h) x
-- Init.Data.Vector.Range
Vector.range'_one : ∀ {s step : ℕ}, Vector.range' s 1 step = #v[s]
-- Mathlib.Analysis.InnerProductSpace.Subspace
OrthogonalFamily.orthonormal_sigma_orthonormal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {G : ι → Type u_5} [inst_3 : (i : ι) → NormedAddCommGroup (G i)]
  [inst_4 : (i : ι) → InnerProductSpace 𝕜 (G i)] {V : (i : ι) → G i →ₗᵢ[𝕜] E},
  OrthogonalFamily 𝕜 G V →
    ∀ {α : ι → Type u_6} {v_family : (i : ι) → α i → G i},
      (∀ (i : ι), Orthonormal 𝕜 (v_family i)) → Orthonormal 𝕜 fun a => (V a.fst) (v_family a.fst a.snd)
-- Mathlib.Computability.AkraBazzi.GrowsPolynomially
AkraBazziRecurrence.GrowsPolynomially.congr_of_eventuallyEq : ∀ {f g : ℝ → ℝ},
  f =ᶠ[Filter.atTop] g → AkraBazziRecurrence.GrowsPolynomially g → AkraBazziRecurrence.GrowsPolynomially f
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The height one prime spectrum of a Dedekind domain `R` is the type of nonzero prime ideals of
`R`. Note that this equals the maximal spectrum if `R` has Krull dimension 1.  -/
IsDedekindDomain.HeightOneSpectrum : (R : Type u_1) → [CommRing R] → Type u_1
-- Mathlib.Order.ModularLattice
strictMono_inf_prod_sup : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {z : α}, StrictMono fun x => (x ⊓ z, x ⊔ z)