mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Ideal.Maps
/-- The pullback of a maximal ideal under a ring isomorphism is a maximal ideal.  -/
Ideal.comap_isMaximal_of_equiv : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {E : Type u_4} [inst_2 : EquivLike E R S]
  [inst_3 : RingEquivClass E R S] (e : E) {p : Ideal S} [hp : p.IsMaximal], (Ideal.comap e p).IsMaximal
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
curveIntegral_add : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {a b : E}
  {ω₁ ω₂ : E → E →L[𝕜] F} {γ : Path a b},
  CurveIntegrable ω₁ γ →
    CurveIntegrable ω₂ γ → curveIntegral (ω₁ + ω₂) γ = ∫ᶜ (x : E) in γ, ω₁ x + ∫ᶜ (x : E) in γ, ω₂ x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.inv_singleton : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Inv α] (a : α), {a}⁻¹ = {a⁻¹}
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.isParabolic_conj_iff : ∀ {R : Type u_1} [inst : CommRing R] {m : Matrix (Fin 2) (Fin 2) R} (g : GL (Fin 2) R),
  (↑g * m * (↑g)⁻¹).IsParabolic ↔ m.IsParabolic
-- Batteries.Recycling.RBTree.Alter
/-- `O(log n)`. In-place replace the corresponding to key `k`.
This takes the element out of the tree while `f` runs,
so it uses the element linearly if `t` is unshared.
 -/
RBTree.RBMap.modify : {α : Type u_1} → {β : Type u_2} → {cmp : α → α → Ordering} → RBTree.RBMap α β cmp → α → (β → β) → RBTree.RBMap α β cmp
-- Aesop.Stats.Basic
Aesop.instToJsonGoalStats : Lean.ToJson Aesop.GoalStats
-- Mathlib.Algebra.Group.Subgroup.Basic
Subgroup.prod_mono_left : ∀ {G : Type u_1} [inst : Group G] {N : Type u_5} [inst_1 : Group N] (H : Subgroup N), Monotone fun K => K.prod H
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.algebraMap_surjective : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι), Function.Surjective ⇑(algebraMap P.Ring S)
-- Init.Data.Array.Find
Array.findIdx_of_getElem?_eq_some : ∀ {α : Type u_1} {p : α → Bool} {y : α} {xs : Array α}, xs[Array.findIdx p xs]? = some y → p y = true
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.map_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  (P : CategoryTheory.MorphismProperty C) (F : CategoryTheory.Functor C D), P.isoClosure.map F = P.map F
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.mul_comp_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {M N X : C} [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] (f₁ f₂ : X ⟶ M) (g : M ⟶ N)
  [CategoryTheory.IsMonHom g] {Z : C} (h : N ⟶ Z),
  CategoryTheory.CategoryStruct.comp (f₁ * f₂) (CategoryTheory.CategoryStruct.comp g h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CategoryStruct.comp f₁ g * CategoryTheory.CategoryStruct.comp f₂ g) h
-- Std.Http.Transport
/-- Receives data, joining all available chunks.
 -/
Std.Http.Internal.Mock.Client.recv? : Std.Http.Internal.Mock.Client → optParam (Option UInt64) none → Std.Async.Async (Option ByteArray)
-- Mathlib.Data.Seq.Computation
Computation.LiftRelAux.eq_3 : ∀ {α : Type u} {β : Type v} (R : α → β → Prop) (C : Computation α → Computation β → Prop) (ca : Computation α) (b : β),
  Computation.LiftRelAux R C (Sum.inr ca) (Sum.inl b) = ∃ a ∈ ca, R a b
-- Init.Data.SInt.Lemmas
ISize.minValue_le : ∀ (a : ISize), ISize.minValue ≤ a
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasStrictDerivAt.mul_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝔸 : Type u_3} [inst_1 : NormedRing 𝔸]
  [inst_2 : NormedAlgebra 𝕜 𝔸] {c : 𝕜 → 𝔸} {c' : 𝔸},
  HasStrictDerivAt c c' x → ∀ (d : 𝔸), HasStrictDerivAt (fun y => c y * d) (c' * d) x
