mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Finsupp
/-- Evaluation of a function `f : ι →₀ M` at a point as an additive monoid homomorphism.

See `Finsupp.lapply` in `Mathlib/LinearAlgebra/Finsupp/Defs.lean` for the stronger version as a
linear map.  -/
Finsupp.applyAddHom : {ι : Type u_1} → {M : Type u_3} → [inst : AddZeroClass M] → ι → (ι →₀ M) →+ M
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_dvd_prod_of_subset : ∀ {ι : Type u_7} {M : Type u_8} [inst : CommMonoid M] (s t : Finset ι) (f : ι → M), s ⊆ t → ∏ i ∈ s, f i ∣ ∏ i ∈ t, f i
-- Mathlib.Analysis.Complex.Trigonometric
Complex.ofReal_sin_ofReal_re : ∀ (x : ℝ), ↑(Complex.sin ↑x).re = Complex.sin ↑x
-- Mathlib.AlgebraicTopology.ModelCategory.Bifibrant
HomotopicalAlgebra.CofibrantObject.mk_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.CategoryWithCofibrations C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] (X : HomotopicalAlgebra.CofibrantObject C),
  ∃ Y, ∃ (x : HomotopicalAlgebra.IsCofibrant Y), X = HomotopicalAlgebra.CofibrantObject.mk Y
-- Mathlib.ModelTheory.Satisfiability
/-- The Łoś–Vaught Test : a criterion for categorical theories to be complete.  -/
Cardinal.Categorical.isComplete : ∀ {L : FirstOrder.Language} (κ : Cardinal.{w}) (T : L.Theory),
  κ.Categorical T →
    Cardinal.aleph0 ≤ κ →
      Cardinal.lift.{w, max u v} L.card ≤ Cardinal.lift.{max u v, w} κ →
        T.IsSatisfiable → (∀ (M : T.ModelType), Infinite ↑M) → T.IsComplete
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.fst_comp_prod : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_4} [inst_7 : TopologicalSpace M₃] [inst_8 : AddCommMonoid M₃]
  [inst_9 : Module R M₃] (f : M₁ →L[R] M₂) (g : M₁ →L[R] M₃), ContinuousLinearMap.fst R M₂ M₃ ∘SL f.prod g = f
-- Mathlib.Analysis.Normed.Group.Pointwise
vadd_sphere_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), x +ᵥ Metric.sphere 0 δ = Metric.sphere x δ
-- Mathlib.Analysis.CStarAlgebra.Unitary.Maps
Unitary.mulLeft_trans_mulLeft : ∀ {R : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : CStarRing A] [inst_3 : Ring R]
  [inst_4 : Module R A] [inst_5 : SMulCommClass R A A] (u v : ↥(unitary A)),
  ((Unitary.mulLeft R A) u).trans ((Unitary.mulLeft R A) v) = (Unitary.mulLeft R A) (v * u)
-- Mathlib.Topology.Order.Basic
pi_Ioo_mem_nhds' : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] {ι : Type u_1} [Finite ι]
  {a' b' x' : ι → α} [Nonempty ι], (∀ (i : ι), a' i < x' i) → (∀ (i : ι), x' i < b' i) → Set.Ioo a' b' ∈ nhds x'
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
/-- The chromatic number of a tree is at most 2.  -/
SimpleGraph.IsTree.chromaticNumber_le_two : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsTree → G.chromaticNumber ≤ 2
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `AddHom.pi_injective`. -/
AddHom.injective_pi : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] {γ : Type w} [Nonempty I] [inst_2 : Add γ]
  (g : (i : I) → γ →ₙ+ f i), (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(AddHom.pi g)
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
_private.Mathlib.RingTheory.AdicCompletion.AsTensorProduct.0.AdicCompletion.tens_exact : ∀ {R : Type u} [inst : CommRing R] (I : Ideal R) (M : Type u) [inst_1 : AddCommGroup M] [inst_2 : Module R M] {ι : Type}
  (f : (ι → R) →ₗ[R] M),
  Function.Surjective ⇑f → Function.Exact ⇑(AdicCompletion.lTensorKerIncl✝ I M f) ⇑(AdicCompletion.lTensorf✝ I M f)
-- Mathlib.RingTheory.HopfAlgebra.GroupLike
GroupLike.instCommGroup : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] → [inst_1 : CommSemiring A] → [inst_2 : HopfAlgebra R A] → CommGroup (GroupLike R A)
-- Init.Data.String.Iterate
String.Slice.instInhabitedRevPosIterator.default : {s : String.Slice} → s.RevPosIterator
-- Mathlib.Data.Multiset.Find
Multiset.find?_eq_choose : ∀ {α : Type u_1} (p : α → Prop) [inst : DecidablePred p] {s : Multiset α} (hp : ∃! x, x ∈ s ∧ p x),
  Multiset.find? p s ⋯ = some (Multiset.choose p s hp)
