mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Shift.Localization
/-- The morphism of localizer from `W` to `W` given by the functor `shiftFunctor C a`
when `a : A` and `W` is compatible with the shift by `A`.  -/
CategoryTheory.MorphismProperty.shiftLocalizerMorphism : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (W : CategoryTheory.MorphismProperty C) →
      {A : Type w} →
        [inst_1 : AddMonoid A] →
          [inst_2 : CategoryTheory.HasShift C A] →
            [W.IsCompatibleWithShift A] → A → CategoryTheory.LocalizerMorphism W W
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Basic
/-- The `n`th group cohomology of a `k`-linear `G`-representation `A` is isomorphic to
`Extⁿ(k, A)` (taken in `Rep k G`), where `k` is a trivial `k`-linear `G`-representation.  -/
groupCohomologyIsoExt : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) →
        (n : ℕ) → groupCohomology A n ≅ ((Ext k (Rep.{u, u, u} k G) n).obj (Opposite.op (Rep.trivial k G k))).obj A
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey.congr_simp : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] (t t_1 : Std.ExtTreeMap α β cmp)
  (e_t : t = t_1) (h : t ≠ ∅), t.maxKey h = t_1.maxKey ⋯
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.Parser.featIdent : Lean.ParserDescr
-- Lean.Meta.Basic
_private.Lean.Meta.Basic.0.Lean.Meta.withNewLocalInstancesImpAux : {n : Type → Type u_1} → [MonadControlT Lean.MetaM n] → [Monad n] → {α : Type} → Array Lean.Expr → ℕ → n α → n α
-- Lean.Meta.Sym.ExprPtr
Lean.Meta.Sym.ExprPtr.mk.inj : ∀ {expr expr_1 : Lean.Expr}, { expr := expr } = { expr := expr_1 } → expr = expr_1
-- Mathlib.Order.Filter.Basic
Filter.Frequently.mp : ∀ {α : Type u} {p q : α → Prop} {f : Filter α},
  (∃ᶠ (x : α) in f, p x) → (∀ᶠ (x : α) in f, p x → q x) → ∃ᶠ (x : α) in f, q x
-- Mathlib.Algebra.Homology.ComplexShape
/-- The `ComplexShape` allowing differentials from `X (j+a)` to `X j`.
(For example when `a = 1`, a homology theory indexed by `ℕ` or `ℤ`)
 -/
ComplexShape.down' : {α : Type u_2} → [inst : Add α] → [IsRightCancelAdd α] → α → ComplexShape α
-- Mathlib.CategoryTheory.Bicategory.CatEnriched
CategoryTheory.CatEnrichedOrdinary.Hom.ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.EnrichedOrdinaryCategory CategoryTheory.Cat C] {X Y : CategoryTheory.CatEnrichedOrdinary C}
  {f g : X ⟶ Y} (α β : f ⟶ g),
  CategoryTheory.CatEnrichedOrdinary.Hom.base α = CategoryTheory.CatEnrichedOrdinary.Hom.base β → α = β
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pushoutCoconeOfLeftIso_ι_app_none : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z)
  [inst_1 : CategoryTheory.IsIso f], (CategoryTheory.Limits.pushoutCoconeOfLeftIso f g).ι.app none = g
-- Mathlib.RingTheory.Flat.Equalizer
LinearMap.lTensor_ker_subtype_tensorKerEquiv_symm : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M] {N : Type u_4}
  {P : Type u_5} [inst_7 : AddCommGroup N] [inst_8 : AddCommGroup P] [inst_9 : Module R N] [inst_10 : Module R P]
  (f : N →ₗ[R] P) [inst_11 : Module.Flat R M] (x : ↥((TensorProduct.AlgebraTensorModule.lTensor S M) f).ker),
  (LinearMap.lTensor M f.ker.subtype) ((LinearMap.tensorKerEquiv S M f).symm x) = ↑x
