mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackObjObj
CategoryTheory.Functor.PushoutObjObj.ι_iso_of_iso_left_inv : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₃)} {f₁ f₁' : CategoryTheory.Arrow C₁}
  {f₂ : CategoryTheory.Arrow C₂} (sq₁₂ : F.PushoutObjObj f₁.hom f₂.hom) (sq₁₂' : F.PushoutObjObj f₁'.hom f₂.hom)
  (iso : f₁ ≅ f₁'), (sq₁₂.ι_iso_of_iso_left sq₁₂' iso).inv = sq₁₂'.mapArrowLeft sq₁₂ iso.inv
-- Mathlib.CategoryTheory.ComposableArrows.Four
CategoryTheory.ComposableArrows.fourδ₄Toδ₃_app_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {i₀ i₁ i₂ i₃ i₄ : C} (f₁ : i₀ ⟶ i₁) (f₂ : i₁ ⟶ i₂)
  (f₃ : i₂ ⟶ i₃) (f₄ : i₃ ⟶ i₄) (f₃₄ : i₂ ⟶ i₄) (h₃₄ : CategoryTheory.CategoryStruct.comp f₃ f₄ = f₃₄),
  (CategoryTheory.ComposableArrows.fourδ₄Toδ₃ f₁ f₂ f₃ f₄ f₃₄ h₃₄).app 0 =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.ComposableArrows.mk₃ f₁ f₂ f₃).obj 0)
-- Init.Grind.Attr
/-- Like `@[grind]`, but also prints the pattern(s) selected by `grind`
as info messages. Useful for debugging annotations and modifiers.
 -/
Lean.Parser.Attr.grind? : Lean.ParserDescr
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.sum_fiberwise : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {α : Type u_2} {M : Type u_3} [inst : AddCommMonoid M]
  (π : BoxIntegral.Prepartition I) (f : BoxIntegral.Box ι → α) (g : BoxIntegral.Box ι → M),
  ∑ y ∈ Finset.image f π.boxes, ∑ J ∈ (π.filter fun J => f J = y).boxes, g J = ∑ J ∈ π.boxes, g J
-- Mathlib.Topology.MetricSpace.Antilipschitz
/-- We say that `f : α → β` is `AntilipschitzWith K` if for any two points `x`, `y` we have
`edist x y ≤ K * edist (f x) (f y)`. This can also be used as a predicate for bounded below
linear operators, see `antilipschitzWith_iff_exists_mul_le_norm`.  -/
AntilipschitzWith : {α : Type u_1} → {β : Type u_2} → [PseudoEMetricSpace α] → [PseudoEMetricSpace β] → NNReal → (α → β) → Prop
-- Mathlib.Order.SetNotation
Set.instSupSet : {α : Type u} → SupSet (Set α)
-- Init.Data.Option.Lemmas
Option.filter_none : ∀ {α : Type u_1} (p : α → Bool), Option.filter p none = none
-- Mathlib.Topology.Maps.Basic
IsOpenMap.image_interior_subset : ∀ {X : Type u_1} {Y : Type u_2} {f : X → Y} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y],
  IsOpenMap f → ∀ (s : Set X), f '' interior s ⊆ interior (f '' s)
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
/-- If `(n-1)!` is invertible in `A` and `I^n = 0`, then `I` admits a divided power structure.
Proposition 1.2.7 of [B74], part (ii).  -/
DividedPowers.OfInvertibleFactorial.dividedPowers : {A : Type u_1} →
  [inst : CommSemiring A] →
    {I : Ideal A} → [DecidablePred fun x => x ∈ I] → {n : ℕ} → IsUnit ↑(n - 1).factorial → I ^ n = 0 → DividedPowers I
