mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Operations
/-- The tree.  -/
Std.DTreeMap.Internal.Impl.Tree.impl : {α : Type u} → {β : α → Type v} → {size : ℕ} → Std.DTreeMap.Internal.Impl.Tree α β size → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Algebra.Group.Submonoid.Operations
/-- The `AddMonoidHom` associated to an inclusion of `AddSubmonoid`s.  -/
AddSubmonoid.inclusion : {M : Type u_1} → [inst : AddZeroClass M] → {S T : AddSubmonoid M} → S ≤ T → ↥S →+ ↥T
-- Lean.Data.Lsp.Internal
Lean.Lsp.instFromJsonModuleRefs : Lean.FromJson Lean.Lsp.ModuleRefs
-- Mathlib.Topology.ContinuousMap.Basic
map_continuousWithinAt : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : FunLike F α β] [ContinuousMapClass F α β] (f : F) (s : Set α) (a : α), ContinuousWithinAt (⇑f) s a
-- Mathlib.ModelTheory.Syntax
/-- Raises all of the bound variables of a formula greater than or equal to `m` by `n'`.  -/
FirstOrder.Language.BoundedFormula.liftAt : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → (n' : ℕ) → ℕ → L.BoundedFormula α n → L.BoundedFormula α (n + n')
-- Mathlib.Data.Matrix.Block
Matrix.blockDiag_blockDiagonal : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : Zero α] [inst_1 : DecidableEq o]
  (M : o → Matrix m n α), (Matrix.blockDiagonal M).blockDiag = M
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
/-- A product taken over a conditional whose condition is an equality test on the index and whose
alternative is `1` has value either the term at that index or `1`.

The difference with `Finset.prod_ite_eq` is that the arguments to `Eq` are swapped.  -/
Finset.prod_ite_eq' : ∀ {ι : Type u_1} {M : Type u_3} [inst : CommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M),
  (∏ x ∈ s, if x = a then b x else 1) = if a ∈ s then b a else 1
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get!_eq_default_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited β] {a : α}, t.contains a = false → Std.ExtDTreeMap.Const.get! t a = default
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.unitsSMulWithCancel.eq_1 : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} (φ : ↥A ≃* ↥B) {d : HNNExtension.NormalWord.TransversalPair G A B}
  (u : ℤˣ) (w : HNNExtension.NormalWord d),
  HNNExtension.NormalWord.unitsSMulWithCancel φ u w =
    HNNExtension.NormalWord.consRecOn (motive := fun x =>
      HNNExtension.NormalWord.Cancels u x → HNNExtension.NormalWord d) w (id fun g a => w) fun g x w x_1 x_2 x_3 can =>
      ↑((HNNExtension.toSubgroupEquiv φ u) ⟨g, ⋯⟩) • w
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- In a category with weak equivalences, this is the quotient of the type
of morphisms `X ⟶ Y` by the equivalence relation generated by right homotopies.  -/
HomotopicalAlgebra.RightHomotopyClass : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → C → C → [HomotopicalAlgebra.CategoryWithWeakEquivalences C] → Type v
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabSort : Lean.Elab.Term.TermElab
-- Mathlib.Computability.Primrec.Basic
Nat.Primrec.brecOn : ∀ {motive : (a : ℕ → ℕ) → Nat.Primrec a → Prop} {a : ℕ → ℕ} (t : Nat.Primrec a),
  (∀ (a : ℕ → ℕ) (t : Nat.Primrec a), Nat.Primrec.below t → motive a t) → motive a t
