mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.ConeMorphism.inv_hom_id : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {c d : CategoryTheory.Limits.Cone F} (f : c ≅ d),
  CategoryTheory.CategoryStruct.comp f.inv.hom f.hom.hom = CategoryTheory.CategoryStruct.id d.pt
-- Init.Data.Vector.Lemmas
Vector.push_beq_push : ∀ {α : Type u_1} [inst : BEq α] {a b : α} {n : ℕ} {xs ys : Vector α n}, (xs.push a == ys.push b) = (xs == ys && a == b)
-- Mathlib.Data.Fin.SuccPred
Fin.castLE_rfl : ∀ (n : ℕ), Fin.castLE ⋯ = id
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Proper
/-- [Stacks Tag 01MC](https://stacks.math.columbia.edu/tag/01MC) -/
AlgebraicGeometry.Proj.instIsSeparated : ∀ {σ : Type u_1} {A : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜], (AlgebraicGeometry.Proj 𝒜).IsSeparated
-- Std.Sat.AIG.CachedGatesLemmas
Std.Sat.AIG.denote_mkNotCached : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {assign : α → Bool} {aig : Std.Sat.AIG α} {gate : aig.Ref},
  ⟦assign, aig.mkNotCached gate⟧ = !⟦assign, { aig := aig, ref := gate }⟧
-- Mathlib.SetTheory.ZFC.Class
/-- The collection of all classes.
We define `Class` as `Set ZFSet`, as this allows us to get many instances automatically. However, in
practice, we treat it as (the definitionally equal) `ZFSet → Prop`. This means, the preferred way to
state that `x : ZFSet` belongs to `A : Class` is to write `A x`.  -/
Class : Type (u_1 + 1)
-- Mathlib.RingTheory.WittVector.Frobenius
WittVector.ghostComponent_frobeniusFun : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (n : ℕ) (x : WittVector p R),
  (WittVector.ghostComponent n) x.frobeniusFun = (WittVector.ghostComponent (n + 1)) x
-- Lean.Parser.Extra
Lean.Parser.ppLine.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.coe_dual : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L},
  I ≠ 0 → ↑(FractionalIdeal.dual A K I) = Submodule.traceDual A K ↑I
-- Mathlib.Topology.Convenient.Category
GeneratedByTopCat.instIsIsoMapTopCatToGeneratedByTopCatAppAdjCounit : ∀ {ι : Type t} {X : ι → Type u} [inst : (i : ι) → TopologicalSpace (X i)] (Z : TopCat),
  CategoryTheory.IsIso (TopCat.toGeneratedByTopCat.map (GeneratedByTopCat.adjCounit.app Z))
-- Mathlib.Tactic.TFAE
Mathlib.Tactic.TFAE.Parser.tfaeType.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.findSomeRev?.eq_1 : ∀ {α : Type u} {β : Type v} (f : α → Option β) (as : Array α),
  Array.findSomeRev? f as = (Array.findSomeRevM? (fun x => pure (f x)) as).run
-- Mathlib.Geometry.Manifold.Algebra.Structures
instFieldContMDiffRing : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞}, ContMDiffRing (modelWithCornersSelf 𝕜 𝕜) n 𝕜
-- Init.Data.Option.Lemmas
Option.get_pfilter : ∀ {α : Type u_1} {o : Option α} {p : (a : α) → o = some a → Bool} (h : (o.pfilter p).isSome = true),
  (o.pfilter p).get h = o.get ⋯
-- Init.Data.UInt.Lemmas
UInt16.ofBitVec_le_iff_le : ∀ {a b : BitVec 16}, { toBitVec := a } ≤ { toBitVec := b } ↔ a ≤ b
-- Mathlib.Topology.Algebra.GroupCompletion
UniformSpace.Completion.coe_neg : ∀ {α : Type u_3} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] (a : α), ↑(-a) = -↑a
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.stieltjesOfMeasurableRat_nonneg : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α] (hf : Measurable f) (a : α) (r : ℝ),
  0 ≤ ↑(ProbabilityTheory.stieltjesOfMeasurableRat f hf a) r
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Priority.int.inj : ∀ {i i_1 : ℤ}, Aesop.Frontend.Priority.int i = Aesop.Frontend.Priority.int i_1 → i = i_1
-- Mathlib.MeasureTheory.Covering.Differentiation
VitaliFamily.ae_tendsto_lintegral_div : ∀ {α : Type u_1} [inst : PseudoMetricSpace α] {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (v : VitaliFamily μ) [SecondCountableTopology α] [BorelSpace α] [MeasureTheory.IsLocallyFiniteMeasure μ]
  {f : α → ENNReal},
  AEMeasurable f μ →
    ∫⁻ (y : α), f y ∂μ ≠ ⊤ →
      ∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun a => (∫⁻ (y : α) in a, f y ∂μ) / μ a) (v.filterAt x) (nhds (f x))
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.preEquivalence.functor_map_left : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.CostructuredArrow G e)
  {X Y : CategoryTheory.CostructuredArrow (CategoryTheory.CostructuredArrow.pre F G e) f} (φ : X ⟶ Y),
  ((CategoryTheory.CostructuredArrow.preEquivalence.functor F f).map φ).left = φ.left.left
