mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
closedBall_sub_closedBall : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] [NormedSpace ℝ E] {δ ε : ℝ} [ProperSpace E],
  0 ≤ ε → 0 ≤ δ → ∀ (a b : E), Metric.closedBall a ε - Metric.closedBall b δ = Metric.closedBall (a - b) (ε + δ)
-- Mathlib.RingTheory.Coalgebra.Equiv
CoalgEquiv.ext : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid A]
  [inst_2 : AddCommMonoid B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : CoalgebraStruct R A]
  [inst_6 : CoalgebraStruct R B] {e e' : A ≃ₗc[R] B}, (∀ (x : A), e x = e' x) → e = e'
-- Mathlib.CategoryTheory.Monoidal.Free.Basic
CategoryTheory.FreeMonoidalCategory.Hom.tensor.inj : ∀ {C : Type u} {W X Y Z : CategoryTheory.FreeMonoidalCategory C} {f : W.Hom Y} {g : X.Hom Z} {f_1 : W.Hom Y}
  {g_1 : X.Hom Z}, f.tensor g = f_1.tensor g_1 → f = f_1 ∧ g = g_1
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- A sequence of functions `Fₙ` converges uniformly on a filter `p'` to a limiting function `f`
with respect to the filter `p` if, for any entourage of the diagonal `u`, one has
`p ×ˢ p'`-eventually `(f x, Fₙ x) ∈ u`.  -/
TendstoUniformlyOnFilter : {α : Type u_1} → {β : Type u_2} → {ι : Type u_4} → [UniformSpace β] → (ι → α → β) → (α → β) → Filter ι → Filter α → Prop
-- Init.Data.Int.DivMod.Lemmas
Int.natAbs_ediv_of_dvd : ∀ {a b : ℤ}, b ∣ a → (a / b).natAbs = a.natAbs / b.natAbs
-- Mathlib.Combinatorics.SimpleGraph.Finsubgraph
/-- The finite subgraph of G generated by a single edge.  -/
SimpleGraph.finsubgraphOfAdj : {V : Type u} → {G : SimpleGraph V} → {u v : V} → G.Adj u v → G.Finsubgraph
-- Mathlib.LinearAlgebra.TensorProduct.Vanishing
/-- **Equational criterion for vanishing**
[A. Altman and S. Kleiman, *A term of commutative algebra* (Lemma 8.16)][altman2021term],
forward direction, generalization.

Assume that the submodule $M' \subseteq M$ generated by the $m_i$
satisfies the property that the map $M' \otimes N \to M \otimes N$ is injective. If the expression
$\sum_i m_i \otimes n_i$ vanishes, then it vanishes trivially.  -/
TensorProduct.vanishesTrivially_of_sum_tmul_eq_zero_of_rTensor_injective : ∀ (R : Type u_1) [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] {ι : Type u_4} [inst_5 : Fintype ι] {m : ι → M} {n : ι → N},
  Function.Injective ⇑(LinearMap.rTensor N (Submodule.span R (Set.range m)).subtype) →
    ∑ i, m i ⊗ₜ[R] n i = 0 → TensorProduct.VanishesTrivially R m n
-- Mathlib.Order.Filter.ENNReal
Real.limsInf_of_not_isCobounded : ∀ {f : Filter ℝ}, ¬Filter.IsCobounded (fun x1 x2 => x1 ≥ x2) f → f.limsInf = 0
-- Mathlib.Algebra.Star.Basic
StarAddMonoid.toStarModuleNat : ∀ {α : Type u_1} [inst : AddMonoid α] [inst_1 : StarAddMonoid α], StarModule ℕ α
-- Mathlib.Algebra.MvPolynomial.Basic
/-- See note [partially-applied ext lemmas].