-- Mathlib.RingTheory.Localization.InvSubmonoid
IsLocalization.toInvSubmonoid_surjective : ∀ {R : Type u_1} [inst : CommRing R] (M : Submonoid R) (S : Type u_2) [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsLocalization M S], Function.Surjective ⇑(IsLocalization.toInvSubmonoid M S)
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.hom_ext_iff : ∀ {M N : SemiNormedGrp} {f g : M ⟶ N}, f = g ↔ SemiNormedGrp.Hom.hom f = SemiNormedGrp.Hom.hom g
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.coeMonoidHom_apply : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : MulOneClass α] (s : Finset α), Finset.coeMonoidHom s = ↑s
-- Mathlib.Order.WellFoundedSet
Set.wellFoundedOn_image : ∀ {α : Type u_2} {β : Type u_3} {r : α → α → Prop} {f : β → α} {s : Set β},
  (f '' s).WellFoundedOn r ↔ s.WellFoundedOn (Function.onFun r f)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.prodMap_toFun : ∀ {A : Type u_2} {B : Type u_3} {C : Type u_4} {D : Type u_5} [inst : AddMonoid A] [inst_1 : AddMonoid B]
  [inst_2 : AddMonoid C] [inst_3 : AddMonoid D] [inst_4 : TopologicalSpace A] [inst_5 : TopologicalSpace B]
  [inst_6 : TopologicalSpace C] [inst_7 : TopologicalSpace D] (f : A →ₜ+ C) (g : B →ₜ+ D) (i : A × B),
  (f.prodMap g) i = (f i.1, g i.2)
-- Mathlib.Combinatorics.Additive.Convolution
Finset.convolution_le_card_right : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A B : Finset G} {x : G}, A.convolution B x ≤ B.card
-- Std.Data.Internal.List.Associative
/-- Internal implementation detail of the hash map  -/
Std.Internal.List.insertListIfNewUnit : {α : Type u} → [BEq α] → List ((_ : α) × Unit) → List α → List ((_ : α) × Unit)
-- Mathlib.MeasureTheory.Group.Arithmetic
Pi.measurableSub : ∀ {ι : Type u_5} {α : ι → Type u_6} [inst : (i : ι) → Sub (α i)] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  [∀ (i : ι), MeasurableSub (α i)], MeasurableSub ((i : ι) → α i)
-- Batteries.Data.Fin.Coding
_private.Batteries.Data.Fin.Coding.0.Fin.encodeOption.match_1.eq_1 : ∀ {n : ℕ} (motive : Option (Fin n) → Sort u_1) (h_1 : Unit → motive none)
  (h_2 : (i : ℕ) → (h : i < n) → motive (some ⟨i, h⟩)),
  (match none with
    | none => h_1 ()
    | some ⟨i, h⟩ => h_2 i h) =
    h_1 ()
