mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.module : {R : Type u_1} →
  {R₂ : Type u_3} →
    {S : Type u_5} →
      {M : Type u_8} →
        {M₂ : Type u_10} →
          [inst : Semiring R] →
            [inst_1 : Semiring R₂] →
              [inst_2 : AddCommMonoid M] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : Module R M] →
                    [inst_5 : Module R₂ M₂] →
                      {σ₁₂ : R →+* R₂} →
                        [inst_6 : Semiring S] →
                          [inst_7 : Module S M₂] → [SMulCommClass R₂ S M₂] → Module S (M →ₛₗ[σ₁₂] M₂)
-- Std.Net.Addr
Std.Net.instDecidableEqIPv4Addr.decEq : (x x_1 : Std.Net.IPv4Addr) → Decidable (x = x_1)
-- Mathlib.Control.Bitraversable.Lemmas
Bitraversable.tfst_eq_fst_id' : ∀ {t : Type u → Type u → Type u} [inst : Bitraversable t] [LawfulBitraversable t] {α α' β : Type u} (f : α → α'),
  Bitraversable.tfst (pure ∘ f) = pure ∘ Bifunctor.fst f
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_rco : ∀ {m n i : ℕ}, (m...n).toList[i]! = if i < n - m then m + i else 0
-- Mathlib.Analysis.Convex.Between
wbtw_pointReflection : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R] [IsStrictOrderedRing R]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P] (x y : P),
  Wbtw R y x ((AffineEquiv.pointReflection R x) y)
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_mul_self' : ∀ {α : Type u} [inst : Mul α] [inst_1 : One α] (a : α) {x : Invertible a}, ⅟a * a = 1
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.subConst.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G), A.subConst B = ↑(A - B).card / ↑A.card
-- Mathlib.Topology.Constructions
continuous_bool_rng : ∀ {X : Type u} [inst : TopologicalSpace X] {f : X → Bool} (b : Bool), Continuous f ↔ IsClopen (f ⁻¹' {b})
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Iter.toArray_eq_match_step.match_1.eq_2 : ∀ {α β : Type u_1} (motive : Std.IterStep (Std.Iter β) β → Sort u_2) (it' : Std.Iter β)
  (h_1 : (it' : Std.Iter β) → (out : β) → motive (Std.IterStep.yield it' out))
  (h_2 : (it' : Std.Iter β) → motive (Std.IterStep.skip it')) (h_3 : Unit → motive Std.IterStep.done),
  (match Std.IterStep.skip it' with
    | Std.IterStep.yield it' out => h_1 it' out
    | Std.IterStep.skip it' => h_2 it'
    | Std.IterStep.done => h_3 ()) =
    h_2 it'
-- Mathlib.Algebra.Order.GroupWithZero.Defs
MulPosMono.mk : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α],
  (∀ ⦃c : α⦄, 0 ≤ c → ∀ ⦃a b : α⦄, a ≤ b → a * c ≤ b * c) → MulPosMono α
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.lim_nonneg : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (x : X), 0 ≤ c.lim x
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Over.coprod_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasBinaryCoproducts C] {A : C}
  {X Y : CategoryTheory.Over A} (k : X ⟶ Y) (g : CategoryTheory.Over A),
  (CategoryTheory.Over.coprod.map k).app g =
    CategoryTheory.Over.homMk
      (CategoryTheory.Limits.coprod.map (CategoryTheory.Over.Hom.left k) (CategoryTheory.CategoryStruct.id g.left)) ⋯