-- Mathlib.Algebra.Ring.Invertible
AddUnits.val_mulRight : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R] (x : AddUnits R) (y : R), ↑(x.mulRight y) = ↑x * y
-- Mathlib.Analysis.Convex.EGauge
egauge_zero_left_eq_top : ∀ (𝕜 : Type u_1) [inst : NNNorm 𝕜] [Nonempty 𝕜] {E : Type u_2} [inst_2 : Zero E] [inst_3 : SMulZeroClass 𝕜 E] {x : E},
  egauge 𝕜 0 x = ⊤ ↔ x ≠ 0
-- Init.Data.UInt.Bitwise
UInt32.ofNatLT_or : ∀ (a b : ℕ) (ha : a < 2 ^ 32) (hb : b < 2 ^ 32),
  UInt32.ofNatLT (a ||| b) ⋯ = UInt32.ofNatLT a ha ||| UInt32.ofNatLT b hb
-- Lean.Elab.Tactic.Omega.Frontend
_private.Lean.Elab.Tactic.Omega.Frontend.0.Lean.Elab.Tactic.Omega.asLinearComboImpl.handleFinVal : Lean.Expr →
  Lean.Expr →
    Lean.Expr →
      Lean.Expr →
        Lean.Elab.Tactic.Omega.OmegaM
          (Lean.Omega.LinearCombo × Lean.Elab.Tactic.Omega.OmegaM Lean.Expr × List Lean.Expr)
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roc_eq_singleton_iff : ∀ {k m n : ℤ}, (m<...=n).toArray = #[k] ↔ n = m + 1 ∧ m + 1 = k
-- Init.Data.Cast
/-- The canonical map `Nat → R`.  -/
NatCast.natCast : {R : Type u} → [self : NatCast R] → ℕ → R
-- Init.Internal.Order.Basic
Lean.Order.chain_apply : ∀ {α : Sort u} {β : α → Sort v} [inst : (x : α) → Lean.Order.PartialOrder (β x)] {c : ((x : α) → β x) → Prop},
  Lean.Order.chain c → ∀ (x : α), Lean.Order.chain fun y => ∃ f, c f ∧ f x = y