-- Lean.Parser.Basic
Lean.Parser.instBEqLeadingIdentBehavior : BEq Lean.Parser.LeadingIdentBehavior
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_congr' : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  (∀ᶠ (x : β) in f, u x ≠ ⊤ → (p x ↔ q x)) → Filter.bliminf u f p = Filter.bliminf u f q
-- Init.Data.Nat.Lemmas
Nat.lt_sub_iff_add_lt' : ∀ {a b c : ℕ}, a < c - b ↔ b + a < c
-- Mathlib.Analysis.Analytic.Order
analyticOrderAt_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {z₀ : 𝕜}, analyticOrderAt f z₀ = 0 ↔ ¬AnalyticAt 𝕜 f z₀ ∨ f z₀ ≠ 0
-- Init.Data.Option.Basic
Option.isNone_none : ∀ {α : Type u_1}, none.isNone = true
-- Mathlib.Topology.Algebra.Field
/-- A topological division ring is a division ring with a topology where all operations are
continuous, including inversion.  -/
IsTopologicalDivisionRing : (K : Type u_1) → [DivisionRing K] → [TopologicalSpace K] → Prop
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Abs
CFC.abs_nnrpow : ∀ {A : Type u_2} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : TopologicalSpace A] [inst_3 : Module ℝ A]
  [inst_4 : SMulCommClass ℝ A A] [inst_5 : IsScalarTower ℝ A A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A]
  [inst_8 : StarOrderedRing A] [inst_9 : NonnegSpectrumClass ℝ A] [IsTopologicalRing A] [T2Space A] (a : A)
  (x : NNReal), CFC.abs a ^ x = (star a * a) ^ (x / 2)
-- Lean.Data.Lsp.CancelParams
Lean.Lsp.instInhabitedCancelParams.default : Lean.Lsp.CancelParams
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
/-- The real power function `x ^ y`, defined as the real part of the complex power function.
For `x > 0`, it is equal to `exp (y log x)`. For `x = 0`, one sets `0 ^ 0=1` and `0 ^ y=0` for
`y ≠ 0`. For `x < 0`, the definition is somewhat arbitrary as it depends on the choice of a complex
determination of the logarithm. With our conventions, it is equal to `exp (y log x) cos (π y)`.  -/
Real.rpow : ℝ → ℝ → ℝ
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.ofClosedAddSubgroup.eq_1 : ∀ {G : ProfiniteAddGrp.{u_1}} (H : ClosedAddSubgroup ↑G.toProfinite.toTop),
  ProfiniteAddGrp.ofClosedAddSubgroup H = ProfiniteAddGrp.of ↥↑H
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciInf_eq_iff : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLinearOrder α] [WellFoundedLT α] [Nonempty ι] (f : ι → α)
  (n : α), ⨅ i, f i = n ↔ (∃ i, f i = n) ∧ ∀ (i : ι), n ≤ f i
-- Mathlib.Util.PrintSorries
Mathlib.PrintSorries.State.mk.sizeOf_spec : ∀ (visited : Lean.NameSet) (sorries : Std.HashSet Lean.Expr) (sorryMsgs : Array Lean.MessageData),
  sizeOf { visited := visited, sorries := sorries, sorryMsgs := sorryMsgs } =
    1 + sizeOf visited + sizeOf sorries + sizeOf sorryMsgs
-- Mathlib.FieldTheory.Minpoly.Basic
minpoly.algEquiv_eq : ∀ {A : Type u_1} {B : Type u_2} {B' : Type u_3} [inst : CommRing A] [inst_1 : Ring B] [inst_2 : Ring B']
  [inst_3 : Algebra A B] [inst_4 : Algebra A B'] (f : B ≃ₐ[A] B') (x : B), minpoly A (f x) = minpoly A x
