mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.castNum.match_1.eq_2 : ∀ (motive : Num → Sort u_1) (p : PosNum) (h_1 : Unit → motive Num.zero) (h_2 : (p : PosNum) → motive (Num.pos p)),
  (match Num.pos p with
    | Num.zero => h_1 ()
    | Num.pos p => h_2 p) =
    h_2 p
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.OplaxFunctor.mapComp'.congr_simp : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {b₀ b₁ b₂ : B} (f : b₀ ⟶ b₁) (g : b₁ ⟶ b₂) (fg : b₀ ⟶ b₂)
  (h : CategoryTheory.CategoryStruct.comp f g = fg), F.mapComp' f g fg h = F.mapComp' f g fg h
-- Mathlib.Order.BooleanSubalgebra
/-- A Boolean subalgebra of a lattice inherits a bottom element.  -/
BooleanSubalgebra.instBotCoe : {α : Type u_2} → [inst : BooleanAlgebra α] → {L : BooleanSubalgebra α} → Bot ↥L
-- Mathlib.CategoryTheory.Category.ULift
CategoryTheory.down_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : CategoryTheory.AsSmall C} (f : X ⟶ Y) (g : Y ⟶ Z),
  (CategoryTheory.CategoryStruct.comp f g).down = CategoryTheory.CategoryStruct.comp f.down g.down
-- Init.Data.Iterators.PostconditionMonad
Std.Iterators.PostconditionT.operation_map : ∀ {m : Type w → Type w'} [inst : Functor m] {α β : Type w} {x : Std.Iterators.PostconditionT m α} {f : α → β},
  (Std.Iterators.PostconditionT.map f x).operation = (fun a => ⟨f ↑a, ⋯⟩) <$> x.operation
-- Mathlib.Data.Set.Finite.Basic
/-- **Alias** of the forward direction of `Set.finite_def`. -/
Set.Finite.nonempty_fintype : ∀ {α : Type u} {s : Set α}, s.Finite → Nonempty (Fintype ↑s)
-- Mathlib.Algebra.FreeNonUnitalNonAssocAlgebra
FreeNonUnitalNonAssocAlgebra.of_comp_lift : ∀ (R : Type u_1) {X : Type u_2} {A : Type u_3} [inst : Semiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : IsScalarTower R A A] [inst_4 : SMulCommClass R A A] (f : X → A),
  ⇑((FreeNonUnitalNonAssocAlgebra.lift R) f) ∘ FreeNonUnitalNonAssocAlgebra.of R = f
-- Std.Do.SPred.SVal
Std.Do.SVal.GetTy.mk : {σ : Type u} → {σs : List (Type u)} → Std.Do.SVal σs σ → Std.Do.SVal.GetTy σ σs
-- Mathlib.Tactic.TermCongr
/-- Key for congruence hole metadata.
For a `Nat` recording how old this congruence hole is, to prevent reprocessing them
if they leak into the local context.  -/
_private.Mathlib.Tactic.TermCongr.0.Mathlib.Tactic.TermCongr.congrHoleIndex : Lean.Name
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.HomologyData.ofIsLimitKernelFork S hf c hc).right =
    CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc
-- Mathlib.Algebra.Category.ModuleCat.Topology.Basic
TopModuleCat.instHasLimitsOfShapeOfModuleCat : ∀ {R : Type u} [inst : Ring R] [inst_1 : TopologicalSpace R] {J : Type u_2}
  [inst_2 : CategoryTheory.Category.{v_1, u_2} J] [CategoryTheory.Limits.HasLimitsOfShape J (ModuleCat R)],
  CategoryTheory.Limits.HasLimitsOfShape J (TopModuleCat R)
-- Mathlib.Algebra.Homology.HomologySequenceLemmas
HomologicalComplex.HomologySequence.composableArrows₂.eq_1 : ∀ {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)) (i : ι),
  HomologicalComplex.HomologySequence.composableArrows₂ S i =
    CategoryTheory.ComposableArrows.mk₂ (HomologicalComplex.homologyMap S.f i) (HomologicalComplex.homologyMap S.g i)
