mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendMap_id : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] (K : HomologicalComplex C c) (e : c.Embedding c'),
  HomologicalComplex.extendMap (CategoryTheory.CategoryStruct.id K) e = CategoryTheory.CategoryStruct.id (K.extend e)
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.integral_monotoneOn_of_integrand_ae : ∀ {α : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : PartialOrder E] [IsOrderedAddMonoid E] [IsOrderedModule ℝ E]
  [ClosedIciTopology E] {β : Type u_6} [inst_6 : Preorder β] {f : α → β → E} {s : Set β},
  (∀ᵐ (x : α) ∂μ, MonotoneOn (f x) s) →
    (∀ a ∈ s, MeasureTheory.Integrable (fun x => f x a) μ) → MonotoneOn (fun b => ∫ (x : α), f x b ∂μ) s
-- Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities
_private.Mathlib.RingTheory.MvPolynomial.Symmetric.NewtonIdentities.0.MvPolynomial.NewtonIdentities.pairMap_involutive : ∀ (σ : Type u_1) [inst : DecidableEq σ], Function.Involutive (MvPolynomial.NewtonIdentities.pairMap✝ σ)
-- Std.Do.WP.SimpLemmas
_private.Std.Do.WP.SimpLemmas.0.Option.isSome.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (val : α) (h_1 : (val : α) → motive (some val))
  (h_2 : Unit → motive none),
  (match some val with
    | some val => h_1 val
    | none => h_2 ()) =
    h_1 val
-- Mathlib.Geometry.Euclidean.Sphere.SecondInter
/-- If the vector is zero, `secondInter` gives the original point.  -/
EuclideanGeometry.Sphere.secondInter_zero : ∀ (V : Type u_1) {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] (s : EuclideanGeometry.Sphere P) (p : P), s.secondInter p 0 = p
-- Mathlib.Probability.Kernel.Basic
ProbabilityTheory.Kernel.deterministic.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β) (hf : Measurable f),
  ProbabilityTheory.Kernel.deterministic f hf =
    { toFun := fun a => MeasureTheory.Measure.dirac (f a), measurable' := ⋯ }
-- Mathlib.Analysis.InnerProductSpace.PiL2
/-- Given a natural number `n` one less than the `finrank` of a finite-dimensional inner product
space, there exists an isometry from the orthogonal complement of a nonzero singleton to
`EuclideanSpace 𝕜 (Fin n)`.  -/
OrthonormalBasis.fromOrthogonalSpanSingleton : {𝕜 : Type u_3} →
  [inst : RCLike 𝕜] →
    {E : Type u_4} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : InnerProductSpace 𝕜 E] →
          (n : ℕ) → [Fact (Module.finrank 𝕜 E = n + 1)] → {v : E} → v ≠ 0 → OrthonormalBasis (Fin n) 𝕜 ↥(𝕜 ∙ v)ᗮ
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Scheme
AlgebraicGeometry.ProjectiveSpectrum.Proj.toStalk_specStalkEquiv : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubgroupClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f : A) (x : ↥(ProjectiveSpectrum.basicOpen 𝒜 f)) {m : ℕ} (f_deg : f ∈ 𝒜 m) (hm : 0 < m),
  CategoryTheory.CategoryStruct.comp
      (AlgebraicGeometry.StructureSheaf.toStalk (HomogeneousLocalization.Away 𝒜 f)
        ((CategoryTheory.ConcreteCategory.hom (AlgebraicGeometry.ProjectiveSpectrum.Proj.toSpec 𝒜 f).base) x))
      (AlgebraicGeometry.ProjectiveSpectrum.Proj.specStalkEquiv 𝒜 f x f_deg hm).hom =
    CommRingCat.ofHom (HomogeneousLocalization.mapId 𝒜 ⋯)
-- Mathlib.Topology.MetricSpace.ShrinkingLemma
/-- Let `R : α → ℝ` be a (possibly discontinuous) positive function on a proper metric space. Then
there exists a collection of pairs of balls `Metric.ball (c i) (r i)`, `Metric.ball (c i) (r' i)`
such that

* for all `i` we have `0 < r i < r' i < R (c i)`;
* the family of balls `Metric.ball (c i) (r' i)` is locally finite;
* the balls `Metric.ball (c i) (r i)` cover the whole space.