We set the priority higher than that of `MvPolynomial.algHom_ext'`.  -/
MvPolynomial.algHom_ext : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : Algebra R A]
  {f g : MvPolynomial σ R →ₐ[R] A}, (∀ (i : σ), f (MvPolynomial.X i) = g (MvPolynomial.X i)) → f = g
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → γ} {k k' : α} {fallback : γ},
  m.WF → m.getKey? k = some k' → (Std.HashMap.Raw.map f m).getD k fallback = (Option.map (f k') m[k]?).getD fallback
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.preimage_image_mk_eq_iUnion_image : ∀ {α : Type u_1} [inst : AddGroup α] (N : AddSubgroup α) (s : Set α),
  QuotientAddGroup.mk ⁻¹' QuotientAddGroup.mk '' s = ⋃ x, (fun x_1 => x_1 + ↑x) '' s
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.of.eq_1 : ∀ {α : Type u_1} (x : α), FreeMonoid.of x = FreeMonoid.ofList [x]
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.of_subsingleton_cod : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {f : α → β} [inst : TopologicalSpace β] [Subsingleton β],
  MeasureTheory.StronglyMeasurable f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_union!_of_contains_eq_false_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (contains_eq_false : Std.DTreeMap.Internal.Impl.contains k m₂ = false)
  {h' : Std.DTreeMap.Internal.Impl.contains k (m₁.union! m₂) = true},
  Std.DTreeMap.Internal.Impl.Const.get (m₁.union! m₂) k h' = Std.DTreeMap.Internal.Impl.Const.get m₁ k ⋯
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_le_cardinalMk : ∀ (α : Type u) [inst : Preorder α], Order.cof α ≤ Cardinal.mk α
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.inner_rightAngleRotation_self : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x : E), inner ℝ (o.rightAngleRotation x) x = 0
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
AddMonoidAlgebra.mapDomain_injective : ∀ {R : Type u_3} {M : Type u_6} {N : Type u_7} [inst : Semiring R] {f : M → N},
  Function.Injective f → Function.Injective (AddMonoidAlgebra.mapDomain f)
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.ObjectProperty.IsSeparating.epi_coproductFrom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.ObjectProperty C},
  P.IsSeparating →
    ∀ (X : C) [inst_1 : CategoryTheory.Limits.HasCoproduct (P.coproductFromFamily X)],
      CategoryTheory.Epi (P.coproductFrom X)
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
Summable.nat_tsum_vanishing : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] {f : ℕ → G},
  Summable f → ∀ ⦃e : Set G⦄, e ∈ nhds 0 → ∃ N, ∀ t ⊆ {n | N ≤ n}, ∑' (n : ↑t), f ↑n ∈ e
-- Mathlib.Combinatorics.Matroid.Minor.Restrict
Matroid.IsBasis.isBase_of_isBase_subset : ∀ {α : Type u_1} {M : Matroid α} {I X B : Set α}, M.IsBasis I X → M.IsBase B → B ⊆ X → M.IsBase I
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.prodAddEquiv_apply : ∀ {G : Type u} [inst : AddGroup G] {H : Type v} [inst_1 : AddGroup H] (A : AddSubgroup G) (B : AddSubgroup H)
  [inst_2 : A.Normal] [inst_3 : B.Normal] (q : (G × H) ⧸ A.prod B),
  (QuotientAddGroup.prodAddEquiv A B) q = Quotient.liftOn' q (fun x => (↑x.1, ↑x.2)) ⋯
-- Mathlib.Algebra.Ring.Divisibility.Basic
/-- If an element `a` divides another element `c` in a ring, `a` divides the difference of another
element `b` with `c` iff `a` divides `b`.  -/
dvd_sub_left : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ c → (a ∣ b - c ↔ a ∣ b)
-- Init.NotationExtra
_private.Init.NotationExtra.0.Lean.expandBracketedBindersAux.loop : Lean.Syntax → (binders : Array Lean.Syntax) → (i : ℕ) → i ≤ binders.size → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getD_insertMany!_list_of_contains_eq_false : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : BEq α] [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List (α × β)} {k : α} {fallback : β},
      (List.map Prod.fst l).contains k = false →
        Std.DTreeMap.Internal.Impl.Const.getD (↑(Std.DTreeMap.Internal.Impl.Const.insertMany! t l)) k fallback =
          Std.DTreeMap.Internal.Impl.Const.getD t k fallback
-- Mathlib.GroupTheory.GroupAction.SubMulAction.Combination
Set.powersetCard.addActionHom_of_embedding_surjective : ∀ (G : Type u_1) [inst : AddGroup G] (α : Type u_2) [inst_1 : AddAction G α] {n : ℕ} [inst_2 : DecidableEq α],
  Function.Surjective ⇑(Set.powersetCard.addActionHom_of_embedding G α n)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapLeftIso_counitIso_hom_app_right : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (R : CategoryTheory.Functor B T)
  {L₁ L₂ : CategoryTheory.Functor A T} (i : L₁ ≅ L₂) (X : CategoryTheory.Comma L₂ R),
  ((CategoryTheory.Comma.mapLeftIso R i).counitIso.hom.app X).right = CategoryTheory.CategoryStruct.id X.right
