mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Covering.Quotient
IsQuotientCoveringMap.toContinuousConstSMul : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {G : Type u_3}
  [inst_2 : Group G] [inst_3 : MulAction G E], IsQuotientCoveringMap f G → ContinuousConstSMul G E
-- Mathlib.Order.SuccPred.Limit
Order.isPredPrelimitRecOn.eq_1 : ∀ {α : Type u_1} (b : α) {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : PredOrder α]
  (succ : (a : α) → ¬IsMin a → motive (Order.pred a)) (isSuccPrelimit : (a : α) → Order.IsPredPrelimit a → motive a),
  Order.isPredPrelimitRecOn b succ isSuccPrelimit =
    if hb : Order.IsPredPrelimit b then isSuccPrelimit b hb else cast ⋯ (succ (Classical.choose ⋯) ⋯)
-- Mathlib.Order.Lattice
le_sup_inf : ∀ {α : Type u} [inst : DistribLattice α] {x y z : α}, (x ⊔ y) ⊓ (x ⊔ z) ≤ x ⊔ y ⊓ z
-- Mathlib.Algebra.Order.Group.Pointwise.CompleteLattice
sInf_sub : ∀ {M : Type u_1} [inst : CompleteLattice M] [inst_1 : AddGroup M] [AddLeftMono M] [AddRightMono M] (s t : Set M),
  sInf (s - t) = sInf s - sSup t
-- Mathlib.Algebra.Polynomial.Derivation
/-- For a derivation `d : A → M` and an element `a : A`, `d.compAEval a` is the
derivation of `R[X]` which takes a polynomial `f` to `d(aeval a f)`.

This derivation takes values in `Module.AEval R M a`, which is `M`, regarded as an
`R[X]`-module, with the action of a polynomial `f` defined by `f • m = (aeval a f) • m`.
 -/
Derivation.compAEval : {R : Type u_1} →
  {A : Type u_2} →
    {M : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : AddCommMonoid M] →
              [inst_4 : Module A M] →
                [inst_5 : Module R M] →
                  [inst_6 : IsScalarTower R A M] →
                    Derivation R A M → (a : A) → Derivation R (Polynomial R) (Module.AEval R M a)
-- Mathlib.Data.Multiset.Range
Multiset.range_disjoint_map_add : ∀ (a : ℕ) (m : Multiset ℕ), Disjoint (Multiset.range a) (Multiset.map (fun x => a + x) m)
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
Finset.sum_sdiff_ne_sum_sdiff_iff : ∀ {ι : Type u_1} {M : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCancelCommMonoid M] {s t : Finset ι} {f : ι → M},
  ∑ i ∈ s \ t, f i ≠ ∑ i ∈ t \ s, f i ↔ ∑ i ∈ s, f i ≠ ∑ i ∈ t, f i
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_bitVecToNat : ∀ (n : BitVec 16), UInt16.ofNatLT n.toNat ⋯ = { toBitVec := n }
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Twice the angle between two multiples of a vector is 0.  -/
Orientation.two_zsmul_oangle_smul_smul_self : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x : V) {r₁ r₂ : ℝ}, 2 • o.oangle (r₁ • x) (r₂ • x) = 0
-- Mathlib.Algebra.Order.Archimedean.Basic
le_iff_forall_lt_rat_imp_le : ∀ {K : Type u_4} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] [Archimedean K] {x y : K},
  x ≤ y ↔ ∀ (q : ℚ), y < ↑q → x ≤ ↑q
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- The monomial symmetric `MvPolynomial σ R` with exponent set μ.
It is the sum over all the monomials in `MvPolynomial σ R` such that
the multiset of exponents is equal to the multiset of parts of μ.  -/
MvPolynomial.msymm : (σ : Type u_5) →
  (R : Type u_6) → [inst : CommSemiring R] → [Fintype σ] → [DecidableEq σ] → {n : ℕ} → n.Partition → MvPolynomial σ R
-- Mathlib.RingTheory.Derivation.Basic
Derivation.leibniz_of_mul_eq_one : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_2} [inst_1 : CommRing A] [inst_2 : Algebra R A] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module A M] [inst_5 : Module R M] (D : Derivation R A M) {a b : A},
  a * b = 1 → D a = -a ^ 2 • D b
