mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_map_sectL : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : PartialOrder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : DecidableLE (α × β)] (a b : α) (c : β),
  Finset.map (Function.Embedding.sectL α c) (Finset.Ioo a b) = Finset.Ioo (a, c) (b, c)
-- Mathlib.Algebra.Algebra.Subalgebra.MulOpposite
Subalgebra.unop_inf : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  (S₁ S₂ : Subalgebra R Aᵐᵒᵖ), (S₁ ⊓ S₂).unop = S₁.unop ⊓ S₂.unop
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderLimitsOfShape.condition : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {W : CategoryTheory.MorphismProperty C} {J : Type u_1}
  {inst_1 : CategoryTheory.Category.{v_1, u_1} J} [self : W.IsStableUnderLimitsOfShape J]
  (X₁ X₂ : CategoryTheory.Functor J C) (c₁ : CategoryTheory.Limits.Cone X₁) (c₂ : CategoryTheory.Limits.Cone X₂)
  (x : CategoryTheory.Limits.IsLimit c₁) (h₂ : CategoryTheory.Limits.IsLimit c₂) (f : X₁ ⟶ X₂),
  W.functorCategory J f →
    ∀ (φ : c₁.pt ⟶ c₂.pt),
      (∀ (j : J),
          CategoryTheory.CategoryStruct.comp φ (c₂.π.app j) =
            CategoryTheory.CategoryStruct.comp (c₁.π.app j) (f.app j)) →
        W φ
-- Mathlib.RingTheory.RingHom.PurelyInseparable
/-- Composition of purely inseparable ring homomorphisms between fields is purely inseparable.  -/
RingHom.IsPurelyInseparable.comp : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K] {f : F →+* E}
  {g : E →+* K}, f.IsPurelyInseparable → g.IsPurelyInseparable → (g.comp f).IsPurelyInseparable
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.instInhabitedHomOplaxFunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] → {F G : CategoryTheory.OplaxFunctor B C} → {η : F ⟶ G} → Inhabited (η ⟶ η)
-- Init.Data.Int.Lemmas
Int.neg_add : ∀ {a b : ℤ}, -(a + b) = -a + -b
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.tensorHom.eq_2 : ∀ (a y₁_2 y₂_2 : SimplexCategory) (f₁_2 : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of y₁_2)
  (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.of y₂_2),
  AugmentedSimplexCategory.tensorHom f₁_2 x =
    CategoryTheory.CategoryStruct.comp f₁_2
      (CategoryTheory.CategoryStruct.comp (SimplexCategory.mkHom (Fin.castAddOrderEmb (y₂_2.len + 1)).toOrderHom)
        (CategoryTheory.eqToHom ⋯))
-- Mathlib.NumberTheory.Transcendental.Liouville.Measure
ae_not_liouville : ∀ᵐ (x : ℝ), ¬Liouville x
-- Mathlib.Algebra.Group.Hom.Defs
map_zpow' : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : DivInvMonoid G]
  [inst_2 : DivInvMonoid H] [MonoidHomClass F G H] (f : F),
  (∀ (x : G), f x⁻¹ = (f x)⁻¹) → ∀ (a : G) (n : ℤ), f (a ^ n) = f a ^ n
-- Mathlib.CategoryTheory.InducedCategory
CategoryTheory.InducedCategory.faithful : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v, u₂} D] (F : C → D),
  (CategoryTheory.inducedFunctor F).Faithful
-- Mathlib.Topology.Defs.Filter
/-- `x` specializes to `y` (notation: `x ⤳ y`) if either of the following equivalent properties
hold:

* `𝓝 x ≤ 𝓝 y`; this property is used as the definition;
* `pure x ≤ 𝓝 y`; in other words, any neighbourhood of `y` contains `x`;
* `y ∈ closure {x}`;
* `closure {y} ⊆ closure {x}`;
* for any closed set `s` we have `x ∈ s → y ∈ s`;
* for any open set `s` we have `y ∈ s → x ∈ s`;
* `y` is a cluster point of the filter `pure x = 𝓟 {x}`.

This relation defines a `Preorder` on `X`. If `X` is a T₀ space, then this preorder is a partial
order. If `X` is a T₁ space, then this partial order is trivial : `x ⤳ y ↔ x = y`.  -/
«term_⤳_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The `weightedOrder` of the product of two formal power series
is at least the sum of their orders.  -/
MvPowerSeries.le_weightedOrder_mul : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {f g : MvPowerSeries σ R},
  MvPowerSeries.weightedOrder w f + MvPowerSeries.weightedOrder w g ≤ MvPowerSeries.weightedOrder w (f * g)
