mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.cylinder_p₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  {F : CategoryTheory.PreOneHypercover S} [inst_1 : CategoryTheory.Limits.HasPullbacks C] (f g : E.Hom F)
  {p q : (i : E.I₀) × F.I₁ (f.s₀ i) (g.s₀ i)} (k : ULift.{max w w', w} (E.I₁ p.fst q.fst)),
  (CategoryTheory.PreOneHypercover.cylinder f g).p₁ k =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst
        (CategoryTheory.Limits.pullback.map (CategoryTheory.PreOneHypercover.cylinderf f g p.snd)
          (CategoryTheory.PreOneHypercover.cylinderf f g q.snd) (E.f p.fst) (E.f q.fst)
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ p.fst) (g.h₀ p.fst) ⋯)
            (F.toPullback p.snd))
          (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.lift (f.h₀ q.fst) (g.h₀ q.fst) ⋯)
            (F.toPullback q.snd))
          (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)
        (CategoryTheory.Limits.pullback.lift (E.p₁ k.down) (E.p₂ k.down) ⋯))
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.PreOneHypercover.cylinderf f g p.snd)
        (CategoryTheory.PreOneHypercover.cylinderf f g q.snd))
-- Mathlib.SetTheory.Cardinal.Aleph
Ordinal.preOmega_le_of_forall_lt : ∀ {o a : Ordinal.{u_1}}, a.IsInitial → (∀ b < o, Ordinal.preOmega b < a) → Ordinal.preOmega o ≤ a
-- Mathlib.Tactic.CategoryTheory.Coherence
Mathlib.Tactic.Coherence.LiftHom.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : Mathlib.Tactic.Coherence.LiftObj X] →
        [inst_2 : Mathlib.Tactic.Coherence.LiftObj Y] →
          {f : X ⟶ Y} →
            (Mathlib.Tactic.Coherence.LiftObj.lift X ⟶ Mathlib.Tactic.Coherence.LiftObj.lift Y) →
              Mathlib.Tactic.Coherence.LiftHom f
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_lt_mul_right_of_neg : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] [ExistsAddOfLE R] [MulPosStrictMono R]
  [AddRightStrictMono R] [AddRightReflectLT R] {a b c : R}, c < 0 → (a * c < b * c ↔ b < a)
-- Init.Data.Nat.Lemmas
Nat.max_eq_zero_iff : ∀ {m n : ℕ}, max m n = 0 ↔ m = 0 ∧ n = 0
-- Mathlib.LinearAlgebra.SModEq.Pow
SModEq.pow_add_one : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {p : ℕ},
  ↑p ∈ I → ∀ {x y : R} {m : ℕ}, m ≠ 0 → x ≡ y [SMOD I ^ m] → x ^ p ≡ y ^ p [SMOD I ^ (m + 1)]
-- Mathlib.ModelTheory.Quotients
FirstOrder.Language.Prestructure.fun_equiv : ∀ {L : FirstOrder.Language} {M : Type u_1} {s : Setoid M} [self : L.Prestructure s] {n : ℕ} {f : L.Functions n}
  (x y : Fin n → M), x ≈ y → FirstOrder.Language.Structure.funMap f x ≈ FirstOrder.Language.Structure.funMap f y
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.eq_d₀₁_comp_inv_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑A),
  (CategoryTheory.ConcreteCategory.hom
        (CochainComplex.of.d (fun n => ModuleCat.of k ((Fin n → G) → ↑A)) (fun n => inhomogeneousCochains.d A n) 0 1))
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₀ A).inv) x) =
    (CategoryTheory.ConcreteCategory.hom (groupCohomology.cochainsIso₁ A).inv)
      ((CategoryTheory.ConcreteCategory.hom (groupCohomology.d₀₁ A)) x)