-- Mathlib.Topology.CWComplex.Classical.Finite
/-- If we want to construct a finite CW complex we can add the conditions `eventually_isEmpty_cell`
and `finite_cell`, relax the condition `mapsTo` and remove the condition `closed'`.  -/
Topology.CWComplex.mkFinite : {X : Type u} →
  [inst : TopologicalSpace X] →
    (C : Set X) →
      (cell : ℕ → Type u) →
        (map : (n : ℕ) → cell n → PartialEquiv (Fin n → ℝ) X) →
          (∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (cell n)) →
            (∀ (n : ℕ), Finite (cell n)) →
              (∀ (n : ℕ) (i : cell n), (map n i).source = Metric.ball 0 1) →
                (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i)) (Metric.closedBall 0 1)) →
                  (∀ (n : ℕ) (i : cell n), ContinuousOn (↑(map n i).symm) (map n i).target) →
                    (Set.univ.PairwiseDisjoint fun ni => ↑(map ni.fst ni.snd) '' Metric.ball 0 1) →
                      (∀ (n : ℕ) (i : cell n),
                          Set.MapsTo (↑(map n i)) (Metric.sphere 0 1)
                            (⋃ m, ⋃ (_ : m < n), ⋃ j, ↑(map m j) '' Metric.closedBall 0 1)) →
                        ⋃ n, ⋃ j, ↑(map n j) '' Metric.closedBall 0 1 = C → Topology.CWComplex C
-- Std.Data.ExtTreeSet.Basic
/-- Tries to retrieve the smallest element of the tree set, returning `fallback` if the tree set is empty.
 -/
Std.ExtTreeSet.minD : {α : Type u} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → Std.ExtTreeSet α cmp → α → α
-- Mathlib.CategoryTheory.Subobject.Basic
/-- Declare a function on subobjects of `X` by specifying a function on monomorphisms with
codomain `X`.  -/
CategoryTheory.Subobject.lift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {α : Sort u_1} →
      {X : C} →
        (F : ⦃A : C⦄ → (f : A ⟶ X) → [CategoryTheory.Mono f] → α) →
          (∀ ⦃A B : C⦄ (f : A ⟶ X) (g : B ⟶ X) [inst_1 : CategoryTheory.Mono f] [inst_2 : CategoryTheory.Mono g]
              (i : A ≅ B), CategoryTheory.CategoryStruct.comp i.hom g = f → F f = F g) →
            CategoryTheory.Subobject X → α
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.IsPrincipal`.

---

An ordinal `o` is said to be principal (or indecomposable) under an operation when `Iio o` is
closed under that operation.

For simplicity, we break usual convention and regard `0` as principal.  -/
Ordinal.Principal : (Ordinal.{u_1} → Ordinal.{u_1} → Ordinal.{u_1}) → Ordinal.{u_1} → Prop
-- Lean.Compiler.InlineAttrs
Lean.Compiler.hasMacroInlineAttribute : Lean.Environment → Lean.Name → Bool
-- Mathlib.Topology.Algebra.Module.Spaces.UniformConvergenceCLM
/-- Reinterpret `f : E →SL[σ] F` as an element of `E →SLᵤ[σ, 𝔖] F`.  -/
UniformConvergenceCLM.ofFun : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    [inst : NormedField 𝕜₁] →
      [inst_1 : NormedField 𝕜₂] →
        (σ : 𝕜₁ →+* 𝕜₂) →
          {E : Type u_3} →
            (F : Type u_4) →
              [inst_2 : AddCommGroup E] →
                [inst_3 : Module 𝕜₁ E] →
                  [inst_4 : TopologicalSpace E] →
                    [inst_5 : AddCommGroup F] →
                      [inst_6 : Module 𝕜₂ F] →
                        [inst_7 : TopologicalSpace F] → (𝔖 : Set (Set E)) → (E →SL[σ] F) ≃ UniformConvergenceCLM σ F 𝔖
-- Init.Grind.Ring.Envelope
Lean.Grind.CommRing.OfCommSemiring.instIntCastQ : {α : Type u} →
  [inst : Lean.Grind.CommSemiring α] →
    [Lean.Grind.CommRing (Lean.Grind.Ring.OfSemiring.Q α)] → IntCast (Lean.Grind.Ring.OfSemiring.Q α)
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
_private.Mathlib.Combinatorics.SetFamily.AhlswedeZhang.0.Finset.upper_aux : ∀ {α : Type u_1} [inst : SemilatticeInf α] {s t : Finset α} {a : α} [inst_1 : DecidableEq α],
  a ∈ upperClosure ↑(s ∪ t) ↔ a ∈ upperClosure ↑s ∨ a ∈ upperClosure ↑t
-- Mathlib.Combinatorics.SimpleGraph.Extremal.Basic
/-- If `H` contains a copy of `H'`, then `extremalNumber n H` is at most `extremalNumber n H`.  -/
SimpleGraph.IsContained.extremalNumber_le : ∀ {n : ℕ} {W : Type u_2} {H : SimpleGraph W} {W' : Type u_4} {H' : SimpleGraph W'},
  H'.IsContained H → SimpleGraph.extremalNumber n H' ≤ SimpleGraph.extremalNumber n H
-- Mathlib.Algebra.Module.Submodule.Lattice
AddSubmonoid.toNatSubmodule_symm : ∀ {M : Type u_3} [inst : AddCommMonoid M], ⇑AddSubmonoid.toNatSubmodule.symm = Submodule.toAddSubmonoid
-- Mathlib.CategoryTheory.Functor.KanExtension.Pointwise
CategoryTheory.Functor.instIsLeftKanExtensionPointwiseLeftKanExtensionPointwiseLeftKanExtensionUnit : ∀ {C : Type u_1} {D : Type u_2} {H : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_4, u_4} H]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasPointwiseLeftKanExtension F],
  (L.pointwiseLeftKanExtension F).IsLeftKanExtension (L.pointwiseLeftKanExtensionUnit F)