-- Mathlib.Data.NNRat.Defs
NNRat.coe_eq_zero : ∀ {q : ℚ≥0}, ↑q = 0 ↔ q = 0
-- Mathlib.Algebra.Ring.Hom.Defs
RingHom.mk.inj : ∀ {α : Type u_5} {β : Type u_6} {inst : NonAssocSemiring α} {inst_1 : NonAssocSemiring β} {toMonoidHom : α →* β}
  {map_zero' : (↑toMonoidHom).toFun 0 = 0}
  {map_add' : ∀ (x y : α), (↑toMonoidHom).toFun (x + y) = (↑toMonoidHom).toFun x + (↑toMonoidHom).toFun y}
  {toMonoidHom_1 : α →* β} {map_zero'_1 : (↑toMonoidHom_1).toFun 0 = 0}
  {map_add'_1 : ∀ (x y : α), (↑toMonoidHom_1).toFun (x + y) = (↑toMonoidHom_1).toFun x + (↑toMonoidHom_1).toFun y},
  { toMonoidHom := toMonoidHom, map_zero' := map_zero', map_add' := map_add' } =
      { toMonoidHom := toMonoidHom_1, map_zero' := map_zero'_1, map_add' := map_add'_1 } →
    toMonoidHom = toMonoidHom_1
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- **Alias** of `isClosed_setOfPred_lipschitzOnWith`. -/
isClosed_setOf_lipschitzOnWith : ∀ {α : Type u_4} {β : Type u_5} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] (K : NNReal) (s : Set α),
  IsClosed {f | LipschitzOnWith K f s}
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.Bounds
HurwitzKernelBounds.F_nat.eq_1 : ∀ (k : ℕ) (a t : ℝ), HurwitzKernelBounds.F_nat k a t = ∑' (n : ℕ), HurwitzKernelBounds.f_nat k a t n
-- Mathlib.Topology.Category.UniformSpace
UniformSpaceCat.Hom.mk.injEq : ∀ {X : UniformSpaceCat} {Y : UniformSpaceCat} (hom' hom'_1 : { f // UniformContinuous f }),
  ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.RingTheory.Ideal.Maps
Submodule.annihilator_smul : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (N : Submodule R M), N.annihilator • N = ⊥
-- Lean.MetavarContext
Lean.MetavarContext.MkBinding.State.nextMacroScope : Lean.MetavarContext.MkBinding.State → Lean.MacroScope
-- Mathlib.Algebra.Group.Invertible.Basic
val_unitOfInvertible : ∀ {α : Type u} [inst : Monoid α] (a : α) [inst_1 : Invertible a], ↑(unitOfInvertible a) = a
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.integrable_condExpL2_of_isFiniteMeasure : ∀ {α : Type u_1} {E : Type u_2} {𝕜 : Type u_7} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : CompleteSpace E] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  (hm : m ≤ m0) [MeasureTheory.IsFiniteMeasure μ] {f : ↥(MeasureTheory.Lp E 2 μ)},
  MeasureTheory.Integrable (↑↑↑((MeasureTheory.condExpL2 E 𝕜 hm) f)) μ
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.neg : ∀ {R : Type uR} [inst : Ring R] {r : R → R → Prop} ⦃a b : R⦄, RingQuot.Rel r a b → RingQuot.Rel r (-a) (-b)
-- Mathlib.Analysis.Calculus.Taylor
/-- The Taylor polynomial with derivatives inside of a set `s`.

The Taylor polynomial is given by
$$∑_{k=0}^n \frac{(x - x₀)^k}{k!} f^{(k)}(x₀),$$
where $f^{(k)}(x₀)$ denotes the iterated derivative in the set `s`.  -/
taylorWithin : {E : Type u_2} →
  [inst : NormedAddCommGroup E] → [inst_1 : NormedSpace ℝ E] → (ℝ → E) → ℕ → Set ℝ → ℝ → PolynomialModule ℝ E
-- Mathlib.Order.RelIso.Basic
RelIso.preimage_symm_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α ≃ β) (s : β → β → Prop) (a : β), (RelIso.preimage f s).symm a = f.symm a
-- Mathlib.CategoryTheory.Limits.WeakLimits.WeakEqualizers
/-- If a weak equalizer of `f` and `g` exists, we can access the morphism
`weakEqualizer f g ⟶ X` by saying `weakEqualizer.ι f g`.  -/
CategoryTheory.Limits.weakEqualizer.ι : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {X Y : C} →
      (f g : X ⟶ Y) →
        [inst_1 : CategoryTheory.Limits.HasWeakEqualizer f g] → CategoryTheory.Limits.weakEqualizer f g ⟶ X
-- Lean.Meta.Tactic.Grind.Inv
_private.Lean.Meta.Tactic.Grind.Inv.0.Lean.Meta.Grind.checkEqc : Lean.Meta.Grind.ENode → Lean.Meta.Grind.GoalM Unit
-- Mathlib.LinearAlgebra.CliffordAlgebra.EvenEquiv
QuadraticMap.sq.congr_simp : ∀ {R : Type u_3} {A : Type u_7} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  [inst_3 : SMulCommClass R A A] [inst_4 : IsScalarTower R A A], QuadraticMap.sq = QuadraticMap.sq
-- Std.Http.Data.URI.Basic
/-- Path segments (will be encoded when building).
 -/
Std.Http.URI.Builder.pathSegments : Std.Http.URI.Builder → Array String
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.continuous_eval₂ : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommRing R] [inst_1 : UniformSpace R] {S : Type u_3} [inst_2 : CommRing S]
  [inst_3 : UniformSpace S] {φ : R →+* S} {a : σ → S} [IsTopologicalSemiring R] [IsUniformAddGroup R]
  [IsUniformAddGroup S] [CompleteSpace S] [T2Space S] [IsTopologicalRing S] [IsLinearTopology S S],
  Continuous ⇑φ → MvPowerSeries.HasEval a → Continuous (MvPowerSeries.eval₂ φ a)
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Subalgebra.map_comap_eq_self_of_surjective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : Semiring B] [inst_4 : Algebra R B] {f : A →ₐ[R] B},
  Function.Surjective ⇑f → ∀ (S : Subalgebra R B), Subalgebra.map f (Subalgebra.comap f S) = S
-- Mathlib.Order.WithBot
WithBot.ne_bot_iff_exists : ∀ {α : Type u_1} {x : WithBot α}, x ≠ ⊥ ↔ ∃ a, ↑a = x
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.HasEval.mono : ∀ {σ : Type u_1} {S : Type u_4} [inst : CommRing S] {a : σ → S} {t u : TopologicalSpace S},
  t ≤ u → MvPowerSeries.HasEval a → MvPowerSeries.HasEval a
-- Mathlib.Order.WithBot
WithTop.ofDual_top : ∀ {α : Type u_1}, WithTop.ofDual ⊤ = ⊥
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.Hom.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} (toHom : E.Hom F.toPreZeroHypercover)
  (s₁ : {i j : E.I₀} → E.I₁ i j → F.I₁ (toHom.s₀ i) (toHom.s₀ j))
  (h₁ h₁_1 : {i j : E.I₀} → (k : E.I₁ i j) → E.Y k ⟶ F.Y (s₁ k)) (e_h₁ : h₁ = h₁_1)
  (w₁₁ :
    ∀ {i j : E.I₀} (k : E.I₁ i j),
      CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₁ (s₁ k)) =
        CategoryTheory.CategoryStruct.comp (E.p₁ k) (toHom.h₀ i))
  (w₁₂ :
    ∀ {i j : E.I₀} (k : E.I₁ i j),
      CategoryTheory.CategoryStruct.comp (h₁ k) (F.p₂ (s₁ k)) =
        CategoryTheory.CategoryStruct.comp (E.p₂ k) (toHom.h₀ j)),
  { toHom := toHom, s₁ := s₁, h₁ := h₁, w₁₁ := w₁₁, w₁₂ := w₁₂ } =
    { toHom := toHom, s₁ := s₁, h₁ := h₁_1, w₁₁ := ⋯, w₁₂ := ⋯ }
