mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₁₂.D₂.eq_1 : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₁₂] [inst_9 : CategoryTheory.Preadditive C₄]
  (F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂))
  (G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)) [inst_10 : F₁₂.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_12 : G.Additive]
  [inst_13 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9}
  {ι₁₂ : Type u_10} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : K₁.HasMapBifunctor K₂ F₁₂ c₁₂] [inst_18 : DecidableEq ι₁₂]
  [inst_19 : (K₁.mapBifunctor K₂ F₁₂ c₁₂).HasMapBifunctor K₃ G c₄]
  [inst_20 : HomologicalComplex.HasGoodTrifunctor₁₂Obj F₁₂ G K₁ K₂ K₃ c₁₂ c₄] (j j' : ι₄),
  HomologicalComplex.mapBifunctor₁₂.D₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ j j' =
    HomologicalComplex.mapBifunctor₁₂.mapBifunctor₁₂Desc fun i₁ i₂ i₃ x =>
      HomologicalComplex.mapBifunctor₁₂.d₂ F₁₂ G K₁ K₂ K₃ c₁₂ c₄ i₁ i₂ i₃ j'
-- Mathlib.Order.SupClosed
infClosure.eq_1 : ∀ {α : Type u_3} [inst : SemilatticeInf α],
  infClosure =
    ClosureOperator.ofPred (fun s => {a | ∃ t, ∃ (ht : t.Nonempty), ↑t ⊆ s ∧ t.inf' ht id = a}) InfClosed ⋯ ⋯ ⋯
-- Lean.Meta.Sym.SynthInstance
Lean.Meta.Sym.synthInstance? : Lean.Expr → Lean.Meta.Sym.SymM (Option Lean.Expr)
-- Mathlib.Analysis.Normed.Ring.Basic
nnnorm_pow : ∀ {α : Type u_2} [inst : SeminormedRing α] [NormOneClass α] [NormMulClass α] (a : α) (n : ℕ), ‖a ^ n‖₊ = ‖a‖₊ ^ n
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map_assoc : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X}
  {G : CategoryTheory.Functor Cᵒᵖ A} (hG₀ : CategoryTheory.Presheaf.IsSheaf J₀ (F.op.comp G))
  (hG : (X : C) → CategoryTheory.Limits.IsLimit ((data X).toOneHypercover.multifork G)) {X : C} {S : J.Cover X}
  (s : CategoryTheory.Limits.Multifork (S.index G)) (i : (data X).I₀) {Z : A}
  (h : G.obj (Opposite.op (F.obj ((data X).X i))) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift✝ hG₀ hG s)
      (CategoryTheory.CategoryStruct.comp (G.map ((data X).f i).op) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux✝ hG₀ s i) h
-- Mathlib.Logic.Relation
/-- The join of a relation on a single type is a new relation for which
pairs of terms are related if there is a third term they are both
related to.  For example, if `r` is a relation representing rewrites
in a term rewriting system, then *confluence* is the property that if
`a` rewrites to both `b` and `c`, then `join r` relates `b` and `c`
(see `Relation.church_rosser`).
 -/
Relation.Join : {α : Type u_1} → (α → α → Prop) → α → α → Prop
-- Mathlib.Algebra.Group.Equiv.Opposite
AddHom.mulUnop.eq_1 : ∀ {α : Type u_3} {β : Type u_4} [inst : Add α] [inst_1 : Add β], AddHom.mulUnop = AddHom.mulOp.symm
-- Mathlib.Analysis.BoxIntegral.Partition.Filter
/-- A set `s : Set (TaggedPrepartition I)` belongs to `l.toFilterDistortioniUnion I c π₀` if
there exists a function `r : ℝⁿ → (0, ∞)` (or a constant `r` if `l.bRiemann = true`) such that `s`
contains each prepartition `π` such that `l.MemBaseSet I c r π` and `π.iUnion = π₀.iUnion`.  -/
BoxIntegral.IntegrationParams.toFilterDistortioniUnion : {ι : Type u_1} →
  [Fintype ι] →
    BoxIntegral.IntegrationParams →
      (I : BoxIntegral.Box ι) → NNReal → BoxIntegral.Prepartition I → Filter (BoxIntegral.TaggedPrepartition I)
-- Mathlib.RingTheory.Localization.NumDen
IsFractionRing.den.congr_simp : ∀ (A : Type u_1) [inst : CommRing A] [inst_1 : IsDomain A] [inst_2 : UniqueFactorizationMonoid A] {K : Type u_2}
  [inst_3 : Field K] [inst_4 : Algebra A K] [inst_5 : IsFractionRing A K] (x x_1 : K),
  x = x_1 → IsFractionRing.den A x = IsFractionRing.den A x_1
-- Mathlib.Order.BooleanAlgebra.Set
Set.ite_empty_right : ∀ {α : Type u_1} (t s : Set α), t.ite s ∅ = s ∩ t
-- Mathlib.SetTheory.Ordinal.FixedPoint
Ordinal.nfpFamily_monotone : ∀ {ι : Type u_1} {f : ι → Ordinal.{u} → Ordinal.{u}} [Small.{u, u_1} ι],
  (∀ (i : ι), Monotone (f i)) → Monotone (Ordinal.nfpFamily f)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.aeval_C : ∀ {R : Type u_1} {R' : Type u_2} [inst : CommRing R] [inst_1 : CommRing R'] [inst_2 : Algebra R R'] (x : R') (n : ℤ),
  (Polynomial.aeval x) (Polynomial.Chebyshev.C R n) = Polynomial.eval x (Polynomial.Chebyshev.C R' n)
-- Mathlib.Algebra.Group.Pointwise.Set.Card
Cardinal.mk_sub_le : ∀ {M : Type u_2} [inst : SubNegMonoid M] {s t : Set M}, Cardinal.mk ↑(s - t) ≤ Cardinal.mk ↑s * Cardinal.mk ↑t
-- Init.Data.UInt.Lemmas
UInt32.sub_mul : ∀ {a b c : UInt32}, (a - b) * c = a * c - b * c
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
CategoryTheory.Abelian.epi_of_mono_of_epi_of_mono' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 2} (φ : R₁ ⟶ R₂),
  R₁.Exact →
    R₂.map' 0 2 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_2
          CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1 =
        0 →
      CategoryTheory.Mono
          (R₂.map' 0 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_9
            CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6) →
        CategoryTheory.Epi
            (CategoryTheory.ComposableArrows.app' φ 1 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_6) →
          CategoryTheory.Mono
              (CategoryTheory.ComposableArrows.app' φ 2 CategoryTheory.Abelian.mono_of_epi_of_epi_mono'._proof_1) →
            CategoryTheory.Epi
              (CategoryTheory.ComposableArrows.app' φ 0 CategoryTheory.Abelian.mono_of_epi_of_mono_of_mono'._proof_2)
-- Mathlib.Topology.Order.ScottTopology
Topology.IsScott.isOpen_iff_isUpperSet_and_scottHausdorff_open : ∀ {α : Type u_1} {D : Set (Set α)} [inst : Preorder α] [inst_1 : TopologicalSpace α] {s : Set α} [Topology.IsScott α D],
  IsOpen s ↔ IsUpperSet s ∧ IsOpen s
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.inter.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (m₁ m₁_1 : Std.ExtHashMap α β),
  m₁ = m₁_1 → ∀ (m₂ m₂_1 : Std.ExtHashMap α β), m₂ = m₂_1 → m₁.inter m₂ = m₁_1.inter m₂_1
-- Mathlib.Combinatorics.SimpleGraph.Coloring.EdgeLabeling
/-- Compose an edge-labeling with a function on the color set.  -/
SimpleGraph.EdgeLabeling.compRight : {V : Type u_1} →
  {G : SimpleGraph V} → {K : Type u_3} → {K' : Type u_4} → G.EdgeLabeling K → (K → K') → G.EdgeLabeling K'
-- Mathlib.Data.Part
Part.assert_defined : ∀ {α : Type u_1} {p : Prop} {f : p → Part α} (h : p), (f h).Dom → (Part.assert p f).Dom
-- Mathlib.GroupTheory.Sylow
/-- If the kernel of `f : H →* G` is a `p`-group,
then `Finite (Sylow p G)` implies `Finite (Sylow p H)`.  -/
Sylow.finite_of_ker_is_pGroup : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {H : Type u_2} [inst_1 : Group H] {f : H →* G},
  IsPGroup p ↥f.ker → ∀ [Finite (Sylow p G)], Finite (Sylow p H)
-- Mathlib.Algebra.Group.Subsemigroup.Operations
AddSubsemigroup.mem_map_equiv : ∀ {M : Type u_1} {N : Type u_2} [inst : Add M] [inst_1 : Add N] {f : M ≃+ N} {K : AddSubsemigroup M} {x : N},
  x ∈ AddSubsemigroup.map (↑f) K ↔ f.symm x ∈ K
-- Mathlib.Topology.Metrizable.CompletelyMetrizable
/-- The product of two completely metrizable spaces is completely metrizable.  -/
TopologicalSpace.IsCompletelyMetrizableSpace.prod : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [TopologicalSpace.IsCompletelyMetrizableSpace X]
  [inst_2 : TopologicalSpace Y] [TopologicalSpace.IsCompletelyMetrizableSpace Y],
  TopologicalSpace.IsCompletelyMetrizableSpace (X × Y)
-- Aesop.Forward.Match.Types
Aesop.Match.instToMessageData : Lean.ToMessageData Aesop.Match
-- Init.Data.Vector.Find
Vector.findSome?_replicate_of_isSome : ∀ {α : Type u_1} {α_1 : Type u_2} {f : α → Option α_1} {n : ℕ} {a : α},
  (f a).isSome = true → Vector.findSome? f (Vector.replicate n a) = if n = 0 then none else f a
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
/-- A subgroupoid is wide if its carrier set is all of `C`.  -/
CategoryTheory.Subgroupoid.IsWide : {C : Type u} → [inst : CategoryTheory.Groupoid C] → CategoryTheory.Subgroupoid C → Prop
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.coeff_neg : ∀ {k : Type u_1} {G : Type u_2} [inst : AddGroup k] (a : SkewMonoidAlgebra k G), (-a).coeff = -a.coeff
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.instCompleteLattice : {Ω : Type u_1} →
  {ι : Type u_2} → {m : MeasurableSpace Ω} → [inst : Preorder ι] → CompleteLattice (MeasureTheory.Filtration ι m)
-- Mathlib.Algebra.Polynomial.Mirror
Polynomial.mirror_eq_iff : ∀ {R : Type u_1} [inst : Semiring R] {p q : Polynomial R}, p.mirror = q ↔ p = q.mirror
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.getD_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashSet α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  {k fallback : α}, (m₁ \ m₂).getD k fallback = if k ∈ m₂ then fallback else m₁.getD k fallback
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
StarAlgebra.elemental.eq_1 : ∀ (R : Type u_1) {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : IsSemitopologicalSemiring A] [inst_6 : ContinuousStar A]
  [inst_7 : Algebra R A] [inst_8 : StarModule R A] (x : A),
  StarAlgebra.elemental R x = (StarAlgebra.adjoin R {x}).topologicalClosure
-- Mathlib.CategoryTheory.Limits.Comma
/-- Let `F : J ⥤ Comma L R`. If `L` preserves the colimit of
`F ⋙ fst _ _`, then `Comma.fst L R` and `Comma.snd L R` jointly
reflect the colimit of `F`, i.e. if `c` is a cocone for `F` which
becomes a colimit after applying `Comma.fst L R` and `Comma.snd L R`,
then `c` is a colimit.  -/
CategoryTheory.Comma.fstSndJointlyReflectColimit : {J : Type w} →
  [inst : CategoryTheory.Category.{w', w} J] →
    {A : Type u₁} →
      [inst_1 : CategoryTheory.Category.{v₁, u₁} A] →
        {B : Type u₂} →
          [inst_2 : CategoryTheory.Category.{v₂, u₂} B] →
            {T : Type u₃} →
              [inst_3 : CategoryTheory.Category.{v₃, u₃} T] →
                {L : CategoryTheory.Functor A T} →
                  {R : CategoryTheory.Functor B T} →
                    {F : CategoryTheory.Functor J (CategoryTheory.Comma L R)} →
                      {c : CategoryTheory.Limits.Cocone F} →
                        [CategoryTheory.Limits.PreservesColimit (F.comp (CategoryTheory.Comma.fst L R)) L] →
                          CategoryTheory.Limits.IsColimit ((CategoryTheory.Comma.fst L R).mapCocone c) →
                            CategoryTheory.Limits.IsColimit ((CategoryTheory.Comma.snd L R).mapCocone c) →
                              CategoryTheory.Limits.IsColimit c
-- Mathlib.Analysis.Seminorm
/-- Seminorm-balls at the origin are absorbent.  -/
Seminorm.absorbent_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {r : ℝ}, 0 < r → Absorbent 𝕜 (p.ball 0 r)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
/-- The truncated cast `ENNReal.truncateToReal t : ℝ≥0∞ → ℝ` is monotone when `t ≠ ∞`.  -/
ENNReal.monotone_truncateToReal : ∀ {t : ENNReal}, t ≠ ⊤ → Monotone t.truncateToReal
-- Init.Data.String.Basic
String.toRawSubstring'.eq_1 : ∀ (s : String), s.toRawSubstring' = s.toRawSubstring
-- Batteries.Data.String.Lemmas
String.Pos.Raw.extract.go₂_add_right_cancel : ∀ (s : List Char) (i e n : ℕ),
  String.Pos.Raw.extract.go₂ s { byteIdx := i + n } { byteIdx := e + n } =
    String.Pos.Raw.extract.go₂ s { byteIdx := i } { byteIdx := e }
-- Mathlib.Data.Finsupp.Single
Finsupp.single_apply_eq_zero : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] {a x : α} {b : M}, (fun₀ | a => b) x = 0 ↔ x = a → b = 0
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.Hom.instInhabited : (X : Bipointed) → Inhabited (X.Hom X)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1.stepAux.match_1.eq_6 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Inhabited Γ]
  (motive : Turing.TM1.Stmt Γ Λ σ → σ → Turing.Tape Γ → Sort u_4) (v : σ) (T : Turing.Tape Γ)
  (h_1 :
    (d : Turing.Dir) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.move d q) v T)
  (h_2 :
    (a : Γ → σ → Γ) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.write a q) v T)
  (h_3 :
    (s : Γ → σ → σ) →
      (q : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.load s q) v T)
  (h_4 :
    (p : Γ → σ → Bool) →
      (q₁ q₂ : Turing.TM1.Stmt Γ Λ σ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.branch p q₁ q₂) v T)
  (h_5 : (l : Γ → σ → Λ) → (v : σ) → (T : Turing.Tape Γ) → motive (Turing.TM1.Stmt.goto l) v T)
  (h_6 : (v : σ) → (T : Turing.Tape Γ) → motive Turing.TM1.Stmt.halt v T),
  (match Turing.TM1.Stmt.halt, v, T with
    | Turing.TM1.Stmt.move d q, v, T => h_1 d q v T
    | Turing.TM1.Stmt.write a q, v, T => h_2 a q v T
    | Turing.TM1.Stmt.load s q, v, T => h_3 s q v T
    | Turing.TM1.Stmt.branch p q₁ q₂, v, T => h_4 p q₁ q₂ v T
    | Turing.TM1.Stmt.goto l, v, T => h_5 l v T
    | Turing.TM1.Stmt.halt, v, T => h_6 v T) =
    h_6 v T
-- Init.Data.String.Pattern.Pred
String.Slice.Pattern.CharPred.Decidable.instToForwardSearcherForallCharPropDefaultForwardSearcherForallBoolDecide : {p : Char → Prop} →
  [inst : DecidablePred p] →
    String.Slice.Pattern.ToForwardSearcher p
      (String.Slice.Pattern.ToForwardSearcher.DefaultForwardSearcher fun x => decide (p x))
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.ExpLog.Order
CFC.tendsto_ite_cfc_rpow_sub_one_ite_log : ∀ {A : Type u_1} [inst : CStarAlgebra A] [inst_1 : PartialOrder A] [StarOrderedRing A],
  Filter.Tendsto (fun p a => if a ∈ {b | IsStrictlyPositive b} then cfc (fun x => p⁻¹ * (x ^ p - 1)) a else 0)
    (nhdsWithin 0 (Set.Ioi 0)) (nhds fun a => if a ∈ {b | IsStrictlyPositive b} then CFC.log a else 0)
-- Mathlib.RingTheory.Congruence.Defs
RingConGen.Rel.below.of : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop}
  {motive : (a a_1 : R) → RingConGen.Rel r a a_1 → Prop} (x y : R) (a : r x y), RingConGen.Rel.below ⋯
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_le_mk_iff_dvd : ∀ {M : Type u_1} [inst : CommMonoid M] {a b : M}, Associates.mk a ≤ Associates.mk b ↔ a ∣ b
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.insertMany_emptyWithCapacity_list_nil : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α],
  ↑(Std.DHashMap.Internal.Raw₀.emptyWithCapacity.insertMany []) = Std.DHashMap.Internal.Raw₀.emptyWithCapacity