-- Mathlib.Topology.Algebra.Monoid
ContinuousOn.fun_nsmul : ∀ {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M] [inst_2 : AddMonoid M]
  [ContinuousAdd M] {f : X → M} {s : Set X}, ContinuousOn f s → ∀ (n : ℕ), ContinuousOn (fun i => n • f i) s
-- Mathlib.Data.Finite.Prod
Set.Finite.image2 : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} (f : α → β → γ),
  s.Finite → t.Finite → (Set.image2 f s t).Finite
-- Batteries.Data.List.Basic
/-- Two cons lists are related by `Forall₂ R`
if the heads are related by `R` and the tails are related by `Forall₂ R`  -/
List.Forall₂.cons : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a : α} {b : β} {l₁ : List α} {l₂ : List β},
  R a b → List.Forall₂ R l₁ l₂ → List.Forall₂ R (a :: l₁) (b :: l₂)
-- Mathlib.Algebra.GroupWithZero.Basic
/-- A reduced structure has no nonzero nilpotent elements.  -/
IsReduced.eq_zero : ∀ {R : Type u_5} {inst : Zero R} {inst_1 : Pow R ℕ} [self : IsReduced R] (x : R), IsNilpotent x → x = 0
-- Mathlib.Data.PFunctor.Multivariate.W
/-- W-types are functorial  -/
MvPFunctor.wMap : {n : ℕ} → (P : MvPFunctor.{u} (n + 1)) → {α β : TypeVec.{u} n} → α.Arrow β → P.W α → P.W β
-- Mathlib.Topology.Order.OrderClosed
disjoint_nhds_atTop : ∀ {α : Type u} [inst : Preorder α] [NoTopOrder α] [inst_2 : TopologicalSpace α] [ClosedIciTopology α] (a : α),
  Disjoint (nhds a) Filter.atTop
-- Mathlib.Data.Set.Prod
Set.mk_preimage_prod_left_eq_empty : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {b : β}, b ∉ t → (fun a => (a, b)) ⁻¹' s ×ˢ t = ∅
-- Mathlib.Data.List.Triplewise
/-- Whether a predicate holds for all ordered triples of elements of a list.  -/
List.Triplewise : {α : Type u_1} → (α → α → α → Prop) → List α → Prop
-- Mathlib.LinearAlgebra.Matrix.DotProduct
/-- Note that this applies to `ℂ` via `RCLike.toStarOrderedRing`.  -/
dotProduct_self_star_nonneg : ∀ {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : PartialOrder R] [inst_2 : NonUnitalRing R]
  [inst_3 : StarRing R] [StarOrderedRing R] (v : n → R), 0 ≤ v ⬝ᵥ star v
-- Mathlib.Combinatorics.Additive.Convolution
Finset.card_smul_inter : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  (x • A ∩ B).card = A.convolution B⁻¹ x⁻¹
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.ext_keys_unit : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {t₁ t₂ : Std.ExtTreeMap α Unit cmp},
  t₁.keys.Perm t₂.keys → t₁ = t₂