-- Init.Data.Int.Basic
Int.instMul : Mul ℤ
-- Mathlib.Algebra.Group.InjSurj
/-- A type endowed with `*` is a semigroup, if it admits a surjective map that preserves `*` from a
semigroup. See note [reducible non-instances].  -/
Function.Surjective.semigroup : {M₁ : Type u_1} →
  {M₂ : Type u_2} →
    [inst : Mul M₂] →
      [inst_1 : Semigroup M₁] →
        (f : M₁ → M₂) → Function.Surjective f → (∀ (x y : M₁), f (x * y) = f x * f y) → Semigroup M₂
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.GrothendieckTopology.sheafify_isSheaf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [(CategoryTheory.forget D).ReflectsIsomorphisms] (P : CategoryTheory.Functor Cᵒᵖ D),
  CategoryTheory.Presheaf.IsSheaf J (J.sheafify P)
-- Mathlib.Analysis.SpecialFunctions.Exponential
hasDerivAt_exp_smul_const_of_mem_ball' : ∀ {𝕂 : Type u_1} {𝔸 : Type u_3} [inst : NontriviallyNormedField 𝕂] [CharZero 𝕂] [inst_2 : NormedRing 𝔸]
  [inst_3 : NormedAlgebra 𝕂 𝔸] [CompleteSpace 𝔸] (x : 𝔸) (t : 𝕂),
  t • x ∈ Metric.eball 0 (NormedSpace.expSeries 𝕂 𝔸).radius →
    HasDerivAt (fun u => NormedSpace.exp (u • x)) (x * NormedSpace.exp (t • x)) t