-- Mathlib.Order.Interval.Finset.Defs
Finset.mem_Icc' : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] {a b x : α}, x ∈ Finset.Icc a b ↔ x ≤ b ∧ a ≤ x
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.singleFunctor_map_comp_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] [inst_3 : HasDerivedCategory C] {X Y Z : C} (f : X ⟶ Y) {n : ℕ}
  (x : CategoryTheory.Abelian.Ext Y Z n),
  CategoryTheory.CategoryStruct.comp ((DerivedCategory.singleFunctor C 0).map f) x.hom =
    ((CategoryTheory.Abelian.Ext.mk₀ f).comp x ⋯).hom
-- Mathlib.Algebra.Group.Subsemigroup.Basic
AddSubsemigroup.closure_iUnion : ∀ {M : Type u_1} [inst : Add M] {ι : Sort u_3} (s : ι → Set M),
  AddSubsemigroup.closure (⋃ i, s i) = ⨆ i, AddSubsemigroup.closure (s i)
-- Init.System.ST
EST.Out.ok.sizeOf_spec : ∀ {ε σ α : Type} [inst : SizeOf ε] [inst_1 : SizeOf σ] [inst_2 : SizeOf α] (a : α) (a_1 : Void σ),
  sizeOf (EST.Out.ok a a_1) = 1 + sizeOf a + sizeOf a_1