-- Init.Data.Iterators.Lemmas.Consumers.Collect
Std.Iter.toListRev_ensureTermination : ∀ {α β : Type u_1} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterators.Finite α Id] {it : Std.Iter β},
  it.ensureTermination.toListRev = it.toList.reverse
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.counitAlgHom_comp_mapRingHom : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : CommMonoid M]
  (f : R →+* S),
  (Bialgebra.counitAlgHom S (MonoidAlgebra S M)).comp (MonoidAlgebra.mapRingHom M f) =
    f.comp (Bialgebra.counitAlgHom R (MonoidAlgebra R M)).toRingHom
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.ElabSimpArgsResult.mk : Lean.Meta.Simp.Context →
  Lean.Meta.Simp.SimprocsArray →
    Array (Lean.Syntax × Lean.Elab.Tactic.ElabSimpArgResult) → Lean.Elab.Tactic.ElabSimpArgsResult
-- Mathlib.RingTheory.Kaehler.Basic
/-- The linear map from `Ω[S⁄R]`, associated with a derivation.  -/
Derivation.liftKaehlerDifferential : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {M : Type u_1} →
            [inst_3 : AddCommGroup M] →
              [inst_4 : Module R M] → [inst_5 : Module S M] → [IsScalarTower R S M] → Derivation R S M → Ω[S⁄R] →ₗ[S] M
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.injective_codRestrict : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] {S : Type u_5} [inst_2 : SetLike S N]
  [inst_3 : AddSubmonoidClass S N] (f : M →+ N) (s : S) (h : ∀ (x : M), f x ∈ s),
  Function.Injective ⇑(f.codRestrict s h) ↔ Function.Injective ⇑f
-- Mathlib.Analysis.Normed.Module.WeakDual
/-- The extension `StrongDual.extendRCLike` as a continuous linear equivalence between
the weak duals.  -/
WeakDual.extendRCLikeL : {𝕜 : Type u_5} →
  {F : Type u_7} →
    [inst : RCLike 𝕜] →
      [inst_1 : AddCommGroup F] →
        [inst_2 : Module 𝕜 F] →
          [inst_3 : TopologicalSpace F] →
            [ContinuousConstSMul 𝕜 F] → [inst_5 : Module ℝ F] → [IsScalarTower ℝ 𝕜 F] → WeakDual ℝ F ≃L[ℝ] WeakDual 𝕜 F
-- Std.Data.DTreeMap.Raw.Lemmas
/-- Variant of `getD_map` that holds without `LawfulEqCmp`.  -/
Std.DTreeMap.Raw.Const.getD_map' : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Raw α (fun x => β) cmp}
  [inst : Std.TransCmp cmp] {f : α → β → γ} {k : α} {fallback : γ} (h : t.WF),
  Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.map f t) k fallback =
    (Option.pmap (fun v h => f (t.getKey k h) v) (Std.DTreeMap.Raw.Const.get? t k) ⋯).getD fallback
-- Init.GrindInstances.Ring.UInt
Lean.Grind.instPowUInt16UintOfNatNat : Lean.Grind.ToInt.Pow UInt16 (Lean.Grind.IntInterval.uint 16)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_succ_Ioi_succ : ∀ {n : ℕ} (i : Fin n), Fin.succ ⁻¹' Set.Ioi i.succ = Set.Ioi i
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MultispanShape.prod_L : ∀ (ι : Type w), (CategoryTheory.Limits.MultispanShape.prod ι).L = (ι × ι)
-- Mathlib.Dynamics.PeriodicPts.Lemmas
Function.minimalPeriod_fst_dvd : ∀ {α : Type u_1} {β : Type u_2} {f : α → α} {g : β → β} {x : α × β},
  Function.minimalPeriod f x.1 ∣ Function.minimalPeriod (Prod.map f g) x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCast?_filter_containsKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.getValueCast? k (List.filter (fun p => Std.Internal.List.containsKey p.fst l₂) l₁) =
      if Std.Internal.List.containsKey k l₂ = true then Std.Internal.List.getValueCast? k l₁ else none
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_X_pow : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [Nontrivial R] (s : σ) (n : ℕ),
  (MvPolynomial.X s ^ n).totalDegree = n
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- Evaluating the Cantor normal form of an ordinal returns the ordinal.  -/
Ordinal.CNF.foldr : ∀ (b o : Ordinal.{u_1}), List.foldr (fun p r => b ^ p.1 * p.2 + r) 0 (Ordinal.CNF b o) = o
-- Mathlib.Order.UpperLower.Prod
UpperSet.prod_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] (s : UpperSet α) (t₁ t₂ : UpperSet β),
  s ×ˢ (t₁ ⊓ t₂) = s ×ˢ t₁ ⊓ s ×ˢ t₂
