mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.MeasureTheory.Measure.Regular
/-- If `μ` is inner regular for finite measure sets with respect to compact sets, then its
restriction to any set also is.  -/
MeasureTheory.Measure.InnerRegularCompactLTTop.restrict : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α]
  [h : μ.InnerRegularCompactLTTop] (A : Set α), (μ.restrict A).InnerRegularCompactLTTop
-- Mathlib.Analysis.Normed.Operator.Banach
/-- A surjective continuous linear map between Banach spaces admits a (possibly nonlinear)
controlled right inverse. In general, it is not possible to ensure that such a right inverse
is linear (take for instance the map from `E` to `E/F` where `F` is a closed subspace of `E`
without a closed complement. Then it doesn't have a continuous linear right inverse.)  -/
ContinuousLinearMap.nonlinearRightInverseOfSurjective : {𝕜 : Type u_5} →
  {𝕜' : Type u_6} →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NontriviallyNormedField 𝕜'] →
        {σ : 𝕜 →+* 𝕜'} →
          {E : Type u_7} →
            [inst_2 : NormedAddCommGroup E] →
              [inst_3 : NormedSpace 𝕜 E] →
                {F : Type u_8} →
                  [inst_4 : NormedAddCommGroup F] →
                    [inst_5 : NormedSpace 𝕜' F] →
                      {σ' : 𝕜' →+* 𝕜} →
                        [inst_6 : RingHomInvPair σ σ'] →
                          [RingHomIsometric σ] →
                            [RingHomIsometric σ'] →
                              [CompleteSpace F] →
                                [CompleteSpace E] → (f : E →SL[σ] F) → (↑f).range = ⊤ → f.NonlinearRightInverse
-- Lean.Meta.Match.SimpH
/-- Given an equation of the form `lhs = rhs` where `rhs` is variable in `xs`,
replace it everywhere with `lhs`.
 -/
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.substRHS : Lean.FVarId → Lean.FVarId → Lean.Meta.Match.SimpH.M✝ Unit
-- Mathlib.Algebra.Group.Defs
/-- A variant of `nsmulRec` which is a semigroup homomorphism from `ℕ₊` to `M`.
 -/
nsmulRec' : {M : Type u_2} → [Zero M] → [Add M] → ℕ → M → M
-- Mathlib.Topology.Defs.Sequences
SeqCompactSpace.mk : ∀ {X : Type u_1} [inst : TopologicalSpace X], IsSeqCompact Set.univ → SeqCompactSpace X
-- Mathlib.Analysis.Convex.Gauge
gauge_lt_one_of_mem_of_isOpen : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} [inst_2 : TopologicalSpace E]
  [ContinuousSMul ℝ E], IsOpen s → ∀ {x : E}, x ∈ s → gauge s x < 1
-- Lean.Meta.AppBuilder
/-- Returns instance for `[Monad m]` if there is one  -/
Lean.Meta.isMonad? : Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Data.Sym.Sym2
/-- The `fromRel` set of a symmetric relation `r` is equivalent to summing that set restricted to
fibers of a function `f`, given that `f` agrees on elements related by `r`.  -/
Equiv.sigmaFiberFromRel : {α : Type u_1} →
  {β : Type u_2} →
    {r : α → α → Prop} →
      (sym : Std.Symm r) → {f : α → β} → r ≤ ⇑(Setoid.ker f) → ↑(Sym2.fromRel sym) ≃ (b : β) × ↑(Sym2.fromRel ⋯)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
GradedTensorProduct.instMonoid : {R : Type u_1} →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] → [Module ι (Additive ℤˣ)] → Monoid (GradedTensorProduct R 𝒜 ℬ)
-- Mathlib.Analysis.InnerProductSpace.Projection.FiniteDimensional
/-- If a family of submodules is orthogonal, then the `orthogonalProjection` on a direct sum
is just the coefficient of that direct sum.  -/
OrthogonalFamily.projection_directSum_coeAddHom : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} [inst_3 : DecidableEq ι] {V : ι → Submodule 𝕜 E},
  (OrthogonalFamily 𝕜 (fun i => ↥(V i)) fun i => (V i).subtypeₗᵢ) →
    ∀ (x : DirectSum ι fun i => ↥(V i)) (i : ι) [inst_4 : CompleteSpace ↥(V i)],
      (V i).orthogonalProjectionOnto ((DirectSum.coeAddMonoidHom V) x) = x i
-- Init.Data.List.Find
List.findIdx_le_findIdx : ∀ {α : Type u_1} {l : List α} {p q : α → Bool}, (∀ x ∈ l, p x = true → q x = true) → List.findIdx q l ≤ List.findIdx p l
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.natDegree_lt_natDegree_iff : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p ≠ 0 → (p.natDegree < q.natDegree ↔ p.degree < q.degree)
-- Init.Data.SInt.Bitwise
ISize.shiftRight_or : ∀ {a b c : ISize}, (a ||| b) >>> c = a >>> c ||| b >>> c
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
/-- Auxiliary definition for `IsMeasurableRatCDF.stieltjesFunction`: turn `f : α → ℚ → ℝ` into
a function `α → ℝ → ℝ` by assigning to `f a x` the infimum of `f a q` over `q : ℚ` with `x < q`.  -/
ProbabilityTheory.IsMeasurableRatCDF.stieltjesFunctionAux : {α : Type u_2} → (α → ℚ → ℝ) → α → ℝ → ℝ
-- Mathlib.Data.Set.Function
Set.MapsTo.surjOn_compl : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
  Set.MapsTo f s t → Function.Surjective f → Set.SurjOn f sᶜ tᶜ
-- Mathlib.GroupTheory.DivisibleHull
DivisibleHull.zsmul_mk : ∀ {M : Type u_2} [inst : AddCommGroup M] (a : ℤ) (m : M) (s : ℕ+), a • DivisibleHull.mk m s = DivisibleHull.mk (a • m) s
-- Std.Sync.CancellationToken
/-- Cancels the token with the given reason, notifying all currently waiting consumers.
Once cancelled, the token remains cancelled.
 -/
Std.CancellationToken.cancel : Std.CancellationToken → optParam Std.CancellationReason Std.CancellationReason.cancel → BaseIO Unit
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.parentD.eq_1 : ∀ (arr : Array Batteries.UFNode) (i : ℕ),
  Batteries.UnionFind.parentD arr i = if h : i < arr.size then arr[i].parent else i
-- Mathlib.Geometry.Manifold.VectorBundle.ContMDiffSection
ContMDiff.const_smul_section : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_5} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {n : WithTop ℕ∞} {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → TopologicalSpace (V x)] [inst_10 : FiberBundle F V] [inst_11 : (x : M) → AddCommGroup (V x)]
  [inst_12 : (x : M) → Module 𝕜 (V x)] [VectorBundle 𝕜 F V] {a : 𝕜} {s : (x : M) → V x},
  (ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, s x⟩) →
    ContMDiff I (I.prod (modelWithCornersSelf 𝕜 F)) n fun x => ⟨x, (a • s) x⟩
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.instFunLikeNatSet : {X : Type u_1} → [inst : TopologicalSpace X] → FunLike (CompactExhaustion X) ℕ (Set X)
-- Std.Data.Internal.List.Associative
Std.Internal.List.alterKey_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {a : α} {f : Option (β a) → Option (β a)},
  Std.Internal.List.alterKey a f [] =
    match f none with
    | none => []
    | some b => [⟨a, b⟩]
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
/-- Non-unital star algebra homomorphisms commute with the non-unital continuous functional
calculus.  -/
NonUnitalStarAlgHomClass.map_cfcₙ : ∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} {A : Type u_4} {B : Type u_5} {p : A → Prop} {q : B → Prop}
  [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R] [inst_3 : MetricSpace R]
  [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : CommRing S] [inst_7 : Algebra R S]
  [inst_8 : NonUnitalRing A] [inst_9 : StarRing A] [inst_10 : TopologicalSpace A] [inst_11 : Module R A]
  [inst_12 : IsScalarTower R A A] [inst_13 : SMulCommClass R A A] [inst_14 : NonUnitalRing B] [inst_15 : StarRing B]
  [inst_16 : TopologicalSpace B] [inst_17 : Module R B] [inst_18 : IsScalarTower R B B] [inst_19 : SMulCommClass R B B]
  [inst_20 : Module S A] [inst_21 : Module S B] [IsScalarTower R S A] [IsScalarTower R S B]
  [inst_24 : NonUnitalContinuousFunctionalCalculus R A p] [inst_25 : NonUnitalContinuousFunctionalCalculus R B q]
  [ContinuousMapZero.UniqueHom R B] [inst_27 : FunLike F A B] [NonUnitalAlgHomClass F S A B] [StarHomClass F A B]
  (φ : F) (f : R → R) (a : A),
  autoParam (ContinuousOn f (quasispectrum R a)) NonUnitalStarAlgHomClass.map_cfcₙ._auto_1 →
    autoParam (f 0 = 0) NonUnitalStarAlgHomClass.map_cfcₙ._auto_3 →
      autoParam (Continuous ⇑φ) NonUnitalStarAlgHomClass.map_cfcₙ._auto_5 →
        autoParam (p a) NonUnitalStarAlgHomClass.map_cfcₙ._auto_7 →
          autoParam (q (φ a)) NonUnitalStarAlgHomClass.map_cfcₙ._auto_9 → φ (cfcₙ f a) = cfcₙ f (φ a)
