mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.coe_continuousLinearEquivAt_eq' : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : NontriviallyNormedField R]
  [inst_1 : (x : B) → AddCommMonoid (E x)] [inst_2 : (x : B) → Module R (E x)] [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace R F] [inst_5 : TopologicalSpace B] [inst_6 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_7 : (x : B) → TopologicalSpace (E x)] [inst_8 : FiberBundle F E]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_9 : Bundle.Trivialization.IsLinear R e] {b : B}
  (hb : b ∈ e.baseSet),
  ↑(Bundle.Trivialization.continuousLinearEquivAt R e b hb) = Bundle.Trivialization.continuousLinearMapAt R e b
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.instGroup : {R : Type u} → [inst : CommRing R] → Group (WeierstrassCurve.VariableChange R)
-- Mathlib.Analysis.Asymptotics.Theta
/-- **Alias** of the forward direction of `Asymptotics.isTheta_const_mul_left`. -/
Asymptotics.IsTheta.of_const_mul_left : ∀ {α : Type u_1} {F : Type u_4} {𝕜 : Type u_14} [inst : Norm F] [inst_1 : NormedField 𝕜] {g : α → F} {l : Filter α}
  {c : 𝕜} {f : α → 𝕜}, c ≠ 0 → (fun x => c * f x) =Θ[l] g → f =Θ[l] g
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- Construct an `α`-indexed cochain complex from a dependently-typed differential.
 -/
CochainComplex.of : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      {α : Type u_2} →
        [inst_2 : AddRightCancelSemigroup α] →
          [inst_3 : One α] →
            [DecidableEq α] →
              (X : α → V) →
                (d : (n : α) → X n ⟶ X (n + 1)) →
                  (∀ (n : α), CategoryTheory.CategoryStruct.comp (d n) (d (n + 1)) = 0) → CochainComplex V α
-- Mathlib.Order.Interval.Set.OrdConnected
/-- It suffices to prove `[[x, y]] ⊆ s` for `x y ∈ s`, `x ≤ y`.  -/
Set.ordConnected_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, s.OrdConnected ↔ ∀ x ∈ s, ∀ y ∈ s, x ≤ y → Set.Icc x y ⊆ s
-- Mathlib.RingTheory.Localization.Defs
IsLocalization.of_le : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [IsLocalization M S] (N : Submonoid R),
  M ≤ N → (∀ r ∈ N, IsUnit ((algebraMap R S) r)) → IsLocalization N S
-- Mathlib.Algebra.Algebra.Hom
AlgHom.coe_addMonoidHom_injective : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B], Function.Injective AddMonoidHomClass.toAddMonoidHom
-- Mathlib.Data.Multiset.Fintype
Multiset.card_toEnumFinset : ∀ {α : Type u_1} [inst : DecidableEq α] (m : Multiset α), m.toEnumFinset.card = m.card
-- Mathlib.RingTheory.Finiteness.Descent
/-- If `T ⊗[R] S` is of finite type over `T` and `T` is `R`-faithfully flat,
then `S` is of finite type over `R`  -/
Algebra.FiniteType.of_finiteType_tensorProduct_of_faithfullyFlat : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Type u_3)
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [Module.FaithfullyFlat R T] [Algebra.FiniteType T (TensorProduct R T S)],
  Algebra.FiniteType R S
-- Mathlib.Analysis.Calculus.IteratedDeriv.FaaDiBruno
iteratedDeriv_vcomp_three : ∀ {𝕜 : 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] {g : E → F} {f : 𝕜 → E} {x : 𝕜},
  ContDiffAt 𝕜 3 g (f x) →
    ContDiffAt 𝕜 3 f x →
      iteratedDeriv 3 (g ∘ f) x =
        ((iteratedFDeriv 𝕜 3 g (f x)) fun x_1 => deriv f x) +
              (iteratedFDeriv 𝕜 2 g (f x)) ![iteratedDeriv 2 f x, deriv f x] +
            2 • (iteratedFDeriv 𝕜 2 g (f x)) ![deriv f x, iteratedDeriv 2 f x] +
          (fderiv 𝕜 g (f x)) (iteratedDeriv 3 f x)
