mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {S' : C} {p : S' ⟶ S} {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S'}
  {α : ι' → ι} {p' : (j : ι') → X' j ⟶ X (α j)}
  (w : ∀ (j : ι'), CategoryTheory.CategoryStruct.comp (p' j) (f (α j)) = CategoryTheory.CategoryStruct.comp (f' j) p)
  (D : F.DescentData f) (j : ι'),
  (CategoryTheory.Pseudofunctor.DescentData.pullFunctorObj w D).obj j =
    (F.map (p' j).op.toLoc).toFunctor.obj (D.obj (α j))
-- Mathlib.Topology.MetricSpace.HolderNorm
nnHolderNorm_const : ∀ (X : Type u_1) {Y : Type u_2} [inst : PseudoEMetricSpace X] [inst_1 : PseudoEMetricSpace Y] (r : NNReal) (c : Y),
  nnHolderNorm r (Function.const X c) = 0
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.action_actionHomRight : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (y : D) (z : C) {x x' : C} (f : x ⟶ x'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj y z) f =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso y z x).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight y
          (CategoryTheory.MonoidalCategoryStruct.whiskerLeft z f))
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso y z x').hom)
-- Lean.Meta.Tactic.Grind.Intro
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.IntroResult.done.inj : ∀ {goal goal_1 : Lean.Meta.Grind.Goal},
  Lean.Meta.Grind.IntroResult.done✝ goal = Lean.Meta.Grind.IntroResult.done✝ goal_1 → goal = goal_1
-- Mathlib.Algebra.Homology.LeftResolution.Reduced
CategoryTheory.Abelian.LeftResolution.karoubi.F'_obj_X : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : CategoryTheory.Preadditive A] (X : A),
  ((CategoryTheory.Abelian.LeftResolution.karoubi.F' Λ).obj X).X = Λ.F.obj X
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.RciSliceData.treeMap : {α : Type u} →
  {β : α → Type v} → [inst : Ord α] → Std.DTreeMap.Internal.RciSliceData α β → Std.DTreeMap.Internal.Impl α β
-- Mathlib.Algebra.Homology.HomologySequence
HomologicalComplex.HomologySequence.snakeInput_v₁₂ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {c : ComplexShape ι} {S : CategoryTheory.ShortComplex (HomologicalComplex C c)} (hS : S.ShortExact) (i j : ι)
  (hij : c.Rel i j),
  (HomologicalComplex.HomologySequence.snakeInput hS i j hij).v₁₂ =
    S.mapNatTrans (HomologicalComplex.natTransOpCyclesToCycles C c i j)
-- Mathlib.Topology.GDelta.Basic
/-- A countable union of meagre sets is meagre.  -/
isMeagre_iUnion : ∀ {X : Type u_1} {ι' : Sort u_4} [inst : TopologicalSpace X] [Countable ι'] {f : ι' → Set X},
  (∀ (i : ι'), IsMeagre (f i)) → IsMeagre (⋃ i, f i)
-- Mathlib.Order.Monotone.Monovary
AntivaryOn.comp_antitoneOn_right : ∀ {ι : Type u_1} {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder α] [inst_1 : LinearOrder β]
  [inst_2 : Preorder γ] {f : ι → α} {g : ι → β} {g' : β → γ} {s : Set ι},
  AntivaryOn f g s → AntitoneOn g' (g '' s) → MonovaryOn f (g' ∘ g) s
-- Lean.Parser.Extra
/-- No-op parser that advises the pretty printer to emit a hard line break.  -/
Lean.Parser.ppLine : Lean.Parser.Parser
-- Mathlib.Analysis.SpecialFunctions.Gamma.Deligne
/-- Reformulation of the reflection formula in terms of `Gammaℝ`.  -/
Complex.Gammaℝ_one_sub_mul_Gammaℝ_one_add : ∀ (s : ℂ), (1 - s).Gammaℝ * (1 + s).Gammaℝ = (Complex.cos (↑Real.pi * s / 2))⁻¹
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.transpose_zero : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] (B : E →L[ℝ] F →L[ℝ] G), MeasureTheory.VectorMeasure.transpose 0 B = 0
-- Mathlib.CategoryTheory.Limits.Constructions.Filtered
/-- The `liftToFinset` functor, precomposed with forming a colimit, is a coproduct on the original
functor.  -/
CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinsetColimIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {α : Type w} →
      [inst_1 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        [inst_2 : CategoryTheory.Limits.HasColimitsOfShape (Finset (CategoryTheory.Discrete α)) C] →
          [inst_3 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C] →
            (CategoryTheory.Limits.CoproductsFromFiniteFiltered.liftToFinset C α).comp CategoryTheory.Limits.colim ≅
              CategoryTheory.Limits.colim
-- Mathlib.AlgebraicTopology.SimplicialSet.HoFunctorMonoidal
SSet.Truncated.HomotopyCategory.BinaryProduct.iso_hom_toFunctor : ∀ (X Y : SSet.Truncated 2),
  (SSet.Truncated.HomotopyCategory.BinaryProduct.iso X Y).hom.toFunctor =
    SSet.Truncated.HomotopyCategory.BinaryProduct.functor X Y
-- Mathlib.GroupTheory.Coprod.Basic
/-- Coproduct of two monoids or groups.  -/
Monoid.Coprod : (M : Type u_1) → (N : Type u_2) → [MulOneClass M] → [MulOneClass N] → Type (max u_1 u_2)
-- Plausible.Gen
/-- Execute a `Gen` until it actually produces an output. May diverge for bad generators!  -/
Plausible.Gen.runUntil : {α : Type} → optParam (Option ℕ) none → Plausible.Gen α → ℕ → IO α
-- Init.SizeOf
Substring.Raw.mk.sizeOf_spec : ∀ (str : String) (startPos stopPos : String.Pos.Raw),
  sizeOf { str := str, startPos := startPos, stopPos := stopPos } = 1 + sizeOf str + sizeOf startPos + sizeOf stopPos
-- Mathlib.Algebra.Algebra.Subalgebra.Basic
Subalgebra.toSubring_subtype : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] (S : Subalgebra R A),
  S.toSubring.subtype = ↑S.val
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.InhabitedColimitType : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J CommRingCat) → Inhabited (CommRingCat.Colimits.ColimitType F)
-- Lean.Meta.Tactic.Grind.EMatch
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.applyAssignment.go.eq_def : ∀ (mvars : Array Lean.Expr) (numParams i : ℕ),
  Lean.Meta.Grind.EMatch.applyAssignment.go✝ mvars numParams i =
    if h : i < mvars.size then
      have bidx := numParams - i - 1;
      do
      let __do_lift ← get
      have v : Lean.Expr := __do_lift.assignment[bidx]!
      have __do_jp : Unit → OptionT (StateT Lean.Meta.Grind.EMatch.Choice Lean.Meta.Grind.EMatch.M) Unit := fun __r =>
        Lean.Meta.Grind.EMatch.applyAssignment.go✝ mvars numParams (i + 1)
      if Lean.Meta.Sym.isSameExpr v Lean.Meta.Grind.EMatch.delayedEqProof✝ = true then do
          let __r ← Lean.Meta.Grind.EMatch.processDelayed✝ mvars i h
          __do_jp __r
        else
          if (!Lean.Meta.Sym.isSameExpr v Lean.Meta.Grind.EMatch.unassigned✝) = true then do
            let __r ← Lean.Meta.Grind.EMatch.processUnassigned✝ mvars i v h
            __do_jp __r
          else __do_jp ()
    else pure ()
-- Mathlib.Data.Int.Basic
Int.dvd_natCast : ∀ {m : ℤ} {n : ℕ}, m ∣ ↑n ↔ m.natAbs ∣ n
-- Mathlib.Data.List.OfFn
List.forall_mem_ofFn_iff : ∀ {α : Type u} {n : ℕ} {f : Fin n → α} {P : α → Prop}, (∀ i ∈ List.ofFn f, P i) ↔ ∀ (j : Fin n), P (f j)
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isLittleO_principal : ∀ {α : Type u_1} {F' : Type u_7} {E'' : Type u_9} [inst : SeminormedAddCommGroup F'] [inst_1 : NormedAddCommGroup E'']
  {g' : α → F'} {f'' : α → E''} {s : Set α}, f'' =o[Filter.principal s] g' ↔ ∀ x ∈ s, f'' x = 0
-- Init.Data.Array.Basic
Array.instMembership : {α : Type u} → Membership α (Array α)
-- Init.Data.Rat.Lemmas
Rat.intCast_neg_iff : ∀ {a : ℤ}, ↑a < 0 ↔ a < 0
-- Mathlib.Algebra.Group.Basic
zero_sub_add_zero_sub_rev : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a b : α), 0 - a + (0 - b) = 0 - (b + a)
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
Metric.ball_eq_singleton_of_subsingleton : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x : α} {ε : ℝ} [Subsingleton α], 0 < ε → Metric.ball x ε = {x}
-- Mathlib.Topology.Algebra.Group.Basic
MonoidHom.isOpenQuotientMap_iff_isQuotientMap : ∀ {A : Type u_1} [inst : Group A] [inst_1 : TopologicalSpace A] [ContinuousMul A] {B : Type u_2} [inst_3 : Group B]
  [inst_4 : TopologicalSpace B] {F : Type u_3} [inst_5 : FunLike F A B] [MonoidHomClass F A B] {φ : F},
  IsOpenQuotientMap ⇑φ ↔ Topology.IsQuotientMap ⇑φ
-- Mathlib.CategoryTheory.Sites.Point.Map
/-- The image of a point of a site by a cocontinuous functor.  -/
CategoryTheory.GrothendieckTopology.Point.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {J : CategoryTheory.GrothendieckTopology C} →
          J.Point →
            (F : CategoryTheory.Functor C D) →
              (K : CategoryTheory.GrothendieckTopology D) →
                [F.IsCocontinuous J K] → [CategoryTheory.LocallySmall.{w, v', u'} D] → K.Point
-- Mathlib.Topology.Separation.Hausdorff
isIrreducible_iff_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T2Space X] {S : Set X}, IsIrreducible S ↔ ∃ x, S = {x}
-- Mathlib.Tactic.Algebra.Basic
/-- Evaluate the product of two normalized expressions in `R` using `ring`.  -/
Mathlib.Tactic.Algebra.RingCompute.mul : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} →
      {sR : Q(CommSemiring «$R»)} →
        {sA : Q(CommSemiring «$A»)} →
          (sAlg : Q(Algebra «$R» «$A»)) →
            Mathlib.Tactic.Ring.Common.Cache sR →
              {a b : Q(«$A»)} →
                Mathlib.Tactic.Algebra.BaseType sAlg a →
                  Mathlib.Tactic.Algebra.BaseType sAlg b →
                    Lean.MetaM (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Algebra.BaseType sAlg) q(«$a» * «$b»))
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_ofBitVec : ∀ (n : BitVec System.Platform.numBits) (h : System.Platform.numBits = 64),
  { toBitVec := n }.toBitVec64 h = BitVec.cast h n
-- Mathlib.Data.ENNReal.Operations
ENNReal.lt_add_of_sub_lt_right : ∀ {a b c : ENNReal}, a ≠ ⊤ ∨ c ≠ ⊤ → a - c < b → a < b + c
-- Batteries.Data.List.Basic
_private.Batteries.Data.List.Basic.0.List.takeWhile₂.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α × List β → Sort u_3) (as' : List α) (bs' : List β)
  (h_1 : (as' : List α) → (bs' : List β) → motive (as', bs')),
  (match (as', bs') with
    | (as', bs') => h_1 as' bs') =
    h_1 as' bs'
-- Init.Data.BitVec.Bitblast
BitVec.sdiv_intMin : ∀ {w : ℕ} {x : BitVec w}, x.sdiv (BitVec.intMin w) = if x = BitVec.intMin w then 1#w else 0#w
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.size_ofList_le : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α},
  (Std.ExtHashSet.ofList l).size ≤ l.length
-- Mathlib.Order.ConditionallyCompletePartialOrder.Basic
sup_eq_top_of_top_mem : ∀ {α : Type u_1} [inst : ConditionallyCompletePartialOrderSup α] {s : Set α} [inst_1 : OrderTop α], ⊤ ∈ s → sSup s = ⊤
-- Std.Time.Format.Modifier
Std.Time.Modifier.y.injEq : ∀ (presentation presentation_1 : Std.Time.Year),
  (Std.Time.Modifier.y presentation = Std.Time.Modifier.y presentation_1) = (presentation = presentation_1)
-- Mathlib.Analysis.Matrix.PosDef
Matrix.PosDef.re_dotProduct_pos : ∀ {n : Type u_2} {𝕜 : Type u_3} [inst : Fintype n] [inst_1 : RCLike 𝕜] {A : Matrix n n 𝕜},
  A.PosDef → ∀ {x : n → 𝕜}, x ≠ 0 → 0 < RCLike.re (star x ⬝ᵥ A.mulVec x)
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.π_comp_eqToHom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u_1} (f : J → C)
  [inst_1 : CategoryTheory.Limits.HasProduct f] {j j' : J} (w : j = j') {Z : C} (h : f j' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.π f j') h