This is a simple corollary of `refinement_of_locallyCompact_sigmaCompact_of_nhds_basis`
and `exists_iUnion_ball_eq_radius_pos_lt` or `exists_locallyFinite_subset_iUnion_ball_radius_lt`.  -/
exists_locallyFinite_iUnion_eq_ball_radius_lt : ∀ {α : Type u} [inst : MetricSpace α] [ProperSpace α] {R : α → ℝ},
  (∀ (x : α), 0 < R x) →
    ∃ ι c r r',
      (∀ (i : ι), 0 < r i ∧ r i < r' i ∧ r' i < R (c i)) ∧
        (LocallyFinite fun i => Metric.ball (c i) (r' i)) ∧ ⋃ i, Metric.ball (c i) (r i) = Set.univ
-- Lean.Data.Lsp.Window
Lean.Lsp.instFromJsonShowMessageRequestParams.fromJson : Lean.Json → Except String Lean.Lsp.ShowMessageRequestParams
-- Mathlib.Algebra.GroupWithZero.Basic
pow_ne_zero : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] {a : M₀} [IsReduced M₀] (n : ℕ), a ≠ 0 → a ^ n ≠ 0
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
/-- **Alias** of the reverse direction of `Matrix.separatingLeft_transpose_iff`. -/
Matrix.SeparatingRight.separatingLeft_transpose : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Finite m]
  [inst_2 : Finite n], M.SeparatingRight → M.transpose.SeparatingLeft
-- Mathlib.RingTheory.Coalgebra.Basic
/-- Data fields for `Coalgebra`, to allow API to be constructed before proving `Coalgebra.coassoc`.

See `Coalgebra` for documentation.  -/
CoalgebraStruct : (R : Type u) → (A : Type v) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid A] → [Module R A] → Type (max u v)
-- Mathlib.Order.Filter.Bases.Basic
/-- A version of `eventually_prod_self_iff` that is more suitable for forward rewriting.  -/
Filter.eventually_prod_self_iff' : ∀ {α : Type u_1} {la : Filter α} {r : α × α → Prop},
  (∀ᶠ (x : α × α) in la ×ˢ la, r x) ↔ ∃ t ∈ la, ∀ x ∈ t, ∀ y ∈ t, r (x, y)
-- Mathlib.SetTheory.Cardinal.Ordinal
Ordinal.card_iSup_Iio_le_card_mul_iSup : ∀ {o : Ordinal.{u}} (f : ↑(Set.Iio o) → Ordinal.{max u v}),
  (⨆ a, f a).card ≤ Cardinal.lift.{v, u} o.card * ⨆ a, (f a).card
-- Mathlib.Algebra.Group.Subgroup.Defs
/-- A subgroup of a group inherits an integer power  -/
Subgroup.zpow : {G : Type u_1} → [inst : Group G] → (H : Subgroup G) → Pow ↥H ℤ
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.symm_trans_apply : ∀ {R₁ : Type u_2} {R₂ : Type u_3} {R₃ : Type u_4} {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} [inst : Semiring R₁]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M₁] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] {module_M₁ : Module R₁ M₁} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} {σ₁₃ : R₁ →+* R₃} {σ₃₁ : R₃ →+* R₁} [inst_6 : RingHomInvPair σ₁₃ σ₃₁]
  [inst_7 : RingHomInvPair σ₃₁ σ₁₃] {σ₂₃ : R₂ →+* R₃} {σ₃₂ : R₃ →+* R₂} {re₁₂ : RingHomInvPair σ₁₂ σ₂₁}
  {re₂₁ : RingHomInvPair σ₂₁ σ₁₂} {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃}
  [inst_8 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_9 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {e₁₂ : M₁ ≃ₛₗ[σ₁₂] M₂}
  {e₂₃ : M₂ ≃ₛₗ[σ₂₃] M₃} (c : M₃), (e₁₂.trans e₂₃).symm c = e₁₂.symm (e₂₃.symm c)
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.LiftRel.swap_lem : ∀ {α : Type u} {β : Type v} {R : α → β → Prop} {s1 : Stream'.WSeq α} {s2 : Stream'.WSeq β},
  Stream'.WSeq.LiftRel R s1 s2 → Stream'.WSeq.LiftRel (Function.swap R) s2 s1
-- Init.Data.String.Lemmas.Pattern.TakeDrop.String
String.Slice.revAll_slice_iff : ∀ {pat s : String.Slice}, s.revAll pat = true ↔ ∃ n, s.copy = String.join (List.replicate n pat.copy)
-- Mathlib.Data.List.Cycle
_private.Mathlib.Data.List.Cycle.0.List.nextOr.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → α → α → Sort u_2) (head x default : α) (h_1 : (x default : α) → motive [] x default)
  (h_2 : (head x default : α) → motive [head] x default)
  (h_3 : (y z : α) → (xs : List α) → (x default : α) → motive (y :: z :: xs) x default),
  (match [head], x, default with
    | [], x, default => h_1 x default
    | [head], x, default => h_2 head x default
    | y :: z :: xs, x, default => h_3 y z xs x default) =
    h_2 head x default
