mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Homotopy.Basic
ContinuousMap.Homotopy.mk.injEq : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f₀ f₁ : C(X, Y)}
  (toContinuousMap : C(↑unitInterval × X, Y)) (map_zero_left : ∀ (x : X), toContinuousMap.toFun (0, x) = f₀ x)
  (map_one_left : ∀ (x : X), toContinuousMap.toFun (1, x) = f₁ x) (toContinuousMap_1 : C(↑unitInterval × X, Y))
  (map_zero_left_1 : ∀ (x : X), toContinuousMap_1.toFun (0, x) = f₀ x)
  (map_one_left_1 : ∀ (x : X), toContinuousMap_1.toFun (1, x) = f₁ x),
  ({ toContinuousMap := toContinuousMap, map_zero_left := map_zero_left, map_one_left := map_one_left } =
      { toContinuousMap := toContinuousMap_1, map_zero_left := map_zero_left_1, map_one_left := map_one_left_1 }) =
    (toContinuousMap = toContinuousMap_1)
-- Mathlib.LinearAlgebra.PiTensorProduct.Finsupp
PiTensorProduct.ofFinsuppEquiv_symm_single_tprod : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : ι → Type u_4} [inst : CommSemiring R] [inst_1 : Fintype ι]
  [inst_2 : DecidableEq ι] [inst_3 : (i : ι) → DecidableEq (κ i)] [inst_4 : (i : ι) → AddCommMonoid (M i)]
  [inst_5 : (i : ι) → Module R (M i)] [inst_6 : (i : ι) → DecidableEq (M i)] (p : (i : ι) → κ i) (m : (i : ι) → M i),
  (PiTensorProduct.ofFinsuppEquiv.symm fun₀ | p => ⨂ₜ[R] (i : ι), m i) =
    (PiTensorProduct.tprod R) fun i => fun₀ | p i => m i
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.DHashMap.Raw.forIn.eq_1 : ∀ {α : Type u} {β : α → Type v} {δ : Type w} {m : Type w → Type w'} [inst : Monad m]
  (f : (a : α) → β a → δ → m (ForInStep δ)) (init : δ) (b : Std.DHashMap.Raw α β),
  Std.DHashMap.Raw.forIn f init b = forIn b.buckets init fun bucket acc => bucket.forInStep acc f
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanClass.orderHom.eq_1 : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] {N : Type u_2}
  [inst_3 : AddCommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedAddMonoid N] (f : M →+o N),
  ArchimedeanClass.orderHom f = (ArchimedeanOrder.orderHom f).antisymmetrization
-- Mathlib.Data.Rat.Cast.Order
NNRat.not_cast_lt_zero : ∀ {K : Type u_5} [inst : Semifield K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K] {q : ℚ≥0}, ¬↑q < 0
-- Mathlib.LinearAlgebra.BilinearForm.Properties
/-- The restriction of a symmetric bilinear form on a submodule is also symmetric.  -/
LinearMap.BilinForm.IsSymm.restrict : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {B : LinearMap.BilinForm R M}, B.IsSymm → ∀ (W : Submodule R M), (B.restrict W).IsSymm
-- Mathlib.AlgebraicGeometry.OpenImmersion
AlgebraicGeometry.Scheme.Hom.preimage_image_eq : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [H : AlgebraicGeometry.IsOpenImmersion f] (U : X.Opens),
  (TopologicalSpace.Opens.map f.base).obj ((AlgebraicGeometry.Scheme.Hom.opensFunctor f).obj U) = U
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get!_filter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  [inst_1 : Inhabited β] {f : α → β → Bool} {k : α} (h : t.WF),
  Std.DTreeMap.Internal.Impl.Const.get! (Std.DTreeMap.Internal.Impl.filter f t ⋯).impl k =
    ((Std.DTreeMap.Internal.Impl.Const.get? t k).pfilter fun x h' => f (t.getKey k ⋯) x).get!
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- A morphism `π` satisfying `f ≫ π = 0` determines a cokernel cofork on `f`.  -/
CategoryTheory.Limits.CokernelCofork.ofπ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {Z : C} → (π : Y ⟶ Z) → CategoryTheory.CategoryStruct.comp f π = 0 → CategoryTheory.Limits.CokernelCofork f
-- Mathlib.Topology.Maps.Basic
Topology.IsInducing.tendsto_nhds_iff : ∀ {Y : Type u_2} {Z : Type u_3} {ι : Type u_4} {g : Y → Z} [inst : TopologicalSpace Y] [inst_1 : TopologicalSpace Z]
  {f : ι → Y} {l : Filter ι} {y : Y},
  Topology.IsInducing g → (Filter.Tendsto f l (nhds y) ↔ Filter.Tendsto (g ∘ f) l (nhds (g y)))
-- Mathlib.Analysis.InnerProductSpace.Positive
ContinuousLinearMap.IsPositive.inner_left_eq_inner_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E}, T.IsPositive → ∀ (x y : E), inner 𝕜 (T x) y = inner 𝕜 x (T y)
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.ofFractionRing_inv : ∀ {K : Type u} [inst : CommRing K] [inst_1 : IsDomain K] (p : FractionRing (Polynomial K)),
  { toFractionRing := p⁻¹ } = { toFractionRing := p }⁻¹