-- Mathlib.Order.Ideal
Order.Ideal.coe_subset_coe : ∀ {P : Type u_1} [inst : LE P] {s t : Order.Ideal P}, ↑s ⊆ ↑t ↔ s ≤ t
-- Mathlib.Analysis.Calculus.FDeriv.Congr
DifferentiableWithinAt.congr_of_eventuallyEq_insert : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f f₁ : E → F} {x : E} {s : Set E},
  DifferentiableWithinAt 𝕜 f s x → f₁ =ᶠ[nhdsWithin x (insert x s)] f → DifferentiableWithinAt 𝕜 f₁ s x
-- Mathlib.Order.SymmDiff
symmDiff_snd : ∀ {α : Type u_2} {β : Type u_3} [inst : GeneralizedCoheytingAlgebra α] [inst_1 : GeneralizedCoheytingAlgebra β]
  (a b : α × β), (symmDiff a b).2 = symmDiff a.2 b.2
-- Init.Data.List.Sublist
List.replicate_sublist_replicate : ∀ {α : Type u_1} {m n : ℕ} (a : α), (List.replicate m a).Sublist (List.replicate n a) ↔ m ≤ n
-- Mathlib.Geometry.Manifold.Diffeomorph
/-- `n`-times continuously differentiable diffeomorphism between `E` and `E'`.  -/
Manifold.«term_≃ₘ^_[_]_» : Lean.TrailingParserDescr
-- Init.Data.List.Nat.TakeDrop
List.zip_replicate : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} {m n : ℕ},
  (List.replicate m a).zip (List.replicate n b) = List.replicate (min m n) (a, b)
-- Init.Data.Array.MinMax
Array.min_mem : ∀ {α : Type u_1} [inst : Min α] [Std.MinEqOr α] {xs : Array α} (h : xs ≠ #[]), xs.min h ∈ xs
-- Mathlib.Analysis.Normed.Affine.AddTorsorBases
isOpenMap_barycentric_coord : ∀ {ι : Type u_1} {𝕜 : Type u_2} {E : Type u_3} {P : Type u_4} [inst : NontriviallyNormedField 𝕜] [CompleteSpace 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] [inst_4 : MetricSpace P] [inst_5 : NormedAddTorsor E P]
  [Nontrivial ι] (b : AffineBasis ι 𝕜 P) (i : ι), IsOpenMap ⇑(b.coord i)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
SimplyConnectedSpace.mk : ∀ {X : Type u_3} [inst : TopologicalSpace X],
  Nonempty (FundamentalGroupoid X ≌ CategoryTheory.Discrete Unit) → SimplyConnectedSpace X
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
AbsoluteValue.map_neg : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : PartialOrder S] [IsOrderedRing S] [inst_3 : Ring R]
  (abv : AbsoluteValue R S) [NoZeroDivisors S] (a : R), abv (-a) = abv a
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.IsNilpotent_substAlgHom : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommRing R] {τ : Type u_4} {S : Type u_5} [inst_1 : CommRing S]
  [inst_2 : Algebra R S] {a : σ → MvPowerSeries τ S} (ha : MvPowerSeries.HasSubst a) {f : MvPowerSeries σ R},
  IsNilpotent (MvPowerSeries.constantCoeff f) →
    IsNilpotent (MvPowerSeries.constantCoeff ((MvPowerSeries.substAlgHom ha) f))
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.natural.congr_simp : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} {β : ι → Type u_3} [inst : (i : ι) → TopologicalSpace (β i)]
  [inst_1 : ∀ (i : ι), TopologicalSpace.MetrizableSpace (β i)] [mβ : (i : ι) → MeasurableSpace (β i)]
  [inst_2 : ∀ (i : ι), BorelSpace (β i)] [inst_3 : Preorder ι] (u u_1 : (i : ι) → Ω → β i) (e_u : u = u_1)
  (hum : ∀ (i : ι), MeasureTheory.StronglyMeasurable (u i)),
  MeasureTheory.Filtration.natural u hum = MeasureTheory.Filtration.natural u_1 ⋯
