mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeSet.Raw.Basic
/-- Returns the `n`-th smallest element, or `fallback` if `n` is at least `t.size`.  -/
Std.TreeSet.Raw.atIdxD : {α : Type u} → {cmp : α → α → Ordering} → Std.TreeSet.Raw α cmp → ℕ → α → α
-- Mathlib.CategoryTheory.Limits.Constructions.Over.Basic
/-- Make sure we can derive equalizers in `Over B`.  -/
CategoryTheory.Over.instHasEqualizers : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {B : C} [CategoryTheory.Limits.HasEqualizers C],
  CategoryTheory.Limits.HasEqualizers (CategoryTheory.Over B)
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.vle_mul_comm : ∀ {R : Type u_1} {inst : Semiring R} [self : ValuativeRel R] {x y : R}, x * y ≤ᵥ y * x
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
OrderDual.instSMulZeroClass_1 : {G₀ : Type u_1} → {M₀ : Type u_2} → [inst : Zero M₀] → [SMulZeroClass G₀ M₀] → SMulZeroClass G₀ M₀ᵒᵈ
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
_private.Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas.0.Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.deleteOne.match_1.splitter : {n : ℕ} →
  (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) → Sort u_1) →
    (x : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n)) →
      (Unit → motive none) →
        ((l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
            (nodupkey : ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l]) →
              (nodup : [l].Nodup) → motive (some { clause := [l], nodupkey := nodupkey, nodup := nodup })) →
          ((val : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
              (∀ (l : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n))
                  (nodupkey :
                    ∀ (l_1 : Std.Tactic.BVDecide.LRAT.Internal.PosFin n), (l_1, true) ∉ [l] ∨ (l_1, false) ∉ [l])
                  (nodup : [l].Nodup), val = { clause := [l], nodupkey := nodupkey, nodup := nodup } → False) →
                motive (some val)) →
            motive x
-- Mathlib.NumberTheory.Dioph
IsPoly.brecOn : ∀ {α : Type u_1} {motive : (a : (α → ℕ) → ℤ) → IsPoly a → Prop} {a : (α → ℕ) → ℤ} (t : IsPoly a),
  (∀ (a : (α → ℕ) → ℤ) (t : IsPoly a), IsPoly.below t → motive a t) → motive a t
-- Mathlib.RingTheory.Lasker
/-- **Alias** of `Submodule.decomposition_erase_inf`. -/
Ideal.decomposition_erase_inf : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {N : Submodule R M} {s : Finset (Submodule R M)},
  s.inf id = N → ∃ t ⊆ s, t.inf id = N ∧ ∀ ⦃J : Submodule R M⦄, J ∈ t → ¬(t.erase J).inf id ≤ J
-- Mathlib.Analysis.RCLike.TangentCone
/-- In a real or complex vector space, a convex set with nonempty interior is a set of unique
differentiability.  -/
uniqueDiffWithinAt_convex_of_isRCLikeNormedField : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [h𝕜 : IsRCLikeNormedField 𝕜] {E : Type u_2}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedSpace ℝ E] {s : Set E} {x : E},
  Convex ℝ s → (interior s).Nonempty → x ∈ closure s → UniqueDiffWithinAt 𝕜 s x
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.HasPushouts.hasPushout : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {P : CategoryTheory.MorphismProperty C} [self : P.HasPushouts]
  {X Y S : C} {f : S ⟶ X} (g : S ⟶ Y), P f → CategoryTheory.Limits.HasPushout f g