-- Mathlib.AlgebraicGeometry.StructureSheaf
AlgebraicGeometry.StructureSheaf.const_mul_cancel' : ∀ {R : Type u} [inst : CommRing R] (f g₁ g₂ : R) (U : TopologicalSpace.Opens ↑(AlgebraicGeometry.PrimeSpectrum.Top R))
  (hu₁ : U ≤ PrimeSpectrum.basicOpen g₁) (hu₂ : U ≤ PrimeSpectrum.basicOpen g₂),
  AlgebraicGeometry.StructureSheaf.const g₁ g₂ U hu₂ * AlgebraicGeometry.StructureSheaf.const f g₁ U hu₁ =
    AlgebraicGeometry.StructureSheaf.const f g₂ U hu₂
-- Mathlib.MeasureTheory.Measure.AbsolutelyContinuous
MeasureTheory.Measure.AbsolutelyContinuous.add : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ₁ μ₂ ν ν' : MeasureTheory.Measure α},
  μ₁.AbsolutelyContinuous ν → μ₂.AbsolutelyContinuous ν' → (μ₁ + μ₂).AbsolutelyContinuous (ν + ν')
-- Mathlib.Data.EReal.Inv
EReal.div_mul_cancel : ∀ {a b : EReal}, b ≠ ⊥ → b ≠ ⊤ → b ≠ 0 → a / b * b = a
-- Mathlib.RingTheory.EssentialFiniteness
Algebra.EssFiniteType.iff_of_algEquiv : ∀ {R : Type u_1} {S : Type u_2} {T : Type u_3} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] (f : S ≃ₐ[R] T), Algebra.EssFiniteType R S ↔ Algebra.EssFiniteType R T
-- Lean.ErrorExplanation
Lean.ErrorExplanation.instFromJsonMetadata : Lean.FromJson Lean.ErrorExplanation.Metadata
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.toArray_toList : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [inst_4 : Std.Rxc.IsAlwaysFinite α], r.toList.toArray = r.toArray
-- Mathlib.Geometry.Manifold.PartitionOfUnity
/-- The center point of each bump in the smooth covering.  -/
SmoothBumpCovering.c : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] →
                    [inst_5 : FiniteDimensional ℝ E] →
                      {s : optParam (Set M) Set.univ} → SmoothBumpCovering ι I M s → ι → M
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomMulAct.smul_Lp_neg : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : SMul M α] [inst_3 : MeasureTheory.SMulInvariantMeasure M α μ]
  [inst_4 : MeasurableConstSMul M α] (c : Mᵈᵐᵃ) (f : ↥(MeasureTheory.Lp E p μ)), c • -f = -(c • f)
-- Mathlib.Order.Hom.Basic
OrderHom.snd_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (self : α × β), OrderHom.snd self = self.2
-- Mathlib.Geometry.Manifold.Algebra.Monoid
instZeroContMDiffAddMonoidMorphism.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_2} [inst_1 : TopologicalSpace H]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {G : Type u_4}
  [inst_4 : AddMonoid G] [inst_5 : TopologicalSpace G] [inst_6 : ChartedSpace H G] {H' : Type u_5}
  [inst_7 : TopologicalSpace H'] {E' : Type u_6} [inst_8 : NormedAddCommGroup E'] [inst_9 : NormedSpace 𝕜 E']
  {I' : ModelWithCorners 𝕜 E' H'} {G' : Type u_7} [inst_10 : AddMonoid G'] [inst_11 : TopologicalSpace G']
  [inst_12 : ChartedSpace H' G'],
  instZeroContMDiffAddMonoidMorphism =
    {
      zero :=
        let __MonoidHom := 0;
        { toAddMonoidHom := __MonoidHom, contMDiff_toFun := ⋯ } }
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.instDescScheme : ∀ {X : AlgebraicGeometry.Scheme} {ι : Type v} [inst : Small.{u, v} ι] {Y : ι → AlgebraicGeometry.Scheme}
  {f : (i : ι) → Y i ⟶ X} [∀ (i : ι), AlgebraicGeometry.Flat (f i)],
  AlgebraicGeometry.Flat (CategoryTheory.Limits.Sigma.desc f)
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
SheafOfModules.mk.injEq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : CategoryTheory.GrothendieckTopology C}
  {R : CategoryTheory.Sheaf J RingCat} (val : PresheafOfModules R.obj)
  (isSheaf : CategoryTheory.Presheaf.IsSheaf J val.presheaf) (val_1 : PresheafOfModules R.obj)
  (isSheaf_1 : CategoryTheory.Presheaf.IsSheaf J val_1.presheaf),
  ({ val := val, isSheaf := isSheaf } = { val := val_1, isSheaf := isSheaf_1 }) = (val = val_1)