-- Mathlib.Order.ModularLattice
inf_sup_assoc_of_le : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {x : α} (y : α) {z : α}, z ≤ x → x ⊓ y ⊔ z = x ⊓ (y ⊔ z)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrp.instBraided.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  [inst_4 : CategoryTheory.BraidedCategory C] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.Braided],
  CategoryTheory.Functor.mapGrp.instBraided F =
    { toMonoidal := CategoryTheory.Functor.mapGrp.instMonoidal F, braided := ⋯ }
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.tensorUnit_carrier : (CategoryTheory.MonoidalCategoryStruct.tensorUnit SFinKer).carrier = PUnit.{u + 1}
-- Mathlib.Topology.Order
/-- A topological space is discrete if every set is open, that is,
its topology equals the discrete topology `⊥`.  -/
DiscreteTopology : (α : Type u_2) → [t : TopologicalSpace α] → Prop
-- Mathlib.Algebra.Star.StarAlgHom
NonUnitalStarAlgHom.prodEquiv_symm_apply : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {C : Type u_4} [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : DistribMulAction R A] [inst_3 : Star A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction R B] [inst_6 : Star B] [inst_7 : NonUnitalNonAssocSemiring C]
  [inst_8 : DistribMulAction R C] [inst_9 : Star C] (f : A →⋆ₙₐ[R] B × C),
  NonUnitalStarAlgHom.prodEquiv.symm f =
    ((NonUnitalStarAlgHom.fst R B C).comp f, (NonUnitalStarAlgHom.snd R B C).comp f)
-- Mathlib.Order.Directed
/-- Local notation for a relation  -/
_private.Mathlib.Order.Directed.0.DirectedOn.«term_≼₂_» : Lean.TrailingParserDescr
-- Std.Do.PostCond
Std.Do.PostCond.entails_mayThrow : ∀ {α : Type u_1} {ps : Std.Do.PostShape} (p : Std.Do.PostCond α ps) (q : α → Std.Do.Assertion ps),
  p.entails (Std.Do.PostCond.mayThrow q) ↔ ∀ (a : α), p.1 a ⊢ₛ q a
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey!_filter_key : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] [inst : Inhabited α]
  {f : α → Bool} {k : α}, (Std.TreeMap.filter (fun k x => f k) t).getKey! k = (Option.filter f (t.getKey? k)).get!
-- Mathlib.Order.Interval.Set.SuccPred
Set.insert_Ico_succ_left_eq_Ico : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a b : α},
  a < b → insert a (Set.Ico (Order.succ a) b) = Set.Ico a b
-- Init.Data.BitVec.Basic
BitVec.instMul : {n : ℕ} → Mul (BitVec n)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.IsRevMatch.mk : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {startPos : s.Pos},
  String.Slice.Pattern.Model.PatternModel.Matches pat (s.sliceFrom startPos).copy →
    String.Slice.Pattern.Model.IsRevMatch pat startPos
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.dual : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  RightOrdContinuous f → LeftOrdContinuous (⇑OrderDual.toDual ∘ f ∘ ⇑OrderDual.ofDual)
-- Mathlib.RingTheory.NonUnitalSubring.Defs
/-- The ring homomorphism associated to an inclusion of `NonUnitalSubring`s.  -/
NonUnitalSubring.inclusion : {R : Type u} → [inst : NonUnitalNonAssocRing R] → {S T : NonUnitalSubring R} → S ≤ T → ↥S →ₙ+* ↥T
-- Mathlib.LinearAlgebra.Projection
LinearMap.ofIsCompl_smul : ∀ {R : Type u_7} [inst : CommRing R] {E : Type u_8} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_9}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] {p q : Submodule R E} (h : IsCompl p q) {φ : ↥p →ₗ[R] F}
  {ψ : ↥q →ₗ[R] F} (c : R), LinearMap.ofIsCompl h (c • φ) (c • ψ) = c • LinearMap.ofIsCompl h φ ψ
-- Init.Data.BitVec.Bitblast
_private.Init.Data.BitVec.Bitblast.0.BitVec.addRecAux_extractAndExtend_eq_cpopNatRec : ∀ {w n : ℕ} {x : BitVec w}, BitVec.addRecAux✝ (BitVec.extractAndExtend w x) n 0#w = ↑(x.cpopNatRec n 0)
-- Mathlib.FieldTheory.Finite.Polynomial
/-- A polynomial over the integers is divisible by `n : ℕ`
if and only if it is zero over `ZMod n`.  -/
MvPolynomial.C_dvd_iff_zmod : ∀ {σ : Type u_1} (n : ℕ) (φ : MvPolynomial σ ℤ),
  MvPolynomial.C ↑n ∣ φ ↔ (MvPolynomial.map (Int.castRingHom (ZMod n))) φ = 0
