mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Lemmas
Array.foldl_append_eq_append : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : α → Array β} {ys : Array β},
  Array.foldl (fun x1 x2 => x1 ++ f x2) ys xs = ys ++ (Array.map f xs).flatten
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
/-- Evaluation on an object `X` gives a functor
`SheafOfModules R ⥤ ModuleCat (R.val.obj X)`.  -/
SheafOfModules.evaluation : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (R : CategoryTheory.Sheaf J RingCat) →
        (X : Cᵒᵖ) → CategoryTheory.Functor (SheafOfModules R) (ModuleCat ↑(R.obj.obj X))
-- Mathlib.SetTheory.Cardinal.Defs
/-- **Alias** of `Cardinal.mk_congr_lift`. -/
Equiv.lift_cardinal_eq : ∀ {α : Type u} {β : Type v} (e : α ≃ β), Cardinal.lift.{v, u} (Cardinal.mk α) = Cardinal.lift.{u, v} (Cardinal.mk β)
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.areaForm_comp_rightAngleRotation : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)) (x y : E),
  (o.areaForm (o.rightAngleRotation x)) (o.rightAngleRotation y) = (o.areaForm x) y
-- Mathlib.LinearAlgebra.QuadraticForm.Prod
QuadraticMap.prod_apply : ∀ {R : Type u_2} {M₁ : Type u_3} {M₂ : Type u_4} {P : Type u_7} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid P] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R P] (Q₁ : QuadraticMap R M₁ P) (Q₂ : QuadraticMap R M₂ P) (a : M₁ × M₂),
  (Q₁.prod Q₂) a = Q₁ a.1 + Q₂ a.2
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.Sigma.ι_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasCoproduct f] (b c : β),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b) (CategoryTheory.Limits.Sigma.π f c) =
    if h : b = c then CategoryTheory.eqToHom ⋯ else 0
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_natCast_mul_add' : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : LinearOrder R] [inst_2 : IsOrderedAddMonoid R]
  [inst_3 : Archimedean R] {p : R} (hp : 0 < p) (a b : R) (m : ℕ), toIocMod hp (↑m * p + a) b = ↑m * p + toIocMod hp a b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₁ ∪ t₂ → k ∉ t₂ → k ∈ t₁
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
/-- The coequalizer of `f` and `g` exists.  -/
CategoryTheory.NormalEpiCategory.hasColimit_parallelPair : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteCoproducts C] [CategoryTheory.Limits.HasCokernels C]
  [CategoryTheory.IsNormalEpiCategory C] {X Y : C} (f g : X ⟶ Y),
  CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f g)
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- Equal measurable spaces are equivalent.  -/
MeasurableEquiv.cast : {α β : Type u_6} → [i₁ : MeasurableSpace α] → [i₂ : MeasurableSpace β] → α = β → i₁ ≍ i₂ → α ≃ᵐ β
-- Mathlib.MeasureTheory.Measure.MutuallySingular
MeasureTheory.Measure.MutuallySingular.symm : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ ν : MeasureTheory.Measure α}, ν.MutuallySingular μ → μ.MutuallySingular ν
-- Mathlib.Order.CompleteLattice.Basic
biSup_const : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {a : α} {s : Set β}, s.Nonempty → ⨆ i ∈ s, a = a
-- Mathlib.Algebra.Group.Action.Units
/-- Transfer `IsScalarTower G M α` to `IsScalarTower G Mˣ α`.  -/
Units.isScalarTower'_left : ∀ {G : Type u_1} {M : Type u_3} {α : Type u_5} [inst : Group G] [inst_1 : Monoid M] [inst_2 : MulAction G M]
  [inst_3 : SMul M α] [inst_4 : SMul G α] [inst_5 : SMulCommClass G M M] [inst_6 : IsScalarTower G M M]
  [IsScalarTower G M α], IsScalarTower G Mˣ α
-- Mathlib.Order.Monotone.Monovary
AntivaryOn.dual_left : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : Preorder α] [inst_1 : Preorder β] {f : ι → α} {g : ι → β}
  {s : Set ι}, AntivaryOn f g s → MonovaryOn (⇑OrderDual.toDual ∘ f) g s