-- Mathlib.RingTheory.DedekindDomain.SelmerGroup
IsDedekindDomain.HeightOneSpectrum.valuationOfNeZero.congr_simp : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type v} [inst_2 : Field K] [inst_3 : Algebra R K]
  [inst_4 : IsFractionRing R K] (v v_1 : IsDedekindDomain.HeightOneSpectrum R),
  v = v_1 → v.valuationOfNeZero = v_1.valuationOfNeZero
-- Mathlib.MeasureTheory.Function.AbsolutelyContinuous
AbsolutelyContinuousOnInterval.neg : ∀ {F : Type u_2} [inst : SeminormedAddCommGroup F] {a b : ℝ} {f : ℝ → F},
  AbsolutelyContinuousOnInterval f a b → AbsolutelyContinuousOnInterval (-f) a b
-- Init.Data.Option.Attach
_private.Init.Data.Option.Attach.0.OptionT.instMonadAttach.match_1.eq_2 : ∀ {m : Type u_1 → Type u_2} [inst : MonadAttach m] {α : Type u_1} (x : OptionT m α)
  (motive : Subtype (MonadAttach.CanReturn x.run) → Sort u_3) (property : MonadAttach.CanReturn x.run none)
  (h_1 : (a : α) → (h : MonadAttach.CanReturn x.run (some a)) → motive ⟨some a, h⟩)
  (h_2 : (property : MonadAttach.CanReturn x.run none) → motive ⟨none, property⟩),
  (match ⟨none, property⟩ with
    | ⟨some a, h⟩ => h_1 a h
    | ⟨none, property⟩ => h_2 property) =
    h_2 property
-- Mathlib.CategoryTheory.Limits.Preserves.Basic
/-- A functor `F : C ⥤ D` reflects limits of shape `J` if
whenever the image of a cone over some `K : J ⥤ C` under `F` is a limit cone in `D`,
the cone was already a limit cone in `C`.
Note that we do not assume a priori that `D` actually has any limits.
 -/
CategoryTheory.Limits.ReflectsLimitsOfShape : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) → [CategoryTheory.Category.{w', w} J] → CategoryTheory.Functor C D → Prop
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.prod_normal : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (H : AddSubgroup G) (K : AddSubgroup N)
  [hH : H.Normal] [hK : K.Normal], (H.prod K).Normal
-- Std.Http.Data.Body.Stream
/-- Attempts to receive a chunk from the channel without blocking.
Returns `some chunk` only when a producer is already waiting.
 -/
Std.Http.Body.Stream.tryRecv : Std.Http.Body.Stream → Std.Async.Async (Option Std.Http.Chunk)
-- Mathlib.Logic.Function.Basic
Function.Surjective.right_cancellable : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β},
  Function.Surjective f → ∀ {g₁ g₂ : β → γ}, g₁ ∘ f = g₂ ∘ f ↔ g₁ = g₂
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
thickenedIndicatorAux_mono : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {δ₁ δ₂ : ℝ},
  δ₁ ≤ δ₂ → ∀ (E : Set α), thickenedIndicatorAux δ₁ E ≤ thickenedIndicatorAux δ₂ E
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
/-- This instance allows `do` notation for `PMF` to be used across universes, for instance as
```lean4
example {R : Type u} [Ring R] (x : PMF ℕ) : PMF R := do
  let ⟨n⟩ ← ULiftable.up x
  pure n
```
where `x` is in universe `0`, but the return value is in universe `u`.
 -/
PMF.instULiftable : ULiftable PMF PMF
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.HasSpectralSequence.isZero_H_obj_mk₁_i₃_le : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Abelian C} {inst_2 : Preorder ι} {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  {X : CategoryTheory.Abelian.SpectralObject C ι}
  {data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀} [self : X.HasSpectralSequence data]
  (r r' : ℤ) (pq : κ),
  (∀ (pq' : κ), ¬(c r).Rel pq' pq) →
    ∀ (n : ℤ),
      n = data.deg pq - 1 →
        ∀ (hrr' : autoParam (r + 1 = r') CategoryTheory.Abelian.SpectralObject.HasSpectralSequence._auto_9)
          (hr : autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.HasSpectralSequence._auto_11),
          CategoryTheory.Limits.IsZero ((X.H n).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE ⋯)))
