mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
/-- The canonical morphism `Δ[1] ⟶ TopCat.toSSet.obj TopCat.I`: by adjunction,
it corresponds to the isomorphism `toTopObjIsoI : |Δ[1]| ≅ TopCat.I`.  -/
SSet.stdSimplex.toSSetObjI : SSet.stdSimplex.obj { len := 1 } ⟶ TopCat.toSSet.obj TopCat.I
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Implementation of `Mon.equivLaxMonoidalFunctorPUnit`.  -/
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.unitIso : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.Functor.id (CategoryTheory.LaxMonoidalFunctor (CategoryTheory.Discrete PUnit.{w + 1}) C) ≅
        (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.laxMonoidalToMon C).comp
          (CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.monToLaxMonoidal C)
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableOn.of_subsingleton_codomain : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {s : Set α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε'] [inst_1 : ESeminormedAddMonoid ε'] [Subsingleton ε'] {f : α → ε'},
  MeasureTheory.IntegrableOn f s μ
-- Init.Data.String.Lemmas.Order
String.Pos.ofSliceFrom_lt_iff : ∀ {s : String} {p₀ : s.Pos} {p : (s.sliceFrom p₀).Pos} {q : s.Pos},
  String.Pos.ofSliceFrom p < q ↔ ∃ (h : p₀ ≤ q), p < p₀.sliceFrom q h
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.str : (self : AddCommMonCat) → AddCommMonoid ↑self
-- Std.Data.TreeMap.Raw.Slice
Std.TreeMap.Raw.instSliceableRiiSlice : {α : Type u} →
  {β : Type v} →
    (cmp : autoParam (α → α → Ordering) Std.TreeMap.Raw.instSliceableRiiSlice._auto_1) →
      Std.Rii.Sliceable (Std.TreeMap.Raw α β cmp) α (Std.DTreeMap.Internal.Const.RiiSlice α β)