-- Mathlib.Algebra.Homology.SpectralObject.Page
CategoryTheory.Abelian.SpectralObject.instEpiπE : ∀ {C : Type u_2} {ι : Type u_4} [inst : CategoryTheory.Category.{u_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{u_3, u_4} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k l : ι} (f₁ : i ⟶ j) (f₂ : j ⟶ k) (f₃ : k ⟶ l) (n₀ n₁ n₂ : ℤ)
  (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂), CategoryTheory.Epi (X.πE f₁ f₂ f₃ n₀ n₁ n₂ hn₁ hn₂)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskerRight_twice : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {H K : CategoryTheory.Functor B C} (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (α : H ⟶ K),
  CategoryTheory.Functor.whiskerRight (CategoryTheory.Functor.whiskerRight α F) G =
    CategoryTheory.CategoryStruct.comp (H.associator F G).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight α (F.comp G)) (K.associator F G).inv)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {l : List ((a : α) × β a)} {k : α}
  (contains_eq_false : (List.map Sigma.fst l).contains k = false) {h : k ∈ m.insertMany l},
  (m.insertMany l).getKey k h = m.getKey k ⋯
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.mapMon_obj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.LaxMonoidal] (A : CategoryTheory.Mon C), (F.mapMon.obj A).X = F.obj A.X
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Given `F : WalkingParallelPair ⥤ C`, which is really the same as
`parallelPair (F.map left) (F.map right)` and a cone on `F`, we get a fork on
`F.map left` and `F.map right`.  -/
CategoryTheory.Limits.Fork.ofCone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingParallelPair C} →
      CategoryTheory.Limits.Cone F →
        CategoryTheory.Limits.Fork (F.map CategoryTheory.Limits.WalkingParallelPairHom.left)
          (F.map CategoryTheory.Limits.WalkingParallelPairHom.right)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulConstC.go.eq_def : ∀ (k : ℤ) (c : ℕ) (a : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.mulConstC.go k c a =
    match a with
    | Lean.Grind.CommRing.Poly.num k' => Lean.Grind.CommRing.Poly.num (k * k' % ↑c)
    | Lean.Grind.CommRing.Poly.add k' m p =>
      have k_1 := k * k' % ↑c;
      bif k_1 == 0 then Lean.Grind.CommRing.Poly.mulConstC.go k c p
      else Lean.Grind.CommRing.Poly.add k_1 m (Lean.Grind.CommRing.Poly.mulConstC.go k c p)