-- Init.Data.Cast
NatCast.mk : {R : Type u} → (ℕ → R) → NatCast R
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.map_one_of_isCocycle₁ : ∀ {G : Type u_1} {A : Type u_2} [inst : Monoid G] [inst_1 : AddCommGroup A] [inst_2 : MulAction G A] {f : G → A},
  groupCohomology.IsCocycle₁ f → f 1 = 0
-- Init.Data.List.Attach
List.filterMap_subtype : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Option β} {g : α → Option β},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → List.filterMap f l = List.filterMap g l.unattach
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
instIsLeftCancelMulOfMulLeftReflectLE : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [MulLeftReflectLE α], IsLeftCancelMul α
-- Mathlib.RingTheory.RingHom.Finite
/-- If `S` is a finite `R`-algebra, then `S' = M⁻¹S` is a finite `R' = M⁻¹R`-algebra.  -/
RingHom.finite_localizationPreserves : RingHom.LocalizationPreserves @RingHom.Finite
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
/-- This expresses the tail of the coefficient sequence of the `GenContFract.of` an element `v` of
`K` as the coefficient sequence of that of the inverse of the fractional part of `v`.
 -/
GenContFract.of_s_tail : ∀ {K : Type u_1} [inst : DivisionRing K] [inst_1 : LinearOrder K] [inst_2 : FloorRing K] (v : K)
  [IsStrictOrderedRing K], (GenContFract.of v).s.tail = (GenContFract.of (Int.fract v)⁻¹).s
-- Mathlib.Order.Basic
/-- Any ordered subsingleton is densely ordered. Not an instance to avoid a heavy subsingleton
typeclass search.  -/
Subsingleton.instDenselyOrdered : ∀ {X : Type u_5} [Subsingleton X] [inst : LT X], DenselyOrdered X
-- Mathlib.Algebra.Group.Commute.Units
Commute.div_eq_div_iff_of_isUnit : ∀ {M : Type u_1} [inst : DivisionMonoid M] {a b c d : M},
  Commute b d → IsUnit b → IsUnit d → (a / b = c / d ↔ a * d = c * b)
-- Mathlib.CategoryTheory.Monad.Monadicity
CategoryTheory.Monad.instPreservesColimitWalkingParallelPairParallelPairMapAAppCounitObjAOfPreservesColimitOfIsSplitPair : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₁, u₂} D]
  {G : CategoryTheory.Functor D C} {F : CategoryTheory.Functor C D} (adj : F ⊣ G)
  [CategoryTheory.Monad.PreservesColimitOfIsSplitPair G] (A : adj.toMonad.Algebra),
  CategoryTheory.Limits.PreservesColimit (CategoryTheory.Limits.parallelPair (F.map A.a) (adj.counit.app (F.obj A.A))) G
-- Init.Data.UInt.Lemmas
UInt32.right_eq_add : ∀ {a b : UInt32}, b = a + b ↔ a = 0
-- Mathlib.Tactic.Hint
/-- Register a tactic for use with the `hint` tactic, e.g. `register_hint 1000 simp_all`.
The numeric argument specifies the priority: tactics with larger priorities run before
those with smaller priorities. The priority must be provided explicitly.
 -/
Mathlib.Tactic.Hint.registerHintStx : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Order.Group
tendsto_abs_nhdsNE_zero : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : AddCommGroup G] [inst_2 : LinearOrder G] [IsOrderedAddMonoid G]
  [OrderTopology G], Filter.Tendsto abs (nhdsWithin 0 {0}ᶜ) (nhdsWithin 0 (Set.Ioi 0))
-- Mathlib.Algebra.Polynomial.Div
Polynomial.natDegree_modByMonic_le : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R) {g : Polynomial R}, g.Monic → (p %ₘ g).natDegree ≤ g.natDegree
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.instSMulCotangentOfAlgebra : {R : Type u_2} →
  {S : Type u_1} → [inst : CommRing R] → [inst_1 : CommSemiring S] → [Algebra S R] → (I : Ideal R) → SMul S I.Cotangent
