mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.rightAngleRotationAux₁_def : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)),
  o.rightAngleRotationAux₁ =
    have to_dual := (InnerProductSpace.toDual ℝ E).toLinearEquiv ≪≫ₗ LinearMap.toContinuousLinearMap.symm;
    ↑to_dual.symm ∘ₗ o.areaForm
-- Mathlib.Topology.Sheaves.CommRingCat
/-- The map into the presheaf of total quotient rings  -/
TopCat.Presheaf.toTotalQuotientPresheaf : {X : TopCat} → (F : TopCat.Presheaf CommRingCat X) → F ⟶ F.totalQuotientPresheaf
-- Mathlib.Algebra.GradedMonoid
/-- The index used by `List.dProd`. Propositionally this is equal to `(l.map fι).Sum`, but
definitionally it needs to have a different form to avoid introducing `Eq.rec`s in `List.dProd`.  -/
List.dProdIndex : {ι : Type u_1} → {α : Type u_2} → [AddMonoid ι] → List α → (α → ι) → ι
-- Mathlib.Algebra.Order.Hom.Basic
/-- the image of a product is less or equal than the sum of the images.  -/
MulLEAddHomClass.map_mul_le_add : ∀ {F : Type u_7} {α : outParam (Type u_8)} {β : outParam (Type u_9)} {inst : Mul α} {inst_1 : Add β} {inst_2 : LE β}
  {inst_3 : FunLike F α β} [self : MulLEAddHomClass F α β] (f : F) (a b : α), f (a * b) ≤ f a + f b
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- The norm, relative to `ℤ`, of `ζ - 1` in a `p ^ (k + 1)`-th cyclotomic extension of `ℚ` is
a prime if `p ≠ 2`.  -/
IsPrimitiveRoot.prime_norm_toInteger_sub_one_of_prime_ne_two : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  p ≠ 2 → Prime ((Algebra.norm ℤ) (hζ.toInteger - 1))
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat_natCast : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv] (n : ℕ), CauSeq.Completion.ofRat ↑n = ↑n
-- Mathlib.Data.Finsupp.Single
Finsupp.single_apply : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a a' : α} {b : M} [inst_1 : Decidable (a = a')],
  (fun₀ | a => b) a' = if a = a' then b else 0
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
SubMulAction.conjMap_ofFixingSubgroup.eq_1 : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s t : Set α} {g : M} (hg : g • t = s),
  SubMulAction.conjMap_ofFixingSubgroup hg =
    {
      toFun := fun x =>
        match x with
        | ⟨x, hx⟩ => ⟨g • x, ⋯⟩,
      map_smul' := ⋯ }
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ'_three : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R), W.preΨ' 3 = W.Ψ₃
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
/-- The underlying structure which gives a pairing for
`Subcomplex.unionProd Λ[m + 1, k.castSucc] ∂Δ[n]`
when `k : Fin (m + 1)` and `n : ℕ`.  -/
SSet.prodStdSimplex.pairingCore : {m : ℕ} → (k : Fin (m + 1)) → (n : ℕ) → ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).PairingCore
-- Std.Http.Protocol.H1.Reader
Std.Http.Protocol.H1.Reader.instInhabitedBodyState : Inhabited Std.Http.Protocol.H1.Reader.BodyState
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.comm₁ : ∀ {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]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (self : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃),
  CategoryTheory.CategoryStruct.comp v₁₂ self.m₁ = CategoryTheory.CategoryStruct.comp u₂₃ v₁₃
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.whiskerLeft_μ_comp_μ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
      (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.obj Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z)
          (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).hom)))
-- Mathlib.Probability.StrongLaw
/-- Preliminary lemma for the strong law of large numbers for vector-valued random variables:
the composition of the random variables with a simple function satisfies the strong law of large
numbers.  -/
ProbabilityTheory.strong_law_ae_simpleFunc_comp : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure μ]
  {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] [inst_3 : MeasurableSpace E]
  (X : ℕ → Ω → E),
  Measurable (X 0) →
    Pairwise (Function.onFun (fun x1 x2 => ProbabilityTheory.IndepFun x1 x2 μ) X) →
      (∀ (i : ℕ), ProbabilityTheory.IdentDistrib (X i) (X 0) μ μ) →
        ∀ (φ : MeasureTheory.SimpleFunc E E),
          ∀ᵐ (ω : Ω) ∂μ,
            Filter.Tendsto (fun n => (↑n)⁻¹ • ∑ i ∈ Finset.range n, φ (X i ω)) Filter.atTop
              (nhds (∫ (x : Ω), (⇑φ ∘ X 0) x ∂μ))