-- Std.Sync.Broadcast
_private.Std.Sync.Broadcast.0.Std.Broadcast.mk.inj : ∀ {α : Type} {inner inner_1 : Std.Bounded✝ α}, { inner := inner } = { inner := inner_1 } → inner = inner_1
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.singularValues.congr_simp : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T T_1 : E →ₗ[𝕜] F), T = T_1 → T.singularValues = T_1.singularValues
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
/-- The homology class map from cycles to the homology of a homological complex.  -/
HomologicalComplex.homologyπ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          (K : HomologicalComplex C c) → (i : ι) → [inst_2 : K.HasHomology i] → K.cycles i ⟶ K.homology i
-- Mathlib.RingTheory.FinitePresentation
AlgHom.FinitePresentation.of_surjective : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A →ₐ[R] B),
  Function.Surjective ⇑f → (RingHom.ker f.toRingHom).FG → f.FinitePresentation
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.setTR.go.match_1.splitter : {α : Type u_1} →
  (motive : List α → ℕ → Array α → Sort u_2) →
    (x : List α) →
      (x_1 : ℕ) →
        (x_2 : Array α) →
          ((x : ℕ) → (x_3 : Array α) → motive [] x x_3) →
            ((head : α) → (xs : List α) → (acc : Array α) → motive (head :: xs) 0 acc) →
              ((x : α) → (xs : List α) → (n : ℕ) → (acc : Array α) → motive (x :: xs) n.succ acc) → motive x x_1 x_2
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL1
MeasureTheory.condExpIndL1Fin_disjoint_union : ∀ {α : Type u_1} {G : Type u_4} [inst : NormedAddCommGroup G] {m m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {s t : Set α} [inst_1 : NormedSpace ℝ G] {hm : m ≤ m0} [inst_2 : MeasureTheory.SigmaFinite (μ.trim hm)]
  (hs : MeasurableSet s) (ht : MeasurableSet t) (hμs : μ s ≠ ⊤) (hμt : μ t ≠ ⊤),
  Disjoint s t →
    ∀ (x : G),
      MeasureTheory.condExpIndL1Fin hm ⋯ ⋯ x =
        MeasureTheory.condExpIndL1Fin hm hs hμs x + MeasureTheory.condExpIndL1Fin hm ht hμt x
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.IsLittleO.right_isBigO_add' : ∀ {α : Type u_1} {E' : Type u_6} [inst : SeminormedAddCommGroup E'] {l : Filter α} {f₁ f₂ : α → E'},
  f₁ =o[l] f₂ → f₂ =O[l] (f₂ + f₁)
-- Mathlib.Analysis.Complex.HasPrimitives
_private.Mathlib.Analysis.Complex.HasPrimitives.0.Complex.mem_ball_of_map_re_aux : ∀ {c : ℂ} {r a₁ a₂ b : ℝ},
  ↑a₁ + ↑b * Complex.I ∈ Metric.ball c r →
    ↑a₂ + ↑b * Complex.I ∈ Metric.ball c r → (fun x => ↑x + ↑b * Complex.I) '' Set.uIcc a₁ a₂ ⊆ Metric.ball c r
-- Lean.Compiler.NameMangling
_private.Lean.Compiler.NameMangling.0.Lean.Name.demangleAux.nameStart.eq_def : ∀ (s : String) (p : s.Pos) (res : Lean.Name),
  Lean.Name.demangleAux.nameStart✝ s p res =
    if h : p = s.endPos then res
    else
      let ch := p.get h;
      let p_1 := p.next h;
      if ch.isDigit = true then
        if h_1 : ch = '0' ∧ ∃ (h : p_1 ≠ s.endPos), p_1.get h = '0' then Lean.Name.demangleAux✝ s (p_1.next ⋯) res "" 0
        else Lean.Name.demangleAux.decodeNum✝ s p_1 res (ch.val - 48).toNat
      else
        if ch = '_' then Lean.Name.demangleAux✝ s p_1 res "" 1
        else Lean.Name.demangleAux✝ s p_1 res (String.singleton ch) 0