-- Mathlib.CategoryTheory.MorphismProperty.Descent
CategoryTheory.MorphismProperty.DescendsAlong.of_isPullback : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {P Q : CategoryTheory.MorphismProperty C}
  [self : P.DescendsAlong Q] {A X Y Z : C} {fst : A ⟶ X} {snd : A ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g → Q f → P fst → P g
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.Hom.mk.injEq : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} ι] [inst_2 : CategoryTheory.Abelian C]
  {X X' : CategoryTheory.Abelian.SpectralObject C ι} (hom : (n : ℤ) → X.H n ⟶ X'.H n)
  (comm :
    autoParam
      (∀ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
        CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁) ((hom n₁).app (CategoryTheory.ComposableArrows.mk₁ f)) =
          CategoryTheory.CategoryStruct.comp ((hom n₀).app (CategoryTheory.ComposableArrows.mk₁ g))
            (X'.δ f g n₀ n₁ hn₁))
      CategoryTheory.Abelian.SpectralObject.Hom.comm._autoParam)
  (hom_1 : (n : ℤ) → X.H n ⟶ X'.H n)
  (comm_1 :
    autoParam
      (∀ (n₀ n₁ : ℤ) (hn₁ : n₀ + 1 = n₁) {i j k : ι} (f : i ⟶ j) (g : j ⟶ k),
        CategoryTheory.CategoryStruct.comp (X.δ f g n₀ n₁ hn₁)
            ((hom_1 n₁).app (CategoryTheory.ComposableArrows.mk₁ f)) =
          CategoryTheory.CategoryStruct.comp ((hom_1 n₀).app (CategoryTheory.ComposableArrows.mk₁ g))
            (X'.δ f g n₀ n₁ hn₁))
      CategoryTheory.Abelian.SpectralObject.Hom.comm._autoParam),
  ({ hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 }) = (hom = hom_1)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Arctan
Real.arctan_mem_Ioo : ∀ (x : ℝ), Real.arctan x ∈ Set.Ioo (-(Real.pi / 2)) (Real.pi / 2)
-- Std.Data.DTreeMap.AdditionalOperations
/-- Given a proof that such a mapping exists, retrieves the key-value pair with the largest key that is
less than the given key.
 -/
Std.DTreeMap.getEntryLT : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      [Std.TransCmp cmp] → (t : Std.DTreeMap α β cmp) → (k : α) → (∃ a ∈ t, cmp a k = Ordering.lt) → (a : α) × β a
-- Mathlib.RingTheory.Extension.Presentation.Basic
/-- A presentation of an `R`-algebra `S` is a family of
generators with `σ → MvPolynomial ι R`: The assignment of
each relation to a polynomial in the generators.
 -/
Algebra.Presentation : (R : Type u) →
  (S : Type v) →
    Type w → Type t → [inst : CommRing R] → [inst_1 : CommRing S] → [Algebra R S] → Type (max (max (max t u) v) w)
-- Lean.Server.Completion.SyntheticCompletion
_private.Lean.Server.Completion.SyntheticCompletion.0.Lean.Server.Completion.findBest?.isBetter : {α : Type} → (α → α → Bool) → Option α → Option α → Bool
-- Mathlib.FieldTheory.Minpoly.Field
/-- The minimal polynomial of `0` is `X`.  -/
minpoly.zero : ∀ (A : Type u_1) (B : Type u_2) [inst : Field A] [inst_1 : Ring B] [inst_2 : Algebra A B] [Nontrivial B],
  minpoly A 0 = Polynomial.X
-- Init.Data.List.Basic
List.intersperse.eq_3 : ∀ {α : Type u} (sep a : α) (as : List α),
  (as = [] → False) → List.intersperse sep (a :: as) = a :: sep :: List.intersperse sep as
-- Mathlib.Algebra.Category.AlgCat.Basic
_private.Mathlib.Algebra.Category.AlgCat.Basic.0.AlgCat.Hom.mk.sizeOf_spec : ∀ {R : Type u} [inst : CommRing R] {A B : AlgCat R} [inst_1 : SizeOf R] (hom' : ↑A →ₐ[R] ↑B),
  sizeOf { hom' := hom' } = 1 + sizeOf hom'
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.Meq.condition : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [inst_3 : CategoryTheory.ConcreteCategory D FD] {X : C}
  {P : CategoryTheory.Functor Cᵒᵖ D} {S : J.Cover X} (x : CategoryTheory.Meq P S) (I : S.Relation),
  (CategoryTheory.ConcreteCategory.hom (P.map I.r.g₁.op)) (↑x (S.shape.fst I)) =
    (CategoryTheory.ConcreteCategory.hom (P.map I.r.g₂.op)) (↑x (S.shape.snd I))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKeyD_filter_key : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → Bool} {k fallback : α},
  m.WF → (Std.DHashMap.Raw.filter (fun k x => f k) m).getKeyD k fallback = (Option.filter f (m.getKey? k)).getD fallback
-- Mathlib.Data.Set.Pairwise.Basic
Set.pairwiseDisjoint_range_singleton : ∀ {ι : Type u_4}, (Set.range singleton).PairwiseDisjoint id
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.lineDerivCLM_apply_of_le : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace ℝ E] {Ω : TopologicalSpace.Opens E} {F : Type u_4} [inst_3 : NormedAddCommGroup F]
  [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace 𝕜 F] {n k : ℕ∞} [inst_6 : Algebra ℝ 𝕜] [inst_7 : IsScalarTower ℝ 𝕜 F]
  {f : TestFunction Ω F n} {v x : E}, k + 1 ≤ n → ((TestFunction.lineDerivCLM 𝕜 v) f) x = lineDeriv ℝ (⇑f) x v
-- Mathlib.NumberTheory.Modular
/-- The image of the fundamental domain `𝒟` in `ℂ` is closed.
This is not immediate (unlike the analogous statement for `𝒟ᵒ`),
since the inclusion of `ℍ` in `ℂ` is an open but not a closed map.
 -/
ModularGroup.isClosed_coe_fd : IsClosed (UpperHalfPlane.coe '' ModularGroup.fd)
-- Mathlib.Algebra.GroupWithZero.Action.TransferInstance
/-- Transfer `SMulZeroClass` across an `Equiv`  -/
Equiv.smulZeroClass : (M : Type u_1) →
  {A : Type u_3} → {B : Type u_4} → (e : A ≃ B) → [inst : Zero B] → [SMulZeroClass M B] → SMulZeroClass M A
-- Std.Data.DHashMap.Internal.AssocList.Iterator
_private.Std.Data.DHashMap.Internal.AssocList.Iterator.0.Std.DHashMap.Internal.AssocList.instIteratorAssocListIteratorIdSigma.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : Std.IterStep (Std.IterM Id ((a : α) × β a)) ((a : α) × β a) → Sort u_3) →
      (x : Std.IterStep (Std.IterM Id ((a : α) × β a)) ((a : α) × β a)) →
        ((it' : Std.IterM Id ((a : α) × β a)) → (out : (a : α) × β a) → motive (Std.IterStep.yield it' out)) →
          ((it : Std.IterM Id ((a : α) × β a)) → motive (Std.IterStep.skip it)) →
            (Unit → motive Std.IterStep.done) → motive x
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.getKey?_insertManyIfNewUnit_list_of_not_mem_of_mem : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] (h : t.WF)
  {l : List α} {k k' : α},
  compare k k' = Ordering.eq →
    k ∉ t →
      List.Pairwise (fun a b => ¬compare a b = Ordering.eq) l →
        k ∈ l → (↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit t l ⋯)).getKey? k' = some k
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
/-- Eta-expanded form of `MeasureTheory.StronglyMeasurable.inf` -/
MeasureTheory.StronglyMeasurable.fun_inf : ∀ {α : Type u_1} {β : Type u_2} {f g : α → β} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Min β]
  [ContinuousInf β],
  MeasureTheory.StronglyMeasurable f →
    MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun i => f i ⊓ g i