-- Mathlib.Topology.UniformSpace.Equiv
/-- Product of two uniform isomorphisms.  -/
UniformEquiv.prodCongr : {α : Type u} →
  {β : Type u_1} →
    {γ : Type u_2} →
      {δ : Type u_3} →
        [inst : UniformSpace α] →
          [inst_1 : UniformSpace β] →
            [inst_2 : UniformSpace γ] → [inst_3 : UniformSpace δ] → α ≃ᵤ β → γ ≃ᵤ δ → α × γ ≃ᵤ β × δ
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_increaseBy : ∀ {p : String.Pos.Raw} {n : ℕ}, (p.increaseBy n).byteIdx = p.byteIdx + n
-- Mathlib.Data.WSeq.Relation
_private.Mathlib.Data.WSeq.Relation.0.Stream'.WSeq.LiftRelO.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Option (α × Stream'.WSeq α) → Option (β × Stream'.WSeq β) → Sort u_3)
  (h_1 : Unit → motive none none)
  (h_2 : (a : α) → (s : Stream'.WSeq α) → (b : β) → (t : Stream'.WSeq β) → motive (some (a, s)) (some (b, t)))
  (h_3 : (x : Option (α × Stream'.WSeq α)) → (x_1 : Option (β × Stream'.WSeq β)) → motive x x_1),
  (match none, none with
    | none, none => h_1 ()
    | some (a, s), some (b, t) => h_2 a s b t
    | x, x_1 => h_3 x x_1) =
    h_1 ()
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.isOpen_iff_of_mem' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set (OnePoint X)},
  OnePoint.infty ∈ s → (IsOpen s ↔ IsCompact (OnePoint.some ⁻¹' s)ᶜ ∧ IsOpen (OnePoint.some ⁻¹' s))
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.dropPrefix?_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String},
  s.toSlice.dropPrefix? pat = s.dropPrefix? pat
-- Mathlib.Algebra.Ring.Defs
NonUnitalNonAssocSemiring.toDistrib : {α : Type u} → [self : NonUnitalNonAssocSemiring α] → Distrib α
-- Batteries.Recycling.RBTree.WF
_private.Batteries.Recycling.RBTree.WF.0.RBTree.RBNode.del.match_1.eq_2 : ∀ (motive : RBTree.RBColor → Sort u_1) (h_1 : Unit → motive RBTree.RBColor.black)
  (h_2 : Unit → motive RBTree.RBColor.red),
  (match RBTree.RBColor.red with
    | RBTree.RBColor.black => h_1 ()
    | RBTree.RBColor.red => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofRealCLM_apply : ∀ {K : Type u_1} [inst : RCLike K], ⇑RCLike.ofRealCLM = RCLike.ofReal
-- Batteries.Data.List.Lemmas
/-- **Alias** of `List.IsChain.imp`. -/
List.Chain.imp : ∀ {α : Type u_1} {R S : α → α → Prop} {l : List α}, (∀ ⦃a b : α⦄, R a b → S a b) → List.IsChain R l → List.IsChain S l
-- Mathlib.Algebra.Group.AddChar
AddChar.neg_apply' : ∀ {A : Type u_1} {M : Type u_2} [inst : AddCommGroup A] [inst_1 : DivisionCommMonoid M] (ψ : AddChar A M) (a : A),
  (-ψ) a = (ψ a)⁻¹
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- Negating the first vector passed to `oangle` negates the sign of the angle.  -/
Orientation.oangle_sign_neg_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) (x y : V), (o.oangle (-x) y).sign = -(o.oangle x y).sign
-- Init.Data.Array.Count
Array.count_le_count_map : ∀ {α : Type u_2} [inst : BEq α] [LawfulBEq α] {β : Type u_1} [inst_2 : BEq β] [LawfulBEq β] {xs : Array α} {f : α → β}
  {x : α}, Array.count x xs ≤ Array.count (f x) (Array.map f xs)
-- Mathlib.Data.Rat.NatSqrt.Defs
Nat.ratSqrt_nonneg : ∀ (x prec : ℕ), 0 ≤ x.ratSqrt prec
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsThetaTVS.trans_isLittleOTVS : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} {G : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] [inst_7 : AddCommGroup G] [inst_8 : TopologicalSpace G]
  [inst_9 : Module 𝕜 G] {l : Filter α} {f : α → E} {g : α → F} {k : α → G}, f =Θ[𝕜; l] g → g =o[𝕜; l] k → f =o[𝕜; l] k
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.toMatrix_comp : ∀ {R₁ : Type u_1} {M₁ : Type u_2} [inst : CommSemiring R₁] [inst_1 : AddCommMonoid M₁] [inst_2 : Module R₁ M₁]
  {n : Type u_5} {o : Type u_6} [inst_3 : Fintype n] [inst_4 : Fintype o] [inst_5 : DecidableEq n]
  (b : Module.Basis n R₁ M₁) {M₂' : Type u_7} [inst_6 : AddCommMonoid M₂'] [inst_7 : Module R₁ M₂']
  (c : Module.Basis o R₁ M₂') [inst_8 : DecidableEq o] (B : LinearMap.BilinForm R₁ M₁) (l r : M₂' →ₗ[R₁] M₁),
  (LinearMap.BilinForm.toMatrix c) (B.comp l r) =
    ((LinearMap.toMatrix c b) l).transpose * (LinearMap.BilinForm.toMatrix b) B * (LinearMap.toMatrix c b) r
-- Mathlib.Data.PEquiv
PEquiv.ext_iff : ∀ {α : Type u} {β : Type v} {f g : α ≃. β}, f = g ↔ ∀ (x : α), f x = g x
-- Aesop.Nanos
Aesop.Nanos.mk.inj : ∀ {nanos nanos_1 : ℕ}, { nanos := nanos } = { nanos := nanos_1 } → nanos = nanos_1
-- Mathlib.CategoryTheory.CommSq
CategoryTheory.CommSq.LiftStruct.mk.sizeOf_spec : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y}
  {g : B ⟶ Y} {sq : CategoryTheory.CommSq f i p g} [inst_1 : SizeOf C] (l : B ⟶ X)
  (fac_left :
    autoParam (CategoryTheory.CategoryStruct.comp i l = f) CategoryTheory.CommSq.LiftStruct.fac_left._autoParam)
  (fac_right :
    autoParam (CategoryTheory.CategoryStruct.comp l p = g) CategoryTheory.CommSq.LiftStruct.fac_right._autoParam),
  sizeOf { l := l, fac_left := fac_left, fac_right := fac_right } = 1 + sizeOf l + sizeOf fac_left + sizeOf fac_right
-- Lean.Server.Rpc.Basic
Lean.Server.instInhabitedWithRpcRef : {a : Type u_1} → [Inhabited a] → Inhabited (Lean.Server.WithRpcRef a)
-- Mathlib.Combinatorics.Additive.Convolution
Finset.convolution_pos : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A B : Finset G} {x : G}, 0 < A.convolution B x ↔ x ∈ A * B
-- Mathlib.CategoryTheory.Localization.Bousfield
CategoryTheory.ObjectProperty.le_isLocal_isLocal : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C),
  P ≤ P.isLocal.isLocal
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.mk_unit : Cardinal.mk Unit = 1
-- Init.Data.Nat.Basic
_private.Init.Data.Nat.Basic.0.Nat.beq.match_1.eq_4 : ∀ (motive : ℕ → ℕ → Sort u_1) (n m : ℕ) (h_1 : Unit → motive Nat.zero Nat.zero) (h_2 : (n : ℕ) → motive Nat.zero n.succ)
  (h_3 : (n : ℕ) → motive n.succ Nat.zero) (h_4 : (n m : ℕ) → motive n.succ m.succ),
  (match n.succ, m.succ with
    | Nat.zero, Nat.zero => h_1 ()
    | Nat.zero, n.succ => h_2 n
    | n.succ, Nat.zero => h_3 n
    | n.succ, m.succ => h_4 n m) =
    h_4 n m
-- Mathlib.Algebra.Group.Hom.Defs
ne_one_of_map : ∀ {R : Type u_10} {S : Type u_11} {F : Type u_12} [inst : One R] [inst_1 : One S] [inst_2 : FunLike F R S]
  [OneHomClass F R S] {f : F} {x : R}, f x ≠ 1 → x ≠ 1
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
/-- The smallest two-sided ideal containing a set.
 -/
TwoSidedIdeal.span : {R : Type u_1} → [inst : NonUnitalNonAssocRing R] → Set R → TwoSidedIdeal R
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.expSeries_div_summable : ∀ {𝔸 : Type u_1} [inst : NormedDivisionRing 𝔸] [NormedAlgebra ℚ 𝔸] [CompleteSpace 𝔸] (x : 𝔸),
  Summable fun n => x ^ n / ↑n.factorial
-- Mathlib.Topology.OpenPartialHomeomorph.Composition
/-- Composition of open partial homeomorphisms respects equivalence.  -/
OpenPartialHomeomorph.EqOnSource.trans' : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {e e' : OpenPartialHomeomorph X Y} {f f' : OpenPartialHomeomorph Y Z},
  e ≈ e' → f ≈ f' → e.trans f ≈ e'.trans f'
-- Mathlib.Combinatorics.SimpleGraph.Matching
SimpleGraph.Subgraph.IsPerfectMatching.even_card : ∀ {V : Type u_1} {G : SimpleGraph V} {M : G.Subgraph} [inst : Fintype V], M.IsPerfectMatching → Even (Fintype.card V)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The special case of the first simplicial identity  -/
CategoryTheory.SimplicialObject.δ_comp_δ_self : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)},
  CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) (X.δ i) = CategoryTheory.CategoryStruct.comp (X.δ i.succ) (X.δ i)
-- Mathlib.MeasureTheory.Function.AEEqFun.DomAct
DomMulAct.instSMulAEEqFun.eq_1 : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : SMul M α] [inst_3 : MeasurableConstSMul M α]
  [inst_4 : MeasureTheory.SMulInvariantMeasure M α μ],
  DomMulAct.instSMulAEEqFun = { smul := fun c f => f.compMeasurePreserving (fun x => DomMulAct.mk.symm c • x) ⋯ }
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.IsPrincipal.iSup`. -/
Ordinal.Principal.iSup : ∀ {op : Ordinal.{u_2} → Ordinal.{u_2} → Ordinal.{u_2}} {ι : Sort u_1} {f : ι → Ordinal.{u_2}},
  (∀ (i : ι), Ordinal.IsPrincipal op (f i)) → Ordinal.IsPrincipal op (⨆ i, f i)
-- Mathlib.Algebra.Notation.Support
Function.support_eq_iff : ∀ {ι : Type u_1} {M : Type u_3} [inst : Zero M] {f : ι → M} {s : Set ι},
  Function.support f = s ↔ (∀ x ∈ s, f x ≠ 0) ∧ ∀ x ∉ s, f x = 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_inv : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : DecidableEq α] [inst_1 : DecidableEq β] [inst_2 : Group α]
  [inst_3 : DivisionMonoid β] [inst_4 : FunLike F α β] [MonoidHomClass F α β] (f : F) (s : Finset α),
  Finset.image (⇑f) s⁻¹ = (Finset.image (⇑f) s)⁻¹
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- The functor `C ⥤ Type w ⥤ C` which sends `X : C` and `α : Type w` to
the coproduct of copies of `X` indexed by `α`.  -/
CategoryTheory.Limits.sigmaFunctor : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Limits.HasCoproducts C] → CategoryTheory.Functor C (CategoryTheory.Functor (Type w) C)
-- Init.Data.Nat.Power2.Basic
Nat.isPowerOfTwo_nextPowerOfTwo : ∀ (n : ℕ), n.nextPowerOfTwo.isPowerOfTwo
-- Mathlib.Analysis.Normed.Algebra.Unitization
Unitization.continuous_snd : ∀ {𝕜 : Type u_3} {A : Type u_4} [inst : NontriviallyNormedField 𝕜] [inst_1 : NonUnitalNormedRing A],
  Continuous fun x => x.toProd.2
-- Init.Data.Array.Basic
Array.ext' : ∀ {α : Type u} {xs ys : Array α}, xs.toList = ys.toList → xs = ys
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.iUnion_def : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} (π : BoxIntegral.Prepartition I), π.iUnion = ⋃ J ∈ π, ↑J
-- Mathlib.Combinatorics.Schnirelmann
schnirelmannDensity_univ : schnirelmannDensity Set.univ = 1
-- Lean.Elab.Match
Lean.Elab.Term.expandMacrosInPatterns : {k : Lean.SyntaxNodeKinds} → Array (Lean.Elab.Term.MatchAltView k) → Lean.MacroM (Array (Lean.Elab.Term.MatchAltView k))
-- Init.Data.UInt.Lemmas
UInt8.toNat_ofFin : ∀ (x : Fin UInt8.size), (UInt8.ofFin x).toNat = ↑x
-- Mathlib.Algebra.Colimit.Ring
Ring.DirectLimit.map_comp : ∀ {ι : Type u_1} [inst : Preorder ι] {G : ι → Type u_2} [inst_1 : (i : ι) → CommRing (G i)]
  {f : (i j : ι) → i ≤ j → G i →+* G j} {G' : ι → Type u_4} [inst_2 : (i : ι) → CommRing (G' i)]
  {f' : (i j : ι) → i ≤ j → G' i →+* G' j} {G'' : ι → Type u_5} [inst_3 : (i : ι) → CommRing (G'' i)]
  {f'' : (i j : ι) → i ≤ j → G'' i →+* G'' j} (g₁ : (i : ι) → G i →+* G' i) (g₂ : (i : ι) → G' i →+* G'' i)
  (hg₁ : ∀ (i j : ι) (h : i ≤ j), (g₁ j).comp (f i j h) = (f' i j h).comp (g₁ i))
  (hg₂ : ∀ (i j : ι) (h : i ≤ j), (g₂ j).comp (f' i j h) = (f'' i j h).comp (g₂ i)),
  (Ring.DirectLimit.map g₂ hg₂).comp (Ring.DirectLimit.map g₁ hg₁) =
    Ring.DirectLimit.map (fun i => (g₂ i).comp (g₁ i)) ⋯
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.GoodProducts.smaller_mono : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o₁ o₂ : Ordinal.{u}},
  o₁ ≤ o₂ → Profinite.NobelingProof.GoodProducts.smaller C o₁ ⊆ Profinite.NobelingProof.GoodProducts.smaller C o₂
-- Mathlib.Topology.Order.HullKernel
/-- When `α` is complete, a set is Lower topology relative-open if and only if it is of the form
`(hull T a)ᶜ` for some `a` in `α`.  -/
PrimitiveSpectrum.isOpen_iff : ∀ {α : Type u_1} [inst : CompleteLattice α] {T : Set α} [inst_1 : TopologicalSpace α] [Topology.IsLower α],
  (∀ p ∈ T, InfPrime p) → ∀ (S : Set ↑T), IsOpen S ↔ ∃ a, S = (PrimitiveSpectrum.hull T a)ᶜ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem!_inter : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited β], t₁.WF → t₂.WF → ∀ {k : α}, (t₁ ∩ t₂)[k]! = if k ∈ t₂ then t₁[k]! else default
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.TwoVariable
/-- The series defining the theta function is summable if and only if `0 < im τ`.  -/
summable_jacobiTheta₂_term_iff : ∀ (z τ : ℂ), (Summable fun x => jacobiTheta₂_term x z τ) ↔ 0 < τ.im
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.OneCochain.instMul : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {G : CategoryTheory.Functor Cᵒᵖ GrpCat} →
      {I : Type w'} → {U : I → C} → Mul (CategoryTheory.PresheafOfGroups.OneCochain G U)
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_eq_one : ∀ {α : Type u_1} [inst : One α] {a : αᵒᵈ}, OrderDual.ofDual a = 1 ↔ a = 1
-- Mathlib.Data.Set.Countable
/-- **Alias** of the reverse direction of `Set.Countable.biUnion_iff`. -/
Set.Countable.biUnion : ∀ {α : Type u} {β : Type v} {s : Set α} {t : (a : α) → a ∈ s → Set β},
  s.Countable → (∀ (a : α) (ha : a ∈ s), (t a ha).Countable) → (⋃ a, ⋃ (h : a ∈ s), t a h).Countable
-- Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
/-- We say a set `s` is an `EventuallyMeasurableSet` with respect to a given
σ-algebra `m` and σ-filter `l` if it differs from a set in `m` by a set in
the dual ideal of `l`.  -/
EventuallyMeasurableSet : {α : Type u_1} → MeasurableSpace α → (l : Filter α) → [CountableInterFilter l] → Set α → Prop
-- Mathlib.GroupTheory.Nilpotent
/-- **Alias** of `Group.nilpotent_quotient_of_nilpotent`.

---

A quotient of a nilpotent group is nilpotent.  -/
nilpotent_quotient_of_nilpotent : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [inst_1 : H.Normal] [_h : Group.IsNilpotent G],
  Group.IsNilpotent (G ⧸ H)
-- Mathlib.SetTheory.ZFC.Rank
ZFSet.rank_empty : ∅.rank = 0
-- Mathlib.Order.Monotone.Defs
monotone_prod_iff : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {h : α × β → γ}, Monotone h ↔ (∀ (a : α), Monotone fun b => h (a, b)) ∧ ∀ (b : β), Monotone fun a => h (a, b)
-- Mathlib.RingTheory.HahnSeries.Cardinal
HahnSeries.mem_cardSuppLTAddSubgroup : ∀ {Γ : Type u_1} {R : Type u_2} (κ : Cardinal.{u_1}) [inst : PartialOrder Γ] [inst_1 : AddGroup R]
  [hκ : Fact (Cardinal.aleph0 ≤ κ)] {x : HahnSeries Γ R}, x ∈ HahnSeries.cardSuppLTAddSubgroup Γ R κ ↔ x.cardSupp < κ
-- Mathlib.Order.Basic
/-- The pointwise partial order on a product.
(The lexicographic ordering is defined in `Order.Lexicographic`, and the instances are
available via the type synonym `α ×ₗ β = α × β`.)  -/
Prod.instPartialOrder : (α : Type u_5) → (β : Type u_6) → [PartialOrder α] → [PartialOrder β] → PartialOrder (α × β)
-- Mathlib.Algebra.CharP.Basic
/-- Characteristic `≠ 2` and nontrivial implies that `-1 ≠ 1`.  -/
Ring.neg_one_ne_one_of_char_ne_two : ∀ {R : Type u_2} [inst : NonAssocRing R] [Nontrivial R], ringChar R ≠ 2 → -1 ≠ 1
-- Mathlib.Topology.ContinuousMap.ContinuousMapZero
ContinuousMapZero.continuous_precomp : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : Zero X] [inst_1 : Zero Y] [inst_2 : Zero R]
  [inst_3 : TopologicalSpace X] [inst_4 : TopologicalSpace Y] [inst_5 : TopologicalSpace R] (f : ContinuousMapZero X Y),
  Continuous fun g => g.comp f
-- Mathlib.Data.Int.Log
Int.clog_natCast : ∀ {R : Type u_1} [inst : Semifield R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorSemiring R]
  (b n : ℕ), Int.clog b ↑n = ↑(Nat.clog b n)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMap.toNNReal_one : ∀ {X : Type u_1} [inst : TopologicalSpace X], ContinuousMap.toNNReal 1 = 1
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.Inner.Basic
SSet.innerAnodyneExtensions_eq_retracts_transfiniteCompositions : SSet.innerAnodyneExtensions =
  (CategoryTheory.MorphismProperty.transfiniteCompositions.{u, u, u + 1}
      (CategoryTheory.MorphismProperty.coproducts.{u, u, u + 1} SSet.innerHornInclusions).pushouts).retracts
-- Mathlib.Data.Nat.DvdSequence
/-- **Alias** of `IsDvdSequence.id`. -/
isDivSequence_id : ∀ (α : Type u_1) [inst : Dvd α], IsDvdSequence id
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval'.X_smul_of : ∀ {R : Type u_2} {M : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (φ : M →ₗ[R] M)
  (m : M), Polynomial.X • (Module.AEval'.of φ) m = (Module.AEval'.of φ) (φ m)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instInhabitedMessageMetaData : Inhabited Lean.JsonRpc.MessageMetaData
-- Init.Data.Ord.Basic
List.compareLex.eq_4 : ∀ {α : Type u_1} (cmp : α → α → Ordering) (x_2 : α) (xs : List α) (y : α) (ys : List α),
  List.compareLex cmp (x_2 :: xs) (y :: ys) =
    match cmp x_2 y with
    | Ordering.lt => Ordering.lt
    | Ordering.eq => List.compareLex cmp xs ys
    | Ordering.gt => Ordering.gt
-- Mathlib.Algebra.Order.Floor.Ring
Int.cast_mul_floor_div_cancel_of_pos : ∀ {R : Type u_4} [inst : Ring R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R] [inst_3 : FloorRing R] {n : ℤ},
  0 < n → ∀ (a : R), ⌊↑n * a⌋ / n = ⌊a⌋
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.finStronglyMeasurable_zero : ∀ {α : Type u_5} {β : Type u_6} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : Zero β]
  [inst_1 : TopologicalSpace β], MeasureTheory.FinStronglyMeasurable 0 μ