-- Mathlib.GroupTheory.Coset.Basic
/-- The natural bijection between the cosets `g + s` and `s`.  -/
AddSubgroup.leftCosetEquivAddSubgroup : {α : Type u_1} → [inst : AddGroup α] → {s : AddSubgroup α} → (g : α) → ↑(g +ᵥ ↑s) ≃ ↥s
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.equivTuple_apply : ∀ {R : Type u_1} (c₁ c₂ c₃ : R) (x : QuaternionAlgebra R c₁ c₂ c₃),
  (QuaternionAlgebra.equivTuple c₁ c₂ c₃) x = ![x.re, x.imI, x.imJ, x.imK]
-- Lean.Meta.Tactic.Simp.Types
Lean.Meta.Simp.SimpM.run : {α : Type} →
  Lean.Meta.Simp.Context →
    optParam Lean.Meta.Simp.State { } →
      optParam Lean.Meta.Simp.Methods { } → Lean.Meta.SimpM α → Lean.MetaM (α × Lean.Meta.Simp.State)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.pure_elim : ∀ {σs : List (Type u)} {Q R : Std.Do.SPred σs} {φ : Prop}, (Q ⊢ₛ ⌜φ⌝) → (φ → Q ⊢ₛ R) → Q ⊢ₛ R
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.isSome_getKey?_eq_contains : ∀ {α : Type u} {β : Type v} {m : Std.HashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], m.WF → ∀ {a : α}, (m.getKey? a).isSome = m.contains a
-- Mathlib.Data.Real.Basic
Real.instPreorder : Preorder ℝ
-- Mathlib.Analysis.Normed.Module.Completion
UniformSpace.Completion.instNormedCommRing : (A : Type u_3) → [inst : SeminormedCommRing A] → NormedCommRing (UniformSpace.Completion A)
-- Mathlib.AlgebraicTopology.SimplicialSet.RelativeMorphism
SSet.RelativeMorphism.const_map : ∀ {X Y : SSet} {A : X.Subcomplex} {y : Y.obj (Opposite.op { len := 0 })}
  {φ : A.toSSet ⟶ (SSet.Subcomplex.ofSimplex y).toSSet}, SSet.RelativeMorphism.const.map = SSet.const y
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblenWith_veblenWith_of_lt : ∀ {f : Ordinal.{u} → Ordinal.{u}} {o₁ o₂ : Ordinal.{u}},
  Order.IsNormal f →
    o₁ < o₂ → ∀ (a : Ordinal.{u}), Ordinal.veblenWith f o₁ (Ordinal.veblenWith f o₂ a) = Ordinal.veblenWith f o₂ a
-- Mathlib.Analysis.Complex.Conformal
/-- The **Cauchy-Riemann Equation**: A real-differentiable function `f` on `ℂ` is complex-differentiable
at `x` within `s` iff the derivative `fderivWithin ℝ f s x` maps `I` to
`I • (fderivWithin ℝ f s x) 1`.
 -/
differentiableWithinAt_complex_iff_differentiableWithinAt_real : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} {x : ℂ} {s : Set ℂ},
  UniqueDiffWithinAt ℝ s x →
    (DifferentiableWithinAt ℂ f s x ↔
      DifferentiableWithinAt ℝ f s x ∧ (fderivWithin ℝ f s x) Complex.I = Complex.I • (fderivWithin ℝ f s x) 1)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.exists_ne_zero_and_le_and_le : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : WithZero α}, x ≠ 0 → y ≠ 0 → ∃ z, z ≠ 0 ∧ z ≤ x ∧ z ≤ y