-- Mathlib.RingTheory.RingHom.Locally
/-- If `P` preserves localizations, then `Locally P` is stable under composition if `P` is.  -/
RingHom.locally_stableUnderComposition : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.RespectsIso fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.LocalizationPreserves fun {R S} [CommRing R] [CommRing S] => P) →
      (RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] => P) →
        RingHom.StableUnderComposition fun {R S} [CommRing R] [CommRing S] =>
          RingHom.Locally fun {R S} [CommRing R] [CommRing S] => P
-- Mathlib.Data.Nat.Digits.Lemmas
List.ne_empty_of_mem_consFixedLengthDigits : ∀ {b : ℕ} (hb : 1 < b) {l d : ℕ} {L : List ℕ}, L ∈ List.consFixedLengthDigits hb l d → L ≠ []
-- Mathlib.Topology.Order
sierpinskiSpace : TopologicalSpace Prop
-- Mathlib.Analysis.Complex.Trigonometric
Complex.cos_neg : ∀ (x : ℂ), Complex.cos (-x) = Complex.cos x
-- Mathlib.NumberTheory.ModularForms.Bounds
/-- If `f, f'` are modular forms, then `petersson k f f'` is bounded by a constant multiple of
`max τ.im (1 / τ.im) ^ k`.  -/
ModularFormClass.exists_petersson_le : ∀ {k : ℤ},
  0 ≤ k →
    ∀ (Γ : Subgroup (GL (Fin 2) ℝ)) [Γ.IsArithmetic] {F : Type u_2} {F' : Type u_3} (f : F) (f' : F')
      [inst : FunLike F UpperHalfPlane ℂ] [inst_1 : FunLike F' UpperHalfPlane ℂ] [ModularFormClass F Γ k]
      [ModularFormClass F' Γ k],
      ∃ C, ∀ (τ : UpperHalfPlane), ‖UpperHalfPlane.petersson k (⇑f) (⇑f') τ‖ ≤ C * max τ.im (1 / τ.im) ^ k
-- Mathlib.Data.Set.Basic
SetCoe.forall' : ∀ {α : Type u} {s : Set α} {p : (x : α) → x ∈ s → Prop}, (∀ (x : α) (h : x ∈ s), p x h) ↔ ∀ (x : ↑s), p ↑x ⋯
-- Mathlib.Topology.MetricSpace.HolderNorm
eHolderNorm_nsmul : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : NormedAddCommGroup Y] {r : NNReal} {f : X → Y}
  [NormedSpace ℝ Y] (n : ℕ), eHolderNorm r (n • f) = n • eHolderNorm r f
-- Mathlib.Probability.Kernel.CondDistrib
MeasureTheory.Integrable.norm_integral_condDistrib : ∀ {α : Type u_1} {β : Type u_2} {Ω : Type u_3} {F : Type u_4} [inst : MeasurableSpace Ω] [inst_1 : StandardBorelSpace Ω]
  [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F] {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : MeasureTheory.IsFiniteMeasure μ] {X : α → β} {Y : α → Ω} {mβ : MeasurableSpace β} {f : β × Ω → F}
  [inst_5 : NormedSpace ℝ F],
  AEMeasurable X μ →
    AEMeasurable Y μ →
      MeasureTheory.Integrable f (MeasureTheory.Measure.map (fun a => (X a, Y a)) μ) →
        MeasureTheory.Integrable (fun a => ‖∫ (y : Ω), f (X a, y) ∂(ProbabilityTheory.condDistrib Y X μ) (X a)‖) μ
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
/-- **Newton's identities** give a recurrence relation for the kth elementary symmetric polynomial
in terms of lower degree elementary symmetric polynomials and power sums.  -/
MvPolynomial.mul_esymm_eq_sum : ∀ (σ : Type u_1) [inst : Fintype σ] (R : Type u_2) [inst_1 : CommRing R] (k : ℕ),
  ↑k * MvPolynomial.esymm σ R k =
    (-1) ^ (k + 1) *
      ∑ a ∈ Finset.HasAntidiagonal.antidiagonal k with a.1 < k,
        (-1) ^ a.1 * MvPolynomial.esymm σ R a.1 * MvPolynomial.psum σ R a.2
-- Mathlib.Combinatorics.Quiver.Path.Weight
Quiver.Path.weight.eq_def : ∀ {V : Type u_1} [inst : Quiver V] {R : Type u_2} [inst_1 : Monoid R] (w : {i j : V} → (i ⟶ j) → R) (x x_1 : V)
  (x_2 : Quiver.Path x x_1),
  Quiver.Path.weight w x_2 =
    match x, x_1, x_2 with
    | a, .(a), Quiver.Path.nil => 1
    | a, x, p.cons e => Quiver.Path.weight (fun {i j} => w) p * w e
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Cnstr.match.inj : ∀ {gen? : Option Lean.Meta.Grind.GenPatternInfo} {pat e : Lean.Expr} {gen?_1 : Option Lean.Meta.Grind.GenPatternInfo}
  {pat_1 e_1 : Lean.Expr},
  Lean.Meta.Grind.EMatch.Cnstr.match gen? pat e = Lean.Meta.Grind.EMatch.Cnstr.match gen?_1 pat_1 e_1 →
    gen? = gen?_1 ∧ pat = pat_1 ∧ e = e_1
-- Mathlib.Algebra.Regular.Opposite
isLeftRegular_op : ∀ {R : Type u_1} [inst : Mul R] {a : R}, IsLeftRegular (MulOpposite.op a) ↔ IsRightRegular a
-- Mathlib.LinearAlgebra.AffineSpace.Independent
AffineIndependent.eq_of_sum_eq_sum : ∀ {k : Type u_1} {V : Type u_2} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V] {ι : Type u_4}
  {s : Finset ι} {w₁ w₂ : ι → k} {p : ι → V},
  AffineIndependent k p →
    ∑ i ∈ s, w₁ i = ∑ i ∈ s, w₂ i → ∑ i ∈ s, w₁ i • p i = ∑ i ∈ s, w₂ i • p i → ∀ i ∈ s, w₁ i = w₂ i
-- Mathlib.Topology.Order.IsLUB
IsLUB.exists_seq_monotone_tendsto : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {t : Set α} {x : α}
  [(nhds x).IsCountablyGenerated],
  IsLUB t x →
    t.Nonempty → ∃ u, Monotone u ∧ (∀ (n : ℕ), u n ≤ x) ∧ Filter.Tendsto u Filter.atTop (nhds x) ∧ ∀ (n : ℕ), u n ∈ t
-- Init.Data.Fin.Lemmas
Fin.pred_mk_succ : ∀ {n : ℕ} (i : ℕ) (h : i < n + 1), ⟨i + 1, ⋯⟩.pred ⋯ = ⟨i, h⟩
-- Init.Data.Array.Attach
Array.attachWith.eq_1 : ∀ {α : Type u_1} (xs : Array α) (P : α → Prop) (H : ∀ x ∈ xs, P x),
  xs.attachWith P H = { toList := xs.toList.attachWith P ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.Rel.in₁₀ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)} ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄,
  (a, b, c) ∈ t → SimpleGraph.TripartiteFromTriangles.Rel t (Sum3.in₁ b) (Sum3.in₀ a)
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
Orthonormal.ne_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E}, Orthonormal 𝕜 v → ∀ (i : ι), v i ≠ 0
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
contMDiff_fst : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {G : Type u_9} [inst_8 : TopologicalSpace G] {J : ModelWithCorners 𝕜 F G} {N : Type u_10}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞}, ContMDiff (I.prod J) I n Prod.fst
-- Mathlib.Data.Finset.Image
Finset.range_sdiff_zero : ∀ {n : ℕ}, Finset.range (n + 1) \ {0} = Finset.image Nat.succ (Finset.range n)
-- Mathlib.Algebra.Divisibility.Units
IsRelPrime.dvd_of_dvd_mul_left_of_isPrimal : ∀ {α : Type u_1} [inst : CommMonoid α] {x y z : α}, IsRelPrime x y → x ∣ y * z → IsPrimal x → x ∣ z
-- Mathlib.Data.ENNReal.Inv
ENNReal.exists_mem_Ioc_zpow : ∀ {x y : ENNReal}, x ≠ 0 → x ≠ ⊤ → 1 < y → y ≠ ⊤ → ∃ n, x ∈ Set.Ioc (y ^ n) (y ^ (n + 1))
-- Mathlib.AlgebraicGeometry.Sites.Proetale
AlgebraicGeometry.Scheme.instHasIsosProetalePrecoverage : AlgebraicGeometry.Scheme.proetalePrecoverage.HasIsos
-- Mathlib.Analysis.Distribution.SchwartzSpace.Deriv
SchwartzMap.lineDerivOp_apply : ∀ {E : Type u_5} {F : Type u_8} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  [inst_3 : NormedSpace ℝ E] (m : E) (f : SchwartzMap E F) (x : E), (LineDeriv.lineDerivOp m f) x = lineDeriv ℝ (⇑f) x m
-- Mathlib.Analysis.Calculus.VectorField
/-- Variant of `lieBracketWithin_congr_set` where one requires the sets to coincide only in
the complement of a point.  -/
VectorField.lieBracketWithin_congr_set' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {V W : E → E} {s t : Set E} {x : E} (y : E),
  s =ᶠ[nhdsWithin x {y}ᶜ] t → VectorField.lieBracketWithin 𝕜 V W s x = VectorField.lieBracketWithin 𝕜 V W t x
