mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Rcc.Internal.toList_eq_toList_iter : ∀ {α : Type u} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.Rxc.IsAlwaysFinite α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Rcc α},
  r.toList = (Std.Rcc.Internal.iter r).toList
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {k : α} {v : β}, Std.DHashMap.Const.get? (m.insert k v) k = some v
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
/-- A pair of roots which pair to `+3` are also sufficient to distinguish an embedded `𝔤₂`.  -/
RootPairing.EmbeddedG2.ofPairingInThree : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] →
                [inst_4 : Module R N] →
                  (P : RootPairing ι R M N) →
                    [CharZero R] →
                      [inst_6 : P.IsCrystallographic] →
                        [P.IsReduced] → (long short : ι) → P.pairingIn ℤ long short = 3 → P.EmbeddedG2
-- Mathlib.Topology.Compactness.Paracompact
/-- Every open cover of a paracompact space assumes a locally finite refinement.  -/
ParacompactSpace.locallyFinite_refinement : ∀ {X : Type v} {inst : TopologicalSpace X} [self : ParacompactSpace X] (α : Type v) (s : α → Set X),
  (∀ (a : α), IsOpen (s a)) →
    ⋃ a, s a = Set.univ →
      ∃ β t, (∀ (b : β), IsOpen (t b)) ∧ ⋃ b, t b = Set.univ ∧ LocallyFinite t ∧ ∀ (b : β), ∃ a, t b ⊆ s a
-- Init.Data.Nat.Lemmas
Nat.pred_one_add : ∀ (n : ℕ), (1 + n).pred = n
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.exact_iff_mono_fromOpcycles : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasHomology], S.Exact ↔ CategoryTheory.Mono S.fromOpcycles
-- Lean.Meta.Sym.AlphaShareCommon
_private.Lean.Meta.Sym.AlphaShareCommon.0.Lean.Meta.Sym.hashChild : Lean.Expr → UInt64
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Complex
Complex.cos_eq_cos_iff : ∀ {x y : ℂ}, Complex.cos x = Complex.cos y ↔ ∃ k, y = 2 * ↑k * ↑Real.pi + x ∨ y = 2 * ↑k * ↑Real.pi - x
-- Init.Data.Iterators.Combinators.Monadic.Attach
Std.Iterators.Types.Attach.mk : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        {P : β → Prop} →
          (inner : Std.IterM m β) →
            (∀ (out : β), inner.IsPlausibleIndirectOutput out → P out) → Std.Iterators.Types.Attach α m P
-- Init.Data.Bool
Bool.not' : Bool → Bool
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {f : Option β → Option β} {h : k ∈ Std.ExtDHashMap.Const.alter m k f},
  Std.ExtDHashMap.Const.get (Std.ExtDHashMap.Const.alter m k f) k h = (f (Std.ExtDHashMap.Const.get? m k)).get ⋯
-- Lean.Elab.DocString
/-- Resolves a name against `NameMap` that contains a list of builtin expanders, taking into account
open namespaces and the current namespace. This is needed because builtin doc roles/code
blocks/directives are not present in the environment when `Lean` is not imported, so standard name
resolution (`realizeGlobalConstNoOverload`) won't find them.

This is called as a fallback when the identifier can't be resolved.
 -/
_private.Lean.Elab.DocString.0.Lean.Doc.resolveBuiltinDocName : {α : Type} → Lean.NameMap α → Lean.Name → Lean.Elab.TermElabM (Option α)
-- Mathlib.GroupTheory.GroupAction.Defs
/-- The stabilizer of an element under an action, i.e. what sends the element to itself.
A subgroup.  -/
MulAction.stabilizer : (G : Type u_1) → {α : Type u_2} → [inst : Group G] → [MulAction G α] → α → Subgroup G
-- Mathlib.Combinatorics.Configuration
Configuration.ProjectivePlane.card_lines : ∀ (P : Type u_1) (L : Type u_2) [inst : Membership P L] [inst_1 : Configuration.ProjectivePlane P L] [Finite P]
  [inst_3 : Fintype L],
  Fintype.card L = Configuration.ProjectivePlane.order P L ^ 2 + Configuration.ProjectivePlane.order P L + 1
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.IsAffineOpen.fromSpec_preimage_zeroLocus : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} (hU : AlgebraicGeometry.IsAffineOpen U)
  (s : Set ↑(X.presheaf.obj (Opposite.op U))), ⇑hU.fromSpec ⁻¹' X.zeroLocus s = PrimeSpectrum.zeroLocus s
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.rootSpace.eq_1 : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] (χ : ↥H → R),
  LieAlgebra.rootSpace H χ = LieModule.genWeightSpace L χ
