mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.NumberTheory.SmoothNumbers
/-- The sets of `N`-smooth and of `(N+1)`-smooth numbers are the same when `N` is not prime.
See `Nat.equivProdNatSmoothNumbers` for when `N` is prime.  -/
Nat.smoothNumbers_succ : ∀ {N : ℕ}, ¬Nat.Prime N → (N + 1).smoothNumbers = N.smoothNumbers
-- Mathlib.CategoryTheory.MorphismProperty.Basic
/-- The class of morphisms given by a family of morphisms `f i : X i ⟶ Y i`.  -/
CategoryTheory.MorphismProperty.ofHoms : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {ι : Type u_3} → {X Y : ι → C} → ((i : ι) → X i ⟶ Y i) → CategoryTheory.MorphismProperty C
-- Lean.Meta.Match.Match
_private.Lean.Meta.Match.Match.0.Lean.Meta.Match.instBEqMatcherKey : BEq Lean.Meta.Match.MatcherKey✝
-- Mathlib.Order.BooleanAlgebra.Basic
inf_sdiff_left_comm : ∀ {α : Type u} [inst : GeneralizedBooleanAlgebra α] (a b c : α), a ⊓ b \ c = b ⊓ a \ c
-- Init.Data.SInt.Lemmas
Int16.ofInt_toInt : ∀ (x : Int16), Int16.ofInt x.toInt = x
-- Mathlib.Data.ENNReal.Real
ENNReal.toNNReal_le_toNNReal : ∀ {a b : ENNReal}, a ≠ ⊤ → b ≠ ⊤ → (a.toNNReal ≤ b.toNNReal ↔ a ≤ b)
-- Mathlib.Geometry.Euclidean.SignedDist
AffineSubspace.abs_signedInfDist_eq_dist_of_mem_affineSpan_insert : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : AffineSubspace ℝ P} [inst_4 : Nonempty ↥s]
  [inst_5 : s.direction.HasOrthogonalProjection] {p x : P},
  x ∈ affineSpan ℝ (insert p ↑s) → |(s.signedInfDist p) x| = dist x ↑((EuclideanGeometry.orthogonalProjection s) x)