-- Mathlib.CategoryTheory.Shift.ShiftedHom
CategoryTheory.ShiftedHom.comp_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {M : Type u_4} [inst_1 : AddMonoid M]
  [inst_2 : CategoryTheory.HasShift C M] {X Y Z : C} [inst_3 : CategoryTheory.Preadditive C]
  [∀ (a : M), (CategoryTheory.shiftFunctor C a).Additive] {a b c : M} (α : CategoryTheory.ShiftedHom X Y a)
  (β₁ β₂ : CategoryTheory.ShiftedHom Y Z b) (h : b + a = c), α.comp (β₁ + β₂) h = α.comp β₁ h + α.comp β₂ h
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_eq_self_of_le : ∀ {o₁ o₂ a : Ordinal.{u}}, o₁ ≤ o₂ → Ordinal.veblen o₂ a = a → Ordinal.veblen o₁ a = a
-- Init.System.ST
Void.nonemptyType : Type → NonemptyType
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjCyclesSelfIso_hom_naturality_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  {A B : C} (f : A ⟶ B) {Z : C} (h : B ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.cyclesMap ((HomologicalComplex.single C c j).map f) j)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j B).hom h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.addContent_accumulate : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] (m : MeasureTheory.AddContent G C),
  MeasureTheory.IsSetRing C →
    ∀ {s : ℕ → Set α},
      Pairwise (Function.onFun Disjoint s) →
        (∀ (i : ℕ), s i ∈ C) → ∀ (n : ℕ), m (Set.accumulate s n) = ∑ i ∈ Finset.range (n + 1), m (s i)
-- Mathlib.Logic.Basic
not_exists_mem : ∀ {α : Sort u_1} {p : α → Prop} {P : (x : α) → p x → Prop}, (¬∃ x, ∃ (h : p x), P x h) ↔ ∀ (x : α) (h : p x), ¬P x h
-- Mathlib.Analysis.Complex.Trigonometric
Real.tan_mul_cos : ∀ {x : ℝ}, Real.cos x ≠ 0 → Real.tan x * Real.cos x = Real.sin x
-- Mathlib.Analysis.Normed.Unbundled.FiniteExtension
/-- For any `K`-basis of `L`, if the norm on `K` is nonarchimedean, then so is `B.norm`.  -/
Module.Basis.norm_isNonarchimedean : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : Ring L] [inst_2 : Algebra K L] {ι : Type u_3}
  [inst_3 : Fintype ι] [inst_4 : Nonempty ι] {B : Module.Basis ι K L}, IsNonarchimedean norm → IsNonarchimedean B.norm
-- Mathlib.Analysis.SpecialFunctions.Exponential
/-- The exponential map in `𝕂 = ℝ` or `𝕂 = ℂ` has strict derivative `1` at zero.  -/
hasStrictDerivAt_exp_zero : ∀ {𝕂 : Type u_1} [inst : RCLike 𝕂], HasStrictDerivAt NormedSpace.exp 1 0
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RioSliceData.mk.inj : ∀ {α : Type u} {β : Type v} {inst : Ord α} {treeMap : Std.DTreeMap.Internal.Impl α fun x => β} {range : Std.Rio α}
  {treeMap_1 : Std.DTreeMap.Internal.Impl α fun x => β} {range_1 : Std.Rio α},
  { treeMap := treeMap, range := range } = { treeMap := treeMap_1, range := range_1 } →
    treeMap = treeMap_1 ∧ range = range_1
-- Lean.Meta.LetToHave
/-- Checks whether the mvar creates a dependency on any let fvars.
Note: the local context of `mvarId` cannot depend on `letFVars`, since it was created outside these `let`s.
The only consideration is delayed assignments and which variables they depend on;
if the fvar is not passed among the `args`, the mvar cannot depend on it.
 -/
