mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.denote_mulC_nc_go : ∀ {α : Type u_1} {c : ℕ} [inst : Lean.Grind.Ring α] [Lean.Grind.IsCharP α c] (ctx : Lean.Grind.CommRing.Context α)
  (p₁ p₂ acc : Lean.Grind.CommRing.Poly),
  Lean.Grind.CommRing.Poly.denote ctx (Lean.Grind.CommRing.Poly.mulC_nc.go p₂ c p₁ acc) =
    Lean.Grind.CommRing.Poly.denote ctx acc +
      Lean.Grind.CommRing.Poly.denote ctx p₁ * Lean.Grind.CommRing.Poly.denote ctx p₂
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
MultipliableLocallyUniformlyOn.hasProdLocallyUniformlyOn : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {s : Set β}
  [inst_1 : UniformSpace α] [inst_2 : TopologicalSpace β],
  MultipliableLocallyUniformlyOn f s → HasProdLocallyUniformlyOn f (fun x => ∏' (i : ι), f i x) s
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.toPoly'.go.eq_7 : ∀ (coeff : ℤ) (a : Lean.Grind.Linarith.Expr),
  Lean.Grind.Linarith.Expr.toPoly'.go coeff a.neg = Lean.Grind.Linarith.Expr.toPoly'.go (-coeff) a
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded function and `x : R` is
multiplicative for `f`, then `seminormFromBounded' f x = f x`.  -/
seminormFromBounded_of_mul_apply : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ},
  0 ≤ f →
    (∀ (x y : R), f (x * y) ≤ c * f x * f y) →
      ∀ {x : R}, (∀ (y : R), f (x * y) = f x * f y) → seminormFromBounded' f x = f x
