mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Array.Basic
_private.Init.Data.Array.Basic.0.Array.mapM.map : {α : Type u} → {β : Type v} → {m : Type v → Type w} → [Monad m] → (α → m β) → Array α → ℕ → Array β → m (Array β)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.valuation_apply_eq_ofVal : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  (x : WithVal v), (WithVal.valuation v) x = v x.ofVal
-- Mathlib.Topology.ContinuousMap.ZeroAtInfty
ZeroAtInftyContinuousMap.instAddZeroClass : {α : Type u} →
  {β : Type v} →
    [inst : TopologicalSpace α] →
      [inst_1 : TopologicalSpace β] →
        [inst_2 : AddZeroClass β] → [ContinuousAdd β] → AddZeroClass (ZeroAtInftyContinuousMap α β)
-- Std.Data.HashSet.Raw
Std.HashSet.Raw.WF.inter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α}, m₁.WF → m₂.WF → (m₁ ∩ m₂).WF
-- Mathlib.CategoryTheory.Monoidal.Discrete
CategoryTheory.Discrete.addMonoidalFunctorMonoidal : {M : Type u} →
  [inst : AddMonoid M] →
    {N : Type u'} → [inst_1 : AddMonoid N] → (F : M →+ N) → (CategoryTheory.Discrete.addMonoidalFunctor F).Monoidal
-- Mathlib.NumberTheory.ArithmeticFunction.Moebius
ArithmeticFunction.moebius_ne_zero_iff_eq_or : ∀ {n : ℕ}, ArithmeticFunction.moebius n ≠ 0 ↔ ArithmeticFunction.moebius n = 1 ∨ ArithmeticFunction.moebius n = -1
-- Mathlib.Combinatorics.Matroid.Basic
Matroid.IsBasis.union_isBasis_union : ∀ {α : Type u_1} {M : Matroid α} {I J X Y : Set α},
  M.IsBasis I X → M.IsBasis J Y → M.Indep (I ∪ J) → M.IsBasis (I ∪ J) (X ∪ Y)
-- Mathlib.CategoryTheory.Functor.OfSequence
_private.Mathlib.CategoryTheory.Functor.OfSequence.0.CategoryTheory.Functor.OfSequence.map.match_3.eq_1 : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{u_1, u_2} C]
  (motive : (x : ℕ → C) → ((n : ℕ) → x n ⟶ x (n + 1)) → ℕ → ℕ → Sort u_3) (x : ℕ → C) (x_1 : (n : ℕ) → x n ⟶ x (n + 1))
  (h_1 : (x : ℕ → C) → (x_2 : (n : ℕ) → x n ⟶ x (n + 1)) → motive x x_2 0 0)
  (h_2 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → motive x f 0 1)
  (h_3 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → (l : ℕ) → motive x f 0 l.succ)
  (h_4 : (x : ℕ → C) → (x_2 : (n : ℕ) → x n ⟶ x (n + 1)) → (n : ℕ) → motive x x_2 n.succ 0)
  (h_5 : (x : ℕ → C) → (f : (n : ℕ) → x n ⟶ x (n + 1)) → (k l : ℕ) → motive x f k.succ l.succ),
  (match x, x_1, 0, 0 with
    | x, x_2, 0, 0 => h_1 x x_2
    | x, f, 0, 1 => h_2 x f
    | x, f, 0, l.succ => h_3 x f l
    | x, x_2, n.succ, 0 => h_4 x x_2 n
    | x, f, k.succ, l.succ => h_5 x f k l) =
    h_1 x x_1
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.subset : ∀ {α : Type u_1} {M : Matroid α} {X Y : Set α}, M.IsRkFinite X → Y ⊆ X → M.IsRkFinite Y
-- Mathlib.Topology.Algebra.Module.LinearPMap
LinearPMap.IsClosable.closure_mono : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup E] [inst_2 : AddCommGroup F]
  [inst_3 : Module R E] [inst_4 : Module R F] [inst_5 : TopologicalSpace E] [inst_6 : TopologicalSpace F]
  [inst_7 : ContinuousAdd E] [inst_8 : ContinuousAdd F] [inst_9 : TopologicalSpace R] [inst_10 : ContinuousSMul R E]
  [inst_11 : ContinuousSMul R F] {f g : E →ₗ.[R] F}, g.IsClosable → f ≤ g → f.closure ≤ g.closure