-- Mathlib.Algebra.Lie.Weights.Cartan
LieAlgebra.zeroRootSubalgebra_eq_iff_is_cartan : ∀ (R : Type u_1) (L : Type u_2) [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  (H : LieSubalgebra R L) [inst_3 : LieRing.IsNilpotent ↥H] [IsNoetherian R L],
  LieAlgebra.zeroRootSubalgebra R L H = H ↔ H.IsCartanSubalgebra
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S} {f : Y ⟶ h.pullback}
  {f_p₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f h.p₁ = g₁)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁._autoParam}
  {f_p₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f h.p₂ = g₂)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂._autoParam}
  {f_p :
    autoParam (CategoryTheory.CategoryStruct.comp f h.p = b)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p._autoParam}
  {f_1 : Y ⟶ h.pullback}
  {f_p₁_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f_1 h.p₁ = g₁)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₁._autoParam}
  {f_p₂_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f_1 h.p₂ = g₂)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p₂._autoParam}
  {f_p_1 :
    autoParam (CategoryTheory.CategoryStruct.comp f_1 h.p = b)
      CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p._autoParam},
  { f := f, f_p₁ := f_p₁, f_p₂ := f_p₂, f_p := f_p } = { f := f_1, f_p₁ := f_p₁_1, f_p₂ := f_p₂_1, f_p := f_p_1 } →
    f = f_1
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.mem_dual : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} {s : Set M} {y : N}, y ∈ PointedCone.dual p s ↔ ∀ ⦃x : M⦄, x ∈ s → 0 ≤ (p x) y
-- Init.Data.String.PosRaw
String.Pos.Raw.byteIdx_unoffsetBy : ∀ {p offset : String.Pos.Raw}, (p.unoffsetBy offset).byteIdx = p.byteIdx - offset.byteIdx
-- Aesop.Tree.Traversal
Aesop.preTraverseUp : {m : Type → Type} →
  [Monad m] →
    [MonadLiftT (ST IO.RealWorld) m] →
      (Aesop.GoalRef → m Bool) → (Aesop.RappRef → m Bool) → (Aesop.MVarClusterRef → m Bool) → Aesop.TreeRef → m Unit
-- Mathlib.SetTheory.Ordinal.Family
Ordinal.iSup_eq_lsub_or_succ_iSup_eq_lsub : ∀ {ι : Type u_3} (f : ι → Ordinal.{max u_4 u_3}), iSup f = Ordinal.lsub f ∨ Order.succ (iSup f) = Ordinal.lsub f
-- Mathlib.Algebra.Order.Field.Basic
one_div_lt_of_neg : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  a < 0 → b < 0 → (1 / a < b ↔ 1 / b < a)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
_private.Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point.0.tacticC_simp : Lean.ParserDescr
-- Mathlib.Algebra.WithConv
WithConv.toConv_ofConv : ∀ {A : Type u_2} (x : WithConv A), WithConv.toConv x.ofConv = x
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.ite_prod_one : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] (p : Prop) [inst_1 : Decidable p] (s : Finset ι) (f : ι → M),
  (if p then ∏ x ∈ s, f x else 1) = ∏ x ∈ s, if p then f x else 1
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- **Alias** of the reverse direction of `differentiableWithinAt_insert`. -/
DifferentiableWithinAt.insert' : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] {f : E → F} {x : E} {s : Set E} [T1Space E] {y : E},
  DifferentiableWithinAt 𝕜 f s x → DifferentiableWithinAt 𝕜 f (insert y s) x
-- Mathlib.GroupTheory.SemidirectProduct
/-- Define a group hom `N ⋊[φ] G →* H`, by defining maps `N →* H` and `G →* H`  -/
SemidirectProduct.lift : {N : Type u_1} →
  {G : Type u_2} →
    {H : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group G] →
          [inst_2 : Group H] →
            {φ : G →* MulAut N} →
              (fn : N →* H) →
                (fg : G →* H) →
                  (∀ (g : G),
                      fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn) →
                    N ⋊[φ] G →* H
-- Mathlib.FieldTheory.SeparableClosure
/-- The (infinite) separable degree for a general field extension `E / F` is defined
to be the degree of `separableClosure F E / F`.  -/
Field.sepDegree : (F : Type u) → (E : Type v) → [inst : Field F] → [inst_1 : Field E] → [Algebra F E] → Cardinal.{v}
-- Mathlib.Data.List.Basic
List.getLast_replicate_succ : ∀ {α : Type u} (m : ℕ) (a : α), (List.replicate (m + 1) a).getLast ⋯ = a
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.localTriv_symm_apply : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (i : ι) (p : B × F),
  ↑(Z.localTriv i).symm p = ⟨p.1, Z.coordChange i (Z.indexAt p.1) p.1 p.2⟩
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- A telescoping sum along `{0, ..., n-1}` of an `ℕ`-valued function reduces to the difference of
the last and first terms when the function we are summing is monotone.  -/
Finset.sum_range_tsub : ∀ {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [inst_2 : Sub M] [OrderedSub M] [AddLeftMono M]
  [AddLeftReflectLE M] [ExistsAddOfLE M] {f : ℕ → M},
  Monotone f → ∀ (n : ℕ), ∑ i ∈ Finset.range n, (f (i + 1) - f i) = f n - f 0
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
HasProdUniformly.multipliableUniformly : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : CommMonoid α] {f : ι → β → α} {g : β → α}
  [inst_1 : UniformSpace α], HasProdUniformly f g → MultipliableUniformly f