-- Init.Data.Range.Polymorphic.PRange
Std.Rio.mk.injEq : ∀ {α : Type u} (upper upper_1 : α), ((*...upper) = *...upper_1) = (upper = upper_1)
-- Mathlib.AlgebraicTopology.DoldKan.Projections
AlgebraicTopology.DoldKan.Q_zero : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {X : CategoryTheory.SimplicialObject C}, AlgebraicTopology.DoldKan.Q 0 = 0
-- Init.Data.Int.Basic
Int.ofNat.injEq : ∀ (a a_1 : ℕ), (Int.ofNat a = Int.ofNat a_1) = (a = a_1)
-- Mathlib.Algebra.Colimit.Module
Module.DirectLimit.module : {R : Type u_1} →
  [inst : Semiring R] →
    {ι : Type u_2} →
      [inst_1 : Preorder ι] →
        (G : ι → Type u_3) →
          [inst_2 : (i : ι) → AddCommMonoid (G i)] →
            [inst_3 : (i : ι) → Module R (G i)] →
              (f : (i j : ι) → i ≤ j → G i →ₗ[R] G j) → [inst_4 : DecidableEq ι] → Module R (Module.DirectLimit G f)
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.gcd_dvd : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R),
  EuclideanDomain.gcd a b ∣ a ∧ EuclideanDomain.gcd a b ∣ b
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.IsCycle.cycleOf_eq : ∀ {α : Type u_2} {f : Equiv.Perm α} {x : α} [inst : DecidableRel f.SameCycle], f.IsCycle → f x ≠ x → f.cycleOf x = f
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.discard_apply : ∀ {α : Type u_1} {mα : MeasurableSpace α} (a : α),
  (ProbabilityTheory.Kernel.discard α) a = MeasureTheory.Measure.dirac PUnit.unit
