mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Filter.AtTopBot.Archimedean
atTop_hasAntitoneBasis_of_archimedean : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [IsOrderedRing R] [Archimedean R],
  Filter.atTop.HasAntitoneBasis fun n => Set.Ici ↑n
-- Mathlib.Analysis.InnerProductSpace.NormDet
LinearMap.normDet.congr_simp : ∀ {𝕜 : Type u_1} {U : Type u_2} {V : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup U]
  [inst_2 : InnerProductSpace 𝕜 U] [inst_3 : FiniteDimensional 𝕜 U] [inst_4 : NormedAddCommGroup V]
  [inst_5 : InnerProductSpace 𝕜 V] (f f_1 : U →ₗ[𝕜] V), f = f_1 → f.normDet = f_1.normDet
-- Mathlib.Data.ENNReal.Basic
ENNReal.instIsOrderedRing : IsOrderedRing ENNReal
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_smul_vectorMeasure : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G} (f : X → E) (c : ℝ),
  ∫ᵛ (x : X), f x ∂[B; c • μ] = c • ∫ᵛ (x : X), f x ∂[B; μ]
-- Mathlib.Computability.Primrec.List
/-- Checking if any element of a list satisfies a decidable predicate is primitive recursive.  -/
PrimrecPred.exists_mem_list : ∀ {α : Type u_1} {p : α → Prop} [inst : Primcodable α], PrimrecPred p → PrimrecPred fun L => ∃ a ∈ L, p a
-- Lean.MetavarContext
/-- Low level API for adding/declaring universe level metavariable declarations.
It is used to implement actions in the monads `MetaM`, `ElabM` and `TacticM`.
It should not be used directly since the argument `(mvarId : MVarId)` is assumed to be "unique".  -/
Lean.MetavarContext.addLevelMVarDecl : Lean.MetavarContext → Lean.LMVarId → Lean.MetavarContext
-- Mathlib.Analysis.Convex.Combination
Finset.centerMass_congr_weights : ∀ {R : Type u_1} {E : Type u_3} {ι : Type u_5} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  {t : Finset ι} {w : ι → R} {z : ι → E} {w' : ι → R}, (∀ i ∈ t, w i = w' i) → t.centerMass w z = t.centerMass w' z
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.inter_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {t₃ : Std.TreeMap.Raw α β cmp}, t₁.WF → t₂.WF → t₃.WF → t₂.Equiv t₃ → (t₁ ∩ t₂).Equiv (t₁ ∩ t₃)
-- Mathlib.Algebra.Divisibility.Basic
dvd_mul_of_dvd_right : ∀ {α : Type u_1} [inst : CommSemigroup α] {a b : α}, a ∣ b → ∀ (c : α), a ∣ c * b
-- Batteries.Data.Fin.Coding
Fin.decodeFun_encodeFun : ∀ {m n : ℕ} (x : Fin m → Fin n), Fin.decodeFun (Fin.encodeFun x) = x
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.shape_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  (S : J.Cover X) (I : S.Relation), S.shape.snd I = I.snd
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.Scheme.coprodPresheafObjIso_hom_snd_assoc : ∀ {X Y : AlgebraicGeometry.Scheme} (U : (X ⨿ Y).Opens) {Z : CommRingCat}
  (h : Y.presheaf.obj (Opposite.op ((TopologicalSpace.Opens.map CategoryTheory.Limits.coprod.inr.base).obj U)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.coprodPresheafObjIso U).hom
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.prod.snd h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.app CategoryTheory.Limits.coprod.inr U) h
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.map_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] (g : β → γ) (f : MeasureTheory.SimpleFunc α β)
  (a : α), (MeasureTheory.SimpleFunc.map g f) a = g (f a)
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.algebraMvPolynomial : {σ : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] → [Algebra R A] → Algebra (MvPolynomial σ R) (MvPowerSeries σ A)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instAddActionOfAddActionHomClass.eq_1 : ∀ {R : Type u_1} {ι : 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 ι] [inst_4 : AddMonoid R]
  [inst_5 : (i : ι) → AddAction R (G i)] [inst_6 : ∀ (i j : ι) (h : i ≤ j), AddActionHomClass (T h) R (G i) (G j)],
  DirectLimit.instAddActionOfAddActionHomClass = { toVAdd := DirectLimit.instVAdd, add_vadd := ⋯, zero_vadd := ⋯ }