-- Std.Do.Triple.SpecLemmas
/-- Like `StringSliceInvariant.withEarlyReturn`, but for the new `do` elaborator which uses `Prod`
instead of `MProd` for the state tuple.  -/
Std.Do.StringSliceInvariant.withEarlyReturnNewDo : {β : Type (max u₁ u₂)} →
  {ps : Std.Do.PostShape} →
    {γ : Type (max u₁ u₂)} →
      {s : String.Slice} →
        (s.Pos → β → Std.Do.Assertion ps) →
          (γ → β → Std.Do.Assertion ps) →
            optParam (Std.Do.ExceptConds ps) Std.Do.ExceptConds.false → Std.Do.StringSliceInvariant s (Option γ × β) ps
-- Std.Time.Duration
/-- Proof that the duration is valid, ensuring that the `second` and `nano` values are correctly related.
 -/
Std.Time.Duration.proof : ∀ (self : Std.Time.Duration), self.second.val ≥ 0 ∧ ↑self.nano ≥ 0 ∨ self.second.val ≤ 0 ∧ ↑self.nano ≤ 0
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatLeftHomologyData_liftK_hom : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {M : ModuleCat R} (φ : M ⟶ S.X₂)
  (h : CategoryTheory.CategoryStruct.comp φ S.g = 0),
  ModuleCat.Hom.hom (S.moduleCatLeftHomologyData.liftK φ h) =
    LinearMap.codRestrict (ModuleCat.Hom.hom S.g).ker (ModuleCat.Hom.hom φ) ⋯
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.besselPotential_besselPotential_apply : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] (s s' : ℝ) (f : TemperedDistribution E F),
  (TemperedDistribution.besselPotential E F s') ((TemperedDistribution.besselPotential E F s) f) =
    (TemperedDistribution.besselPotential E F (s + s')) f
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKeyD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List (α × β)} {k fallback : α},
  (List.map Prod.fst l).contains k = false → (t.insertMany l).getKeyD k fallback = t.getKeyD k fallback
-- Init.Data.List.Scan.Lemmas
_private.Init.Data.List.Scan.Lemmas.0.List.scanAuxM.go.match_1.eq_1 : ∀ {β : Type u_2} {α : Type u_1} (motive : List α → β → List β → Sort u_3) (last : β) (acc : List β)
  (h_1 : (last : β) → (acc : List β) → motive [] last acc)
  (h_2 : (x : α) → (xs : List α) → (last : β) → (acc : List β) → motive (x :: xs) last acc),
  (match [], last, acc with
    | [], last, acc => h_1 last acc
    | x :: xs, last, acc => h_2 x xs last acc) =
    h_1 last acc
-- Init.Tactics
/-- `intros` repeatedly applies `intro` to introduce zero or more hypotheses
until the goal is no longer a *binding expression*
(i.e., a universal quantifier, function type, implication, or `have`/`let`),
without performing any definitional reductions (no unfolding, beta, eta, etc.).
The introduced hypotheses receive inaccessible (hygienic) names.

`intros x y z` is equivalent to `intro x y z` and exists only for historical reasons.
The `intro` tactic should be preferred in this case.

## Properties and relations

- `intros` succeeds even when it introduces no hypotheses.

- `repeat intro` is like `intros`, but it performs definitional reductions
  to expose binders, and as such it may introduce more hypotheses than `intros`.

- `intros` is equivalent to `intro _ _ … _`,
  with the fewest trailing `_` placeholders needed so that the goal is no longer a binding expression.
  The trailing introductions do not perform any definitional reductions.

## Examples

Implications:
```lean
example (p q : Prop) : p → q → p := by
  intros
  /- Tactic state
     a✝¹ : p
     a✝ : q
     ⊢ p      -/
  assumption
```

Let-bindings:
```lean
example : let n := 1; let k := 2; n + k = 3 := by
  intros
  /- n✝ : Nat := 1
     k✝ : Nat := 2
     ⊢ n✝ + k✝ = 3 -/
  rfl
```

Does not unfold definitions:
```lean
def AllEven (f : Nat → Nat) := ∀ n, f n % 2 = 0

example : ∀ (f : Nat → Nat), AllEven f → AllEven (fun k => f (k + 1)) := by
  intros
  /- Tactic state
     f✝ : Nat → Nat
     a✝ : AllEven f✝
     ⊢ AllEven fun k => f✝ (k + 1) -/
  sorry
```
 -/
Lean.Parser.Tactic.intros : Lean.ParserDescr
-- Mathlib.CategoryTheory.SmallObject.IsCardinalForSmallObjectArgument
CategoryTheory.SmallObject.transfiniteCompositionsOfShape_ιObj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (I : CategoryTheory.MorphismProperty C) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [inst_2 : OrderBot κ.ord.ToType] [inst_3 : I.IsCardinalForSmallObjectArgument κ] {X Y : C}
  (f : X ⟶ Y),
  (CategoryTheory.MorphismProperty.coproducts.{w, v, u} I).pushouts.transfiniteCompositionsOfShape κ.ord.ToType
    (CategoryTheory.SmallObject.ιObj I κ f)
-- Mathlib.Analysis.Calculus.TangentCone.Real
uniqueDiffOn_Ici : ∀ (a : ℝ), UniqueDiffOn ℝ (Set.Ici a)
-- Mathlib.NumberTheory.LSeries.Convolution
/-- We give an expression of the `LSeries.term` of the convolution of two functions
in terms of a sum over `Nat.divisorsAntidiagonal`.  -/
LSeries.term_convolution : ∀ (f g : ℕ → ℂ) (s : ℂ) (n : ℕ),
  LSeries.term (LSeries.convolution f g) s n = ∑ p ∈ n.divisorsAntidiagonal, LSeries.term f s p.1 * LSeries.term g s p.2
-- Lean.Meta.Tactic.Grind.Arith.Simproc
Lean.Meta.Grind.Arith.normIntSubInst : Lean.Meta.Simp.DSimproc
-- Mathlib.Geometry.Euclidean.Sphere.Basic
EuclideanGeometry.Sphere.IsDiameter.left_eq_right_iff : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s : EuclideanGeometry.Sphere P} {p₁ p₂ : P},
  s.IsDiameter p₁ p₂ → (p₁ = p₂ ↔ s.radius = 0)
-- Lean.Parser.Types
/-- Run `p` under the given context transformation with a fresh cache (see also `withResetCacheFn`).  -/
Lean.Parser.adaptUncacheableContextFn : (Lean.Parser.ParserContextCore → Lean.Parser.ParserContextCore) → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Data.String.Basic
String.le_iff_toList_le : ∀ {s₁ s₂ : String}, s₁ ≤ s₂ ↔ s₁.toList ≤ s₂.toList
-- Mathlib.Computability.Partrec
Nat.rfind_spec : ∀ {p : ℕ →. Bool} {n : ℕ}, n ∈ Nat.rfind p → true ∈ p n
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.piUnique_symm_apply : ∀ {ι : Type u_7} (R : ι → Type u_8) [inst : Unique ι] [inst_1 : (i : ι) → NonUnitalNonAssocSemiring (R i)],
  ⇑(RingEquiv.piUnique R).symm = uniqueElim
-- Mathlib.Data.TypeVec
/-- arrow composition in the category of `TypeVec`  -/
TypeVec.comp : {n : ℕ} → {α : TypeVec.{u} n} → {β : TypeVec.{v} n} → {γ : TypeVec.{w} n} → β.Arrow γ → α.Arrow β → α.Arrow γ
-- Mathlib.Algebra.Group.TypeTags.Basic
instSubsingletonAdditive : ∀ {α : Type u} [Subsingleton α], Subsingleton (Additive α)
-- Mathlib.Algebra.FreeMonoid.Basic
/-- A version of `List.cases_on` for `FreeMonoid` using `1` and `FreeMonoid.of x * xs` instead of
`[]` and `x :: xs`.  -/
FreeMonoid.casesOn : {α : Type u_1} →
  {motive : FreeMonoid α → Sort u_6} →
    (xs : FreeMonoid α) → motive 1 → ((x : α) → (xs : FreeMonoid α) → motive (FreeMonoid.of x * xs)) → motive xs
-- Mathlib.Data.Nat.Factorization.Defs
/-- For any `p : ℕ` and any function `g : α → ℕ` that's non-zero on `S : Finset α`,
the power of `p` in `S.prod g` equals the sum over `x ∈ S` of the powers of `p` in `g x`.
Generalises `factorization_mul`, which is the special case where `#S = 2` and `g = id`.  -/
Nat.factorization_prod : ∀ {α : Type u_1} {S : Finset α} {g : α → ℕ},
  (∀ x ∈ S, g x ≠ 0) → (S.prod g).factorization = ∑ x ∈ S, (g x).factorization
-- Mathlib.AlgebraicGeometry.Cover.Open
AlgebraicGeometry.Scheme.openCover_affineOpenCover : ∀ (X : AlgebraicGeometry.Scheme), X.affineOpenCover.openCover = X.affineCover
-- Mathlib.Order.Filter.Basic
Filter.monotone_mem : ∀ {α : Type u} {f : Filter α}, Monotone fun s => s ∈ f
-- Mathlib.CategoryTheory.Filtered.CostructuredArrow
_private.Mathlib.CategoryTheory.Filtered.CostructuredArrow.0.CategoryTheory.isFiltered_of_isFiltered_costructuredArrow_small : ∀ {A : Type u₁} [inst : CategoryTheory.SmallCategory A] {B : Type u₁} [inst_1 : CategoryTheory.SmallCategory B]
  {T : Type u₁} [inst_2 : CategoryTheory.SmallCategory T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) [CategoryTheory.IsFiltered B] [R.Final]
  [∀ (b : B), CategoryTheory.IsFiltered (CategoryTheory.CostructuredArrow L (R.obj b))], CategoryTheory.IsFiltered A
-- Mathlib.Analysis.Convex.SpecificFunctions.Pow
NNReal.strictConcaveOn_rpow : ∀ {p : ℝ}, 0 < p → p < 1 → StrictConcaveOn NNReal Set.univ fun x => x ^ p
-- Mathlib.Algebra.Order.Monovary
/-- **Alias** of the forward direction of `antivary_inv_right₀`. -/
Antivary.of_inv_right₀ : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : Semifield β] [inst_2 : LinearOrder β]
  [IsStrictOrderedRing β] {f : ι → α} {g : ι → β}, StrongLT 0 g → Antivary f g⁻¹ → Monovary f g
-- Mathlib.Order.Hom.Lattice
SupHom.instOrderTop.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Max α] [inst_1 : SemilatticeSup β] [inst_2 : OrderTop β],
  SupHom.instOrderTop = OrderTop.lift DFunLike.coe ⋯ ⋯