-- Mathlib.CategoryTheory.Comma.Basic
/-- Two equal natural transformations `R₁ ⟶ R₂` yield naturally isomorphic functors
`Comma L R₁ ⥤ Comma L R₂`.  -/
CategoryTheory.Comma.mapRightEq : {B : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} B] →
    {A : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
        {T : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} T] →
            (L : CategoryTheory.Functor A T) →
              {R₁ R₂ : CategoryTheory.Functor B T} →
                (r r' : R₂ ⟶ R₁) → r = r' → (CategoryTheory.Comma.mapRight L r ≅ CategoryTheory.Comma.mapRight L r')
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.MorphismProperty.fst'_self_eq_snd : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.MorphismProperty C}
  {G : CategoryTheory.Functor Cᵒᵖ (Type v₁)},
  P ≤ CategoryTheory.MorphismProperty.monomorphisms C →
    ∀ {X : C} {f : CategoryTheory.yoneda.obj X ⟶ G} (hf : P.presheaf f), ⋯.fst' f = ⋯.snd f
-- Mathlib.Data.ZMod.Basic
ZMod.cast_eq_val : ∀ {n : ℕ} {R : Type u_1} [inst : AddGroupWithOne R] [NeZero n] (a : ZMod n), a.cast = ↑a.val
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.order_eq_orderTop_of_ne_zero : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] {x : HahnSeries Γ R} [inst_2 : Zero Γ],
  x ≠ 0 → ↑x.order = x.orderTop
-- Mathlib.RingTheory.WittVector.MulCoeff
_private.Mathlib.RingTheory.WittVector.MulCoeff.0.WittVector.term𝕄 : Lean.ParserDescr
-- Mathlib.Algebra.Order.Ring.Idempotent
instBooleanAlgebraSubtypeIsIdempotentElem : {R : Type u_1} → [inst : CommRing R] → BooleanAlgebra { a // IsIdempotentElem a }
-- Mathlib.Algebra.Lie.Basic
/-- A Lie ring bracket vanishes on the diagonal in L × L.  -/
LieRing.lie_self : ∀ {L : Type v} [self : LieRing L] (x : L), ⁅x, x⁆ = 0
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_X_add_C : ∀ {R : Type u} [Nontrivial R] [inst : Semiring R] (x : R), (Polynomial.X + Polynomial.C x).natDegree = 1
-- Mathlib.Analysis.InnerProductSpace.Reproducing
_private.Mathlib.Analysis.InnerProductSpace.Reproducing.0.RKHS.OfKernel.kerFunAux : {𝕜 : Type u_1} →
  [inst : RCLike 𝕜] →
    {X : Type u_2} →
      {V : Type u_3} →
        [inst_1 : NormedAddCommGroup V] →
          [inst_2 : InnerProductSpace 𝕜 V] →
            [inst_3 : CompleteSpace V] →
              {K : Matrix X X (V →L[𝕜] V)} →
                [inst_4 : Fact K.PosSemidef] → X → V →ₗ[𝕜] UniformSpace.Completion (RKHS.H₀ K)
-- Mathlib.RingTheory.Polynomial.IsIntegral
/-- [Stacks Tag 030A](https://stacks.math.columbia.edu/tag/030A) -/
instIsIntegrallyClosedPolynomialOfIsDomain : ∀ {R : Type u_4} [inst : CommRing R] [IsDomain R] [IsIntegrallyClosed R], IsIntegrallyClosed (Polynomial R)
-- Mathlib.Analysis.Normed.Affine.AddTorsor
DilationEquiv.smulTorsor.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : NormSMulClass 𝕜 E] {P : Type u_3} [inst_4 : PseudoMetricSpace P] [inst_5 : NormedAddTorsor E P] (c c_1 : P),
  c = c_1 → ∀ {k k_1 : 𝕜} (e_k : k = k_1) (hk : k ≠ 0), DilationEquiv.smulTorsor c hk = DilationEquiv.smulTorsor c_1 ⋯
-- Lean.Compiler.InlineAttrs
Lean.Compiler.InlineAttributeKind.alwaysInline : Lean.Compiler.InlineAttributeKind
-- Init.Data.Order.PackageFactories
/-- Use this factory to conveniently define a linear preorder on a type `α` and all the associated
operations and instances given an `LE α` instance.

Creates a `LinearPreorderPackage α` instance. Such an instance entails `LE α`, `LT α`, `BEq α` and
`Ord α` instances as well as an `IsLinearPreorder α` instance and `LawfulOrder*` instances proving
the compatibility of the operations with the linear preorder.

In the presence of `LE α`, `DecidableLE α`, `Total (· ≤ ·)` and `Trans (· ≤ ·) (· ≤ ·) (· ≤ ·)`
instances, no arguments are required and the factory can be used as in this example:

```lean
public instance : LinearPreorderPackage X := .ofLE X
```

If not all of these instances are available via typeclass synthesis, it is necessary to explicitly
provide some arguments:

```lean
public instance : LinearPreorderPackage X := .ofLE X {
  le_total := sorry
  le_trans := sorry }
```

It is also possible to do all of this by hand, without resorting to `LinearPreorderPackage`. This
can be useful if, say, one wants to avoid specifying an `LT α` instance, which is not possible with
`LinearPreorderPackage`.

**How the arguments are filled**

Lean tries to fill all of the fields of the `args : Packages.LinearPreorderOfLEArgs α` parameter
automatically. If it fails, it is necessary to provide some of the fields manually.

* For the data-carrying typeclasses `LE`, `LT`, `BEq` and `Ord`, existing instances are always
  preferred. If no existing instances can be synthesized, it is attempted to derive an instance from
  the `LE` instance.
* Some proof obligations can be filled automatically if the data-carrying typeclasses have been
  derived from the `LE` instance. For example: If the `beq` field is omitted and no `BEq α` instance
  can be synthesized, it is derived from the `LE α` instance. In this case, `beq_iff_le_and_ge` can be
  omitted because Lean can infer that `BEq α` and `LE α` are compatible.
* Other proof obligations, namely `le_total` and `le_trans`, can be omitted if `Total` and `Trans`
  instances can be synthesized.
 -/
Std.LinearPreorderPackage.ofLE : (α : Type u) →
  autoParam (Std.Packages.LinearPreorderOfLEArgs α) Std.LinearPreorderPackage.ofLE._auto_1 → Std.LinearPreorderPackage α
-- Mathlib.Control.ULiftable
ReaderT.instULiftableULiftULift : {s : Type u₀} →
  {m : Type (max u₀ v₀) → Type u_5} →
    {m' : Type (max u₀ v₁) → Type u_6} →
      [ULiftable m m'] → ULiftable (ReaderT (ULift.{max v₀ u₀, u₀} s) m) (ReaderT (ULift.{max v₁ u₀, u₀} s) m')
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
tsum_eisSummand_eq_riemannZeta_mul_eisensteinSeries : ∀ {k : ℕ},
  3 ≤ k →
    ∀ (z : UpperHalfPlane),
      ∑' (v : Fin 2 → ℤ), EisensteinSeries.eisSummand (↑k) v z = riemannZeta ↑k * eisensteinSeries 0 (↑k) z
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.of_lift : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : IsAdicComplete I N]
  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m)
  (x : M), (AdicCompletion.of I N) ((IsAdicComplete.lift I f ⋯) x) = (AdicCompletion.lift I f ⋯) x
-- Lean.EnvExtension
Lean.SimplePersistentEnvExtensionDescr.addEntryFn : {α σ : Type} → Lean.SimplePersistentEnvExtensionDescr α σ → σ → α → σ
-- Init.Data.Nat.Lemmas
Nat.sub_one_lt_of_le : ∀ {a b : ℕ}, 0 < a → a ≤ b → a - 1 < b
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.injective_lift_iff : ∀ {G : Type u_1} {M : Type u_4} [inst : Group G] [inst_1 : Monoid M] (N : Subgroup G) [nN : N.Normal] (φ : G →* M)
  (HN : N ≤ φ.ker), Function.Injective ⇑(QuotientGroup.lift N φ HN) ↔ N = φ.ker
-- Mathlib.Topology.MetricSpace.HolderNorm
MemHolder.smul : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : NormedAddCommGroup Y] {r : NNReal} {f : X → Y}
  {𝕜 : Type u_3} [inst_2 : SeminormedRing 𝕜] [inst_3 : Module 𝕜 Y] [IsBoundedSMul 𝕜 Y] {c : 𝕜},
  MemHolder r f → MemHolder r (c • f)