-- Mathlib.CategoryTheory.Adjunction.Limits
CategoryTheory.Adjunction.isEquivalence_preservesColimits : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : CategoryTheory.Functor C D) [E.IsEquivalence],
  CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} E
-- Init.Grind.AC
Lean.Grind.AC.diseq_simp_lhs_middle : ∀ {α : Sort u_1} (ctx : Lean.Grind.AC.Context α) {x : Std.Associative ctx.op}
  (lhs₁ rhs₁ head tail lhs₂ rhs₂ lhs₂' : Lean.Grind.AC.Seq),
  Lean.Grind.AC.simp_middle_cert lhs₁ rhs₁ head tail lhs₂ lhs₂' = true →
    Lean.Grind.AC.Seq.denote ctx lhs₁ = Lean.Grind.AC.Seq.denote ctx rhs₁ →
      Lean.Grind.AC.Seq.denote ctx lhs₂ ≠ Lean.Grind.AC.Seq.denote ctx rhs₂ →
        Lean.Grind.AC.Seq.denote ctx lhs₂' ≠ Lean.Grind.AC.Seq.denote ctx rhs₂
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_emod_unique' : ∀ {a b r q : ℤ}, b < 0 → (a / b = q ∧ a % b = r ↔ r + b * q = a ∧ 0 ≤ r ∧ r < -b)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
isAddCyclic_of_surjective : ∀ {G : Type u_2} {G' : Type u_3} [inst : AddGroup G] [inst_1 : AddGroup G'] {F : Type u_4} [hH : IsAddCyclic G']
  [inst_2 : FunLike F G' G] [AddMonoidHomClass F G' G] (f : F), Function.Surjective ⇑f → IsAddCyclic G
-- Mathlib.Tactic.Translate.ToAdditive
/-- Environment extension used for guessing the translation of a name.  -/
Mathlib.Tactic.ToAdditive.guessNameExt : Mathlib.Tactic.GuessName.GuessNameExt
-- Mathlib.Algebra.MvPolynomial.Equiv
_private.Mathlib.Algebra.MvPolynomial.Equiv.0.Option.elim.match_1.eq_2 : ∀ {α : Type u_1} {β : Sort u_3} (motive : Option α → β → (α → β) → Sort u_2) (y : β) (x : α → β)
  (h_1 : (x : α) → (x_1 : β) → (f : α → β) → motive (some x) x_1 f) (h_2 : (y : β) → (x : α → β) → motive none y x),
  (match none, y, x with
    | some x, x_1, f => h_1 x x_1 f
    | none, y, x => h_2 y x) =
    h_2 y x
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.Basic
/-- If `C` is an abelian category, we shall say that it satisfies `IsGrothendieckAbelian.{w} C`
if it is locally small (relative to `w`), has exact filtered colimits of size `w` (AB5) and has a
separator.
If `[Category.{v} C]` and `w = v`, this means that `C` satisfies `AB5` and has a separator;
general results about Grothendieck abelian categories can be
reduced to this case using the instance `ShrinkHoms.isGrothendieckAbelian` below.

The introduction of the auxiliary universe `w` shall be needed for certain
applications to categories of sheaves. That the present definition still preserves essential
properties of Grothendieck categories is ensured by `IsGrothendieckAbelian.of_equivalence`,
which shows that every instance for `C` implies an instance for `ShrinkHoms C` with hom sets in
`Type w`.
 -/
CategoryTheory.IsGrothendieckAbelian : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → Prop
-- Init.GrindInstances.ToInt
Lean.Grind.instOfNatIntIi : Lean.Grind.ToInt.OfNat ℤ Lean.Grind.IntInterval.ii
-- Mathlib.CategoryTheory.Monad.Limits
CategoryTheory.Monad.ForgetCreatesLimits.newCone_π_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {T : CategoryTheory.Monad C} {J : Type u}
  [inst_1 : CategoryTheory.Category.{v, u} J] (D : CategoryTheory.Functor J T.Algebra)
  (c : CategoryTheory.Limits.Cone (D.comp T.forget)) (X : J),
  (CategoryTheory.Monad.ForgetCreatesLimits.newCone D c).π.app X =
    CategoryTheory.CategoryStruct.comp (T.map (c.π.app X)) (D.obj X).a
-- Mathlib.Logic.Small.Defs
Shrink.ext : ∀ {α : Type v} [inst : Small.{w, v} α] {x y : Shrink.{w, v} α}, (equivShrink α).symm x = (equivShrink α).symm y → x = y
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_append_size_add' : ∀ {a b : ByteArray} {i j k : ℕ}, k = a.size → (a ++ b).extract (k + i) (k + j) = b.extract i j
-- Lean.Compiler.IR.CompilerM
Lean.IR.log : Lean.IR.LogEntry → Lean.IR.CompilerM Unit
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Split.Hom.mk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {S₁ S₂ : CategoryTheory.SimplicialObject.Split C}
  (F F_1 : S₁.X ⟶ S₂.X) (e_F : F = F_1) (f f_1 : (n : ℕ) → S₁.s.N n ⟶ S₂.s.N n) (e_f : f = f_1)
  (comm :
    ∀ (n : ℕ),
      CategoryTheory.CategoryStruct.comp (S₁.s.ι n) (F.app (Opposite.op { len := n })) =
        CategoryTheory.CategoryStruct.comp (f n) (S₂.s.ι n)),
  { F := F, f := f, comm := comm } = { F := F_1, f := f_1, comm := ⋯ }
-- Mathlib.Combinatorics.Quiver.Symmetric
/-- The inclusion of a quiver in its symmetrification  -/
Quiver.Symmetrify.of : {V : Type u_2} → [inst : Quiver V] → V ⥤q Quiver.Symmetrify V
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
CochainComplex.mappingCone.shiftIso.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {K L : CochainComplex C ℤ} (φ : K ⟶ L) (n : ℤ),
  CochainComplex.mappingCone.shiftIso φ n =
    {
      hom :=
        CochainComplex.mappingCone.lift ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)
          (n.negOnePow • (CochainComplex.mappingCone.fst φ).shift n) ((CochainComplex.mappingCone.snd φ).shift n) ⋯,
      inv :=
        CochainComplex.mappingCone.desc ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map φ)
          (n.negOnePow • (CochainComplex.mappingCone.inl φ).shift n)
          ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).map (CochainComplex.mappingCone.inr φ)) ⋯,
      hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.Topology.ContinuousOn