-- Init.Data.Nat.Dvd
Nat.mul_dvd_mul_right : ∀ {a b : ℕ}, a ∣ b → ∀ (c : ℕ), a * c ∣ b * c
-- Lean.Server.FileWorker.Utils
Lean.Server.FileWorker.RpcSession.mk.inj : ∀ {objects : Lean.Server.RpcObjectStore} {expireTime : ℕ} {objects_1 : Lean.Server.RpcObjectStore} {expireTime_1 : ℕ},
  { objects := objects, expireTime := expireTime } = { objects := objects_1, expireTime := expireTime_1 } →
    objects = objects_1 ∧ expireTime = expireTime_1
-- Mathlib.Data.List.Nodup
List.not_nodup_of_get_eq_of_ne : ∀ {α : Type u} (xs : List α) (n m : Fin xs.length), xs.get n = xs.get m → n ≠ m → ¬xs.Nodup
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁_obj_map_app : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X₁ : C)
  {X₂ Y₂ : C} (φ : X₂ ⟶ Y₂) (X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁ C).obj X₁).map φ).app X₃ =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X₃) X₁
-- Lean.Syntax
/-- Advance to the left sibling of the current node, if any.  -/
Lean.Syntax.Traverser.left : Lean.Syntax.Traverser → Lean.Syntax.Traverser
-- Init.Data.Range.Polymorphic.PRange
/-- `a<...b` is the range of elements greater than `a` and less than `b`.
See also `Std.Roo`.
 -/
Std.«term_<..._» : Lean.TrailingParserDescr
-- Init.Data.Vector.Attach
Vector.toList_pmap : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {xs : Vector α n} {P : α → Prop} {f : (a : α) → P a → β} {H : ∀ a ∈ xs, P a},
  (Vector.pmap f xs H).toList = List.pmap f xs.toList ⋯
-- Mathlib.Algebra.FreeAbelianGroup.Finsupp
FreeAbelianGroup.eq_sum_support_coeff_smul_of : ∀ {X : Type u_1} (a : FreeAbelianGroup X), a = ∑ x ∈ a.support, (FreeAbelianGroup.coeff x) a • FreeAbelianGroup.of x
-- Mathlib.Logic.Function.Basic
/-- The inverse of a function (which is a left inverse if `f` is injective
and a right inverse if `f` is surjective).  -/
Function.invFun : {α : Sort u} → {β : Sort u_3} → [Nonempty α] → (α → β) → β → α
-- Mathlib.Probability.Process.Stopping
MeasureTheory.IsStoppingTime.measurableSet_min_iff : ∀ {Ω : Type u_1} {ι : Type u_3} {m : MeasurableSpace Ω} [inst : LinearOrder ι] {f : MeasureTheory.Filtration ι m}
  {τ π : Ω → WithTop ι} (hτ : MeasureTheory.IsStoppingTime f τ) (hπ : MeasureTheory.IsStoppingTime f π) (s : Set Ω),
  MeasurableSet s ↔ MeasurableSet s ∧ MeasurableSet s
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.degreeOf.eq_2 : ∀ (x : Lean.Grind.CommRing.Var) (p : Lean.Grind.CommRing.Power) (m_1 : Lean.Grind.CommRing.Mon),
  (Lean.Grind.CommRing.Mon.mult p m_1).degreeOf x = bif p.x == x then p.k else m_1.degreeOf x