-- Mathlib.Data.Set.Finite.Basic
Set.Finite.exists_finset : ∀ {α : Type u} {s : Set α}, s.Finite → ∃ s', ∀ (a : α), a ∈ s' ↔ a ∈ s
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.monObjMkPullbackSnd_mul : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {X R S : C} {f : R ⟶ X} {g : S ⟶ X} [inst_2 : CategoryTheory.MonObj (CategoryTheory.Over.mk f)],
  CategoryTheory.MonObj.mul =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Functor.LaxMonoidal.μ (CategoryTheory.Over.pullback g) (CategoryTheory.Over.mk f)
        (CategoryTheory.Over.mk f))
      ((CategoryTheory.Over.pullback g).map CategoryTheory.MonObj.mul)
-- Mathlib.CategoryTheory.IsConnected
/-- If `J` is preconnected, then `Jᵒᵖ` is preconnected as well.  -/
CategoryTheory.isPreconnected_op : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] [CategoryTheory.IsPreconnected J],
  CategoryTheory.IsPreconnected Jᵒᵖ
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.eq_one_of_pos_of_log_eq_zero : ∀ {x : ℝ}, 0 < x → Real.log x = 0 → x = 1
-- Mathlib.Algebra.Module.Presentation.Cokernel
Module.Presentation.cokernel_relation : ∀ {A : Type u} [inst : Ring A] {M₁ : Type v₁} {M₂ : Type v₂} [inst_1 : AddCommGroup M₁] [inst_2 : Module A M₁]
  [inst_3 : AddCommGroup M₂] [inst_4 : Module A M₂] (pres₂ : Module.Presentation A M₂) {f : M₁ →ₗ[A] M₂} {ι : Type w₁}
  {g₁ : ι → M₁} (data : pres₂.CokernelData f g₁) (hg₁ : Submodule.span A (Set.range g₁) = ⊤) (x : pres₂.R ⊕ ι),
  (pres₂.cokernel data hg₁).relation x =
    match x with
    | Sum.inl r => pres₂.relation r
    | Sum.inr i => data.lift i
-- Mathlib.Analysis.SpecialFunctions.SmoothTransition
Real.smoothTransition.one_of_one_le : ∀ {x : ℝ}, 1 ≤ x → x.smoothTransition = 1
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- The existence of binary biproducts implies that there is at most one preadditive structure.  -/
CategoryTheory.Limits.biprod.add_eq_lift_id_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {X Y : C} (f g : X ⟶ Y)
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X X],
  f + g =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.biprod.lift (CategoryTheory.CategoryStruct.id X) (CategoryTheory.CategoryStruct.id X))
      (CategoryTheory.Limits.biprod.desc f g)
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenex.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → Sort u_4) (x : ℕ)
  (t₁ t₂ : L.Term (α ⊕ Fin x)) (h_1 : (x : ℕ) → motive x FirstOrder.Language.BoundedFormula.falsum)
  (h_2 : (x : ℕ) → (t₁ t₂ : L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.equal t₁ t₂))
  (h_3 :
    (x l : ℕ) →
      (R : L.Relations l) → (ts : Fin l → L.Term (α ⊕ Fin x)) → motive x (FirstOrder.Language.BoundedFormula.rel R ts))
  (h_4 : (x : ℕ) → (f₁ f₂ : L.BoundedFormula α x) → motive x (f₁.imp f₂))
  (h_5 : (x : ℕ) → (f : L.BoundedFormula α (x + 1)) → motive x f.all),
  (match x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ with
    | x, FirstOrder.Language.BoundedFormula.falsum => h_1 x
    | x, FirstOrder.Language.BoundedFormula.equal t₁ t₂ => h_2 x t₁ t₂
    | x, FirstOrder.Language.BoundedFormula.rel R ts => h_3 x l R ts
    | x, f₁.imp f₂ => h_4 x f₁ f₂
    | x, f.all => h_5 x f) =
    h_2 x t₁ t₂