-- Mathlib.Order.RelClasses
/-- **Alias** of `LT.lt.trans_subset`.

---

Set notation form of `LT.lt.trans_le` -/
HasSSubset.SSubset.trans_subset : ∀ {α : Type u_1} [UsesSetNotationForOrder α] [inst : Preorder α] {a b c : α}, a ⊂ b → b ⊆ c → a ⊂ c
-- Init.Control.Lawful.Instances
OptionT.map_failure : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] [LawfulMonad m] {α β : Type u_1} (f : α → β), f <$> failure = failure
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.isConnected_of_isConnected_op : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsConnected Jᵒᵖ],
  CategoryTheory.IsConnected J
-- Mathlib.Algebra.Polynomial.Div
Polynomial.eval₂_modByMonic_eq_self_of_root : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] {f : R →+* S} {p q : Polynomial R} {x : S},
  Polynomial.eval₂ f x q = 0 → Polynomial.eval₂ f x (p %ₘ q) = Polynomial.eval₂ f x p
-- Mathlib.Algebra.Group.Basic
/-- **Alias** of the reverse direction of `div_eq_one`. -/
div_eq_one_of_eq : ∀ {G : Type u_3} [inst : Group G] {a b : G}, a = b → a / b = 1
-- Lean.DocString.Markdown
/-- Render an `α` to its Markdown lines. The lines should not contain literal `\n`
characters; line breaks are encoded by the array structure.
 -/