-- Mathlib.Data.Finset.BooleanAlgebra
Finset.compl_filter : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] (p : α → Prop) [inst_2 : DecidablePred p]
  [inst_3 : (x : α) → Decidable ¬p x], (Finset.filter p Finset.univ)ᶜ = {x | ¬p x}
-- Lean.Widget.InteractiveDiagnostic
/-- Nested tags denote `Info` objects in `infos`.  -/
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.code : Lean.Elab.ContextInfo → Std.TreeMap ℕ Lean.Elab.Info compare → Lean.Widget.EmbedFmt✝
-- Std.Internal.Parsec.Basic
Std.Internal.Parsec.Input.next : {ι : Type} →
  {elem idx : outParam Type} →
    {inst : DecidableEq idx} → {inst_1 : DecidableEq elem} → [self : Std.Internal.Parsec.Input ι elem idx] → ι → ι
-- Mathlib.CategoryTheory.Join.Basic
CategoryTheory.Join.inclRight_obj : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (a : D), (CategoryTheory.Join.inclRight C D).obj a = CategoryTheory.Join.right a
-- Init.Data.String.Lemmas.Pattern.String.ForwardPattern
String.Slice.Pattern.ForwardSliceSearcher.skipPrefix?.fun_cases_unfolding : ∀ (pat s : String.Slice) (motive : Option s.Pos → Prop),
  (String.Slice.Pattern.ForwardSliceSearcher.startsWith pat s = true →
      motive (some (s.pos! (pat.rawEndPos.offsetBy s.startPos.offset)))) →
    (¬String.Slice.Pattern.ForwardSliceSearcher.startsWith pat s = true → motive none) →
      motive (String.Slice.Pattern.ForwardSliceSearcher.skipPrefix? pat s)
