mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.maxEntry?.match_1.eq_2 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) (size : ℕ) (k : α)
  (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1))),
  (match Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1) =>
      h_3 size k v l r size_1 k_1 v_1 l_1 r_1 h) =
    h_2 size k v l
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyze.analyzePi : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeM Unit
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.ArctanDeriv
HasStrictFDerivAt.arctan : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {f' : StrongDual ℝ E} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt (fun x => Real.arctan (f x)) ((1 / (1 + f x ^ 2)) • f') x
-- Mathlib.Data.Num.Lemmas
Num.ppred.eq_2 : ∀ (p : PosNum), (Num.pos p).ppred = some p.pred'
-- Mathlib.Algebra.Ring.Subring.Basic
/-- The subring `R` of the ring `R`.  -/
Subring.instTop : {R : Type u} → [inst : NonAssocRing R] → Top (Subring R)
-- Mathlib.RingTheory.FractionalIdeal.Inverse
FractionalIdeal.instInvNonZeroDivisors : (K : Type u_3) →
  [inst : Field K] →
    {R₁ : Type u_4} →
      [inst_1 : CommRing R₁] →
        [IsDomain R₁] → [inst_3 : Algebra R₁ K] → [IsFractionRing R₁ K] → Inv (FractionalIdeal (nonZeroDivisors R₁) K)
-- Mathlib.CategoryTheory.Abelian.Preradical.Radical
CategoryTheory.Abelian.Radical.instIsIsoPreradicalToColonObjIsRadical : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Φ : CategoryTheory.Abelian.Radical C), CategoryTheory.IsIso (Φ.obj.toColon Φ.obj)
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk
_private.Mathlib.Combinatorics.SimpleGraph.Regularity.Chunk.0.SzemerediRegularity.eps_le_card_star_div : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α] {P : Finpartition Finset.univ} {hP : P.IsEquipartition}
  {G : SimpleGraph α} [inst_2 : DecidableRel G.Adj] {ε : ℝ} {U V : Finset α} [Nonempty α],
  P.parts.card * 16 ^ P.parts.card ≤ Fintype.card α →
    100 ≤ 4 ^ P.parts.card * ε ^ 5 →
      ε ≤ 1 →
        ∀ (hU : U ∈ P.parts),
          V ∈ P.parts →
            U ≠ V → ¬G.IsUniform ε U V → 4 / 5 * ε ≤ ↑(SzemerediRegularity.star hP G ε hU V).card / 4 ^ P.parts.card
-- Mathlib.Order.Category.PartOrdEmb
PartOrdEmb.hasForgetToPartOrd : CategoryTheory.HasForget₂ PartOrdEmb PartOrd
-- Mathlib.Order.Heyting.Hom
CoheytingHom.toLatticeHom : {α : Type u_6} →
  {β : Type u_7} → [inst : CoheytingAlgebra α] → [inst_1 : CoheytingAlgebra β] → CoheytingHom α β → LatticeHom α β
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
MeasurableSpace.measurableSet_countablePartition : ∀ {α : Type u_1} [m : MeasurableSpace α] [h : MeasurableSpace.CountablyGenerated α] (n : ℕ) {s : Set α},
  s ∈ MeasurableSpace.countablePartition α n → MeasurableSet s
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.inv_hom_apply : ∀ {R S : RingCat} (e : R ≅ S) (r : ↑R),
  (CategoryTheory.ConcreteCategory.hom e.inv) ((CategoryTheory.ConcreteCategory.hom e.hom) r) = r
-- Mathlib.Topology.MetricSpace.Gluing
Metric.instInhabitedInductiveLimitOfOfNatNat : {X : ℕ → Type u} →
  [inst : (n : ℕ) → MetricSpace (X n)] →
    {f : (n : ℕ) → X n → X (n + 1)} →
      (I : ∀ (n : ℕ), Isometry (f n)) → [Inhabited (X 0)] → Inhabited (Metric.InductiveLimit I)
