mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.Horn
SSet.horn.edge₃_coe_down : ∀ (n : ℕ) (i a b : Fin (n + 1)) (hab : a ≤ b) (H : 3 ≤ n),
  (↑(SSet.horn.edge₃ n i a b hab H)).down = SimplexCategory.Hom.mk { toFun := ![a, b], monotone' := ⋯ }
-- Mathlib.Order.Interval.Set.Fin
Fin.image_castAdd_Iio : ∀ {n : ℕ} (m : ℕ) (i : Fin n), Fin.castAdd m '' Set.Iio i = Set.Iio (Fin.castAdd m i)
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_mul : ∀ {M : Type u_1} [inst : TopologicalSpace M] [inst_1 : Mul M] [inst_2 : ContinuousMul M] (a b : M),
  SeparationQuotient.mk (a * b) = SeparationQuotient.mk a * SeparationQuotient.mk b
-- Mathlib.Topology.Constructions
Continuous.quotient_liftOn' : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Setoid X} {f : X → Y},
  Continuous f → ∀ (hs : ∀ (a b : X), s a b → f a = f b), Continuous fun x => x.liftOn' f hs
-- Mathlib.SetTheory.Ordinal.Veblen
/-- For any given `x`, there exists a unique pair `(o, a)` such that `ω ^ x = veblen o a` and
`a < ω ^ x`. `invVeblen₁ x` and `invVeblen₂ x` return the first and second entries of this pair,
respectively. See `veblen_eq_opow_iff` for a proof.

Composing this function with `Ordinal.CNF` yields a predicative ordinal notation up to `Γ₀`.  -/
Ordinal.invVeblen₂ : Ordinal.{u_1} → Ordinal.{u_1}
-- Plausible.Testable
Plausible.instPrintableProp : {p : Prop} → Plausible.PrintableProp p
-- Mathlib.GroupTheory.Index
Subgroup.card_map_dvd : ∀ {G : Type u_1} {G' : Type u_2} [inst : Group G] [inst_1 : Group G'] (H : Subgroup G) (f : G →* G'),
  Nat.card ↥(Subgroup.map f H) ∣ Nat.card ↥H
-- Mathlib.FieldTheory.Minpoly.MinpolyDiv
natDegree_minpolyDiv_succ : ∀ {R : Type u_2} {S : Type u_1} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {x : S},
  IsIntegral R x → ∀ [Nontrivial S], (minpolyDiv R x).natDegree + 1 = (minpoly R x).natDegree
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → k ∉ t₁ ∩ t₂
-- Mathlib.Analysis.BoundedVariation
LocallyBoundedVariationOn.bilinear_comp : ∀ {α : Type u_2} [inst : LinearOrder α] {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedAddCommGroup G]
  [inst_6 : NormedSpace ℝ G] {s : Set α} {f : α → E} {g : α → F},
  LocallyBoundedVariationOn f s →
    LocallyBoundedVariationOn g s → ∀ (B : E →L[ℝ] F →L[ℝ] G), LocallyBoundedVariationOn (fun x => (B (f x)) (g x)) s
-- Mathlib.Algebra.Group.EvenFunction
/-- Any constant function is even.  -/
Function.Even.const : ∀ {α : Type u_1} {β : Type u_2} [inst : Neg α] (b : β), Function.Even fun x => b
-- Mathlib.Data.FunLike.Equiv
/-- This is not an instance to avoid slowing down every single `Subsingleton` typeclass search.  -/
EquivLike.subsingleton_dom : ∀ {E : Sort u_1} {α : Sort u_3} {β : Sort u_4} [EquivLike E α β] [Subsingleton α], Subsingleton E
-- Mathlib.Data.Nat.BitIndices
Nat.bitIndices_two_mul : ∀ (n : ℕ), (2 * n).bitIndices = List.map (fun x => x + 1) n.bitIndices
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.castNum.match_1.splitter : (motive : Num → Sort u_1) → (x : Num) → (Unit → motive Num.zero) → ((p : PosNum) → motive (Num.pos p)) → motive x
-- Lean.Util.Diff
Lean.Diff.instReprAction.repr : Lean.Diff.Action → ℕ → Std.Format
-- Lean.Data.Lsp.Capabilities
/-- The resource operations the client supports. Clients should at least support 'create', 'rename' and 'delete' files and folders.  -/
Lean.Lsp.WorkspaceEditClientCapabilities.resourceOperations? : Lean.Lsp.WorkspaceEditClientCapabilities → Option (Array String)
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.fromArrowArrowFunctor_obj_f₃₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow (CategoryTheory.Arrow C)),
  (CategoryTheory.Square.fromArrowArrowFunctor.obj f).f₃₄ = CategoryTheory.Arrow.Hom.right f.hom
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
intEquivOfZMultiplesEqTop_symm_apply_zsmul : ∀ {G : Type u_2} [inst : Infinite G] [inst_1 : AddGroup G] {g : G} (hg : AddSubgroup.zmultiples g = ⊤) (k : ℤ),
  (intEquivOfZMultiplesEqTop g hg).symm (k • g) = k
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanIndex.ι_fstSigmaMap : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  (I : CategoryTheory.Limits.MultispanIndex J C) [inst_1 : CategoryTheory.Limits.HasCoproduct I.left]
  [inst_2 : CategoryTheory.Limits.HasCoproduct I.right] (b : J.L),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι I.left b) I.fstSigmaMap =
    CategoryTheory.CategoryStruct.comp (I.fst b) (CategoryTheory.Limits.Sigma.ι I.right (J.fst b))
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.eq_rpow_inv_iff : ∀ {x y : NNReal} {z : ℝ}, z ≠ 0 → (x = y ^ z⁻¹ ↔ x ^ z = y)
-- Mathlib.CategoryTheory.Bicategory.Opposites
/-- Type synonym for 2-morphisms in the opposite bicategory.  -/
Bicategory.Opposite.Hom2 : {B : Type u} → [inst : CategoryTheory.Bicategory B] → {a b : Bᵒᵖ} → (a ⟶ b) → (a ⟶ b) → Type w
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.coeff_zero_mul_X : ∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R), (PowerSeries.coeff 0) (φ * PowerSeries.X) = 0
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.MatcherInfo.getFirstDiscrPos : Lean.Meta.MatcherInfo → ℕ
-- Mathlib.Logic.Equiv.PartialEquiv
/-- Postcompose a partial equivalence with an equivalence.
We modify the source and target to have better definitional behavior.  -/
PartialEquiv.transEquiv : {α : Type u_1} → {β : Type u_2} → {γ : Type u_3} → PartialEquiv α β → β ≃ γ → PartialEquiv α γ
-- Mathlib.LinearAlgebra.BilinearForm.DualLattice
LinearMap.BilinForm.dualSubmoduleToDual.congr_simp : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : Field S] [inst_2 : AddCommGroup M]
  [inst_3 : Algebra R S] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (B : LinearMap.BilinForm S M) [inst_7 : IsDomain R] [inst_8 : Module.IsTorsionFree R S] (N : Submodule R M),
  B.dualSubmoduleToDual N = B.dualSubmoduleToDual N
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.prodAdditive_apply : ∀ (G : Type u_2) (H : Type u_3) [inst : Mul G] [inst_1 : Mul H] (x : Additive (G × H)),
  (AddEquiv.prodAdditive G H) x = (Additive.ofMul (Additive.toMul x).1, Additive.ofMul (Additive.toMul x).2)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