-- Init.Grind.Norm
Lean.Grind.not_false : (¬False) = True
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Only symbols with priority `>= minPrio` are considered in patterns.  -/
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.NormalizePattern.Context.minPrio : Lean.Meta.Grind.NormalizePattern.Context✝ → ℕ
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.mk.congr_simp : ∀ (R : Type u) (M : Type v) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Module.Invertible R M], CommRing.Pic.mk R M = CommRing.Pic.mk R M
-- Mathlib.Algebra.Polynomial.Sequence
/-- Basis elements have strictly monotone degree.  -/
Polynomial.Sequence.basis_degree_strictMono : ∀ {R : Type u_1} [inst : Ring R] (S : Polynomial.Sequence R) [inst_1 : IsDomain R]
  (hCoeff : ∀ (i : ℕ), IsUnit (↑S i).leadingCoeff), StrictMono (Polynomial.degree ∘ ⇑(S.basis hCoeff))
-- Mathlib.Topology.Algebra.Order.Archimedean
/-- In a nontrivial densely linear ordered archimedean topological additive group,
a subgroup is either dense or is cyclic, but not both.

For a non-exclusive `Or` version with weaker assumptions, see `AddSubgroup.dense_or_cyclic` above.
 -/
AddSubgroup.dense_xor_cyclic : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] [IsOrderedAddMonoid G] [inst_3 : TopologicalSpace G]
  [OrderTopology G] [Archimedean G] [Nontrivial G] [DenselyOrdered G] (s : AddSubgroup G),
  Xor (Dense ↑s) (∃ a, s = AddSubgroup.zmultiples a)
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderivWithin_const_sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {s : Set E},
  UniqueDiffWithinAt 𝕜 s x → ∀ (c : F), fderivWithin 𝕜 (fun y => c - f y) s x = -fderivWithin 𝕜 f s x
-- Init.Data.List.Nat.Range
List.mem_zipIdx_iff_le_and_getElem?_sub : ∀ {α : Type u_1} {x : α × ℕ} {l : List α} {k : ℕ}, x ∈ l.zipIdx k ↔ k ≤ x.2 ∧ l[x.2 - k]? = some x.1
-- Mathlib.Order.Bounds.Basic
IsCoinitialFor.mono_right : ∀ {α : Type u_1} [inst : Preorder α] {s t u : Set α}, t ⊆ u → IsCoinitialFor s t → IsCoinitialFor s u
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getKeyDₘ_eq_getKeyD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α] {k : α}
  {t : Std.DTreeMap.Internal.Impl α β} {fallback : α},
  t.Ordered → Std.DTreeMap.Internal.Impl.getKeyDₘ k t fallback = Std.Internal.List.getKeyD k t.toListModel fallback
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPowerSeries.algebraMvPowerSeries : {σ : Type u_1} →
  {R : Type u_2} →
    {A : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] → [Algebra R A] → Algebra (MvPowerSeries σ R) (MvPowerSeries σ A)
-- Mathlib.Algebra.BigOperators.Finprod
/-- Monotonicity of `finsum.`  -/
finsum_le_finsum' : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f g : α → M} [inst_1 : PartialOrder M] [AddLeftMono M],
  Function.HasFiniteSupport f → Function.HasFiniteSupport g → f ≤ g → ∑ᶠ (a : α), f a ≤ ∑ᶠ (a : α), g a
-- Mathlib.Topology.Order.Basic
order_separated : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {a₁ a₂ : α},
  a₁ < a₂ → ∃ u v, IsOpen u ∧ IsOpen v ∧ a₁ ∈ u ∧ a₂ ∈ v ∧ ∀ b₁ ∈ u, ∀ b₂ ∈ v, b₁ < b₂
-- Mathlib.Probability.Distributions.Cauchy
ProbabilityTheory.cauchyPDFReal_def' : ∀ (x₀ : ℝ) (γ : NNReal) (x : ℝ), ProbabilityTheory.cauchyPDFReal x₀ γ x = Real.pi⁻¹ * ↑γ⁻¹ * (1 + ((x - x₀) / ↑γ) ^ 2)⁻¹
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.LetValue.updatePapImp : {pu : Lean.Compiler.LCNF.Purity} →
  Lean.Compiler.LCNF.LetValue pu → Lean.Name → Array (Lean.Compiler.LCNF.Arg pu) → Lean.Compiler.LCNF.LetValue pu