-- Mathlib.Analysis.InnerProductSpace.Dual
_private.Mathlib.Analysis.InnerProductSpace.Dual.0.InnerProductSpace.«term_†» : Lean.TrailingParserDescr
-- Mathlib.Data.List.SplitBy
_private.Mathlib.Data.List.SplitBy.0.List.isChain_getLast_head_splitByLoop : ∀ {α : Type u_1} {r : α → α → Bool} (l : List α) {a : α} {g : List α} {gs : List (List α)},
  [] ∉ gs →
    List.IsChain (fun b a => ∃ (ha : a ≠ []) (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false) gs →
      (∀ m ∈ gs.head?,
          ∃ (ha : m ≠ []) (hb : g.reverse ++ [a] ≠ []), r (m.getLast ha) ((g.reverse ++ [a]).head hb) = false) →
        List.IsChain (fun a b => ∃ (ha : a ≠ []) (hb : b ≠ []), r (a.getLast ha) (b.head hb) = false)
          (List.splitBy.loop r l a g gs)
-- Lean.Elab.DefView
Lean.Elab.DefView.deriving? : Lean.Elab.DefView → Option (Array Lean.Syntax)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
Topology.IsOpenEmbedding.measurableEmbedding : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [mα : MeasurableSpace α] [BorelSpace α]
  [mβ : TopologicalSpace β] [inst_2 : MeasurableSpace β] [BorelSpace β] {f : α → β},
  Topology.IsOpenEmbedding f → MeasurableEmbedding f
-- Mathlib.NumberTheory.PrimeCounting
Nat.primeCounting_sub_one : ∀ (n : ℕ), (n - 1).primeCounting = n.primeCounting'
-- Mathlib.Data.Nat.Init
_private.Mathlib.Data.Nat.Init.0.Nat.pincerRecursion.match_1.eq_1 : ∀ (motive : ℕ → ℕ → Sort u_1) (m : ℕ) (h_1 : (m : ℕ) → motive m 0) (h_2 : (n : ℕ) → motive 0 n)
  (h_3 : (n n_1 : ℕ) → motive n.succ n_1.succ),
  (match m, 0 with
    | m, 0 => h_1 m
    | 0, n => h_2 n
    | n.succ, n_1.succ => h_3 n n_1) =
    h_1 m
-- Mathlib.Order.CompleteLattice.Basic
iSup_subtype'' : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} (s : Set ι) (f : ι → α), ⨆ i, f ↑i = ⨆ t ∈ s, f t
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mdifferentiableWithinAt_prod_module_iff : ∀ {𝕜 : 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} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F₁ : Type u_17} [inst_6 : NormedAddCommGroup F₁]
  [inst_7 : NormedSpace 𝕜 F₁] {F₂ : Type u_18} [inst_8 : NormedAddCommGroup F₂] [inst_9 : NormedSpace 𝕜 F₂] {s : Set M}
  {x : M} (f : M → F₁ × F₂), MDiffAt[s] f x ↔ MDiffAt[s] (Prod.fst ∘ f) x ∧ MDiffAt[s] (Prod.snd ∘ f) x
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.insertMany_list_singleton : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, t.insertMany [(k, v)] = t.insert k v
-- Mathlib.Data.ULift
PLift.up_bijective : ∀ {α : Sort u}, Function.Bijective PLift.up
-- Mathlib.Geometry.Convex.Cone.Basic
ConvexCone.instInhabited : {R : Type u_2} →
  {M : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] → [inst_2 : AddCommMonoid M] → [inst_3 : SMul R M] → Inhabited (ConvexCone R M)
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Biproducts
/-- The composition in the opposite direction is equal to the identity if and only if `F` preserves
the biproduct, see `preservesBiproduct_of_monoBiproductComparison`.  -/
CategoryTheory.Functor.biproductComparison'_comp_biproductComparison_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {J : Type w₁}
  (F : CategoryTheory.Functor C D) (f : J → C) [inst_4 : CategoryTheory.Limits.HasBiproduct f]
  [inst_5 : CategoryTheory.Limits.HasBiproduct (F.obj ∘ f)] [F.PreservesZeroMorphisms] {Z : D} (h : ⨁ F.obj ∘ f ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.biproductComparison' f)
      (CategoryTheory.CategoryStruct.comp (F.biproductComparison f) h) =
    h
-- Mathlib.Tactic.LinearCombinationPrime
Mathlib.Tactic.LinearCombinationPrime.Expanded.proof.sizeOf_spec : ∀ (pf : Lean.Term), sizeOf (Mathlib.Tactic.LinearCombinationPrime.Expanded.proof pf) = 1 + sizeOf pf
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.symm_commRingEquiv : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N],
  MonoidAlgebra.commRingEquiv.symm = MonoidAlgebra.commRingEquiv
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.restrict_isLoop_iff : ∀ {α : Type u_1} {M : Matroid α} {e : α} {R : Set α}, (M.restrict R).IsLoop e ↔ e ∈ R ∧ (M.IsLoop e ∨ e ∉ M.E)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instVAdd : {β : Type u_2} → {α : Type u_1} → [VAdd β α] → VAdd β (Lex α)
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instIsScalarTower : ∀ {S : Type u_1} {T : Type u_2} {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] [inst_5 : Monoid S]
  [inst_6 : Monoid T] [inst_7 : DistribMulAction S N] [inst_8 : DistribMulAction T N] [inst_9 : SMulCommClass S R N]
  [inst_10 : SMulCommClass T R N] [inst_11 : SMul S T] [IsScalarTower S T N], IsScalarTower S T (QuadraticMap R M N)