-- Lean.Elab.Match
/-- Creates syntax for a fresh `h : `-notation annotation for a discriminant, copying source
information from an existing annotation `stx`.  -/
_private.Lean.Elab.Match.0.Lean.Elab.Term.mkFreshDiscrIdentFrom : Lean.Syntax → Lean.CoreM Lean.Ident
-- Mathlib.Algebra.Group.Submonoid.Defs
/-- `SubmonoidClass S M` says `S` is a type of subsets `s ≤ M` that contain `1`
and are closed under `(*)`  -/
SubmonoidClass : (S : Type u_3) → (M : outParam (Type u_4)) → [MulOneClass M] → [SetLike S M] → Prop
-- Mathlib.RingTheory.Polynomial.Bernstein
bernsteinPolynomial.eq_1 : ∀ (R : Type u_1) [inst : CommRing R] (n ν : ℕ),
  bernsteinPolynomial R n ν = ↑(n.choose ν) * Polynomial.X ^ ν * (1 - Polynomial.X) ^ (n - ν)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_eq_getKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {a fallback : α} {h : a ∈ t}, t.getKey a h = t.getKeyD a fallback
-- Mathlib.Algebra.Star.Subalgebra
StarAlgebra.adjoin_le : ∀ {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : Algebra R A] [inst_4 : StarRing A] [inst_5 : StarModule R A] {S : StarSubalgebra R A} {s : Set A},
  s ⊆ ↑S → StarAlgebra.adjoin R s ≤ S