-- Init.Data.Nat.Lemmas
Nat.mul_left_cancel : ∀ {n m k : ℕ}, 0 < n → n * m = n * k → m = k
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.mem_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α}, k ∈ t.insertManyIfNewUnit l ↔ k ∈ t ∨ l.contains k = true
-- Mathlib.CategoryTheory.Limits.Creates
/-- `F` creates colimits of shape `J` if `F` creates the colimit of any diagram
`K : J ⥤ C`.
 -/
CategoryTheory.CreatesColimitsOfShape : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [CategoryTheory.Category.{w', w} J] →
            CategoryTheory.Functor C D → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w) w')
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable.0.EisensteinSeries.aux_tendsto_tsum : ∀ (z : UpperHalfPlane),
  Filter.Tendsto (fun n => 2 / ↑z * ∑' (m : ℕ+), (1 / (-↑n / ↑z - ↑↑m) + 1 / (-↑n / ↑z + ↑↑m))) Filter.atTop
    (nhds (-2 * ↑Real.pi * Complex.I / ↑z))
-- Mathlib.Order.UpperLower.Prod
LowerSet.Iic_prod : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (x : α × β),
  LowerSet.Iic x = LowerSet.Iic x.1 ×ˢ LowerSet.Iic x.2
-- Mathlib.LinearAlgebra.Complex.Module
selfAdjoint.imaginaryPart_coe : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  {x : ↥(selfAdjoint A)}, imaginaryPart ↑x = 0
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Icc_Icc_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α},
  Filter.TendstoIxxClass Set.Icc (Filter.principal (Set.Icc a b)) (Filter.principal (Set.Icc a b))
-- Mathlib.Data.Nat.BinaryRec
Nat.bit_ne_zero_iff : ∀ {n : ℕ} {b : Bool}, Nat.bit b n ≠ 0 ↔ n = 0 → b = true
-- Mathlib.ModelTheory.ElementaryMaps
/-- Bundles an embedding satisfying the Tarski-Vaught test as an elementary embedding.  -/
FirstOrder.Language.Embedding.toElementaryEmbedding : {L : FirstOrder.Language} →
  {M : Type u_1} →
    {N : Type u_2} →
      [inst : L.Structure M] →
        [inst_1 : L.Structure N] →
          (f : L.Embedding M N) →
            (∀ (n : ℕ) (φ : L.BoundedFormula Empty (n + 1)) (x : Fin n → M) (a : N),
                φ.Realize default (Fin.snoc (⇑f ∘ x) a) → ∃ b, φ.Realize default (Fin.snoc (⇑f ∘ x) (f b))) →
              L.ElementaryEmbedding M N
-- Mathlib.Combinatorics.Additive.AP.Three.Defs
threeAPFree_singleton : ∀ {α : Type u_2} [inst : AddMonoid α] (a : α), ThreeAPFree {a}
-- Mathlib.Analysis.SpecialFunctions.Log.NegMulLog
Real.negMulLog_nonneg : ∀ {x : ℝ}, 0 ≤ x → x ≤ 1 → 0 ≤ x.negMulLog
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instSetLike.eq_1 : ∀ {G : Type u} [inst : AddGroup G] [inst_1 : TopologicalSpace G],
  OpenNormalAddSubgroup.instSetLike = { coe := fun U => ↑U.toOpenAddSubgroup, coe_injective := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_blockDiagonal : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {o : Type u_3}
  [inst_3 : Fintype o] [inst_4 : DecidableEq o] (M : o → Matrix n n R), (Matrix.blockDiagonal M).det = ∏ k, (M k).det
-- Mathlib.MeasureTheory.Integral.IntegralEqImproper
MeasureTheory.AECover.ae_eventually_mem : ∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι} {φ : ι → Set α},
  MeasureTheory.AECover μ l φ → ∀ᵐ (x : α) ∂μ, ∀ᶠ (i : ι) in l, x ∈ φ i
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.parseFractionNum : ℕ → ℕ → Std.Internal.Parsec.String.Parser ℕ
-- Mathlib.LinearAlgebra.Contraction
homTensorHomEquiv.eq_1 : ∀ (R : Type u_2) (M : Type u_3) (N : Type u_4) (P : Type u_5) (Q : Type u_6) [inst : CommSemiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : AddCommMonoid Q]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R P] [inst_8 : Module R Q]
  [inst_9 : Module.Projective R M] [inst_10 : Module.Finite R M] [inst_11 : Module.Projective R N]
  [inst_12 : Module.Finite R N],
  homTensorHomEquiv R M N P Q =
    ((rTensorHomEquivHomRTensor R M P (N →ₗ[R] Q)).trans
          ((LinearEquiv.refl R M).arrowCongr (lTensorHomEquivHomLTensor R N P Q))).trans
      (TensorProduct.lift.equiv (RingHom.id R) M N (TensorProduct R P Q))