-- Mathlib.Computability.Ackermann
max_ack_left : ∀ (m₁ m₂ n : ℕ), ack (max m₁ m₂) n = max (ack m₁ n) (ack m₂ n)
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.coe_mk_contLinear_eq_linear : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} {Q : Type u_5} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace Q] [inst_8 : AddTorsor W Q] [inst_9 : TopologicalSpace V]
  [inst_10 : IsTopologicalAddTorsor P] [inst_11 : TopologicalSpace W] [inst_12 : IsTopologicalAddTorsor Q]
  (f : P →ᵃ[R] Q) (h : Continuous f.toFun), ⇑{ toAffineMap := f, cont := h }.contLinear = ⇑f.linear
-- Mathlib.Analysis.Complex.UpperHalfPlane.Topology
UpperHalfPlane.comp_ofComplex : ∀ (f : UpperHalfPlane → ℂ) (z : UpperHalfPlane), (f ∘ ↑UpperHalfPlane.ofComplex) ↑z = f z
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.addCommGroup : {R : Type u_1} → {M : Type u_4} → [inst : Ring R] → AddCommGroup (AddMonoidAlgebra R M)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
AlgebraicGeometry.Proj.instQuasiCompactToSpecZeroOfFiniteTypeSubtypeMemOfNatNat : ∀ {σ : Type u_1} {A : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] [Algebra.FiniteType (↥(𝒜 0)) A],
  AlgebraicGeometry.QuasiCompact (AlgebraicGeometry.Proj.toSpecZero 𝒜)
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.insertMany_append : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {l₁ l₂ : List α}, m.insertMany (l₁ ++ l₂) = (m.insertMany l₁).insertMany l₂
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Equiv.diff_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ m₃ : Std.DHashMap.Internal.Raw₀ α β}
  [EquivBEq α] [LawfulHashable α],
  (↑m₁).WF → (↑m₂).WF → (↑m₃).WF → (↑m₂).Equiv ↑m₃ → (↑(m₁.diff m₂)).Equiv ↑(m₁.diff m₃)
-- Mathlib.Geometry.Euclidean.Angle.Sphere
/-- **Thales' theorem**: For three distinct points, the angle at the second point
is a right angle if and only if the second point lies on the sphere having the first and third
points as diameter endpoints.  -/
EuclideanGeometry.Sphere.angle_eq_pi_div_two_iff_mem_sphere_ofDiameter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  EuclideanGeometry.angle p₁ p₂ p₃ = Real.pi / 2 ↔ p₂ ∈ EuclideanGeometry.Sphere.ofDiameter p₁ p₃
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.ToTerm.Kind.regular.sizeOf_spec : sizeOf Lean.Elab.Term.Do.ToTerm.Kind.regular = 1
-- Mathlib.RingTheory.Kaehler.Basic
KaehlerDifferential.kerToTensor_apply : ∀ (R : Type u) [inst : CommRing R] (A : Type u_2) (B : Type u_3) [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra A B] (x : ↥(RingHom.ker (algebraMap A B))),
  (KaehlerDifferential.kerToTensor R A B) x = 1 ⊗ₜ[A] (KaehlerDifferential.D R A) ↑x
-- Mathlib.Algebra.Algebra.Equiv
RingEquiv.toIntAlgEquiv_apply : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R ≃+* S) (a : R), f.toIntAlgEquiv a = f a
-- Mathlib.AlgebraicGeometry.ColimitsOver
AlgebraicGeometry.Scheme.Cover.ColimitGluingData.gluedCocone_pt : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [inst : P.IsStableUnderBaseChange]
  [inst_1 : P.IsMultiplicative] {S : AlgebraicGeometry.Scheme} {J : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} J] {D : CategoryTheory.Functor J (P.Over ⊤ S)} {𝒰 : S.OpenCover}
  [inst_3 : CategoryTheory.Category.{v_2, u_2} 𝒰.I₀] [inst_4 : AlgebraicGeometry.Scheme.Cover.LocallyDirected 𝒰]
  (d : AlgebraicGeometry.Scheme.Cover.ColimitGluingData D 𝒰)
  [inst_5 :
    ∀ {i j : 𝒰.I₀} (hij : i ⟶ j),
      CategoryTheory.Limits.PreservesColimitsOfShape J
        (CategoryTheory.MorphismProperty.Over.pullback P ⊤ (AlgebraicGeometry.Scheme.Cover.trans 𝒰 hij))]
  [inst_6 : Quiver.IsThin 𝒰.I₀] [inst_7 : Small.{u, u_2} 𝒰.I₀] [inst_8 : AlgebraicGeometry.IsZariskiLocalAtTarget P],
  d.gluedCocone.pt = d.glued
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
IsTopologicalGroup.tendstoLocallyUniformlyOn_iff : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Group G] [u : UniformSpace G] [inst_1 : IsTopologicalGroup G]
  [inst_2 : TopologicalSpace α] (F : ι → α → G) (f : α → G) (p : Filter ι) (s : Set α),
  IsTopologicalGroup.rightUniformSpace G = u →
    (TendstoLocallyUniformlyOn F f p s ↔
      ∀ u_1 ∈ nhds 1, ∀ x ∈ s, ∃ t ∈ nhdsWithin x s, ∀ᶠ (i : ι) in p, ∀ a ∈ t, F i a / f a ∈ u_1)