-- Mathlib.Topology.UniformSpace.Basic
instUniformSpaceBool : UniformSpace Bool
-- Mathlib.CategoryTheory.Limits.Indization.IndObject
CategoryTheory.Limits.IndObjectPresentation.yoneda_F : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : C),
  (CategoryTheory.Limits.IndObjectPresentation.yoneda X).F = CategoryTheory.Functor.fromPUnit X
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.mul_dvd_mul_eq : ∀ {a b c : ℤ}, a ≠ 0 → (a * b ∣ a * c ↔ b ∣ c)
-- Std.Http.Data.Response
/-- Creates a new HTTP Response builder with the 403 status code.
 -/
Std.Http.Response.forbidden : Std.Http.Response.Builder
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- Formula for `completedSinZeta` as a Dirichlet series in the convergence range
(second version, with sum over `ℕ`).  -/
HurwitzZeta.hasSum_nat_completedSinZeta : ∀ (a : ℝ) {s : ℂ},
  1 < s.re →
    HasSum (fun n => (s + 1).Gammaℝ * ↑(Real.sin (2 * Real.pi * a * ↑n)) / ↑n ^ s) (HurwitzZeta.completedSinZeta (↑a) s)
-- Lean.Util.LeanOptions
Lean.instOfNatLeanOptionValue : {n : ℕ} → OfNat Lean.LeanOptionValue n
-- Mathlib.Algebra.Homology.HomotopyCofiber
HomologicalComplex.cylinder.ι₀.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  {c : ComplexShape ι} (K : HomologicalComplex C c) [inst_2 : DecidableRel c.Rel]
  [inst_3 : ∀ (i : ι), CategoryTheory.Limits.HasBinaryBiproduct (K.X i) (K.X i)] [inst_4 : K.HasCylinder],
  HomologicalComplex.cylinder.ι₀ K =
    CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (HomologicalComplex.homotopyCofiber.inr
        (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id K) (-CategoryTheory.CategoryStruct.id K)))