-- Mathlib.GroupTheory.GroupAction.Embedding
Function.Embedding.instAddAction.eq_1 : ∀ {G : Type u_1} {α : Type u_3} {β : Type u_4} [inst : AddGroup G] [inst_1 : AddAction G β],
  Function.Embedding.instAddAction = Function.Injective.addAction DFunLike.coe ⋯ ⋯
-- Mathlib.RingTheory.HopfAlgebra.MonoidAlgebra
MonoidAlgebra.instHopfAlgebra : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : Semiring A] →
        [HopfAlgebra R A] → {G : Type u_3} → [inst_3 : Group G] → HopfAlgebra R (MonoidAlgebra A G)
-- Mathlib.RingTheory.Valuation.ValuationSubring
ValuationSubring.mem_nonunits_iff_or : ∀ {K : Type u} [inst : Field K] (A : ValuationSubring K) {x : K}, x ∈ A.nonunits ↔ x = 0 ∨ x⁻¹ ∉ A
-- Init.Data.Nat.Div.Basic
Nat.modCore.go.eq_1 : ∀ (y : ℕ) (hy : 0 < y) (x fuel_2 : ℕ) (hfuel_2 : x < fuel_2.succ),
  Nat.modCore.go y hy fuel_2.succ x hfuel_2 = if h : y ≤ x then Nat.modCore.go y hy fuel_2 (x - y) ⋯ else x
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiffOn_infty : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F}, ContDiffOn 𝕜 (↑⊤) f s ↔ ∀ (n : ℕ), ContDiffOn 𝕜 (↑n) f s
-- Mathlib.RingTheory.Ideal.Span
Ideal.span_pair_comm : ∀ {α : Type u} [inst : Semiring α] {x y : α}, Ideal.span {x, y} = Ideal.span {y, x}
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulMonC.go.induct_unfolding : ∀ (k : ℤ) (m : Lean.Grind.CommRing.Mon) (c : ℕ) (motive : Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Prop),
  (∀ (k_1 : ℤ),
      have k := k * k_1 % ↑c;
      (k == 0) = true → motive (Lean.Grind.CommRing.Poly.num k_1) (Lean.Grind.CommRing.Poly.num 0)) →
    (∀ (k_1 : ℤ),
        have k := k * k_1 % ↑c;
        (k == 0) = false →
          motive (Lean.Grind.CommRing.Poly.num k_1)
            (Lean.Grind.CommRing.Poly.add k m (Lean.Grind.CommRing.Poly.num 0))) →
      (∀ (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
          have k_2 := k * k_1 % ↑c;
          (k_2 == 0) = true →
            motive p (Lean.Grind.CommRing.Poly.mulMonC.go k m c p) →
              motive (Lean.Grind.CommRing.Poly.add k_1 m_1 p) (Lean.Grind.CommRing.Poly.mulMonC.go k m c p)) →
        (∀ (k_1 : ℤ) (m_1 : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
            have k_2 := k * k_1 % ↑c;
            (k_2 == 0) = false →
              motive p (Lean.Grind.CommRing.Poly.mulMonC.go k m c p) →
                motive (Lean.Grind.CommRing.Poly.add k_1 m_1 p)
                  (Lean.Grind.CommRing.Poly.add k_2 (m.mul m_1) (Lean.Grind.CommRing.Poly.mulMonC.go k m c p))) →
          ∀ (a : Lean.Grind.CommRing.Poly), motive a (Lean.Grind.CommRing.Poly.mulMonC.go k m c a)
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- A class of morphisms `W` has the of-postcomp property w.r.t. `W'` if whenever
`g` is in `W'` and `f ≫ g` is in `W`, also `f` is in `W`.  -/
CategoryTheory.MorphismProperty.HasOfPostcompProperty : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C → Prop
-- Init.Data.String.Lemmas.IsEmpty
String.isEmpty_sliceFrom : ∀ {s : String} {p : s.Pos}, (s.sliceFrom p).isEmpty = true ↔ p = s.endPos
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.monomialToExpr : ℕ → Nat.Internal.Linear.Var → Nat.Internal.Linear.Expr
-- Init.Data.Array.Subarray
/-- Extracts an element from the subarray.

The index is relative to the start of the subarray, rather than the underlying array.
 -/
Subarray.get : {α : Type u_1} → (s : Subarray α) → Fin (Std.Slice.size s) → α
-- Batteries.Data.Nat.Lemmas
Nat.casesDiagOn_succ_zero : ∀ {motive : ℕ → ℕ → Sort u_1} (zero_zero : motive 0 0) (zero_succ : (n : ℕ) → motive 0 (n + 1))
  (succ_zero : (m : ℕ) → motive (m + 1) 0) (succ_succ : (m n : ℕ) → motive (m + 1) (n + 1)) (m : ℕ),
  Nat.casesDiagOn (m + 1) 0 zero_zero zero_succ succ_zero succ_succ = succ_zero m
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.one_apply_ne : ∀ {n : Type u_2} {A : Type u_5} [inst : DecidableEq n] [inst_1 : Zero A] [inst_2 : One A] {i j : n}, i ≠ j → 1 i j = 0
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
/-- The bundled additive monoid giving the filtered colimit of a diagram.  -/
AddMonCat.FilteredColimits.colimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    CategoryTheory.Functor J AddMonCat → [CategoryTheory.IsFiltered J] → AddMonCat
-- Mathlib.CategoryTheory.Shift.Pullback
CategoryTheory.pullbackShiftFunctorZero_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A : Type u_2} {B : Type u_3} [inst_1 : AddMonoid A]
  [inst_2 : AddMonoid B] [inst_3 : CategoryTheory.HasShift C B] (φ : A →+ B) (X : CategoryTheory.PullbackShift C φ),
  (CategoryTheory.shiftFunctorZero (CategoryTheory.PullbackShift C φ) A).hom.app X =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.pullbackShiftIso C φ 0 0 ⋯).hom.app X)
      ((CategoryTheory.shiftFunctorZero C B).hom.app X)