-- Init.Data.Array.Perm
Array.instTransPerm : {α : Type u_1} → Trans Array.Perm Array.Perm Array.Perm
-- Mathlib.Data.Nat.Multiplicity
_private.Mathlib.Data.Nat.Multiplicity.0.Nat.factorial.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Std.Internal.UV.System
Std.Internal.UV.System.CPUInfo.mk.sizeOf_spec : ∀ (model : String) (speed : UInt64) (times : Std.Internal.UV.System.CPUTimes),
  sizeOf { model := model, speed := speed, times := times } = 1 + sizeOf model + sizeOf speed + sizeOf times
-- Mathlib.Data.EReal.Inv
EReal.inv_top : ⊤⁻¹ = 0
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.relations_R : ∀ (R : Type u) [inst : CommRing R] (ι : Type u_4) [inst_1 : DecidableEq ι] (M : Type u_5) [inst_2 : AddCommGroup M]
  [inst_3 : Module R M], (exteriorPower.presentation.relations R ι M).R = exteriorPower.presentation.Rels R ι M
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey_maxKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [inst : Std.TransCmp cmp] (h : t.WF)
  {km : α} {hc : t.contains km = true}, t.maxKey?.get ⋯ = km → t.getKey km hc = km
-- Mathlib.Topology.MetricSpace.Infsep
Set.Finite.infsep_pos_iff_nontrivial : ∀ {α : Type u_1} [inst : MetricSpace α] {s : Set α}, s.Finite → (0 < s.infsep ↔ s.Nontrivial)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.maxKeyD_modify : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {f : β → β},
  (Std.DTreeMap.Const.modify t k f).isEmpty = false →
    ∀ {fallback : α},
      (Std.DTreeMap.Const.modify t k f).maxKeyD fallback =
        if cmp (t.maxKeyD fallback) k = Ordering.eq then k else t.maxKeyD fallback
-- Mathlib.CategoryTheory.Monad.Adjunction
CategoryTheory.Coreflective.comparison_essSurj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {R : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Coreflective R],
  (CategoryTheory.Comonad.comparison (CategoryTheory.coreflectorAdjunction R)).EssSurj
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.inhabited : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] → [inst_1 : Inhabited T] → Inhabited (CategoryTheory.Over default)
-- Init.Data.String.Basic
ByteArray.utf8Decode?.go.induct_unfolding : ∀ (b : ByteArray) (motive : (i : ℕ) → Array Char → i ≤ b.size → Option (Array Char) → Prop),
  (∀ (i : ℕ) (acc : Array Char) (hi : i ≤ b.size), i < b.size → b.utf8DecodeChar? i = none → motive i acc hi none) →
    (∀ (i : ℕ) (acc : Array Char) (hi : i ≤ b.size),
        i < b.size →
          ∀ (c : Char) (h : b.utf8DecodeChar? i = some c),
            motive (i + c.utf8Size) (acc.push c) ⋯ (ByteArray.utf8Decode?.go b (i + c.utf8Size) (acc.push c) ⋯) →
              motive i acc hi (ByteArray.utf8Decode?.go b (i + c.utf8Size) (acc.push c) ⋯)) →
      (∀ (i : ℕ) (acc : Array Char) (hi : i ≤ b.size), ¬i < b.size → motive i acc hi (some acc)) →
        ∀ (i : ℕ) (acc : Array Char) (hi : i ≤ b.size), motive i acc hi (ByteArray.utf8Decode?.go b i acc hi)
