mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.prod_ite_eq : ∀ {α : Type u_1} {M : Type u_8} {N : Type u_10} [inst : Zero M] [inst_1 : CommMonoid N] [inst_2 : DecidableEq α]
  (f : α →₀ M) (a : α) (b : α → M → N),
  (f.prod fun x v => if a = x then b x v else 1) = if a ∈ f.support then b a (f a) else 1
-- Mathlib.GroupTheory.Finiteness
/-- The product of two finitely generated submonoids is finitely generated.  -/
Submonoid.FG.prod : ∀ {M : Type u_1} {N : Type u_2} [inst : Monoid M] [inst_1 : Monoid N] {P : Submonoid M} {Q : Submonoid N},
  P.FG → Q.FG → (P.prod Q).FG
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.mem_inv' : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : InvolutiveInv α] {s : Finset α} {a : α}, a ∈ s⁻¹ ↔ a⁻¹ ∈ s
-- Mathlib.LinearAlgebra.Determinant
LinearMap.detAux_def : ∀ {M : Type u_7} [inst : AddCommGroup M] {ι : Type u_8} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι] {A : Type u_9}
  [inst_3 : CommRing A] [inst_4 : Module A M],
  LinearMap.detAux = Trunc.lift (fun b => Matrix.detMonoidHom.comp ↑(LinearMap.toMatrixAlgEquiv b)) ⋯
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.instDecidableEq : (p : ENNReal) → (V : Type u_4) → [DecidableEq V] → DecidableEq (WithLp p V)
-- Lean.EnvExtension
Lean.mkStateFromImportedEntries : {α σ : Type} → (σ → α → σ) → σ → Array (Array α) → σ
-- Mathlib.Topology.Category.CompHausLike.Basic
CompHausLike.coe_of : ∀ (P : TopCat → Prop) (X : Type u) [inst : TopologicalSpace X] [inst_1 : CompactSpace X] [inst_2 : T2Space X]
  [inst_3 : CompHausLike.HasProp P X], ↑(CompHausLike.of P X).toTop = X
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.F₄_off_diag_nonpos : ∀ (i j : Fin 4), i ≠ j → CartanMatrix.F₄ i j ≤ 0
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.subst.sizeOf_spec : ∀ (x : Int.Internal.Linear.Var) (c₁ : Lean.Meta.Grind.Arith.Cutsat.EqCnstr)
  (c₂ : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.subst x c₁ c₂) = 1 + sizeOf x + sizeOf c₁ + sizeOf c₂
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.subset_disjointOfDiff : ∀ {α : Type u_1} {C : Set (Set α)} {s t : Set α} (hC : MeasureTheory.IsSetSemiring C) (hs : s ∈ C) (ht : t ∈ C),
  ↑(hC.disjointOfDiff hs ht) ⊆ C
-- Mathlib.RingTheory.Etale.Kaehler
/-- (Implementation)
If `J ≃ Q ⊗ₚ I` (e.g. when `T = Q ⊗ₚ S` and `P → Q` is flat), then `T ⊗ₛ I/I² ≃ J/J²`.
This is the inverse.  -/
Algebra.Extension.tensorCotangentInvFun : {R : Type u_1} →
  {S : Type u_2} →
    {T : Type u_3} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : CommRing T] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra R T] →
                [inst_5 : Algebra S T] →
                  {P : Algebra.Extension R S} →
                    {Q : Algebra.Extension R T} →
                      (f : P.Hom Q) →
                        [alg : Algebra P.Ring Q.Ring] →
                          (halg : algebraMap P.Ring Q.Ring = f.toRingHom) →
                            Function.Bijective ⇑(LinearMap.liftBaseChange Q.Ring (f.mapKer halg)) →
                              Q.Cotangent →+ TensorProduct S T P.Cotangent