-- Mathlib.GroupTheory.GroupAction.ConjAct
MulAut.conjNormal_inv_apply : ∀ {G : Type u_3} [inst : Group G] {H : Subgroup G} [inst_1 : H.Normal] (g : G) (h : ↥H),
  ↑((MulAut.conjNormal g)⁻¹ h) = g⁻¹ * ↑h * g
-- Mathlib.MeasureTheory.Measure.Prokhorov
MeasureTheory.exists_measure_iUnion_gt_of_isCompact_closure : ∀ {𝓧 : Type u_1} {m𝓧 : MeasurableSpace 𝓧} [inst : PseudoMetricSpace 𝓧] [inst_1 : OpensMeasurableSpace 𝓧]
  [SecondCountableTopology 𝓧] {S : Set (MeasureTheory.ProbabilityMeasure 𝓧)} (U : ℕ → Set 𝓧),
  (∀ (i : ℕ), IsOpen (U i)) →
    ⋃ i, U i = Set.univ →
      IsCompact (closure S) → ∀ (ε : ENNReal), 0 < ε → ε ≤ 1 → ∃ k, ∀ μ ∈ S, 1 - ε < ↑(μ (⋃ i, ⋃ (_ : i ≤ k), U i))
-- Lean.Meta.Tactic.Grind.Anchor
Lean.Meta.Grind.ExprWithAnchor : Type
-- Lean.ExtraModUses
Lean.IndirectModUse.mk : String → Lean.Name → Lean.IndirectModUse
-- Mathlib.Dynamics.TopologicalEntropy.CoverEntropy
Dynamics.coverEntropyInfEntourage_empty : ∀ {X : Type u_1} {T : X → X} {U : SetRel X X}, Dynamics.coverEntropyInfEntourage T ∅ U = ⊥
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Power.denote.eq_1 : ∀ {α : Type u_1} [inst : Lean.Grind.Semiring α] (ctx : Lean.Grind.CommRing.Context α) (x_1 : Lean.Grind.CommRing.Var),
  Lean.Grind.CommRing.Power.denote ctx { x := x_1, k := 0 } = 1