-- Mathlib.Data.Nat.Cast.Defs
_private.Mathlib.Data.Nat.Cast.Defs.0.Nat.unaryCast.match_1.splitter : (motive : ℕ → Sort u_1) → (x : ℕ) → (Unit → motive 0) → ((n : ℕ) → motive n.succ) → motive x
-- Mathlib.Topology.Order
NontrivialTopology.mk : ∀ {α : Type u_2} [inst : TopologicalSpace α], inst ≠ ⊤ → NontrivialTopology α
-- Mathlib.Data.Multiset.Defs
/-- The quotient map from `List α` to `Multiset α`.  -/
Multiset.ofList : {α : Type u_1} → List α → Multiset α
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- A monoidal category is semicartesian if the unit for the tensor product is a terminal object.  -/
CategoryTheory.SemiCartesianMonoidalCategory : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.Data.ENat.Lattice
ENat.sInf_add : ∀ {a : ℕ∞} {s : Set ℕ∞}, sInf s + a = ⨅ b ∈ s, b + a
-- Mathlib.Order.PartialSups
partialSups_eq_biUnion_range : ∀ {α : Type u_1} (s : ℕ → Set α) (n : ℕ), (partialSups s) n = ⋃ i ∈ Finset.range (n + 1), s i
-- Mathlib.Data.Quot
Quot.instUnique : {α : Sort u_1} → {ra : α → α → Prop} → [Unique α] → Unique (Quot ra)
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofFieldInfo.injEq : ∀ (i i_1 : Lean.Elab.FieldInfo), (Lean.Elab.Info.ofFieldInfo i = Lean.Elab.Info.ofFieldInfo i_1) = (i = i_1)
-- Mathlib.Data.Sym.Sym2
Sym2.ind : ∀ {α : Type u_1} {f : Sym2 α → Prop}, (∀ (x y : α), f s(x, y)) → ∀ (i : Sym2 α), f i
-- Mathlib.Data.Rat.Init
NNRat.instNNRatCast : NNRatCast ℚ≥0
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_map : ∀ {o : Type u_4} {m' : o → Type u_7} {n' : o → Type u_8} {α : Type u_12} {β : Type u_13} [inst : DecidableEq o]
  [inst_1 : Zero α] [inst_2 : Zero β] (M : (i : o) → Matrix (m' i) (n' i) α) (f : α → β),
  f 0 = 0 → (Matrix.blockDiagonal' M).map f = Matrix.blockDiagonal' fun k => (M k).map f
-- Mathlib.RingTheory.Valuation.Basic
Valuation.IsEquiv.ofClass_eq_zero : ∀ {R : Type u_3} {Γ₀ : Type u_4} {Γ'₀ : Type u_5} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀]
  [inst_2 : LinearOrderedCommMonoidWithZero Γ'₀] {v₁ : Valuation R Γ₀} {v₂ : Valuation R Γ'₀},
  v₁.IsEquiv v₂ → ∀ {r : R}, (MonoidWithZeroHom.ofClass v₁) r = 0 ↔ (MonoidWithZeroHom.ofClass v₂) r = 0
-- Mathlib.Analysis.Complex.UpperHalfPlane.Exp
Function.Periodic.im_invQParam_pos_of_norm_lt_one : ∀ {h : ℝ}, 0 < h → ∀ {q : ℂ}, ‖q‖ < 1 → q ≠ 0 → 0 < (Function.Periodic.invQParam h q).im
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instSupSet : {R : Type u} → {M : Type v} → [inst : SMul R M] → SupSet (SubMulAction R M)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.foldr_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} {δ : Type w} [Std.TransCmp cmp] {f : α → δ → δ}
  {init : δ}, t₁.Equiv t₂ → Std.TreeSet.foldr f init t₁ = Std.TreeSet.foldr f init t₂
-- Mathlib.Algebra.Lie.AdjointAction.Derivation
LieDerivation.maxTrivSubmodule_eq_bot_of_center_eq_bot : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L],
  LieAlgebra.center R L = ⊥ → LieModule.maxTrivSubmodule R L (LieDerivation R L L) = ⊥