/-- Two measures which are finite on closed intervals are equal if they agree on all
closed intervals.  -/
MeasureTheory.Measure.ext_of_Icc' : ∀ {α : Type u_5} [inst : TopologicalSpace α] {m : MeasurableSpace α} [SecondCountableTopology α]
  [inst_2 : LinearOrder α] [OrderTopology α] [BorelSpace α] (μ ν : MeasureTheory.Measure α),
  (∀ ⦃a b : α⦄, a ≤ b → μ (Set.Icc a b) ≠ ⊤) → (∀ ⦃a b : α⦄, a ≤ b → μ (Set.Icc a b) = ν (Set.Icc a b)) → μ = ν
-- Init.Data.Rat.Basic
/-- Construct a normalized `Rat` from a numerator and nonzero denominator.
This is a "smart constructor" that divides the numerator and denominator by
the gcd to ensure that the resulting rational number is normalized.
 -/
Rat.normalize : ℤ → (den : optParam ℕ 1) → autoParam (den ≠ 0) Rat.normalize._auto_1 → ℚ
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.linearEquiv_apply : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] {S : Type u_3}
  [inst_2 : Ring S] [inst_3 : Module R S] (v : Valuation S Γ₀) (x : WithVal v), (WithVal.linearEquiv R v) x = x.ofVal