-- Mathlib.Combinatorics.Matroid.Basic
/-- **Alias** of `Matroid.ExchangeProperty.encard_sdiff_eq`.

---

For any two sets `B₁`, `B₂` in a family with the exchange property, the differences `B₁ \ B₂`
and `B₂ \ B₁` have the same `ℕ∞`-cardinality.  -/
Matroid.ExchangeProperty.encard_diff_eq : ∀ {α : Type u_1} {IsBase : Set α → Prop} {B₁ B₂ : Set α},
  Matroid.ExchangeProperty IsBase → IsBase B₁ → IsBase B₂ → (B₁ \ B₂).encard = (B₂ \ B₁).encard
-- Mathlib.Tactic.Order
/-- `order_core` is an implementation detail of the `order` tactic. It proves the main goal,
which must be `⊢ False`, by deriving a contradiction from hypotheses which are formulas in the
language of orders.  -/
_private.Mathlib.Tactic.Order.0.Mathlib.Tactic.Order.order_core : Lean.ParserDescr
-- Lean.Data.Iterators.Producers.PersistentHashMap
/-- A frame of entries from a trie node.  -/
Lean.PersistentHashMap.Zipper.consEntries : {α : Type u} →
  {β : Type v} →
    Subarray (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)) →
      Lean.PersistentHashMap.Zipper α β → Lean.PersistentHashMap.Zipper α β
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instNegCoeOfNegMemClass : {ι : Type u_1} →
  (R : ι → Type u_2) →
    {𝓕 : Filter ι} →
      {S : ι → Type u_3} →
        [inst : (i : ι) → SetLike (S i) (R i)] →
          {B : (i : ι) → S i} →
            [inst_1 : (i : ι) → Neg (R i)] →
              [∀ (i : ι), NegMemClass (S i) (R i)] → Neg (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) 𝓕)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.instInhabited : {M : Type u_1} → [inst : Monoid M] → Inhabited (Associates M)
-- Mathlib.Data.Finset.Functor
Finset.map_comp_coe : ∀ {α β : Type u} (h : α → β), Functor.map h ∘ Multiset.toFinset = Multiset.toFinset ∘ Functor.map h
-- Mathlib.CategoryTheory.Sums.Associator
/-- Further characterizing the composition of the associator and the left inclusion.  -/
CategoryTheory.sum.inrCompInlCompAssociator : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (E : Type u₃) →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (CategoryTheory.Sum.inr_ C D).comp
                ((CategoryTheory.Sum.inl_ (C ⊕ D) E).comp (CategoryTheory.sum.associator C D E)) ≅
              (CategoryTheory.Sum.inl_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E))
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.limsup_add_of_right_tendsto_zero : ∀ {ι : Type u_4} {u : Filter ι} {g : ι → ENNReal},
  Filter.Tendsto g u (nhds 0) → ∀ (f : ι → ENNReal), Filter.limsup (f + g) u = Filter.limsup f u
-- Lean.DocString.Parser
/-- Match the character indicated, pushing nothing to the stack in case of success  -/
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.skipChFn : Char → Lean.Parser.ParserFn
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiChainComplexEquivalence_unitIso_hom_app_f_f : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (α : Type u_3)
  [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α]
  (P : CategoryTheory.Idempotents.Karoubi (HomologicalComplex C (ComplexShape.down α))) (n : α),
  ((CategoryTheory.Idempotents.karoubiChainComplexEquivalence C α).unitIso.hom.app P).f.f n = P.p.f n
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.instHasHomotopyCofiberOfHasBinaryBiproductXHAddOfNat : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_3}
  [inst_2 : AddRightCancelSemigroup ι] [inst_3 : One ι] {F G : CochainComplex C ι} (φ : F ⟶ G)
  [∀ (p : ι), CategoryTheory.Limits.HasBinaryBiproduct (F.X (p + 1)) (G.X p)], HomologicalComplex.HasHomotopyCofiber φ