-- Mathlib.Data.Bundle
/-- `Bundle.Trivial B F` is the trivial bundle over `B` of fiber `F`.  -/
Bundle.Trivial : (B : Type u_4) → Type u_5 → B → Type u_5
-- Mathlib.CategoryTheory.Preadditive.Basic
/-- If a preadditive category has all kernels, then it also has all equalizers.  -/
CategoryTheory.Preadditive.hasEqualizers_of_hasKernels : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [CategoryTheory.Limits.HasKernels C], CategoryTheory.Limits.HasEqualizers C
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getD_insertManyIfNewUnit_list : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α Unit cmp} {l : List α} {k : α} {fallback : Unit},
  (t.insertManyIfNewUnit l).getD k fallback = ()
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.exists_lt_of_sum_lt : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddMonoid M] [inst_1 : LinearOrder M] [AddRightMono M] [AddLeftMono M]
  {l : List ι} (f g : ι → M), (List.map f l).sum < (List.map g l).sum → ∃ i ∈ l, f i < g i
-- Mathlib.CategoryTheory.Abelian.SerreClass.Bousfield
CategoryTheory.Abelian.isLocalization_isoModSerre_kernel_of_leftAdjoint : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Abelian C]
  [inst_3 : CategoryTheory.Abelian D] {G : CategoryTheory.Functor D C}
  [inst_4 : CategoryTheory.Limits.PreservesFiniteLimits G] [inst_5 : CategoryTheory.Limits.PreservesFiniteColimits G]
  {F : CategoryTheory.Functor C D} (adj : G ⊣ F) [F.Full] [F.Faithful], G.IsLocalization G.kernel.isoModSerre
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeff_neg : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R) (n : ℕ), (-p).coeff n = -p.coeff n
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.coe_smul : ∀ {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M]
  [inst_2 : AddCommMonoid N] [inst_3 : TopologicalSpace N] {R' : Type u_7} {A : Type u_9} [inst_4 : Monoid R']
  [inst_5 : Semiring A] [inst_6 : Module A M] [inst_7 : Module A N] [inst_8 : DistribMulAction R' N]
  [inst_9 : ContinuousConstSMul R' N] [inst_10 : SMulCommClass A R' N] (f : M [⋀^ι]→L[A] N) (c : R'), ⇑(c • f) = c • ⇑f
-- Mathlib.NumberTheory.HeckeRing.Defs
/-- The left subgroup is contained in `Δ`.  -/
IsHeckeTriple.left_le : ∀ {G : Type u_1} {inst : Group G} {Δ : Submonoid G} {H₁ : Subgroup G} (H₂ : Subgroup G) [self : IsHeckeTriple Δ H₁ H₂],
  H₁.toSubmonoid ≤ Δ
-- Mathlib.Topology.Inseparable
Specializes.trans : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x y z : X}, x ⤳ y → y ⤳ z → x ⤳ z
-- Mathlib.Topology.CWComplex.Classical.Graph
Topology.CWComplex.OneSkeletonGraph.exists_isLoopAt_iff_subsingleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] {C : Set X} [inst_1 : Topology.CWComplex C]
  (e : Topology.RelCWComplex.cell C 1),
  (∃ x, (Topology.CWComplex.OneSkeletonGraph C).IsLoopAt e x) ↔ (Topology.RelCWComplex.cellFrontier 1 e).Subsingleton
-- Init.Data.Array.Find
Array.findFinIdx?_singleton : ∀ {α : Type u_1} {a : α} {p : α → Bool}, Array.findFinIdx? p #[a] = if p a = true then some ⟨0, ⋯⟩ else none
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_eq_get!_getElem? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α}, m[a]! = m[a]?.get!
-- Init.Data.List.Lemmas
List.append_singleton_inj : ∀ {α : Type u_1} {a b : α} {as bs : List α}, as ++ [a] = bs ++ [b] ↔ as = bs ∧ a = b
-- Mathlib.NumberTheory.NumberField.Units.Regulator
/-- An `equiv` between `Fin (rank K)`, used to index the family of units, and `{w // w ≠ w₀}`
the index of the `logSpace`.
 -/