-- Lean.Language.Basic
Lean.Language.TransformedSnap.mk.sizeOf_spec : ∀ {α : Type} [inst : SizeOf α] (raw : α) (transform : Lean.Language.SnapshotTreeTransform),
  sizeOf { raw := raw, transform := transform } = 1 + sizeOf raw + sizeOf transform
-- Mathlib.Topology.Category.LightProfinite.Basic
LightProfinite.of.congr_simp : ∀ (X : Type u_1) [inst : TopologicalSpace X] [inst_1 : CompactSpace X] [inst_2 : T2Space X]
  [inst_3 : TotallyDisconnectedSpace X] [inst_4 : SecondCountableTopology X], LightProfinite.of X = LightProfinite.of X
-- Mathlib.NumberTheory.LegendreSymbol.JacobiSymbol
/-- We have that `J(a^e | b) = J(a | b)^e`.  -/
jacobiSym.pow_left : ∀ (a : ℤ) (e b : ℕ), jacobiSym (a ^ e) b = jacobiSym a b ^ e
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.coe_lt_inducedMap_iff`. -/
LinearOrderedField.coe_lt_inducedMap_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α} {q : ℚ},
  ↑q < ConditionallyCompleteLinearOrderedField.inducedMap α β a ↔ ↑q < a
-- Mathlib.CategoryTheory.Sites.Point.Skyscraper
CategoryTheory.GrothendieckTopology.Point.skyscraperPresheafHomEquiv_naturality_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.Limits.HasProducts A]
  {P Q : CategoryTheory.Functor Cᵒᵖ A} {M : A} [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A]
  (f : P ⟶ Q) (g : Φ.presheafFiber.obj Q ⟶ M),
  Φ.skyscraperPresheafHomEquiv (CategoryTheory.CategoryStruct.comp (Φ.presheafFiber.map f) g) =
    CategoryTheory.CategoryStruct.comp f (Φ.skyscraperPresheafHomEquiv g)
-- Mathlib.CategoryTheory.Presentable.IsCardinalFiltered
/-- A category is `κ`-filtered iff
1. any family of objects of cardinality `< κ` admits a map towards a common object, and
2. any family of morphisms `j ⟶ k` of cardinality `< κ` (between *fixed* objects
   `j` and `k`) can be coequalized by a suitable morphism `k ⟶ l`.
 -/
CategoryTheory.isCardinalFiltered_iff : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J] (κ : Cardinal.{w}) [inst_1 : Fact κ.IsRegular],
  CategoryTheory.IsCardinalFiltered J κ ↔
    (∀ ⦃ι : Type w⦄ (j : ι → J), HasCardinalLT ι κ → ∃ k, ∀ (i : ι), Nonempty (j i ⟶ k)) ∧
      ∀ ⦃ι : Type w⦄ ⦃j k : J⦄ (f : ι → (j ⟶ k)),
        HasCardinalLT ι κ → ∃ l a b, ∀ (i : ι), CategoryTheory.CategoryStruct.comp (f i) a = b
-- Mathlib.Data.Vector.Basic
/-- The `tail` of a `nil` vector is `nil`.  -/
List.Vector.tail_nil : ∀ {α : Type u_1}, List.Vector.nil.tail = List.Vector.nil
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instAddRightMono : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : PartialOrder β]
  [inst_3 : AddZeroClass β] [inst_4 : ContinuousAdd β] [AddRightMono β],
  AddRightMono (CompactlySupportedContinuousMap α β)
-- Lean.Expr
Lean.PExprSet : Type
-- Mathlib.RingTheory.WittVector.Basic
WittVector.ghostMap.bijective_of_invertible : ∀ (p : ℕ) (R : Type u_1) [inst : CommRing R] [inst_1 : Fact (Nat.Prime p)] [Invertible ↑p],
  Function.Bijective ⇑WittVector.ghostMap
-- Mathlib.Algebra.WithConv
WithConv.ofConv_sum : ∀ {A : Type u_2} [inst : AddCommMonoid A] {ι : Type u_5} (s : Finset ι) (f : ι → WithConv A),
  (∑ i ∈ s, f i).ofConv = ∑ i ∈ s, (f i).ofConv
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context.bInfos : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context → Array Lean.BinderInfo
-- Mathlib.LinearAlgebra.FreeProduct.Basic
LinearAlgebra.FreeProduct.instAlgebra : {I : Type u} →
  [inst : DecidableEq I] →
    (R : Type v) →
      [inst_1 : CommSemiring R] →
        (A : I → Type w) →
          [inst_2 : (i : I) → Semiring (A i)] →
            [inst_3 : (i : I) → Algebra R (A i)] → Algebra R (LinearAlgebra.FreeProduct R A)
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.mkIso_inv_f : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  {X Y : CategoryTheory.DifferentialObject S C} (f : X.obj ≅ Y.obj)
  (hf :
    CategoryTheory.CategoryStruct.comp X.d ((CategoryTheory.shiftFunctor C 1).map f.hom) =
      CategoryTheory.CategoryStruct.comp f.hom Y.d),
  (CategoryTheory.DifferentialObject.mkIso f hf).inv.f = f.inv
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
Subsemigroup.op_injective : ∀ {M : Type u_2} [inst : Mul M], Function.Injective Subsemigroup.op
-- Init.Prelude
/-- Adds an element to the end of an array. The resulting array's size is one greater than the input
array. If there are no other references to the array, then it is modified in-place.

This takes amortized `O(1)` time because `Array α` is represented by a dynamic array.

Examples:
* `#[].push "apple" = #["apple"]`
* `#["apple"].push "orange" = #["apple", "orange"]`
 -/