-- Mathlib.Analysis.Complex.Hadamard
/-- Proof that `F` is bounded by one on the edges.  -/
Complex.HadamardThreeLines.F_edge_le_one : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E),
  ∀ ε > 0,
    ∀ (z : ℂ),
      BddAbove (norm ∘ f '' Complex.HadamardThreeLines.verticalClosedStrip 0 1) →
        z ∈ Complex.re ⁻¹' {0, 1} → ‖Complex.HadamardThreeLines.F f ε z‖ ≤ 1
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜}, MeromorphicOn id U
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.symm_apply : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁)
  (x : ↑unitInterval × ↑unitInterval), F.symm x = F (unitInterval.symm x.1, x.2)
-- Mathlib.Topology.FiberBundle.Basic
FiberPrebundle.continuous_totalSpaceMk : ∀ {B : Type u_2} {F : Type u_3} {E : B → Type u_5} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : (x : B) → TopologicalSpace (E x)] (a : FiberPrebundle F E) (b : B), Continuous (Bundle.TotalSpace.mk b)
-- Mathlib.Tactic.Have
Mathlib.Tactic.haveIdLhs'.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Std.Data.Internal.List.Associative
Std.Internal.List.map_fst_map_toProd_eq_keys : ∀ {α : Type u} {β : Type v} {l : List ((_ : α) × β)},
  List.map Prod.fst (List.map (fun x => (x.fst, x.snd)) l) = Std.Internal.List.keys l
-- Init.Data.List.Basic
List.cons_lex_nil : ∀ {α : Type u} {lt : α → α → Bool} [inst : BEq α] {a : α} {as : List α}, (a :: as).lex [] lt = false
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
LinearMap.separatingRight_toMatrix₂_iff : ∀ {R : Type u_1} {M₁ : Type u_6} {M₂ : Type u_7} {n : Type u_11} {m : Type u_12} [inst : CommRing R]
  [inst_1 : DecidableEq m] [inst_2 : Fintype m] [inst_3 : DecidableEq n] [inst_4 : Fintype n]
  [inst_5 : AddCommMonoid M₁] [inst_6 : Module R M₁] [inst_7 : AddCommMonoid M₂] [inst_8 : Module R M₂]
  (b₁ : Module.Basis m R M₁) (b₂ : Module.Basis n R M₂) {B : M₁ →ₗ[R] M₂ →ₗ[R] R},
  ((LinearMap.toMatrix₂ b₁ b₂) B).SeparatingRight ↔ B.SeparatingRight
-- Std.Data.DTreeMap.Raw.Basic
/-- Folds the given function over the mappings in the map in ascending order.  -/
Std.DTreeMap.Raw.foldl : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → {δ : Type w} → (δ → (a : α) → β a → δ) → δ → Std.DTreeMap.Raw α β cmp → δ
-- Mathlib.Combinatorics.SimpleGraph.DegreeSum
SimpleGraph.Dart.edge_fiber : ∀ {V : Type u} {G : SimpleGraph V} [inst : Fintype V] [inst_1 : DecidableRel G.Adj] [inst_2 : DecidableEq V]
  (d : G.Dart), {d' | d'.edge = d.edge} = {d, d.symm}
-- Mathlib.Probability.Distributions.Geometric
/-- The integral of a function taking values in a finite-dimensional space
against `geometricMeasure p` is given by its sum weighted by `(1 - p) ^ n * p`. This version
does not require integrability, as the integral exists if and only if the sum exists, and otherwise
they are both defined to be zero.

See `integral_geometricMeasure'` with a general codomain which assumes integrability.  -/
ProbabilityTheory.integral_geometricMeasure : ∀ {p : ↑unitInterval} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E],
  p ≠ 0 → ∀ (f : ℕ → E), ∫ (n : ℕ), f n ∂ProbabilityTheory.geometricMeasure p = ∑' (n : ℕ), ((1 - ↑p) ^ n * ↑p) • f n