NumberField.Units.equivFinRank : (K : Type u_1) →
  [inst : Field K] →
    [inst_1 : NumberField K] → Fin (NumberField.Units.rank K) ≃ { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.IneqCnstrProof.subst : Lean.Grind.Linarith.Var →
  Lean.Meta.Grind.Arith.Linear.EqCnstr →
    Lean.Meta.Grind.Arith.Linear.IneqCnstr → Lean.Meta.Grind.Arith.Linear.IneqCnstrProof
-- Mathlib.Analysis.Complex.Norm
Complex.nnnorm_ofNat : ∀ (n : ℕ) [inst : n.AtLeastTwo], ‖OfNat.ofNat n‖₊ = OfNat.ofNat n
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.minKeyD_modify_eq_minKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp]
  {k : α} {f : β → β} {fallback : α}, (t.modify k f).minKeyD fallback = t.minKeyD fallback
-- Init.Data.Fin.Lemmas
Fin.le_or_lt : ∀ {n : ℕ} (a b : Fin n), a ≤ b ∨ b < a
-- Lean.CoreM
Lean.ImportM.runCoreM : {α : Type} → Lean.CoreM α → Lean.ImportM α
-- Init.Data.Nat.Basic
Nat.add_assoc : ∀ (n m k : ℕ), n + m + k = n + (m + k)
-- Lean.Compiler.InitAttr
Lean.setBuiltinInitAttr : Lean.Environment → Lean.Name → optParam Lean.Name Lean.Name.anonymous → Except String Lean.Environment
-- Init.Grind.ToInt
Lean.Grind.IntInterval.ii.sizeOf_spec : sizeOf Lean.Grind.IntInterval.ii = 1
-- Mathlib.Data.Vector3
_private.Mathlib.Data.Vector3.0.Fin2.add.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((k : ℕ) → motive k.succ) → motive x
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.single_eq_monomial : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (s : σ →₀ ℕ) (a : R),
  AddMonoidAlgebra.single s a = (MvPolynomial.monomial s) a
-- Init.GetElem
getElem?_eq_none_iff : ∀ {cont : Type u_1} {idx : Type u_2} {elem : Type u_3} {dom : cont → idx → Prop} [inst : GetElem? cont idx elem dom]
  [LawfulGetElem cont idx elem dom] (c : cont) (i : idx) [Decidable (dom c i)], c[i]? = none ↔ ¬dom c i
-- Mathlib.GroupTheory.Coxeter.Length
/-- **Alias** of `CoxeterSystem.exists_isReduced`. -/
CoxeterSystem.exists_reduced_word' : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (w : W),
  ∃ ω, cs.IsReduced ω ∧ w = cs.wordProd ω
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_erase_self : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k : α}, Std.DTreeMap.Internal.Impl.Const.get? (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl k = none
-- Mathlib.Data.Finset.Defs
Finset.instDecidableLT : {α : Type u_1} → [DecidableEq α] → DecidableLT (Finset α)
-- Init.Data.FloatArray.Basic
FloatArray.get : (ds : FloatArray) → (i : ℕ) → autoParam (i < ds.size) FloatArray.get._auto_1 → Float
-- Mathlib.Analysis.Normed.Group.Uniform
dist_add_add_le : ∀ {E : Type u_2} [inst : SeminormedAddCommGroup E] (a₁ a₂ b₁ b₂ : E), dist (a₁ + a₂) (b₁ + b₂) ≤ dist a₁ b₁ + dist a₂ b₂
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- `spectralNorm K L y` is positive if `y ≠ 0`.  -/
spectralNorm_zero_lt : ∀ {K : Type u_2} [inst : NormedField K] {L : Type u_3} [inst_1 : Field L] [inst_2 : Algebra K L] {y : L},
  y ≠ 0 → IsAlgebraic K y → 0 < spectralNorm K L y
-- Mathlib.CategoryTheory.SmallObject.Construction
/-- The canonical projection on the base object.  -/
CategoryTheory.SmallObject.πFunctorObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {I : Type w} →
      {A B : I → C} →
        (f : (i : I) → A i ⟶ B i) →
          {S X : C} →
            (πX : X ⟶ S) →
              [inst_1 :
                  CategoryTheory.Limits.HasColimitsOfShape
                    (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX)) C] →
                [inst_2 :
                    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
                      (CategoryTheory.SmallObject.functorObjLeft f πX)] →
                  CategoryTheory.SmallObject.functorObj f πX ⟶ S