-- Mathlib.Data.SubtypeNeLift
Function.subtypeNeLift.congr_simp : ∀ {ι : Type u_1} {inst : DecidableEq ι} [inst_1 : DecidableEq ι] {M : ι → Type u_2} (i₀ : ι)
  (f f_1 : (j : { i // i ≠ i₀ }) → M ↑j),
  f = f_1 → ∀ (x x_1 : M i₀), x = x_1 → ∀ (i : ι), Function.subtypeNeLift i₀ f x i = Function.subtypeNeLift i₀ f_1 x_1 i
-- Mathlib.RingTheory.Unramified.LocalRing
Localization.localRingHom_injective_of_primesOver_eq_singleton : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R}
  [inst_3 : p.IsPrime] {q : Ideal S} [inst_4 : q.IsPrime] (hq : p.primesOver S = {q}) [Algebra.IsIntegral R S]
  [FaithfulSMul R S], Function.Injective ⇑(Localization.localRingHom p q (algebraMap R S) ⋯)
-- Init.Data.Nat.Basic
Nat.add_one_le_iff : ∀ {n m : ℕ}, n + 1 ≤ m ↔ n < m
-- Mathlib.Data.Holor
/-- Two holors are equal if all their slices are equal.  -/
Holor.slice_eq : ∀ {α : Type} {d : ℕ} {ds : List ℕ} (x y : Holor α (d :: ds)), x.slice = y.slice → x = y
-- Mathlib.Algebra.Order.Hom.Monoid
OrderAddMonoidHom.zero_apply : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : AddZeroClass α]
  [inst_3 : AddZeroClass β] (a : α), 0 a = 0
-- Mathlib.Algebra.LieRinehartAlgebra.Subalgebra
LieRinehartSubalgebra.instAddSubgroupClass : ∀ (A : Type u_1) (L : Type u_2) [inst : CommRing A] [inst_1 : LieRing L] [inst_2 : Module A L],
  AddSubgroupClass (LieRinehartSubalgebra A L) L
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.iteratedSliceForward_forget : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} (f : CategoryTheory.Over X),
  f.iteratedSliceForward.comp (CategoryTheory.Over.forget f.left) =
    (CategoryTheory.Over.forget f).comp (CategoryTheory.Over.forget X)
-- Mathlib.Data.Part
Part.map_get : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) (o : Part α) (a : o.Dom), (Part.map f o).get a = (f ∘ o.get) a
-- Lean.MonadEnv
Lean.getConstInfoRec : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → [Lean.MonadError m] → Lean.Name → m Lean.RecursorVal
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_opow_omega0 : ∀ {a : Ordinal.{u_1}}, 1 < a → (a ^ Ordinal.omega0).card = max Cardinal.aleph0 a.card
-- Mathlib.Algebra.Notation.Indicator
Set.indicator_empty : ∀ {α : Type u_1} {M : Type u_3} [inst : Zero M] (f : α → M), ∅.indicator f = fun x => 0
-- Mathlib.Probability.Kernel.MeasurableIntegral
ProbabilityTheory.measurableSet_integrable : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  {E : Type u_4} [inst : NormedAddCommGroup E] ⦃f : β → E⦄,
  MeasureTheory.StronglyMeasurable f → MeasurableSet {a | MeasureTheory.Integrable f (κ a)}
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.union.eq_1 : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m₁ m₂ : Std.ExtHashMap α β), m₁.union m₂ = { inner := m₁.inner.union m₂.inner }
-- Mathlib.Order.KrullDimension
Order.krullDimLE_iff : ∀ (n : ℕ) (α : Type u_1) [inst : Preorder α], Order.KrullDimLE n α ↔ Order.krullDim α ≤ ↑n
-- Mathlib.Data.Sign.Basic
/-- We can decompose a sum of absolute value `n` into a sum of `n` signs.  -/
exists_signed_sum : ∀ {α : Type u} [inst : DecidableEq α] (s : Finset α) (f : α → ℤ),
  ∃ β x sgn g,
    (∀ (b : β), g b ∈ s) ∧
      Fintype.card β = ∑ a ∈ s, (f a).natAbs ∧ ∀ a ∈ s, (∑ b, if g b = a then ↑(sgn b) else 0) = f a
-- Mathlib.CategoryTheory.Limits.Cones
/-- A cone extended by an isomorphism is isomorphic to the original cone.  -/
CategoryTheory.Limits.Cone.extendIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F : CategoryTheory.Functor J C} →
          (s : CategoryTheory.Limits.Cone F) → {X : C} → (f : s.pt ≅ X) → s ≅ s.extend f.inv