-- Mathlib.Order.Lattice
SemilatticeInf.ext : ∀ {α : Type u_1} {A B : SemilatticeInf α}, (∀ (y x : α), y ≤ x ↔ y ≤ x) → A = B
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_add_const_Iic : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a b : α),
  (fun x => x + a) ⁻¹' Set.Iic b = Set.Iic (b - a)
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.instTypeNameInlayHintState : TypeName Lean.Server.FileWorker.InlayHintState
-- Mathlib.SetTheory.Ordinal.Univ
Ordinal.lift_univ : Ordinal.lift.{w, max (u + 1) v} Ordinal.univ.{u, v} = Ordinal.univ.{u, max v w}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.contains_insertIfNew : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k a : α} {v : β k}, (m.insertIfNew k v).contains a = (k == a || m.contains a)
-- Mathlib.Algebra.Algebra.Tower
/-- Any `f : A →ₐ[R] B` is also an `S`-algebra homomorphism if the `R`-algebra structure on
`A` and `B` factors via a surjective ring homomorphism `R →+* S`.  -/
AlgHom.extendScalarsHomOfSurjective : {R : Type u} →
  {S : Type v} →
    {A : Type w} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Semiring A] →
            [inst_3 : Algebra R S] →
              [inst_4 : Algebra S A] →
                [inst_5 : Algebra R A] →
                  [IsScalarTower R S A] → Function.Surjective ⇑(algebraMap R S) → (A →ₐ[R] A) ≃* (A →ₐ[S] A)
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.LawfulBackwardPatternModel.toLawfulBackwardPattern : ∀ {ρ : Type} {pat : ρ} {inst : String.Slice.Pattern.BackwardPattern pat}
  {inst_1 : String.Slice.Pattern.Model.PatternModel pat}
  [self : String.Slice.Pattern.Model.LawfulBackwardPatternModel pat], String.Slice.Pattern.LawfulBackwardPattern pat
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.mkTerminalAction : Lean.Syntax → Lean.Elab.Term.Do.CodeBlock
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.denote_mul : ∀ (ctx : Int.Internal.Linear.Context) (p : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.Poly.denote ctx (p.mul k) = k * Int.Internal.Linear.Poly.denote ctx p
-- Mathlib.Data.Nat.Hyperoperation
_private.Mathlib.Data.Nat.Hyperoperation.0.hyperoperation.match_1.eq_5 : ∀ (motive : ℕ → ℕ → ℕ → Sort u_1) (n m k : ℕ) (h_1 : (x k : ℕ) → motive 0 x k) (h_2 : (m : ℕ) → motive 1 m 0)
  (h_3 : (x : ℕ) → motive 2 x 0) (h_4 : (n x : ℕ) → motive n.succ.succ.succ x 0)
  (h_5 : (n m k : ℕ) → motive n.succ m k.succ),
  (match n.succ, m, k.succ with
    | 0, x, k => h_1 x k
    | 1, m, 0 => h_2 m
    | 2, x, 0 => h_3 x
    | n.succ.succ.succ, x, 0 => h_4 n x
    | n.succ, m, k.succ => h_5 n m k) =
    h_5 n m k
-- Mathlib.CategoryTheory.Grothendieck
CategoryTheory.Grothendieck.pre_comp_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {F : CategoryTheory.Functor C CategoryTheory.Cat} (G : CategoryTheory.Functor D C)
  {H : CategoryTheory.Functor C CategoryTheory.Cat} (α : F ⟶ H),
  (CategoryTheory.Grothendieck.pre F G).comp (CategoryTheory.Grothendieck.map α) =
    (CategoryTheory.Grothendieck.map (G.whiskerLeft α)).comp (CategoryTheory.Grothendieck.pre H G)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_alter : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] {k k' : α} [inst_4 : Inhabited β] {f : Option β → Option β},
  m.WF →
    Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.Const.alter m k f) k' =
      if (k == k') = true then (f (Std.DHashMap.Raw.Const.get? m k)).get! else Std.DHashMap.Raw.Const.get! m k'
-- Mathlib.LinearAlgebra.TensorProduct.Graded.Internal
/-- The casting equivalence to move between regular and graded tensor products.  -/
GradedTensorProduct.of : (R : Type u_1) →
  {ι : Type u_2} →
    {A : Type u_3} →
      {B : Type u_4} →
        [inst : CommSemiring ι] →
          [inst_1 : DecidableEq ι] →
            [inst_2 : CommRing R] →
              [inst_3 : Ring A] →
                [inst_4 : Ring B] →
                  [inst_5 : Algebra R A] →
                    [inst_6 : Algebra R B] →
                      (𝒜 : ι → Submodule R A) →
                        (ℬ : ι → Submodule R B) →
                          [inst_7 : GradedAlgebra 𝒜] →
                            [inst_8 : GradedAlgebra ℬ] → TensorProduct R A B ≃ₗ[R] GradedTensorProduct R 𝒜 ℬ
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivativeFinsupp_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (p : Polynomial R) (f : R →+* S),
  Polynomial.derivativeFinsupp (Polynomial.map f p) =
    Finsupp.mapRange (fun x => Polynomial.map f x) ⋯ (Polynomial.derivativeFinsupp p)
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.Hom.comp_τ₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} (φ₁₂ : S₁.Hom S₂) (φ₂₃ : S₂.Hom S₃),
  (φ₁₂.comp φ₂₃).τ₃ = CategoryTheory.CategoryStruct.comp φ₁₂.τ₃ φ₂₃.τ₃
-- Init.Data.SInt.Lemmas
ISize.toBitVec_toUSize : ∀ (x : ISize), x.toUSize.toBitVec = x.toBitVec