ContinuousOn.mono : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s t : Set α},
  ContinuousOn f s → t ⊆ s → ContinuousOn f t
-- Lean.Meta.Tactic.Grind.Types
/-- Invokes model-based theory combination extensions in all registered solvers.  -/
Lean.Meta.Grind.Solvers.mbtc : Lean.Meta.Grind.GoalM Bool
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
MvPolynomial.IsSymmetric.smul : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] {φ : MvPolynomial σ R} (r : R),
  φ.IsSymmetric → (r • φ).IsSymmetric
-- Lean.Meta.KExprMap
Lean.Meta.KExprMap.mk.injEq : ∀ {α : Type} (map map_1 : Lean.PHashMap Lean.HeadIndex (Lean.AssocList Lean.Expr α)),
  ({ map := map } = { map := map_1 }) = (map = map_1)
-- Lean.Compiler.IR.Basic
Lean.IR.instInhabitedAlt.default_1 : Lean.IR.Alt
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.Monomial.majorized_tail_toFun_head : ∀ {t : Tactic.ComputeAsymptotics.Monomial} {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis},
  List.length t.unit = List.length basis_tl →
    Tactic.ComputeAsymptotics.WellFormedBasis (basis_hd :: basis_tl) →
      Tactic.ComputeAsymptotics.Majorized (t.toFun basis_tl) basis_hd 0