-- Mathlib.Order.Filter.EventuallyConst
Filter.EventuallyConst.comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {l : Filter α} {f : α → β},
  Filter.EventuallyConst f l → ∀ (g : β → γ), Filter.EventuallyConst (g ∘ f) l
-- Mathlib.NumberTheory.Padics.HeightOneSpectrum
Rat.HeightOneSpectrum.primesEquiv.eq_1 : ∀ {R : Type u_2} [inst : CommRing R] [inst_1 : Algebra R ℚ] [inst_2 : IsIntegralClosure R ℤ ℚ]
  [inst_3 : IsDedekindDomain R],
  Rat.HeightOneSpectrum.primesEquiv =
    { toFun := fun v => ⟨Rat.HeightOneSpectrum.natGenerator v, ⋯⟩,
      invFun := fun p =>
        have h := ⋯;
        IsDedekindDomain.HeightOneSpectrum.ofPrime h,
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Topology.TietzeExtension
/-- **Tietze extension theorem** for real-valued bounded continuous maps, a version for a closed
set. Let `s` be a closed set in a normal topological space `Y`. Let `f` be a bounded continuous
real-valued function on `s`. Let `t` be a nonempty convex set of real numbers (we use
`OrdConnected` instead of `Convex` to automatically deduce this argument by typeclass search) such
that `f x ∈ t` for all `x : s`. Then there exists a bounded continuous real-valued function
`g : Y →ᵇ ℝ` such that `g y ∈ t` for all `y` and `g.domRestrict s = f`.  -/
BoundedContinuousFunction.exists_forall_mem_domRestrict_eq_of_closed : ∀ {Y : Type u_2} [inst : TopologicalSpace Y] [NormalSpace Y] {s : Set Y} (f : BoundedContinuousFunction ↑s ℝ),
  IsClosed s →
    ∀ {t : Set ℝ} [t.OrdConnected], (∀ (x : ↑s), f x ∈ t) → t.Nonempty → ∃ g, (∀ (y : Y), g y ∈ t) ∧ g.domRestrict s = f
-- Mathlib.Data.Nat.Log
/-- See also `log_lt_of_lt_pow'` for a version that assumes `x ≠ 0` instead of `y ≠ 0`.  -/
Nat.log_lt_of_lt_pow : ∀ {b x y : ℕ}, y ≠ 0 → y < b ^ x → Nat.log b y < x
-- Mathlib.Algebra.QuadraticAlgebra.Defs
instDecidableEqQuadraticAlgebra : {R : Type u_1} → {a b : R} → [DecidableEq R] → DecidableEq (QuadraticAlgebra R a b)
-- Mathlib.SetTheory.Ordinal.Principal
Ordinal.add_of_omega0_opow_le : ∀ {a b c : Ordinal.{u}}, a < Ordinal.omega0 ^ b → Ordinal.omega0 ^ b ≤ c → a + c = c
-- Mathlib.Analysis.Analytic.CPolynomial
CPolynomialAt.sub : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f g : E → F} {x : E},
  CPolynomialAt 𝕜 f x → CPolynomialAt 𝕜 g x → CPolynomialAt 𝕜 (f - g) x