Lean.Doc.ToMarkdown.toMarkdown : {α : Type u} → [self : Lean.Doc.ToMarkdown α] → α → Lean.Doc.MarkdownM (Array String)
-- Mathlib.Data.Finsupp.Defs
Finsupp.onFinset.congr_simp : ∀ {α : Type u_1} {M : Type u_4} [inst : Zero M] (s s_1 : Finset α) (e_s : s = s_1) (f f_1 : α → M) (e_f : f = f_1)
  (hf : ∀ (a : α), f a ≠ 0 → a ∈ s), Finsupp.onFinset s f hf = Finsupp.onFinset s_1 f_1 ⋯
-- Mathlib.Analysis.Calculus.Deriv.MeanValue
/-- Lagrange's Mean Value Theorem, `HasDerivAt` version  -/
exists_hasDerivAt_eq_slope : ∀ (f f' : ℝ → ℝ) {a b : ℝ},
  a < b →
    ContinuousOn f (Set.Icc a b) →
      (∀ x ∈ Set.Ioo a b, HasDerivAt f (f' x) x) → ∃ c ∈ Set.Ioo a b, f' c = (f b - f a) / (b - a)
-- Mathlib.Algebra.TrivSqZeroExt.Basic
TrivSqZeroExt.mulAction : {S : Type u_2} →
  {R : Type u} → {M : Type v} → [inst : Monoid S] → [MulAction S R] → [MulAction S M] → MulAction S (TrivSqZeroExt R M)
-- Mathlib.Topology.ContinuousMap.CompactlySupported
CompactlySupportedContinuousMap.instLatticeOfTopologicalLattice : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : Lattice β] →
          [TopologicalLattice β] → [inst_4 : Zero β] → Lattice (CompactlySupportedContinuousMap α β)
-- Mathlib.Algebra.Group.Center
Set.center_eq_univ : ∀ (M : Type u_1) [inst : CommSemigroup M], Set.center M = Set.univ
-- Lean.Meta.Tactic.Grind.EMatch
Lean.Meta.Grind.EMatch.Cnstr.match.injEq : ∀ (gen? : Option Lean.Meta.Grind.GenPatternInfo) (pat e : Lean.Expr) (gen?_1 : Option Lean.Meta.Grind.GenPatternInfo)
  (pat_1 e_1 : Lean.Expr),
  (Lean.Meta.Grind.EMatch.Cnstr.match gen? pat e = Lean.Meta.Grind.EMatch.Cnstr.match gen?_1 pat_1 e_1) =
    (gen? = gen?_1 ∧ pat = pat_1 ∧ e = e_1)
-- Mathlib.GroupTheory.FreeGroup.Reduce
FreeAddGroup.reduce_negRev : ∀ {α : Type u_1} [inst : DecidableEq α] {w : List (α × Bool)},
  FreeAddGroup.reduce (FreeAddGroup.negRev w) = FreeAddGroup.negRev (FreeAddGroup.reduce w)
-- Mathlib.Order.WithBot
WithTop.instOrderBot : {α : Type u_1} → [inst : LE α] → [OrderBot α] → OrderBot (WithTop α)
-- Mathlib.Analysis.BoxIntegral.Partition.Tagged
BoxIntegral.TaggedPrepartition.disjUnion_tag_of_mem_left : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π₁ π₂ : BoxIntegral.TaggedPrepartition I}
  (h : Disjoint π₁.iUnion π₂.iUnion), J ∈ π₁ → (π₁.disjUnion π₂ h).tag J = π₁.tag J
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Sheafification
PresheafOfModules.instReflectsIsomorphismsSheafOfModulesSheafAddCommGrpCatToSheaf : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat}, (SheafOfModules.toSheaf R).ReflectsIsomorphisms
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NFBelow.mono : ∀ {o : ONote} {b₁ b₂ : Ordinal.{0}}, b₁ ≤ b₂ → o.NFBelow b₁ → o.NFBelow b₂
-- Lean.Data.Lsp.BasicAux
/-- We adopt the convention that zero-based UTF-16 positions as sent by LSP clients
are represented by `Lsp.Position` while internally we mostly use `String.Pos` UTF-8
offsets. For diagnostics, one-based `Lean.Position`s are used internally.
`character` is accepted liberally: actual character := min(line length, character)  -/
Lean.Lsp.Position : Type
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Cech
CategoryTheory.Limits.FormalCoproduct.cechFunctor_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasFiniteProducts C]
  (U : CategoryTheory.Limits.FormalCoproduct C), CategoryTheory.Limits.FormalCoproduct.cechFunctor.obj U = U.cech