-- Mathlib.AlgebraicGeometry.Morphisms.Separated
AlgebraicGeometry.IsSeparated.instMap : ∀ (R S : CommRingCat) (f : R ⟶ S), AlgebraicGeometry.IsSeparated (AlgebraicGeometry.Spec.map f)
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
/-- The additive version of `AddMonoidAlgebra.addMonoidAlgebraEquivDirectSum`.  -/
addMonoidAlgebraAddEquivDirectSum : {ι : Type u_1} →
  {M : Type u_3} →
    [DecidableEq ι] →
      [inst : Semiring M] → [(m : M) → Decidable (m ≠ 0)] → AddMonoidAlgebra M ι ≃+ DirectSum ι fun x => M
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.sinh_half_dist : ∀ (z w : UpperHalfPlane), Real.sinh (dist z w / 2) = dist ↑z ↑w / (2 * √(z.im * w.im))
-- Mathlib.Analysis.Convex.Cone.Basic
ProperCone.convex : ∀ {R : Type u_2} {E : Type u_3} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module R E] (C : ProperCone R E), Convex R ↑C
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.ArgSpec.flag.sizeOf_spec : ∀ (name : Lean.Name) (default : Bool), sizeOf (Lean.Doc.ArgSpec.flag✝ name default) = 1 + sizeOf name + sizeOf default
-- Mathlib.Algebra.Homology.Embedding.ExtendHomotopy
/-- If `e : c.Embedding c'` is an embedding of complex shapes and `h` is a
homotopy between morphisms of homological complexes of shape `c`, this is
the corresponding homotopy between the extension of these morphisms.  -/
Homotopy.extend : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
              [inst_2 : CategoryTheory.Preadditive C] →
                {K L : HomologicalComplex C c} →
                  {f g : K ⟶ L} →
                    Homotopy f g →
                      (e : c.Embedding c') →
                        [e.IsRelIff] → Homotopy (HomologicalComplex.extendMap f e) (HomologicalComplex.extendMap g e)
-- Mathlib.Combinatorics.SetFamily.FourFunctions
le_collapse_of_mem : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq α] [inst_1 : CommSemiring β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {𝒜 : Finset (Finset α)} {a : α} {f : Finset α → β} {s t : Finset α},
  a ∉ s → 0 ≤ f → t = s → t ∈ 𝒜 → f t ≤ collapse✝ 𝒜 a f s
-- Mathlib.LinearAlgebra.ExteriorPower.Basis
/-- If `b` is a basis of `M` indexed by a linearly ordered type `I` and `s` is a finset of
`I` of cardinality `n`, then we get a linear form on the `n`th exterior power of `M` by
applying the `exteriorPower.linearForm` construction to the family of linear forms
given by the coordinates of `b` indexed by elements of `s` (ordered using the given order on
`I`).  -/
exteriorPower.ιMultiDual : (R : Type u_1) →
  {M : Type u_3} →
    (n : ℕ) →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            {I : Type u_5} → [LinearOrder I] → Module.Basis I R M → ↑(Set.powersetCard I n) → Module.Dual R ↥(⋀[R]^n M)
-- Mathlib.Analysis.Normed.Group.Basic
eq_zero_or_nnnorm_pos : ∀ {E : Type u_5} [inst : NormedAddGroup E] (a : E), a = 0 ∨ 0 < ‖a‖₊
-- Std.Sat.AIG.RefVecOperator.Map
Std.Sat.AIG.RefVec.MapTarget.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {len : ℕ} {vec : aig.RefVec len}
  {func : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α}
  {lawful : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref func} {chainable : Std.Sat.AIG.RefVec.LawfulMapOperator α func}
  {vec_1 : aig.RefVec len} {func_1 : (aig : Std.Sat.AIG α) → aig.Ref → Std.Sat.AIG.Entrypoint α}
  {lawful_1 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.Ref func_1}
  {chainable_1 : Std.Sat.AIG.RefVec.LawfulMapOperator α func_1},
  { vec := vec, func := func, lawful := lawful, chainable := chainable } =
      { vec := vec_1, func := func_1, lawful := lawful_1, chainable := chainable_1 } →
    vec = vec_1 ∧ func = func_1
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
/-- `associated` is the linear map that sends a quadratic map over a commutative ring to its
associated symmetric bilinear map.  -/
QuadraticMap.associated : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] →
            [inst_3 : AddCommGroup N] →
              [inst_4 : Module R N] → [Invertible 2] → QuadraticMap R M N →ₗ[R] LinearMap.BilinMap R M N
-- Mathlib.Topology.Constructions.SumProd
isClosed_range_inl : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y], IsClosed (Set.range Sum.inl)
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote.eq_def : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly),
  Int.Internal.Linear.Poly.denote ctx p =
    match p with
    | Int.Internal.Linear.Poly.num k => k
    | Int.Internal.Linear.Poly.add k v p =>
      k * Int.Internal.Linear.Var.denote ctx v + Int.Internal.Linear.Poly.denote ctx p
-- Mathlib.Topology.Algebra.Group.Torsor
ContinuousOn.sdiv : ∀ {V : Type u_1} {P : Type u_2} {α : Type u_3} [inst : Group V] [inst_1 : TopologicalSpace V] [inst_2 : Torsor V P]
  [inst_3 : TopologicalSpace P] [IsTopologicalTorsor P] [inst_5 : TopologicalSpace α] {f g : α → P} {s : Set α},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun x => f x /ₛ g x) s
-- Batteries.Data.Fin.Lemmas
Fin.isSome_findSomeRev?_iff : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, (Fin.findSomeRev? f).isSome = true ↔ ∃ i, (f i).isSome = true
-- Lean.Attributes
Lean.EnumAttributes.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (attrs : List Lean.AttributeImpl)
  (ext : Lean.PersistentEnvExtension (Lean.Name × α) (Lean.Name × α) (Lean.NameMap α)),
  sizeOf { attrs := attrs, ext := ext } = 1 + sizeOf attrs + sizeOf ext
-- Mathlib.Algebra.PEmptyInstances
AddSemigroupPEmpty : AddSemigroup PEmpty.{u + 1}
-- Mathlib.AlgebraicGeometry.Geometrically.Reduced
/-- We say that morphism `f : X ⟶ Y` is geometrically reduced if for all `Spec K ⟶ Y` with `K`
a field, `X ×[Y] Spec K` is reduced.  -/
AlgebraicGeometry.GeometricallyReduced : {X Y : AlgebraicGeometry.Scheme} → (X ⟶ Y) → Prop
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Expr.toPolyC.go.match_4.congr_eq_3 : ∀ (motive : Lean.Grind.CommRing.Expr → Sort u_1) (x : Lean.Grind.CommRing.Expr)
  (h_1 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.num k))
  (h_2 : (k : ℕ) → motive (Lean.Grind.CommRing.Expr.natCast k))
  (h_3 : (k : ℤ) → motive (Lean.Grind.CommRing.Expr.intCast k))
  (h_4 : (x : Lean.Grind.CommRing.Var) → motive (Lean.Grind.CommRing.Expr.var x))
  (h_5 : (a b : Lean.Grind.CommRing.Expr) → motive (a.add b))
  (h_6 : (a b : Lean.Grind.CommRing.Expr) → motive (a.mul b)) (h_7 : (a : Lean.Grind.CommRing.Expr) → motive a.neg)
  (h_8 : (a b : Lean.Grind.CommRing.Expr) → motive (a.sub b))
  (h_9 : (a : Lean.Grind.CommRing.Expr) → (k : ℕ) → motive (a.pow k)) (k : ℤ),
  x = Lean.Grind.CommRing.Expr.intCast k →
    (match x with
      | Lean.Grind.CommRing.Expr.num k => h_1 k
      | Lean.Grind.CommRing.Expr.natCast k => h_2 k
      | Lean.Grind.CommRing.Expr.intCast k => h_3 k
      | Lean.Grind.CommRing.Expr.var x => h_4 x
      | a.add b => h_5 a b
      | a.mul b => h_6 a b
      | a.neg => h_7 a
      | a.sub b => h_8 a b
      | a.pow k => h_9 a k) ≍
      h_3 k
-- Mathlib.Probability.Distributions.Gaussian.IsGaussianProcess.Independence
/-- Assume that the processes $((X^t_s)_{s \in S_t})_{t \in T}$ are jointly Gaussian. Then they are
independent if for all $t_1, t_2 \in T$ with $t_1 \ne t_2$ and
$s_1 \in S_{t_1}$, $s_2 \in S_{t_2}$, $X^{t_1}_{s_1}$ and $X^{t_2}_{s_2}$ are uncorrelated.  -/
ProbabilityTheory.IsGaussianProcess.iIndepFun_of_covariance_inner : ∀ {T : Type u_1} {Ω : Type u_2} {E : Type u_3} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω}
  [inst : NormedAddCommGroup E] [inst_1 : MeasurableSpace E] [BorelSpace E] [SecondCountableTopology E]
  [CompleteSpace E] {S : T → Type u_4} {X : (t : T) → S t → Ω → E} [inst_5 : InnerProductSpace ℝ E],
  ProbabilityTheory.IsGaussianProcess (fun p ω => X p.fst p.snd ω) P →
    (∀ (t : T) (s : S t), AEMeasurable (X t s) P) →
      (∀ (t₁ t₂ : T),
          t₁ ≠ t₂ →
            ∀ (s₁ : S t₁) (s₂ : S t₂) (x y : E),
              ProbabilityTheory.covariance (fun ω => inner ℝ x (X t₁ s₁ ω)) (fun ω => inner ℝ y (X t₂ s₂ ω)) P = 0) →
        ProbabilityTheory.iIndepFun (fun t ω s => X t s ω) P
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.map_id : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.map_id._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.map_id._auto_3),
  X.map f₁ f₂ f₃ f₁ f₂ f₃ (CategoryTheory.CategoryStruct.id (CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃)) n₀ n₁ n₂ hn₁
      hn₂ =
    CategoryTheory.CategoryStruct.id (X.E f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.iSup_eq_adjoin : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] {ι : Sort u_3}
  (f : ι → IntermediateField F E), ⨆ i, f i = IntermediateField.adjoin F (⋃ i, ↑(f i))