-- Mathlib.Data.W.Constructions
/-- `WType.Natα` is equivalent to `PUnit ⊕ PUnit`.
This is useful when considering the associated polynomial endofunctor.
 -/
WType.NatαEquivPUnitSumPUnit : WType.Natα ≃ PUnit.{u + 1} ⊕ PUnit.{u_1 + 1}
-- Mathlib.RepresentationTheory.Coinduced
Rep.resCoindHomEquiv_symm_apply : ∀ {k : Type u} {G : Type v} {H : Type w} [inst : CommRing k] [inst_1 : Monoid G] [inst_2 : Monoid H] (φ : G →* H)
  (B : Rep.{max w t, u, w} k H) (A : Rep.{max w t, u, v} k G) (f : B ⟶ Rep.coind.{u, v, w, max t w} φ A),
  (Rep.resCoindHomEquiv.{t, u, v, w} φ B A).symm f =
    Rep.ofHom
      { toLinearMap := LinearMap.proj 1 ∘ₗ (Representation.coindV φ A.ρ).subtype ∘ₗ (Rep.Hom.hom f).toLinearMap,
        isIntertwining' := ⋯ }
-- Init.Grind.AC
Lean.Grind.AC.Seq.cons : Lean.Grind.AC.Var → Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.trans_id : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  (𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X)
  [inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀] [inst_1 : 𝒰.LocallyDirected] (i : 𝒰.I₀),
  𝒰.trans (CategoryTheory.CategoryStruct.id i) = CategoryTheory.CategoryStruct.id (𝒰.X i)
-- Lean.Widget.InteractiveDiagnostic
Lean.Widget.instInhabitedMsgEmbed.default : Lean.Widget.MsgEmbed
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_of_mul_le_of_one_le_right : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulRightMono α] {a b c : α}, a * b ≤ c → 1 ≤ a → b ≤ c
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromConst
seminormFromConst_isNonarchimedean : ∀ {R : Type u_1} [inst : CommRing R] {c : R} {f : RingSeminorm R},
  f 1 ≤ 1 → f c ≠ 0 → IsPowMul ⇑f → IsNonarchimedean ⇑f → IsNonarchimedean (seminormFromConst' c f)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.WidePushoutShape.Hom.id : {J : Type w} → (X : CategoryTheory.Limits.WidePushoutShape J) → X.Hom X
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Turn an element of a type `F` satisfying `MulDistribMulActionHomClass F M X Y` into an actual
`MulDistribMulActionHom`. This is declared as the default coercion from `F` to
`MulDistribMulActionHom M X Y`.  -/
MulDistribMulActionSemiHomClass.toMulDistribMulActionHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {A : Type u_4} →
            [inst_2 : Monoid A] →
              [inst_3 : MulDistribMulAction M A] →
                {B : Type u_5} →
                  [inst_4 : Monoid B] →
                    [inst_5 : MulDistribMulAction N B] →
                      {F : Type u_10} →
                        [inst_6 : FunLike F A B] → [MulDistribMulActionSemiHomClass F (⇑φ) A B] → F → A →ₑ*[φ] B
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonCompletionList.toJson : Lean.Lsp.CompletionList → Lean.Json
-- Mathlib.Algebra.Group.Shrink
Shrink.instOne.eq_1 : ∀ {α : Type u_2} [inst : Small.{v, u_2} α] [inst_1 : One α], Shrink.instOne = (equivShrink α).symm.one
-- Mathlib.Order.SuccPred.Basic
WithTop.pred_untop : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderTop α] [inst_2 : PredOrder α] (a : WithTop α) (ha : a ≠ ⊤),
  Order.pred (a.untop ha) = (Order.pred a).untop ⋯
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.comp_apply : ∀ {M N O : SemiNormedGrp} (f : M ⟶ N) (g : N ⟶ O) (r : M.carrier),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) r =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) r)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.quot_liftOn_mk : ∀ {α : Type u} {L : List (α × Bool)} (β : Type v) (f : List (α × Bool) → β)
  (H : ∀ (L₁ L₂ : List (α × Bool)), FreeGroup.Red.Step L₁ L₂ → f L₁ = f L₂), Quot.liftOn (FreeGroup.mk L) f H = f L