-- Lean.Elab.AutoBound
/-- Checks whether a string is a name that can be auto-bound when the `relaxedAutoImplicit` option is
set to `false`.

In "strict" auto implicit mode, a identifier can only be auto-bound if it is a single character (`α`
or `x`) or has an arbitrary postfix sequence of numbers, subscripts, and underscores. Therefore,
both `αᵣₒₛₑ₂₁₁'''` and `X123_45` can be auto-bound even with `relaxedAutoBound` set to `false`.
 -/
_private.Lean.Elab.AutoBound.0.Lean.Elab.isValidAutoBoundSuffix : String → Bool
-- Mathlib.Tactic.FunProp.Theorems
/-- map: function property name × theorem type → lambda theorem  -/
Mathlib.Meta.FunProp.LambdaTheorems.theorems : Mathlib.Meta.FunProp.LambdaTheorems →
  Std.HashMap (Lean.Name × Mathlib.Meta.FunProp.LambdaTheoremType) (Array Mathlib.Meta.FunProp.LambdaTheorem)
-- Mathlib.Algebra.Module.LinearMap.Polynomial
/-- `LinearMap.polyCharpolyAux` is independent of the choice of basis of the target module.

Proof strategy:
1. Rewrite `polyCharpolyAux` as the (honest, ordinary) characteristic polynomial
   of the base change of `φ` to the multivariate polynomial ring `MvPolynomial ι R`.
2. Use that the characteristic polynomial of a linear map is independent of the choice of basis.
   This independence result is used transitively via
   `LinearMap.polyCharpolyAux_map_aeval` and `LinearMap.polyCharpolyAux_map_eq_charpoly`.
 -/
LinearMap.polyCharpolyAux_basisIndep : ∀ {R : Type u_1} {L : Type u_2} {M : Type u_3} {ι : Type u_5} {ιM : Type u_7} [inst : CommRing R]
  [inst_1 : AddCommGroup L] [inst_2 : Module R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M]
  (φ : L →ₗ[R] Module.End R M) [inst_5 : Fintype ι] [inst_6 : Fintype ιM] [inst_7 : DecidableEq ι]
  [inst_8 : DecidableEq ιM] (b : Module.Basis ι R L) (bₘ : Module.Basis ιM R M) {ιM' : Type u_8} [inst_9 : Fintype ιM']
  [inst_10 : DecidableEq ιM'] (bₘ' : Module.Basis ιM' R M), φ.polyCharpolyAux b bₘ = φ.polyCharpolyAux b bₘ'
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.span_map_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z),
  (CategoryTheory.Limits.span f g).map CategoryTheory.Limits.WalkingSpan.Hom.fst = f
-- Mathlib.RingTheory.Binomial
Ring.descPochhammer_eq_factorial_smul_choose : ∀ {R : Type u_1} [inst : NonAssocRing R] [inst_1 : Pow R ℕ] [inst_2 : BinomialRing R] [NatPowAssoc R] (r : R) (n : ℕ),
  (descPochhammer ℤ n).smeval r = n.factorial • Ring.choose r n
-- Init.Data.Nat.Internal.SOM
_private.Init.Data.Nat.Internal.SOM.0.Nat.Internal.SOM.Mon.mul.go.match_1.eq_1 : ∀ (motive : Nat.Internal.SOM.Mon → Nat.Internal.SOM.Mon → Sort u_1) (m₁ : Nat.Internal.SOM.Mon)
  (h_1 : (m₁ : Nat.Internal.SOM.Mon) → motive m₁ []) (h_2 : (m₂ : Nat.Internal.SOM.Mon) → motive [] m₂)
  (h_3 :
    (v₁ : Nat.Internal.Linear.Var) →
      (m₁ : List Nat.Internal.Linear.Var) →
        (v₂ : Nat.Internal.Linear.Var) → (m₂ : List Nat.Internal.Linear.Var) → motive (v₁ :: m₁) (v₂ :: m₂)),
  (match m₁, [] with
    | m₁, [] => h_1 m₁
    | [], m₂ => h_2 m₂
    | v₁ :: m₁, v₂ :: m₂ => h_3 v₁ m₁ v₂ m₂) =
    h_1 m₁