-- Mathlib.Computability.Partrec
Computable.fin_app : ∀ {σ : Type u_4} [inst : Primcodable σ] {n : ℕ}, Computable₂ id
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.lakeAdd : Lean.Environment → Lean.ConstantInfo → Lean.Environment
-- Mathlib.MeasureTheory.Measure.Decomposition.Lebesgue
MeasureTheory.Measure.absolutelyContinuous_withDensity_rnDeriv_swap : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [ν.HaveLebesgueDecomposition μ],
  (ν.withDensity (μ.rnDeriv ν)).AbsolutelyContinuous (μ.withDensity (ν.rnDeriv μ))
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertManyIfNew_eq_foldl_impl : ∀ {α : Type u} {β : α → Type v} {x : Ord α} {t₁ : Std.DTreeMap.Internal.Impl α β} (h₁ : t₁.Balanced)
  {t₂ : Std.DTreeMap.Internal.Impl α β},
  ↑(t₁.insertManyIfNew t₂ h₁) =
    Std.DTreeMap.Internal.Impl.foldl (fun acc k v => Std.DTreeMap.Internal.Impl.insertIfNew! k v acc) t₁ t₂
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.liftWith_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} → StateT σ m β → m (β × σ)) → m α) (post : α → σ → Pred),
  ⦃ fun s => Std.Internal.Do.wp (f fun {β} x => x.run s) (fun a => post a s) epost ⦄ MonadControl.liftWith f ⦃ post;
    epost ⦄
-- Mathlib.Analysis.Calculus.Deriv.Basic
deriv_id' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜], deriv id = fun x => 1
-- Mathlib.MeasureTheory.Measure.AEMeasurable
aemeasurable_iUnion_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {f : α → β}
  {μ : MeasureTheory.Measure α} [Countable ι] {s : ι → Set α},
  AEMeasurable f (μ.restrict (⋃ i, s i)) ↔ ∀ (i : ι), AEMeasurable f (μ.restrict (s i))
-- Mathlib.Topology.Algebra.Module.Multilinear.Basic
ContinuousMultilinearMap.mk : {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₂] →
                      (toMultilinearMap : MultilinearMap R M₁ M₂) →
                        Continuous toMultilinearMap.toFun → ContinuousMultilinearMap R M₁ M₂
-- Mathlib.FieldTheory.Galois.Basic
/-- The Galois correspondence as a `GaloisInsertion`.  -/
IsGalois.galoisInsertionIntermediateFieldSubgroup : {F : Type u_1} →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] →
        [inst_2 : Algebra F E] →
          [FiniteDimensional F E] →
            GaloisInsertion (⇑OrderDual.toDual ∘ IntermediateField.fixingSubgroup)
              (IntermediateField.fixedField ∘ ⇑OrderDual.toDual)
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- The family of 2-morphisms out of an absolute left Kan extension.  -/
CategoryTheory.Bicategory.LeftExtension.IsAbsKan.desc : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} →
        {g : a ⟶ c} →
          {t : CategoryTheory.Bicategory.LeftExtension f g} →
            t.IsAbsKan →
              {x : B} →
                {h : c ⟶ x} →
                  (s : CategoryTheory.Bicategory.LeftExtension f (CategoryTheory.CategoryStruct.comp g h)) →
                    CategoryTheory.CategoryStruct.comp t.extension h ⟶ s.extension
-- Init.Prelude
/-- Alias for `Or.inl`.  -/
Or.intro_left : ∀ {a : Prop} (b : Prop), a → a ∨ b
-- Mathlib.Logic.Equiv.Option
Equiv.removeNone_none : ∀ {α : Type u_1} {β : Type u_2} (e : Option α ≃ Option β) {x : α}, e (some x) = none → some (e.removeNone x) = e none
-- Mathlib.Order.SymmDiff
symmDiff_sdiff_right : ∀ {α : Type u_2} [inst : GeneralizedBooleanAlgebra α] (a b : α), symmDiff a b \ b = a \ b
-- Mathlib.Analysis.Normed.Module.Bases
/-- The projections start at `0`.  -/
SchauderBasis.RankOneDecomposition.proj_zero : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (self : SchauderBasis.RankOneDecomposition 𝕜 X), self.P 0 = 0
-- Init.Data.List.Lemmas
List.eraseDupsBy_cons : ∀ {α : Type u_1} {a : α} {as : List α} {r : α → α → Bool},
  List.eraseDupsBy r (a :: as) = a :: List.eraseDupsBy r (List.filter (fun b => decide (r b a = false)) as)
-- Mathlib.Analysis.Normed.Field.Basic
/-- An injective non-unital ring homomorphism from a `Field` to a `NormedRing` induces a
`NormedField` structure on the domain.

See note [reducible non-instances]  -/
NormedField.induced : {F : Type u_5} →
  (R : Type u_6) →
    (S : Type u_7) →
      [inst : FunLike F R S] →
        [inst_1 : Field R] →
          [inst_2 : NormedField S] → [NonUnitalRingHomClass F R S] → (f : F) → Function.Injective ⇑f → NormedField R