-- Mathlib.CategoryTheory.Limits.WeakLimits.Basic
CategoryTheory.Limits.IsWeakLimit.liftConeMorphism_hom : ∀ {J : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} J] {C : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_3, u_3} C] {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cone F}
  (h : CategoryTheory.Limits.IsWeakLimit t) (s : CategoryTheory.Limits.Cone F), (h.liftConeMorphism s).hom = h.lift s
-- Init.Data.String.Lemmas.Pattern.Char
String.Slice.Pattern.Model.Char.isLongestRevMatchAt_iff_isLongestRevMatchAt_beq : ∀ {c : Char} {s : String.Slice} {pos pos' : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatchAt c pos pos' ↔
    String.Slice.Pattern.Model.IsLongestRevMatchAt (fun x => x == c) pos pos'
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.completedHurwitzZetaOdd_neg : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedHurwitzZetaOdd (-a) s = -HurwitzZeta.completedHurwitzZetaOdd a s
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_get?_eq_contains : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a : α}, (t.get? a).isSome = t.contains a
-- Mathlib.Data.PFunctor.Multivariate.Basic
MvPFunctor.mk : {n : ℕ} → (A : Type u) → (A → TypeVec.{u} n) → MvPFunctor.{u} n
-- Mathlib.Analysis.Normed.Group.Constructions
Multiplicative.normedGroup : {E : Type u_2} → [NormedAddGroup E] → NormedGroup (Multiplicative E)
-- Mathlib.Order.SuccPred.IntervalSucc
/-- If `α` is a linear pred order, `β` is a preorder, and `f : α → β` is a monotone function, then
the intervals `Set.Ioc (f Order.pred n) (f n)` are pairwise disjoint.  -/
Monotone.pairwise_disjoint_on_Ioc_pred : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : PredOrder α] [inst_2 : Preorder β] {f : α → β},
  Monotone f → Pairwise (Function.onFun Disjoint fun n => Set.Ioc (f (Order.pred n)) (f n))
-- Init.Data.SInt.Bitwise
ISize.toBitVec_shiftLeft : ∀ (a b : ISize), (a <<< b).toBitVec = a.toBitVec <<< b.toBitVec.smod ↑System.Platform.numBits
-- Mathlib.RingTheory.IdealFilter.Basic
IdealFilter.IsGabriel.mk : ∀ {A : Type u_1} [inst : Ring A] {F : IdealFilter A} [toIsUniform : F.IsUniform],
  (∀ (I : Ideal A), (∃ J ∈ F, ∀ x ∈ J, Submodule.colon I {x} ∈ F) → I ∈ F) → F.IsGabriel