-- Mathlib.Analysis.Normed.Module.PiTensorProduct.ProjectiveSeminorm
PiTensorProduct.liftIsometry.eq_1 : ∀ {ι : Type u_1} [inst : Fintype ι] (𝕜 : Type u_2) (E : ι → Type u_3) [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)]
  [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : (i : ι) → NormedSpace 𝕜 (E i)] (F : Type u_4)
  [inst_4 : SeminormedAddCommGroup F] [inst_5 : NormedSpace 𝕜 F],
  PiTensorProduct.liftIsometry 𝕜 E F = LinearIsometryEquiv.ofBounds (PiTensorProduct.liftEquiv 𝕜 E F) ⋯ ⋯
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.Basic
CStarAlgebra.nonneg_iff_eq_star_mul_self : ∀ {A : Type u_1} [inst : PartialOrder A] [inst_1 : NonUnitalRing A] [inst_2 : TopologicalSpace A] [inst_3 : StarRing A]
  [inst_4 : Module ℝ A] [inst_5 : SMulCommClass ℝ A A] [inst_6 : IsScalarTower ℝ A A] [StarOrderedRing A]
  [NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [NonnegSpectrumClass ℝ A] [IsSemitopologicalRing A]
  [T2Space A] {a : A}, 0 ≤ a ↔ ∃ b, a = star b * b
-- Mathlib.Algebra.Module.LinearMap.End
LinearMap.zero_smulRight : ∀ {R : Type u_1} {S : Type u_3} {M : Type u_4} {M₁ : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₁] [inst_3 : Module R M] [inst_4 : Module R M₁] [inst_5 : Semiring S] [inst_6 : Module R S]
  [inst_7 : Module S M] [inst_8 : IsScalarTower R S M] (x : M), LinearMap.smulRight 0 x = 0
-- Aesop.Tree.TreeM
Aesop.TreeM.instInhabited : {α : Type} → Inhabited (Aesop.TreeM α)
-- Mathlib.NumberTheory.Modular
/-- Explicit description of the truncated fundamental domain as a subset of `ℂ`, given by
obviously closed conditions.  -/
ModularGroup.coe_truncatedFundamentalDomain : ∀ (y : ℝ),
  UpperHalfPlane.coe '' ModularGroup.truncatedFundamentalDomain y = {z | 0 ≤ z.im ∧ z.im ≤ y ∧ |z.re| ≤ 1 / 2 ∧ 1 ≤ ‖z‖}
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.lift_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {G H₁ H₂ : CategoryTheory.AddGrp C} (f : G ⟶ H₁) (g : G ⟶ H₂),
  (CategoryTheory.CartesianMonoidalCategory.lift f g).hom = CategoryTheory.CartesianMonoidalCategory.lift f.hom g.hom
-- Mathlib.Combinatorics.Schnirelmann
/-- The Schnirelmann density is unaffected by adding `0`.  -/
schnirelmannDensity_insert_zero : ∀ {A : Set ℕ} [inst : DecidablePred fun x => x ∈ A] [inst_1 : DecidablePred fun x => x ∈ insert 0 A],
  schnirelmannDensity (insert 0 A) = schnirelmannDensity A
-- Mathlib.Data.Part
Part.some_inj : ∀ {α : Type u_1} {a b : α}, Part.some a = Part.some b ↔ a = b
-- Lean.Widget.InteractiveDiagnostic
/-- Nested text is ignored.  -/
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.widget : Lean.Widget.WidgetInstance → Std.Format → Lean.Widget.EmbedFmt✝
-- Lean.Server.CodeActions.Attr
/-- Read a hole code action from a declaration of the right type.  -/
Lean.CodeAction.mkHoleCodeAction : Lean.Name → Lean.ImportM Lean.CodeAction.HoleCodeAction
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.Iter.foldM_mapM : ∀ {α β γ δ : Type w} {n : Type w → Type w'} {o : Type w → Type w''} {Pred EPred : Type w} [inst : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_2 : Monad n] [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n]
  [inst_6 : Monad o] [inst_7 : Std.Internal.Do.Assertion Pred] [inst_8 : Std.Internal.Do.Assertion EPred]
  [inst_9 : Std.Internal.Do.WPMonad o Pred EPred] [inst_10 : Std.IteratorLoop α Id n]
  [inst_11 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id n] [Std.LawfulIteratorLoop α Id o]
  [inst_14 : MonadLiftT n o] [LawfulMonadLiftT n o] {f : β → n γ} {g : δ → γ → o δ} {init : δ} {it : Std.Iter β}
  {P : Pred} {Q : δ → Pred} {eQ : EPred},
  ⦃ P ⦄
      Std.Iter.foldM
        (fun d b => do
          let c ← liftM (f b)
          g d c)
        init it ⦃
      Q; eQ ⦄ →
    ⦃ P ⦄ Std.IterM.foldM g init (Std.Iter.mapM f it) ⦃ Q; eQ ⦄
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.instAdditiveObjEIntFunctorETruncGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (i : EInt), (t.eTruncGE.obj i).Additive
-- Mathlib.Tactic.CategoryTheory.Reassoc
/-- Version of `reassocExpr` for the `TermElabM` monad. Handles instance metavariables automatically.
 -/
Mathlib.Tactic.Reassoc.reassocExpr' : Lean.Expr → Lean.Elab.TermElabM Lean.Expr
-- Std.Data.HashMap.Raw
Std.HashMap.Raw.instMembershipOfBEqOfHashable : {α : Type u} → {β : Type v} → [BEq α] → [Hashable α] → Membership α (Std.HashMap.Raw α β)
-- Mathlib.Analysis.Normed.Operator.Mul
/-- **Alias** of `ContinuousLinearMap.toSpanSingletonLE`. -/
ContinuousLinearMap.ring_lmap_equiv_selfₗ : (R : Type u_1) →
  (S : Type u_2) →
    (M : Type u_3) →
      [inst : Semiring R] →
        [inst_1 : Semiring S] →
          [inst_2 : AddCommMonoid M] →
            [inst_3 : Module R M] →
              [inst_4 : Module S M] →
                [inst_5 : SMulCommClass R S M] →
                  [inst_6 : TopologicalSpace M] →
                    [inst_7 : ContinuousAdd M] →
                      [inst_8 : ContinuousConstSMul S M] →
                        [inst_9 : TopologicalSpace R] → [ContinuousSMul R M] → M ≃ₗ[S] R →L[R] M
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.add : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} {w x y z : R},
  RingConGen.Rel r w x → RingConGen.Rel r y z → RingConGen.Rel r (w + y) (x + z)
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.natDegree_pos_of_eraseLead_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] {f : Polynomial R}, f.eraseLead ≠ 0 → 0 < f.natDegree
-- Init.Data.BitVec.Decidable
/-- For small numerals this isn't necessary (as typeclass search can use the above two instances),
but for large numerals this provides a shortcut.
Note, however, that for large numerals the decision procedure may be very slow,
and you should use `bv_decide` if possible.
 -/