-- Lean.Compiler.Specialize
/-- Marks a type for weak specialization: Parameters of this type are only specialized when
another argument already triggers specialization. Unlike `@[nospecialize]`, if specialization
happens for other reasons, parameters of this type will participate in the specialization
rather than being ignored.
 -/
Lean.Compiler.weakSpecializeAttr : Lean.TagAttribute
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.link2.match_5.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (motive : (r : Std.DTreeMap.Internal.Impl α β) → r.Balanced → Sort u_3) →
      (r : Std.DTreeMap.Internal.Impl α β) →
        (hr : r.Balanced) →
          ((hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
              r = Std.DTreeMap.Internal.Impl.leaf → motive Std.DTreeMap.Internal.Impl.leaf hr) →
            ((szr : ℕ) →
                (k'' : α) →
                  (v'' : β k'') →
                    (l'' r'' : Std.DTreeMap.Internal.Impl α β) →
                      (hr : (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'').Balanced) →
                        r = Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'' →
                          motive (Std.DTreeMap.Internal.Impl.inner szr k'' v'' l'' r'') hr) →
              motive r hr
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.coeMulHom.eq_1 : ∀ {α : Type u_1} {M : Type u_5} [inst : Monoid M] (l : Filter α),
  Filter.Germ.coeMulHom l = { toFun := Filter.Germ.ofFun, map_one' := ⋯, map_mul' := ⋯ }
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.inv_Ioi : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : PartialOrder α] [IsOrderedMonoid α] (a : α), (Set.Ioi a)⁻¹ = Set.Iio a⁻¹
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.NatTrans.CommShiftCore.shift_app_comm_assoc : ∀ {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] {F₁ F₂ : CategoryTheory.Functor C D} (τ : F₁ ⟶ F₂) {A : Type u_5}
  [inst_2 : AddMonoid A] [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A]
  [inst_5 : F₁.CommShift A] [inst_6 : F₂.CommShift A] {a : A},
  CategoryTheory.NatTrans.CommShiftCore τ a →
    ∀ (X : C) {Z : D} (h : (CategoryTheory.shiftFunctor D a).obj (F₂.obj X) ⟶ Z),
      CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₁ a).hom.app X)
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor D a).map (τ.app X)) h) =
        CategoryTheory.CategoryStruct.comp (τ.app ((CategoryTheory.shiftFunctor C a).obj X))
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Functor.commShiftIso F₂ a).hom.app X) h)
-- Mathlib.Analysis.Meromorphic.Order
/-- A meromorphic function converges to infinity iff its order is negative.  -/
tendsto_cobounded_iff_meromorphicOrderAt_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜},
  MeromorphicAt f x → (Filter.Tendsto f (nhdsWithin x {x}ᶜ) (Bornology.cobounded E) ↔ meromorphicOrderAt f x < 0)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey!_erase_eq_iff_not_compare_minKey!_eq : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α] (h : t.WF) {k : α},
  (Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.isEmpty = false →
    ((Std.DTreeMap.Internal.Impl.erase k t ⋯).impl.minKey! = t.minKey! ↔ ¬compare k t.minKey! = Ordering.eq)
-- Std.Do.SPred.SPred
Std.Do.SPred.iff_nil : ∀ {P Q : Std.Do.SPred []}, spred(P ↔ Q) = { down := P.down ↔ Q.down }
-- Init.Data.UInt.Lemmas
UInt16.le_antisymm_iff : ∀ {a b : UInt16}, a = b ↔ a ≤ b ∧ b ≤ a
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_eq_of_contains : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k fallback : α}, t.contains k = true → t.getKeyD k fallback = k
-- Mathlib.Topology.UniformSpace.Completion
/-- Completion functor acting on morphisms  -/
UniformSpace.Completion.map : {α : Type u_1} →
  [inst : UniformSpace α] →
    {β : Type u_2} → [inst_1 : UniformSpace β] → (α → β) → UniformSpace.Completion α → UniformSpace.Completion β
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.id_c : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C),
  (CategoryTheory.CategoryStruct.id X).c = CategoryTheory.CategoryStruct.id X.presheaf
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
AddSubgroup.unop_top : ∀ {G : Type u_2} [inst : AddGroup G], ⊤.unop = ⊤
-- Mathlib.Analysis.Convex.Birkhoff
/-- The set of extreme points of the doubly stochastic matrices is the set of permutation matrices.
 -/