-- Mathlib.Order.CompleteLattice.Basic
iInf_top : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α], ⨅ x, ⊤ = ⊤
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.count_span_normalizedFactors_eq_of_normUnit`. -/
count_span_normalizedFactors_eq_of_normUnit : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R]
  [inst_3 : NormalizationMonoid R] [inst_4 : DecidableEq R] {r X : R},
  r ≠ 0 →
    normUnit X = 1 →
      Prime X →
        Multiset.count (Ideal.span {X}) (UniqueFactorizationMonoid.normalizedFactors (Ideal.span {r})) =
          Multiset.count X (UniqueFactorizationMonoid.normalizedFactors r)
-- Mathlib.Order.MinMax
le_of_le_min_right : ∀ {α : Type u} [inst : LinearOrder α] {a b c : α}, c ≤ min a b → c ≤ b
-- Mathlib.Algebra.Category.Ring.Basic
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
SemiRingCat.Hom.Simps.hom : (R S : SemiRingCat) → R.Hom S → ↑R →+* ↑S
-- Mathlib.Algebra.Homology.Embedding.TruncGE
ComplexShape.Embedding.truncGE'Functor_map : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') [inst : e.IsTruncGE]
  (C : Type u_4) [inst_1 : CategoryTheory.Category.{v_2, u_4} C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.CategoryWithHomology C] {X Y : HomologicalComplex C c'} (φ : X ⟶ Y),
  (e.truncGE'Functor C).map φ = HomologicalComplex.truncGE'Map φ e
-- Mathlib.Order.Category.BoolAlg
BoolAlg.hom_ext : ∀ {X Y : BoolAlg} {f g : X ⟶ Y}, BoolAlg.Hom.hom f = BoolAlg.Hom.hom g → f = g
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.any_toList : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α]
  {p : (a : α) → β a → Bool}, m.WF → (m.toList.any fun x => p x.fst x.snd) = m.any p
-- Mathlib.CategoryTheory.Monad.Products
CategoryTheory.overToCoalgebra_obj_A : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C) [inst_1 : CategoryTheory.Limits.HasBinaryProducts C]
  (f : CategoryTheory.Over X), ((CategoryTheory.overToCoalgebra X).obj f).A = f.left
-- Mathlib.RingTheory.DedekindDomain.Different
coeSubmodule_differentIdeal_fractionRing : ∀ (A : Type u_1) (B : Type u_3) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] [inst_3 : IsDomain A]
  [IsIntegrallyClosed A] [inst_5 : IsDedekindDomain B] [inst_6 : Module.IsTorsionFree A B] [Algebra.IsIntegral A B]
  [Algebra.IsSeparable (FractionRing A) (FractionRing B)] [FiniteDimensional (FractionRing A) (FractionRing B)],
  IsLocalization.coeSubmodule (FractionRing B) (differentIdeal A B) = 1 / Submodule.traceDual A (FractionRing A) 1
-- Mathlib.Analysis.Convex.EGauge
egauge_ball_one_le_of_one_lt_norm : ∀ {𝕜 : Type u_1} [inst : NormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E]
  {c : 𝕜}, 1 < ‖c‖ → ∀ (x : E), egauge 𝕜 (Metric.ball 0 1) x ≤ ‖c‖ₑ * ‖x‖ₑ
-- Mathlib.RingTheory.Coalgebra.MulOpposite
MulOpposite.counit_def : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A], CoalgebraStruct.counit = CoalgebraStruct.counit ∘ₗ ↑(MulOpposite.opLinearEquiv R).symm
-- Mathlib.RepresentationTheory.Basic
Representation.trivial_apply : ∀ (k : Type u_1) {G : Type u_2} {V : Type u_3} [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (g : G) (v : V), ((Representation.trivial k G V) g) v = v
-- Mathlib.Computability.RegularExpressions
/-- This is the definition of regular expressions. The names used here are meant to mirror the
[definition of a Kleene algebra](https://en.wikipedia.org/wiki/Kleene_algebra).
* `0` (`zero`) matches nothing
* `1` (`epsilon`) matches only the empty string
* `char a` matches only the string 'a'
* `star P` matches any finite concatenation of strings that match `P`
* `P + Q` (`plus P Q`) matches anything that matches `P` or `Q`
* `P * Q` (`comp P Q`) matches `x ++ y` if `x` matches `P` and `y` matches `Q`
 -/
RegularExpression : Type u → Type u
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.π_map_assoc : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{u, u, u} k H}
  {B : Rep.{u, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B) (n : ℕ) {Z : ModuleCat k} (h : groupCohomology B n ⟶ Z),
  CategoryTheory.CategoryStruct.comp (groupCohomology.π A n)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.map f φ n) h) =
    CategoryTheory.CategoryStruct.comp (groupCohomology.cocyclesMap f φ n)
      (CategoryTheory.CategoryStruct.comp (groupCohomology.π B n) h)
-- Mathlib.Order.Interval.Finset.Defs
/-- The finset $[a, ∞)$ of elements `x` such that `a ≤ x`. Basically `Set.Ici a` as a finset.  -/
Finset.Ici : {α : Type u_1} → [inst : Preorder α] → [LocallyFiniteOrderTop α] → α → Finset α
-- Mathlib.CategoryTheory.Monoidal.Internal.Module
/-- Converting a bundled algebra to a monoid object in `ModuleCat R`.
 -/
ModuleCat.MonModuleEquivalenceAlgebra.inverseObj : {R : Type u} → [inst : CommRing R] → (A : AlgCat R) → CategoryTheory.MonObj (ModuleCat.of R ↑A)
-- Init.Data.UInt.Lemmas
UInt64.sub_neg : ∀ {a b : UInt64}, a - -b = a + b
-- Mathlib.Data.Finset.Density
Finset.dens_singleton : ∀ {α : Type u_2} [inst : Fintype α] (a : α), {a}.dens = (↑(Fintype.card α))⁻¹
-- Init.Data.Vector.Count
Vector.countP_append : ∀ {α : Type u_1} {p : α → Bool} {n m : ℕ} {xs : Vector α n} {ys : Vector α m},
  Vector.countP p (xs ++ ys) = Vector.countP p xs + Vector.countP p ys
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.presheafIso_hom_app_hom_apply : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} [inst_2 : G.IsCoverDense K] [inst_3 : G.IsLocallyFull K]
  {ℱ ℱ' : CategoryTheory.Sheaf K (Type v)} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) (X : Dᵒᵖ)
  (x : ℱ.obj.obj (Opposite.op (Opposite.unop X))),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.Functor.IsCoverDense.Types.presheafIso i).hom.app X)) x =
    ⋯.amalgamate
      (fun x_1 x_2 hf =>
        (CategoryTheory.ConcreteCategory.hom (ℱ'.obj.map (Nonempty.some hf).lift.op))
          ((CategoryTheory.ConcreteCategory.hom (i.hom.app (Opposite.op (Nonempty.some hf).1)))
            ((CategoryTheory.ConcreteCategory.hom (ℱ.obj.map (Nonempty.some hf).map.op)) x)))
      ⋯
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
/-- If matrix A is left invertible, then its inverse equals its left inverse.  -/
Matrix.inv_eq_left_inv : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] {A B : Matrix n n α},
  B * A = 1 → A⁻¹ = B
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The cone `Pi.cone X` is a limit cone.  -/
CategoryTheory.Limits.productIsProduct' : {α : Type w₂} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C) →
        [inst_1 : CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] →
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.Pi.cone X)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.foldM_eq_match_step : ∀ {α β : Type w} {γ : Type x} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] {m : Type x → Type x'}
  [inst_2 : Monad m] [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m]
  {f : γ → β → m γ} {init : γ} {it : Std.Iter β},
  Std.Iter.foldM f init it =
    match it.step with
    | ⟨Std.IterStep.yield it' out, property⟩ => do
      let __do_lift ← f init out
      Std.Iter.foldM f __do_lift it'
    | ⟨Std.IterStep.skip it', property⟩ => Std.Iter.foldM f init it'
    | ⟨Std.IterStep.done, property⟩ => pure init
-- Std.Data.ExtHashMap.Basic
Std.ExtHashMap.mk.inj : ∀ {α : Type u} {β : Type v} {inst : BEq α} {inst_1 : Hashable α} {inner inner_1 : Std.ExtDHashMap α fun x => β},
  { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiff_pi_space : ∀ {𝕜 : 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] {n : WithTop ℕ∞} {ι : Type u_16} [inst_6 : Fintype ι]
  {Fi : ι → Type u_17} [inst_7 : (i : ι) → NormedAddCommGroup (Fi i)] [inst_8 : (i : ι) → NormedSpace 𝕜 (Fi i)]
  {φ : M → (i : ι) → Fi i},
  ContMDiff I (modelWithCornersSelf 𝕜 ((i : ι) → Fi i)) n φ ↔
    ∀ (i : ι), ContMDiff I (modelWithCornersSelf 𝕜 (Fi i)) n fun x => φ x i
-- Init.Data.String.Lemmas.Splits
String.Pos.Splits.exists_eq_append_singleton : ∀ {t₁ t₂ s : String} {p : s.Pos} (hp : p ≠ s.endPos),
  (p.next hp).Splits t₁ t₂ → ∃ t₁', t₁ = t₁' ++ String.singleton (p.get hp)
-- Mathlib.Data.Set.Basic
Set.Subset.trans : ∀ {α : Type u} {a b c : Set α}, a ⊆ b → b ⊆ c → a ⊆ c
-- Mathlib.Algebra.Homology.DerivedCategory.Plus
CochainComplex.truncGE.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K K_1 : CochainComplex C ℤ) (e_K : K = K_1) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n n_1 : ℤ), n = n_1 → K.truncGE n = K_1.truncGE n_1
-- Init.Data.Int.Order
Int.natAbs_neg : ∀ (a : ℤ), (-a).natAbs = a.natAbs
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
/-- The modification between the underlying strong transformations of oplax functors  -/
CategoryTheory.Oplax.StrongTrans.Modification.toOplax : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} →
          {η θ : F ⟶ G} →
            CategoryTheory.Oplax.StrongTrans.Modification η θ →
              (CategoryTheory.Oplax.StrongTrans.toOplax η).Modification (CategoryTheory.Oplax.StrongTrans.toOplax θ)
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_single_mul_of_forall_mul_ne : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {m m' : M} [inst_1 : Mul M] (r : R) (x : MonoidAlgebra R M),
  (∀ (d : M), m * d ≠ m') → (MonoidAlgebra.single m r * x).coeff m' = 0