-- Mathlib.Logic.Embedding.Basic
Equiv.embeddingCongr_refl : ∀ {α : Sort u_1} {β : Sort u_2}, (Equiv.refl α).embeddingCongr (Equiv.refl β) = Equiv.refl (α ↪ β)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- `φ`-equivariant functions `X → Y`,
where `φ : M → N`, where `M` and `N` act on `X` and `Y` respectively.  -/
«MulActionHomLocal≺» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsComp'App_inv_apply : ∀ {R₁ : Type u₁} {R₂ : Type u₂} {R₃ : Type u₃} [inst : Ring R₁] [inst_1 : Ring R₂] [inst_2 : Ring R₃] (f : R₁ →+* R₂)
  (g : R₂ →+* R₃) (gf : R₁ →+* R₃) (hgf : gf = g.comp f) (M : ModuleCat R₃) (x : ↑M),
  (CategoryTheory.ConcreteCategory.hom (ModuleCat.restrictScalarsComp'App f g gf hgf M).inv) x = x
-- Mathlib.Analysis.Normed.Ring.Basic
Real.iSup_prod_eq_prod_iSup_of_nonnegHomClass : ∀ {α : Type u_5} {R : Type u_6} [inst : Fintype α] {ι : α → Type u} [∀ (a : α), Finite (ι a)] {F : Type u_7}
  [inst_2 : FunLike F R ℝ] [NonnegHomClass F R ℝ] (v : F) {x : (a : α) → ι a → R},
  ⨆ i, ∏ a, v (x a (i a)) = ∏ a, ⨆ i, v (x a i)
-- Mathlib.Analysis.InnerProductSpace.NormDet
/-- Using Hausdorff measure with the domain dimension, the volume of the image is scaled by
`LinearMap.normDet`.
 -/
LinearMap.hausdorffMeasure_image : ∀ {U : Type u_5} {V : Type u_6} [inst : NormedAddCommGroup U] [inst_1 : InnerProductSpace ℝ U]
  [inst_2 : FiniteDimensional ℝ U] [inst_3 : NormedAddCommGroup V] [inst_4 : InnerProductSpace ℝ V]
  [inst_5 : MeasurableSpace U] [inst_6 : BorelSpace U] [inst_7 : MeasurableSpace V] [inst_8 : BorelSpace V]
  (f : U →ₗ[ℝ] V) (s : Set U),
  (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ U)) (⇑f '' s) =
    ENNReal.ofReal f.normDet * (MeasureTheory.Measure.hausdorffMeasure ↑(Module.finrank ℝ U)) s
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_top : ⊤.log = ⊤
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.ParentSet.mk.sizeOf_spec : ∀ (parents : List Lean.Expr), sizeOf { parents := parents } = 1 + sizeOf parents
-- Init.Data.BitVec.Lemmas
BitVec.toInt_ofInt : ∀ {n : ℕ} (i : ℤ), (BitVec.ofInt n i).toInt = i.bmod (2 ^ n)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_desc_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {β : Type w} {f : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] {P : C} (p : (b : β) → f b ⟶ P) (b : β) {Z : C} (h : P ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.desc p) h) =
    CategoryTheory.CategoryStruct.comp (p b) h
-- Mathlib.LinearAlgebra.Dimension.Finite
Submodule.finrank_eq_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsDomain R]
  [Module.IsTorsionFree R M] [StrongRankCondition R] {S : Submodule R M} [Module.Finite R ↥S],
  Module.finrank R ↥S = 0 ↔ S = ⊥
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.norm_setToL1_le_norm_setToL1SCLM : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T : Set α → E →L[ℝ] F} {C : ℝ} (hT : MeasureTheory.DominatedFinMeasAdditive μ T C),
  ‖MeasureTheory.L1.setToL1 hT‖ ≤ ‖MeasureTheory.L1.SimpleFunc.setToL1SCLM α E μ hT‖
-- Batteries.Data.UInt
UInt32.toUInt16_toNat : ∀ (x : UInt32), x.toUInt16.toNat = x.toNat % 2 ^ 16
-- Mathlib.RepresentationTheory.Rep.Basic
Rep.instMonoidalClosed : {k : Type u} →
  [inst : CommRing k] → {G : Type v} → [inst_1 : Group G] → CategoryTheory.MonoidalClosed (Rep.{u, u, v} k G)
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.linearEquiv_apply : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} {M'' : Type u_4}
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M'] [inst_3 : AddCommMonoid M''] [inst_4 : Module R M]
  [inst_5 : Module R M'] [inst_6 : Module R M''] (f : M →ₗ[R] M') (g : M →ₗ[R] M'') [inst_7 : IsLocalizedModule S f]
  [inst_8 : IsLocalizedModule S g] (x : M), (IsLocalizedModule.linearEquiv S f g) (f x) = g x
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
OpenPartialHomeomorph.eventually_nhds' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) {x : X} (p : X → Prop),
  x ∈ e.source → ((∀ᶠ (y : Y) in nhds (↑e x), p (↑e.symm y)) ↔ ∀ᶠ (x : X) in nhds x, p x)
-- Init.Data.List.Sublist
List.prefix_append_inj_of_length_eq : ∀ {α : Type u_1} {l₁ l₂ s₁ s₂ : List α}, s₁.length = s₂.length → (s₁ ++ l₁ <+: s₂ ++ l₂ ↔ s₁ = s₂ ∧ l₁ <+: l₂)
-- Mathlib.Algebra.GroupWithZero.Basic
div_mul_eq_mul_div₀ : ∀ {G₀ : Type u_2} [inst : CommGroupWithZero G₀] (a b c : G₀), a / c * b = a * b / c
-- Lean.Environment
Lean.Kernel.Exception.deterministicTimeout : Lean.Kernel.Exception
-- Aesop.Search.Expansion
Aesop.SafeRuleResult.postponed.injEq : ∀ (result result_1 : Aesop.PostponedSafeRule),
  (Aesop.SafeRuleResult.postponed result = Aesop.SafeRuleResult.postponed result_1) = (result = result_1)
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- Thus conjugation defines an equivalence between isomorphisms.  -/
CategoryTheory.Bicategory.conjugateIsoEquiv : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {c d : B} →
      {l₁ l₂ : c ⟶ d} →
        {r₁ r₂ : d ⟶ c} →
          CategoryTheory.Bicategory.Adjunction l₁ r₁ →
            CategoryTheory.Bicategory.Adjunction l₂ r₂ → (l₂ ≅ l₁) ≃ (r₁ ≅ r₂)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