-- Mathlib.Order.Bounded
Set.unbounded_lt_inter_not_lt : ∀ {α : Type u_1} {s : Set α} [inst : SemilatticeSup α] (a : α),
  Set.Unbounded (fun x1 x2 => x1 < x2) (s ∩ {b | ¬b < a}) ↔ Set.Unbounded (fun x1 x2 => x1 < x2) s
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.AttributeEntry.mk.inj : ∀ {γ : Type} {toOLeanEntry : Lean.KeyedDeclsAttribute.OLeanEntry} {isBuiltin : Bool} {value : γ}
  {toOLeanEntry_1 : Lean.KeyedDeclsAttribute.OLeanEntry} {isBuiltin_1 : Bool} {value_1 : γ},
  { toOLeanEntry := toOLeanEntry, isBuiltin := isBuiltin, value := value } =
      { toOLeanEntry := toOLeanEntry_1, isBuiltin := isBuiltin_1, value := value_1 } →
    toOLeanEntry = toOLeanEntry_1 ∧ isBuiltin = isBuiltin_1 ∧ value = value_1
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.map_fixingSubgroup : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (E : IntermediateField K L)
  (σ : Gal(L/K)), (IntermediateField.map (↑σ) E).fixingSubgroup = MulAut.conj σ • E.fixingSubgroup
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.isSome_succMany?_of_lt_length_toList : ∀ {α : Type u} {r : Std.Rci α} [inst : LT α] [DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst : Std.Rxi.IsAlwaysFinite α] {i : ℕ}, i < r.toList.length → (Std.PRange.succMany? i r.lower).isSome = true
-- Plausible.Random
/-- Get the range of Nat that can be generated by the generator `g`  -/
Plausible.Rand.range : {m : Type → Type u_1} → {g : Type} → [RandomGen g] → [Monad m] → Plausible.RandGT g m (ℕ × ℕ)
-- Mathlib.Order.TransfiniteIteration
monotone_transfiniteIterate : ∀ {I : Type u} [inst : CompleteLattice I] (φ : I → I) (i₀ : I) {J : Type w} [inst_1 : LinearOrder J] [OrderBot J]
  [inst_3 : SuccOrder J] [inst_4 : WellFoundedLT J], (∀ (i : I), i ≤ φ i) → Monotone fun j => transfiniteIterate φ j i₀
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.colimitUnopIsoOpLimit.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor Jᵒᵖ Cᵒᵖ) [inst_2 : CategoryTheory.Limits.HasLimit F],
  CategoryTheory.Limits.colimitUnopIsoOpLimit F =
    CategoryTheory.Limits.colimit.isoColimitCocone
      { cocone := CategoryTheory.Limits.coconeUnopOfCone (CategoryTheory.Limits.limit.cone F),
        isColimit := CategoryTheory.Limits.isColimitCoconeUnopOfCone F (CategoryTheory.Limits.limit.isLimit F) }
-- Mathlib.Data.Matrix.PEquiv
PEquiv.toMatrix_trans : ∀ {l : Type u_2} {m : Type u_3} {n : Type u_4} {α : Type u_5} [inst : Fintype m] [inst_1 : DecidableEq m]
  [inst_2 : DecidableEq n] [inst_3 : NonAssocSemiring α] (f : l ≃. m) (g : m ≃. n),
  (f.trans g).toMatrix = f.toMatrix * g.toMatrix
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.ext_iff : ∀ {x y : SimplexCategoryGenRel}, x = y ↔ x.len = y.len
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.CaseTrace.i : Lean.Meta.Grind.CaseTrace → ℕ
-- Mathlib.MeasureTheory.Measure.Prod
/-- The Lebesgue integral is measurable. This shows that the integrand of (the right-hand-side of)
Tonelli's theorem is measurable.  -/
Measurable.lintegral_prod_right' : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {ν : MeasureTheory.Measure β}
  [MeasureTheory.SFinite ν] {f : α × β → ENNReal}, Measurable f → Measurable fun x => ∫⁻ (y : β), f (x, y) ∂ν
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.Simprocs.mk.sizeOf_spec : ∀ (pre post : Lean.Meta.Simp.SimprocTree) (simprocNames erased : Lean.PHashSet Lean.Name),
  sizeOf { pre := pre, post := post, simprocNames := simprocNames, erased := erased } =
    1 + sizeOf pre + sizeOf post + sizeOf simprocNames + sizeOf erased