-- Mathlib.Algebra.Group.Basic
mul_inv_mul_mul_cancel : ∀ {G : Type u_3} [inst : Group G] (a b c : G), a * b⁻¹ * (b * c) = a * c
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.unop : C ⥤ D` reflects colimits, then `F : Cᵒᵖ ⥤ Dᵒᵖ` reflects limits.  -/
CategoryTheory.Limits.reflectsLimits_of_unop : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor Cᵒᵖ Dᵒᵖ) [CategoryTheory.Limits.ReflectsColimits F.unop],
  CategoryTheory.Limits.ReflectsLimits F
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.extract.injEq : ∀ {w : ℕ} (start len : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w) (w_1 start_1 : ℕ)
  (expr_1 : Std.Tactic.BVDecide.BVExpr w_1),
  (Std.Tactic.BVDecide.BVExpr.extract start len expr = Std.Tactic.BVDecide.BVExpr.extract start_1 len expr_1) =
    (w = w_1 ∧ start = start_1 ∧ expr ≍ expr_1)
-- Init.Data.Array.Lemmas
Array.flatten_replicate_empty : ∀ {n : ℕ} {α : Type u_1}, (Array.replicate n #[]).flatten = #[]
-- Mathlib.ModelTheory.Substructures
FirstOrder.Language.Substructure.map_surjective_of_surjective : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {f : L.Hom M N},
  Function.Surjective ⇑f → Function.Surjective (FirstOrder.Language.Substructure.map f)
-- Mathlib.RingTheory.WittVector.Domain
WittVector.instNoZeroDivisorsOfCharP : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] [CharP R p] [NoZeroDivisors R],
  NoZeroDivisors (WittVector p R)
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Centroid
Affine.Simplex.point_vsub_faceOppositeCentroid_eq_smul_vsub : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {n : ℕ} [inst_4 : NeZero n] [CharZero k] (s : Affine.Simplex k P n) (i : Fin (n + 1)),
  s.points i -ᵥ s.faceOppositeCentroid i = (↑n + 1) • (s.centroid -ᵥ s.faceOppositeCentroid i)
-- Mathlib.Logic.Nonempty
Nonempty.imp : ∀ {α : Sort u_3} {p : Prop}, Nonempty α → p ↔ ∀ (a : α), p
-- Mathlib.Algebra.Exact.Basic
LinearMap.ker_eq_bot_range_liftQ_iff : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {P : Type u_6} [inst : Ring R] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : AddCommGroup P] [inst_4 : Module R M] [inst_5 : Module R N] [inst_6 : Module R P]
  {f : M →ₗ[R] N} {g : N →ₗ[R] P} (h : f.range ≤ g.ker), (f.range.liftQ g h).ker = ⊥ ↔ g.ker = f.range
-- Mathlib.CategoryTheory.Monoidal.Hopf_
/-- The antipode is an endomorphism of the underlying object of the Hopf monoid.  -/
CategoryTheory.HopfObj.«term𝒮[_]» : Lean.ParserDescr
-- Mathlib.Topology.ContinuousOn
Topology.IsQuotientMap.continuousOn_isOpen_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {g : β → γ},
  Topology.IsQuotientMap f → ∀ {s : Set β}, IsOpen s → (ContinuousOn g s ↔ ContinuousOn (g ∘ f) (f ⁻¹' s))
-- Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker
_private.Std.Tactic.BVDecide.LRAT.Internal.CompactLRATChecker.0.Std.Tactic.BVDecide.LRAT.Internal.compactLratChecker.go.match_3.eq_2 : ∀ {n : ℕ} (motive : Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClauseAction n) → Sort u_1) (id : ℕ)
  (rupHints : Array ℕ) (h_1 : Unit → motive none)
  (h_2 : (id : ℕ) → (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints)))
  (h_3 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (rupHints : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints)))
  (h_4 :
    (id : ℕ) →
      (c : Std.Tactic.BVDecide.LRAT.Internal.DefaultClause n) →
        (pivot : Std.Sat.Literal (Std.Tactic.BVDecide.LRAT.Internal.PosFin n)) →
          (rupHints : Array ℕ) →
            (ratHints : Array (ℕ × Array ℕ)) →
              motive (some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints)))
  (h_5 : (ids : Array ℕ) → motive (some (Std.Tactic.BVDecide.LRAT.Action.del ids))),
  (match some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) with
    | none => h_1 ()
    | some (Std.Tactic.BVDecide.LRAT.Action.addEmpty id rupHints) => h_2 id rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRup id c rupHints) => h_3 id c rupHints
    | some (Std.Tactic.BVDecide.LRAT.Action.addRat id c pivot rupHints ratHints) => h_4 id c pivot rupHints ratHints
    | some (Std.Tactic.BVDecide.LRAT.Action.del ids) => h_5 ids) =
    h_2 id rupHints
-- Mathlib.Data.Complex.Basic
Complex.instOne : One ℂ
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.mul_one : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F (x.mul CommRingCat.Colimits.Prequotient.one) x
-- Init.Data.Format.Basic
Std.instInhabitedFormat.default : Std.Format
-- Mathlib.Analysis.Calculus.Implicit
ImplicitFunctionData.range_leftDeriv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : CompleteSpace E] {F : Type u_3} [inst_4 : NormedAddCommGroup F]
  [inst_5 : NormedSpace 𝕜 F] [inst_6 : CompleteSpace F] {G : Type u_4} [inst_7 : NormedAddCommGroup G]
  [inst_8 : NormedSpace 𝕜 G] [inst_9 : CompleteSpace G] (self : ImplicitFunctionData 𝕜 E F G),
  (↑self.leftDeriv).range = ⊤
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- If `A : Cᵒᵖ ⥤ Type v` is a presheaf, then the Yoneda embedding for
`CostructuredArrow yoneda A` factors through `Over A` via a forgetful functor and an
equivalence.

This is Lemma 1.4.12 in [Kashiwara2006].  -/
CategoryTheory.CostructuredArrow.toOverCompOverEquivPresheafCostructuredArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (A : CategoryTheory.Functor Cᵒᵖ (Type v)) →
      (CategoryTheory.CostructuredArrow.toOver CategoryTheory.yoneda A).comp
          (CategoryTheory.overEquivPresheafCostructuredArrow A).functor ≅
        CategoryTheory.yoneda
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.div_eq_zero_of_lt : ∀ {a b : Ordinal.{u_4}}, a < b → a / b = 0
-- Init.Data.UInt.Basic
/-- Bitwise right shift for 16-bit unsigned integers. Usually accessed via the `>>>` operator.

This function is overridden at runtime with an efficient implementation.
 -/
UInt16.shiftRight : UInt16 → UInt16 → UInt16
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffOn.continuousOn_zero : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F}, ContDiffOn 𝕜 0 f s → ContinuousOn f s
-- Init.Data.Rat.Lemmas
Rat.inv_divInt : ∀ (n d : ℤ), (Rat.divInt n d)⁻¹ = Rat.divInt d n
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.lcongr_apply_apply : ∀ {M : Type u_2} {N : Type u_3} {R : Type u_5} {R₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : Module R M] [inst_4 : AddCommMonoid N] [inst_5 : Module R₂ N] {σ : R →+* R₂}
  {σ_inv : R₂ →+* R} [inst_6 : RingHomInvPair σ σ_inv] [inst_7 : RingHomInvPair σ_inv σ] {ι : Type u_9} {κ : Type u_10}
  (e₁ : ι ≃ κ) (e₂ : M ≃ₛₗ[σ] N) (f : ι →₀ M) (k : κ), ((Finsupp.lcongr e₁ e₂) f) k = e₂ (f (e₁.symm k))
-- Init.Data.Sum.Lemmas
Sum.forall_sum : ∀ {α : Type u_1} {β : Type u_2} {γ : α ⊕ β → Sort u_3} {p : ((ab : α ⊕ β) → γ ab) → Prop},
  (∀ (fab : (ab : α ⊕ β) → γ ab), p fab) ↔
    ∀ (fa : (val : α) → γ (Sum.inl val)) (fb : (val : β) → γ (Sum.inr val)), p fun t => Sum.rec fa fb t
-- Mathlib.MeasureTheory.Integral.Lebesgue.Countable
MeasureTheory.lintegral_singleton' : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  Measurable f → ∀ (a : α), ∫⁻ (x : α) in {a}, f x ∂μ = f a * μ {a}
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mahlerMeasure.eq_1 : ∀ (p : Polynomial ℂ), p.mahlerMeasure = if p ≠ 0 then Real.exp p.logMahlerMeasure else 0
-- Mathlib.MeasureTheory.Measure.WithDensity
MeasureTheory.ae_withDensity_iff' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {p : α → Prop} {f : α → ENNReal},
  AEMeasurable f μ → ((∀ᵐ (x : α) ∂μ.withDensity f, p x) ↔ ∀ᵐ (x : α) ∂μ, f x ≠ 0 → p x)
-- Init.Core
instSubsingletonPUnit : Subsingleton PUnit.{u_1}
-- Init.Data.Range.Polymorphic.BitVec
BitVec.succ?_eq_some : ∀ {n : ℕ} {x y : BitVec n}, Std.PRange.succ? x = some y ↔ x.toNat < 2 ^ n - 1 ∧ y.toNat = x.toNat + 1
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- A submonoid of a unital magma inherits a unital magma structure.  -/
Submonoid.toMulOneClass : {M : Type u_5} → [inst : MulOneClass M] → (S : Submonoid M) → MulOneClass ↥S
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
/-- The condition for a square matrix `A` to be skew-adjoint with respect to the square matrix
`J`.  -/
Matrix.IsSkewAdjoint : {R : Type u_1} → {n : Type u_11} → [CommRing R] → [Fintype n] → Matrix n n R → Matrix n n R → Prop
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.delayFootnote : Lean.StrLit → Lean.ElabInline
-- Lean.Data.DeclarationRange
Lean.instReprDeclarationLocation : Repr Lean.DeclarationLocation
-- Mathlib.Order.Interval.Finset.Fin
Fin.finsetImage_castSucc_uIcc : ∀ {n : ℕ} (i j : Fin n), Finset.image Fin.castSucc (Finset.uIcc i j) = Finset.uIcc i.castSucc j.castSucc
-- Mathlib.Order.Filter.Prod
Filter.Tendsto.coprod_of_prod_top_right : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α × β → γ} {la : Filter α} {lb : Filter β} {lc : Filter γ},
  (∀ s ∈ la, Filter.Tendsto f (Filter.principal sᶜ ×ˢ lb) lc) →
    Filter.Tendsto f (la ×ˢ ⊤) lc → Filter.Tendsto f (la.coprod lb) lc
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.prod_mono : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {s₁ s₂ : Subsemigroup M} {t₁ t₂ : Subsemigroup N},
  s₁ ≤ s₂ → t₁ ≤ t₂ → s₁.prod t₁ ≤ s₂.prod t₂
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.LaxTrans.mk : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          (app : (a : B) → F.obj a ⟶ G.obj a) →
            (naturality :
                {a b : B} →
                  (f : a ⟶ b) →
                    CategoryTheory.CategoryStruct.comp (app a) (G.map f) ⟶
                      CategoryTheory.CategoryStruct.comp (F.map f) (app b)) →
              autoParam
                  (∀ {a b : B} {f g : a ⟶ b} (η : f ⟶ g),
                    CategoryTheory.CategoryStruct.comp (naturality f)
                        (CategoryTheory.Bicategory.whiskerRight (F.map₂ η) (app b)) =
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.map₂ η))
                        (naturality g))
                  CategoryTheory.Lax.LaxTrans.naturality_naturality._autoParam →
                autoParam
                    (∀ (a : B),
                      CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapId a))
                          (naturality (CategoryTheory.CategoryStruct.id a)) =
                        CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (app a)).hom
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (app a)).inv
                            (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (app a))))
                    CategoryTheory.Lax.LaxTrans.naturality_id._autoParam →
                  autoParam
                      (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c),
                        CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Bicategory.whiskerLeft (app a) (G.mapComp f g))
                            (naturality (CategoryTheory.CategoryStruct.comp f g)) =
                          CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.Bicategory.associator (app a) (G.map f) (G.map g)).inv
                            (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.Bicategory.whiskerRight (naturality f) (G.map g))
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.Bicategory.associator (F.map f) (app b) (G.map g)).hom
                                (CategoryTheory.CategoryStruct.comp
                                  (CategoryTheory.Bicategory.whiskerLeft (F.map f) (naturality g))
                                  (CategoryTheory.CategoryStruct.comp
                                    (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (app c)).inv
                                    (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g) (app c)))))))
                      CategoryTheory.Lax.LaxTrans.naturality_comp._autoParam →
                    CategoryTheory.Lax.LaxTrans F G
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.Equiv.of_toList_perm : ∀ {α : Type u} {m₁ m₂ : Std.HashSet.Raw α}, m₁.toList.Perm m₂.toList → m₁.Equiv m₂
-- Mathlib.NumberTheory.DiophantineApproximation.Basic
/-- The set of good rational approximations to a real number `ξ` is infinite if and only if
`ξ` is irrational.  -/
Real.infinite_rat_abs_sub_lt_one_div_den_sq_iff_irrational : ∀ (ξ : ℝ), {q | |ξ - ↑q| < 1 / ↑q.den ^ 2}.Infinite ↔ Irrational ξ
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.toOpens.eq_1 : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] (U : OpenSubgroup G),
  ↑U = { carrier := ↑U, is_open' := ⋯ }
-- Mathlib.Topology.Order.HullKernel
/-- The relative-open sets of the form `(hull T a)ᶜ` for `a` in `α` form a basis for the relative
Lower topology.
 -/
PrimitiveSpectrum.isTopologicalBasis_relativeLower : ∀ {α : Type u_1} [inst : SemilatticeInf α] {T : Set α} [OrderTop α] [inst_2 : TopologicalSpace α] [Topology.IsLower α],
  (∀ p ∈ T, InfPrime p) → TopologicalSpace.IsTopologicalBasis {S | ∃ a, (PrimitiveSpectrum.hull T a)ᶜ = S}
-- Mathlib.CategoryTheory.Sites.Hypercover.IsSheaf
CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.fac'_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {A : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} A] {H : J.OneHypercoverFamily} {P : CategoryTheory.Functor Cᵒᵖ A}
  (hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (CategoryTheory.Limits.IsLimit (E.multifork P))) {X : C}
  {S : CategoryTheory.Sieve X} {E : J.OneHypercover X} (hE : H E) (le : E.sieve₀ ≤ S)
  (F : CategoryTheory.Limits.Multifork (CategoryTheory.GrothendieckTopology.Cover.index ⟨S, ⋯⟩ P)) (i : E.I₀) {Z : A}
  (h : P.obj (Opposite.op (E.X i)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.GrothendieckTopology.OneHypercoverFamily.IsSheafIff.lift hP hE le F)
      (CategoryTheory.CategoryStruct.comp (P.map (E.f i).op) h) =
    CategoryTheory.CategoryStruct.comp (F.ι { Y := E.X i, f := E.f i, hf := ⋯ }) h
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Basic
AugmentedSimplexCategory.inclusion_map : ∀ {X Y : SimplexCategory} (f : X ⟶ Y), AugmentedSimplexCategory.inclusion.map f = f
-- Mathlib.LinearAlgebra.TensorProduct.DirectLimit
/-- `limᵢ (Gᵢ ⊗ M)` and `(limᵢ Gᵢ) ⊗ M` are isomorphic as modules
 -/
TensorProduct.directLimitLeft : {R : Type u_1} →
  [inst : CommSemiring R] →
    {ι : Type u_2} →
      [inst_1 : DecidableEq ι] →
        [inst_2 : Preorder ι] →
          {G : ι → Type u_3} →
            [inst_3 : (i : ι) → AddCommMonoid (G i)] →
              [inst_4 : (i : ι) → Module R (G i)] →
                (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) →
                  (M : Type u_4) →
                    [inst_5 : AddCommMonoid M] →
                      [inst_6 : Module R M] →
                        TensorProduct R (Module.DirectLimit G f) M ≃ₗ[R]
                          Module.DirectLimit (fun x => TensorProduct R (G x) M) fun i j h =>
                            LinearMap.rTensor M (f i j h)
-- Mathlib.Algebra.Polynomial.Degree.IsMonicOfDegree
Polynomial.IsMonicOfDegree.mul : ∀ {R : Type u_1} [inst : Semiring R] {p q : Polynomial R} {m n : ℕ},
  p.IsMonicOfDegree m → q.IsMonicOfDegree n → (p * q).IsMonicOfDegree (m + n)
-- Mathlib.Algebra.Group.Units.Hom
Units.val_zpow_eq_zpow_val : ∀ {α : Type u_1} [inst : DivisionMonoid α] (u : αˣ) (n : ℤ), ↑(u ^ n) = ↑u ^ n
-- Mathlib.Algebra.Module.Torsion.Free
IsRegular.smul_right_inj : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {r : R} {m₁ m₂ : M}
  [Module.IsTorsionFree R M], IsRegular r → (r • m₁ = r • m₂ ↔ m₁ = m₂)
-- Mathlib.Data.Set.NAry
/-- image2 is monotone with respect to `⊆`.  -/
Set.image2_subset : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} {f : α → β → γ} {s s' : Set α} {t t' : Set β},
  s ⊆ s' → t ⊆ t' → Set.image2 f s t ⊆ Set.image2 f s' t'
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.shiftRight.inj : ∀ {m n : ℕ} {lhs : Std.Tactic.BVDecide.BVExpr m} {rhs : Std.Tactic.BVDecide.BVExpr n} {n_1 : ℕ}
  {lhs_1 : Std.Tactic.BVDecide.BVExpr m} {rhs_1 : Std.Tactic.BVDecide.BVExpr n_1},
  lhs.shiftRight rhs = lhs_1.shiftRight rhs_1 → n = n_1 ∧ lhs = lhs_1 ∧ rhs ≍ rhs_1
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
/-- **Alias** of `Order.le_cof_iff`. -/
Order.le_cof : ∀ {α : Type u} [inst : Preorder α] {c : Cardinal.{u}}, c ≤ Order.cof α ↔ ∀ (s : Set α), IsCofinal s → c ≤ Cardinal.mk ↑s
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.delabFailureId : Lean.InternalExceptionId
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instHashableSymbolKind : Hashable Lean.Lsp.SymbolKind
-- Mathlib.AlgebraicTopology.SimplicialObject.Op
SimplicialObject.opFunctorCompOpFunctorIso_hom_app_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] (X : CategoryTheory.SimplicialObject C)
  (n : SimplexCategoryᵒᵖ),
  (SimplicialObject.opFunctorCompOpFunctorIso.hom.app X).app n =
    CategoryTheory.CategoryStruct.comp SimplicialObject.opObjIso.hom SimplicialObject.opObjIso.hom
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.opEquiv_symm_apply : ∀ {X : SSet} (y : X.S), SSet.S.opEquiv.symm y = { dim := y.dim, simplex := SSet.opObjEquiv.symm y.simplex }
-- Mathlib.Data.Finset.Sym
Finset.val_sum_eq_sum_count_nsmul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : AddCommMonoid α] {n : ℕ} {k : Sym α n} {s : Finset α},
  k ∈ s.sym n → (↑k).sum = ∑ d ∈ s, Multiset.count d ↑k • d
-- Lean.Server.CodeActions.Attr
_private.Lean.Server.CodeActions.Attr.0.Lean.CodeAction.mkCommandCodeAction.unsafe_impl_2 : Lean.Name → Lean.Environment → Lean.Options → ExceptT String Id Lean.CodeAction.CommandCodeAction
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.cos_int_mul_two_pi_sub : ∀ (x : ℝ) (n : ℤ), Real.cos (↑n * (2 * Real.pi) - x) = Real.cos x
-- Mathlib.Probability.Moments.MGFAnalytic
/-- For `t ∈ interior (integrableExpSet X μ)`, the n-th derivative of `mgf X μ` at `t` is
`μ[X ^ n * exp (t * X)]`.  -/
ProbabilityTheory.iteratedDeriv_mgf : ∀ {Ω : Type u_1} {m : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω} {t : ℝ},
  t ∈ interior (ProbabilityTheory.integrableExpSet X μ) →
    ∀ (n : ℕ), iteratedDeriv n (ProbabilityTheory.mgf X μ) t = ∫ (x : Ω), (fun ω => X ω ^ n * Real.exp (t * X ω)) x ∂μ
-- Lean.Data.Lsp.CodeActions
Lean.Lsp.instToJsonCodeActionTriggerKind : Lean.ToJson Lean.Lsp.CodeActionTriggerKind
-- Mathlib.RingTheory.Polynomial.Basic
_private.Mathlib.RingTheory.Polynomial.Basic.0.MvPolynomial.prime_C_iff_of_fintype : ∀ {R : Type u} (σ : Type v) {r : R} [inst : CommRing R] [Finite σ], Prime (MvPolynomial.C r) ↔ Prime r
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_Ioo_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)] (f : (i : ι) → α i)
  (i : ι) (a : α i), Function.update f i '' Set.Ioo a (f i) = Set.Ioo (Function.update f i a) f
-- Mathlib.Topology.MetricSpace.Gluing
/-- Given two isometric embeddings `Φ : Z → X` and `Ψ : Z → Y`, we define a pseudometric space
structure on `X ⊕ Y` by declaring that `Φ x` and `Ψ x` are at distance `0`.  -/
Metric.gluePremetric : {X : Type u} →
  {Y : Type v} →
    {Z : Type w} →
      [Nonempty Z] →
        [inst : MetricSpace Z] →
          [inst_1 : MetricSpace X] →
            [inst_2 : MetricSpace Y] → {Φ : Z → X} → {Ψ : Z → Y} → Isometry Φ → Isometry Ψ → PseudoMetricSpace (X ⊕ Y)
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Subgroup.vaddInvariantMeasure : ∀ {G : Type u_3} {α : Type u_4} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (H : AddSubgroup G),
  MeasureTheory.VAddInvariantMeasure (↥H) α μ