_private.Lean.Meta.LetToHave.0.Lean.Meta.LetToHave.checkMVar : Lean.MVarId → Array Lean.Expr → Lean.Meta.LetToHave.M✝ Unit
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_mul_leadingCoeff_inv : ∀ {K : Type u_1} [inst : DivisionRing K] (p : Polynomial K) {q : Polynomial K},
  q ≠ 0 → (p * Polynomial.C q.leadingCoeff⁻¹).natDegree = p.natDegree
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.coe_expand : ∀ {σ : Type u_1} {R : Type u_3} [inst : CommSemiring R] (p : ℕ),
  ⇑(MvPolynomial.expand p) = MvPolynomial.eval₂ MvPolynomial.C ((fun s => MvPolynomial.X s) ^ p)
-- Mathlib.NumberTheory.ModularForms.Basic
CuspForm.instIsAddApplyUpperHalfPlaneComplex : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ}, IsAddApply (CuspForm Γ k) UpperHalfPlane ℂ
-- Mathlib.LinearAlgebra.LinearIndependent.Lemmas
LinearIndepOn.subset_extend : ∀ {ι : Type u'} {K : Type u_3} {V : Type u} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  {v : ι → V} {s t : Set ι} (hs : LinearIndepOn K v s) (hst : s ⊆ t), s ⊆ hs.extend hst
-- Init.Data.Vector.Algebra
Vector.mul_smul : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {d : α} [inst : Mul α] [inst_1 : SMul α β],
  (∀ (c d : α) (x : β), (c * d) • x = c • d • x) → ∀ (c : α) (xs : Vector β n), (c * d) • xs = c • d • xs
-- Mathlib.Data.Finset.Option
Finset.forall_mem_insertNone : ∀ {α : Type u_1} {s : Finset α} {p : Option α → Prop}, (∀ a ∈ Finset.insertNone s, p a) ↔ p none ∧ ∀ a ∈ s, p (some a)
-- Mathlib.Order.SuccPred.LinearLocallyFinite
toZ_iterate_pred_of_not_isMin : ∀ {ι : Type u_1} [inst : LinearOrder ι] [inst_1 : SuccOrder ι] [inst_2 : IsSuccArchimedean ι] [inst_3 : PredOrder ι]
  {i0 : ι} (n : ℕ), ¬IsMin (Order.pred^[n] i0) → toZ i0 (Order.pred^[n] i0) = -↑n
-- Mathlib.Topology.Algebra.FilterBasis
GroupFilterBasis.one' : ∀ {G : Type u} {inst : Group G} [self : GroupFilterBasis G] {U : Set G}, U ∈ self.sets → 1 ∈ U
-- Mathlib.RepresentationTheory.Homological.TateCohomology.Basic
/-- The functor taking a representation of `G` to its Tate complex.  -/
tateComplexFunctor : (R G : Type u) →
  [inst : CommRing R] →
    [inst_1 : Group G] → [Fintype G] → CategoryTheory.Functor (Rep.{u, u, u} R G) (CochainComplex (ModuleCat R) ℤ)
-- Mathlib.Algebra.FiveLemma
/-- One four lemma in terms of additive groups.
For a diagram explaining the variables, see the module docstring.  -/
AddMonoidHom.surjective_of_surjective_of_surjective_of_injective : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {M₄ : Type u_4} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8}
  {N₄ : Type u_9} [inst : AddGroup M₁] [inst_1 : AddGroup M₂] [inst_2 : AddGroup M₃] [inst_3 : AddGroup M₄]
  [inst_4 : AddGroup N₁] [inst_5 : AddGroup N₂] [inst_6 : AddGroup N₃] [inst_7 : AddGroup N₄] (f₁ : M₁ →+ M₂)
  (f₂ : M₂ →+ M₃) (f₃ : M₃ →+ M₄) (g₁ : N₁ →+ N₂) (g₂ : N₂ →+ N₃) (g₃ : N₃ →+ N₄) (i₁ : M₁ →+ N₁) (i₂ : M₂ →+ N₂)
  (i₃ : M₃ →+ N₃) (i₄ : M₄ →+ N₄),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      g₃.comp i₃ = i₄.comp f₃ →
        Function.Exact ⇑f₂ ⇑f₃ →
          Function.Exact ⇑g₁ ⇑g₂ →
            Function.Exact ⇑g₂ ⇑g₃ →
              Function.Surjective ⇑i₁ → Function.Surjective ⇑i₃ → Function.Injective ⇑i₄ → Function.Surjective ⇑i₂