-- Mathlib.MeasureTheory.Group.Measure
/-- If a left-invariant measure gives finite mass to a set with nonempty interior, then it gives
finite mass to any compact set.  -/
MeasureTheory.measure_lt_top_of_isCompact_of_isAddLeftInvariant' : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [IsTopologicalAddGroup G] [μ.IsAddLeftInvariant] {U : Set G},
  (interior U).Nonempty → μ U ≠ ⊤ → ∀ {K : Set G}, IsCompact K → μ K < ⊤
-- Mathlib.Data.Matrix.Mul
isStablyFiniteRing_iff : ∀ (R : Type u_10) [inst : MulOne R] [inst_1 : AddCommMonoid R],
  IsStablyFiniteRing R ↔ ∀ (n : ℕ), IsDedekindFiniteMonoid (Matrix (Fin n) (Fin n) R)
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LongExactSequence
/-- Exactness of `Hⁱ(G, X₃) ⟶ Hʲ(G, X₁) ⟶ Hʲ(G, X₂)`.  -/
groupCohomology.mapShortComplex₁_exact : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {X : CategoryTheory.ShortComplex (Rep.{u, u, u} k G)}
  (hX : X.ShortExact) {i j : ℕ} (hij : i + 1 = j), (groupCohomology.mapShortComplex₁ hX hij).Exact
-- Mathlib.Topology.Category.TopCat.Limits.Basic
/-- Given a functor `F : J ⥤ TopCat` and a cocone `c : Cocone (F ⋙ forget)`
of the underlying cocone of types, the colimit of `F` is `c.pt` equipped
with the supremum of the coinduced topologies by the maps `c.ι.app j`.  -/
TopCat.isColimitCoconeOfForget : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    {F : CategoryTheory.Functor J TopCat} →
      (c : CategoryTheory.Limits.Cocone (F.comp (CategoryTheory.forget TopCat))) →
        CategoryTheory.Limits.IsColimit c → CategoryTheory.Limits.IsColimit (TopCat.coconeOfCoconeForget c)
-- Mathlib.Topology.Category.TopCommRingCat
TopCommRingCat.forgetToTopCatCommRing : (R : TopCommRingCat) → CommRing ↑((CategoryTheory.forget₂ TopCommRingCat TopCat).obj R)
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
SlashInvariantForm.coe_const : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : Γ.HasDetOne] (x : ℂ),
  ⇑(SlashInvariantForm.const x) = Function.const UpperHalfPlane x
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.neg.inj : ∀ {c c_1 : Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr},
  Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.neg c = Lean.Meta.Grind.Arith.Cutsat.DiseqCnstrProof.neg c_1 → c = c_1
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree_lt_card_sub_one : ∀ {V : Type u_1} (G : SimpleGraph V) [inst : Fintype V] [inst_1 : DecidableRel G.Adj] (v : V),
  G.degree v < Fintype.card V - 1 ↔ ¬G.IsUniversal v
-- Init.Data.UInt.Lemmas
UInt32.toNat_toBitVec : ∀ (x : UInt32), x.toBitVec.toNat = x.toNat
-- Init.Data.SInt.Lemmas
Int32.toInt_toInt64 : ∀ (x : Int32), x.toInt64.toInt = x.toInt
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instOrdPosition : Ord Lean.Lsp.Position
-- Mathlib.CategoryTheory.ObjectProperty.FullSubcategory
CategoryTheory.ObjectProperty.full_ιOfLE : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P P' : CategoryTheory.ObjectProperty C} (h : P ≤ P'),
  (CategoryTheory.ObjectProperty.ιOfLE h).Full
-- Std.Data.HashMap.Lemmas
/-- Simpler variant of `getElem!_filter` when `LawfulBEq` is available.  -/
Std.HashMap.getElem!_filter' : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [LawfulBEq α] [inst : Inhabited β]
  {f : α → β → Bool} {k : α}, (Std.HashMap.filter f m)[k]! = (Option.filter (f k) m[k]?).get!
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
MeasureTheory.condExpL2_comp_continuousLinearMap : ∀ {α : Type u_1} {E' : Type u_3} (𝕜 : Type u_7) [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E']
  [inst_2 : InnerProductSpace 𝕜 E'] [inst_3 : CompleteSpace E'] [inst_4 : NormedSpace ℝ E'] {m m0 : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {E'' : Type u_8} (𝕜' : Type u_9) [inst_5 : RCLike 𝕜'] [inst_6 : NormedAddCommGroup E'']
  [inst_7 : InnerProductSpace 𝕜' E''] [inst_8 : CompleteSpace E''] [inst_9 : NormedSpace ℝ E''] (hm : m ≤ m0)
  (T : E' →L[ℝ] E'') (f : ↥(MeasureTheory.Lp E' 2 μ)),
  ↑↑↑((MeasureTheory.condExpL2 E'' 𝕜' hm) (T.compLp f)) =ᵐ[μ] ↑↑(T.compLp ↑((MeasureTheory.condExpL2 E' 𝕜 hm) f))