-- Init.Grind.Order
Lean.Grind.Order.eq_of_le_of_le : ∀ {α : Type u_1} [inst : LE α] [Std.IsPartialOrder α] {a b : α}, a ≤ b → b ≤ a → a = b
-- Mathlib.Algebra.Group.UniqueProds.Basic
_private.Mathlib.Algebra.Group.UniqueProds.Basic.0.instAddI.eq_1 : ∀ (G : Type u) (H : Type v) [inst : Add G] [inst_1 : Add H] (t : Bool), instAddI✝ G H t = Bool.rec ULift.add ULift.add t
-- Mathlib.RingTheory.Localization.Defs
Localization.mk_eq_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Submonoid R}, Localization.mk = IsLocalization.mk' (Localization M)
-- Init.Data.UInt.Lemmas
UInt16.mul_def : ∀ (a b : UInt16), a * b = { toBitVec := a.toBitVec * b.toBitVec }
-- Mathlib.Topology.ContinuousOn
Continuous.tendsto_nhdsSet_nhds : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : Set α} {b : β}
  {f : α → β}, Continuous f → Set.EqOn f (fun x => b) s → Filter.Tendsto f (nhdsSet s) (nhds b)
-- Mathlib.RingTheory.Congruence.Hom
RingCon.lift_bijective_iff : ∀ {M : Type u_1} {P : Type u_3} [inst : NonAssocSemiring M] [inst_1 : NonAssocSemiring P] {c : RingCon M} {f : M →+* P}
  {h : c ≤ RingCon.ker f}, Function.Bijective ⇑(c.lift f h) ↔ c = RingCon.ker f ∧ Function.Surjective ⇑f
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.SheafedSpace.GlueData.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : SizeOf C]
  (toGlueData : CategoryTheory.GlueData (AlgebraicGeometry.SheafedSpace C))
  (f_open : ∀ (i j : toGlueData.J), AlgebraicGeometry.SheafedSpace.IsOpenImmersion (toGlueData.f i j)),
  sizeOf { toGlueData := toGlueData, f_open := f_open } = 1 + sizeOf toGlueData
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.C_smul : ∀ {R : Type u_1} {S : Type u_2} {a b : R} [inst : Zero R] [inst_1 : SMulZeroClass S R] (s : S) (r : R),
  QuadraticAlgebra.C (s • r) = s • QuadraticAlgebra.C r
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.Uniformizer.mk.inj : ∀ {Γ : Type u_1} {inst : LinearOrderedCommGroupWithZero Γ} {A : Type u_2} {inst_1 : Ring A} {v : Valuation A Γ}
  {hv : v.IsRankOneDiscrete} {val : ↥v.integer} {valuation_gt_one : v.IsUniformizer ↑val} {val_1 : ↥v.integer}
  {valuation_gt_one_1 : v.IsUniformizer ↑val_1},
  { val := val, valuation_gt_one := valuation_gt_one } = { val := val_1, valuation_gt_one := valuation_gt_one_1 } →
    val = val_1