-- Mathlib.Topology.CWComplex.Classical.Subcomplex
/-- **Alias** of `Topology.RelCWComplex.Subcomplex.finiteType_subcomplex_of_finiteType`. -/
Topology.CWComplex.Subcomplex.finiteType_subcomplex_of_finiteType : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : T2Space X] [inst_1 : Topology.RelCWComplex C D]
  [Topology.RelCWComplex.FiniteType C] (E : Topology.RelCWComplex.Subcomplex C), Topology.RelCWComplex.FiniteType ↑E
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsFundamentalDomain.measure_eq_tsum : ∀ {G : Type u_1} {α : Type u_3} [inst : Group G] [inst_1 : MulAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstSMul G α] [MeasureTheory.SMulInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsFundamentalDomain G s μ → ∀ (t : Set α), μ t = ∑' (g : G), μ (g • t ∩ s)
-- Mathlib.CategoryTheory.Sites.Descent.Precoverage
CategoryTheory.Pseudofunctor.DescentData.isEquivalence_toDescentData_of_sieve_le : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat)
  {J : CategoryTheory.GrothendieckTopology C} [F.IsPrestack J] {ι : Type t} {S : C} {X : ι → C} {f : (i : ι) → X i ⟶ S}
  {ι' : Type t'} {X' : ι' → C} {f' : (j : ι') → X' j ⟶ S},
  CategoryTheory.Sieve.ofArrows X' f' ∈ J S →
    CategoryTheory.Sieve.ofArrows X' f' ≤ CategoryTheory.Sieve.ofArrows X f →
      ∀ [(F.toDescentData f').IsEquivalence], (F.toDescentData f).IsEquivalence
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Functor.FullyFaithful.addMonObj_zero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D} [inst_4 : F.OplaxMonoidal] (hF : F.FullyFaithful) (X : C)
  [inst_5 : CategoryTheory.AddMonObj (F.obj X)],
  CategoryTheory.AddMonObj.zero =
    hF.preimage
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OplaxMonoidal.η F) CategoryTheory.AddMonObj.zero)
-- Mathlib.Data.Setoid.Basic
Setoid.comap_id : ∀ {α : Type u_1} (c : Setoid α), Setoid.comap id c = c
-- Lean.Data.PersistentHashMap
Lean.PersistentHashMap.root : {α : Type u} →
  {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Lean.PersistentHashMap α β → Lean.PersistentHashMap.Node α β
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof.oneNeZero : Lean.Meta.Grind.Arith.Linear.DiseqCnstrProof
-- Mathlib.Order.Sublocale
Sublocale.carrier.instHImp : {X : Type u_1} → [inst : Order.Frame X] → {S : Sublocale X} → HImp ↥S
-- Mathlib.GroupTheory.Congruence.Hom
Con.map.eq_1 : ∀ {M : Type u_1} [inst : MulOneClass M] (c d : Con M) (h : c ≤ d), c.map d h = c.lift d.mk' ⋯
-- Mathlib.Logic.Equiv.Set
Equiv.image_eq_preimage_symm : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) (s : Set α), ⇑e '' s = ⇑e.symm ⁻¹' s
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.hom_zsum : ∀ {V W : SemiNormedGrp} (n : ℤ) (f : V ⟶ W), SemiNormedGrp.Hom.hom (n • f) = n • SemiNormedGrp.Hom.hom f
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.weight.eq_1 : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommRing R] (k : ℕ) (t : Finset σ × σ),
  MvPolynomial.NewtonIdentities.weight✝ σ R k t =
    (-1) ^ t.1.card * ((∏ a ∈ t.1, MvPolynomial.X a) * MvPolynomial.X t.2 ^ (k - t.1.card))