-- Mathlib.Algebra.Group.Pointwise.Finset.Interval
Finset.Ico_mul_Icc_subset' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : PartialOrder α] [inst_2 : DecidableEq α] [MulLeftStrictMono α]
  [MulRightStrictMono α] [inst_5 : LocallyFiniteOrder α] (a b c d : α),
  Finset.Ico a b * Finset.Icc c d ⊆ Finset.Ico (a * c) (b * d)
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
lt_div_iff_mul_lt' : ∀ {α : Type u} [inst : CommGroup α] [inst_1 : LT α] [MulLeftStrictMono α] {a b c : α}, b < c / a ↔ a * b < c
-- Init.Data.Array.Monadic
Array.toList_filterRevM : ∀ {m : Type → Type u_1} {α : Type} [inst : Monad m] [LawfulMonad m] {xs : Array α} {p : α → m Bool},
  Array.toList <$> Array.filterRevM p xs = List.filterRevM p xs.toList
-- Mathlib.NumberTheory.DirichletCharacter.GaussSum
/-- If `χ` is a primitive character, then the function `a ↦ gaussSum χ (e.mulShift a)`, for any
fixed additive character `e`, is a constant multiple of `χ⁻¹`.  -/
gaussSum_mulShift_of_isPrimitive : ∀ {N : ℕ} [inst : NeZero N] {R : Type u_1} [inst_1 : CommRing R] (e : AddChar (ZMod N) R) [IsDomain R]
  {χ : DirichletCharacter R N}, χ.IsPrimitive → ∀ (a : ZMod N), gaussSum χ (e.mulShift a) = χ⁻¹ a * gaussSum χ e
-- Init.Grind.Ring.Envelope
Lean.Grind.Ring.OfSemiring.zero_mul : ∀ {α : Type u} [inst : Lean.Grind.Semiring α] (a : Lean.Grind.Ring.OfSemiring.Q α),
  Lean.Grind.Ring.OfSemiring.mul (Lean.Grind.Ring.OfSemiring.natCast 0) a = Lean.Grind.Ring.OfSemiring.natCast 0
-- Init.Core
/-- Prove that `α` is a subsingleton by showing that any two elements are equal.  -/
Subsingleton.intro : ∀ {α : Sort u}, (∀ (a b : α), a = b) → Subsingleton α
-- Mathlib.Analysis.Seminorm
Seminorm.instIsSMulApplyReal : ∀ {R : Type u_1} {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddGroup E] [inst_2 : SMul 𝕜 E]
  [inst_3 : SMul R ℝ] [inst_4 : SMul R NNReal] [inst_5 : IsScalarTower R NNReal ℝ], IsSMulApply R (Seminorm 𝕜 E) E ℝ
-- Mathlib.Order.Interval.Finset.Defs
Finset.Ioo_orderDual_def : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] (a b : αᵒᵈ),
  Finset.Ioo a b = Finset.map OrderDual.toDual.toEmbedding (Finset.Ioo (OrderDual.ofDual b) (OrderDual.ofDual a))
-- Mathlib.Data.List.Forall2
List.SublistForall₂.cons : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop} {a₁ : α} {a₂ : β} {l₁ : List α} {l₂ : List β},
  R a₁ a₂ → List.SublistForall₂ R l₁ l₂ → List.SublistForall₂ R (a₁ :: l₁) (a₂ :: l₂)
-- Mathlib.GroupTheory.GroupAction.Defs
MulAction.orbit_smul : ∀ {G : Type u_1} {α : Type u_2} [inst : Group G] [inst_1 : MulAction G α] (g : G) (a : α),
  MulAction.orbit G (g • a) = MulAction.orbit G a