/-- Type-alias for modifications between lax transformations of lax functors. This is the type
used for the 2-homomorphisms in the bicategory of lax functors equipped with lax
transformations.  -/
CategoryTheory.Lax.LaxTrans.Hom : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} → (F ⟶ G) → (F ⟶ G) → Type (max u₁ w₂)
-- Mathlib.MeasureTheory.Integral.PeakFunction
/-- Consider a nonnegative function `φ` with integral one, decaying quickly enough at infinity.
Then suitable renormalizations of `φ` form a sequence of peak functions around any point:
`∫ (c ^ d * φ (c • (x₀ - x)) • g x` converges to `g x₀` as `c → ∞` if `g` is continuous at `x₀`
and integrable.  -/
tendsto_integral_comp_smul_smul_of_integrable' : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {F : Type u_4}
  [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] [FiniteDimensional ℝ F] [inst_6 : MeasurableSpace F]
  [BorelSpace F] {μ : MeasureTheory.Measure F} [μ.IsAddHaarMeasure] {φ : F → ℝ},
  (∀ (x : F), 0 ≤ φ x) →
    ∫ (x : F), φ x ∂μ = 1 →
      Filter.Tendsto (fun x => ‖x‖ ^ Module.finrank ℝ F * φ x) (Bornology.cobounded F) (nhds 0) →
        ∀ {g : F → E} {x₀ : F},
          MeasureTheory.Integrable g μ →
            ContinuousAt g x₀ →
              Filter.Tendsto (fun c => ∫ (x : F), (c ^ Module.finrank ℝ F * φ (c • (x₀ - x))) • g x ∂μ) Filter.atTop
                (nhds (g x₀))
-- Mathlib.Algebra.Group.Submonoid.Operations
MonoidHom.decidableMemMker.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : MulOneClass M] [inst_1 : MulOneClass N] {F : Type u_4} [inst_2 : FunLike F M N]
  [mc : MonoidHomClass F M N] [inst_3 : DecidableEq N] (f : F) (x : M),
  MonoidHom.decidableMemMker f x = decidable_of_iff (f x = 1) ⋯
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
/-- Lift a `OneHom` to `Finset` via `image`.  -/
Finset.imageOneHom : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : One α] →
        [DecidableEq β] →
          [inst_2 : One β] → [inst_3 : FunLike F α β] → [OneHomClass F α β] → F → OneHom (Finset α) (Finset β)
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PullbackCone.unop_ι_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : Cᵒᵖ} {f : X ⟶ Z} {g : Y ⟶ Z}
  (c : CategoryTheory.Limits.PullbackCone f g) (X_1 : CategoryTheory.Limits.WalkingSpan),
  c.unop.ι.app X_1 =
    CategoryTheory.CategoryStruct.comp
      (match X_1 with
          | none => CategoryTheory.Iso.refl Z
          | some CategoryTheory.Limits.WalkingPair.left => CategoryTheory.Iso.refl X
          | some CategoryTheory.Limits.WalkingPair.right => CategoryTheory.Iso.refl Y).hom.unop
      (c.π.app X_1).unop