extremePoints_doublyStochastic : ∀ {R : Type u_1} {n : Type u_2} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : Field R] [inst_3 : LinearOrder R]
  [inst_4 : IsStrictOrderedRing R],
  Set.extremePoints R ↑(doublyStochastic R n) = {x | ∃ σ, Equiv.Perm.permMatrix R σ = x}
-- Mathlib.Algebra.BigOperators.Group.Finset.Sigma
Finset.sum_finset_product' : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : AddCommMonoid β] (r : Finset (γ × α)) (s : Finset γ)
  (t : γ → Finset α),
  (∀ (p : γ × α), p ∈ r ↔ p.1 ∈ s ∧ p.2 ∈ t p.1) → ∀ {f : γ → α → β}, ∑ p ∈ r, f p.1 p.2 = ∑ c ∈ s, ∑ a ∈ t c, f c a
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- Two morphisms in an exact sequence are exact on pseudoelements.  -/
CategoryTheory.Abelian.Pseudoelement.pseudo_exact_of_exact : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  {S : CategoryTheory.ShortComplex C},
  S.Exact →
    ∀ (b : CategoryTheory.Abelian.Pseudoelement S.X₂),
      CategoryTheory.Abelian.Pseudoelement.pseudoApply S.g b = 0 →
        ∃ a, CategoryTheory.Abelian.Pseudoelement.pseudoApply S.f a = b
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getD_inter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β}
  [inst_2 : LawfulBEq α],
  m₁.WF →
    m₂.WF → ∀ {k : α} {fallback : β k}, (m₁ ∩ m₂).getD k fallback = if k ∈ m₂ then m₁.getD k fallback else fallback
-- Init.Data.List.OfFn
List.ofFn_succ : ∀ {α : Type u_1} {n : ℕ} {f : Fin (n + 1) → α}, List.ofFn f = f 0 :: List.ofFn fun i => f i.succ
-- Batteries.Data.List.Lemmas
List.mem_findIdxs_iff_exists_getElem_pos : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {i : ℕ}, i ∈ List.findIdxs p xs ↔ ∃ (hix : i < xs.length), p xs[i] = true
-- Mathlib.Data.Num.Lemmas
_private.Mathlib.Data.Num.Lemmas.0.PosNum.testBit.match_1.eq_3 : ∀ (motive : PosNum → ℕ → Sort u_1) (a : PosNum) (h_1 : Unit → motive PosNum.one 0) (h_2 : (x : ℕ) → motive PosNum.one x)
  (h_3 : (a : PosNum) → motive a.bit0 0) (h_4 : (p : PosNum) → (n : ℕ) → motive p.bit0 n.succ)
  (h_5 : (a : PosNum) → motive a.bit1 0) (h_6 : (p : PosNum) → (n : ℕ) → motive p.bit1 n.succ),
  (match a.bit0, 0 with
    | PosNum.one, 0 => h_1 ()
    | PosNum.one, x => h_2 x
    | a.bit0, 0 => h_3 a
    | p.bit0, n.succ => h_4 p n
    | a.bit1, 0 => h_5 a
    | p.bit1, n.succ => h_6 p n) =
    h_3 a