-- Mathlib.Topology.Gluing
TopCat.GlueData.range_fromOpenSubsetsGlue : ∀ {α : Type u} [inst : TopologicalSpace α] {J : Type u} (U : J → TopologicalSpace.Opens α),
  Set.range ⇑(CategoryTheory.ConcreteCategory.hom (TopCat.GlueData.fromOpenSubsetsGlue U)) = ⋃ i, ↑(U i)
-- Lean.Parser.Term
Lean.Parser.Term.showTermElabImpl.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Galois.Topology
/-- If `G` is a functor of categories of finite types, the induced map `Aut F → Aut (F ⋙ G)` is
continuous.  -/
CategoryTheory.PreGaloisCategory.continuous_mapAut_whiskeringRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat)
  (G : CategoryTheory.Functor FintypeCat FintypeCat),
  Continuous ⇑(CategoryTheory.Functor.mapAut F ((CategoryTheory.Functor.whiskeringRight C FintypeCat FintypeCat).obj G))
-- Mathlib.RingTheory.MvPolynomial.IrreducibleQuadratic
MvPolynomial.sumSMulX.eq_1 : ∀ {n : Type u_1} {R : Type u_2} [inst : CommRing R], MvPolynomial.sumSMulX = Finsupp.linearCombination R MvPolynomial.X
-- Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
Set.preimage_smul : ∀ {α : Type u_2} {β : Type u_3} [inst : Group α] [inst_1 : MulAction α β] (a : α) (t : Set β),
  (fun x => a • x) ⁻¹' t = a⁻¹ • t
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.instInhabitedBVBit : Inhabited Std.Tactic.BVDecide.BVBit
-- Mathlib.ModelTheory.Algebra.Ring.Basic
/-- Addition in the `Language.ring.Structure` is the same as the addition given by the
`Add` instance  -/
FirstOrder.Ring.CompatibleRing.funMap_add : ∀ {R : Type u_2} {inst : Add R} {inst_1 : Mul R} {inst_2 : Neg R} {inst_3 : One R} {inst_4 : Zero R}
  [self : FirstOrder.Ring.CompatibleRing R] (x : Fin 2 → R),
  FirstOrder.Language.Structure.funMap FirstOrder.Ring.addFunc x = x 0 + x 1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.coprod.symmetry' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C]
  (P Q : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl)
      (CategoryTheory.Limits.coprod.desc CategoryTheory.Limits.coprod.inr CategoryTheory.Limits.coprod.inl) =
    CategoryTheory.CategoryStruct.id (P ⨿ Q)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.braiding'_hom : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (P Q : C),
  (CategoryTheory.Limits.biprod.braiding' P Q).hom =
    CategoryTheory.Limits.biprod.desc CategoryTheory.Limits.biprod.inr CategoryTheory.Limits.biprod.inl
-- Mathlib.Algebra.Free
/-- Lifts a function `α → β` to a magma homomorphism `FreeMagma α → β` given a magma `β`.  -/
FreeMagma.liftAux : {α : Type u} → {β : Type v} → [Mul β] → (α → β) → FreeMagma α → β
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.coe_nonneg : ∀ {x : ℝ}, 0 ≤ ↑x ↔ 0 ≤ x
-- Mathlib.CategoryTheory.Limits.Yoneda
CategoryTheory.coyonedaFunctor_preservesLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Limits.PreservesLimitsOfSize.{t, w, v, max u v, u, max u (v + 1)} CategoryTheory.coyoneda
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.any_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  {p : α → β → Bool}, t₁.Equiv t₂ → t₁.any p = t₂.any p
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.mem.match_1.eq_2 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.eq)
  (h_3 : Unit → motive Ordering.gt),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.eq => h_2 ()
    | Ordering.gt => h_3 ()) =
    h_2 ()
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.cotangentToQuotientSquare_injective : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R), Function.Injective ⇑I.cotangentToQuotientSquare
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
/-- The natural isomorphism of bifunctors `F - ⊗ F - ≅ F (- ⊗ -)`, given a monoidal functor `F`.  -/
CategoryTheory.MonoidalCategory.Functor.curriedTensorPreIsoPost : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u_2} →
        [inst_2 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_3 : CategoryTheory.MonoidalCategory D] →
            (F : CategoryTheory.Functor C D) →
              [F.Monoidal] →
                CategoryTheory.MonoidalCategory.curriedTensorPre F ≅ CategoryTheory.MonoidalCategory.curriedTensorPost F