-- Lean.Data.NameMap.Basic
Lean.NameMap.instInsertProdName : {α : Type} → Insert (Lean.Name × α) (Lean.NameMap α)
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_eq_zpow_neg_valuation : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℚ_[p]}, x ≠ 0 → ‖x‖ = ↑p ^ (-x.valuation)
-- Mathlib.LinearAlgebra.Matrix.FixedDetMatrices
_private.Mathlib.LinearAlgebra.Matrix.FixedDetMatrices.0.FixedDetMatrices.prop_red_T : ∀ {m : ℤ} {C : FixedDetMatrix (Fin 2) ℤ m → Prop},
  (∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (ModularGroup.S • B)) →
    (∀ (B : FixedDetMatrix (Fin 2) ℤ m), C B → C (ModularGroup.T • B)) →
      ∀ (B : FixedDetMatrix (Fin 2) ℤ m), C (ModularGroup.T • B) ↔ C B
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_erase_self : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {k : α}, Std.ExtDTreeMap.Const.get! (t.erase k) k = default
-- Mathlib.Probability.Martingale.Basic
MeasureTheory.Martingale.neg : ∀ {Ω : Type u_1} {E : Type u_2} {ι : Type u_3} [inst : Preorder ι] {m0 : MeasurableSpace Ω}
  {μ : MeasureTheory.Measure Ω} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] {f : ι → Ω → E}
  {ℱ : MeasureTheory.Filtration ι m0} [CompleteSpace E],
  MeasureTheory.Martingale f ℱ μ → MeasureTheory.Martingale (-f) ℱ μ
-- Mathlib.Analysis.Normed.Group.Bounded
isBounded_iff_forall_norm_le' : ∀ {E : Type u_2} [inst : SeminormedGroup E] {s : Set E}, Bornology.IsBounded s ↔ ∃ C, ∀ x ∈ s, ‖x‖ ≤ C
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CaseTrace.source : Lean.Meta.Grind.CaseTrace → Lean.Meta.Grind.SplitSource
-- Mathlib.Data.List.Fold
List.foldl_cons_eq_apply_foldl : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {v : β → α → β} {a : α} {b : β} [hv : RightCommutative v],
  List.foldl v b (a :: l) = v (List.foldl v b l) a
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.ext_iff : ∀ {R : Type u_2} {M : Type u_3} {inst : Semiring R} {inst_1 : AddCommMonoid M} {inst_2 : TopologicalSpace M}
  {inst_3 : Module R M} {x y : ClosedSubmodule R M}, x = y ↔ (↑x).carrier = (↑y).carrier
-- Mathlib.CategoryTheory.Limits.Opposites
/-- Turn a colimit for `F : J ⥤ Cᵒᵖ` into a limit for `F.leftOp : Jᵒᵖ ⥤ C`.  -/
CategoryTheory.Limits.isLimitOfCoconeOfConeLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} J] →
        (F : CategoryTheory.Functor J Cᵒᵖ) →
          {c : CategoryTheory.Limits.Cone F.leftOp} →
            CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.coconeOfConeLeftOp c) →
              CategoryTheory.Limits.IsLimit c