-- Mathlib.RingTheory.Jacobson.Ideal
/-- The Jacobson radical of `I` is the infimum of all maximal (left) ideals containing `I`.  -/
Ideal.jacobson : {R : Type u} → [inst : Ring R] → Ideal R → Ideal R
-- Mathlib.Algebra.Lie.Basic
/-- The identity map is a morphism of Lie algebras.  -/
LieHom.id : {R : Type u} → {L₁ : Type v} → [inst : CommRing R] → [inst_1 : LieRing L₁] → [inst_2 : LieAlgebra R L₁] → L₁ →ₗ⁅R⁆ L₁
-- Lean.Data.Trie
/-- Returns an `Array` of all values in the trie, in no particular order.  -/
Lean.Data.Trie.values : {α : Type} → Lean.Data.Trie α → Array α
-- Mathlib.Data.Matrix.Mul
Matrix.zero_vecMul : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype m]
  (A : Matrix m n α), Matrix.vecMul 0 A = 0
-- Mathlib.CategoryTheory.Limits.MonoCoprod
CategoryTheory.Limits.MonoCoprod.binaryCofanSum.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {I₁ : Type u_2} {I₂ : Type u_3} {X : I₁ ⊕ I₂ → C}
  (c : CategoryTheory.Limits.Cofan X) (c₁ : CategoryTheory.Limits.Cofan (X ∘ Sum.inl))
  (c₂ : CategoryTheory.Limits.Cofan (X ∘ Sum.inr)) (hc₁ : CategoryTheory.Limits.IsColimit c₁)
  (hc₂ : CategoryTheory.Limits.IsColimit c₂),
  CategoryTheory.Limits.MonoCoprod.binaryCofanSum c c₁ c₂ hc₁ hc₂ =
    CategoryTheory.Limits.BinaryCofan.mk (CategoryTheory.Limits.Cofan.IsColimit.desc hc₁ fun i₁ => c.inj (Sum.inl i₁))
      (CategoryTheory.Limits.Cofan.IsColimit.desc hc₂ fun i₂ => c.inj (Sum.inr i₂))
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_sdiff_eq_sdiff_union`. -/
Set.diff_diff_eq_sdiff_union : ∀ {α : Type u_1} {s t u : Set α}, u ⊆ s → s \ (t \ u) = s \ t ∪ u
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.multiset_map_sum : ∀ {α : Type u_1} {γ : Type u_3} {β : Type u_7} {M : Type u_8} [inst : Zero M] {f : α →₀ M} {m : β → γ}
  {h : α → M → Multiset β}, Multiset.map m (f.sum h) = f.sum fun a b => Multiset.map m (h a b)
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.binomial_eq_binomial : ∀ {R : Type u} [inst : Semiring R] {k l m n : ℕ} {u v : R},
  u ≠ 0 →
    v ≠ 0 →
      (Polynomial.C u * Polynomial.X ^ k + Polynomial.C v * Polynomial.X ^ l =
          Polynomial.C u * Polynomial.X ^ m + Polynomial.C v * Polynomial.X ^ n ↔
        k = m ∧ l = n ∨ u = v ∧ k = n ∧ l = m ∨ u + v = 0 ∧ k = l ∧ m = n)
-- Mathlib.Data.PFunctor.Univariate.M
_private.Mathlib.Data.PFunctor.Univariate.M.0.PFunctor.Approx.head'.match_1.eq_1 : ∀ {F : PFunctor.{u_1, u_2}} (motive : (x : ℕ) → PFunctor.Approx.CofixA F x.succ → Sort u_3) (x : ℕ) (i : F.A)
  (a : F.B i → PFunctor.Approx.CofixA F x)
  (h_1 : (x : ℕ) → (i : F.A) → (a : F.B i → PFunctor.Approx.CofixA F x) → motive x (PFunctor.Approx.CofixA.intro i a)),
  (match x, PFunctor.Approx.CofixA.intro i a with
    | x, PFunctor.Approx.CofixA.intro i a => h_1 x i a) =
    h_1 x i a
-- Mathlib.Algebra.Homology.Monoidal
HomologicalComplex.monoidalCategory : (C : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.Preadditive C] →
        [CategoryTheory.Limits.HasZeroObject C] →
          [(CategoryTheory.MonoidalCategory.curriedTensor C).Additive] →
            [∀ (X₁ : C), ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁).Additive] →
              {I : Type u_2} →
                [inst_6 : AddMonoid I] →
                  (c : ComplexShape I) →
                    [c.TensorSigns] →
                      [∀ (X₁ X₂ : CategoryTheory.GradedObject I C), X₁.HasTensor X₂] →
                        [∀ (X₁ : C),
                              CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                                ((CategoryTheory.MonoidalCategory.curriedTensor C).obj X₁)] →
                          [∀ (X₂ : C),
                                CategoryTheory.Limits.PreservesColimit (CategoryTheory.Functor.empty C)
                                  ((CategoryTheory.MonoidalCategory.curriedTensor C).flip.obj X₂)] →
                            [∀ (X₁ X₂ X₃ X₄ : CategoryTheory.GradedObject I C), X₁.HasTensor₄ObjExt X₂ X₃ X₄] →
                              [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensor₁₂Tensor X₂ X₃] →
                                [∀ (X₁ X₂ X₃ : CategoryTheory.GradedObject I C), X₁.HasGoodTensorTensor₂₃ X₂ X₃] →
                                  [DecidableEq I] → CategoryTheory.MonoidalCategory (HomologicalComplex C c)
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.sSup_adj : ∀ {V : Type u} {G : SimpleGraph V} {a b : V} {s : Set G.Subgraph}, (sSup s).Adj a b ↔ ∃ G_1 ∈ s, G_1.Adj a b
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getD_toList_roo_eq_add : ∀ {m n fallback : ℤ} {i : ℕ}, i < (n - (m + 1)).toNat → (m<...n).toList.getD i fallback = m + 1 + ↑i
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
/-- Let `J` be injective and `g` a morphism into `J`, then `g` can be factored through any monomorphism.
 -/
CategoryTheory.Injective.factorThru : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J X Y : C} → [CategoryTheory.Injective J] → (X ⟶ J) → (f : X ⟶ Y) → [CategoryTheory.Mono f] → Y ⟶ J
-- Mathlib.Data.Finset.Sort
/-- `orderEmbOfFin {a} h` sends any argument to `a`.  -/
Finset.orderEmbOfFin_singleton : ∀ {α : Type u_1} [inst : LinearOrder α] (a : α) (i : Fin 1), ({a}.orderEmbOfFin ⋯) i = a
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.mkVar : Lean.Expr → Lean.Meta.Grind.AC.ACM Lean.Grind.AC.Var
-- Mathlib.CategoryTheory.Monoidal.Braided.Reflection
/-- The uncurried retraction of the unit in the proof of `4 → 1` in `isIso_tfae` below.  -/
_private.Mathlib.CategoryTheory.Monoidal.Braided.Reflection.0.CategoryTheory.Monoidal.Reflective.adjRetractionAux : {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] →
        [inst_2 : CategoryTheory.MonoidalCategory D] →
          [CategoryTheory.SymmetricCategory D] →
            [inst_4 : CategoryTheory.MonoidalClosed D] →
              {R : CategoryTheory.Functor C D} →
                [R.Faithful] →
                  [R.Full] →
                    {L : CategoryTheory.Functor D C} →
                      (adj : L ⊣ R) →
                        (c : C) →
                          (d : D) →
                            [CategoryTheory.IsIso
                                  (L.map
                                    (CategoryTheory.MonoidalCategoryStruct.tensorHom (adj.unit.app (d ⟹ R.obj c))
                                      (adj.unit.app d)))] →
                              CategoryTheory.MonoidalCategoryStruct.tensorObj d ((L.comp R).obj (d ⟹ R.obj c)) ⟶ R.obj c
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonWorkDoneProgressReport : Lean.ToJson Lean.Lsp.WorkDoneProgressReport
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.c₄_of_isShortNF_of_char_three : ∀ {R : Type u_1} [inst : CommRing R] (W : WeierstrassCurve R) [W.IsShortNF] [CharP R 3], W.c₄ = 0
-- Mathlib.Geometry.Manifold.Algebra.LeftInvariantDerivation
LeftInvariantDerivation.commutator_coe_derivation : ∀ {𝕜 : 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} {G : Type u_4}
  [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : Monoid G] [inst_7 : ContMDiffMul I (↑⊤) G]
  (X Y : LeftInvariantDerivation I G), ⇑⁅X, Y⁆ = ⇑⁅↑X, ↑Y⁆
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.EqCnstrProof.erase0.sizeOf_spec : ∀ (c : Lean.Meta.Grind.AC.EqCnstr), sizeOf (Lean.Meta.Grind.AC.EqCnstrProof.erase0 c) = 1 + sizeOf c
-- Init.Data.ToString.Basic
instToStringProd : {α : Type u} → {β : Type v} → [ToString α] → [ToString β] → ToString (α × β)
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.DiagnosticsState.mk.injEq : ∀ (stickyDiagsRef : IO.Ref (Lean.PersistentArray Lean.Widget.InteractiveDiagnostic))
  (diags : Lean.PersistentArray Lean.Widget.InteractiveDiagnostic) (isIncremental : Bool) (publishedDiagsAmount : ℕ)
  (stickyDiagsRef_1 : IO.Ref (Lean.PersistentArray Lean.Widget.InteractiveDiagnostic))
  (diags_1 : Lean.PersistentArray Lean.Widget.InteractiveDiagnostic) (isIncremental_1 : Bool)
  (publishedDiagsAmount_1 : ℕ),
  ({ stickyDiagsRef := stickyDiagsRef, diags := diags, isIncremental := isIncremental,
        publishedDiagsAmount := publishedDiagsAmount } =
      { stickyDiagsRef := stickyDiagsRef_1, diags := diags_1, isIncremental := isIncremental_1,
        publishedDiagsAmount := publishedDiagsAmount_1 }) =
    (stickyDiagsRef = stickyDiagsRef_1 ∧
      diags = diags_1 ∧ isIncremental = isIncremental_1 ∧ publishedDiagsAmount = publishedDiagsAmount_1)
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- If an alternating map in finitely many variables on seminormed spaces
sends vectors with a component of norm zero to vectors of norm zero
and satisfies the inequality `‖f m‖ ≤ C * ∏ i, ‖m i‖` on a shell `ε i / ‖c i‖ < ‖m i‖ < ε i`
for some positive numbers `ε i` and elements `c i : 𝕜`, `1 < ‖c i‖`,
then it satisfies this inequality for all `m`.

The first assumption is automatically satisfied on normed spaces, see `bound_of_shell` below.
For seminormed spaces, it follows from continuity of `f`,
see lemma `bound_of_shell_of_continuous` below.  -/
AlternatingMap.bound_of_shell_of_norm_map_coord_zero : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→ₗ[𝕜] F),
  (∀ {m : ι → E} {i : ι}, ‖m i‖ = 0 → ‖f m‖ = 0) →
    ∀ {ε : ι → ℝ} {C : ℝ},
      (∀ (i : ι), 0 < ε i) →
        ∀ {c : ι → 𝕜},
          (∀ (i : ι), 1 < ‖c i‖) →
            (∀ (m : ι → E), (∀ (i : ι), ε i / ‖c i‖ ≤ ‖m i‖) → (∀ (i : ι), ‖m i‖ < ε i) → ‖f m‖ ≤ C * ∏ i, ‖m i‖) →
              ∀ (m : ι → E), ‖f m‖ ≤ C * ∏ i, ‖m i‖
-- Init.Core
instInhabitedNonScalar.default : NonScalar
-- Mathlib.Order.Preorder.Finsupp
Finsupp.le_def : ∀ {ι : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : LE M] {f g : ι →₀ M}, f ≤ g ↔ ∀ (i : ι), f i ≤ g i
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.toOplax_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.Pseudofunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Pseudofunctor.StrongTrans.Modification η θ)
  (a : B), Γ.toOplax.app a = Γ.app a
-- Mathlib.MeasureTheory.Measure.Decomposition.RadonNikodym
/-- Auxiliary lemma for `inv_rnDeriv`.  -/
MeasureTheory.Measure.inv_rnDeriv_aux : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [μ.HaveLebesgueDecomposition ν]
  [ν.HaveLebesgueDecomposition μ] [MeasureTheory.SigmaFinite μ],
  μ.AbsolutelyContinuous ν → ν.AbsolutelyContinuous μ → (μ.rnDeriv ν)⁻¹ =ᵐ[μ] ν.rnDeriv μ
-- Init.Data.List.Sort.Lemmas
List.map_mergeSort : ∀ {α : Type u_2} {β : Type u_1} {r : α → α → Bool} {s : β → β → Bool} {f : α → β} {l : List α},
  (∀ a ∈ l, ∀ b ∈ l, r a b = s (f a) (f b)) → List.map f (l.mergeSort r) = (List.map f l).mergeSort s
-- Init.System.ST
instMonadST : (σ : Type) → Monad (ST σ)
-- Std.Internal.UV.System
Std.Internal.UV.System.UnameInfo.sysname : Std.Internal.UV.System.UnameInfo → String
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
TopologicalSpace.UpgradedIsCompletelyMetrizableSpace.toMetricSpace : {X : Type u_3} → [self : TopologicalSpace.UpgradedIsCompletelyMetrizableSpace X] → MetricSpace X
-- Mathlib.Algebra.CharP.Lemmas
neg_one_pow_char : ∀ (R : Type u_1) [inst : Ring R] (p : ℕ) [hp : Fact (Nat.Prime p)] [CharP R p], (-1) ^ p = -1
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.isLE_eTruncLT_obj_obj : ∀ {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 : ℤ),
  ∀ i ≤ WithBotTop.coe (n + 1), ∀ (X : C), t.IsLE ((t.eTruncLT.obj i).obj X) n
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.tendsto_coe_atTop : Filter.Tendsto Real.toEReal Filter.atTop (nhds ⊤)
-- Mathlib.Order.Heyting.Basic
LE.le.codisjoint_hnot_left : ∀ {α : Type u_2} [inst : CoheytingAlgebra α] {a b : α}, a ≤ b → Codisjoint (￢a) b
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback₃.p₂₃_p_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S} {f₃ : X₃ ⟶ S}
  {h₁₂ : CategoryTheory.Limits.ChosenPullback f₁ f₂} {h₂₃ : CategoryTheory.Limits.ChosenPullback f₂ f₃}
  {h₁₃ : CategoryTheory.Limits.ChosenPullback f₁ f₃} (h : CategoryTheory.Limits.ChosenPullback₃ h₁₂ h₂₃ h₁₃) {Z : C}
  (h_1 : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp h.p₂₃ (CategoryTheory.CategoryStruct.comp h₂₃.p h_1) =
    CategoryTheory.CategoryStruct.comp h.p h_1
-- Lean.Expr
Lean.BinderInfo.toUInt64 : Lean.BinderInfo → UInt64
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.lam.injEq : ∀ (thm thm_1 : Mathlib.Meta.FunProp.LambdaTheorem),
  (Mathlib.Meta.FunProp.Theorem.lam thm = Mathlib.Meta.FunProp.Theorem.lam thm_1) = (thm = thm_1)
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.isTorsion'_powers_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : Monoid R] [inst_1 : AddCommMonoid M] [inst_2 : DistribMulAction R M] (p : R),
  Module.IsTorsion' M ↥(Submonoid.powers p) ↔ ∀ (x : M), ∃ n, p ^ n • x = 0
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.w₁₃_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex.SnakeInput C), CategoryTheory.CategoryStruct.comp S.v₁₂.τ₃ S.v₂₃.τ₃ = 0
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.closure_le : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {L : BooleanSubalgebra α} {s : Set α},
  BooleanSubalgebra.closure s ≤ L ↔ s ⊆ ↑L
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.mapShortComplexH1.eq_1 : ∀ {k G H : Type u} [inst : CommRing k] [inst_1 : Group G] [inst_2 : Group H] {A : Rep.{max u u_1, u, u} k H}
  {B : Rep.{max u u_1, u, u} k G} (f : G →* H) (φ : Rep.res f A ⟶ B),
  groupCohomology.mapShortComplexH1 f φ =
    { τ₁ := Rep.Hom.toModuleCatHom φ, τ₂ := groupCohomology.cochainsMap₁ f φ, τ₃ := groupCohomology.cochainsMap₂ f φ,
      comm₁₂ := ⋯, comm₂₃ := ⋯ }
-- Lean.Elab.Tactic.Grind.Param
Lean.Elab.Tactic.addEMatchTheorem : Lean.Meta.Grind.Params →
  Lean.Ident →
    Lean.Name →
      Lean.Meta.Grind.EMatchTheoremKind →
        Bool → optParam Bool false → optParam Bool true → Lean.MetaM Lean.Meta.Grind.Params