-- Init.Data.List.Nat.Modify
List.length_modifyTailIdx : ∀ {α : Type u_1} (f : List α → List α),
  (∀ (l : List α), (f l).length = l.length) → ∀ (l : List α) (i : ℕ), (l.modifyTailIdx i f).length = l.length
-- Mathlib.Algebra.Category.GrpWithZero
/-- Construct a bundled `GrpWithZero` from a `GroupWithZero`.  -/
GrpWithZero.of : (carrier : Type u_1) → [str : GroupWithZero carrier] → GrpWithZero
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extend.mapX_none : ∀ {ι : Type u_1} {c : ComplexShape ι} {C : Type u_3} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K L : HomologicalComplex C c} (φ : K ⟶ L) {i : Option ι}, i = none → HomologicalComplex.extend.mapX φ i = 0
-- Std.Time.Date.Basic
/-- Convert `Week.Offset` into `Minute.Offset`.
 -/
Std.Time.Minute.Offset.ofWeeks : Std.Time.Week.Offset → Std.Time.Minute.Offset
-- Mathlib.Algebra.Ring.Subsemiring.Defs
Subsemiring.coe_carrier_toSubmonoid : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R), s.carrier = ↑s
-- Batteries.Data.MLList.Basic
/-- Construct a `MLList` by iteration. (`m` must be a stateful monad for this to be useful.)  -/
MLList.iterate : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → m α → MLList m α
-- Mathlib.Order.CountableDenseLinearOrder
/-- Any countable linear order embeds in any nontrivial dense linear order.  -/
Order.embedding_from_countable_to_dense : ∀ (α : Type u_1) (β : Type u_2) [inst : LinearOrder α] [inst_1 : LinearOrder β] [Countable α] [DenselyOrdered β]
  [Nontrivial β], Nonempty (α ↪o β)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.topEquiv_apply : ∀ {M : Type u_5} [inst : AddZeroClass M] (x : ↥⊤), AddSubmonoid.topEquiv x = ↑x