-- Mathlib.RingTheory.LocalProperties.Exactness
bijective_of_isLocalized_span : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (s : Set R),
  Ideal.span s = ⊤ →
    ∀ (Mₚ : ↑s → Type u_5) [inst_5 : (r : ↑s) → AddCommMonoid (Mₚ r)] [inst_6 : (r : ↑s) → Module R (Mₚ r)]
      (f : (r : ↑s) → M →ₗ[R] Mₚ r) [inst_7 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (f r)] (Nₚ : ↑s → Type u_6)
      [inst_8 : (r : ↑s) → AddCommMonoid (Nₚ r)] [inst_9 : (r : ↑s) → Module R (Nₚ r)] (g : (r : ↑s) → N →ₗ[R] Nₚ r)
      [inst_10 : ∀ (r : ↑s), IsLocalizedModule.Away (↑r) (g r)] (F : M →ₗ[R] N),
      (∀ (r : ↑s), Function.Bijective ⇑((IsLocalizedModule.map (Submonoid.powers ↑r) (f r) (g r)) F)) →
        Function.Bijective ⇑F
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.basicOpen_eq_of_affine : ∀ {R : CommRingCat} (f : ↑R),
  (AlgebraicGeometry.Spec R).basicOpen
      ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.Scheme.ΓSpecIso R).inv) f) =
    PrimeSpectrum.basicOpen f
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.decay' : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (self : SchwartzMap E F) (k n : ℕ),
  ∃ C, ∀ (x : E), ‖x‖ ^ k * ‖iteratedFDeriv ℝ n self.toFun x‖ ≤ C
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Rel.whisker_right_id : ∀ {B : Type u} [inst : Quiver B] {a b : B} {f g : CategoryTheory.FreeBicategory.Hom a b}
  (η : CategoryTheory.FreeBicategory.Hom₂ f g),
  CategoryTheory.FreeBicategory.Rel
    (CategoryTheory.FreeBicategory.Hom₂.whisker_right (CategoryTheory.FreeBicategory.Hom.id b) η)
    ((CategoryTheory.FreeBicategory.Hom₂.right_unitor f).vcomp
      (η.vcomp (CategoryTheory.FreeBicategory.Hom₂.right_unitor_inv g)))
-- ProofWidgets.Compat
ProofWidgets.ExprWithCtx.expr : ProofWidgets.ExprWithCtx → Lean.Expr
-- Init.Data.Vector.Lemmas
Vector.setIfInBounds.eq_1 : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n) (i : ℕ) (x : α),
  xs.setIfInBounds i x = Vector.mk (xs.toArray.setIfInBounds i x) ⋯