-- Init.Data.Int.Order
Int.one_ne_zero : 1 ≠ 0
-- Init.System.IOError
IO.Error.instToString : ToString IO.Error
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
/-- The isomorphism
`DerivedCategory.singleFunctors C ≅ (CochainComplex.singleFunctors C).postcomp Q`.  -/
DerivedCategory.singleFunctorsPostcompQIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        DerivedCategory.singleFunctors C ≅ (CochainComplex.singleFunctors C).postcomp DerivedCategory.Q
-- Mathlib.CategoryTheory.MorphismProperty.Basic
CategoryTheory.MorphismProperty.ofHoms_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_3} {X Y : ι → C} (f : (i : ι) → X i ⟶ Y i)
  {A B : C} (g : A ⟶ B),
  CategoryTheory.MorphismProperty.ofHoms f g ↔ ∃ i, CategoryTheory.Arrow.mk g = CategoryTheory.Arrow.mk (f i)
-- Mathlib.Algebra.GroupWithZero.ProdHom
MonoidWithZeroHom.snd.eq_1 : ∀ (G₀ : Type u_1) (H₀ : Type u_2) [inst : GroupWithZero G₀] [inst_1 : GroupWithZero H₀],
  MonoidWithZeroHom.snd G₀ H₀ = WithZero.lift' ((Units.coeHom H₀).comp (MonoidHom.snd G₀ˣ H₀ˣ))
-- Mathlib.Order.Interval.Finset.Fin
Fin.attachFin_Ioo : ∀ {n : ℕ} (a b : Fin n), (Finset.Ioo ↑a ↑b).attachFin ⋯ = Finset.Ioo a b
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- The image of `R` in `S` is linearly disjoint with any other submodules.  -/
Submodule.LinearDisjoint.one_left : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (N : Submodule R S),
  Submodule.LinearDisjoint 1 N
-- Mathlib.Algebra.Group.Units.Defs
/-- Units of a monoid have an induced multiplication.  -/
Units.instMul : {α : Type u} → [inst : Monoid α] → Mul αˣ
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.instIsStableUnderBaseChangeTop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], ⊤.IsStableUnderBaseChange
-- Mathlib.LinearAlgebra.Span.Basic
/-- Given an element `x` of a module `M` over `R`, the natural map from
`R` to scalar multiples of `x`. See also `LinearMap.ringLmapEquivSelf`.  -/
LinearMap.toSpanSingleton : (R : Type u_1) →
  (M : Type u_4) → [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → M → R →ₗ[R] M
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.weight_add_weight_pairMap : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommRing R] [inst_1 : DecidableEq σ] [inst_2 : Fintype σ] {k : ℕ},
  ∀ t ∈ MvPolynomial.NewtonIdentities.pairs✝ σ k,
    MvPolynomial.NewtonIdentities.weight✝ σ R k t +
        MvPolynomial.NewtonIdentities.weight✝ σ R k (MvPolynomial.NewtonIdentities.pairMap✝ σ t) =
      0
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
CategoryTheory.MorphismProperty.LeftFraction₃.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C} {X Y Y' : C}
  {f f' f'' : X ⟶ Y'} {s : Y ⟶ Y'} {hs : W s} {Y'_1 : C} {f_1 f'_1 f''_1 : X ⟶ Y'_1} {s_1 : Y ⟶ Y'_1} {hs_1 : W s_1},
  { Y' := Y', f := f, f' := f', f'' := f'', s := s, hs := hs } =
      { Y' := Y'_1, f := f_1, f' := f'_1, f'' := f''_1, s := s_1, hs := hs_1 } →
    Y' = Y'_1 ∧ f ≍ f_1 ∧ f' ≍ f'_1 ∧ f'' ≍ f''_1 ∧ s ≍ s_1
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.dvd_solve_elim' : ∀ {x d₁ a₁ p₁ d₂ a₂ p₂ d : ℤ},
  d = ↑((a₁ * d₂).gcd (a₂ * d₁)) → d₁ ∣ a₁ * x + p₁ → d₂ ∣ a₂ * x + p₂ → d ∣ a₂ * p₁ - a₁ * p₂
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.ringEquivOfRingEquiv.congr_simp : ∀ {R : Type u_5} {S : Type u_6} (K : Type u_7) (L : Type u_8) [inst : CommRing R] [inst_1 : IsDomain R]
  [inst_2 : CommRing S] [inst_3 : IsDomain S] [inst_4 : CommRing K] [inst_5 : CommRing L] [inst_6 : Algebra R K]
  [inst_7 : Algebra S L] [inst_8 : IsFractionRing R K] [inst_9 : IsFractionRing S L] (f f_1 : R ≃+* S),
  f = f_1 → FractionalIdeal.ringEquivOfRingEquiv K L f = FractionalIdeal.ringEquivOfRingEquiv K L f_1
-- Mathlib.AlgebraicGeometry.Group.Affine
/-- `Spec` as a functor from `R`-bialgebras to monoid schemes over `Spec R`.  -/
AlgebraicGeometry.bialgSpec : (R : CommRingCat) →
  CategoryTheory.Functor (CommBialgCat ↑R)ᵒᵖ (CategoryTheory.Mon (CategoryTheory.Over (AlgebraicGeometry.Spec R)))
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.IsAdjMatrix.toGraph_compl_eq : ∀ {α : Type u_1} {V : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq V] {A : Matrix V V α}
  [inst_2 : MulZeroOneClass α] [inst_3 : Nontrivial α] (h : A.IsAdjMatrix), ⋯.toGraph = h.toGraphᶜ
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- The functor between fundamental groupoids induced by a continuous map.  -/
FundamentalGroupoid.termπₘ : Lean.ParserDescr
-- Init.Notation
/-- `#check_simp t !~>` checks `simp` fails on reducing `t`.
 -/
Lean.Parser.checkSimpFailure : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Field.UnitBall
Metric.unitSphere.coe_pow : ∀ {𝕜 : Type u_1} [inst : SeminormedRing 𝕜] [inst_1 : NormMulClass 𝕜] [inst_2 : NormOneClass 𝕜]
  (x : ↑(Metric.sphere 0 1)) (n : ℕ), ↑(x ^ n) = ↑x ^ n
-- Mathlib.Combinatorics.SimpleGraph.DeleteEdges
/-- Given a vertex `x`, remove the edges incident to `x` from the edge set.  -/
SimpleGraph.deleteIncidenceSet : {V : Type u_1} → SimpleGraph V → V → SimpleGraph V
-- Mathlib.LinearAlgebra.RootSystem.RootPositive
RootPairing.RootPositiveForm.form_apply_root_ne_zero : ∀ {ι : Type u_1} {R : Type u_2} {S : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing S]
  [inst_1 : LinearOrder S] [inst_2 : CommRing R] [inst_3 : Algebra S R] [inst_4 : AddCommGroup M] [inst_5 : Module R M]
  [inst_6 : AddCommGroup N] [inst_7 : Module R N] {P : RootPairing ι R M N} [inst_8 : P.IsValuedIn S]
  (B : RootPairing.RootPositiveForm S P) [FaithfulSMul S R] (i : ι), (B.form (P.root i)) (P.root i) ≠ 0
-- Mathlib.Analysis.Calculus.BumpFunction.FiniteDimension
/-- An auxiliary function to construct partitions of unity on finite-dimensional real vector spaces.
It is the convolution between a smooth function of integral `1` supported in the ball of radius `D`,
with the indicator function of the closed unit ball. Therefore, it is smooth, equal to `1` on the
ball of radius `1 - D`, with support equal to the ball of radius `1 + D`.  -/
ExistsContDiffBumpBase.y : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] → [FiniteDimensional ℝ E] → [inst_3 : MeasurableSpace E] → [BorelSpace E] → ℝ → E → ℝ
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.forIn_toList : ∀ {m : Type w → Type u_1} {γ α β : Type w} [inst : Monad m] [LawfulMonad m] [inst_2 : Std.Iterator α Id β]
  [Std.Iterators.Finite α Id] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.IterM Id β}
  {f : β → γ → m (ForInStep γ)} {init : γ}, forIn it.toList.run init f = forIn it init f
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
/-- A precoverage respects isomorphisms if the property of being covering
is stable under isomorphism.
Use `PreZeroHypercover.presieve₀_mem_of_iso` for no universe restrictions.  -/
CategoryTheory.Precoverage.RespectsIso : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Precoverage C → Prop