-- Init.Data.SInt.Lemmas
Int32.mul_succ : ∀ {a b : Int32}, a * (b + 1) = a * b + a
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.infinitePos_mul_infinitePos : ∀ {x y : ℝ*}, x.InfinitePos → y.InfinitePos → (x * y).InfinitePos
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.ext_iff : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι}, I = J ↔ ∀ (x : ι → ℝ), x ∈ I ↔ x ∈ J
-- Lean.Meta.Sym.DSimp.DSimpM
Lean.Meta.Sym.dsimp : Lean.Expr →
  optParam Lean.Meta.Sym.DSimp.Methods { } → optParam Lean.Meta.Sym.DSimp.Config { } → Lean.Meta.Sym.SymM Lean.Expr
-- Mathlib.Dynamics.BirkhoffSum.NormedSpace
/-- **Alias** of `isClosed_setOfPred_tendsto_birkhoffAverage`.

---

If `f : X → X` is a non-strictly contracting map (i.e., it is Lipschitz with constant `1`),
`g : X → E` is a uniformly continuous, and `l : X → E` is a continuous function,
then the set of points `x`
such that the Birkhoff average of `g` along the orbit of `x` tends to `l x`
is a closed set.  -/
isClosed_setOf_tendsto_birkhoffAverage : ∀ (𝕜 : Type u_1) {X : Type u_2} {E : Type u_3} [inst : PseudoEMetricSpace X] [inst_1 : RCLike 𝕜]
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : X → X} {g l : X → E},
  LipschitzWith 1 f →
    UniformContinuous g →
      Continuous l → IsClosed {x | Filter.Tendsto (fun x_1 => birkhoffAverage 𝕜 f g x_1 x) Filter.atTop (nhds (l x))}
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
tprod_singleton : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] (b : β) (f : β → α),
  ∏' (x : ↑{b}), f ↑x = f b
-- Mathlib.RingTheory.Localization.Submodule
IsLocalization.coeSubmodule_bot : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Type u_2) [inst_1 : CommSemiring S] [inst_2 : Algebra R S],
  IsLocalization.coeSubmodule S ⊥ = ⊥
-- Mathlib.RingTheory.TensorProduct.Quotient
Algebra.TensorProduct.quotIdealMapEquivTensorQuot_mk : ∀ {A : Type u_1} (B : Type u_2) [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (I : Ideal A) (b : B),
  (Algebra.TensorProduct.quotIdealMapEquivTensorQuot B I) ((Ideal.Quotient.mk (Ideal.map (algebraMap A B) I)) b) =
    b ⊗ₜ[A] 1
-- Mathlib.Algebra.Symmetrized
SymAlg.instSub : {α : Type u_1} → [Sub α] → Sub αˢʸᵐ
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv.congr_simp : ∀ {α : Type u_3} {γ : Type u_4} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ κ_1 : ProbabilityTheory.Kernel α γ),
  κ = κ_1 →
    ∀ (η η_1 : ProbabilityTheory.Kernel α γ),
      η = η_1 → ∀ (a a_1 : α), a = a_1 → ∀ (x x_1 : γ), x = x_1 → κ.rnDeriv η a x = κ_1.rnDeriv η_1 a_1 x_1
-- Mathlib.Algebra.Module.LocalizedModule.Basic
LocalizedModule.mk_smul_mk : ∀ {R : Type u} [inst : CommSemiring R] {S : Submonoid R} {M : Type v} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (r : R) (m : M) (s t : ↥S), Localization.mk r s • LocalizedModule.mk m t = LocalizedModule.mk (r • m) (s * t)
-- Mathlib.Order.Interval.Set.UnorderedInterval
Set.uIcc_injective_left : ∀ {α : Type u_1} [inst : DistribLattice α] (a : α), Function.Injective (Set.uIcc a)
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.apply_lt_top : ∀ {α : Type u_1} (p : PMF α) (a : α), p a < ⊤
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.kerCompPreimage.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_3} {T : Type u_7} [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T]
  [inst_6 : IsScalarTower R S T] (Q : Algebra.Generators S T ι') (P : Algebra.Generators R S ι) (x : ↥Q.ker),
  Q.kerCompPreimage P x =
    ⟨(↑x).coeff.sum fun n r =>
        (MvPolynomial.rename Sum.inr) (P.σ r) * (MvPolynomial.monomial (Finsupp.mapDomain Sum.inl n)) 1,
      ⋯⟩
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context.fType : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.App.Context → Lean.Expr
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- The inclusion functor of the category of sheaves in the category of presheaves.  -/
CategoryTheory.sheafToPresheaf : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (J : CategoryTheory.GrothendieckTopology C) →
      (A : Type u₂) →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} A] →
          CategoryTheory.Functor (CategoryTheory.Sheaf J A) (CategoryTheory.Functor Cᵒᵖ A)