BitVec.instDecidableForallBitVec : (n : ℕ) → (P : BitVec n → Prop) → [DecidablePred P] → Decidable (∀ (v : BitVec n), P v)
-- Batteries.Data.AssocList
Batteries.AssocList.isEmpty.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (x : Batteries.AssocList α β), (x = Batteries.AssocList.nil → False) → x.isEmpty = false
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffAt_iff_nat : ∀ {𝕜 : 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] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x : M} {n : ℕ∞},
  ContMDiffAt I I' (↑n) f x ↔ ∀ (m : ℕ), ↑m ≤ n → ContMDiffAt I I' (↑m) f x
-- Mathlib.RingTheory.SimpleModule.Basic
IsSimpleModule.instIsPrincipal : ∀ (R : Type u_2) [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsSimpleModule R M]
  (S : Submodule R M), S.IsPrincipal
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
UniqueMDiffWithinAt.mono_nhds : ∀ {𝕜 : 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] {s t : Set M} {x : M},
  UniqueMDiffAt[s] x → nhdsWithin x s ≤ nhdsWithin x t → UniqueMDiffAt[t] x
-- Mathlib.NumberTheory.Pell
/-- If `(x, y)` is a solution with `x` positive, then all its powers have positive `x`.  -/
Pell.Solution₁.x_zpow_pos : ∀ {d : ℤ} {a : Pell.Solution₁ d}, 0 < a.x → ∀ (n : ℤ), 0 < (a ^ n).x