-- Lean.Environment
Lean.instLTOLeanLevel : LT Lean.OLeanLevel
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.mem_alter_of_not_compare_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α] (h : t.WF)
  {k k' : α} {f : Option β → Option β},
  ¬compare k k' = Ordering.eq → (k' ∈ (Std.DTreeMap.Internal.Impl.Const.alter k f t ⋯).impl ↔ k' ∈ t)
-- Mathlib.Topology.Category.CompHausLike.Limits
/-- The inclusion of one of the factors into the explicit finite coproduct.
 -/
CompHausLike.finiteCoproduct.ι : {P : TopCat → Prop} →
  {α : Type w} →
    [inst : Finite α] →
      (X : α → CompHausLike P) →
        [inst_1 : CompHausLike.HasExplicitFiniteCoproduct X] → (a : α) → X a ⟶ CompHausLike.finiteCoproduct X
-- Mathlib.Order.Hom.Bounded
/-- The function preserves the bottom element. The preferred spelling is `map_bot`.  -/
BoundedOrderHom.map_bot' : ∀ {α : Type u_6} {β : Type u_7} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : BoundedOrder α]
  [inst_3 : BoundedOrder β] (self : BoundedOrderHom α β), self.toFun ⊥ = ⊥
-- Mathlib.SetTheory.Ordinal.Arithmetic
_private.Mathlib.SetTheory.Ordinal.Arithmetic.0.Ordinal.mul_le_of_limit_aux : ∀ {α β : Type u_4} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s]
  {c : Ordinal.{u_4}},
  Order.IsSuccLimit (Ordinal.type s) →
    (∀ b' < Ordinal.type s, Ordinal.type r * b' ≤ c) → c < Ordinal.type r * Ordinal.type s → False
-- Mathlib.NumberTheory.ModularForms.Discriminant
/-- The first q-expansion coefficient of the modular discriminant is 1.  -/
ModularForm.discriminant_qExpansion_coeff_one : (PowerSeries.coeff 1) (UpperHalfPlane.qExpansion 1 ModularForm.discriminant) = 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Basic
WeierstrassCurve.Jacobian.nonsingular_iff_of_Z_ne_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  P 2 ≠ 0 →
    (W.Nonsingular P ↔
      W.Equation P ∧ ((MvPolynomial.eval P) W.polynomialX ≠ 0 ∨ (MvPolynomial.eval P) W.polynomialY ≠ 0))
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- When both maps `S.f` and `S.g` of a short complex `S` are zero, this is the right homology map
data (for the identity of `S`) which relates the right homology data
`RightHomologyData.ofIsLimitKernelFork` and `ofZeros` .  -/
CategoryTheory.ShortComplex.RightHomologyMapData.compatibilityOfZerosOfIsLimitKernelFork : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      (S : CategoryTheory.ShortComplex C) →
        (hf : S.f = 0) →
          (hg : S.g = 0) →
            (c : CategoryTheory.Limits.KernelFork S.g) →
              (hc : CategoryTheory.Limits.IsLimit c) →
                CategoryTheory.ShortComplex.RightHomologyMapData (CategoryTheory.CategoryStruct.id S)
                  (CategoryTheory.ShortComplex.RightHomologyData.ofIsLimitKernelFork S hf c hc)
                  (CategoryTheory.ShortComplex.RightHomologyData.ofZeros S hf hg)