-- Mathlib.Geometry.Manifold.LocalInvariantProperties
StructureGroupoid.liftPropWithinAt_univ : ∀ {H : Type u_1} {M : Type u_2} {H' : Type u_3} {M' : Type u_4} [inst : TopologicalSpace H]
  [inst_1 : TopologicalSpace M] [inst_2 : ChartedSpace H M] [inst_3 : TopologicalSpace H']
  [inst_4 : TopologicalSpace M'] [inst_5 : ChartedSpace H' M'] {P : (H → H') → Set H → H → Prop} {g : M → M'} {x : M},
  ChartedSpace.LiftPropWithinAt P g Set.univ x ↔ ChartedSpace.LiftPropAt P g x
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_Icc : ∀ {a b : ℝ}, MeasureTheory.volume (Set.Icc a b) = ENNReal.ofReal (b - a)
-- Init.Conv
/-- `(convs)` runs the `convs` in sequence on the current list of targets.
This is pure grouping with no added effects.  -/
Lean.Parser.Tactic.Conv.paren : Lean.ParserDescr
-- Init.Classical
Classical.epsilon_singleton : ∀ {α : Sort u} (x : α), (Classical.epsilon fun y => y = x) = x
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.existsInv : FirstOrder.Field.FieldAxiom
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.lineMap_vsub_lineMap : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V1] [inst_2 : Module k V1]
  [inst_3 : AddTorsor V1 P1] (p₁ p₂ p₃ p₄ : P1) (c : k),
  (AffineMap.lineMap p₁ p₂) c -ᵥ (AffineMap.lineMap p₃ p₄) c = (AffineMap.lineMap (p₁ -ᵥ p₃) (p₂ -ᵥ p₄)) c
-- Mathlib.Order.DirectedInverseSystem
/-- A partial family of bijections between `F` and `piLT X` defined on some set in `ι`.  -/
InverseSystem.PEquivOn.equiv : {ι : Type u_6} →
  {F : ι → Type u_7} →
    {X : ι → Type u_8} →
      [inst : LinearOrder ι] →
        {f : ⦃i j : ι⦄ → i ≤ j → F j → F i} →
          [inst_1 : SuccOrder ι] →
            {equivSucc : ⦃i : ι⦄ → ¬IsMax i → F (Order.succ i) ≃ F i × X i} →
              {s : Set ι} → InverseSystem.PEquivOn f equivSucc s → (i : ↑s) → F ↑i ≃ InverseSystem.piLT X ↑i
-- Lean.Parser.Do
Lean.Parser.Term.doDebugAssert.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Combinatorics.Additive.PluenneckeRuzsa
/-- **Ruzsa's triangle inequality**. Mul-mulinv-mul version.  -/
Finset.ruzsa_triangle_inequality_mul_mulInv_mul : ∀ {G : Type u_1} [inst : DecidableEq G] [inst_1 : Group G] (A B C : Finset G),
  B.card * (A * C).card ≤ (B * A⁻¹).card * (B * C).card
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_of_injective : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {P : Type u_4} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module S P] [IsNoetherian S P]
  {σ : R →+* S} {σ' : S →+* R} [RingHomInvPair σ σ'] [RingHomInvPair σ' σ] (f : M →ₛₗ[σ] P),
  Function.Injective ⇑f → IsNoetherian R M
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- The multiplicative indicators of closed δ-thickenings of a set tend pointwise to the
multiplicative indicator of the set, as δ tends to zero.  -/
tendsto_mulIndicator_cthickening_mulIndicator_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : One β] [inst_2 : TopologicalSpace β] (f : α → β)
  (E : Set α),
  Filter.Tendsto (fun δ => (Metric.cthickening δ E).mulIndicator f) (nhds 0) (nhds ((closure E).mulIndicator f))
-- Mathlib.CategoryTheory.Distributive.Monoidal
/-- The composite of `(X ◁ coprod.inr) : X ⊗ Z ⟶ X ⊗ (Y ⨿ Z)` and
`(∂L X Y Z).inv :  X ⊗ (Y ⨿ Z) ⟶ (X ⊗ Y) ⨿ (X ⊗ Z)`
is equal to the right coprojection `coprod.inr : X ⊗ Z ⟶ (X ⊗ Y) ⨿ (X ⊗ Z)`.  -/
CategoryTheory.whiskerLeft_coprod_inr_leftDistrib_inv : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] [inst_3 : CategoryTheory.IsMonoidalLeftDistrib C] {X Y Z : C},
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X CategoryTheory.Limits.coprod.inr)
      (CategoryTheory.leftDistrib X Y Z).inv =
    CategoryTheory.Limits.coprod.inr
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.K'.main : Turing.PartrecToTM2.K'
-- Mathlib.MeasureTheory.Function.L1Space.Integrable
MeasureTheory.Integrable.of_mem_Icc : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ] (a b : ℝ)
  {X : α → ℝ}, AEMeasurable X μ → (∀ᵐ (ω : α) ∂μ, X ω ∈ Set.Icc a b) → MeasureTheory.Integrable X μ