-- Mathlib.Data.NNReal.Defs
NNReal.lt_iff_exists_rat_btwn : ∀ (a b : NNReal), a < b ↔ ∃ q, 0 ≤ q ∧ a < (↑q).toNNReal ∧ (↑q).toNNReal < b
-- Mathlib.Tactic.ComputeDegree
/-- `splitApply mvs static` takes two lists of `MVarId`s.  The first list, `mvs`,
corresponds to goals that are potentially within the scope of `compute_degree`:
namely, goals of the form
`natDegree f ≤ d`, `degree f ≤ d`, `natDegree f = d`, `degree f = d`, `coeff f d = r`.

`splitApply` determines which of these goals are actually within the scope, it applies the relevant
lemma and returns two lists: the left-over goals of all the applications, followed by the
concatenation of the previous `static` list, followed by the newly discovered goals outside of the
scope of `compute_degree`.  -/
Mathlib.Tactic.ComputeDegree.splitApply : List Lean.MVarId → List Lean.MVarId → Lean.MetaM (List Lean.MVarId × List Lean.MVarId)
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.isOrderedMonoid : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α], IsOrderedMonoid (WithZero α)
-- Mathlib.Analysis.Normed.Group.Seminorm
GroupNorm.groupNormClass : ∀ {E : Type u_3} [inst : Group E], GroupNormClass (GroupNorm E) E ℝ
-- Mathlib.RingTheory.RootsOfUnity.CyclotomicUnits
/-- If `p` is prime and `ζ` is a `p`-th primitive root of unity, then `ζ - 1` and `η₁ - η₂` are
associated for all distinct `p`-th roots of unity `η₁` and `η₂`.  -/
IsPrimitiveRoot.nthRootsFinset_pairwise_associated_sub_one_sub_of_prime : ∀ {p : ℕ} {A : Type u_1} {ζ : A} [inst : CommRing A] [inst_1 : IsDomain A],
  IsPrimitiveRoot ζ p →
    Nat.Prime p → (↑(Polynomial.nthRootsFinset p 1)).Pairwise fun η₁ η₂ => Associated (ζ - 1) (η₁ - η₂)
-- Mathlib.NumberTheory.Cyclotomic.Basic
/-- Separably closed fields are `S`-cyclotomic extensions over themselves if
`NeZero ((a : ℕ) : K)` for all nonzero `a ∈ S`.  -/
IsSepClosed.isCyclotomicExtension : ∀ (S : Set ℕ) (K : Type w) [inst : Field K] [IsSepClosed K], (∀ a ∈ S, a ≠ 0 → NeZero ↑a) → IsCyclotomicExtension S K K
-- Mathlib.Analysis.Convex.Slope
/-- If for any three points `x < y < z`, the slope of the secant line of `f : 𝕜 → 𝕜` on `[x, y]` is
greater than the slope of the secant line of `f` on `[y, z]`, then `f` is concave.  -/
concaveOn_of_slope_anti_adjacent : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜] {s : Set 𝕜} {f : 𝕜 → 𝕜},
  Convex 𝕜 s →
    (∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)) → ConcaveOn 𝕜 s f