-- Mathlib.Tactic.Contrapose
Mathlib.Tactic.Contrapose.contrapose_iff₂ : ∀ {p q : Prop}, (p ↔ ¬q) → (¬p ↔ q)
-- Mathlib.Computability.Primrec.Basic
Primrec.succ : Primrec Nat.succ
-- Mathlib.MeasureTheory.Function.SimpleFuncDenseLp
MeasureTheory.SimpleFunc.memLp_approxOn : ∀ {β : Type u_2} {E : Type u_4} [inst : MeasurableSpace β] [inst_1 : MeasurableSpace E] [inst_2 : NormedAddCommGroup E]
  {p : ENNReal} [inst_3 : BorelSpace E] {f : β → E} {μ : MeasureTheory.Measure β} (fmeas : Measurable f),
  MeasureTheory.MemLp f p μ →
    ∀ {s : Set E} {y₀ : E} (h₀ : y₀ ∈ s) [inst_4 : TopologicalSpace.SeparableSpace ↑s],
      MeasureTheory.MemLp (fun x => y₀) p μ →
        ∀ (n : ℕ), MeasureTheory.MemLp (⇑(MeasureTheory.SimpleFunc.approxOn f fmeas s y₀ h₀ n)) p μ
-- Mathlib.Algebra.Homology.SpectralObject.Basic
CategoryTheory.Abelian.SpectralObject.Hom.mk : {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) →
              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 →
                X.Hom X'
-- Mathlib.AlgebraicTopology.SimplicialSet.CategoryWithFibrations
SSet.modelCategoryQuillen.fibrations_eq : HomotopicalAlgebra.fibrations SSet = SSet.modelCategoryQuillen.J.rlp
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
/-- The ideal of `MvPolynomial (ℕ × M) R` generated by `Rel`.  -/
DividedPowerAlgebra.RelI : (R : Type u_2) →
  (M : Type u_3) → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [Module R M] → Ideal (MvPolynomial (ℕ × M) R)
-- Mathlib.RingTheory.MvPolynomial.Homogeneous
MvPolynomial.totalDegree_eq_zero_iff : ∀ (σ : Type u_1) {R : Type u_3} [inst : CommSemiring R] (p : MvPolynomial σ R),
  p.totalDegree = 0 ↔ ∀ m ∈ p.support, ∀ (x : σ), m x = 0
-- Mathlib.Data.QPF.Univariate.Basic
QPF.recF_eq' : ∀ {F : Type u → Type v} [q : QPF F] {α : Type u} (g : F α → α) (a : (QPF.P F).A) (f : (QPF.P F).B a → (QPF.P F).W),
  QPF.recF g (WType.mk a f) = g (QPF.abs ((QPF.P F).map (QPF.recF g) ⟨a, f⟩))
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.norm_sub_eq_max : ∀ {α : Type u} [inst : TopologicalSpace α] {R : Type u_1} [inst_1 : NonUnitalSeminormedRing R] [IsCancelMulZero R]
  {f g : BoundedContinuousFunction α R}, f * g = 0 → ‖f - g‖ = max ‖f‖ ‖g‖
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- The weights for a single vertex of a simplex, in terms of
`pointsWithCircumcenter`.  -/
Affine.Simplex.pointWeightsWithCircumcenter : {n : ℕ} → Fin (n + 1) → Affine.Simplex.PointsWithCircumcenterIndex n → ℝ
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiff.continuous : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞}, ContDiff 𝕜 n f → Continuous f
-- Mathlib.ModelTheory.PartialEquiv
FirstOrder.Language.PartialEquiv.ext : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  {f g : L.PartialEquiv M N} (h_dom : f.dom = g.dom),
  (∀ (x : M) (h : x ∈ f.dom), f.cod.subtype (f.toEquiv ⟨x, h⟩) = g.cod.subtype (g.toEquiv ⟨x, ⋯⟩)) → f = g
-- Mathlib.Data.Setoid.Partition
IndexedPartition.equivQuotient_index_apply : ∀ {ι : Type u_1} {α : Type u_2} {s : ι → Set α} (hs : IndexedPartition s) (x : α),
  hs.equivQuotient (hs.index x) = hs.proj x