-- Mathlib.Combinatorics.Quiver.Subquiver
/-- the target vertex of an arrow  -/
Quiver.Total.right : {V : Type u} → [inst : Quiver V] → Quiver.Total V → V
-- Mathlib.Algebra.GroupWithZero.Associated
associated_unit_mul_right_iff : ∀ {N : Type u_2} [inst : CommMonoid N] {a b : N} {u : Nˣ}, Associated a (↑u * b) ↔ Associated a b
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.inv_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y)
  [H : AlgebraicGeometry.PresheafedSpace.IsOpenImmersion f] {U V : (TopologicalSpace.Opens ↑↑X)ᵒᵖ} (i : U ⟶ V) {Z : C}
  (h :
    Y.presheaf.obj
        (Opposite.op ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).obj (Opposite.unop V))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (X.presheaf.map i)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f (Opposite.unop V))
        h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.invApp f (Opposite.unop U))
      (CategoryTheory.CategoryStruct.comp
        (Y.presheaf.map ((AlgebraicGeometry.PresheafedSpace.IsOpenImmersion.opensFunctor f).op.map i)) h)
-- Mathlib.RingTheory.UniqueFactorizationDomain.NormalizedFactors
UniqueFactorizationMonoid.normalize_normalized_factor : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizationMonoid α] [inst_2 : UniqueFactorizationMonoid α]
  {a : α}, ∀ x ∈ UniqueFactorizationMonoid.normalizedFactors a, normalize x = x
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKey?_eq_some_minKeyD : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.minKey? = some (t.minKeyD fallback)
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableSub₂.toMeasurableSub : ∀ {G : Type u_2} [inst : MeasurableSpace G] [inst_1 : Sub G] [MeasurableSub₂ G], MeasurableSub G
-- Lean.Parser.Do
Lean.Parser.Term.doForward.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.CommSq.HasLift.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B X Y : C} {f f_1 : A ⟶ X} (e_f : f = f_1)
  {i i_1 : A ⟶ B} (e_i : i = i_1) {p p_1 : X ⟶ Y} (e_p : p = p_1) {g g_1 : B ⟶ Y} (e_g : g = g_1)
  (sq : CategoryTheory.CommSq f i p g), sq.HasLift = ⋯.HasLift
-- Mathlib.LinearAlgebra.BilinearMap
LinearMap.lcomp_apply : ∀ {R : Type u_1} {S : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] {M : Type u_5} {M₂ : Type u_6} {N : Type u_7}
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : AddCommMonoid N] [inst_5 : Module R M]
  [inst_6 : Module R M₂] [inst_7 : Module S N] [inst_8 : Module R N] [inst_9 : SMulCommClass R S N] (f : M →ₗ[R] M₂)
  (g : M₂ →ₗ[R] N) (x : M), ((LinearMap.lcomp S N f) g) x = g (f x)
-- Mathlib.NumberTheory.JacobiSum.Basic
jacobiSum.eq_1 : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : Fintype R] [inst_2 : CommRing R'] (χ ψ : MulChar R R'),
  jacobiSum χ ψ = ∑ x, χ x * ψ (1 - x)
-- Init.Grind.Module.Basic
/-- Addition is associative.  -/
Lean.Grind.AddCommMonoid.add_assoc : ∀ {M : Type u} [self : Lean.Grind.AddCommMonoid M] (a b c : M), a + b + c = a + (b + c)
-- Mathlib.Order.Lattice
OrderDual.instSemilatticeSup.eq_1 : ∀ (α : Type u_1) [h : SemilatticeInf α],
  OrderDual.instSemilatticeSup α =
    { toPartialOrder := OrderDual.instPartialOrder α, sup := fun a b => SemilatticeInf.inf a b, le_sup_left := ⋯,
      le_sup_right := ⋯, sup_le := ⋯ }
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.IsFiniteMeasureOnCompacts.mk : ∀ {α : Type u_1} {m0 : MeasurableSpace α} [inst : TopologicalSpace α] {μ : MeasureTheory.Measure α},
  (∀ ⦃K : Set α⦄, IsCompact K → μ K < ⊤) → MeasureTheory.IsFiniteMeasureOnCompacts μ
-- Mathlib.Algebra.Lie.Nilpotent
LieModule.IsNilpotent.mk : ∀ {R : Type u} {L : Type v} (M : Type w) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M] {k : ℕ},
  LieModule.lowerCentralSeries R L M k = ⊥ → LieModule.IsNilpotent L M
-- Init.Data.Rat.Lemmas
Rat.floor_intCast : ∀ (a : ℤ), (↑a).floor = a