-- Mathlib.Probability.Kernel.Category.SFinKer
SFinKer.whiskerLeft_hom : ∀ (X Y₁ Y₂ : SFinKer) (κ : Y₁ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X κ).hom = ProbabilityTheory.Kernel.id.parallelComp κ.hom
-- Mathlib.Combinatorics.Enumerative.InclusionExclusion
/-- **Inclusion-exclusion principle** for the sum of a function over a union.

The sum of a function `f` over the union of the `S i` over `i ∈ s` is the alternating sum of the
sums of `f` over the intersections of the `S i`.  -/
Finset.inclusion_exclusion_sum_biUnion : ∀ {ι : Type u_1} {α : Type u_2} {G : Type u_3} [inst : AddCommGroup G] [inst_1 : DecidableEq α] (s : Finset ι)
  (S : ι → Finset α) (f : α → G), ∑ a ∈ s.biUnion S, f a = ∑ t, (-1) ^ ((↑t).card + 1) • ∑ a ∈ (↑t).inf' ⋯ S, f a
-- Mathlib.NumberTheory.ModularForms.JacobiTheta.OneVariable
jacobiTheta_S_smul : ∀ (τ : UpperHalfPlane), jacobiTheta ↑(ModularGroup.S • τ) = (-Complex.I * ↑τ) ^ (1 / 2) * jacobiTheta ↑τ
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_nonneg : ∀ {x : ℝ}, 0 ≤ x → 0 ≤ Real.artanh x
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.instHasRightCalculusOfFractionsIsoModSerre : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (P : CategoryTheory.ObjectProperty C) [inst_2 : P.IsSerreClass], P.isoModSerre.HasRightCalculusOfFractions
-- Init.Data.List.ToArray
List.push_append_toArray : ∀ {α : Type u_1} {as : Array α} {a : α} {bs : List α}, as.push a ++ bs.toArray = as ++ (a :: bs).toArray
-- Init.Data.UInt.Lemmas
UInt16.ofNat_mod_size : ∀ {x : ℕ}, UInt16.ofNat (x % 2 ^ 16) = UInt16.ofNat x
-- Mathlib.Topology.Algebra.ValuativeRel.ValuativeTopology
Valuation.discreteTopology_of_forall_map_eq_one : ∀ {R : Type u_1} [inst : Ring R] [inst_1 : ValuativeRel R] {Γ₀ : Type u_3} [inst_2 : LinearOrderedCommGroupWithZero Γ₀]
  [_t : TopologicalSpace R] [IsValuativeTopology R] (v : Valuation R Γ₀) [v.Compatible],
  (∀ (x : R), x ≠ 0 → v x = 1) → DiscreteTopology R
-- Mathlib.Topology.SmallInductiveDimension
smallInductiveDimension_le : ∀ (X : Type u_1) [inst : TopologicalSpace X] (n : ℕ) [H : HasSmallInductiveDimensionLE X n],
  smallInductiveDimension X ≤ ↑n
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.log_exp : ∀ (x : ℝ), Real.log (Real.exp x) = x
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.Hom.mk.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {D₁ D₂ : F.DescentData f} (hom hom_1 : (i : ι) → D₁.obj i ⟶ D₂.obj i)
  (e_hom : hom = hom_1)
  (comm :
    ∀ ⦃Y : C⦄ (q : Y ⟶ S) ⦃i₁ i₂ : ι⦄ (f₁ : Y ⟶ X i₁) (f₂ : Y ⟶ X i₂)
      (hf₁ : CategoryTheory.CategoryStruct.comp f₁ (f i₁) = q) (hf₂ : CategoryTheory.CategoryStruct.comp f₂ (f i₂) = q),
      CategoryTheory.CategoryStruct.comp ((F.map f₁.op.toLoc).toFunctor.map (hom i₁)) (D₂.hom q f₁ f₂ ⋯ ⋯) =
        CategoryTheory.CategoryStruct.comp (D₁.hom q f₁ f₂ ⋯ ⋯) ((F.map f₂.op.toLoc).toFunctor.map (hom i₂))),
  { hom := hom, comm := comm } = { hom := hom_1, comm := ⋯ }