-- Mathlib.FieldTheory.RatFunc.Basic
/-- `FractionRing.instFaithfulSMul` specialized to `R⟮X⟯`.  -/
RatFunc.faithfulSMul : ∀ (K : Type u_3) (E : Type u_4) [inst : Field K] [inst_1 : Field E] [inst_2 : Algebra K E] [FaithfulSMul K E],
  FaithfulSMul (Polynomial K) (RatFunc E)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_combine : ∀ {α : Type u_1} [inst : Lean.Grind.Ring α] (ctx : Lean.Grind.CommRing.Context α) (p₁ p₂ : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (p₁.combine p₂) =
    Lean.Grind.CommRing.Poly.denote ctx p₁ + Lean.Grind.CommRing.Poly.denote ctx p₂
-- Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula
_private.Mathlib.NumberTheory.ModularForms.LevelOne.DimensionFormula.0.ModularForm.weight_two_qExpansion_eq_zero : ∀ (f : ModularForm (Matrix.SpecialLinearGroup.mapGL ℝ).range 2), UpperHalfPlane.qExpansion 1 ⇑f = 0
-- Mathlib.Algebra.Group.Basic
sub_eq_of_eq_add' : ∀ {G : Type u_3} [inst : AddCommGroup G] {a b c : G}, a = b + c → a - b = c
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.nonempty_countableGeneratingSet : ∀ {α : Type u_1} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace.CountablyGenerated α],
  (MeasurableSpace.countableGeneratingSet α).Nonempty
-- Mathlib.Geometry.Manifold.BumpFunction
SmoothBumpFunction.isClosed_symm_image_closedBall : ∀ {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] {c : M}
  (f : SmoothBumpFunction I c) [FiniteDimensional ℝ E] [T2Space M],
  IsClosed (↑(extChartAt I c).symm '' (Metric.closedBall (↑(extChartAt I c) c) f.rOut ∩ Set.range ↑I))
-- Mathlib.Algebra.Group.Action.Faithful
FaithfulSMul.tower_bot : ∀ (R : Type u_4) (S : Type u_5) (T : Type u_6) [inst : Monoid S] [inst_1 : MulOneClass T] [inst_2 : SMul R S]
  [inst_3 : SMul R T] [inst_4 : MulAction S T] [IsScalarTower R S S] [IsScalarTower R T T] [IsScalarTower R S T]
  [FaithfulSMul R T], FaithfulSMul R S
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.coe_sndL : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : Semiring 𝕜] [inst_3 : AddCommGroup α] [inst_4 : AddCommGroup β] [inst_5 : Module 𝕜 α] [inst_6 : Module 𝕜 β],
  ↑(WithLp.sndL p 𝕜 α β) = WithLp.sndₗ p 𝕜 α β
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.EnoughInjectives
DerivedCategory.to_singleFunctor_obj_eq_zero_of_injective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {I : C} [CategoryTheory.Injective I] {K : CochainComplex C ℤ} {i : ℤ}
  (φ : DerivedCategory.Q.obj K ⟶ DerivedCategory.Q.obj ((CochainComplex.singleFunctor C i).obj I)) (n : ℤ),
  i < n → ∀ [K.IsStrictlyGE n], φ = 0
-- Mathlib.Order.Lattice
ofDual_sup : ∀ {α : Type u} [inst : Min α] (a b : αᵒᵈ), OrderDual.ofDual (a ⊔ b) = OrderDual.ofDual a ⊓ OrderDual.ofDual b
-- Init.Data.Order.Opposite
Std.OppositeOrderInstances.instLawfulOrderInfOpposite : ∀ {α : Type u_1} {il : LE α} {im : Min α} [Std.LawfulOrderInf α], Std.LawfulOrderSup α
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.isAmalgamation_iff_ofArrows : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (P : CategoryTheory.Functor Cᵒᵖ (Type w)) {B : C}
  {I : Type u_1} {X : I → C} (π : (i : I) → X i ⟶ B)
  (x : CategoryTheory.Presieve.FamilyOfElements P (CategoryTheory.Presieve.ofArrows X π)) (t : P.obj (Opposite.op B)),
  x.IsAmalgamation t ↔ ∀ (i : I), (CategoryTheory.ConcreteCategory.hom (P.map (π i).op)) t = x (π i) ⋯