-- Mathlib.Geometry.Euclidean.Projection
/-- The distance between `p₁` and the reflection of `p₂` equals that
between the reflection of `p₁` and `p₂`.  -/
EuclideanGeometry.dist_reflection : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] (s : AffineSubspace 𝕜 P)
  [inst_5 : Nonempty ↥s] [inst_6 : s.direction.HasOrthogonalProjection] (p₁ p₂ : P),
  dist p₁ ((EuclideanGeometry.reflection s) p₂) = dist ((EuclideanGeometry.reflection s) p₁) p₂
-- Mathlib.Data.Set.Basic
Set.decidableSetOf : {α : Type u} → (a : α) → (p : α → Prop) → [Decidable (p a)] → Decidable (a ∈ {a | p a})
-- Mathlib.SetTheory.Cardinal.Aleph
/-- `ℵ₁` is the first uncountable cardinal. 

Conventions for notations in identifiers:

 * The recommended spelling of `ℵ₁` in identifiers is `aleph_one`. -/
Cardinal.termℵ₁ : Lean.ParserDescr
-- Mathlib.Order.Filter.IsBounded
Filter.isCobounded_bot : ∀ {α : Type u_1} {r : α → α → Prop}, Filter.IsCobounded r ⊥ ↔ ∃ b, ∀ (x : α), r b x
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instNonAssocRingOfRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → NonAssocRing (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), RingHomClass (T h) (G i) (G j)] → NonAssocRing (DirectLimit G f)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.rightUnitor_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasTerminal C]
  [inst_2 : CategoryTheory.Limits.HasBinaryProducts C] (f : X ⟶ Y) {Z : C} (h : Y ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f (CategoryTheory.CategoryStruct.id (⊤_ C)))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor Y).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.rightUnitor X).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Analysis.Normed.Group.Constructions
norm_prod_le_iff : ∀ {E : Type u_2} {F : Type u_3} [inst : Norm E] [inst_1 : Norm F] {x : E × F} {r : ℝ}, ‖x‖ ≤ r ↔ ‖x.1‖ ≤ r ∧ ‖x.2‖ ≤ r
-- Mathlib.Data.DFinsupp.Defs
/-- `DFinsupp.erase` as an `AddMonoidHom`.  -/
DFinsupp.eraseAddHom : {ι : Type u} →
  (β : ι → Type v) → [DecidableEq ι] → [inst : (i : ι) → AddZeroClass (β i)] → ι → (Π₀ (i : ι), β i) →+ Π₀ (i : ι), β i
-- Mathlib.Analysis.Meromorphic.LogDeriv
/-- Eta-expanded form of `Meromorphic.logDeriv_zpow_eventuallyEq`

---

Away from a codiscrete subset of `𝕜`, the logarithmic derivative of the `n`-th power of a
meromorphic function is `n` times the logarithmic derivative.
 -/
Meromorphic.logDeriv_fun_zpow_eventuallyEq : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {𝕜' : Type u_2} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {f : 𝕜 → 𝕜'},
  Meromorphic f → ∀ (n : ℤ), (logDeriv fun i => f i ^ n) =ᶠ[Filter.codiscrete 𝕜] fun i => n • logDeriv f i
-- Mathlib.CategoryTheory.Sites.Coherent.LocallySurjective
CategoryTheory.extensiveTopology.presheafIsLocallySurjective_iff : ∀ {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] {FD : D → D → Type u_3} {CD : D → Type w}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  [inst_4 : CategoryTheory.FinitaryPreExtensive C] {F G : CategoryTheory.Functor Cᵒᵖ D} (f : F ⟶ G)
  [CategoryTheory.Limits.PreservesFiniteProducts F] [CategoryTheory.Limits.PreservesFiniteProducts G]
  [CategoryTheory.Limits.PreservesFiniteProducts (CategoryTheory.forget D)],
  CategoryTheory.Presheaf.IsLocallySurjective (CategoryTheory.extensiveTopology C) f ↔
    ∀ (X : C), Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X)))