-- Mathlib.Data.ENat.Basic
ENat.WithBot.ofNat_add_cancel : ∀ {a b : WithBot ℕ∞} {c : ℕ} [inst : c.AtLeastTwo], OfNat.ofNat c + a = OfNat.ofNat c + b ↔ a = b
-- Lean.Elab.PreDefinition.WF.PackMutual
/-- Processes the expression and replaces calls to  the `preDefs` with calls to `f`.
 -/
Lean.Elab.WF.packCalls : Lean.Elab.FixedParamPerms → Lean.Meta.ArgsPacker → Array Lean.Name → Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Lean.Elab.Command
Lean.Elab.Command.MacroExpandedSnapshot.toSnapshot : Lean.Elab.Command.MacroExpandedSnapshot → Lean.Language.Snapshot
-- Mathlib.Order.Interval.Set.OrdConnected
Set.image_subtype_val_Ico : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [s.OrdConnected] (x y : ↑s), Subtype.val '' Set.Ico x y = Set.Ico ↑x ↑y
-- Mathlib.Algebra.Lie.Matrix
LieModule.instIsFaithfulMatrixForall : ∀ {R : Type u} [inst : CommRing R] {n : Type w} [inst_1 : DecidableEq n] [inst_2 : Fintype n],
  LieModule.IsFaithful R (Matrix n n R) (n → R)
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.String.Slice.Pos.nextn.match_1.congr_eq_1 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  n = 0 →
    (match n with
      | 0 => h_1 ()
      | n.succ => h_2 n) ≍
      h_1 ()
-- Mathlib.Algebra.Opposites
AddOpposite.unop.eq_1 : ∀ {α : Type u_1}, AddOpposite.unop = PreOpposite.unop'
-- Mathlib.Analysis.CStarAlgebra.Classes
MulOpposite.instNonUnitalCommCStarAlgebra : {A : Type u_1} → [NonUnitalCommCStarAlgebra A] → NonUnitalCommCStarAlgebra Aᵐᵒᵖ
-- Mathlib.AlgebraicGeometry.EllipticCurve.NormalForms
WeierstrassCurve.exists_variableChange_isCharThreeNF : ∀ {F : Type u_2} [inst : Field F] [CharP F 3] (W : WeierstrassCurve F), ∃ C, (C • W).IsCharThreeNF
-- Lean.Parser.Term.Basic
/-- The syntax `{ tacs }` is an alternative syntax for `· tacs`.
It runs the tactics in sequence, and fails if the goal is not solved.  -/
Lean.Parser.Tactic.tacticSeqBracketed : Lean.Parser.Parser
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.IsSubordinate.disjUnion : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I} {r : (ι → ℝ) → ↑(Set.Ioi 0)}
  [inst : Fintype ι],
  π₁.IsSubordinate r → π₂.IsSubordinate r → ∀ (h : Disjoint π₁.iUnion π₂.iUnion), (π₁.disjUnion π₂ h).IsSubordinate r