-- Init.Data.SInt.Lemmas
Int32.toInt_ofIntLE : ∀ {x : ℤ} {h₁ : Int32.minValue.toInt ≤ x} {h₂ : x ≤ Int32.maxValue.toInt}, (Int32.ofIntLE x h₁ h₂).toInt = x
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.ofHom_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G K : CochainComplex C ℤ} (f : F ⟶ G) (g : G ⟶ K),
  CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp f g) =
    (CochainComplex.HomComplex.Cochain.ofHom f).comp (CochainComplex.HomComplex.Cochain.ofHom g) ⋯
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.Result'.isNNRat.inj : ∀ {inst : Lean.Expr} {q : ℚ} {n d proof inst_1 : Lean.Expr} {q_1 : ℚ} {n_1 d_1 proof_1 : Lean.Expr},
  Mathlib.Meta.NormNum.Result'.isNNRat inst q n d proof =
      Mathlib.Meta.NormNum.Result'.isNNRat inst_1 q_1 n_1 d_1 proof_1 →
    inst = inst_1 ∧ q = q_1 ∧ n = n_1 ∧ d = d_1 ∧ proof = proof_1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get.congr_simp : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m m_1 : Std.ExtDHashMap α fun x => β) (e_m : m = m_1) (a a_1 : α) (e_a : a = a_1) (h : a ∈ m),
  Std.ExtDHashMap.Const.get m a h = Std.ExtDHashMap.Const.get m_1 a_1 ⋯
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPushout.epi_f₂₄ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square C},
  sq.IsPushout → ∀ [CategoryTheory.Epi sq.f₁₃], CategoryTheory.Epi sq.f₂₄
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Functor.mapGrpNatIso.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_4 : F.Monoidal] [inst_5 : F'.Monoidal] (e : F ≅ F'),
  CategoryTheory.Functor.mapGrpNatIso e =
    CategoryTheory.NatIso.ofComponents (fun X => CategoryTheory.Grp.mkIso (e.app X.X) ⋯ ⋯) ⋯
-- Lean.Data.DeclarationRange
Lean.instReprDeclarationRanges.repr : Lean.DeclarationRanges → ℕ → Std.Format
-- Mathlib.Algebra.Group.Subgroup.Finite
Subgroup.eq_bot_of_card_le : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G) [Finite ↥H], Nat.card ↥H ≤ 1 → H = ⊥
-- Mathlib.CategoryTheory.Preadditive.Yoneda.Basic
/-- The Yoneda embedding for preadditive categories sends an object `Y` to the presheaf sending an
object `X` to the group of morphisms `X ⟶ Y`. At each point, we get an additional `End Y`-module
structure, see `preadditiveYonedaObj`.
 -/
CategoryTheory.preadditiveYoneda : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] → CategoryTheory.Functor C (CategoryTheory.Functor Cᵒᵖ AddCommGrpCat)
-- Mathlib.Tactic.Algebra.AlgebraNF
/-- Clean up the normal form into a more human-friendly format. This does everything
`RingNF.cleanup` does and also pulls the scalar multiplication from the end of of each term to
the start. i.e. x * y * (r • 1) → r • (x * y)
Used by `cleanup`.  -/
Mathlib.Tactic.Algebra.cleanupSMul : Mathlib.Tactic.RingNF.Config → Lean.Meta.Simp.Result → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.Algebra.Module.Presentation.Basic
/-- any solution in a module `N : Type w'` is obtained in a unique way
by postcomposing `solution : relations.Solution M` by a linear map `M →ₗ[A] N`.  -/
Module.Relations.Solution.IsPresentationCore.desc : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module A M] →
            {solution : relations.Solution M} →
              solution.IsPresentationCore →
                {N : Type w'} → [inst_3 : AddCommGroup N] → [inst_4 : Module A N] → relations.Solution N → M →ₗ[A] N
-- Mathlib.Algebra.Opposites
MulOpposite.op_one : ∀ {α : Type u_1} [inst : One α], MulOpposite.op 1 = 1