-- Mathlib.RingTheory.Congruence.Hom
RingCon.quotientQuotientEquivQuotientₐ_symm_mk : ∀ {M : Type u_1} (R : Type u_4) [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M] {c d : RingCon M}
  (h : c ≤ d) (x : M), (RingCon.quotientQuotientEquivQuotientₐ R h).symm ⟦x⟧ = ⟦⟦x⟧⟧
-- Mathlib.Data.Matrix.Diagonal
Matrix.diagonal_ofNat' : ∀ {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : Zero α] [inst_2 : NatCast α] (m : ℕ)
  [inst_3 : m.AtLeastTwo], Matrix.diagonal (OfNat.ofNat m) = OfNat.ofNat m
-- Mathlib.Data.PFunctor.Univariate.M
/-- `IsPath p x` tells us if `p` is a valid path through `x`  -/
PFunctor.M.IsPath : {F : PFunctor.{uA, uB}} → PFunctor.Approx.Path F → F.M → Prop
-- Init.Data.Option.Basic
Option.instReflBEq : ∀ (α : Type u_1) [inst : BEq α] [ReflBEq α], ReflBEq (Option α)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.get?_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → (m₁ \ m₂).get? k = none
-- Init.Data.Array.BasicAux
/-- Applies the monadic action `f` to every element in the array, left-to-right, and returns the array
of results. Furthermore, the resulting array's type guarantees that it contains the same number of
elements as the input array.
 -/
Array.mapM' : {m : Type u_1 → Type u_2} →
  {α : Type u_3} → {β : Type u_1} → [Monad m] → (α → m β) → (as : Array α) → m { bs // bs.size = as.size }
-- Mathlib.MeasureTheory.Measure.Typeclasses.Probability
/-- Note that this is not quite as useful as it looks because the measure takes values in `ℝ≥0∞`.
Thus the subtraction appearing is the truncated subtraction of `ℝ≥0∞`, rather than the
better-behaved subtraction of `ℝ`.  -/
MeasureTheory.prob_compl_eq_one_sub₀ : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α}
  [MeasureTheory.IsProbabilityMeasure μ], MeasureTheory.NullMeasurableSet s μ → μ sᶜ = 1 - μ s
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.neg_nonneg_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommGroup M] [Lean.Grind.OrderedAdd M]
  {a : M}, 0 ≤ -a ↔ a ≤ 0
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.mem_bot : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {x : A},
  x ∈ ⊥ ↔ x ∈ Set.range ⇑(algebraMap R A)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_lt_zpow_of_neg₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀} [ZeroLEOneClass G₀]
  {n : ℤ}, 0 < a → a < 1 → n < 0 → 1 < a ^ n
-- Lean.DocString.Types
/-- A logical division of a document.
 -/
Lean.Doc.Part : Type u → Type v → Type w → Type (max u v w)
-- Mathlib.Analysis.ODE.PicardLindelof
/-- The map `next` has a fixed point in the space of curves. This will be used to construct a
solution `α : ℝ → E` to the ODE.  -/
ODE.FunSpace.exists_isFixedPt_next : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E → E} {tmin tmax : ℝ}
  {t₀ : ↑(Set.Icc tmin tmax)} {x₀ x : E} {a r L K : NNReal} [CompleteSpace E] (hf : IsPicardLindelof f t₀ x₀ a r L K)
  (hx : x ∈ Metric.closedBall x₀ ↑r), ∃ α, Function.IsFixedPt (ODE.FunSpace.next hf hx) α