-- Mathlib.CategoryTheory.Sites.Closed
/-- Closing under `J` is stable under pullback.  -/
CategoryTheory.GrothendieckTopology.pullback_close : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J₁ : CategoryTheory.GrothendieckTopology C) {X Y : C}
  (f : Y ⟶ X) (S : CategoryTheory.Sieve X),
  J₁.close (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f (J₁.close S)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    t.isEmpty = false →
      ∀ {km fallback : α}, t.minKeyD fallback = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (compare km k).isLE = true
-- Init.Data.String.Basic
/-- Constructs a valid position `s` from a position, panicking if the position is not valid.  -/
String.pos! : (s : String) → String.Pos.Raw → s.Pos
-- Mathlib.Algebra.GroupWithZero.Basic
isNilpotent_iff_eq_zero : ∀ {R : Type u_3} {x : R} [inst : MonoidWithZero R] [IsReduced R], IsNilpotent x ↔ x = 0
-- Mathlib.Probability.Moments.Covariance
ProbabilityTheory.covariance_const_left : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {Y : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ] (c : ℝ), ProbabilityTheory.covariance (fun x => c) Y μ = 0
-- Mathlib.Combinatorics.Hindman
/-- We could have taken this as the definition of `U * V`, but then we would have to prove that it
defines an ultrafilter.  -/
Ultrafilter.eventually_mul : ∀ {M : Type u_1} [inst : Mul M] (U V : Ultrafilter M) (p : M → Prop),
  (∀ᶠ (m : M) in ↑(U * V), p m) ↔ ∀ᶠ (m : M) in ↑U, ∀ᶠ (m' : M) in ↑V, p (m * m')
-- Mathlib.Data.Finset.Pi
Finset.restrict_def : ∀ {ι : Type u_2} {π : ι → Type u_3} (s : Finset ι), s.restrict = fun f x => f ↑x
-- Mathlib.Data.List.Lookmap
List.lookmap_some : ∀ {α : Type u_1} (l : List α), List.lookmap some l = l
-- Mathlib.RingTheory.PowerSeries.Derivative
PowerSeries.derivative_inv' : ∀ {R : Type u_1} [inst : Field R] (f : PowerSeries R),
  (PowerSeries.derivative R) f⁻¹ = -f⁻¹ ^ 2 * (PowerSeries.derivative R) f
-- Batteries.Control.LawfulMonadState
/-- Setting the monad twice is the same as just setting to the final state.  -/
LawfulMonadStateOf.set_bind_set : ∀ {σ : semiOutParam (Type u_1)} {m : Type u_1 → Type u_2} {inst : Monad m} {inst_1 : MonadStateOf σ m}
  [self : LawfulMonadStateOf σ m] (s s' : σ),
  (do
      set s
      set s') =
    set s'
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
MonotoneOn.const_mul' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α} {s : Set β}
  [MulLeftMono α], MonotoneOn f s → ∀ (a : α), MonotoneOn (fun x => a * f x) s
-- Mathlib.Algebra.Order.WithTop.Untop0
WithTop.le_of_untop₀_le_untop₀ : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] {a b : WithTop α},
  a ≠ ⊤ → a.untop₀ ≤ b.untop₀ → a ≤ b
-- Mathlib.Analysis.Seminorm
/-- Seminorm-balls at the origin are balanced.  -/
Seminorm.balanced_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) (r : ℝ), Balanced 𝕜 (p.ball 0 r)
-- Init.Internal.Order.Basic
Lean.Order.monotone_stateTRun : ∀ {γ : Sort u_1} {m : Type u_2 → Type u_3} {σ α : Type u_2} [inst : Lean.Order.PartialOrder γ] [Monad m]
  [inst_2 : (α : Type u_2) → Lean.Order.PartialOrder (m α)] (f : γ → StateT σ m α),
  Lean.Order.monotone f → ∀ (s : σ), Lean.Order.monotone fun x => (f x).run s
-- Mathlib.RingTheory.Ideal.Maximal
Ideal.IsMaximal.exists_inv : ∀ {α : Type u} [inst : Semiring α] {I : Ideal α}, I.IsMaximal → ∀ {x : α}, x ∉ I → ∃ y, ∃ i ∈ I, y * x + i = 1
-- Mathlib.Analysis.Calculus.Deriv.Inv
derivWithin_inv' : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {s : Set 𝕜} {𝕜' : Type u_1}
  [inst_1 : NontriviallyNormedField 𝕜'] [inst_2 : NormedAlgebra 𝕜 𝕜'] {c : 𝕜 → 𝕜'},
  DifferentiableWithinAt 𝕜 c s x → c x ≠ 0 → derivWithin c⁻¹ s x = -derivWithin c s x / c x ^ 2
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.cyclesMap'_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₁ ⟶ S₂) (φ₂ : S₂ ⟶ S₃) (h₁ : S₁.LeftHomologyData)
  (h₂ : S₂.LeftHomologyData) (h₃ : S₃.LeftHomologyData),
  CategoryTheory.ShortComplex.cyclesMap' (CategoryTheory.CategoryStruct.comp φ₁ φ₂) h₁ h₃ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.cyclesMap' φ₁ h₁ h₂)
      (CategoryTheory.ShortComplex.cyclesMap' φ₂ h₂ h₃)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.Point.zero_def : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R}, 0 = WeierstrassCurve.Affine.Point.zero
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- If `L` and `R` are semilinear maps whose composite is linear, and `f` has Fréchet derivative
`f'` at `R z`, then `L ∘ f ∘ R` has Fréchet derivative `L ∘ f' ∘ R` at `z`.  -/
HasFDerivAt.comp_semilinear : ∀ {𝕜 : Type u_1} {V : Type u_2} {V' : Type u_3} {W : Type u_4} {W' : Type u_5} [inst : NontriviallyNormedField 𝕜]
  {σ σ' : 𝕜 →+* 𝕜} [inst_1 : NormedAddCommGroup V] [inst_2 : NormedSpace 𝕜 V] [inst_3 : NormedAddCommGroup V']
  [inst_4 : NormedSpace 𝕜 V'] [inst_5 : NormedAddCommGroup W] [inst_6 : NormedSpace 𝕜 W]
  [inst_7 : NormedAddCommGroup W'] [inst_8 : NormedSpace 𝕜 W'] [RingHomIsometric σ] [inst_10 : RingHomInvPair σ σ']
  (L : W →SL[σ] W') (R : V' →SL[σ'] V) {f : V → W} {z : V'} {f' : V →L[𝕜] W},
  HasFDerivAt f f' (R z) → HasFDerivAt (⇑L ∘ f ∘ ⇑R) (L ∘SL f' ∘SL R) z
-- Mathlib.NumberTheory.Bernoulli
_private.Mathlib.NumberTheory.Bernoulli.0.Bernoulli.pIntegral : (p : ℕ) → ℚ → [Fact (Nat.Prime p)] → Prop
-- Init.Data.Iterators.Consumers.Monadic.Loop
_private.Init.Data.Iterators.Consumers.Monadic.Loop.0.Std.IterM.DefaultConsumers.forIn'.match_3.eq_3 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (property : it.IsPlausibleStep Std.IterStep.done)
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.done, property⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_3 property
-- Mathlib.Topology.NhdsWithin
nhdsWithin_restrict'' : ∀ {α : Type u_1} [inst : TopologicalSpace α] {a : α} (s : Set α) {t : Set α},
  t ∈ nhdsWithin a s → nhdsWithin a s = nhdsWithin a (s ∩ t)
-- Mathlib.CategoryTheory.MorphismProperty.Limits
CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C},
  autoParam
      (∀ (J : Type w') [inst_1 : CategoryTheory.Category.{w, w'} J] [CategoryTheory.IsFiltered J],
        W.IsStableUnderColimitsOfShape J)
      CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.isStableUnderColimitsOfShape._autoParam →
    CategoryTheory.MorphismProperty.IsStableUnderFilteredColimits.{w, w', v, u} W
-- Mathlib.Probability.Moments.Variance
ProbabilityTheory.variance_const_sub : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {X : Ω → ℝ} {μ : MeasureTheory.Measure Ω}
  [MeasureTheory.IsProbabilityMeasure μ],
  MeasureTheory.AEStronglyMeasurable X μ →
    ∀ (c : ℝ), ProbabilityTheory.variance (fun ω => c - X ω) μ = ProbabilityTheory.variance X μ
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.extendedDayPeriodIndex : Std.Time.ExtendedDayPeriod → Fin 6
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.smul_comp : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} {U : Type u_5} [inst : Monoid G] [inst_1 : Ring R]
  [inst_2 : AddCommGroup V] [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V]
  [inst_6 : AddCommGroup W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : Module R W]
  [inst_10 : AddCommGroup U] [inst_11 : Module R U] [inst_12 : TopologicalSpace U] [inst_13 : IsTopologicalAddGroup U]
  {π₁ : ContRepresentation R G V} {π₂ : ContRepresentation R G W} {π₃ : ContRepresentation R G U} {S : Type u_7}
  [inst_14 : Monoid S] [inst_15 : DistribMulAction S U] [inst_16 : SMulCommClass R S U]
  [inst_17 : ContinuousConstSMul S U] [inst_18 : LinearMap.CompatibleSMul U U S R] (s : S)
  (f : ContIntertwiningMap π₂ π₃) (g : ContIntertwiningMap π₁ π₂), (s • f).comp g = s • f.comp g
-- Init.Control.MonadAttach
/-- Like `Bind.bind`, `pbind` sequences two computations `x : m α` and `f`,
allowing the second to depend on the value computed by the first.
But other than with `Bind.bind`, the second computation can also depend on a proof that
the return value `a` of `x` satisfies `MonadAttach.CanReturn x a`.
 -/
MonadAttach.pbind : {m : Type u_1 → Type u_2} →
  {α β : Type u_1} → [Monad m] → [inst : MonadAttach m] → (x : m α) → ((a : α) → MonadAttach.CanReturn x a → m β) → m β
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedFunctor.mk.inj : ∀ {𝒮 : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} 𝒮} {𝒳 : CategoryTheory.BasedCategory 𝒮}
  {𝒴 : CategoryTheory.BasedCategory 𝒮} {toFunctor : CategoryTheory.Functor 𝒳.obj 𝒴.obj}
  {w : autoParam (toFunctor.comp 𝒴.p = 𝒳.p) CategoryTheory.BasedFunctor.w._autoParam}
  {toFunctor_1 : CategoryTheory.Functor 𝒳.obj 𝒴.obj}
  {w_1 : autoParam (toFunctor_1.comp 𝒴.p = 𝒳.p) CategoryTheory.BasedFunctor.w._autoParam},
  { toFunctor := toFunctor, w := w } = { toFunctor := toFunctor_1, w := w_1 } → toFunctor = toFunctor_1
-- Mathlib.MeasureTheory.Group.Action
MeasureTheory.vadd_set_ae_eq : ∀ {G : Type u} {α : Type w} {m : MeasurableSpace α} [inst : AddGroup G] [inst_1 : AddAction G α]
  {μ : MeasureTheory.Measure α} [MeasureTheory.VAddInvariantMeasure G α μ] (c : G) {s t : Set α},
  c +ᵥ s =ᵐ[μ] c +ᵥ t ↔ s =ᵐ[μ] t
-- Mathlib.GroupTheory.GroupAction.MultipleTransitivity
MulAction.IsMultiplyPretransitive.eq_1 : ∀ (G : Type u_1) (α : Type u_2) [inst : Group G] [inst_1 : MulAction G α] (n : ℕ),
  MulAction.IsMultiplyPretransitive G α n = MulAction.IsPretransitive G (Fin n ↪ α)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
/-- The root form of an anisotropic pairing as an invariant form.  -/
RootPairing.toInvariantForm : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : Fintype ι] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : CommRing R] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] → (P : RootPairing ι R M N) → [P.IsAnisotropic] → P.InvariantForm
-- Mathlib.CategoryTheory.Subfunctor.Finite
/-- A subpresheaf of types is "finite" if it is generated by finitely many sections.  -/
CategoryTheory.Subfunctor.IsFinite : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor Cᵒᵖ (Type w)} → CategoryTheory.Subfunctor F → Prop
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_ofList_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → (Std.HashMap.Raw.ofList l).getKey! k' = k
-- Mathlib.Data.List.Sigma
List.sizeOf_dedupKeys : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] [inst_1 : SizeOf (Sigma β)] (xs : List (Sigma β)),
  sizeOf xs.dedupKeys ≤ sizeOf xs
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- The kernel of `biproduct.π f i` is `⨁ Subtype.restrict {i}ᶜ f`.  -/
CategoryTheory.Limits.kernelBiproductπIso : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (f : J → C) →
          (i : J) →
            [inst_2 : CategoryTheory.Limits.HasBiproduct f] →
              [inst_3 : CategoryTheory.Limits.HasBiproduct (Subtype.restrict (fun j => j ≠ i) f)] →
                CategoryTheory.Limits.kernel (CategoryTheory.Limits.biproduct.π f i) ≅
                  ⨁ Subtype.restrict (fun j => j ≠ i) f