-- Lean.Declaration
Lean.instBEqOpaqueVal.beq : Lean.OpaqueVal → Lean.OpaqueVal → Bool
-- Mathlib.Algebra.Free
FreeAddSemigroup.lift.eq_1 : ∀ {α : Type u} {β : Type v} [inst : AddSemigroup β],
  FreeAddSemigroup.lift =
    { toFun := fun f => { toFun := fun x => List.foldl (fun a b => a + f b) (f x.head) x.tail, map_add' := ⋯ },
      invFun := fun f => ⇑f ∘ FreeAddSemigroup.of, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.NumberTheory.PellMatiyasevic
Pell.xy_modEq_of_modEq : ∀ {a b c : ℕ} (a1 : 1 < a) (b1 : 1 < b),
  a ≡ b [MOD c] → ∀ (n : ℕ), Pell.xn a1 n ≡ Pell.xn b1 n [MOD c] ∧ Pell.yn a1 n ≡ Pell.yn b1 n [MOD c]
-- Mathlib.NumberTheory.Pell
/-- If `d` is a positive integer that is not a square, then there exists a nontrivial solution
to the Pell equation `x^2 - d*y^2 = 1`.  -/
Pell.Solution₁.exists_nontrivial_of_not_isSquare : ∀ {d : ℤ}, 0 < d → ¬IsSquare d → ∃ a, a ≠ 1 ∧ a ≠ -1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get?_map : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] {f : (a : α) → β a → γ a} {k : α}, (Std.ExtDHashMap.map f m).get? k = Option.map (f k) (m.get? k)
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.RightExtension.IsPointwiseRightKanExtension.hom_ext : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H} {E : L.RightExtension F}
  (h : E.IsPointwiseRightKanExtension) {G : L.RightExtension F} {f₁ f₂ : G ⟶ E}, f₁ = f₂