-- Mathlib.Analysis.Distribution.TestFunction
TestFunctionClass.mk : {B : Type u_6} →
  {E : outParam (Type u_7)} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {Ω : outParam (TopologicalSpace.Opens E)} →
          {F : outParam (Type u_8)} →
            [inst_2 : NormedAddCommGroup F] →
              [inst_3 : NormedSpace ℝ F] →
                {n : outParam ℕ∞} →
                  [toDFunLike : DFunLike B E fun x => F] →
                    (∀ (f : B), ContDiff ℝ ↑n ⇑f) →
                      (∀ (f : B), HasCompactSupport ⇑f) → (∀ (f : B), tsupport ⇑f ⊆ ↑Ω) → TestFunctionClass B Ω F n
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgHom.range_comp : ∀ {R : Type u} {A : Type v} {B : Type w} {C : Type w'} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B]
  [inst_5 : NonUnitalNonAssocSemiring C] [inst_6 : Module R C] (f : A →ₙₐ[R] B) (g : B →ₙₐ[R] C),
  NonUnitalAlgHom.range (g.comp f) = NonUnitalSubalgebra.map g (NonUnitalAlgHom.range f)
-- Mathlib.RingTheory.MvPolynomial.Ideal
MonomialOrder.span_leadingTerm_eq_span_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {m : MonomialOrder σ} {B : Set (MvPolynomial σ R)},
  (∀ p ∈ B, IsUnit (m.leadingCoeff p)) →
    Ideal.span (m.leadingTerm '' B) = Ideal.span ((fun p => (MvPolynomial.monomial (m.degree p)) 1) '' B)
-- Mathlib.Data.Fintype.Sets
Set.toFinset_eq_empty : ∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s], s.toFinset = ∅ ↔ s = ∅
-- Mathlib.CategoryTheory.GradedObject.Monoidal
CategoryTheory.GradedObject.Monoidal.ιTensorObj₃_eq : ∀ {I : Type u} [inst : AddMonoid I] {C : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ X₃ : CategoryTheory.GradedObject I C) [inst_3 : X₂.HasTensor X₃]
  [inst_4 : X₁.HasTensor (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃)] (i₁ i₂ i₃ j : I) (h : i₁ + i₂ + i₃ = j)
  (i₂₃ : I) (h' : i₂ + i₃ = i₂₃),
  CategoryTheory.GradedObject.Monoidal.ιTensorObj₃ X₁ X₂ X₃ i₁ i₂ i₃ j h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (X₁ i₁)
        (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₂ X₃ i₂ i₃ i₂₃ h'))
      (CategoryTheory.GradedObject.Monoidal.ιTensorObj X₁ (CategoryTheory.GradedObject.Monoidal.tensorObj X₂ X₃) i₁ i₂₃
        j ⋯)
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
MeasureTheory.MemLp.eLpNorm_mk_lt_top : ∀ {α : Type u_6} {E : Type u_7} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : NormedAddCommGroup E]
  {p : ENNReal} {f : α → E} (hfp : MeasureTheory.MemLp f p μ),
  MeasureTheory.eLpNorm (↑(MeasureTheory.AEEqFun.mk f ⋯)) p μ < ⊤
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.and_elim_l' : ∀ {σs : List (Type u)} {P Q R : Std.Do.SPred σs}, (P ⊢ₛ R) → P ∧ Q ⊢ₛ R
-- Init.Data.Int.Order
Int.lt_trichotomy : ∀ (a b : ℤ), a < b ∨ a = b ∨ b < a
-- Mathlib.Order.Interval.Set.Basic
Set.right_mem_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, a ∈ Set.Icc b a ↔ b ≤ a
-- Aesop.Tree.Data
Aesop.Goal.mk : Aesop.GoalData Aesop.Rapp Aesop.MVarCluster → Aesop.Goal
-- Mathlib.Algebra.Homology.CommSq
CategoryTheory.CommSq.cokernelCofork.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {X₁ X₂ X₃ X₄ : C}
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X₂ X₃] {f : X₁ ⟶ X₂} {g : X₁ ⟶ X₃} {inl inl_1 : X₂ ⟶ X₄}
  (e_inl : inl = inl_1) {inr inr_1 : X₃ ⟶ X₄} (e_inr : inr = inr_1) (sq : CategoryTheory.CommSq f g inl inr),
  sq.cokernelCofork = ⋯.cokernelCofork
-- Init.Control.Lawful.Instances
monadMap_refl : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (f : {α : Type u_1} → m α → m α), monadMap f = f
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolAux.children? : {Self : Type} → Lean.Lsp.DocumentSymbolAux Self → Option (Array Self)
-- Lean.Meta.Tactic.Grind.SimpUtil
Lean.Meta.Grind.simpOr : Lean.Meta.Simp.Simproc
-- Mathlib.Algebra.Ring.Invertible
invOf_two_add_invOf_two : ∀ {R : Type u_1} [inst : NonAssocSemiring R] [inst_1 : Invertible 2], ⅟2 + ⅟2 = 1
-- Std.Internal.Do.WP.Conjunctive
/-- `Except ε` is conjunctive: its `wp` is evaluation at the result.  -/
Std.Internal.Do.Except.instWPConjunctive : ∀ {ε α : Type u}, Std.Internal.Do.WPConjunctive (Except ε α) α Prop EPost⟨ε → Prop⟩
-- Mathlib.Topology.Order.LowerUpperTopology
Topology.WithUpper.instNonempty : ∀ {α : Type u_1} [Nonempty α], Nonempty (Topology.WithUpper α)
-- Std.Time.Format.Modifier
Std.Time.Modifier.b.inj : ∀ {presentation presentation_1 : Std.Time.Text},
  Std.Time.Modifier.b presentation = Std.Time.Modifier.b presentation_1 → presentation = presentation_1