-- Lean.Parser.Basic
Lean.Parser.ParserState.mergeErrors : Lean.Parser.ParserState → ℕ → Lean.Parser.Error → Lean.Parser.ParserState
-- Init.Data.UInt.Lemmas
UInt32.add_eq_left : ∀ {a b : UInt32}, a + b = a ↔ b = 0
-- Mathlib.Order.Filter.AtTopBot.Defs
Filter.Frequently.forall_exists_of_atBot : ∀ {α : Type u_3} [inst : Preorder α] {p : α → Prop}, (∃ᶠ (x : α) in Filter.atBot, p x) → ∀ (a : α), ∃ b ≤ a, p b
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.apply_symm_apply_eq_coordChangeL : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e e' : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e]
  [inst_9 : Bundle.Trivialization.IsLinear R e'] {b : B},
  b ∈ e.baseSet ∩ e'.baseSet → ∀ (v : F), ↑e' (↑e.symm (b, v)) = (b, (Bundle.Trivialization.coordChangeL R e e' b) v)
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extMk_comp_mk₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.ProjectiveResolution X) {n : ℕ}
  (f : R.complex.X n ⟶ Y) (m : ℕ) (hm : n + 1 = m) (hf : CategoryTheory.CategoryStruct.comp (R.complex.d m n) f = 0)
  {Y' : C} (g : Y ⟶ Y'),
  (R.extMk f m hm hf).comp (CategoryTheory.Abelian.Ext.mk₀ g) ⋯ =
    R.extMk (CategoryTheory.CategoryStruct.comp f g) m hm ⋯
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roi.isEmpty.eq_1 : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] (r : Std.Roi α), r.isEmpty = (Std.PRange.succ? r.lower).isNone
-- Mathlib.Data.Sum.Order
OrderIso.sumDualDistrib_symm_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : LE α] [inst_1 : LE β] (a : α),
  (OrderIso.sumDualDistrib α β).symm (Sum.inl (OrderDual.toDual a)) = OrderDual.toDual (Sum.inl a)
-- Mathlib.AlgebraicTopology.ModelCategory.Homotopy
HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass_symm_mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant X] [inst_3 : HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y),
  HomotopicalAlgebra.leftHomotopyClassEquivRightHomotopyClass.symm (HomotopicalAlgebra.RightHomotopyClass.mk f) =
    HomotopicalAlgebra.LeftHomotopyClass.mk f
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
/-- The endomorphisms of `M` acts on `(ι → R) →ₗ[R] M`, and takes the projection
to a `(ι → R) →ₗ[R] M`.  -/
PiToModule.fromEnd : {ι : Type u_1} →
  [Fintype ι] →
    {M : Type u_2} →
      [inst : AddCommGroup M] →
        (R : Type u_3) → [inst_1 : CommRing R] → [inst_2 : Module R M] → (ι → M) → Module.End R M →ₗ[R] (ι → R) →ₗ[R] M
-- Mathlib.GroupTheory.Nilpotent
AddSubgroup.isNilpotent_of_lowerCentralSeries_eq_bot : ∀ {G : Type u_1} [inst : AddGroup G] {S : AddSubgroup G} {n : ℕ}, S.lowerCentralSeries n = ⊥ → AddGroup.IsNilpotent ↥S