-- Mathlib.Analysis.Fourier.AddCircleMulti
/-- The star subalgebra of `C(UnitAddTorus d, ℂ)` generated by `mFourier n` for `n ∈ ℤᵈ` is in fact
the linear span of these functions.  -/
UnitAddTorus.mFourierSubalgebra_coe : ∀ {d : Type u_1} [inst : Fintype d],
  Subalgebra.toSubmodule (UnitAddTorus.mFourierSubalgebra d).toSubalgebra =
    Submodule.span ℂ (Set.range UnitAddTorus.mFourier)
-- Mathlib.Tactic.NormNum.Result
Nat.rawCast.eq_1 : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ), n.rawCast = ↑n
-- Mathlib.RingTheory.Valuation.Minpoly
/-- For any unit `x : Lˣ`, we prove that a certain power of the valuation of zeroth coefficient of
the minimal polynomial of `x` over `K` is nonzero. This lemma is helpful for defining the valuation
on `L` inducing `v`.  -/
Valuation.pow_coeff_zero_ne_zero_of_unit : ∀ {K : Type u_1} [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] (v : Valuation K Γ₀)
  {L : Type u_3} [inst_2 : Field L] [inst_3 : Algebra K L] [FiniteDimensional K L] (x : L),
  IsUnit x → v ((minpoly K x).coeff 0) ^ (Module.finrank K L / (minpoly K x).natDegree) ≠ 0
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_eq_some_iff : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α} {v : β},
      Std.DTreeMap.Internal.Impl.Const.get? t k = some v ↔
        ∃ (h : Std.DTreeMap.Internal.Impl.contains k t = true), Std.DTreeMap.Internal.Impl.Const.get t k h = v
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cocycle.leftShift_coe : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cocycle K L n) (a n' : ℤ) (hn' : n + a = n'),
  ↑(γ.leftShift a n' hn') = (↑γ).leftShift a n' hn'
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_r_ge : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r) (C : ℝ), ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), C ≤ ↑(r i n)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.not_mem_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∈ t₂ → k ∉ t₁ \ t₂
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.vadd_zero_oreSub_zero_vadd : ∀ {R : Type u_1} {M : Type u_3} {X : Type u_4} [inst : AddMonoid M] {S : AddSubmonoid M}
  [inst_1 : AddOreLocalization.AddOreSet S] [inst_2 : AddAction M X] [inst_3 : VAdd R X] [inst_4 : VAdd R M]
  [inst_5 : VAddAssocClass R M M] [inst_6 : VAddAssocClass R M X] (r : R) (x : AddOreLocalization S X),
  ((r +ᵥ 0) -ₒ 0) +ᵥ x = r +ᵥ x
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.getD_ofList_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α} {k k' fallback : α},
  cmp k k' = Ordering.eq →
    List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (Std.TreeSet.ofList l cmp).getD k' fallback = k
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.Expr.neg.inj : ∀ {a a_1 : Lean.Grind.Linarith.Expr}, a.neg = a_1.neg → a = a_1
-- Mathlib.Order.Monotone.Defs
StrictMono.comp : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {g : β → γ}
  {f : α → β}, StrictMono g → StrictMono f → StrictMono (g ∘ f)
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.matchesAt_iff : ∀ {p : Char → Bool} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.MatchesAt p pos ↔ ∃ (h : pos ≠ s.endPos), p (pos.get h) = true
-- Mathlib.Combinatorics.Graph.Subgraph
/-- `IsSubgraph H G` is NOT the preferred spelling for the subgraph relation. Please use
`H ≤ G` instead.  -/
Graph.IsSubgraph : {α : Type u_1} → {β : Type u_2} → Graph α β → Graph α β → Prop
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.interface.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.interface = 1
-- Mathlib.Algebra.Group.Submonoid.Operations
AddSubmonoid.map_inr : ∀ {N : Type u_2} [inst : AddZeroClass N] {M : Type u_5} [inst_1 : AddZeroClass M] (s : AddSubmonoid N),
  AddSubmonoid.map (AddMonoidHom.inr M N) s = ⊥.prod s
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁_obj_obj_map : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X₁ X₂ : C)
  {X Y : C} (φ : X ⟶ Y),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₃₁ C).obj X₁).obj X₂).map φ =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X₂ X X₁).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X₂ (CategoryTheory.MonoidalCategoryStruct.whiskerRight φ X₁))
        (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y X₁).inv)