-- Mathlib.Data.Finite.Defs
/-- See also `finite_or_infinite`, `fintypeOrInfinite`.  -/
Set.finite_or_infinite : ∀ {α : Type u} (s : Set α), s.Finite ∨ s.Infinite
-- Mathlib.Tactic.ClearExcept
/-- Returns the free variable IDs that can be cleared, excluding those in the preserve list,
class instances, and auxiliary declarations (e.g. recursive hypotheses).  -/
Lean.Elab.Tactic.getVarsToClear : Array Lean.FVarId → Lean.MetaM (Array Lean.FVarId)
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.zero_ne_of : ∀ {α : Type u} (x : α), 0 ≠ FreeCommRing.of x
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.homOfConnectedComponents_apply : ∀ {V : Type u} {V' : Type v} (G : SimpleGraph V) {H : SimpleGraph V'}
  (C : (c : G.ConnectedComponent) → c.toSimpleGraph →g H) (x : V),
  (G.homOfConnectedComponents C) x = (C (G.connectedComponentMk x)) ⟨x, ⋯⟩
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.nonneg_of_mem_sphere : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {ε : ℝ}, y ∈ Metric.sphere x ε → 0 ≤ ε
-- Mathlib.Topology.UniformSpace.Pi
Pi.uniformContinuous_precomp' : ∀ {ι : Type u_1} {ι' : Type u_2} (α : ι → Type u) [U : (i : ι) → UniformSpace (α i)] (φ : ι' → ι),
  UniformContinuous fun f j => f (φ j)
-- Mathlib.Analysis.BoxIntegral.UnitPartition
Module.Basis.isUnitSMul.congr_simp : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (v v_1 : Module.Basis ι R M),
  v = v_1 → ∀ {w w_1 : ι → R} (e_w : w = w_1) (hw : ∀ (i : ι), IsUnit (w i)), v.isUnitSMul hw = v_1.isUnitSMul ⋯
-- Mathlib.Algebra.Homology.ShortComplex.Preadditive
CategoryTheory.ShortComplex.leftHomologyMap_neg : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂) [inst_2 : S₁.HasLeftHomology] [inst_3 : S₂.HasLeftHomology],
  CategoryTheory.ShortComplex.leftHomologyMap (-φ) = -CategoryTheory.ShortComplex.leftHomologyMap φ
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
_private.Init.Data.String.Lemmas.Pattern.TakeDrop.Basic.0.String.Slice.Pos.skipWhile.eq_def : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.ForwardPattern pat],
  pos.skipWhile pat =
    match pos.skip? pat with
    | some nextCurr => if pos < nextCurr then nextCurr.skipWhile pat else pos
    | none => pos
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
/-- Composing the preadditive yoneda embedding with the forgetful functor yields the regular
Yoneda embedding.
 -/
CategoryTheory.whiskering_preadditiveCoyoneda : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C],
  CategoryTheory.preadditiveCoyoneda.comp
      ((CategoryTheory.Functor.whiskeringRight C AddCommGrpCat (Type v)).obj (CategoryTheory.forget AddCommGrpCat)) =
    CategoryTheory.coyoneda