-- Mathlib.Analysis.Asymptotics.TVS
/-- **Alias** of the forward direction of `Asymptotics.isThetaTVS_iff_isTheta`. -/
Asymptotics.IsThetaTVS.isTheta : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : SeminormedAddCommGroup F] [inst_3 : NormedSpace 𝕜 E]
  [inst_4 : NormedSpace 𝕜 F] {f : α → E} {g : α → F} {l : Filter α}, f =Θ[𝕜; l] g → f =Θ[l] g
-- Mathlib.Tactic.Determinant.Bird.Meta
/-- `Ring` evaluation cache for the scalar ring.  -/
Mathlib.Tactic.Determinant.Ctx.cα : {u : Lean.Level} →
  {α : Q(Type u)} →
    {rα : Q(CommRing «$α»)} →
      Mathlib.Tactic.Determinant.Ctx rα →
        Mathlib.Tactic.Ring.Common.Cache (Mathlib.Tactic.Determinant.commSemiringOfCommRing rα)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_union`.

---

The edist to a union is the minimum of the edists  -/
EMetric.infEdist_union : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {s t : Set α},
  Metric.infEDist x (s ∪ t) = min (Metric.infEDist x s) (Metric.infEDist x t)
-- Std.Async.Basic
Std.Async.Async.instMonadAwaitPromise : Std.Async.MonadAwait IO.Promise Std.Async.Async
-- Init.Grind.Module.Envelope
Lean.Grind.IntModule.OfNatModule.neg : {α : Type u} →
  [inst : Lean.Grind.NatModule α] → Lean.Grind.IntModule.OfNatModule.Q α → Lean.Grind.IntModule.OfNatModule.Q α
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.eTruncGEδLT_coe : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ), t.eTruncGEδLT.app (WithBotTop.coe n) = t.truncGEδLT n
-- Lean.Meta.Match.NamedPatterns
Lean.Meta.Match.mkNamedPattern : Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Tactic.Ring.RingNF
/-- Elaborator for the `ring_nf` tactic.  -/
Mathlib.Tactic.RingNF.elabRingNFConv : Lean.Elab.Tactic.Tactic
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.coe_prod : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] (s : Subsemigroup M) (t : Subsemigroup N),
  ↑(s.prod t) = ↑s ×ˢ ↑t
-- Mathlib.Analysis.Convex.StrictConvexSpace
/-- In a strictly convex space, two vectors `x`, `y` are not in the same ray if and only if the
triangle inequality for `x` and `y` is strict.  -/
not_sameRay_iff_norm_add_lt : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [StrictConvexSpace ℝ E] {x y : E},
  ¬SameRay ℝ x y ↔ ‖x + y‖ < ‖x‖ + ‖y‖
-- Mathlib.Topology.Category.TopCat.Limits.Pullbacks
TopCat.pullbackIsoProdSubtype_inv_fst_apply : ∀ {X Y Z : TopCat} (f : X ⟶ Z) (g : Y ⟶ Z)
  (x : { p // (CategoryTheory.ConcreteCategory.hom f) p.1 = (CategoryTheory.ConcreteCategory.hom g) p.2 }),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.pullback.fst f g))
      ((CategoryTheory.ConcreteCategory.hom (TopCat.pullbackIsoProdSubtype f g).inv) x) =
    (↑x).1
-- Mathlib.Algebra.Category.Grp.FilteredColimits
GrpCat.FilteredColimits.colimit_mul_mk_eq' : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J GrpCat) {j : J} (x y : ↑(F.obj j)),
  GrpCat.FilteredColimits.G.mk F ⟨j, x⟩ * GrpCat.FilteredColimits.G.mk F ⟨j, y⟩ =
    GrpCat.FilteredColimits.G.mk F ⟨j, x * y⟩
-- Mathlib.CategoryTheory.Enriched.Basic
/-- The `A`-graded transformation from `F` to `G`  -/
CategoryTheory.GradedNatTrans.app : {V : Type v} →
  [inst : CategoryTheory.Category.{w, v} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₁} →
        [inst_2 : CategoryTheory.EnrichedCategory V C] →
          {D : Type u₂} →
            [inst_3 : CategoryTheory.EnrichedCategory V D] →
              {A : CategoryTheory.Center V} →
                {F G : CategoryTheory.EnrichedFunctor V C D} →
                  CategoryTheory.GradedNatTrans A F G → (X : C) → A.fst ⟶ F.obj X ⟶[V] G.obj X
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.jacobiMatrix.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.PreSubmersivePresentation R S ι σ) [inst_3 : Fintype σ] [inst_4 : DecidableEq σ],
  P.jacobiMatrix = (LinearMap.toMatrix P.basis P.basis) P.differential
-- Mathlib.LinearAlgebra.Matrix.Hermitian
/-- A diagonal matrix is Hermitian if the entries are self-adjoint (as a vector)  -/
Matrix.isHermitian_diagonal_of_self_adjoint : ∀ {α : Type u_1} {n : Type u_4} [inst : AddMonoid α] [inst_1 : StarAddMonoid α] [inst_2 : DecidableEq n] (v : n → α),
  IsSelfAdjoint v → (Matrix.diagonal v).IsHermitian
-- Mathlib.Data.Finset.Density
Finset.dens_eq_one : ∀ {α : Type u_2} [inst : Fintype α] {s : Finset α} [Nonempty α], s.dens = 1 ↔ s = Finset.univ
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.comp_id : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ]
  (f : 𝒜 →ₐᵍ[R] ℬ), f.comp (GradedAlgHom.id R 𝒜) = f
-- Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas
_private.Mathlib.LinearAlgebra.RootSystem.Finite.Lemmas.0.RootPairing.termΦ : Lean.ParserDescr
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Bounded.Receiver.mk.inj : ∀ {α : Type} {state : Std.Mutex (Std.Bounded.State✝ α)} {id : ℕ} {state_1 : Std.Mutex (Std.Bounded.State✝ α)}
  {id_1 : ℕ}, { state := state, id := id } = { state := state_1, id := id_1 } → state = state_1 ∧ id = id_1
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- The graded tensor product of two elements of graded rings.  -/
GradedTensorProduct.tmul : (R : Type u_1) →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      {𝒜 : ι → Submodule R A} →
                        {ℬ : ι → Submodule R B} →
                          [inst_7 : GradedAlgebra 𝒜] → [inst_8 : GradedAlgebra ℬ] → A → B → GradedTensorProduct R 𝒜 ℬ
-- Mathlib.Data.List.Forall2
List.sublistForall₂_map_right_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {R : α → β → Prop} {f : γ → β} {l₁ : List α} {l₂ : List γ},
  List.SublistForall₂ R l₁ (List.map f l₂) ↔ List.SublistForall₂ (fun a c => R a (f c)) l₁ l₂
-- Init.Data.Vector.Count
Vector.countP.eq_1 : ∀ {α : Type u_1} {n : ℕ} (p : α → Bool) (xs : Vector α n), Vector.countP p xs = Array.countP p xs.toArray
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction.go.eq_def : ∀ (pat : ByteArray) (stackPos : ℕ) (hst : stackPos < pat.size) (k : ℕ),
  String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction.go✝ pat stackPos hst k =
    if h : String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat pat k (stackPos + 1) then k
    else
      have this := ⋯;
      String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction.go✝ pat stackPos hst (k - 1)
-- Mathlib.Algebra.Notation.Defs
dite_mul : ∀ {α : Type u_2} (P : Prop) [inst : Decidable P] [inst_1 : Mul α] (a : P → α) (b : ¬P → α) (c : α),
  (if h : P then a h else b h) * c = if h : P then a h * c else b h * c
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Equiv.getKeyGE!_eq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyGE! k = t₂.getKeyGE! k
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get_eq_get : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [inst : LawfulBEq α] {a : α}
  {h : a ∈ m}, Std.DHashMap.Const.get m a h = m.get a h
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mem_mker : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {F : Type u_4}
  [inst_2 : FunLike F M N] [mc : AddMonoidHomClass F M N] {f : F} {x : M}, x ∈ AddMonoidHom.mker f ↔ f x = 0
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imIₗ_apply : ∀ {R : Type u_3} (c₁ c₂ c₃ : R) [inst : CommRing R] (self : QuaternionAlgebra R c₁ c₂ c₃),
  (QuaternionAlgebra.imIₗ c₁ c₂ c₃) self = self.imI
-- Mathlib.Computability.Partrec
Partrec.none : ∀ {α : Type u_1} {σ : Type u_3} [inst : Primcodable α] [inst_1 : Primcodable σ], Partrec fun x => Part.none