-- Mathlib.Combinatorics.SimpleGraph.Coloring.Vertex
SimpleGraph.chromaticNumber_mono : ∀ {V : Type u} {G : SimpleGraph V} (G' : SimpleGraph V), G ≤ G' → G.chromaticNumber ≤ G'.chromaticNumber
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.LaxMonoidal.μ_whiskerRight_comp_μ : ∀ {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.LaxMonoidal] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.Functor.LaxMonoidal.μ F X Y) (F.obj Z))
      (CategoryTheory.Functor.LaxMonoidal.μ F (CategoryTheory.MonoidalCategoryStruct.tensorObj X Y) Z) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (F.obj X) (F.obj Y) (F.obj Z)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) (CategoryTheory.Functor.LaxMonoidal.μ F Y Z))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Functor.LaxMonoidal.μ F X (CategoryTheory.MonoidalCategoryStruct.tensorObj Y Z))
          (F.map (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv)))
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
/-- A set that intersects each order connected component of a set by a single point. Defined as the
range of `Set.ordConnectedProj s`.  -/
Set.ordConnectedSection : {α : Type u_1} → [LinearOrder α] → Set α → Set α
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.instMultiplicative : {A : Type u_2} → [inst : AddMonoid A] → [Finset.HasAntidiagonal A] → Finset.HasMulAntidiagonal (Multiplicative A)
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.toSubsemiring_inj : ∀ {R : Type u} [inst : NonAssocRing R] {s t : Subring R}, s.toSubsemiring = t.toSubsemiring ↔ s = t
-- Mathlib.GroupTheory.Complement
AddSubgroup.IsComplement.rightQuotientEquiv_apply : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} {f : Quotient (QuotientAddGroup.rightRel H) → G}
  (hf : ∀ (q : Quotient (QuotientAddGroup.rightRel H)), Quotient.mk'' (f q) = q)
  (q : Quotient (QuotientAddGroup.rightRel H)), ↑(⋯.rightQuotientEquiv q) = f q