-- Mathlib.CategoryTheory.Enriched.Ordinary.Basic
CategoryTheory.EnrichedOrdinaryCategory.homEquiv_id : ∀ {V : Type u'} {inst : CategoryTheory.Category.{v', u'} V} {inst_1 : CategoryTheory.MonoidalCategory V} {C : Type u}
  {inst_2 : CategoryTheory.Category.{v, u} C} [self : CategoryTheory.EnrichedOrdinaryCategory V C] (X : C),
  CategoryTheory.EnrichedOrdinaryCategory.homEquiv (CategoryTheory.CategoryStruct.id X) = CategoryTheory.eId V X
-- Init.Data.Iterators.Combinators.Monadic.ULift
Std.Iterators.Types.ULiftIterator.instFinite : ∀ {α : Type u} {m : Type u → Type u'} {n : Type (max u v) → Type v'} {β : Type u}
  {lift : ⦃γ : Type u⦄ → m γ → Std.Iterators.ULiftT n γ} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m]
  [inst_2 : Monad n], Std.Iterators.Finite (Std.Iterators.Types.ULiftIterator α m n β lift) n
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.Context.mk.sizeOf_spec : ∀ (level₂ level₁ level₀ : Lean.Level) (B : Q(Type level₀)) (instBicategory : Q(CategoryTheory.Bicategory «$B»)),
  sizeOf { level₂ := level₂, level₁ := level₁, level₀ := level₀, B := B, instBicategory := instBicategory } =
    1 + sizeOf level₂ + sizeOf level₁ + sizeOf level₀ + sizeOf B + sizeOf instBicategory
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.getKey!.eq_2 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Inhabited α] (a a_1 : α) (b : β a_1)
  (es : Std.DHashMap.Internal.AssocList α β),
  Std.DHashMap.Internal.AssocList.getKey! a (Std.DHashMap.Internal.AssocList.cons a_1 b es) =
    if (a_1 == a) = true then a_1 else Std.DHashMap.Internal.AssocList.getKey! a es
-- Mathlib.Analysis.Calculus.FDeriv.Symmetric
/-- Definition recording that a function has a symmetric second derivative at
a point. This is automatic in most cases of interest (open sets over real or complex vector fields,
or general case for analytic functions), but we can express theorems of calculus using this
as a general assumption, and then specialize to these situations.  -/
IsSymmSndFDerivAt : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      {F : Type u_3} →
        [inst_1 : NormedAddCommGroup E] →
          [NormedSpace 𝕜 E] → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → (E → F) → E → Prop
-- Mathlib.Algebra.Order.Ring.Abs
pow_eq_pow_iff_cases : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] {a b : R} {n : ℕ},
  a ^ n = b ^ n ↔ n = 0 ∨ a = b ∨ a = -b ∧ Even n
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.coe_toStrongDual : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E]
  (x' : WeakDual 𝕜 E), ⇑(WeakDual.toStrongDual x') = ⇑x'
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List (α × β)} {k : α} (contains_eq_false : (List.map Prod.fst l).contains k = false)
  {h : k ∈ m.insertMany l}, (m.insertMany l).getKey k h = m.getKey k ⋯
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_neg_iff_add_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddRightStrictMono α] {a b : α}, a < -b ↔ a + b < 0
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.polyCharpolyAux.eq_1 : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ιM] [inst_7 : DecidableEq ι]
  [inst_8 : DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M),
  φ.polyCharpolyAux b bₘ =
    Polynomial.map (↑(MvPolynomial.bind₁ (LinearMap.toMvPolynomial b bₘ.end φ))) (Matrix.charpoly.univ R ιM)
-- Mathlib.CategoryTheory.Limits.MorphismProperty
/-- If `P` is stable under composition, base change and satisfies post-cancellation,
`Over.forget P ⊤ X` creates pullbacks.  -/
CategoryTheory.MorphismProperty.Over.createsLimitsOfShape_walkingCospan : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    (P : CategoryTheory.MorphismProperty T) →
      (X : T) →
        [CategoryTheory.Limits.HasPullbacks T] →
          [P.IsStableUnderComposition] →
            [P.IsStableUnderBaseChange] →
              [P.HasOfPostcompProperty P] →
                CategoryTheory.CreatesLimitsOfShape CategoryTheory.Limits.WalkingCospan
                  (CategoryTheory.MorphismProperty.Over.forget P ⊤ X)
-- Mathlib.Algebra.Ring.Defs
neg_eq_neg_one_mul : ∀ {α : Type u} [inst : MulOneClass α] [inst_1 : HasDistribNeg α] (a : α), -a = -1 * a
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
/-- Because of `coeff_hermite_of_odd_add`, every nonzero coefficient is described as follows.  -/
Polynomial.coeff_hermite_explicit : ∀ (n k : ℕ),
  (Polynomial.hermite (2 * n + k)).coeff k = (-1) ^ n * ↑(2 * n - 1).doubleFactorial * ↑((2 * n + k).choose k)
-- Mathlib.Algebra.Quaternion
/-- First imaginary part (i) of a quaternion.  -/
QuaternionAlgebra.imI : {R : Type u_1} → {a b c : R} → QuaternionAlgebra R a b c → R
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_getKey?_eq_contains : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {a : α},
  (t.getKey? a).isSome = t.contains a