-- Mathlib.Algebra.Free
instDecidableEqFreeAddMagma.decEq : {α : Type u_1} → [DecidableEq α] → (x x_1 : FreeAddMagma α) → Decidable (x = x_1)
-- Mathlib.Tactic.OfNat
/-- This macro is a shorthand for `OfNat.ofNat` combined with `no_index`.

When writing lemmas about `OfNat.ofNat`, the term needs to be wrapped
in `no_index` so as not to confuse `simp`, as `no_index (OfNat.ofNat n)`.

Some discussion is [on Zulip here](https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/.E2.9C.94.20Polynomial.2Ecoeff.20example/near/395438147).
 -/
«termOfNat(_)» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- The map of an empty cocone is a colimit iff the mapped object is initial.
 -/
CategoryTheory.Limits.isColimitMapCoconeEmptyCoconeEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (G : CategoryTheory.Functor C D) →
          (X : C) →
            CategoryTheory.Limits.IsColimit (G.mapCocone (CategoryTheory.Limits.asEmptyCocone X)) ≃
              CategoryTheory.Limits.IsInitial (G.obj X)
-- Batteries.Tactic.Congr
/-- Configuration options for `congr` & `rcongr`  -/
Batteries.Tactic.Congr.Config : Type
-- Lean.Syntax
/-- Converts an `original` or `synthetic (canonical := true)` `SourceInfo` to a
`synthetic (canonical := false)` `SourceInfo`.
This is sometimes useful when `SourceInfo` is being moved around between `Syntax`es.
 -/
Lean.SourceInfo.nonCanonicalSynthetic : Lean.SourceInfo → Lean.SourceInfo
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.logSizeBallStruct.mk.inj : ∀ {T : Type u_2} {finset : Finset T} {point : T} {radius : ℕ} {finset_1 : Finset T} {point_1 : T} {radius_1 : ℕ},
  { finset := finset, point := point, radius := radius } =
      { finset := finset_1, point := point_1, radius := radius_1 } →
    finset = finset_1 ∧ point = point_1 ∧ radius = radius_1
-- Mathlib.NumberTheory.DirichletCharacter.Orthogonality
/-- If `R` is an integral domain that has enough roots of unity and `n ≠ 0`, then
for `a` in `ZMod n`, the sum of `χ a` over all Dirichlet characters mod `n`
with values in `R` vanishes if `a ≠ 1` and has the value `n.totient` if `a = 1`.  -/
DirichletCharacter.sum_characters_eq : ∀ (R : Type u_1) [inst : CommRing R] {n : ℕ} [NeZero n] [HasEnoughRootsOfUnity R (Monoid.exponent (ZMod n)ˣ)]
  [inst_3 : IsDomain R] (a : ZMod n), ∑ χ, χ a = if a = 1 then ↑n.totient else 0
-- Mathlib.MeasureTheory.Measure.Comap
MeasureTheory.Measure.comap_apply : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} (f : α → β),
  Function.Injective f →
    (∀ (s : Set α), MeasurableSet s → MeasurableSet (f '' s)) →
      ∀ (μ : MeasureTheory.Measure β), MeasurableSet s → (MeasureTheory.Measure.comap f μ) s = μ (f '' s)
-- Mathlib.CategoryTheory.Sites.Subsheaf
CategoryTheory.instEpiSheafTypeToImage : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  {F F' : CategoryTheory.Sheaf J (Type w)} (f : F ⟶ F'), CategoryTheory.Epi (CategoryTheory.Sheaf.toImage f)
-- Mathlib.Algebra.Order.Nonneg.Basic
Nonneg.add : {α : Type u_1} → [inst : AddZeroClass α] → [inst_1 : Preorder α] → [AddLeftMono α] → Add { x // 0 ≤ x }
-- Mathlib.Order.Category.Preord
/-- The underlying preordered type.  -/
Preord.carrier : Preord → Type u_1
-- Mathlib.Analysis.MeanInequalitiesPow
Real.rpow_add_rpow_le_add : ∀ {p a b : ℝ}, 0 ≤ a → 0 ≤ b → 1 ≤ p → (a ^ p + b ^ p) ^ (1 / p) ≤ a + b
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey!_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α], t.WF → ∀ {km : α}, t.minKey? = some km → t.getKey! km = km
-- Mathlib.SetTheory.Cardinal.Continuum
Cardinal.aleph0_le_continuum : Cardinal.aleph0 ≤ Cardinal.continuum
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.not_mem_inter_of_not_mem_right : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α}, k ∉ t₂ → k ∉ t₁ ∩ t₂