-- Mathlib.CategoryTheory.Preadditive.Injective.Resolution
/-- A morphism between the cocomplexes  -/
CategoryTheory.InjectiveResolution.Hom.hom : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] →
        {Z : C} →
          {I : CategoryTheory.InjectiveResolution Z} →
            {Z' : C} →
              {I' : CategoryTheory.InjectiveResolution Z'} → {f : Z ⟶ Z'} → I.Hom I' f → (I.cocomplex ⟶ I'.cocomplex)
-- Init.Data.UInt.Bitwise
UInt16.ofNat_and : ∀ (a b : ℕ), UInt16.ofNat (a &&& b) = UInt16.ofNat a &&& UInt16.ofNat b
-- Mathlib.Geometry.RingedSpace.Basic
AlgebraicGeometry.RingedSpace.basicOpen_mul : ∀ (X : AlgebraicGeometry.RingedSpace) {U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace}
  (f g : ↑(X.presheaf.obj (Opposite.op U))), X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g
-- Mathlib.Algebra.GCDMonoid.Basic
Associates.out_eq_zero_iff : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] {a : Associates α}, a.out = 0 ↔ a = 0
-- Mathlib.Algebra.Order.Antidiag.Prod
Finset.HasMulAntidiagonal.mem_mulAntidiagonal_ofAdd_iff_toAdd_mem_antidiagonal : ∀ {A : Type u_2} [inst : AddMonoid A] [inst_1 : Finset.HasAntidiagonal A] {a : A}
  {p : Multiplicative A × Multiplicative A},
  p ∈ Finset.HasMulAntidiagonal.mulAntidiagonal (Multiplicative.ofAdd a) ↔
    (Multiplicative.toAdd p.1, Multiplicative.toAdd p.2) ∈ Finset.HasAntidiagonal.antidiagonal a
-- Mathlib.CategoryTheory.Limits.Shapes.SplitEqualizer
CategoryTheory.IsSplitEqualizer.asFork_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {W : C} {h : W ⟶ X}
  (t : CategoryTheory.IsSplitEqualizer f g h), t.asFork.ι = h
-- Mathlib.RingTheory.LaurentSeries
PowerSeries.coe_zero : ∀ {R : Type u_1} [inst : Semiring R], (HahnSeries.ofPowerSeries ℤ R) 0 = 0
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.instFaithfulSMul_1 : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] (v : Valuation R Γ₀)
  {S : Type u_3} [inst_2 : SMul S R] [FaithfulSMul S R], FaithfulSMul S (WithVal v)
-- Init.Data.Int.DivMod.Lemmas
Int.ediv_eq_one_of_neg_of_le : ∀ {a b : ℤ}, a < 0 → b ≤ a → a / b = 1
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
QuadraticMap.instNeg : {R : Type u_3} →
  {M : Type u_4} →
    {N : Type u_5} →
      [inst : CommRing R] →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] → [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → Neg (QuadraticMap R M N)
-- Init.Data.List.Sublist
List.prefix_iff_eq_take : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ ↔ l₁ = List.take l₁.length l₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constMinEntry_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      ∀ (h : t₁.Equiv t₂) {he : t₁.isEmpty = false},
        Std.DTreeMap.Internal.Impl.Const.minEntry t₁ he = Std.DTreeMap.Internal.Impl.Const.minEntry t₂ ⋯
-- Init.Data.SInt.Lemmas
ISize.toInt32_ofBitVec : ∀ (b : BitVec System.Platform.numBits), (ISize.ofBitVec b).toInt32 = Int32.ofBitVec (BitVec.signExtend 32 b)
-- Mathlib.Geometry.Manifold.ContMDiff.Constructions
ContMDiff.prodMk_space : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {F' : Type u_11} [inst_8 : NormedAddCommGroup F'] [inst_9 : NormedSpace 𝕜 F']
  {n : WithTop ℕ∞} {f : M → E'} {g : M → F'},
  ContMDiff I (modelWithCornersSelf 𝕜 E') n f →
    ContMDiff I (modelWithCornersSelf 𝕜 F') n g → ContMDiff I (modelWithCornersSelf 𝕜 (E' × F')) n fun x => (f x, g x)
-- Mathlib.Geometry.Convex.Cone.Face.Basic
/-- The projection of a face of a product cone onto the second component is a face of the
projection of the product cone onto the second component.  -/
PointedCone.IsFaceOf.snd : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : DivisionRing R] [inst_1 : LinearOrder R]
  [inst_2 : IsOrderedRing R] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : AddCommGroup N]
  [inst_6 : Module R N] {C₁ : PointedCone R M} {C₂ : PointedCone R N} {F : PointedCone R (M × N)},
  F.IsFaceOf (Submodule.prod C₁ C₂) → (PointedCone.map (LinearMap.snd R M N) F).IsFaceOf C₂
-- Mathlib.Algebra.Lie.SemiDirect
LieAlgebra.SemiDirectSum.inl.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] {K : Type u_2} [inst_1 : LieRing K] [inst_2 : LieAlgebra R K] {L : Type u_3}
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ψ : L →ₗ⁅R⁆ LieDerivation R K K),
  LieAlgebra.SemiDirectSum.inl ψ =
    { toFun := fun x => { left := x, right := 0 }, map_add' := ⋯, map_smul' := ⋯, map_lie' := ⋯ }
-- Mathlib.Algebra.Order.IsBotOne
NeZero.pos : ∀ {α : Type u_1} [inst : Zero α] [inst_1 : PartialOrder α] [IsBotZeroClass α] (a : α) [NeZero a], 0 < a
-- Mathlib.Order.Category.DistLat
DistLat.dual_map : ∀ {X Y : DistLat} (f : X ⟶ Y), DistLat.dual.map f = DistLat.ofHom (LatticeHom.dual (DistLat.Hom.hom f))
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMono.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} →
      {f : X ⟶ Y} →
        (retraction : Y ⟶ X) →
          autoParam (CategoryTheory.CategoryStruct.comp f retraction = CategoryTheory.CategoryStruct.id X)
              CategoryTheory.SplitMono.id._autoParam →
            CategoryTheory.SplitMono f