-- Mathlib.RepresentationTheory.Coinduced
Rep.resCoindToHom.eq_1 : ∀ {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 u_1 w, u, w} k H) (A : Rep.{max u_1 w, u, v} k G) (f : Rep.res φ B ⟶ A),
  Rep.resCoindToHom φ B A f =
    Rep.ofHom
      {
        toLinearMap :=
          LinearMap.codRestrict (Representation.coindV φ A.ρ)
            (LinearMap.pi fun h => (Rep.Hom.hom f).toLinearMap ∘ₗ B.ρ h) ⋯,
        isIntertwining' := ⋯ }
-- Mathlib.Order.CountableSupClosed
countableSupClosed_preimage_toDual : ∀ {α : Type u_2} [inst : LE α] {s : Set αᵒᵈ}, CountableSupClosed (⇑OrderDual.toDual ⁻¹' s) ↔ CountableInfClosed s
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- The functor from light condensed sets to topological spaces lands in sequential spaces.  -/
LightCondSet.lightCondSetToSequential : CategoryTheory.Functor LightCondSet Sequential
-- Mathlib.Algebra.Group.Basic
mul_right_comm : ∀ {G : Type u_3} [inst : CommSemigroup G] (a b c : G), a * b * c = a * c * b
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.instToJsonInitializeParams : Lean.ToJson Lean.Lsp.InitializeParams
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.cliqueFree_of_chromaticNumber_lt : ∀ {V : Type u} {G : SimpleGraph V} {n : ℕ}, G.chromaticNumber < ↑n → G.CliqueFree n
-- Mathlib.RingTheory.WittVector.Truncated
WittVector.truncateFun_zero : ∀ (p n : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)], WittVector.truncateFun n 0 = 0
-- Mathlib.MeasureTheory.Constructions.Pi
/-- The measurable equiv `(α₁ → β₁) ≃ᵐ (α₂ → β₂)` induced by `α₁ ≃ α₂` and `β₁ ≃ᵐ β₂` is
measure preserving.  -/
MeasureTheory.measurePreserving_arrowCongr' : ∀ {α₁ : Type u_4} {β₁ : Type u_5} {α₂ : Type u_6} {β₂ : Type u_7} [inst : Fintype α₁] [inst_1 : Fintype α₂]
  [inst_2 : MeasurableSpace β₁] [inst_3 : MeasurableSpace β₂] (μ : α₁ → MeasureTheory.Measure β₁)
  (ν : α₂ → MeasureTheory.Measure β₂) [∀ (i : α₂), MeasureTheory.SigmaFinite (ν i)] (eα : α₁ ≃ α₂) (eβ : β₁ ≃ᵐ β₂),
  (∀ (i : α₁), MeasureTheory.MeasurePreserving (⇑eβ) (μ i) (ν (eα i))) →
    MeasureTheory.MeasurePreserving (⇑(MeasurableEquiv.arrowCongr' eα eβ)) (MeasureTheory.Measure.pi fun i => μ i)
      (MeasureTheory.Measure.pi fun i => ν i)
-- Lean.Server.FileWorker.SignatureHelp
/-- Cursor is in the position of the argument to a function that already has other arguments applied
to it. High precedence.
 -/
Lean.Server.FileWorker.SignatureHelp.CandidateKind.appArg : Lean.Server.FileWorker.SignatureHelp.CandidateKind
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.dist_eq_iSup : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → Dist (α i)] (f g : PiLp ⊤ α),
  dist f g = ⨆ i, dist (f.ofLp i) (g.ofLp i)
-- Mathlib.Order.Fin.Tuple
Relator.LiftFun.eq_1 : ∀ {α : Sort u₁} {β : Sort u₂} {γ : Sort v₁} {δ : Sort v₂} (R : α → β → Prop) (S : γ → δ → Prop) (f : α → γ) (g : β → δ),
  Relator.LiftFun R S f g = ∀ ⦃a : α⦄ ⦃b : β⦄, R a b → S (f a) (g b)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.kernel_map_comp_kernelSubobjectIso_inv_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {f : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasKernel f] {X' Y' : C} {f' : X' ⟶ Y'}
  [inst_3 : CategoryTheory.Limits.HasKernel f'] (sq : CategoryTheory.Arrow.mk f ⟶ CategoryTheory.Arrow.mk f') {Z : C}
  (h : CategoryTheory.Subobject.underlying.obj (CategoryTheory.Limits.kernelSubobject f') ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.map f f' sq.left sq.right ⋯)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f').inv h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectIso f).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernelSubobjectMap sq) h)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.ω₂_div_two_notMem_lattice : ∀ (L : PeriodPair), L.ω₂ / 2 ∉ L.lattice
-- Batteries.Data.Nat.Basic
Nat.strongRec.eq_def : ∀ {motive : ℕ → Sort u_1} (ind : (n : ℕ) → ((m : ℕ) → m < n → motive m) → motive n) (t : ℕ),
  Nat.strongRec ind t = ind t fun m x => Nat.strongRec ind m
-- Mathlib.Analysis.Analytic.Basic
HasFPowerSeriesWithinAt.eq_1 : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (p : FormalMultilinearSeries 𝕜 E F) (s : Set E) (x : E),
  HasFPowerSeriesWithinAt f p s x = ∃ r, HasFPowerSeriesWithinOnBall f p s x r
-- Mathlib.Topology.Sets.CompactOpenCovered
/-- If `U` is compact-open covered and the `X i` have a basis of compact opens,
`U` can be written as the union of images of elements of the basis.  -/
IsCompactOpenCovered.exists_mem_of_isBasis : ∀ {S : Type u_1} {ι : Type u_2} {X : ι → Type u_3} {f : (i : ι) → X i → S} [inst : (i : ι) → TopologicalSpace (X i)]
  {B : (i : ι) → Set (TopologicalSpace.Opens (X i))},
  (∀ (i : ι), TopologicalSpace.Opens.IsBasis (B i)) →
    (∀ (i : ι), ∀ U ∈ B i, IsCompact U.carrier) →
      ∀ {U : Set S}, IsCompactOpenCovered f U → ∃ n a V, (∀ (i : Fin n), V i ∈ B (a i)) ∧ ⋃ i, f (a i) '' ↑(V i) = U
-- Mathlib.Algebra.Group.Defs
MulOne.ext_iff : ∀ {M : Type u_2} {x y : MulOne M}, x = y ↔ One.one = One.one ∧ Mul.mul = Mul.mul
-- Mathlib.Combinatorics.Additive.DoublingConst
/-- Dense sets have small difference constant.  -/
Finset.subConst_le_inv_dens : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {A B : Finset G} [inst_2 : Fintype G],
  A.subConst B ≤ A.dens⁻¹
-- Init.Data.List.Erase
_private.Init.Data.List.Erase.0.List.eraseIdx.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → ℕ → Sort u_2) (x : ℕ) (h_1 : (x : ℕ) → motive [] x)
  (h_2 : (head : α) → (as : List α) → motive (head :: as) 0)
  (h_3 : (a : α) → (as : List α) → (n : ℕ) → motive (a :: as) n.succ),
  (match [], x with
    | [], x => h_1 x
    | head :: as, 0 => h_2 head as
    | a :: as, n.succ => h_3 a as n) =
    h_1 x
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.continuous_map₂ : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  (pkg' : AbstractCompletion.{u_2, uβ} β) {γ : Type uγ} [inst_2 : UniformSpace γ]
  (pkg'' : AbstractCompletion.{vγ, uγ} γ) {δ : Type u_1} [inst_3 : TopologicalSpace δ] {f : α → β → γ}
  {a : δ → pkg.space} {b : δ → pkg'.space},
  Continuous a → Continuous b → Continuous fun d => pkg.map₂ pkg' pkg'' f (a d) (b d)
-- Batteries.Data.MLList.Basic
/-- Enumerate the elements of a monadic lazy list, starting at a specified offset.  -/
MLList.enumFrom : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → ℕ → MLList m α → MLList m (ℕ × α)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
/-- The integral of a polynomial of degree `< 2 * n` with respect to the weight function
`√(1 - x ^ 2)⁻¹` supported on `[-1, 1]` is equal to `π` times the average of its values
on the points `cos ((2 * i + 1) / (2 * n) * π)` for `0 ≤ i < n`.  -/
Polynomial.Chebyshev.integral_eq_sumZeroes : ∀ {n : ℕ} {P : Polynomial ℝ},
  n ≠ 0 →
    P.degree < 2 * ↑n →
      ∫ (x : ℝ), Polynomial.eval x P ∂Polynomial.Chebyshev.measureT = Polynomial.Chebyshev.sumZeroes n P
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.sumElim_onFunction : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} (ϕ : L →ᴸ L') {L'' : FirstOrder.Language} (ψ : L'' →ᴸ L')
  (_n : ℕ) (a : L.Functions _n ⊕ L''.Functions _n),
  (ϕ.sumElim ψ).onFunction a = Sum.elim (fun f => ϕ.onFunction f) (fun f => ψ.onFunction f) a
-- Mathlib.Algebra.Module.Submodule.LinearMap
Module.End.submodule_pow_eq_zero_of_pow_eq_zero : ∀ {R : Type u_1} {M : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Submodule R M}
  {g : Module.End R ↥N} {G : Module.End R M}, G ∘ₗ N.subtype = N.subtype ∘ₗ g → ∀ {k : ℕ}, G ^ k = 0 → g ^ k = 0