-- Init.Data.UInt.Bitwise
USize.not_eq_comm : ∀ {a b : USize}, ~~~a = b ↔ a = ~~~b
-- Plausible.DeriveArbitrary
/-- Creates the function definition for the derived generator  -/
_private.Plausible.DeriveArbitrary.0.Plausible.mkAuxFunction : Lean.Elab.Deriving.Context → ℕ → Lean.Elab.TermElabM Lean.Command
-- Mathlib.CategoryTheory.Monoidal.CommComon_
CategoryTheory.CommComon.comp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {R S T : CategoryTheory.CommComon C} (f : R ⟶ S) (g : S ⟶ T),
  (CategoryTheory.CategoryStruct.comp f g).hom.hom = CategoryTheory.CategoryStruct.comp f.hom.hom g.hom.hom
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.toAddMonoidHom_mulLeft : ∀ (R : Type u_14) {A : Type u_15} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] (a : A), ↑(LinearMap.mulLeft R a) = AddMonoidHom.mulLeft a
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.BuilderOption.index.injEq : ∀ (imode imode_1 : Aesop.IndexingMode),
  (Aesop.Frontend.BuilderOption.index imode = Aesop.Frontend.BuilderOption.index imode_1) = (imode = imode_1)
-- Mathlib.Topology.Algebra.Module.LinearPMap
/-- For every unbounded operator `f` the submodule `f.domain` is a core of its closure.

Note that we don't require that `f` is closable, due to the definition of the closure.  -/
LinearPMap.closureHasCore : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] (f : E →ₗ.[R] F), f.closure.HasCore f.domain
-- Batteries.Data.List.Interleave
List.interleave_flatten_flatten_of_length_eq_length : ∀ {α : Type u_1} {L₁ L₂ : List (List α)} (h₁₂ : L₁.length = L₂.length),
  (∀ (i : ℕ) (hi : i + 1 < L₁.length), L₁[i].length = L₂[i].length) →
    L₁.flatten.interleave L₂.flatten = (List.zipWith List.interleave L₁ L₂).flatten
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItem.detail? : Lean.Lsp.CompletionItem → Option String
-- Mathlib.Data.Sigma.Order
/-- The lexicographical partial order on a sigma type.  -/
Sigma.Lex.partialOrder : {ι : Type u_1} → {α : ι → Type u_2} → [Preorder ι] → [(i : ι) → PartialOrder (α i)] → PartialOrder (Σₗ (i : ι), α i)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.map_add_add_add_map : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (Q : QuadraticMap R M N) (x y z : M),
  Q (x + y + z) + (Q x + Q y + Q z) = Q (x + y) + Q (y + z) + Q (z + x)