-- Mathlib.Order.OrdContinuous
RightOrdContinuous.coe_toOrderEmbedding : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] {f : α → β}
  (hf : RightOrdContinuous f) (h : Function.Injective f), ⇑(RightOrdContinuous.toOrderEmbedding f hf h) = f
-- Mathlib.Algebra.Homology.DerivedCategory.ExactFunctor
CategoryTheory.Functor.instLiftingHomotopyCategoryIntUpDerivedCategoryQhQuasiIsoCompMapHomotopyCategoryMapDerivedCategory : {C₁ : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
    [inst_1 : CategoryTheory.Abelian C₁] →
      [inst_2 : HasDerivedCategory C₁] →
        {C₂ : Type u₂} →
          [inst_3 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_4 : CategoryTheory.Abelian C₂] →
              [inst_5 : HasDerivedCategory C₂] →
                (F : CategoryTheory.Functor C₁ C₂) →
                  [inst_6 : F.Additive] →
                    [inst_7 : CategoryTheory.Limits.PreservesFiniteLimits F] →
                      [inst_8 : CategoryTheory.Limits.PreservesFiniteColimits F] →
                        CategoryTheory.Localization.Lifting DerivedCategory.Qh
                          (HomotopyCategory.quasiIso C₁ (ComplexShape.up ℤ))
                          ((F.mapHomotopyCategory (ComplexShape.up ℤ)).comp DerivedCategory.Qh) F.mapDerivedCategory
-- Mathlib.Topology.Algebra.Ring.Basic
/-- The additive homeomorphism from a topological ring to itself,
induced by left multiplication by a unit.  -/
ContinuousAddEquiv.mulLeft : {R : Type u_1} → [inst : TopologicalSpace R] → [inst_1 : Semiring R] → [IsTopologicalSemiring R] → Rˣ → R ≃ₜ+ R
-- Mathlib.NumberTheory.SelbergSieve
BoundingSieve.mk : Finset ℕ →
  (prodPrimes : ℕ) →
    Squarefree prodPrimes →
      (weights : ℕ → ℝ) →
        (∀ (n : ℕ), 0 ≤ weights n) →
          ℝ →
            (nu : ArithmeticFunction ℝ) →
              nu.IsMultiplicative →
                (∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes → 0 < nu p) →
                  (∀ (p : ℕ), Nat.Prime p → p ∣ prodPrimes → nu p < 1) → BoundingSieve
-- Batteries.Data.Vector.Lemmas
Vector.toList_tail : ∀ {α : Type u_1} {n : ℕ} {v : Vector α n}, v.tail.toList = v.toList.tail
-- Mathlib.Lean.Expr.Basic
/-- Given `(hNotEx : Not (@Exists.{lvl} A p))`,
return a `forall x, Not (p x)` and a proof for it.

This function handles nested existentials.  -/
_private.Mathlib.Lean.Expr.Basic.0.Lean.Expr.forallNot_of_notExists.go : Lean.Level → Lean.Expr → Lean.Expr → Lean.Expr → Lean.MetaM (Lean.Expr × Lean.Expr)
-- Init.Data.BitVec.Lemmas
BitVec.lt_irrefl : ∀ {n : ℕ} (x : BitVec n), ¬x < x
-- Mathlib.RingTheory.WittVector.Domain
WittVector.eq_iterate_verschiebung : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] {x : WittVector p R} {n : ℕ},
  (∀ i < n, x.coeff i = 0) → x = (⇑WittVector.verschiebung)^[n] (x.shift n)