-- Mathlib.Analysis.Distribution.SchwartzSpace.Basic
SchwartzMap.smulLeftCLM_ofReal : ∀ {E : Type u_5} {F : Type u_6} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F]
  [inst_3 : NormedSpace ℝ F] (𝕜' : Type u_10) [inst_4 : RCLike 𝕜'] [inst_5 : NormedSpace 𝕜' F] {g : E → ℝ},
  Function.HasTemperateGrowth g →
    ∀ (f : SchwartzMap E F), (SchwartzMap.smulLeftCLM F fun x => ↑(g x)) f = (SchwartzMap.smulLeftCLM F g) f
-- Batteries.Recycling.RBTree.Basic
/-- The well-formedness invariant for a red-black tree. The first constructor is the real invariant,
and the others allow us to "cheat" in this file and define `insert` and `erase`,
which have more complex proofs that are delayed to `RBTree.Lemmas`.
 -/
RBTree.RBNode.WF : {α : Type u_1} → (α → α → Ordering) → RBTree.RBNode α → Prop
-- Mathlib.CategoryTheory.Limits.Preserves.Creates.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` creates limits of shape `Jᵒᵖ`, then `F : C ⥤ Dᵒᵖ` creates colimits
of shape `J`.  -/
CategoryTheory.Limits.createsColimitsOfShapeOfLeftOp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (J : Type w) →
          [inst_2 : CategoryTheory.Category.{w', w} J] →
            (F : CategoryTheory.Functor C Dᵒᵖ) →
              [CategoryTheory.CreatesLimitsOfShape Jᵒᵖ F.leftOp] → CategoryTheory.CreatesColimitsOfShape J F
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Wequiv.abs : ∀ {F : Type u → Type v} [q : QPF F] (a : (QPF.P F).A) (f : (QPF.P F).B a → (QPF.P F).W) (a' : (QPF.P F).A)
  (f' : (QPF.P F).B a' → (QPF.P F).W), QPF.abs ⟨a, f⟩ = QPF.abs ⟨a', f'⟩ → QPF.Wequiv (WType.mk a f) (WType.mk a' f')
-- Lean.Parser.Types
Lean.Parser.Error.mk.sizeOf_spec : ∀ (unexpectedTk : Lean.Syntax) (unexpected : String) (expected : List String),
  sizeOf { unexpectedTk := unexpectedTk, unexpected := unexpected, expected := expected } =
    1 + sizeOf unexpectedTk + sizeOf unexpected + sizeOf expected
-- Mathlib.Topology.NhdsSet
nhdsSet_interior : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X}, nhdsSet (interior s) = Filter.principal (interior s)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.getLTD_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k fallback : α},
  t₁.Equiv t₂ → t₁.getLTD k fallback = t₂.getLTD k fallback
-- Mathlib.Analysis.Convolution
HasCompactSupport.convolution_integrand_bound_right : ∀ {𝕜 : Type u𝕜} {G : Type uG} {E : Type uE} {E' : Type uE'} {F : Type uF} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup E'] [inst_2 : NormedAddCommGroup F] {f : G → E} {g : G → E'}
  [inst_3 : NontriviallyNormedField 𝕜] [inst_4 : NormedSpace 𝕜 E] [inst_5 : NormedSpace 𝕜 E'] [inst_6 : NormedSpace 𝕜 F]
  (L : E →L[𝕜] E' →L[𝕜] F) [inst_7 : AddGroup G] [inst_8 : TopologicalSpace G],
  HasCompactSupport g →
    Continuous g →
      ∀ {x t : G} {s : Set G},
        x ∈ s → ‖(L (f t)) (g (x - t))‖ ≤ (-tsupport g + s).indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i, ‖g i‖) t
-- Std.Http.Data.URI.Basic
/-- Removes dot segments from the path according to RFC 3986 Section 5.2.4. This handles "."
(current directory) and ".." (parent directory) segments.
 -/
Std.Http.URI.Path.normalize : Std.Http.URI.Path → Std.Http.URI.Path
-- Lean.Elab.InfoTree.Types
Lean.Elab.CompletionInfo.fieldId.injEq : ∀ (stx : Lean.Syntax) (id : Option Lean.Name) (lctx : Lean.LocalContext) (structName : Lean.Name) (stx_1 : Lean.Syntax)
  (id_1 : Option Lean.Name) (lctx_1 : Lean.LocalContext) (structName_1 : Lean.Name),
  (Lean.Elab.CompletionInfo.fieldId stx id lctx structName =
      Lean.Elab.CompletionInfo.fieldId stx_1 id_1 lctx_1 structName_1) =
    (stx = stx_1 ∧ id = id_1 ∧ lctx = lctx_1 ∧ structName = structName_1)
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.OmissionReason.string.sizeOf_spec : ∀ (s : String), sizeOf (Lean.PrettyPrinter.Delaborator.OmissionReason.string s) = 1 + sizeOf s
-- Mathlib.Algebra.Order.Interval.Set.Instances
Set.Icc.coe_nonneg : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : PartialOrder R] (x : ↑(Set.Icc 0 1)), 0 ≤ ↑x
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.AEMeasurable
MeasureTheory.ae_eq_trim_iff_of_aestronglyMeasurable : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] [TopologicalSpace.MetrizableSpace β]
  {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f g : α → β} (hm : m ≤ m0)
  (hfm : MeasureTheory.AEStronglyMeasurable f μ) (hgm : MeasureTheory.AEStronglyMeasurable g μ),
  MeasureTheory.AEStronglyMeasurable.mk f hfm =ᵐ[μ.trim hm] MeasureTheory.AEStronglyMeasurable.mk g hgm ↔ f =ᵐ[μ] g
-- Lean.Meta.AppBuilder
/-- Returns `a ≍ b`.  -/
Lean.Meta.mkHEq : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.Matrix.Basis
Matrix.single_apply_of_col_ne : ∀ {m : Type u_2} {n : Type u_3} {α : Type u_7} [inst : DecidableEq m] [inst_1 : DecidableEq n] [inst_2 : Zero α]
  (i i' : m) {j j' : n}, j ≠ j' → ∀ (a : α), Matrix.single i j a i' j' = 0
-- Mathlib.Topology.Irreducible
isPreirreducible_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] {x : X}, IsPreirreducible {x}
-- Mathlib.Tactic.GRewrite.Core
/-- The key used to determine where to attempt rewriting.  -/
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.GRewriteLemma.index : Mathlib.Tactic.GRewrite.GRewriteLemma✝ → Lean.HeadIndex × ℕ
-- Init.Data.String.OrderInstances
String.Pos.instTransLe : {s : String} → Trans (fun x1 x2 => x1 ≤ x2) (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2
-- Mathlib.Geometry.Manifold.Instances.Sphere
continuousOn_stereoToFun : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] {v : E},
  ContinuousOn (stereoToFun v) {x | ((innerSL ℝ) v) x ≠ 1}
-- Mathlib.LinearAlgebra.Finsupp.LSum
/-- If `M` and `N` are submodules of an `R`-algebra `S`, `n : ι → N` is a family of elements, then
there is an `R`-linear map from `ι →₀ M` to `S` which maps `{ m_i }` to the sum of `m_i * n_i`.
This is used in the definition of linearly disjointness.  -/
Submodule.mulRightMap : {R : Type u_1} →
  [inst : Semiring R] →
    {S : Type u_4} →
      [inst_1 : Semiring S] →
        [inst_2 : Module R S] →
          [SMulCommClass R R S] →
            [IsScalarTower R S S] →
              (M : Submodule R S) → {N : Submodule R S} → {ι : Type u_5} → (ι → ↥N) → (ι →₀ ↥M) →ₗ[R] S
-- Mathlib.CategoryTheory.Monoidal.Closed.InternalCurrying
CategoryTheory.MonoidalClosed.uncurry_ihomUncurry : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x y z : C)
  [inst_2 : CategoryTheory.Closed x] [inst_3 : CategoryTheory.Closed y]
  [inst_4 : CategoryTheory.Closed (CategoryTheory.MonoidalCategoryStruct.tensorObj x y)],
  CategoryTheory.MonoidalClosed.uncurry (CategoryTheory.MonoidalClosed.ihomUncurry x y z) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator x y (y ⟹ x ⟹ z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft x ((CategoryTheory.ihom.ev y).app (x ⟹ z)))
        ((CategoryTheory.ihom.ev x).app z))
-- Mathlib.CategoryTheory.Adjunction.Lifting.Right
/-- Construct the right adjoint to `L`, with object map `constructRightAdjointObj`.  -/
CategoryTheory.LiftRightAdjoint.constructRightAdjoint : {A : Type u₁} →
  {B : Type u₂} →
    {C : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} A] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} C] →
            {U : CategoryTheory.Functor A B} →
              {F : CategoryTheory.Functor B A} →
                (L : CategoryTheory.Functor C B) →
                  (U' : CategoryTheory.Functor A C) →
                    (adj₁ : F ⊣ U) →
                      (L.comp F ⊣ U') →
                        [CategoryTheory.Limits.HasCoreflexiveEqualizers C] →
                          ((X : B) → CategoryTheory.RegularMono (adj₁.unit.app X)) → CategoryTheory.Functor B C
-- Lean.Data.Trie
/-- The empty `Trie`  -/
Lean.Data.Trie.empty : {α : Type} → Lean.Data.Trie α
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
/-- Attempts to verify that `c` can be added to `f` via unit propagation. If it can, it returns
`((f.insert c), true)`. If it can't, it returns false as the second part of the tuple
(and no guarantees are made about what formula is returned).
 -/
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.performRatAdd : {n : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n →
    Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n →
      Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n) →
        Array ℕ → Array (ℕ × Array ℕ) → Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula n × Bool
-- Mathlib.GroupTheory.Torsion
/-- Torsion additive submonoids are torsion.  -/
AddCommMonoid.addTorsion.isAddTorsion : ∀ {G : Type u_1} [inst : AddCommMonoid G], IsAddTorsion ↥(AddCommMonoid.addTorsion G)
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.AssociatorBimod.hom_inv_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasCoequalizers C]
  [inst_3 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorLeft X)]
  [inst_4 :
    ∀ (X : C),
      CategoryTheory.Limits.PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁}
        (CategoryTheory.MonoidalCategory.tensorRight X)]
  {R S T U : CategoryTheory.Mon C} (P : Bimod R S) (Q : Bimod S T) (L : Bimod T U),
  CategoryTheory.CategoryStruct.comp (Bimod.AssociatorBimod.hom P Q L) (Bimod.AssociatorBimod.inv P Q L) =
    CategoryTheory.CategoryStruct.id ((P.tensorBimod Q).tensorBimod L).X
-- Mathlib.CategoryTheory.ObjectProperty.InheritedFromHom
CategoryTheory.ObjectProperty.InheritedFromSource.instMin : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P P' : CategoryTheory.ObjectProperty C)
  (Q : CategoryTheory.MorphismProperty C) [P.InheritedFromSource Q] [P'.InheritedFromSource Q],
  (P ⊓ P').InheritedFromSource Q
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.snd_comp_quotientInfEquivQuotientProd : ∀ {R : Type u_2} [inst : CommRing R] (I J : Ideal R) (coprime : IsCoprime I J),
  (RingHom.snd (R ⧸ I) (R ⧸ J)).comp ↑(I.quotientInfEquivQuotientProd J coprime) = Ideal.Quotient.factor ⋯
-- Init.Data.Vector.Basic
/-- Set an element in a vector using a `Nat` index, with a tactic provided proof that the index is in
bounds.

This will perform the update destructively provided that the vector has a reference count of 1.
 -/
Vector.set : {α : Type u_1} → {n : ℕ} → Vector α n → (i : ℕ) → α → autoParam (i < n) Vector.set._auto_1 → Vector α n
-- Mathlib.Algebra.Ring.Subsemiring.Basic
Subsemiring.mem_centralizer_iff : ∀ {R : Type u_1} [inst : Semiring R] {s : Set R} {z : R}, z ∈ Subsemiring.centralizer s ↔ ∀ g ∈ s, g * z = z * g
-- Mathlib.CategoryTheory.Category.ReflQuiv
CategoryTheory.Cat.freeRefl_map : ∀ {X Y : CategoryTheory.ReflQuiv} (F : X ⟶ Y),
  CategoryTheory.Cat.freeRefl.map F = (CategoryTheory.Cat.freeReflMap F).toCatHom
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_append_extractLsb' : ∀ {w len : ℕ} {x : BitVec (w + len)}, BitVec.extractLsb' len w x ++ BitVec.extractLsb' 0 len x = x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue?_insertEntry : ∀ {α : Type u} {β : Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β},
  Std.Internal.List.getValue? a (Std.Internal.List.insertEntry k v l) =
    if (k == a) = true then some v else Std.Internal.List.getValue? a l
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.equivalenceLeftFractionRel : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C)
  [W.HasLeftCalculusOfFractions] (X Y : C), Equivalence CategoryTheory.MorphismProperty.LeftFractionRel
-- Mathlib.Order.Hom.CompleteLattice
sSupHom.instSSupHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : SupSet α] [inst_1 : SupSet β], sSupHomClass (sSupHom α β) α β
-- Mathlib.Data.DFinsupp.Lex
/-- The less-or-equal relation for the colexicographic ordering is decidable.  -/
DFinsupp.Colex.decidableLE : {ι : Type u_1} →
  {α : ι → Type u_2} →
    [inst : (i : ι) → Zero (α i)] →
      [inst_1 : LinearOrder ι] → [inst_2 : (i : ι) → LinearOrder (α i)] → DecidableLE (Colex (Π₀ (i : ι), α i))
-- Mathlib.Analysis.Fourier.FourierTransform
/-- The uniform norm of the Fourier integral of `f` is bounded by the `L¹` norm of `f`.  -/
VectorFourier.norm_fourierIntegral_le_integral_norm : ∀ {𝕜 : Type u_1} [inst : CommRing 𝕜] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : MeasurableSpace V] {W : Type u_3} [inst_4 : AddCommGroup W] [inst_5 : Module 𝕜 W] {E : Type u_4}
  [inst_6 : NormedAddCommGroup E] [inst_7 : NormedSpace ℂ E] (e : AddChar 𝕜 Circle) (μ : MeasureTheory.Measure V)
  (L : V →ₗ[𝕜] W →ₗ[𝕜] 𝕜) (f : V → E) (w : W), ‖VectorFourier.fourierIntegral e μ L f w‖ ≤ ∫ (v : V), ‖f v‖ ∂μ
-- Mathlib.Algebra.Order.Interval.Basic
instInvInterval : {α : Type u_2} → [inst : CommGroup α] → [inst_1 : PartialOrder α] → [IsOrderedMonoid α] → Inv (Interval α)
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.Quotient.algebraMap_quotient_of_ramificationIdx_neZero : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] (p : Ideal R) (P : Ideal S)
  [inst_3 : NeZero (p.ramificationIdx' P)] (x : R),
  (algebraMap (R ⧸ p) (S ⧸ P)) ((Ideal.Quotient.mk p) x) = (Ideal.Quotient.mk P) ((algebraMap R S) x)
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_iff_exists : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.containsKey a l = true ↔ ∃ a' ∈ Std.Internal.List.keys l, (a == a') = true
-- Mathlib.LinearAlgebra.QuadraticForm.QuadraticModuleCat.Monoidal
/-- Auxiliary definition used to build `QuadraticModuleCat.instMonoidalCategory`.

We want this up front so that we can re-use it to define `whiskerLeft` and `whiskerRight`.  -/
QuadraticModuleCat.instMonoidalCategory.tensorHom : {R : Type u} →
  [inst : CommRing R] →
    [inst_1 : Invertible 2] →
      {W X Y Z : QuadraticModuleCat R} →
        (W ⟶ X) →
          (Y ⟶ Z) →
            (QuadraticModuleCat.instMonoidalCategory.tensorObj W Y ⟶
              QuadraticModuleCat.instMonoidalCategory.tensorObj X Z)
-- Mathlib.CategoryTheory.Sites.EqualizerSheafCondition
CategoryTheory.Equalizer.Sieve.SecondObj.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.Functor Cᵒᵖ (Type (max v u))} {X : C}
  {S : CategoryTheory.Sieve X} (z₁ z₂ : CategoryTheory.Equalizer.Sieve.SecondObj P S),
  (∀ (Y Z : C) (g : Z ⟶ Y) (f : Y ⟶ X) (hf : S.arrows f),
      (CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
          z₁ =
        (CategoryTheory.ConcreteCategory.hom
            (CategoryTheory.Limits.Pi.π (fun f => P.obj (Opposite.op f.snd.fst)) ⟨Y, ⟨Z, ⟨g, ⟨f, hf⟩⟩⟩⟩))
          z₂) →
    z₁ = z₂
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rcc.isSome_succMany?_of_lt_length_toList : ∀ {α : Type u} {r : Std.Rcc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α] {i : ℕ}, i < r.toList.length → (Std.PRange.succMany? i r.lower).isSome = true
-- Mathlib.RingTheory.OrderOfVanishing.Basic
/-- The map `R ⧸ I →ₗ[R] R ⧸ (a • I)` defined by multiplication by `a`
 -/
Ideal.mulQuot : {R : Type u_1} → [inst : CommRing R] → (a : R) → (I : Ideal R) → R ⧸ I →ₗ[R] R ⧸ a • I
-- Mathlib.Order.Filter.Lift
Filter.comap_lift_eq : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set α → Filter β} {m : γ → β},
  Filter.comap m (f.lift g) = f.lift (Filter.comap m ∘ g)
-- Mathlib.Order.Filter.FilterProduct
Filter.Germ.const_lt_iff : ∀ {α : Type u} {β : Type v} {φ : Ultrafilter α} [inst : Preorder β] {x y : β}, ↑x < ↑y ↔ x < y
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Comonad.ForgetCreatesLimits'.newCone_pt : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u} [inst_1 : CategoryTheory.Category.{v, u} J]
  {T : CategoryTheory.Comonad C} {D : CategoryTheory.Functor J T.Coalgebra}
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)), (CategoryTheory.Comonad.ForgetCreatesLimits'.newCone c).pt = c.pt
-- Init.Grind.Module.NatModuleNorm
Lean.Grind.Linarith.Poly.NonnegCoeffs.brecOn : ∀ {motive : (a : Lean.Grind.Linarith.Poly) → a.NonnegCoeffs → Prop} {a : Lean.Grind.Linarith.Poly} (t : a.NonnegCoeffs),
  (∀ (a : Lean.Grind.Linarith.Poly) (t : a.NonnegCoeffs), Lean.Grind.Linarith.Poly.NonnegCoeffs.below t → motive a t) →
    motive a t
-- Mathlib.Analysis.Asymptotics.TVS
ContinuousLinearMap.isBigOTVS_fun_comp : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} (g : E →L[𝕜] F),
  (fun x => g (f x)) =O[𝕜; l] f
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.lintegral_prod_mul : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  {ν : MeasureTheory.Measure β} [MeasureTheory.SFinite ν] {f : α → ENNReal} {g : β → ENNReal},
  AEMeasurable f μ →
    AEMeasurable g ν → ∫⁻ (z : α × β), f z.1 * g z.2 ∂μ.prod ν = (∫⁻ (x : α), f x ∂μ) * ∫⁻ (y : β), g y ∂ν
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigO_const_mul_self : ∀ {α : Type u_1} {R : Type u_13} [inst : SeminormedRing R] (c : R) (f : α → R) (l : Filter α),
  (fun x => c * f x) =O[l] f
-- Init.Data.Nat.Internal.SOM
Nat.Internal.SOM.Expr.num : ℕ → Nat.Internal.SOM.Expr
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Lax
CategoryTheory.Lax.LaxTrans.LaxFunctor.bicategory_associator_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.LaxFunctor B C} (x_3 : CategoryTheory.LaxFunctor B C) (η : x ⟶ x_1) (θ : x_1 ⟶ x_2)
  (ι : x_2 ⟶ x_3) (a : B),
  (CategoryTheory.Bicategory.associator η θ ι).inv.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- Two vertices are adjacent in the complete bipartite graph on two vertex types
if and only if they are not from the same side.
Any bipartite graph may be regarded as a subgraph of one of these.  -/
completeBipartiteGraph : (V : Type u_1) → (W : Type u_2) → SimpleGraph (V ⊕ W)
-- Init.Data.Int.Order
Int.neg_add_le_right_of_le_add : ∀ {a b c : ℤ}, a ≤ b + c → -c + a ≤ b
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.hom_inv_whiskerRight_whiskerRight_assoc : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {f g : a ⟶ b} (η : f ≅ g) (h : b ⟶ c) (k : c ⟶ d)
  {Z : a ⟶ d} (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f h) k ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η.hom h) k)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight η.inv h) k) h_1) =
    h_1
-- Init.Data.Option.Monadic
_private.Init.Data.Option.Monadic.0.Option.instForIn'InferInstanceMembershipOfMonad.match_1.splitter : {β : Type u_1} →
  (motive : ForInStep β → Sort u_2) →
    (__do_lift : ForInStep β) →
      ((r : β) → motive (ForInStep.done r)) → ((r : β) → motive (ForInStep.yield r)) → motive __do_lift
-- Mathlib.Analysis.Convex.Combination
Finset.convexHull_eq : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] (s : Finset E),
  (convexHull R) ↑s = {x | ∃ w, (∀ y ∈ s, 0 ≤ w y) ∧ ∑ y ∈ s, w y = 1 ∧ s.centerMass w id = x}
-- Mathlib.Tactic.NormNum.Irrational
Mathlib.Meta.NormNum.NotPowerCertificate.mk.injEq : ∀ {m n : Q(ℕ)} (k : Q(ℕ)) (pf_left : Q(«$k» ^ «$n» < «$m»)) (pf_right : Q(«$m» < («$k» + 1) ^ «$n»)) (k_1 : Q(ℕ))
  (pf_left_1 : Q(«$k_1» ^ «$n» < «$m»)) (pf_right_1 : Q(«$m» < («$k_1» + 1) ^ «$n»)),
  ({ k := k, pf_left := pf_left, pf_right := pf_right } = { k := k_1, pf_left := pf_left_1, pf_right := pf_right_1 }) =
    (k = k_1 ∧ pf_left = pf_left_1 ∧ pf_right = pf_right_1)
-- Mathlib.Tactic.IntervalCases
Mathlib.Tactic.IntervalCases.Bound.lt.injEq : ∀ (n n_1 : ℤ), (Mathlib.Tactic.IntervalCases.Bound.lt n = Mathlib.Tactic.IntervalCases.Bound.lt n_1) = (n = n_1)
-- Mathlib.LinearAlgebra.Projection
Submodule.prodEquivOfIsCompl_symm_apply_right : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] (p q : Submodule R E)
  (h : IsCompl p q) (x : ↥q), (p.prodEquivOfIsCompl q h).symm ↑x = (0, x)
-- Mathlib.Data.Set.Sigma
biInf_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {β : Type u_4} [inst : CompleteLattice β] (s : Set ι) (t : (i : ι) → Set (α i))
  (f : Sigma α → β), ⨅ ij ∈ s.sigma t, f ij = ⨅ i ∈ s, ⨅ j ∈ t i, f ⟨i, j⟩
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.setTag.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {fvarId : Lean.FVarId} {cidx : ℕ} {k : Lean.Compiler.LCNF.Code pu}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_13} {fvarId_1 : Lean.FVarId}
  {cidx_1 : ℕ} {k_1 : Lean.Compiler.LCNF.Code pu}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_13},
  Lean.Compiler.LCNF.Code.setTag fvarId cidx k h = Lean.Compiler.LCNF.Code.setTag fvarId_1 cidx_1 k_1 h_1 →
    fvarId = fvarId_1 ∧ cidx = cidx_1 ∧ k = k_1
-- Mathlib.Algebra.Group.WithOne.Defs
WithZero.instCoeTC.eq_1 : ∀ {α : Type u}, WithZero.instCoeTC = { coe := WithZero.coe }
-- Mathlib.Topology.CompactOpen
ContinuousMap.mem_nhds_iff : ∀ {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : C(X, Y)}
  {s : Set C(X, Y)},
  s ∈ nhds f ↔
    ∃ S,
      S.Finite ∧
        (∀ (K : Set X) (U : Set Y), (K, U) ∈ S → IsCompact K ∧ IsOpen U ∧ Set.MapsTo (⇑f) K U) ∧
          {g | ∀ (K : Set X) (U : Set Y), (K, U) ∈ S → Set.MapsTo (⇑g) K U} ⊆ s
-- Mathlib.Algebra.Order.Field.Basic
/-- An inequality involving `2`.  -/
sub_one_div_inv_le_two : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a : α},
  2 ≤ a → (1 - 1 / a)⁻¹ ≤ 2