-- Mathlib.Data.ENat.Basic
ENat.mul_top : ∀ {m : ℕ∞}, m ≠ 0 → m * ⊤ = ⊤
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.instFaithfulSMul_1 : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) (d : HNNExtension.NormalWord.TransversalPair G A B),
  FaithfulSMul (HNNExtension G A B φ) (HNNExtension.NormalWord d)
-- Init.Data.String.Pattern.Basic
/-- Checks whether the slice starts with the pattern.
   -/
String.Slice.Pattern.ForwardPattern.startsWith : {ρ : Type} → (pat : ρ) → [self : String.Slice.Pattern.ForwardPattern pat] → String.Slice → Bool
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.mk : {α : Type u_1} →
  [inst : Fintype α] →
    [inst_1 : Nonempty α] →
      {T : ℕ → ℝ} →
        {g : ℝ → ℝ} →
          {a b : α → ℝ} →
            {r : α → ℕ → ℕ} →
              (n₀ : ℕ) →
                0 < n₀ →
                  (∀ (i : α), 0 < a i) →
                    (∀ (i : α), 0 < b i) →
                      (∀ (i : α), b i < 1) →
                        (∀ x ≥ 0, 0 ≤ g x) →
                          AkraBazziRecurrence.GrowsPolynomially g →
                            (∀ (n : ℕ), n₀ ≤ n → T n = ∑ i, a i * T (r i n) + g ↑n) →
                              (∀ n < n₀, 0 < T n) →
                                (∀ (i : α) (n : ℕ), n₀ ≤ n → r i n < n) →
                                  (∀ (i : α),
                                      (fun n => ↑(r i n) - b i * ↑n) =o[Filter.atTop] fun n => ↑n / Real.log ↑n ^ 2) →
                                    AkraBazziRecurrence T g a b r
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.image_inv_Iic : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a : α),
  Inv.inv '' Set.Iic a = Set.Ici a⁻¹
-- Mathlib.Analysis.Calculus.TangentCone.Basic
uniqueDiffWithinAt_congr : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Semiring 𝕜] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] [ContinuousAdd E] {s t : Set E} {x : E},
  nhdsWithin x s = nhdsWithin x t → (UniqueDiffWithinAt 𝕜 s x ↔ UniqueDiffWithinAt 𝕜 t x)
-- Mathlib.RingTheory.PowerBasis
PowerBasis.basis_eq_pow : ∀ {R : Type u_7} {S : Type u_8} [inst : CommRing R] [inst_1 : Ring S] [inst_2 : Algebra R S] (self : PowerBasis R S)
  (i : Fin self.dim), self.basis i = self.gen ^ ↑i
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMulEquiv.coe_mk' : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace N] [inst_2 : Mul M]
  [inst_3 : Mul N] (f : M ≃ₜ N) (h : ∀ (x y : M), f (x * y) = f x * f y), ⇑(ContinuousMulEquiv.mk' f h) = ⇑f
-- Lean.Parser.Extra
/-- No-op parser combinator that advises the pretty printer to group and indent the given syntax.
By default, only syntax categories are grouped.  -/
Lean.Parser.ppGroup : Lean.Parser.Parser → Lean.Parser.Parser
-- Mathlib.Algebra.Order.Group.Abs
_private.Mathlib.Algebra.Order.Group.Abs.0.mabs_mul_eq_mul_mabs_le : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {a b : G},
  a ≤ b → (|a * b|ₘ = |a|ₘ * |b|ₘ ↔ 1 ≤ a ∧ 1 ≤ b ∨ a ≤ 1 ∧ b ≤ 1)
-- Init.Data.Int.DivMod.Lemmas
Int.emod_self_add_one : ∀ {x : ℤ}, 0 ≤ x → x % (x + 1) = x