-- Lean.KeyedDeclsAttribute
Lean.KeyedDeclsAttribute.tableRef : {γ : Type} → Lean.KeyedDeclsAttribute γ → IO.Ref (Lean.KeyedDeclsAttribute.Table γ)
-- Mathlib.Tactic.FunProp.Theorems
Mathlib.Meta.FunProp.Theorem.transition.injEq : ∀ (thm thm_1 : Mathlib.Meta.FunProp.GeneralTheorem),
  (Mathlib.Meta.FunProp.Theorem.transition thm = Mathlib.Meta.FunProp.Theorem.transition thm_1) = (thm = thm_1)
-- Mathlib.CategoryTheory.GlueData
CategoryTheory.GlueData.diagramIso_hom_app_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v, u₁} C] {C' : Type u₂} [inst_1 : CategoryTheory.Category.{v, u₂} C']
  (D : CategoryTheory.GlueData C) (F : CategoryTheory.Functor C C')
  [inst_2 : ∀ (i j k : D.J), CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.cospan (D.f i j) (D.f i k)) F]
  (i : D.J),
  (D.diagramIso F).hom.app (CategoryTheory.Limits.WalkingMultispan.right i) =
    CategoryTheory.CategoryStruct.id ((D.diagram.multispan.comp F).obj (CategoryTheory.Limits.WalkingMultispan.right i))
-- Mathlib.CategoryTheory.Sites.Coverage
CategoryTheory.Coverage.toPrecoverage : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.Coverage C → CategoryTheory.Precoverage C
-- Mathlib.Logic.Equiv.Set
Equiv.prod_assoc_symm_image : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} {s : Set α} {t : Set β} {u : Set γ},
  ⇑(Equiv.prodAssoc α β γ).symm '' s ×ˢ t ×ˢ u = (s ×ˢ t) ×ˢ u
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Idempotent
/-- **Alias** of the forward direction of `ContinuousLinearMap.IsIdempotentElem.ker_mem_invtSubmodule_iff`.

---

`ker f` is invariant under `T` if and only if `f ∘L T ∘L f = f ∘L T`,
for idempotent `f`.  -/
ContinuousLinearMap.IsIdempotentElem.conj_eq_of_ker_mem_invtSubmodule : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace M] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] {f T : M →L[R] M},
  IsIdempotentElem f → (↑f).ker ∈ Module.End.invtSubmodule ↑T → f ∘SL T ∘SL f = f ∘SL T
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Sieve.pullback_pushforward_le : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Sieve X),
  CategoryTheory.Sieve.pushforward f (CategoryTheory.Sieve.pullback f R) ≤ R
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBit.mk.inj : ∀ {var w : ℕ} {idx : Fin w} {var_1 w_1 : ℕ} {idx_1 : Fin w_1},
  { var := var, w := w, idx := idx } = { var := var_1, w := w_1, idx := idx_1 } → var = var_1 ∧ w = w_1 ∧ idx ≍ idx_1