-- Mathlib.Order.Interval.Set.Basic
Set.instNoMaxOrderElemIco : ∀ (α : Type u_1) [inst : Preorder α] [DenselyOrdered α] {x y : α}, NoMaxOrder ↑(Set.Ico y x)
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- The "reproducing" property of the kernel functions, right version.  -/
RKHS.inner_kerFun : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (x : X) (v : V) (f : H),
  inner 𝕜 f ((RKHS.kerFun H x) v) = inner 𝕜 (f x) v
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.galoisConnection_pushforward_pullback : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X),
  GaloisConnection (CategoryTheory.Presieve.pushforward f) (CategoryTheory.Presieve.pullback f)
-- Init.Data.String.Decode
_private.Init.Data.String.Decode.0.ByteArray.utf8DecodeChar?.FirstByte.utf8ByteSize.match_1.eq_4 : ∀ (motive : ByteArray.utf8DecodeChar?.FirstByte → Sort u_1)
  (h_1 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.invalid)
  (h_2 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.done)
  (h_3 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.oneMore)
  (h_4 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.twoMore)
  (h_5 : Unit → motive ByteArray.utf8DecodeChar?.FirstByte.threeMore),
  (match ByteArray.utf8DecodeChar?.FirstByte.twoMore with
    | ByteArray.utf8DecodeChar?.FirstByte.invalid => h_1 ()
    | ByteArray.utf8DecodeChar?.FirstByte.done => h_2 ()
    | ByteArray.utf8DecodeChar?.FirstByte.oneMore => h_3 ()
    | ByteArray.utf8DecodeChar?.FirstByte.twoMore => h_4 ()
    | ByteArray.utf8DecodeChar?.FirstByte.threeMore => h_5 ()) =
    h_4 ()
-- Mathlib.AlgebraicTopology.ModelCategory.Instances
HomotopicalAlgebra.instIsMultiplicativeFibrations : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C]
  [inst_2 : HomotopicalAlgebra.CategoryWithCofibrations C] [inst_3 : HomotopicalAlgebra.CategoryWithFibrations C]
  [(HomotopicalAlgebra.trivialCofibrations C).IsWeakFactorizationSystem (HomotopicalAlgebra.fibrations C)],
  (HomotopicalAlgebra.fibrations C).IsMultiplicative
-- Mathlib.LinearAlgebra.CliffordAlgebra.Contraction
CliffordAlgebra.contractRight_algebraMap_mul : ∀ {R : Type u1} [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} (d : Module.Dual R M) (r : R) (b : CliffordAlgebra Q),
  (CliffordAlgebra.contractRight ((algebraMap R (CliffordAlgebra Q)) r * b)) d =
    (algebraMap R (CliffordAlgebra Q)) r * (CliffordAlgebra.contractRight b) d
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.smul.eq_1 : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M] [hS : SMulMemClass S R M] (s : S),
  SetLike.smul s = { smul := fun r x => ⟨r • ↑x, ⋯⟩ }
-- Mathlib.Data.Set.Lattice
Set.inter_iUnion : ∀ {β : Type u_2} {ι : Sort u_5} (s : Set β) (t : ι → Set β), s ∩ ⋃ i, t i = ⋃ i, s ∩ t i
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.setOfFractNe.eq_1 : ∀ {ι : Type u_3} {s : Set (ι → ℕ)} (hs : IsProperLinearSet s) [inst : Finite ι],
  IsProperLinearSet.setOfFractNe✝ hs = {x | IsProperLinearSet.fract✝ hs x ≠ IsProperLinearSet.base✝ hs}
-- Aesop.Script.StructureStatic
Aesop.Script.StaticStructureM.Context.mk.sizeOf_spec : ∀ (steps : Std.HashMap Lean.MVarId (ℕ × Aesop.Script.Step)), sizeOf { steps := steps } = 1 + sizeOf steps
-- Mathlib.Algebra.AddConstMap.Basic
/-- The map that sends `c` to a translation by `c`
as a monoid homomorphism from `Multiplicative G` to `G →+c[a, a] G`.  -/
AddConstMap.addLeftHom : {G : Type u_1} → [inst : AddMonoid G] → {a : G} → Multiplicative G →* AddConstMap G G a a
-- Mathlib.LinearAlgebra.DFinsupp
/-- Interpret `fun (f : Π₀ i, M i) ↦ f i` as a linear map.  -/
DFinsupp.lapply : {ι : Type u_1} →
  {R : Type u_3} →
    {M : ι → Type u_5} →
      [inst : Semiring R] →
        [inst_1 : (i : ι) → AddCommMonoid (M i)] →
          [inst_2 : (i : ι) → Module R (M i)] → (i : ι) → (Π₀ (i : ι), M i) →ₗ[R] M i