-- Init.Data.List.Sublist
List.instTransSublistMem : {α : Type u_1} → Trans (fun l₁ l₂ => l₂.Sublist l₁) Membership.mem Membership.mem
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'}
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  (D : F.DescentData f) ⦃Y : C⦄ (q : Y ⟶ S') ⦃j₁ j₂ : ι'⦄ (f₁ : Y ⟶ X' j₁) (f₂ : Y ⟶ X' j₂) (q' : Y ⟶ S)
  (f₁' : Y ⟶ X (α j₁)) (f₂' : Y ⟶ X (α j₂))
  (hf₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (f' j₁) = q)
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_1)
  (hf₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (f' j₂) = q)
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_3)
  (hq' :
    autoParam (CategoryTheory.CategoryStruct.comp q p = q')
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_5)
  (hf₁' :
    autoParam (CategoryTheory.CategoryStruct.comp f₁ (p' j₁) = f₁')
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_7)
  (hf₂' :
    autoParam (CategoryTheory.CategoryStruct.comp f₂ (p' j₂) = f₂')
      CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom_eq._auto_9),
  CategoryTheory.Pseudofunctor.DescentData.pullFunctorObjHom w D q f₁ f₂ ⋯ ⋯ =
    CategoryTheory.CategoryStruct.comp
      ((F.mapComp' (p' j₁).op.toLoc f₁.op.toLoc f₁'.op.toLoc ⋯).inv.toNatTrans.app (D.obj (α j₁)))
      (CategoryTheory.CategoryStruct.comp (D.hom q' f₁' f₂' ⋯ ⋯)
        ((F.mapComp' (p' j₂).op.toLoc f₂.op.toLoc f₂'.op.toLoc ⋯).hom.toNatTrans.app (D.obj (α j₂))))
-- Mathlib.Combinatorics.Graph.Basic
Graph.instReflCompatible : ∀ {α : Type u_1} {β : Type u_2}, Std.Refl Graph.Compatible
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_snd_prod : ∀ {α : Type u_1} {E' : Type u_6} {F' : Type u_7} [inst : SeminormedAddCommGroup E'] [inst_1 : SeminormedAddCommGroup F']
  {f' : α → E'} {g' : α → F'} {l : Filter α}, g' =O[l] fun x => (f' x, g' x)
-- Init.Data.String.Basic
ByteArray.utf8Decode?.go.fun_cases_unfolding : ∀ (b : ByteArray) (i : ℕ) (acc : Array Char) (hi : i ≤ b.size) (motive : Option (Array Char) → Prop),
  (i < b.size → b.utf8DecodeChar? i = none → motive none) →
    (i < b.size →
        ∀ (c : Char) (h : b.utf8DecodeChar? i = some c),
          motive (ByteArray.utf8Decode?.go b (i + c.utf8Size) (acc.push c) ⋯)) →
      (¬i < b.size → motive (some acc)) → motive (ByteArray.utf8Decode?.go b i acc hi)
-- Init.Data.String.Pattern.String
_private.Init.Data.String.Pattern.String.0.String.Slice.Pattern.ForwardSliceSearcher.finitenessRelation : {s : String.Slice} → Std.Iterators.FinitenessRelation (String.Slice.Pattern.ForwardSliceSearcher s) Id
-- Init.Data.Bool
true_eq_decide_iff : ∀ {p : Prop} [h : Decidable p], true = decide p ↔ p
-- Mathlib.Topology.MetricSpace.CoveringNumbers
Metric.encard_maximalSeparatedSet : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {A : Set X} {ε : NNReal},
  Metric.packingNumber ε A ≠ ⊤ → (Metric.maximalSeparatedSet ε A).encard = Metric.packingNumber ε A
-- Init.Data.SInt.Basic
instLTInt64 : LT Int64
-- Lean.Meta.Tactic.Induction
Lean.Meta.InductionSubgoal.mvarId : Lean.Meta.InductionSubgoal → Lean.MVarId
-- Mathlib.Algebra.Homology.QuasiIso
quasiIsoAt_iff_exactAt : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i], K.ExactAt i → (QuasiIsoAt f i ↔ L.ExactAt i)
-- Mathlib.Topology.UniformSpace.Dini
/-- **Dini's theorem**: if `F n` is a monotone increasing collection of continuous functions
converging pointwise to a continuous function `f`, then `F n` converges to `f` in the
compact-open topology.  -/
ContinuousMap.tendsto_of_monotone_of_pointwise : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : Preorder ι] [inst_1 : TopologicalSpace α]
  [inst_2 : NormedAddCommGroup G] [inst_3 : Lattice G] [HasSolidNorm G] [IsOrderedAddMonoid G] {F : ι → C(α, G)}
  {f : C(α, G)},
  Monotone F →
    (∀ (x : α), Filter.Tendsto (fun x_1 => (F x_1) x) Filter.atTop (nhds (f x))) →
      Filter.Tendsto F Filter.atTop (nhds f)
-- Mathlib.RingTheory.LocalRing.Pullback
AlgHom.isUnit_pullback_mk_iff : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : CommSemiring R] [inst_1 : Ring A]
  [inst_2 : Algebra R A] [inst_3 : Ring B] [inst_4 : Algebra R B] [inst_5 : Semiring C] [inst_6 : Algebra R C]
  (f : A →ₐ[R] C) (g : B →ₐ[R] C) {a : A × B} (a_in : a ∈ f.pullback g), IsUnit ⟨a, a_in⟩ ↔ IsUnit a.1 ∧ IsUnit a.2
-- Mathlib.LinearAlgebra.FreeModule.Finite.CardQuotient
AddSubgroup.relIndex_eq_abs_det : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℚ E] (L₁ L₂ : AddSubgroup E),
  L₁ ≤ L₂ →
    ∀ {ι : Type u_2} [inst_2 : DecidableEq ι] [inst_3 : Fintype ι] (b₁ b₂ : Module.Basis ι ℚ E),
      L₁ = AddSubgroup.closure (Set.range ⇑b₁) →
        L₂ = AddSubgroup.closure (Set.range ⇑b₂) → ↑(L₁.relIndex L₂) = |b₂.det ⇑b₁|
-- Lean.Parser.Term
Lean.Parser.Term.letrec : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.mem_eigenspace_iff : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {x : M}, x ∈ f.eigenspace μ ↔ f x = μ • x