-- Mathlib.Algebra.Lie.Graded
LieDerivation.ofGradingSum.eq_1 : ∀ {ι : Type u_1} {R : Type u_3} {L : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid ι] [inst_2 : CommRing R]
  [inst_3 : LieRing L] [inst_4 : LieAlgebra R L] (ℒ : ι → Submodule R L) [inst_5 : GradedLieAlgebra ℒ] (φ : ι →+ R),
  LieDerivation.ofGradingSum ℒ φ =
    {
      toLinearMap :=
        DirectSum.toModule R ι (DirectSum ι fun i => ↥(ℒ i)) fun i =>
          DirectSum.lof R ι (fun x => ↥(ℒ x)) i ∘ₗ Module.End.smulLeft (φ i) ⋯,
      leibniz' := ⋯ }
-- Mathlib.Data.Prod.TProd
List.TProd.elim.eq_def : ∀ {ι : Type u} {α : ι → Type v} [inst : DecidableEq ι] (x : List ι) (x_1 : List.TProd α x) (x_2 : ι) (x_3 : x_2 ∈ x),
  x_1.elim x_3 =
    match x, x_1, x_2, x_3 with
    | i :: is, v, j, hj =>
      if hji : j = i then
        Eq.ndrec (motive := fun i => List.TProd α (i :: is) → j ∈ i :: is → α j) (fun v hj => v.1) hji v hj
      else List.TProd.elim v.2 ⋯
-- Mathlib.RingTheory.IsTensorProduct
Algebra.IsPushout.cancelBaseChangeAlg_symm_tmul : ∀ (R : Type u_1) (S : Type v₃) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] (A : Type u_8)
  (B : Type u_9) [inst_3 : CommRing A] [inst_4 : CommRing B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : Algebra A B] [inst_8 : Algebra S B] [inst_9 : IsScalarTower R A B] [inst_10 : IsScalarTower R S B]
  [inst_11 : Algebra.IsPushout R S A B] (C : Type u_11) [inst_12 : CommRing C] [inst_13 : Algebra R C]
  [inst_14 : Algebra A C] [inst_15 : IsScalarTower R A C] (s : S) (c : C),
  (Algebra.IsPushout.cancelBaseChangeAlg R S A B C).symm (s ⊗ₜ[R] c) = (algebraMap S B) s ⊗ₜ[A] c
-- Mathlib.Order.Category.NonemptyFinLinOrd
NonemptyFinLinOrd.instSplitEpiCategory : CategoryTheory.SplitEpiCategory NonemptyFinLinOrd
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.instPartialOrder : {K : Type u_1} →
  {L : Type u_2} → [inst : Field K] → [inst_1 : Field L] → [inst_2 : Algebra K L] → PartialOrder (IntermediateField K L)
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.congr_left_φH : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex C} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  {γ₁ γ₂ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂}, γ₁ = γ₂ → γ₁.left.φH = γ₂.left.φH
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex_d_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (F G : CochainComplex C ℤ) (i j : ℤ) (a : CochainComplex.HomComplex.Cochain F G i),
  (AddCommGrpCat.Hom.hom ((F.HomComplex G).d i j)) a = CochainComplex.HomComplex.δ i j a
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.take_succ_eq_append_of_drop_eq_cons : ∀ {α : Type u_1} {xs : List α} {k : ℕ} {y : α} {ys : List α},
  List.drop k xs = y :: ys → List.take (k + 1) xs = List.take k xs ++ [y]
-- Mathlib.NumberTheory.Modular
/-- The standard open fundamental domain of the action of `SL(2,ℤ)` on `ℍ`.  -/
Modular.«term𝒟ᵒ» : Lean.ParserDescr
-- Mathlib.Topology.Category.Stonean.Basic
CompHaus.lift.eq_1 : ∀ {X Y : CompHaus} {Z : Stonean} (e : Z.compHaus ⟶ Y) (f : X ⟶ Y) [inst : CategoryTheory.Epi f],
  CompHaus.lift e f = CategoryTheory.Projective.factorThru e f