-- Mathlib.Topology.Algebra.Ring.Compact
Ideal.isOpen_of_isMaximal : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R] [CompactSpace R] [T2Space R]
  [IsNoetherianRing R] (I : Ideal R) [I.IsMaximal], IsOpen ↑I
-- Mathlib.Order.WellFoundedSet
Set.isPWO_insert : ∀ {α : Type u_2} [inst : Preorder α] {s : Set α} {a : α}, (insert a s).IsPWO ↔ s.IsPWO
-- Mathlib.Analysis.InnerProductSpace.StandardSubspace
StandardSubspace.symplComp_symplComp_eq : ∀ {H : Type u_1} [inst : NormedAddCommGroup H] [inst_1 : InnerProductSpace ℂ H] [inst_2 : CompleteSpace H]
  (S : StandardSubspace H), S.symplComp.symplComp = S
-- Mathlib.GroupTheory.Perm.Cycle.Basic
Equiv.Perm.IsCycleOn.of_zpow : ∀ {α : Type u_2} {f : Equiv.Perm α} {s : Set α} {n : ℤ}, (f ^ n).IsCycleOn s → Set.BijOn (⇑f) s s → f.IsCycleOn s
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
AddSubgroup.isAddCyclic_zmultiples : ∀ {G : Type u_2} [inst : AddGroup G] (g : G), IsAddCyclic ↥(AddSubgroup.zmultiples g)
-- Mathlib.CategoryTheory.Abelian.Exact
/-- If `(f, g)` is exact, then `image.ι f` is a kernel of `g`.  -/
CategoryTheory.ShortComplex.Exact.isLimitImage' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {S : CategoryTheory.ShortComplex C} →
        S.Exact →
          CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.image.ι S.f) ⋯)