-- Mathlib.Order.RelClasses
/-- **Alias** of `isTrans_gt`. -/
transitive_gt : ∀ {α : Type u} [inst : Preorder α], IsTrans α fun a a_1 => a_1 < a
-- Mathlib.Analysis.Calculus.DerivativeTest
/-- Suppose `f : ℝ → ℝ` is continuous at `a` and `b`, the derivative `f'` is nonnegative on
`Ioo a b` and nonpositive on `Ioo b c`. Then `f` attains its maximum on `Ico a c` at `b`.  -/
isMaxOn_Ico_of_deriv : ∀ {f : ℝ → ℝ} {a b c : ℝ},
  ContinuousAt f a →
    ContinuousAt f b →
      DifferentiableOn ℝ f (Set.Ioo a b) →
        DifferentiableOn ℝ f (Set.Ioo b c) →
          (∀ x ∈ Set.Ioo a b, 0 ≤ deriv f x) → (∀ x ∈ Set.Ioo b c, deriv f x ≤ 0) → IsMaxOn f (Set.Ico a c) b
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.odd_iff : ∀ {p : ℕ}, Nat.Prime p → (Odd p ↔ 3 ≤ p)
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.eq_comp_δ_of_not_surjective' : ∀ {n : ℕ} {Δ : SimplexCategory} (θ : Δ ⟶ { len := n + 1 }) (i : Fin (n + 2)),
  (∀ (x : Fin (Δ.len + 1)), (SimplexCategory.Hom.toOrderHom θ) x ≠ i) →
    ∃ θ', θ = CategoryTheory.CategoryStruct.comp θ' (SimplexCategory.δ i)
-- Mathlib.Algebra.Category.ModuleCat.Monoidal.Basic
/-- Extensionality lemma for morphisms from a module of the form `(M₁ ⊗ M₂) ⊗ M₃`.  -/
SemimoduleCat.MonoidalCategory.tensor_ext₃' : ∀ {R : Type u} [inst : CommSemiring R] {M₁ M₂ M₃ M₄ : SemimoduleCat R}
  {f g :
    CategoryTheory.MonoidalCategoryStruct.tensorObj (CategoryTheory.MonoidalCategoryStruct.tensorObj M₁ M₂) M₃ ⟶ M₄},
  (∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃),
      (CategoryTheory.ConcreteCategory.hom f) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃) =
        (CategoryTheory.ConcreteCategory.hom g) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃)) →
    f = g
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.isSome_get?_iff_mem : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α}, (m.get? a).isSome = true ↔ a ∈ m
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
_private.Mathlib.NumberTheory.EllipticDivisibilitySequence.0.preNormEDS'.match_1.splitter : (motive : ℕ → Sort u_1) →
  (x : ℕ) →
    (Unit → motive 0) →
      (Unit → motive 1) →
        (Unit → motive 2) →
          (Unit → motive 3) → (Unit → motive 4) → ((n : ℕ) → motive n.succ.succ.succ.succ.succ) → motive x
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.ofVal_intCast : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (z : ℤ), (↑z).ofVal = ↑z
-- Init.Internal.Order.Lemmas
Lean.Order.Option.monotone_mapM : ∀ {m : Type u → Type v} [inst : Monad m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)] [Lean.Order.MonoBind m]
  {α β : Type u} {γ : Type w} [inst_3 : Lean.Order.PartialOrder γ] [LawfulMonad m] (f : γ → α → m β) (xs : Option α),
  Lean.Order.monotone f → Lean.Order.monotone fun x => Option.mapM (f x) xs
-- Init.Core
/-- An indication of whether a loop's body terminated early that's used to compile the `for x in xs`
notation.

A collection's `ForIn` or `ForIn'` instance describes how to iterate over its elements. The monadic
action that represents the body of the loop returns a `ForInStep α`, where `α` is the local state
used to implement features such as `let mut`.
 -/
ForInStep : Type u → Type u
-- Mathlib.Algebra.Polynomial.AlgebraMap
Polynomial.mapAlgEquiv_toAlgHom : ∀ {R : Type u} {A : Type z} {B : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A ≃ₐ[R] B), ↑(Polynomial.mapAlgEquiv f) = Polynomial.mapAlgHom ↑f
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.coe_ofLE : ∀ {V : Type u_1} {G₁ G₂ : SimpleGraph V} (h : G₁ ≤ G₂), ⇑(SimpleGraph.Hom.ofLE h) = id
-- Mathlib.Data.List.Perm.Basic
List.Perm.foldl_eq : ∀ {α : Type u_1} {β : Type u_2} {f : β → α → β} {l₁ l₂ : List α} [rcomm : RightCommutative f],
  l₁.Perm l₂ → ∀ (b : β), List.foldl f b l₁ = List.foldl f b l₂
-- Mathlib.Topology.Order.LiminfLimsup
Pi.instBoundedGENhdsClass : ∀ {ι : Type u_1} {π : ι → Type u_6} [Finite ι] [inst : (i : ι) → Preorder (π i)]
  [inst_1 : (i : ι) → TopologicalSpace (π i)] [∀ (i : ι), BoundedGENhdsClass (π i)], BoundedGENhdsClass ((i : ι) → π i)
-- Mathlib.LinearAlgebra.Goursat
/-- **Goursat's lemma** for a submodule of a product with surjective projections.

If `L` is a submodule of `M × N` which projects fully on both factors, then there exist submodules
`M' ≤ M` and `N' ≤ N` such that `M' × N' ≤ L` and the image of `L` in `(M ⧸ M') × (N ⧸ N')` is the
graph of an isomorphism of `R`-modules `(M ⧸ M') ≃ (N ⧸ N')`.

`M` and `N` can be explicitly constructed as `L.goursatFst` and `L.goursatSnd` respectively.  -/
Submodule.goursat_surjective : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {L : Submodule R (M × N)},
  Function.Surjective (Prod.fst ∘ ⇑L.subtype) →
    Function.Surjective (Prod.snd ∘ ⇑L.subtype) →
      ∃ e, (L.goursatFst.mkQ.prodMap L.goursatSnd.mkQ ∘ₗ L.subtype).range = (↑e).graph
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
strongRankCondition_iff_forall_rank_lt_aleph0 : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R],
  StrongRankCondition R ↔ ∀ (n : ℕ), Module.rank R (Fin n → R) < Cardinal.aleph0
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorLeft_toPrelaxFunctor_toPrelaxFunctorStruct_toPrefunctor_obj_str_comp : ∀ (D : Type u₂) [inst : CategoryTheory.Category.{v₂, u₂} D] (C : CategoryTheory.Cat)
  {X Y Z : CategoryTheory.Join (↑C) D} (a : X.Hom Y) (a_1 : Y.Hom Z),
  CategoryTheory.CategoryStruct.comp a a_1 = CategoryTheory.Join.comp a a_1
-- Mathlib.Topology.Constructible
IsRetrocompact.isOpen_inter : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X},
  IsRetrocompact s → IsRetrocompact t → IsOpen s → IsRetrocompact (s ∩ t)
-- Mathlib.Algebra.Algebra.Basic
Algebra.mul_sub_algebraMap_commutes : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Ring A] [inst_2 : Algebra R A] (x : A) (r : R),
  x * (x - (algebraMap R A) r) = (x - (algebraMap R A) r) * x
-- Mathlib.Algebra.Category.CommAlgCat.Basic
CommAlgCat.id_apply : ∀ {R : Type u} [inst : CommRing R] (A : CommAlgCat R) (a : ↑A),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.id A)) a = a
-- Mathlib.LinearAlgebra.SModEq.Basic
SModEq.comm : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {U : Submodule R M}
  {x y : M}, x ≡ y [SMOD U] ↔ y ≡ x [SMOD U]
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.Cache.mk.congr_simp : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit}
  (map map_1 : Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w)
  (e_map : map = map_1)
  (hbound :
    ∀ {i : ℕ} (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ map) (h2 : i < k.w),
      (map.get k h1)[i].gate < aig.decls.size),
  { map := map, hbound := hbound } = { map := map_1, hbound := ⋯ }
-- Mathlib.RepresentationTheory.Basic
Representation.asModuleEquiv_map_smul : ∀ {k : Type u_1} {G : Type u_2} {V : Type u_3} [inst : CommSemiring k] [inst_1 : Monoid G] [inst_2 : AddCommMonoid V]
  [inst_3 : Module k V] (ρ : Representation k G V) (r : MonoidAlgebra k G) (x : ρ.asModule),
  ρ.asModuleEquiv (r • x) = (ρ.asAlgebraHom r) (ρ.asModuleEquiv x)
-- Mathlib.Computability.Ackermann
ack_le_iff_right : ∀ {m n₁ n₂ : ℕ}, ack m n₁ ≤ ack m n₂ ↔ n₁ ≤ n₂
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
HasFDerivWithinAt.uniqueDiffWithinAt_of_continuousLinearEquiv : ∀ {𝕜 : 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}
  {s : Set E} {x : E} (e' : E ≃L[𝕜] F),
  HasFDerivWithinAt f (↑e') s x → UniqueDiffWithinAt 𝕜 s x → UniqueDiffWithinAt 𝕜 (f '' s) (f x)
-- Mathlib.Algebra.Homology.ShortComplex.Exact
CategoryTheory.ShortComplex.Splitting.op_s : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S : CategoryTheory.ShortComplex C} (h : S.Splitting), h.op.s = h.r.op
-- Mathlib.Order.SetAccumulate
/-- `accumulate s` is the union of `s y` for `y ≤ x`.  -/
Set.accumulate : {α : Type u_1} → {β : Type u_2} → [LE α] → (α → Set β) → α → Set β
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.self_le_power : ∀ (a : Cardinal.{u_1}) {b : Cardinal.{u_1}}, 1 ≤ b → a ≤ a ^ b
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.D₂.multispanIndex_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_2 : CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_3 : CategoryTheory.Limits.HasPushouts C] (d : (CategoryTheory.OrthogonalReflection.D₂.multispanShape W Z).L),
  (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z).snd d = (↑d.snd).2
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
Profinite.NobelingProof.succ_exact : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  IsClosed C →
    ∀ (hsC : Profinite.NobelingProof.contained C (Order.succ o)) (ho : o < Ordinal.type fun x1 x2 => x1 < x2),
      {
          X₁ :=
            ModuleCat.of ℤ
              (LocallyConstant ↑(Profinite.NobelingProof.π C fun x => Profinite.NobelingProof.ord I x < o) ℤ),
          X₂ := ModuleCat.of ℤ (LocallyConstant ↑C ℤ),
          X₃ := ModuleCat.of ℤ (LocallyConstant ↑(Profinite.NobelingProof.C' C ho) ℤ),
          f := ModuleCat.ofHom (Profinite.NobelingProof.πs C o),
          g := ModuleCat.ofHom (Profinite.NobelingProof.Linear_CC' C hsC ho), zero := ⋯ }.Exact
-- Mathlib.Data.Set.Finite.Basic
/-- **Alias** of the reverse direction of `Set.Finite.toFinset_ssubset_toFinset`. -/
Set.Finite.toFinset_strictMono : ∀ {α : Type u} {s t : Set α} {hs : s.Finite} {ht : t.Finite}, s ⊂ t → hs.toFinset ⊂ ht.toFinset
-- Mathlib.Geometry.Euclidean.Projection
Affine.Simplex.dist_sq_eq_dist_orthogonalProjection_sq_add_dist_orthogonalProjection_sq : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] [inst_3 : MetricSpace P] [inst_4 : NormedAddTorsor V P] {n : ℕ}
  (s : Affine.Simplex 𝕜 P n) {p₁ : P} (p₂ : P),
  p₁ ∈ affineSpan 𝕜 (Set.range s.points) →
    dist p₁ p₂ * dist p₁ p₂ =
      dist p₁ ↑(s.orthogonalProjectionSpan p₂) * dist p₁ ↑(s.orthogonalProjectionSpan p₂) +
        dist p₂ ↑(s.orthogonalProjectionSpan p₂) * dist p₂ ↑(s.orthogonalProjectionSpan p₂)
-- Mathlib.Topology.VectorBundle.ContinuousAlternatingMap
Bundle.Pretrivialization.continuousAlternatingMap_symm_apply' : ∀ {𝕜 : Type u_1} {ι : Type u_2} [inst : NontriviallyNormedField 𝕜] {B : Type u_3} [inst_1 : TopologicalSpace B]
  {F₁ : Type u_4} [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜 F₁] {E₁ : B → Type u_5}
  [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜 (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] {F₂ : Type u_6} [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜 F₂] {E₂ : B → Type u_7} [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜 (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : (x : B) → TopologicalSpace (E₁ x)] [inst_13 : FiberBundle F₁ E₁]
  [inst_14 : (x : B) → TopologicalSpace (E₂ x)] [inst_15 : FiberBundle F₂ E₂]
  {e₁ : Bundle.Trivialization F₁ Bundle.TotalSpace.proj} {e₂ : Bundle.Trivialization F₂ Bundle.TotalSpace.proj}
  [inst_16 : Bundle.Trivialization.IsLinear 𝕜 e₁] [inst_17 : Bundle.Trivialization.IsLinear 𝕜 e₂] {b : B},
  b ∈ e₁.baseSet ∩ e₂.baseSet →
    ∀ (L : F₁ [⋀^ι]→L[𝕜] F₂),
      (Bundle.Pretrivialization.continuousAlternatingMap 𝕜 ι e₁ e₂).symm b L =
        (Bundle.Trivialization.symmL 𝕜 e₂ b).compContinuousAlternatingMap
          (L.compContinuousLinearMap (Bundle.Trivialization.continuousLinearMapAt 𝕜 e₁ b))
-- Mathlib.NumberTheory.Pell
/-- The `x`-coordinate of a fundamental solution is a lower bound for the `x`-coordinate
of any positive solution.  -/
Pell.IsFundamental.x_le_x : ∀ {d : ℤ} {a₁ : Pell.Solution₁ d}, Pell.IsFundamental a₁ → ∀ {a : Pell.Solution₁ d}, 1 < a.x → a₁.x ≤ a.x
-- Mathlib.Order.Filter.Cocardinal
Filter.frequently_cocardinal : ∀ {α : Type u} {c : Cardinal.{u}} {hreg : c.IsRegular} {p : α → Prop},
  (∃ᶠ (x : α) in Filter.cocardinal α hreg, p x) ↔ c ≤ Cardinal.mk ↑{x | p x}
-- Std.Time.Format
/-- The RFC850 format, which follows the pattern `eee, dd-MMM-YY HH:mm:ss ZZZ`.
This format is an older standard for representing date and time in headers.
 -/
Std.Time.Formats.rfc850 : Std.Time.GenericFormat Std.Time.Awareness.any
-- Mathlib.Order.UpperLower.Relative
isLowerSet_subtype_iff_isRelLowerSet : ∀ {α : Type u_1} {P : α → Prop} [inst : LE α] {s : Set { x // P x }}, IsLowerSet s ↔ IsRelLowerSet (Subtype.val '' s) P
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
/-- For an element `a` in a C⋆-algebra, TFAE:
1. `0 ≤ a`
2. `a = sqrt a * sqrt a`
3. `a = b * b` for some nonnegative `b`
4. `a = b * b` for some self-adjoint `b`
5. `a = star b * b` for some `b`
6. `a = b * star b` for some `b`
7. `a = a⁺`
8. `a` is self-adjoint and `a⁻ = 0`
9. `a` is self-adjoint and has nonnegative spectrum  -/
CStarAlgebra.nonneg_TFAE : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [inst_7 : StarOrderedRing A]
  [inst_8 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_9 : NonnegSpectrumClass ℝ A]
  [IsSemitopologicalRing A] [T2Space A] {a : A},
  [0 ≤ a, a = CFC.sqrt a * CFC.sqrt a, ∃ b, 0 ≤ b ∧ a = b * b, ∃ b, IsSelfAdjoint b ∧ a = b * b, ∃ b, a = star b * b,
      ∃ b, a = b * star b, a = a⁺, IsSelfAdjoint a ∧ a⁻ = 0,
      IsSelfAdjoint a ∧ QuasispectrumRestricts a ⇑ContinuousMap.realToNNReal].TFAE
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.mk : {ι : Type u_1} →
  (Rel : ι → ι → Prop) →
    (∀ {i j j' : ι}, Rel i j → Rel i j' → j = j') → (∀ {i i' j : ι}, Rel i j → Rel i' j → i = i') → ComplexShape ι
-- Mathlib.CategoryTheory.Abelian.Basic
CategoryTheory.Abelian.isIso_factorThruCoimage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {P Q : C} (f : P ⟶ Q)
  [CategoryTheory.Epi f], CategoryTheory.IsIso (CategoryTheory.Abelian.factorThruCoimage f)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryLaxFunctorCore.map₂_id : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryLaxFunctorCore B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.CategoryStruct.id f) = CategoryTheory.CategoryStruct.id (self.map f)
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
CochainComplex.plus_pathObject : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] (K : CochainComplex C ℤ),
  CochainComplex.plus C K → CochainComplex.plus C (HomologicalComplex.pathObject K)
-- Mathlib.Algebra.Order.Kleene
/-- An idempotent commutative semiring is a commutative semiring with the additional property that
addition is idempotent.  -/
IdemCommSemiring : Type u_5 → Type u_5
-- Mathlib.Topology.Algebra.Group.Defs
/-- Eta-expanded form of `ContinuousWithinAt.div'` -/
ContinuousWithinAt.fun_div' : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Div G]
  [ContinuousDiv G] {f g : X → G} {s : Set X} {x : X},
  ContinuousWithinAt f s x → ContinuousWithinAt g s x → ContinuousWithinAt (fun i => f i / g i) s x
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.HasIntegral.neg : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {y : F},
  BoxIntegral.HasIntegral I l f vol y → BoxIntegral.HasIntegral I l (-f) vol (-y)
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.st_neg : ∀ (x : ℝ*), (-x).st = -x.st
-- Mathlib.Topology.Connected.Basic
Quotient.instConnectedSpace : ∀ {α : Type u} [inst : TopologicalSpace α] {s : Setoid α} [ConnectedSpace α], ConnectedSpace (Quotient s)
-- Init.Prelude
/-- Make name `s₁.s₂.s₃`  -/
Lean.Name.mkStr3 : String → String → String → Lean.Name
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.instInhabitedAssignment.default : Std.Tactic.BVDecide.LRAT.Internal.Assignment
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.inter_vadd_union_subset_union : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : VAdd α β] {s₁ s₂ : Finset α} {t₁ t₂ : Finset β}
  [inst_2 : DecidableEq α], s₁ ∩ s₂ +ᵥ t₁ ∪ t₂ ⊆ (s₁ +ᵥ t₁) ∪ (s₂ +ᵥ t₂)
-- Lean.Data.KVMap
Lean.KVMap.empty : Lean.KVMap
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.CodeActionOptions.mk.sizeOf_spec : ∀ (toWorkDoneProgressOptions : Lean.Lsp.WorkDoneProgressOptions)
  (codeActionKinds? : Option (Array Lean.Lsp.CodeActionKind)) (resolveProvider? : Option Bool),
  sizeOf
      { toWorkDoneProgressOptions := toWorkDoneProgressOptions, codeActionKinds? := codeActionKinds?,
        resolveProvider? := resolveProvider? } =
    1 + sizeOf toWorkDoneProgressOptions + sizeOf codeActionKinds? + sizeOf resolveProvider?
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
_private.Mathlib.RingTheory.DividedPowers.SubDPIdeal.0.DividedPowers.Quotient.isSubDPIdeal_aux : ∀ {A : Type u_1} [inst : CommRing A] {I : Ideal A} (hI : DividedPowers I) {J : Ideal A},
  hI.IsSubDPIdeal (J ⊓ I) → hI.IsSubDPIdeal (RingHom.ker (Ideal.Quotient.mk J) ⊓ I)
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_eq_ofNat : ∀ (n : ℕ) {h : n < UInt16.size}, UInt16.ofNatLT n h = UInt16.ofNat n
-- Mathlib.CategoryTheory.Topos.Sheaf
CategoryTheory.Sheaf.classifier_Ω : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C),
  (CategoryTheory.Sheaf.classifier J).Ω = CategoryTheory.Sheaf.Ω J
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.mapMap_id : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  (X : CategoryTheory.GradedObject I C) (p : I → J) [inst_1 : X.HasMap p],
  CategoryTheory.GradedObject.mapMap (CategoryTheory.CategoryStruct.id X) p =
    CategoryTheory.CategoryStruct.id (X.mapObj p)
-- Lean.Data.Iterators.Producers.PersistentHashMap
_private.Lean.Data.Iterators.Producers.PersistentHashMap.0.Lean.PersistentHashMap.Zipper.prependNode.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : Lean.PersistentHashMap.Node α β → Sort u_3)
  (es : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β)))
  (h_1 :
    (es : Array (Lean.PersistentHashMap.Entry α β (Lean.PersistentHashMap.Node α β))) →
      motive (Lean.PersistentHashMap.Node.entries es))
  (h_2 :
    (keys : Array α) →
      (vals : Array β) → (hsz : keys.size = vals.size) → motive (Lean.PersistentHashMap.Node.collision keys vals hsz)),
  (match Lean.PersistentHashMap.Node.entries es with
    | Lean.PersistentHashMap.Node.entries es => h_1 es
    | Lean.PersistentHashMap.Node.collision keys vals hsz => h_2 keys vals hsz) =
    h_1 es