-- Mathlib.SetTheory.ZFC.Class
ZFSet.map_fval : ∀ {f : ZFSet.{u} → ZFSet.{u}} [inst : ZFSet.Definable₁ f] {x y : ZFSet.{u}}, y ∈ x → ↑(ZFSet.map f x) ′ ↑y = ↑(f y)
-- Mathlib.GroupTheory.Perm.Cycle.Concrete
Equiv.Perm.exists_toCycle_toList : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (f : Equiv.Perm α) (hf : f.IsCycle),
  ∃ x, f.toCycle hf = ↑(f.toList x)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKey?_bind_getKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.maxKey?.bind t.getKey? = t.maxKey?
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.io.sizeOf_spec : ∀ (hi : Lean.Meta.Grind.Arith.Cutsat.SymbolicBound),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.SymbolicIntInterval.io hi) = 1 + sizeOf hi
-- Lean.Parser.Term
Lean.Parser.Term.app.formatter : Lean.PrettyPrinter.Formatter
-- Init.Data.SInt.Lemmas
Int64.toInt16_ofNat : ∀ {n : ℕ}, (OfNat.ofNat n).toInt16 = OfNat.ofNat n
-- Mathlib.Analysis.MeanInequalities
Real.arith_mean_weighted_of_constant : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ) (x : ℝ),
  ∑ i ∈ s, w i = 1 → (∀ i ∈ s, w i ≠ 0 → z i = x) → ∑ i ∈ s, w i * z i = x
-- ProofWidgets.Component.Basic
/-- Render a given string as Markdown.
LaTeX is supported with MathJax:
use `$...$` for inline math,
and `$$...$$` for displayed math.

Example usage:
```lean
<MarkdownDisplay contents={"$a + b = c$"} />
```  -/
ProofWidgets.MarkdownDisplay : ProofWidgets.Component ProofWidgets.MarkdownDisplay.Props
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.evaluation₂_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (sq : CategoryTheory.Square C),
  CategoryTheory.Square.evaluation₂.obj sq = sq.X₂
-- Mathlib.CategoryTheory.Elements
/-- The reverse direction of the equivalence `F.Elementsᵒᵖ ≅ (yoneda, F)`,
given by `CategoryTheory.yonedaEquiv`.
 -/
CategoryTheory.CategoryOfElements.fromCostructuredArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (F : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda F)ᵒᵖ F.Elements
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.ι_reflexiveCoequalizerIsoCoequalizer_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C)
  [inst_1 :
    CategoryTheory.Limits.HasCoequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
      (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right)]
  {Z : C}
  (h :
    CategoryTheory.Limits.coequalizer (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
        (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F CategoryTheory.Limits.WalkingReflexivePair.zero)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.reflexiveCoequalizerIsoCoequalizer F).hom h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coequalizer.π (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.left)
        (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right))
      h
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.State.levelNames : Lean.Elab.Term.State → List Lean.Name
-- Mathlib.Topology.UniformSpace.Real
NNReal.instTopologicalSpace : TopologicalSpace NNReal
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.union_mul_inter_subset : ∀ {α : Type u_2} [inst : CommSemigroup α] {s t : Set α}, (s ∪ t) * (s ∩ t) ⊆ s * t
-- Init.Data.Nat.ToString
Nat.digitChar_eq_one : ∀ {n : ℕ}, n.digitChar = '1' ↔ n = 1
-- Lean.HeadIndex
/-- Return the number of arguments in the given expression with respect to its `HeadIndex`  -/
Lean.Expr.headNumArgs : Lean.Expr → ℕ
-- Init.Data.List.Nat.Modify
List.exists_of_modify : ∀ {α : Type u_1} (f : α → α) {i : ℕ} {l : List α},
  i < l.length → ∃ l₁ a l₂, l = l₁ ++ a :: l₂ ∧ l₁.length = i ∧ l.modify i f = l₁ ++ f a :: l₂
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.finsetSum_apply : ∀ {α : Type u_1} {ι : Type u_5} {m : MeasurableSpace α} (I : Finset ι) (μ : ι → MeasureTheory.Measure α) (s : Set α),
  (∑ i ∈ I, μ i) s = ∑ i ∈ I, (μ i) s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A : C),
  (CategoryTheory.CartesianMonoidalCategory.prodComparisonBifunctorNatTrans F).app A =
    CategoryTheory.CartesianMonoidalCategory.prodComparisonNatTrans F A
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonRpcKeepAliveParams.fromJson : Lean.Json → Except String Lean.Lsp.RpcKeepAliveParams
-- Mathlib.LinearAlgebra.UnitaryGroup
Matrix.mem_orthogonalGroup_iff : ∀ (n : Type u) [inst : DecidableEq n] [inst_1 : Fintype n] (R : Type v) [inst_2 : CommRing R] {A : Matrix n n R},
  A ∈ Matrix.orthogonalGroup n R ↔ A * A.transpose = 1