-- Mathlib.Order.Hom.CompleteLattice
/-- Copy of a `CompleteLatticeHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
CompleteLatticeHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : CompleteLattice α] →
      [inst_1 : CompleteLattice β] → (f : CompleteLatticeHom α β) → (f' : α → β) → f' = ⇑f → CompleteLatticeHom α β
-- Mathlib.Combinatorics.SimpleGraph.Diam
SimpleGraph.eq_top_iff_forall_eccent_eq_one : ∀ {α : Type u_1} {G : SimpleGraph α} [Nontrivial α], G = ⊤ ↔ ∀ (u : α), G.eccent u = 1
-- Mathlib.Data.ULift
ULift.up_bijective : ∀ {α : Type u}, Function.Bijective ULift.up
-- Mathlib.Data.Multiset.Bind
Multiset.bind_filterMap : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} (m : Multiset α) (f : α → Option β) (g : β → Multiset γ),
  (Multiset.filterMap f m).bind g = m.bind fun a => (Option.map g (f a)).getD 0
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Poly.add.go.match_1.eq_1 : ∀ (motive : Nat.Internal.SOM.Poly → Nat.Internal.SOM.Poly → Sort u_1) (p₁ : Nat.Internal.SOM.Poly)
  (h_1 : (p₁ : Nat.Internal.SOM.Poly) → motive p₁ []) (h_2 : (p₂ : Nat.Internal.SOM.Poly) → motive [] p₂)
  (h_3 :
    (k₁ : ℕ) →
      (m₁ : Nat.Internal.SOM.Mon) →
        (p₁ : List (ℕ × Nat.Internal.SOM.Mon)) →
          (k₂ : ℕ) →
            (m₂ : Nat.Internal.SOM.Mon) →
              (p₂ : List (ℕ × Nat.Internal.SOM.Mon)) → motive ((k₁, m₁) :: p₁) ((k₂, m₂) :: p₂)),
  (match p₁, [] with
    | p₁, [] => h_1 p₁
    | [], p₂ => h_2 p₂
    | (k₁, m₁) :: p₁, (k₂, m₂) :: p₂ => h_3 k₁ m₁ p₁ k₂ m₂ p₂) =
    h_1 p₁
-- Lean.PrettyPrinter.Delaborator.Options
Lean.pp.structureInstanceTypes : Lean.Option Bool
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.addZ_of_Z_eq_zero_left : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P 2 = 0 → WeierstrassCurve.Jacobian.addZ P Q = P 0 * Q 2 * Q 2
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.exists_nat_pos_inv_lt : ∀ {b : ℝ}, 0 < b → ∃ n, 0 < n ∧ (↑n)⁻¹ < b
-- Mathlib.Data.Sym.Sym2
Sym2.lift_map_apply : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {g : γ → α} (f : { f // ∀ (a₁ a₂ : α), f a₁ a₂ = f a₂ a₁ }) (p : Sym2 γ),
  Sym2.lift f (Sym2.map g p) = Sym2.lift ⟨fun c₁ c₂ => ↑f (g c₁) (g c₂), ⋯⟩ p
-- Init.Data.List.Basic
/-- Returns the first element of a non-empty list.
 -/
List.head : {α : Type u} → (as : List α) → as ≠ [] → α
-- Std.Async.Select
Std.Async.Selectable.case.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] {β : Type} (selector : Std.Async.Selector β) (cont : β → Std.Async.Async α),
  sizeOf { β := β, selector := selector, cont := cont } = 1 + sizeOf β + sizeOf selector
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousAt_iff_limsup_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {γ : Type u_4} [inst_1 : CompleteLinearOrder γ] {f : α → γ},
  UpperSemicontinuousAt f x ↔ Filter.limsup f (nhds x) ≤ f x
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.instHasForget₂SubtypeNormedAddGroupHomCarrierNormNonincSemiNormedGrpCarrier : CategoryTheory.HasForget₂ SemiNormedGrp₁ SemiNormedGrp
-- Lean.Attributes
Lean.registerAttributeImplBuilder : Lean.Name → Lean.AttributeImplBuilder → IO Unit
-- Mathlib.Analysis.Normed.Affine.Isometry
AffineIsometryEquiv.coe_constVSub : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_10} [inst : NormedField 𝕜] [inst_1 : SeminormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : PseudoMetricSpace P] [inst_4 : NormedAddTorsor V P] (p : P),
  ⇑(AffineIsometryEquiv.constVSub 𝕜 p) = fun x => p -ᵥ x
-- Mathlib.Combinatorics.SimpleGraph.Ends.Defs
/-- The induced graph on the vertices `C`.  -/
SimpleGraph.ComponentCompl.coeGraph : {V : Type u} → {G : SimpleGraph V} → {K : Set V} → (C : G.ComponentCompl K) → SimpleGraph ↥C
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.evariance_mul : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} (c : ℝ) (X : Ω → ℝ) (μ : MeasureTheory.Measure Ω),
  ProbabilityTheory.evariance (fun ω => c * X ω) μ = ENNReal.ofReal (c ^ 2) * ProbabilityTheory.evariance X μ
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.involutiveNeg : {α : Type u_2} → [InvolutiveNeg α] → InvolutiveNeg (Set α)
-- Mathlib.Data.DFinsupp.Lex
DFinsupp.Colex.le_iff_of_unique : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : (i : ι) → Zero (α i)] [inst_1 : LinearOrder ι] [inst_2 : Unique ι]
  [inst_3 : (i : ι) → PartialOrder (α i)] {x y : Colex (Π₀ (i : ι), α i)},
  x ≤ y ↔ (ofColex x) default ≤ (ofColex y) default
-- Mathlib.Tactic.FieldSimp.Lemmas
/-- Given an expression `y : Q($M)` with specified sign (either + or -), construct a proof that
the negation of (± `y`) (here taking the specified sign) is ∓ `y`.  -/
Mathlib.Tactic.FieldSimp.Sign.neg : {v : Lean.Level} →
  {M : Q(Type v)} →
    (iM : Q(Field «$M»)) →
      (y : Q(«$M»)) →
        (g : Mathlib.Tactic.FieldSimp.Sign M) →
          Lean.MetaM
            ((G : Mathlib.Tactic.FieldSimp.Sign M) ×
              have a := G.expr y;
              have a_1 := g.expr y;
              Q(-«$a_1» = «$a»))
-- Mathlib.Order.Filter.CountableInter
instCountableInterFilterMap : ∀ {α : Type u_2} {β : Type u_3} (l : Filter α) [CountableInterFilter l] (f : α → β),
  CountableInterFilter (Filter.map f l)
-- Mathlib.Probability.Independence.Basic
/-- A family of sets is independent if the family of measurable space structures they generate is
independent. For a set `s`, the generated measurable space has measurable sets `∅, s, sᶜ, univ`.  -/
ProbabilityTheory.iIndepSet : {Ω : Type u_1} →
  {ι : Type u_2} →
    {_mΩ : MeasurableSpace Ω} →
      (ι → Set Ω) → autoParam (MeasureTheory.Measure Ω) ProbabilityTheory.iIndepSet._auto_1 → Prop
-- Mathlib.AlgebraicTopology.AlternatingFaceMapComplex
AlgebraicTopology.AlternatingFaceMapComplex.map_f : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X Y : CategoryTheory.SimplicialObject C} (f : X ⟶ Y) (n : ℕ),
  (AlgebraicTopology.AlternatingFaceMapComplex.map f).f n = f.app (Opposite.op { len := n })
-- Mathlib.RingTheory.PowerSeries.Ideal
/-- Given an ideal `I` of `R⟦X⟧` such that `X ∈ I`, if `I.map constantCoeff` is generated by
`S : Set T`, then `I` is generated by `insert X (C '' S)`.  -/
PowerSeries.eq_span_insert_X_of_X_mem_of_span_eq : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal (PowerSeries R)} {S : Set R},
  PowerSeries.X ∈ I →
    Ideal.span S = Ideal.map PowerSeries.constantCoeff I → I = Ideal.span (insert PowerSeries.X (⇑PowerSeries.C '' S))
-- Mathlib.Data.Fin.VecNotation
Matrix.vecAppend.eq_1 : ∀ {m n : ℕ} {α : Type u_1} {o : ℕ} (ho : o = m + n) (u : Fin m → α) (v : Fin n → α),
  Matrix.vecAppend ho u v = Fin.append u v ∘ Fin.cast ho
-- Mathlib.Analysis.Convex.Jensen
ConvexOn.bddAbove_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : AddCommGroup β] [inst_5 : LinearOrder β] [IsOrderedAddMonoid β]
  [inst_7 : Module 𝕜 E] [inst_8 : Module 𝕜 β] [IsStrictOrderedModule 𝕜 β] {f : E → β} {s t : Set E},
  s ⊆ t → ConvexOn 𝕜 t f → BddAbove (f '' s) → BddAbove (f '' (convexHull 𝕜) s)
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_toIocMod : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a₁ a₂ b : α), toIocMod hp a₁ (toIocMod hp a₂ b) = toIocMod hp a₁ b
-- Mathlib.CategoryTheory.Category.Cat
/-- Any isomorphism in `Cat` induces an equivalence of the underlying categories.  -/
CategoryTheory.Cat.equivOfIso : {C D : CategoryTheory.Cat} → (C ≅ D) → (↑C ≌ ↑D)