-- Mathlib.Algebra.Homology.ModelCategory.Lifting
CochainComplex.Lifting.cocycle₁.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {A B X Y : CochainComplex C ℤ} {t : A ⟶ X} {i : A ⟶ B} {p : X ⟶ Y} {b : B ⟶ Y} (sq : CategoryTheory.CommSq t i p b)
  (hsq : (n : ℤ) → ⋯.LiftStruct) {Q : CochainComplex C ℤ} {π : B ⟶ Q} {hπ : CategoryTheory.CategoryStruct.comp i π = 0}
  (hQ : CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.CokernelCofork.ofπ π hπ)) {K : CochainComplex C ℤ}
  {ι : K ⟶ X} {hι : CategoryTheory.CategoryStruct.comp ι p = 0}
  (hK : CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.KernelFork.ofι ι hι)),
  CochainComplex.Lifting.cocycle₁ sq hsq hQ hK =
    CochainComplex.HomComplex.Cocycle.mk (CochainComplex.Lifting.cochain₁ sq hsq hQ hK) 2
      CochainComplex.Lifting.cocycle₁'._proof_1 ⋯
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.δ_zero_cochain_v : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (z : CochainComplex.HomComplex.Cochain F G 0) (p q : ℤ) (hpq : p + 1 = q),
  (CochainComplex.HomComplex.δ 0 1 z).v p q hpq =
    CategoryTheory.CategoryStruct.comp (z.v p p ⋯) (G.d p q) - CategoryTheory.CategoryStruct.comp (F.d p q) (z.v q q ⋯)
-- Mathlib.LinearAlgebra.Prod
/-- The prod of two linear maps is a linear map.  -/
LinearMap.prod : {R : Type u} →
  {M : Type v} →
    {M₂ : Type w} →
      {M₃ : Type y} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : AddCommMonoid M₂] →
              [inst_3 : AddCommMonoid M₃] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R M₂] → [inst_6 : Module R M₃] → (M →ₗ[R] M₂) → (M →ₗ[R] M₃) → M →ₗ[R] M₂ × M₃
-- Mathlib.CategoryTheory.Triangulated.Functor
CategoryTheory.Functor.IsTriangulated.instAdditive : ∀ {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.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  [inst_5 : CategoryTheory.Limits.HasZeroObject C] [inst_6 : CategoryTheory.Limits.HasZeroObject D]
  [inst_7 : CategoryTheory.Preadditive C] [inst_8 : CategoryTheory.Preadditive D]
  [inst_9 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_10 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor D n).Additive] [inst_11 : CategoryTheory.Pretriangulated C]
  [inst_12 : CategoryTheory.Pretriangulated D] [F.IsTriangulated], F.Additive
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreOneHypercover.comp_s₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {X Y Z : CategoryTheory.PreOneHypercover S}
  (f : X.Hom Y) (g : Y.Hom Z) (a : X.I₀), (CategoryTheory.CategoryStruct.comp f g).s₀ a = g.s₀ (f.s₀ a)
-- Lean.Server.Rpc.Basic
Lean.Server.ReferencedObject.obj : Lean.Server.ReferencedObject → Dynamic
-- Init.System.Platform
System.Platform.System.Platform.dvd_numBits : 32 ∣ System.Platform.numBits
-- Mathlib.Data.Nat.PrimeFin
Nat.primeFactors_mul : ∀ {a b : ℕ}, a ≠ 0 → b ≠ 0 → (a * b).primeFactors = a.primeFactors ∪ b.primeFactors