-- Init.Data.Range.Polymorphic.IntLemmas
Int.isSome_getElem?_toArray_roc_eq : ∀ {m n : ℤ} {i : ℕ}, ((m<...=n).toArray[i]?.isSome = true) = (i < (n - m).toNat)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get!_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited β] {k : α}, k ∉ m₁ → Std.DHashMap.Const.get! (m₁.diff m₂) k = default
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.Heap.head?.eq_1 : ∀ {α : Type u_1} (le : α → α → Bool),
  Batteries.BinomialHeap.Imp.Heap.head? le Batteries.BinomialHeap.Imp.Heap.nil = none
-- Mathlib.MeasureTheory.Category.MeasCat
MeasCat.instFunLikeSubtypeForallCarrierMeasurable : (X : MeasCat) → (Y : MeasCat) → FunLike { f // Measurable f } X.carrier Y.carrier
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.shift_shift_neg' : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddGroup A]
  [inst_2 : CategoryTheory.HasShift C A] {X Y : C} (f : X ⟶ Y) (i : A),
  (CategoryTheory.shiftFunctor C (-i)).map ((CategoryTheory.shiftFunctor C i).map f) =
    CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorCompIsoId C i (-i) ⋯).hom.app X)
      (CategoryTheory.CategoryStruct.comp f ((CategoryTheory.shiftFunctorCompIsoId C i (-i) ⋯).inv.app Y))
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_map : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] (p : Polynomial R) (f : R →+* S),
  Polynomial.derivative (Polynomial.map f p) = Polynomial.map f (Polynomial.derivative p)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
/-- Matrices with entries in a non-unital C⋆-algebra form a non-unital C⋆-algebra.  -/
CStarMatrix.instNonUnitalCStarAlgebra : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] →
    [inst_1 : PartialOrder A] →
      [StarOrderedRing A] → {n : Type u_3} → [Fintype n] → NonUnitalCStarAlgebra (CStarMatrix n n A)
-- Mathlib.NumberTheory.ArithmeticFunction.Defs
ArithmeticFunction.map_zero : ∀ {R : Type u_1} [inst : Zero R] {f : ArithmeticFunction R}, f 0 = 0
-- Mathlib.Algebra.Homology.ShortComplex.Homology
/-- We shall say that a category `C` is a category with homology when all short complexes
have homology.  -/
CategoryTheory.CategoryWithHomology : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Limits.HasZeroMorphisms C] → Prop
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.instInhabited : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {M : Type u_8} →
      {M₂ : Type u_10} →
        [inst : Semiring R₁] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Module R₁ M] → [inst_5 : Module R₂ M₂] → {σ₁₂ : R₁ →+* R₂} → Inhabited (M →ₛₗ[σ₁₂] M₂)
-- Std.Time.DateTime.Timestamp
Std.Time.Timestamp.compare_def : compare = compareOn fun x => x.val
-- Aesop.Options.Public
/-- Maximum number of norm rules applied to a single goal. When this limit is
exceeded, normalisation is likely stuck in an infinite loop, so Aesop fails. 0
means no limit.
 -/
Aesop.Options.maxNormIterations : Aesop.Options → ℕ
-- Mathlib.Data.Rel
SetRel.comp_iUnion : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {ι : Sort u_5} (R : SetRel α β) (S : ι → SetRel β γ),
  R.comp (⋃ i, S i) = ⋃ i, R.comp (S i)
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.instInhabitedQuotientAddSubgroup.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α),
  QuotientAddGroup.instInhabitedQuotientAddSubgroup s = { default := ↑0 }
-- Init.Simproc
/-- A builtin simplification procedure declaration.
 -/
Lean.Parser.«command_Builtin_simproc_decl_(_):=_» : Lean.ParserDescr
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
le_rank_iff_exists_linearIndependent_finset : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [Module.Free K V] {n : ℕ}, ↑n ≤ Module.rank K V ↔ ∃ s, s.card = n ∧ LinearIndependent K Subtype.val