-- Mathlib.Computability.PartrecCode
Nat.Partrec.Code.comp.sizeOf_spec : ∀ (a a_1 : Nat.Partrec.Code), sizeOf (a.comp a_1) = 1 + sizeOf a + sizeOf a_1
-- Mathlib.Algebra.CharZero.Defs
Nat.cast_ne_one : ∀ {R : Type u_1} [inst : AddMonoidWithOne R] [CharZero R] {n : ℕ}, ↑n ≠ 1 ↔ n ≠ 1
-- Mathlib.Util.Notation3
/-- `notation3` argument matching `extBinders`.  -/
Mathlib.Notation3.bindersItem : Lean.ParserDescr
-- Mathlib.Topology.Instances.Int
Int.instMetricSpace : MetricSpace ℤ
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.assemble₄_eq_some_of_toBitVec : ∀ {w x y z : UInt8},
  ByteArray.utf8DecodeChar?.isInvalidContinuationByte x = false →
    ByteArray.utf8DecodeChar?.isInvalidContinuationByte y = false →
      ByteArray.utf8DecodeChar?.isInvalidContinuationByte z = false →
        ∀ {c : Char},
          65536 ≤ c.val →
            c.val.toBitVec =
                BitVec.setWidth 32
                  (BitVec.setWidth 3 w.toBitVec ++ BitVec.setWidth 6 x.toBitVec ++ BitVec.setWidth 6 y.toBitVec ++
                    BitVec.setWidth 6 z.toBitVec) →
              ByteArray.utf8DecodeChar?.assemble₄ w x y z = some c
-- Mathlib.Order.Filter.Pointwise
Filter.HasBasis.neg : ∀ {α : Type u_2} [inst : InvolutiveNeg α] {f : Filter α} {ι : Sort u_7} {p : ι → Prop} {s : ι → Set α},
  f.HasBasis p s → (-f).HasBasis p fun i => -s i
-- Lean.LocalContext
Lean.LocalContext.anyM : {m : Type → Type u_1} → [Monad m] → Lean.LocalContext → (Lean.LocalDecl → m Bool) → m Bool
-- Init.Control.Lawful.Instances
ReaderT.run_pure : ∀ {m : Type u_1 → Type u_2} {α ρ : Type u_1} [inst : Monad m] (a : α) (ctx : ρ), (pure a).run ctx = pure a
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Scheme.instEtaleHomDiscretePUnit : ∀ (X : AlgebraicGeometry.Scheme) (Y : X.Etale), AlgebraicGeometry.Etale Y.hom
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- The negation of a Jacobian point representative on a Weierstrass curve.  -/
WeierstrassCurve.Jacobian.neg : {R : Type r} → [CommRing R] → WeierstrassCurve.Jacobian R → (Fin 3 → R) → Fin 3 → R
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.insert.match_1.eq_1 : ∀ {n : ℕ} (motive : Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n → Sort u_1)
  (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)))
  (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)))
  (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment)
  (h_1 :
    (clauses : Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n))) →
      (rupUnits ratUnits : Array (Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))) →
        (assignments : Array Std.Tactic.BVDecide.LRAT.Internal.Assignment) →
          motive { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments }),
  (match { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } with
    | { clauses := clauses, rupUnits := rupUnits, ratUnits := ratUnits, assignments := assignments } =>
      h_1 clauses rupUnits ratUnits assignments) =
    h_1 clauses rupUnits ratUnits assignments
-- Mathlib.Algebra.Group.Ext
CancelCommMonoid.ext : ∀ {M : Type u_1} ⦃m₁ m₂ : CancelCommMonoid M⦄, HMul.hMul = HMul.hMul → m₁ = m₂
-- Lean.Declaration
Lean.Declaration.mutualDefnDecl.sizeOf_spec : ∀ (defns : List Lean.DefinitionVal), sizeOf (Lean.Declaration.mutualDefnDecl defns) = 1 + sizeOf defns
-- Mathlib.Analysis.Complex.Conformal
/-- In cases where the **Cauchy-Riemann Equation** guarantees complex differentiability at `x`, the
complex derivative equals the real derivative.
 -/
complexOfReal_derivWithin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {s : Set ℂ},
  DifferentiableWithinAt ℝ f s x →
    (fderivWithin ℝ f s x) Complex.I = Complex.I • (fderivWithin ℝ f s x) 1 →
      UniqueDiffWithinAt ℂ s x → derivWithin f s x = (fderivWithin ℝ f s x) 1
-- Init.Data.Int.DivMod.Lemmas
Int.le_mul_of_ediv_le : ∀ {a b c : ℤ}, 0 ≤ b → b ∣ a → a / b ≤ c → a ≤ c * b
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
CategoryTheory.Triangulated.TStructure.truncLEIsoTruncLT.congr_simp : ∀ {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]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a + 1 = b),
  t.truncLEIsoTruncLT a b h = t.truncLEIsoTruncLT a b h
-- Init.Data.Vector.Lemmas
Vector.not_mem_append : ∀ {α : Type u_1} {n m : ℕ} {a : α} {xs : Vector α n} {ys : Vector α m}, a ∉ xs → a ∉ ys → a ∉ xs ++ ys