-- Mathlib.Algebra.Homology.Single
HomologicalComplex.from_single_hom_ext : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  [inst_2 : CategoryTheory.Limits.HasZeroObject V] {ι : Type u_1} [inst_3 : DecidableEq ι] {c : ComplexShape ι}
  {K : HomologicalComplex V c} {j : ι} {A : V} {f g : (HomologicalComplex.single V c j).obj A ⟶ K},
  f.f j = g.f j → f = g
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Removes the smallest element from the heap, if possible.  -/
Batteries.BinomialHeap.tail : {α : Type u} → {le : α → α → Bool} → Batteries.BinomialHeap α le → Batteries.BinomialHeap α le
-- Mathlib.Tactic.Translate.UnfoldBoundary
/-- An entry for the `UnfoldBoundaries` environment extension.  -/
Mathlib.Tactic.UnfoldBoundary.UnfoldEntry : Type
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.epi_homMk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {S : D} {T : CategoryTheory.Functor C D} {A B : CategoryTheory.StructuredArrow S T} (f : A.right ⟶ B.right)
  (w : CategoryTheory.CategoryStruct.comp A.hom (T.map f) = B.hom) [h : CategoryTheory.Epi f],
  CategoryTheory.Epi (CategoryTheory.StructuredArrow.homMk f w)
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndep.iIndepSets : ∀ {Ω : Type u_1} {ι : Type u_2} {m : ι → MeasurableSpace Ω} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  {s : ι → Set (Set Ω)},
  (∀ (n : ι), m n = MeasurableSpace.generateFrom (s n)) →
    ProbabilityTheory.iIndep m μ → ProbabilityTheory.iIndepSets s μ
-- Mathlib.AlgebraicTopology.Quasicategory.Basic
SSet.quasicategory_iff_hasLiftingProperty : ∀ (S : SSet) {X : SSet} (t : CategoryTheory.Limits.IsTerminal X),
  S.Quasicategory ↔
    ∀ {n : ℕ} {i : Fin (n + 1)}, 0 < i → i < Fin.last n → CategoryTheory.HasLiftingProperty (SSet.horn n i).ι (t.from S)
-- Mathlib.Algebra.Ring.Parity
Even.of_isUnit_two : ∀ {α : Type u_2} [inst : Semiring α], IsUnit 2 → ∀ (a : α), Even a
-- Init.Omega.Int
Int.natAbs.eq_def : ∀ (m : ℤ),
  m.natAbs =
    match m with
    | Int.ofNat m => m
    | Int.negSucc m => m.succ
-- Std.Internal.UV.System
Std.Internal.UV.System.GroupInfo.members : Std.Internal.UV.System.GroupInfo → Array String
-- Std.Do.Triple.SpecLemmas
/-- Like `Invariant.withEarlyReturn`, but for the new `do` elaborator which uses `Prod`
instead of `MProd` for the state tuple.  -/
Std.Do.Invariant.withEarlyReturnNewDo : {β : Type (max u₁ u₂)} →
  {ps : Std.Do.PostShape} →
    {α : Type (max u₁ u₂)} →
      {xs : List α} →
        {γ : Type (max u₁ u₂)} →
          (xs.Cursor → β → Std.Do.Assertion ps) →
            (γ → β → Std.Do.Assertion ps) →
              optParam (Std.Do.ExceptConds ps) Std.Do.ExceptConds.false → Std.Do.Invariant xs (Option γ × β) ps
-- Init.Data.Int.Linear
Int.Internal.Linear.Poly.gcdCoeffs.eq_def : ∀ (x : Int.Internal.Linear.Poly) (x_1 : ℤ),
  x.gcdCoeffs x_1 =
    match x, x_1 with
    | Int.Internal.Linear.Poly.num k, k_1 => k_1
    | Int.Internal.Linear.Poly.add k' v p, k => p.gcdCoeffs ↑(k'.gcd k)
