mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.QuadraticForm.Real
/-- **Sylvester's law of inertia**: A nondegenerate real quadratic form is equivalent to a weighted
sum of squares with the weights being ±1.  -/
QuadraticForm.equivalent_one_neg_one_weighted_sum_squared : ∀ {M : Type u_2} [inst : AddCommGroup M] [inst_1 : Module ℝ M] [FiniteDimensional ℝ M] (Q : QuadraticForm ℝ M),
  LinearMap.SeparatingLeft (QuadraticMap.associated Q) →
    ∃ w,
      (∀ (i : Fin (Module.finrank ℝ M)), w i = -1 ∨ w i = 1) ∧
        QuadraticMap.Equivalent Q (QuadraticMap.weightedSumSquares ℝ w)
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- A morphism `f` induces a function `pseudoApply f` on pseudoelements.  -/
CategoryTheory.Abelian.Pseudoelement.pseudoApply : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {P Q : C} → (P ⟶ Q) → CategoryTheory.Abelian.Pseudoelement P → CategoryTheory.Abelian.Pseudoelement Q
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.blastAdd.denote_mkFullAdderCarry : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] (assign : α → Bool) (aig : Std.Sat.AIG α)
  (input : Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig),
  ⟦assign, Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderCarry aig input⟧ =
    ((⟦assign, { aig := aig, ref := input.lhs }⟧ ^^ ⟦assign, { aig := aig, ref := input.rhs }⟧) &&
        ⟦assign, { aig := aig, ref := input.cin }⟧ ||
      ⟦assign, { aig := aig, ref := input.lhs }⟧ && ⟦assign, { aig := aig, ref := input.rhs }⟧)
-- Mathlib.CategoryTheory.Bicategory.Modification.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.Modification.whiskerRight_naturality : ∀ {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 : B} {a' : C} (f : a ⟶ b) (g : G.obj b ⟶ a'),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (F.map f) (CategoryTheory.Bicategory.whiskerRight (Γ.app b) g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (θ.app b) g).inv
        (CategoryTheory.Bicategory.whiskerRight (θ.naturality f).hom g)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (η.app b) g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f).hom g)
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (Γ.app a) (G.map f)) g))
-- Aesop.RuleTac.ElabRuleTerm
Aesop.elabRuleTermForApplyLike : Lean.Term → Aesop.ElabM Lean.Expr
-- Lean.Elab.InfoTree.Types
Lean.Elab.PartialContextInfo.commandCtx.sizeOf_spec : ∀ (info : Lean.Elab.CommandContextInfo), sizeOf (Lean.Elab.PartialContextInfo.commandCtx info) = 1 + sizeOf info
-- Mathlib.LinearAlgebra.Complex.Module
/-- The real part `ℜ a` of an element `a` of a star module over `ℂ`, as a linear map. This is just
`selfAdjointPart ℝ`, but we provide it as a separate definition in order to link it with lemmas
concerning the `imaginaryPart`, which doesn't exist in star modules over other rings.  -/
realPart : {A : Type u_1} →
  [inst : AddCommGroup A] →
    [inst_1 : Module ℂ A] → [inst_2 : StarAddMonoid A] → [inst_3 : StarModule ℂ A] → A →ₗ[ℝ] ↥(selfAdjoint A)
-- Mathlib.RingTheory.Etale.StandardEtale
Algebra.IsStandardEtale.of_equiv : ∀ {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] (e : S ≃ₐ[R] T) [Algebra.IsStandardEtale R S],
  Algebra.IsStandardEtale R T
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getD_toList_rcc : ∀ {m n i fallback : ℕ}, (m...=n).toList.getD i fallback = if i < n + 1 - m then m + i else fallback
-- Mathlib.Algebra.MvPolynomial.NoZeroDivisors
MvPolynomial.degreeOf_C_mul : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] {p : MvPolynomial σ R} (j : σ),
  ∀ c ∈ nonZeroDivisors R, MvPolynomial.degreeOf j (MvPolynomial.C c * p) = MvPolynomial.degreeOf j p
-- Lean.Meta.Tactic.Grind.AC.Seq
/-- Reverses the sequence  -/
Lean.Grind.AC.Seq.reverse : Lean.Grind.AC.Seq → Lean.Grind.AC.Seq
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.toCat.obj_eq_Fin : ∀ (n : ℕ), ↑(SimplexCategory.toCat.obj { len := n }) = Fin (n + 1)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_apply' : ∀ {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] (M : Matrix n n R),
  M.det = ∑ σ, ↑↑(Equiv.Perm.sign σ) * ∏ i, M (σ i) i
-- Mathlib.Order.Hom.BoundedLattice
SupBotHom.id_toFun : ∀ (α : Type u_2) [inst : Max α] [inst_1 : Bot α] (a : α), (SupBotHom.id α) a = a
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_eq_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] [inst_1 : Inhabited α]
  {a : α} {h : a ∈ t}, t.get a h = t.get! a