-- Init.Data.String.Iterator
/-- Moves the iterator's position forward by one character, unconditionally.

The proof of `it.hasNext` ensures that there is, in fact, a position that's one character forwards.
This function is faster that `String.Iterator.next` due to avoiding a run-time bounds check.
 -/
String.Legacy.Iterator.next' : (it : String.Legacy.Iterator) → it.hasNext = true → String.Legacy.Iterator
-- Mathlib.Order.Atoms
IsCoatom.ne_top_iff_eq : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderTop α] {a b : α}, IsCoatom a → a ≤ b → (b ≠ ⊤ ↔ b = a)
-- Mathlib.LinearAlgebra.Dimension.Basic
rank_top : ∀ (R : Type u) (M : Type v) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Module.rank R ↥⊤ = Module.rank R M
-- Mathlib.RingTheory.Extension.Generators
/-- Construct `Generators` from an assignment `I → S` such that `R[X] → S` is surjective.  -/
Algebra.Generators.ofAlgHom : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {I : Type u_1} → (f : MvPolynomial I R →ₐ[R] S) → Function.Surjective ⇑f → Algebra.Generators R S I
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.eapprox_comp : ∀ {α : Type u_1} {γ : Type u_3} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace γ] {f : γ → ENNReal} {g : α → γ}
  {n : ℕ},
  Measurable f →
    Measurable g → ⇑(MeasureTheory.SimpleFunc.eapprox (f ∘ g) n) = ⇑(MeasureTheory.SimpleFunc.eapprox f n) ∘ g
-- Mathlib.Data.Set.Card
Function.Embedding.encard_le : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (e : ↑s ↪ ↑t), s.encard ≤ t.encard
-- Init.Core
Std.LawfulCommIdentity.toLawfulIdentity : ∀ {α : Sort u} {op : α → α → α} {o : outParam α} {hc : Std.Commutative op} [self : Std.LawfulCommIdentity op o],
  Std.LawfulIdentity op o