-- Mathlib.CategoryTheory.Sites.Over
CategoryTheory.Sieve.overEquiv_symm_generate : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {Y : CategoryTheory.Over X}
  (R : CategoryTheory.Presieve Y.left),
  (CategoryTheory.Sieve.overEquiv Y).symm (CategoryTheory.Sieve.generate R) =
    CategoryTheory.Sieve.generate (CategoryTheory.Presieve.functorPullback (CategoryTheory.Over.forget X) R)
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
LaurentPolynomial.comul_C_mul_T : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] (a : A) (n : ℤ),
  CoalgebraStruct.comul (LaurentPolynomial.C a * LaurentPolynomial.T n) =
    (TensorProduct.map (AddMonoidAlgebra.lsingle n) (AddMonoidAlgebra.lsingle n)) (CoalgebraStruct.comul a)
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.currySumEquiv_symm_apply : ∀ {R : Type uR} {ι : Type uι} {ι' : Type uι'} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] {N : ι ⊕ ι' → Type u_1} [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)]
  [inst_4 : (i : ι ⊕ ι') → Module R (N i)]
  (g : MultilinearMap R (fun i => N (Sum.inl i)) (MultilinearMap R (fun i => N (Sum.inr i)) M₂)),
  MultilinearMap.currySumEquiv.symm g = g.uncurrySum
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
ZeroHom.withBotMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N),
  f.withBotMap = { toFun := WithBot.map ⇑f, map_zero' := ⋯ }
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
IsValuativeTopology.hasBasis_nhds_zero : ∀ (R : Type u_1) [inst : Ring R] [inst_1 : ValuativeRel R] [inst_2 : TopologicalSpace R] [IsValuativeTopology R],
  (nhds 0).HasBasis (fun x => True) fun γ => {x | (ValuativeRel.valuation R) x < ↑γ}
-- Mathlib.RingTheory.Ideal.GoingUp
/-- `comap (algebraMap R S)` is a surjection from the max spec of `S` to max spec of `R`.
`hP : (algebraMap R S).ker ≤ P` is a slight generalization of the extension being injective  -/
Ideal.exists_ideal_over_maximal_of_isIntegral : ∀ {R : Type u_1} [inst : CommRing R] {S : Type u_2} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.IsIntegral R S] (P : Ideal R) [P_max : P.IsMaximal],
  RingHom.ker (algebraMap R S) ≤ P → ∃ Q, Q.IsMaximal ∧ Ideal.comap (algebraMap R S) Q = P
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.instSmallSubtypeExistsEq : ∀ {α : Type v} {β : Type w} {f : α → β} [Std.Internal.Small α], Std.Internal.Small { b // ∃ a, f a = b }
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentContentChangeEvent.rangeChange : Lean.Lsp.Range → String → Lean.Lsp.TextDocumentContentChangeEvent
-- Mathlib.Topology.Algebra.Algebra
ContinuousAlgHom.instMonoid : {R : Type u_1} →
  [inst : CommSemiring R] →
    {A : Type u_2} → [inst_1 : Semiring A] → [inst_2 : TopologicalSpace A] → [inst_3 : Algebra R A] → Monoid (A →A[R] A)
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- A sub-cone `F` of a pointed cone `C` is a face of `C` if any two points of `C` with a strictly
positive combination in `F` are also in `F`.  -/
PointedCone.IsFaceOf : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [inst_1 : PartialOrder R] →
        [inst_2 : IsOrderedRing R] →
          [inst_3 : AddCommGroup M] → [inst_4 : Module R M] → PointedCone R M → PointedCone R M → Prop
-- Init.Data.Fin.Lemmas
Fin.eta : ∀ {n : ℕ} (a : Fin n) (h : ↑a < n), ⟨↑a, h⟩ = a
-- Mathlib.NumberTheory.PrimeCounting
Nat.primesBelow_mono : Monotone Nat.primesBelow
-- Mathlib.Order.Interval.Set.Image
StrictAntiOn.image_Ico_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : PartialOrder α] [inst_1 : Preorder β] {a b : α},
  StrictAntiOn f (Set.Icc a b) → f '' Set.Ico a b ⊆ Set.Ioc (f b) (f a)
-- Mathlib.LinearAlgebra.TensorProduct.Basis
TensorProduct.sum_tmul_basis_left_injective : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} {ι : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (ℬ : Module.Basis ι R M),
  Function.Injective ⇑((Finsupp.lsum R) fun i => (TensorProduct.mk R M N) (ℬ i))
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.toArray_filterMap : ∀ {α β γ : Type w} [inst : Std.Iterator α Id β] {it : Std.Iter β} [Std.Iterators.Finite α Id] {f : β → Option γ},
  (Std.Iter.filterMap f it).toArray = Array.filterMap f it.toArray
-- Init.Data.String.Lemmas.FindPos
String.lt_offset_posGT : ∀ {s : String} {p : String.Pos.Raw} {h : p < s.rawEndPos}, p < (s.posGT p h).offset
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Defs
IntermediateField.lift_sup : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (K : IntermediateField F E)
  (L L' : IntermediateField F ↥K),
  IntermediateField.lift (L ⊔ L') = IntermediateField.lift L ⊔ IntermediateField.lift L'
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.foldl_iter : ∀ {γ : Type u} {α β : Type v} {δ : Type u_1} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  [inst_2 : Std.IteratorLoop α Id Id] {s : Std.Slice γ} {init : δ} {f : δ → β → δ},
  Std.Iter.fold f init s.iter = Std.Slice.foldl f init s
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.insertP.loop.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (r : List α) (h_1 : (r : List α) → motive [] r)
  (h_2 : (b : α) → (l r : List α) → motive (b :: l) r),
  (match [], r with
    | [], r => h_1 r
    | b :: l, r => h_2 b l r) =
    h_1 r
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.toArray_filter : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} {f : α → Bool},
  (Std.TreeSet.filter f t).toArray = Array.filter f t.toArray
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.isLocallySurjective_toSheafify : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C)
  (P : CategoryTheory.Functor Cᵒᵖ (Type (max u v))), CategoryTheory.Presheaf.IsLocallySurjective J (J.toSheafify P)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsAddHaarMeasure.mk : ∀ {G : Type u_3} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [inst_2 : MeasurableSpace G]
  {μ : MeasureTheory.Measure G} [toIsFiniteMeasureOnCompacts : MeasureTheory.IsFiniteMeasureOnCompacts μ]
  [toIsAddLeftInvariant : μ.IsAddLeftInvariant] [toIsOpenPosMeasure : μ.IsOpenPosMeasure], μ.IsAddHaarMeasure
-- Lean.Meta.PProdN
/-- Given values of typs `t₁` and `t₂`, produces value of type `t₁ ×' t₂` (or `t₁ ∧ t₂` if the universes allow)  -/
Lean.Meta.mkPProdMk : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr