mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The constant sheaf of a terminal object is indeed terminal  -/
CategoryTheory.Sheaf.isTerminalTerminal : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      {A : Type u₂} →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          {X : A} →
            (hX : CategoryTheory.Limits.IsTerminal X) →
              CategoryTheory.Limits.IsTerminal (CategoryTheory.Sheaf.terminal J hX)
-- Mathlib.CategoryTheory.Localization.SmallHom
CategoryTheory.Localization.SmallHom.equiv_chgUniv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W : CategoryTheory.MorphismProperty C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (L : CategoryTheory.Functor C D) [inst_2 : L.IsLocalization W] {X Y : C}
  [inst_3 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y]
  [inst_4 : CategoryTheory.Localization.HasSmallLocalizedHom W X Y] (e : CategoryTheory.Localization.SmallHom W X Y),
  (CategoryTheory.Localization.SmallHom.equiv W L) (CategoryTheory.Localization.SmallHom.chgUniv e) =
    (CategoryTheory.Localization.SmallHom.equiv W L) e
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.comp_toGradedRingHom : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {C : Type u_8} {ι : Type u_10} [inst : CommSemiring R]
  [inst_1 : Semiring A] [inst_2 : Semiring B] [inst_3 : Semiring C] [inst_4 : Algebra R A] [inst_5 : Algebra R B]
  [inst_6 : Algebra R C] [inst_7 : DecidableEq ι] [inst_8 : AddMonoid ι] {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B}
  {𝒞 : ι → Submodule R C} [inst_9 : GradedAlgebra 𝒜] [inst_10 : GradedAlgebra ℬ] [inst_11 : GradedAlgebra 𝒞]
  (g : ℬ →ₐᵍ[R] 𝒞) (f : 𝒜 →ₐᵍ[R] ℬ), (g.comp f).toGradedRingHom = g.toGradedRingHom.comp f.toGradedRingHom
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.epi_H_map_twoδ₁Toδ₀' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] [inst_1 : CategoryTheory.Abelian C] {ι' : Type u_3}
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (n₀ n₁ : ℤ),
  n₀ + 1 = n₁ →
    ∀ (i₀ i₁ i₂ : ι') (h₀₁ : i₀ ≤ i₁) (h₁₂ : i₁ ≤ i₂),
      CategoryTheory.Limits.IsZero ((X'.H n₁).obj (CategoryTheory.ComposableArrows.mk₁ (CategoryTheory.homOfLE h₀₁))) →
        CategoryTheory.Epi ((X'.H n₀).map (CategoryTheory.ComposableArrows.twoδ₁Toδ₀' i₀ i₁ i₂ h₀₁ h₁₂))
-- Mathlib.MeasureTheory.MeasurableSpace.Defs
MeasurableSpace.generateFrom_insert_univ : ∀ {α : Type u_1} (S : Set (Set α)), MeasurableSpace.generateFrom (insert Set.univ S) = MeasurableSpace.generateFrom S
-- Mathlib.CategoryTheory.Sites.Point.Monoidal
CategoryTheory.GrothendieckTopology.Point.toPresheafFiber_δ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A] [inst_2 : CategoryTheory.MonoidalCategory A]
  [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] (X : C) (x : Φ.fiber.obj X)
  (G₁ G₂ : CategoryTheory.Functor Cᵒᵖ A),
  CategoryTheory.CategoryStruct.comp (Φ.toPresheafFiber X x (CategoryTheory.MonoidalCategoryStruct.tensorObj G₁ G₂))
      (CategoryTheory.Functor.OplaxMonoidal.δ Φ.presheafFiber G₁ G₂) =
    CategoryTheory.MonoidalCategoryStruct.tensorHom (Φ.toPresheafFiber X x G₁) (Φ.toPresheafFiber X x G₂)
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.getElem_alternatingWord_swapIndices : ∀ {B : Type u_1} (i j : B) (p k : ℕ) (h : k + 1 < p),
  (CoxeterSystem.alternatingWord i j p)[k + 1] = (CoxeterSystem.alternatingWord j i p)[k]
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfStabilizer
/-- The stabilizer of a set acts on that set.  -/
VAdd.ofStabilizer : (G : Type u_1) →
  [inst : AddGroup G] → (α : Type u_2) → [inst_1 : AddAction G α] → (s : Set α) → VAdd ↥(AddAction.stabilizer G s) ↑s
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.range_glueDataObjι : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (U : ↑X.affineOpens),
  Set.range ⇑(I.glueDataObjι U) =
    ⇑(AlgebraicGeometry.IsAffineOpen.isoSpec ⋯).inv '' PrimeSpectrum.zeroLocus ↑(I.ideal U)
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.homEquiv_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {F : CategoryTheory.Functor C (Type v)} {X : C}
  (self : F.CorepresentableBy X) {Y Y' : C} (g : Y ⟶ Y') (f : X ⟶ Y),
  self.homEquiv (CategoryTheory.CategoryStruct.comp f g) =
    (CategoryTheory.ConcreteCategory.hom (F.map g)) (self.homEquiv f)
-- Std.Http.Data.Request
/-- The request body content of type t.
 -/
Std.Http.Request.body : {t : Type} → Std.Http.Request t → t
-- Mathlib.MeasureTheory.Integral.CurveIntegral.Basic
/-- The function `t ↦ ω (γ t) (γ' t)` which appears in the definition of a curve integral.

This definition is used to factor out common parts of lemmas
about `CurveIntegrable` and `curveIntegral`.  -/
curveIntegralFun : {𝕜 : Type u_4} →
  {E : Type u_5} →
    {F : Type u_6} →
      [inst : RCLike 𝕜] →
        [inst_1 : NormedAddCommGroup E] →
          [inst_2 : NormedSpace 𝕜 E] →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → {a b : E} → (E → E →L[𝕜] F) → Path a b → ℝ → F
-- Mathlib.Data.Ordmap.Ordset
Ordnode.erase.valid : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : DecidableLE α] (x : α) {t : Ordnode α},
  t.Valid → (Ordnode.erase x t).Valid
-- Mathlib.Data.EReal.Inv
EReal.sign_bot : SignType.sign ⊥ = -1
-- Init.Grind.AC
Lean.Grind.AC.Expr.toSeq'.eq_def : ∀ (e : Lean.Grind.AC.Expr) (s : Lean.Grind.AC.Seq),
  e.toSeq' s =
    match e with
    | Lean.Grind.AC.Expr.var x => Lean.Grind.AC.Seq.cons x s
    | a.op b => a.toSeq' (b.toSeq' s)
-- Mathlib.Data.Fintype.Sum
infinite_sum : ∀ {α : Type u_1} {β : Type u_2}, Infinite (α ⊕ β) ↔ Infinite α ∨ Infinite β
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion_apply : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  (self : IsDedekindDomain.HeightOneSpectrum.adicCompletion K v),
  (IsDedekindDomain.HeightOneSpectrum.adicCompletion.equivCompletion K v) self = self.toCompletion
-- Aesop.Index.Basic
/-- A rule that, according to the index, should be applied to the current goal.
In addition to the rule, this data structure contains information about how the
rule should be applied. For example, if the rule has rule patterns, we report
the substitutions obtained by matching the rule patterns against the current
goal.  -/
Aesop.IndexMatchResult : Type → Type
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.instPreservesColimitsOfShapeWalkingSpanOfDiscreteWalkingPair : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C] {D : Type u_1}
  [inst_2 : CategoryTheory.Category.{v_1, u_1} D] [Quiver.IsThin D] (F : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F],
  CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingSpan F
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
/-- The natural map from a nonsingular point on a Weierstrass curve in affine coordinates to its
corresponding nonsingular Jacobian point.  -/
WeierstrassCurve.Jacobian.Point.fromAffine : {R : Type r} → [inst : CommRing R] → {W' : WeierstrassCurve.Jacobian R} → [Nontrivial R] → W'.toAffine.Point → W'.Point
-- Mathlib.Order.Monotone.Monovary
monovary_comm : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} [inst : LinearOrder α] [inst_1 : LinearOrder β] {f : ι → α} {g : ι → β},
  Monovary f g ↔ Monovary g f
-- Mathlib.NumberTheory.Dioph
Dioph.proj_dioph_of_nat : ∀ {n : ℕ} (m : ℕ) [inst : Fin2.IsLT m n], Dioph.DiophFn fun v => v (Fin2.ofNat' m)
-- Init.Data.Array.Lemmas
Array.instBEq.eq_1 : ∀ {α : Type u} [inst : BEq α], Array.instBEq = { beq := fun xs ys => xs.isEqv ys BEq.beq }
-- Mathlib.Analysis.CStarAlgebra.ApproximateUnit
/-- To show that `l` is a one-sided approximate unit for `A`, it suffices to verify it only for
`m : A` with `0 ≤ m` and `‖m‖ < 1`.  -/
CStarAlgebra.tendsto_mul_right_of_forall_nonneg_tendsto : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A] {l : Filter A},
  (∀ (m : A), 0 ≤ m → ‖m‖ < 1 → Filter.Tendsto (fun x => x * m) l (nhds m)) →
    ∀ (m : A), Filter.Tendsto (fun x => x * m) l (nhds m)
-- Mathlib.LinearAlgebra.Eigenspace.Basic
/-- If `f` maps a subspace `p` into itself, then the generalized eigenspace of the restriction
of `f` to `p` is the part of the generalized eigenspace of `f` that lies in `p`.  -/
Module.End.genEigenspace_restrict : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (f : Module.End R M)
  (p : Submodule R M) (k : ℕ∞) (μ : R) (hfp : ∀ x ∈ p, f x ∈ p),
  (Module.End.genEigenspace (LinearMap.restrict f hfp) μ) k = Submodule.comap p.subtype ((f.genEigenspace μ) k)
-- Mathlib.Data.Finset.Fin
Finset.attachFin_subset_attachFin : ∀ {n : ℕ} {s t : Finset ℕ} (hst : s ⊆ t) (ht : ∀ m ∈ t, m < n), s.attachFin ⋯ ⊆ t.attachFin ht
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
/-- Given a star `ℝ≥0`-algebra homomorphism `φ` from `C(X, ℝ≥0)` into an `ℝ`-algebra `A`, this is
the unique extension of `φ` from `C(X, ℝ)` to `A` as a star `ℝ`-algebra homomorphism.  -/
StarAlgHom.realContinuousMapOfNNReal : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {A : Type u_2} →
      [inst_1 : Ring A] →
        [inst_2 : StarRing A] → [inst_3 : Algebra ℝ A] → (C(X, NNReal) →⋆ₐ[NNReal] A) → C(X, ℝ) →⋆ₐ[ℝ] A
-- Init.Data.UInt.Lemmas
UInt8.lt_ofNat_iff : ∀ {n : UInt8} {m : ℕ}, m < UInt8.size → (n < UInt8.ofNat m ↔ n.toNat < m)
-- Lean.Data.JsonRpc
Lean.JsonRpc.instFromJsonMessageDirection : Lean.FromJson Lean.JsonRpc.MessageDirection
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.NonUnitalRing.lift_comp_of : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι]
  [inst_4 : (i : ι) → NonUnitalNonAssocSemiring (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] [inst_6 : Nonempty ι] (P : Type u_7)
  [inst_7 : NonUnitalNonAssocSemiring P] (g : (i : ι) → G i →ₙ+* P)
  (Hg : ∀ (i j : ι) (hij : i ≤ j) (x : G i), (g j) ((f i j hij) x) = (g i) x) {i : ι},
  (DirectLimit.NonUnitalRing.lift G f P g Hg).comp (DirectLimit.NonUnitalRing.of G f i) = g i
-- Init.Grind.Attr
/-- Marks a theorem or definition for use by the `grind` tactic.

An optional modifier (e.g. `=`, `→`, `←`, `cases`, `intro`, `ext`, `inj`, etc.)
controls how `grind` uses the declaration:
* whether it is applied forwards, backwards, or both,
* whether equalities are used on the left, right, or both sides,
* whether case-splits, constructors, extensionality, or injectivity are applied,
* or whether custom instantiation patterns are used.

See the individual modifier docstrings for details.
 -/
Lean.Parser.Attr.grind : Lean.ParserDescr
-- Mathlib.Topology.Algebra.Monoid
continuousOn_list_sum : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : AddMonoid M] [ContinuousAdd M] {f : ι → X → M} (l : List ι) {t : Set X},
  (∀ i ∈ l, ContinuousOn (f i) t) → ContinuousOn (fun a => (List.map (fun i => f i a) l).sum) t
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey_insertIfNew : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k a : α} {v : β k} {h₁ : a ∈ m.insertIfNew k v},
  (m.insertIfNew k v).getKey a h₁ = if h₂ : (k == a) = true ∧ k ∉ m then k else m.getKey a ⋯
-- Mathlib.Algebra.Module.Torsion.Basic
isSMulRegular_iff_torsionBy_eq_bot : ∀ {R : Type u_2} (M : Type u_1) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (r : R),
  IsSMulRegular M r ↔ Submodule.torsionBy R M r = ⊥
-- Mathlib.Algebra.Order.Monoid.TypeTags
Multiplicative.isOrderedMonoid : ∀ {α : Type u_1} [inst : AddCommMonoid α] [inst_1 : Preorder α] [IsOrderedAddMonoid α],
  IsOrderedMonoid (Multiplicative α)
-- Mathlib.LinearAlgebra.Isomorphisms
/-- Canonical linear map from the quotient `p/(p ∩ p')` to `(p+p')/p'`, mapping `x + (p ∩ p')`
to `x + p'`, where `p` and `p'` are submodules of an ambient module.

Note that in the following declaration the type of the domain is expressed using
`comap p.subtype p ⊓ comap p.subtype p'`
instead of
`comap p.subtype (p ⊓ p')`
because the former is the simp normal form (see also `Submodule.comap_inf`).  -/
LinearMap.quotientInfToSupQuotient : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup M] →
        [inst_2 : Module R M] →
          (p p' : Submodule R M) →
            ↥p ⧸ Submodule.comap p.subtype p ⊓ Submodule.comap p.subtype p' →ₗ[R]
              ↥(p ⊔ p') ⧸ Submodule.comap (p ⊔ p').subtype p'
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Subgraph
SimpleGraph.Walk.toSubgraph_le_iff : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {w : G.Walk u v},
  ¬w.Nil → ∀ {G' : G.Subgraph}, w.toSubgraph ≤ G' ↔ w.edgeSet ⊆ G'.edgeSet
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.mk : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.IsTrail → p.support.Nodup → p.IsPath
-- Mathlib.Data.Set.Operations
Set.mem_range_self : ∀ {α : Type u} {ι : Sort u_1} {f : ι → α} (i : ι), f i ∈ Set.range f
-- Lean.Data.Lsp.Window
Lean.Lsp.MessageActionItem.mk.inj : ∀ {title title_1 : String}, { title := title } = { title := title_1 } → title = title_1
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.fill : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.vadd_orbit_eq_orbit_vadd : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] (N : AddSubgroup G) [nN : N.Normal] (a : X)
  (g : G), g +ᵥ AddAction.orbit (↥N) a = AddAction.orbit (↥N) (g +ᵥ a)
-- Mathlib.CategoryTheory.Subobject.Limits
CategoryTheory.Limits.imageSubobject_le_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A B X : C} (g : X ⟶ B) [inst_1 : CategoryTheory.Mono g]
  (f : A ⟶ B) [inst_2 : CategoryTheory.Limits.HasImage f] (h : A ⟶ X),
  CategoryTheory.CategoryStruct.comp h g = f → CategoryTheory.Limits.imageSubobject f ≤ CategoryTheory.Subobject.mk g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_maxKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKeyD t.maxKey! fallback = t.maxKey!
-- Mathlib.Topology.Irreducible
IsIrreducible.preimage_of_isPreirreducible_fiber : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {t : Set X},
  IsIrreducible t →
    ∀ (f : Y → X),
      IsOpenMap f → (∀ (x : X), IsPreirreducible (f ⁻¹' {x})) → (t ∩ Set.range f).Nonempty → IsIrreducible (f ⁻¹' t)
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `F` is a field of exponential characteristic `q`, `a : E` is separable over `F`, then
`F⟮a⟯ = F⟮a ^ q ^ n⟯` for any natural number `n`.  -/
IntermediateField.adjoin_simple_eq_adjoin_pow_expChar_pow_of_isSeparable : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] {a : E},
  IsSeparable F a → ∀ (q : ℕ) [ExpChar F q] (n : ℕ), F⟮a⟯ = F⟮a ^ q ^ n⟯
-- Mathlib.Order.Interval.Set.Basic
Set.mem_Ioc_of_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Ioo b a → x ∈ Set.Ioc b a
-- Std.Data.DTreeMap.Raw.WF
Std.DTreeMap.Raw.WF.mergeWith : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp]
  {mergeFn : (a : α) → β a → β a → β a} {t₁ t₂ : Std.DTreeMap.Raw α β cmp},
  t₁.WF → (Std.DTreeMap.Raw.mergeWith mergeFn t₁ t₂).WF
-- Mathlib.CategoryTheory.Limits.Indization.Category
CategoryTheory.instCategoryInd : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Category.{v, max u (v + 1)} (CategoryTheory.Ind C)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.pOpcyclesIso_inv_hom_id_assoc : ∀ {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 j : ι) (hi : c.prev j = i) (h : K.d i j = 0)
  [inst_2 : K.HasHomology j] {Z : C} (h_1 : K.opcycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.pOpcyclesIso i j hi h).inv
      (CategoryTheory.CategoryStruct.comp (K.pOpcycles j) h_1) =
    h_1
-- Mathlib.MeasureTheory.Function.LpSeminorm.Monotonicity
MeasureTheory.MemLp.im : ∀ {α : Type u_1} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α} {𝕜 : Type u_5} [inst : RCLike 𝕜]
  {f : α → 𝕜}, MeasureTheory.MemLp f p μ → MeasureTheory.MemLp (fun x => RCLike.im (f x)) p μ
-- Mathlib.Topology.Sheaves.Skyscraper
SkyscraperPresheafFunctor.map'_app : ∀ {X : TopCat} (p₀ : ↑X) [inst : (U : TopologicalSpace.Opens ↑X) → Decidable (p₀ ∈ U)] {C : Type v}
  [inst_1 : CategoryTheory.Category.{w, v} C] [inst_2 : CategoryTheory.Limits.HasTerminal C] {a b : C} (f : a ⟶ b)
  (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  (SkyscraperPresheafFunctor.map' p₀ f).app U =
    if h : p₀ ∈ Opposite.unop U then
      CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
        (CategoryTheory.CategoryStruct.comp f (CategoryTheory.eqToHom ⋯))
    else (⋯ ▸ CategoryTheory.Limits.terminalIsTerminal).from ((skyscraperPresheaf p₀ a).obj U)
-- Mathlib.Order.BooleanAlgebra.Basic
compl_eq_bot : ∀ {α : Type u} {x : α} [inst : BooleanAlgebra α], xᶜ = ⊥ ↔ x = ⊤
-- Mathlib.CategoryTheory.Bicategory.Modification.Oplax
CategoryTheory.Oplax.OplaxTrans.Modification.whiskerRight_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} {η θ : F ⟶ G} (Γ : CategoryTheory.Oplax.OplaxTrans.Modification η θ) {a b : B}
  {a' : C} (f : a ⟶ b) (g : G.obj b ⟶ a') {Z : F.obj a ⟶ a'}
  (h : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (θ.app a) (G.map f)) g ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft (F.map f) (CategoryTheory.Bicategory.whiskerRight (Γ.app b) g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (θ.app b) g).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (θ.naturality f) g) h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (η.app b) g).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) g)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (Γ.app a) (G.map f)) g) h))
-- Mathlib.AlgebraicTopology.SimplicialSet.KanComplex.MulStruct
SSet.PtSimplex.RelStruct.δ_succ_map_assoc : ∀ {X : SSet} {n : ℕ} {x : X.obj (Opposite.op { len := 0 })} {f g : X.PtSimplex n x} {i : Fin (n + 1)}
  (self : f.RelStruct g i) {Z : SSet} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (SSet.stdSimplex.δ i.succ) (CategoryTheory.CategoryStruct.comp self.map h) =
    CategoryTheory.CategoryStruct.comp g.map h
-- Mathlib.Geometry.Manifold.Immersion
Manifold.IsImmersionAtOfComplement.mk_of_charts : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} {E'' : Type u} {F : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup E'']
  [inst_4 : NormedSpace 𝕜 E''] [inst_5 : NormedAddCommGroup F] [inst_6 : NormedSpace 𝕜 F] {H : Type u_7}
  [inst_7 : TopologicalSpace H] {G : Type u_9} [inst_8 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 E'' G} {M : Type u_11} [inst_9 : TopologicalSpace M] [inst_10 : ChartedSpace H M]
  {N : Type u_13} [inst_11 : TopologicalSpace N] [inst_12 : ChartedSpace G N] {n : WithTop ℕ∞} {f : M → N} {x : M}
  (equiv : (E × F) ≃L[𝕜] E'') (domChart : OpenPartialHomeomorph M H) (codChart : OpenPartialHomeomorph N G),
  x ∈ domChart.source →
    f x ∈ codChart.source →
      domChart ∈ IsManifold.maximalAtlas I n M →
        codChart ∈ IsManifold.maximalAtlas J n N →
          domChart.source ⊆ f ⁻¹' codChart.source →
            Set.EqOn (↑(codChart.extend J) ∘ f ∘ ↑(domChart.extend I).symm) (⇑equiv ∘ fun x => (x, 0))
                (domChart.extend I).target →
              Manifold.IsImmersionAtOfComplement F I J n f x
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.equivToOverUnit_functor : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.equivToOverUnit C).functor =
    CategoryTheory.Over.forget (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.AlgebraicTopology.SimplicialSet.Op
SSet.opEquivalence_unitIso : SSet.opEquivalence.unitIso = SSet.opFunctorCompOpFunctorIso.symm
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
/-- Given a connected component `c` of a graph `G`, `lapMatrix_ker_basis_aux c` is the map
`V → ℝ` which is `1` on the vertices in `c` and `0` elsewhere.
The family of these maps indexed by the connected components of `G` proves to be a basis
of the kernel of `lapMatrix G R`  -/
SimpleGraph.lapMatrix_ker_basis_aux : {V : Type u_1} →
  [inst : Fintype V] →
    (G : SimpleGraph V) →
      [inst_1 : DecidableRel G.Adj] →
        [inst_2 : DecidableEq V] →
          [DecidableEq G.ConnectedComponent] → G.ConnectedComponent → ↥(Matrix.toLin' (SimpleGraph.lapMatrix ℝ G)).ker
-- Mathlib.CategoryTheory.Monoidal.PushoutProduct
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso_inv_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : CategoryTheory.Arrow C) {W : C}
  [inst_3 :
    CategoryTheory.Limits.PreservesColimit
      (CategoryTheory.Limits.span (CategoryTheory.MonoidalCategoryStruct.whiskerRight X₁.hom X₂.left)
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₁.left X₂.hom))
      (CategoryTheory.MonoidalCategory.tensorLeft W)],
  (CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerLeftIso X₁ X₂).inv.left =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.HasColimit.isoOfNatIso
          (CategoryTheory.Limits.spanExt (CategoryTheory.MonoidalCategoryStruct.associator W X₁.left X₂.left).symm
            (CategoryTheory.MonoidalCategoryStruct.associator W X₁.right X₂.left).symm
            (CategoryTheory.MonoidalCategoryStruct.associator W X₁.left X₂.right).symm ⋯ ⋯)).inv
      ⋯.isoPushout.inv
-- Mathlib.Data.Nat.BinaryRec
Nat.bit_shiftRight_one : ∀ (b : Bool) (n : ℕ), Nat.bit b n >>> 1 = n
-- Mathlib.CategoryTheory.ConnectedComponents
/-- Functions from connected components and functors to discrete category are in bijection  -/
CategoryTheory.ConnectedComponents.typeToCatHomEquiv : (J : Type u_2) →
  [inst : CategoryTheory.Category.{v_1, u_2} J] →
    (X : Type u_1) → (CategoryTheory.ConnectedComponents J → X) ≃ CategoryTheory.Functor J (CategoryTheory.Discrete X)
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- Eta-expanded form of `mvfderiv_neg` -/
mvfderiv_fun_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {F : Type u_8} [inst_6 : NormedAddCommGroup F]
  [inst_7 : NormedSpace 𝕜 F] {g : M → F} {x : M}, (d% fun i => -g i) x = -d% g x