-- Mathlib.LinearAlgebra.Matrix.Irreducible.Defs
/-- For a matrix `A` with nonnegative entries, the `(i, j)`-entry of the `k`-th power `A ^ k`
is strictly positive if and only if there exists a path of length `k` from `i` to `j` in the
quiver associated to `A` via `toQuiver`.  -/
Matrix.pow_apply_pos_iff_nonempty_path : ∀ {n : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] {A : Matrix n n R} [inst_2 : Fintype n]
  [IsOrderedRing R] [PosMulStrictMono R] [Nontrivial R] [inst_6 : DecidableEq n],
  (∀ (i j : n), 0 ≤ A i j) → ∀ (k : ℕ) (i j : n), 0 < (A ^ k) i j ↔ Nonempty { p // p.length = k }
-- Mathlib.Analysis.Calculus.BumpFunction.Basic
ContDiffBump.rOut_pos : ∀ {E : Type u_1} {c : E} (f : ContDiffBump c), 0 < f.rOut
-- Mathlib.Order.Filter.Bases.Basic
FilterBasis.mk.inj : ∀ {α : Type u_6} {sets : Set (Set α)} {nonempty : sets.Nonempty}
  {inter_sets : ∀ {x y : Set α}, x ∈ sets → y ∈ sets → ∃ z ∈ sets, z ⊆ x ∩ y} {sets_1 : Set (Set α)}
  {nonempty_1 : sets_1.Nonempty} {inter_sets_1 : ∀ {x y : Set α}, x ∈ sets_1 → y ∈ sets_1 → ∃ z ∈ sets_1, z ⊆ x ∩ y},
  { sets := sets, nonempty := nonempty, inter_sets := inter_sets } =
      { sets := sets_1, nonempty := nonempty_1, inter_sets := inter_sets_1 } →
    sets = sets_1
-- Mathlib.Data.Ordmap.Invariants
Ordnode.size_dual : ∀ {α : Type u_1} (t : Ordnode α), t.dual.size = t.size
-- Mathlib.Algebra.Group.Subgroup.Defs
SubgroupClass.div.eq_1 : ∀ {G : Type u_5} {S : Type u_6} [inst : DivInvMonoid G] [inst_1 : SetLike S G] [inst_2 : SubgroupClass S G] {H : S},
  SubgroupClass.div = { div := fun a b => ⟨↑a / ↑b, ⋯⟩ }
-- Mathlib.Analysis.Complex.UnitDisc.Basic
/-- **Alias** of `Complex.UnitDisc.re_star`. -/
Complex.UnitDisc.re_conj : ∀ (z : Complex.UnitDisc), (star z).re = z.re
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instCoe : Coe Complex.UnitClosedDisc ℂ
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.tsub_lt_iff_left : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable b → b ≤ a → (a - b < c ↔ a < b + c)
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
BoxIntegral.IntegrationParams.MemBaseSet.unionComplToSubordinate : ∀ {ι : Type u_1} [inst : Fintype ι] {I : BoxIntegral.Box ι} {c : NNReal} {l : BoxIntegral.IntegrationParams}
  {r₁ r₂ : (ι → ℝ) → ↑(Set.Ioi 0)} {π₁ : BoxIntegral.TaggedPrepartition I},
  l.MemBaseSet I c r₁ π₁ →
    (∀ x ∈ BoxIntegral.Box.Icc I, r₂ x ≤ r₁ x) →
      ∀ {π₂ : BoxIntegral.Prepartition I} (hU : π₂.iUnion = ↑I \ π₁.iUnion),
        (l.bDistortion = true → π₂.distortion ≤ c) → l.MemBaseSet I c r₁ (π₁.unionComplToSubordinate π₂ hU r₂)
-- Mathlib.Order.Minimal
/-- **Alias** of `OrderEmbedding.inter_preimage_setOfPred_minimal_eq_of_subset`. -/
OrderEmbedding.inter_preimage_setOf_minimal_eq_of_subset : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α ↪o β} {t : Set β},
  t ⊆ ⇑f '' s → (x ∈ s ∩ ⇑f ⁻¹' {y | Minimal (fun x => x ∈ t) y} ↔ Minimal (fun x => x ∈ s ∩ ⇑f ⁻¹' t) x)
-- Mathlib.Topology.Spectral.Hom
SpectralMap.coe_comp_continuousMap' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] (f : SpectralMap β γ) (g : SpectralMap α β), ↑(f.comp g) = (↑f).comp ↑g
-- Mathlib.Geometry.Manifold.VectorBundle.Tensoriality
/-- If the operation `Φ` on sections of a vector bundle `V` is tensorial at `x`, then it depends
only on the value of the section at `x`.  -/
TensorialAt.pointwise : ∀ {𝕜 : 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] {V : M → Type u_6} [inst_8 : TopologicalSpace (Bundle.TotalSpace F V)]
  [inst_9 : (x : M) → AddCommGroup (V x)] [inst_10 : (x : M) → Module 𝕜 (V x)]
  [inst_11 : (x : M) → TopologicalSpace (V x)] [inst_12 : FiberBundle F V] {A : Type u_9} [inst_13 : AddCommGroup A]
  [inst_14 : Module 𝕜 A] {Φ : ((x : M) → V x) → A} {x : M} [inst_15 : VectorBundle 𝕜 F V] [CompleteSpace 𝕜]
  [FiniteDimensional 𝕜 F] [ContMDiffVectorBundle 1 F V I],
  TensorialAt I F Φ x → ∀ {σ σ' : (x : M) → V x}, MDiffAt (T% σ) x → MDiffAt (T% σ') x → σ x = σ' x → Φ σ = Φ σ'
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.surjective_of_epi : ∀ {X Y : Type u} (f : X ⟶ Y) [hf : CategoryTheory.Epi f], Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Topology.Compactification.OnePoint.Basic
OnePoint.infty_ne_coe : ∀ {X : Type u_1} (x : X), OnePoint.infty ≠ ↑x