-- Mathlib.Algebra.Module.LinearMap.End
/-- The canonical (semi)ring isomorphism from `Rᵐᵒᵖ` to `Module.End R R` induced by the right
multiplication.  -/
RingEquiv.moduleEndSelf : (R : Type u_1) → [inst : Semiring R] → Rᵐᵒᵖ ≃+* Module.End R R
-- Init.Control.Lawful.Instances
StateT.run_lift : ∀ {m : Type u → Type u_1} {α σ : Type u} [inst : Monad m] (x : m α) (s : σ),
  (StateT.lift x).run s = do
    let a ← x
    pure (a, s)
-- Mathlib.Algebra.Order.Floor.Div
ceilDiv_of_nonpos : ∀ {α : Type u_2} {β : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [inst_2 : AddCommMonoid β]
  [inst_3 : PartialOrder β] [inst_4 : SMulZeroClass α β] [inst_5 : CeilDiv α β] {a : α}, a ≤ 0 → ∀ (b : β), b ⌈/⌉ a = 0
-- Mathlib.Logic.Equiv.Prod
optionProdEquiv_mk_some : ∀ {α : Type u_9} {β : Type u_10} (a : α) (b : β), optionProdEquiv (some a, b) = Sum.inr (a, b)
-- Mathlib.GroupTheory.GroupExtension.Defs
GroupExtension.mk : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : Group N] →
        [inst_1 : Group E] →
          [inst_2 : Group G] →
            (inl : N →* E) →
              (rightHom : E →* G) →
                Function.Injective ⇑inl →
                  inl.range = rightHom.ker → Function.Surjective ⇑rightHom → GroupExtension N E G
-- Mathlib.Algebra.WithConv
WithConv.toConv_injective : ∀ {A : Type u_2}, Function.Injective WithConv.toConv
-- Mathlib.RingTheory.WittVector.Verschiebung
/-- `verschiebung x` shifts the coefficients of `x` up by one, by inserting 0 as the 0th coefficient.
`x.coeff i` then becomes `(verschiebung x).coeff (i + 1)`.

This is an additive monoid hom with underlying function `verschiebung_fun`.
 -/
WittVector.verschiebung : {p : ℕ} → {R : Type u_1} → [inst : CommRing R] → [hp : Fact (Nat.Prime p)] → WittVector p R →+ WittVector p R
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_div_closedBall_one : ∀ {E : Type u_1} [inst : SeminormedCommGroup E] (δ : ℝ) (x : E), {x} / Metric.closedBall 1 δ = Metric.closedBall x δ
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.UnionProd
SSet.prodStdSimplex.pairingCore.IsIndex.δ_dim : ∀ {m : ℕ} {k : Fin (m + 1)} {n : ℕ} {x : ((SSet.horn (m + 1) k.castSucc).unionProd (SSet.boundary n)).N} {d : ℕ}
  {hd : x.dim = d + 1} {l : Fin (d + 1)} (hl : SSet.prodStdSimplex.pairingCore.IsIndex x hd l.succ), hl.δ.dim = d
-- Mathlib.RingTheory.RingHom.OpenImmersion
Algebra.IsStandardOpenImmersion.inst : ∀ {R : Type u_1} [inst : CommSemiring R], Algebra.IsStandardOpenImmersion R R
-- Mathlib.Algebra.Module.SpanRank
Module.Basis.mk_eq_spanRank : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [RankCondition R]
  {ι : Type u_3} (v : Module.Basis ι R M), Cardinal.mk ↑(Set.range ⇑v) = ⊤.spanRank
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.Small.inf : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J K : CategoryTheory.Precoverage C} [J.Small],
  (∀ ⦃X : C⦄ ⦃R S : CategoryTheory.Presieve X⦄, R ≤ S → S ∈ K.coverings X → R ∈ K.coverings X) → (J ⊓ K).Small
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
NNReal.tsum_lt_tsum : ∀ {α : Type u_1} {f g : α → NNReal} {i : α},
  (∀ (a : α), f a ≤ g a) → f i < g i → Summable g → ∑' (n : α), f n < ∑' (n : α), g n