Array.push : {α : Type u} → Array α → α → Array α
-- Mathlib.Topology.Coherent
Topology.IsCoherentWith.isOpen_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {S : Set (Set X)} {t : Set X},
  Topology.IsCoherentWith S → (IsOpen t ↔ ∀ s ∈ S, IsOpen (Subtype.val ⁻¹' t))
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.CompletionItemKind.function : Lean.Lsp.CompletionItemKind
-- Mathlib.Data.Setoid.Basic
Setoid.refl' : ∀ {α : Type u_1} (r : Setoid α) (x : α), r x x
-- Mathlib.RingTheory.DividedPowers.RatAlgebra
DividedPowers.OfInvertibleFactorial.dpow.eq_1 : ∀ {A : Type u_1} [inst : CommSemiring A] (I : Ideal A) [inst_1 : DecidablePred fun x => x ∈ I] (m : ℕ) (x : A),
  DividedPowers.OfInvertibleFactorial.dpow I m x = if x ∈ I then Ring.inverse ↑m.factorial * x ^ m else 0
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapAddGrpFunctor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : C ⥤ₗ D), CategoryTheory.Functor.mapAddGrpFunctor.obj F = F.obj.mapAddGrp
-- Mathlib.Analysis.Normed.Module.ContinuousInverse
ContinuousLinearMap.HasRightInverse.surjective : ∀ {R : Type u_1} [inst : Semiring R] {E : Type u_2} {F : Type u_4} [inst_1 : TopologicalSpace E]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : TopologicalSpace F] [inst_5 : AddCommMonoid F]
  [inst_6 : Module R F] {f : E →L[R] F}, f.HasRightInverse → Function.Surjective ⇑f
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.ProEt.instPreservesFiniteLimitsOverForget : ∀ (S : AlgebraicGeometry.Scheme), CategoryTheory.Limits.PreservesFiniteLimits (AlgebraicGeometry.Scheme.ProEt.forget S)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_eq_getKey! : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {a : α} {h : a ∈ t}, t.getKey a h = t.getKey! a
-- Mathlib.Algebra.GroupWithZero.Associated
associated_mul_unit_left : ∀ {N : Type u_2} [inst : Monoid N] (a u : N), IsUnit u → Associated (a * u) a
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toProp.eq_6 : ∀ (K : Type u_2) [inst : Add K] [inst_1 : Mul K] [inst_2 : Neg K] [inst_3 : Zero K] [inst_4 : One K],
  FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.oneMul = ∀ (x : K), 1 * x = x
-- Mathlib.Data.Finset.Max
/-- Given a nonempty finset `s` in a linear order `α`, then `s.min' H` is its minimum, as an
element of `α`, where `H` is a proof of nonemptiness. Without this assumption, use instead `s.min`,
taking values in `WithTop α`.  -/
Finset.min' : {α : Type u_2} → [LinearOrder α] → (s : Finset α) → s.Nonempty → α