-- Mathlib.Combinatorics.SimpleGraph.Clique
/-- The neighbors of a vertex `v` form an independent set in a triangle free graph `G`.  -/
SimpleGraph.isIndepSet_neighborSet_of_triangleFree : ∀ {α : Type u_1} (G : SimpleGraph α), G.CliqueFree 3 → ∀ (v : α), G.IsIndepSet (G.neighborSet v)
-- Mathlib.Order.Completion
DedekindCut.principalIso_symm_apply : ∀ {α : Type u_1} [inst : CompleteLattice α] (A : DedekindCut α), DedekindCut.principalIso.symm A = sSup A.left
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaMon.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaMon =
    { obj := fun M => CategoryTheory.yonedaMonObj M.X,
      map := fun {X Y} ψ =>
        { app := fun x => MonCat.ofHom (CategoryTheory.IsMonHom.monoidHom ψ.hom (Opposite.unop x)), naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Data.Finsupp.Multiset
Sym.coe_equivNatSum_apply_apply : ∀ (α : Type u_1) [inst : DecidableEq α] (n : ℕ) (s : Sym α n) (a : α),
  ↑((Sym.equivNatSum α n) s) a = Multiset.count a ↑s
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
/-- Constructor for morphisms in `BifibrantObject C`.  -/
HomotopicalAlgebra.BifibrantObject.homMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C] →
      [inst_2 : CategoryTheory.Limits.HasInitial C] →
        [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C] →
          [inst_4 : CategoryTheory.Limits.HasTerminal C] →
            {X Y : C} →
              [inst_5 : HomotopicalAlgebra.IsCofibrant X] →
                [inst_6 : HomotopicalAlgebra.IsCofibrant Y] →
                  [inst_7 : HomotopicalAlgebra.IsFibrant X] →
                    [inst_8 : HomotopicalAlgebra.IsFibrant Y] →
                      (X ⟶ Y) → (HomotopicalAlgebra.BifibrantObject.mk X ⟶ HomotopicalAlgebra.BifibrantObject.mk Y)
-- Mathlib.Analysis.MellinTransform
/-- Predicate on `f` and `s` asserting that the Mellin integral is well-defined.  -/
MellinConvergent : {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → (ℝ → E) → ℂ → Prop
-- Mathlib.Topology.Maps.Basic
/-- **Alias** of `Topology.IsQuotientMap.of_comp_of_isCoinducing`. -/
Topology.IsQuotientMap.of_comp_of_eq_coinduced : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} {f : X → Y} {g : Y → Z} [inst : TopologicalSpace X]
  [inst_1 : TopologicalSpace Y] [inst_2 : TopologicalSpace Z],
  Topology.IsQuotientMap (g ∘ f) → Topology.IsCoinducing f → Topology.IsQuotientMap g
-- Mathlib.Data.TwoPointing
TwoPointing.bool_fst : TwoPointing.bool.toProd.1 = false
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.next_eq_self' : ∀ {ι : Type u_1} (c : ComplexShape ι) (j : ι), (∀ (k : ι), ¬c.Rel j k) → c.next j = j
-- Lean.Environment
_private.Lean.Environment.0.Lean.VisibilityMap.mk : {α : Type} → α → α → Lean.VisibilityMap✝ α