-- Mathlib.Algebra.Category.MonCat.Basic
MonCat.oneHom_apply : ∀ (X Y : MonCat) (x : ↑X), (MonCat.Hom.hom 1) x = 1
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.PushforwardContinuous
SheafOfModules.pushforward_map_val : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {J : CategoryTheory.GrothendieckTopology C} {K : CategoryTheory.GrothendieckTopology D}
  {F : CategoryTheory.Functor C D} {S : CategoryTheory.Sheaf J RingCat} {R : CategoryTheory.Sheaf K RingCat}
  [inst_2 : F.IsContinuous J K] (φ : S ⟶ (F.sheafPushforwardContinuous RingCat J K).obj R) {X Y : SheafOfModules R}
  (f : X ⟶ Y), ((SheafOfModules.pushforward φ).map f).val = (PresheafOfModules.pushforward φ.hom).map f.val
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
CategoryTheory.Limits.cokernelIsoOfEq_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  {f g h : X ⟶ Y} [inst_2 : CategoryTheory.Limits.HasCokernel f] [inst_3 : CategoryTheory.Limits.HasCokernel g]
  [inst_4 : CategoryTheory.Limits.HasCokernel h] (w₁ : f = g) (w₂ : g = h),
  CategoryTheory.Limits.cokernelIsoOfEq w₁ ≪≫ CategoryTheory.Limits.cokernelIsoOfEq w₂ =
    CategoryTheory.Limits.cokernelIsoOfEq ⋯
-- Init.Data.Option.Lemmas
Option.ext_iff : ∀ {α : Type u_1} {o₁ o₂ : Option α}, o₁ = o₂ ↔ ∀ (a : α), o₁ = some a ↔ o₂ = some a
-- Mathlib.Algebra.Order.GroupWithZero.Defs
PosMulReflectLT.toMulPosReflectLT : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : Preorder α] [IsMulCommutative α] [PosMulReflectLT α],
  MulPosReflectLT α
-- Mathlib.CategoryTheory.Triangulated.Basic
/-- The identity triangle morphism.
 -/
CategoryTheory.Pretriangulated.triangleMorphismId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.HasShift C ℤ] →
      (T : CategoryTheory.Pretriangulated.Triangle C) → CategoryTheory.Pretriangulated.TriangleMorphism T T
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddRightCancelSemigroup.eq_1 : ∀ {α : Type u_1} [inst : AddLeftCancelSemigroup α],
  AddOpposite.instAddRightCancelSemigroup = { toAddSemigroup := AddOpposite.instAddSemigroup, toIsRightCancelAdd := ⋯ }
-- Lean.Expr
/-- Return `some e'` if `e` is of the form `optParam _ e'`  -/
Lean.Expr.getOptParamDefault? : Lean.Expr → Option Lean.Expr
-- Mathlib.CategoryTheory.MorphismProperty.Composition
CategoryTheory.MorphismProperty.instHasTwoOutOfThreePropertyInverseImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (F : CategoryTheory.Functor C D) (W : CategoryTheory.MorphismProperty D) [W.HasTwoOutOfThreeProperty],
  (W.inverseImage F).HasTwoOutOfThreeProperty
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
CategoryTheory.Abelian.SpectralObject.liftCycles_i_assoc : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  (X : CategoryTheory.Abelian.SpectralObject C ι) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k) (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁)
  {A : C} (x : A ⟶ (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g))
  (hx : CategoryTheory.CategoryStruct.comp x (X.δ f g n₀ n₁ hn₁) = 0) {Z : C}
  (h : (X.H n₀).obj (CategoryTheory.ComposableArrows.mk₁ g) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (X.liftCycles f g n₀ n₁ hn₁ x hx)
      (CategoryTheory.CategoryStruct.comp (X.iCycles f g n₀) h) =
    CategoryTheory.CategoryStruct.comp x h
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgHom.map_adjoin : ∀ {F : Type u_1} (R : Type u) (A : Type v) {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] [inst_7 : IsScalarTower R A A] [inst_8 : SMulCommClass R A A]
  [inst_9 : IsScalarTower R B B] [inst_10 : SMulCommClass R B B] (f : F) (s : Set A),
  NonUnitalSubalgebra.map f (NonUnitalAlgebra.adjoin R s) = NonUnitalAlgebra.adjoin R (⇑f '' s)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.recoverSkipWith : Array Lean.Syntax → Lean.Parser.ParserFn → Lean.Parser.ParserFn
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.opcyclesMapIso'_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} (e : S₁ ≅ S₂) (h₁ : S₁.RightHomologyData) (h₂ : S₂.RightHomologyData),
  (CategoryTheory.ShortComplex.opcyclesMapIso' e h₁ h₂).hom = CategoryTheory.ShortComplex.opcyclesMap' e.hom h₁ h₂
-- Lean.Meta.Sym.AlphaShareBuilder
Lean.Meta.Sym.Internal.mkForallS : {m : Type → Type} →
  [Lean.Meta.Sym.Internal.MonadShareCommon m] →
    [Monad m] → Lean.Name → Lean.BinderInfo → Lean.Expr → Lean.Expr → m Lean.Expr
-- Mathlib.Algebra.Opposites
MulOpposite.unop.eq_1 : ∀ {α : Type u_1}, MulOpposite.unop = PreOpposite.unop'
-- Mathlib.CategoryTheory.Localization.Predicate
CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ_lift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (W : CategoryTheory.MorphismProperty C) (E : Type u_3)
  [inst_1 : CategoryTheory.Category.{v_3, u_3} E] (G : CategoryTheory.Functor C E) (hG : W.IsInvertedBy G),
  (CategoryTheory.Localization.strictUniversalPropertyFixedTargetQ W E).lift G hG =
    CategoryTheory.Localization.Construction.lift G hG
-- Mathlib.Topology.FiberBundle.Basic
/-- The inclusion of a fiber into the total space is a continuous map.  -/
FiberBundleCore.continuous_totalSpaceMk : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (b : B), Continuous (Bundle.TotalSpace.mk b)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_union_of_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₂ → k ∈ m₁ ∪ m₂
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Pred
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Pred.0.Std.Tactic.BVDecide.BVPred.bitblast.match_7.eq_1 : ∀ (motive : Std.Tactic.BVDecide.BVPred → Sort u_1) (w : ℕ) (lhs : Std.Tactic.BVDecide.BVExpr w)
  (op : Std.Tactic.BVDecide.BVBinPred) (rhs : Std.Tactic.BVDecide.BVExpr w)
  (h_1 :
    (w : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinPred) →
          (rhs : Std.Tactic.BVDecide.BVExpr w) → motive (Std.Tactic.BVDecide.BVPred.bin lhs op rhs))
  (h_2 :
    (w : ℕ) → (expr : Std.Tactic.BVDecide.BVExpr w) → (idx : ℕ) → motive (Std.Tactic.BVDecide.BVPred.getLsbD expr idx)),
  (match Std.Tactic.BVDecide.BVPred.bin lhs op rhs with
    | Std.Tactic.BVDecide.BVPred.bin lhs op rhs => h_1 w lhs op rhs
    | Std.Tactic.BVDecide.BVPred.getLsbD expr idx => h_2 w expr idx) =
    h_1 w lhs op rhs