mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.card_smul_le : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t : Finset β},
  (s • t).card ≤ s.card * t.card
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.PreZeroHypercover.toPreOneHypercover_p₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  [inst_1 : E.HasPullbacks] (x x_1 : E.I₀) (x_2 : PUnit.{u_2 + 1}),
  E.toPreOneHypercover.p₂ x_2 = CategoryTheory.Limits.pullback.snd (E.f x) (E.f x_1)
-- Init.Data.Range.Polymorphic.SInt
Int64.instUpwardEnumerable : Std.PRange.UpwardEnumerable Int64
-- Mathlib.Algebra.Tropical.Basic
Tropical.leftInverse_trop : ∀ {R : Type u}, Function.LeftInverse Tropical.trop Tropical.untrop
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.toOpens_top : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G], ↑⊤ = ⊤
-- Mathlib.Topology.MetricSpace.Basic
/-- Pull back a metric space structure by an embedding. This is a version of
`MetricSpace.induced` useful in case if the domain already has a `TopologicalSpace` structure.  -/
Topology.IsEmbedding.comapMetricSpace : {α : Type u_2} →
  {β : Type u_3} →
    [inst : TopologicalSpace α] → [m : MetricSpace β] → (f : α → β) → Topology.IsEmbedding f → MetricSpace α
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.functorEquiv_functor_obj_fst_map : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (X : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  (J : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)) {X_1 Y : X} (f : X_1 ⟶ Y),
  ((CategoryTheory.Limits.CategoricalPullback.functorEquiv F G X).functor.obj J).fst.map f = (J.map f).fst
-- Mathlib.Algebra.Module.Submodule.Range
/-- The decreasing sequence of submodules consisting of the ranges of the iterates of a linear map.
 -/
LinearMap.iterateRange : {R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (M →ₗ[R] M) → ℕ →o (Submodule R M)ᵒᵈ
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- For `VAdd G X`, a block system of `X` is a partition of `X` into blocks
for the additive action of `G`  -/
AddAction.IsBlockSystem : (G : Type u_1) → [inst : AddGroup G] → {X : Type u_2} → [AddAction G X] → Set (Set X) → Prop
-- Mathlib.CategoryTheory.Triangulated.TStructure.ETrunc
CategoryTheory.Triangulated.TStructure.instIsIsoFunctorETruncLTιTopEInt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C), CategoryTheory.IsIso (t.eTruncLTι ⊤)
-- Mathlib.Topology.Order.OrderClosed
Ico_mem_nhdsLT_of_mem : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIicTopology α] {a b c : α},
  b ∈ Set.Ioc a c → Set.Ico a c ∈ nhdsWithin b (Set.Iio b)
-- Mathlib.Analysis.Complex.Angle
Complex.angle_div_right_eq_angle_mul_left : ∀ (a x y : ℂ), InnerProductGeometry.angle x (y / a) = InnerProductGeometry.angle (x * a) y
-- Mathlib.NumberTheory.ModularForms.ArithmeticSubgroups
Subgroup.relIndex_adjoinNegOne_ne_zero : ∀ {n : Type u_1} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_2} [inst_2 : Ring R] (𝒢 : Subgroup (GL n R)),
  𝒢.relIndex 𝒢.adjoinNegOne ≠ 0
-- Mathlib.Order.Filter.Finite
Finset.eventuallyEq_iUnion : ∀ {α : Type u} {l : Filter α} {ι : Type u_2} (s : Finset ι) {f g : ι → Set α},
  (∀ i ∈ s, f i =ᶠ[l] g i) → ⋃ i ∈ s, f i =ᶠ[l] ⋃ i ∈ s, g i
-- Init.Data.UInt.Lemmas
USize.toUInt8_neg : ∀ (a : USize), (-a).toUInt8 = -a.toUInt8
-- Mathlib.LinearAlgebra.AffineSpace.Ordered
left_lt_lineMap_iff_lt : ∀ {k : Type u_1} {E : Type u_2} [inst : Ring k] [inst_1 : PartialOrder k] [IsOrderedRing k] [inst_3 : AddCommGroup E]
  [inst_4 : PartialOrder E] [IsOrderedAddMonoid E] [inst_6 : Module k E] [IsStrictOrderedModule k E] {a b : E} {r : k}
  [PosSMulReflectLT k E], 0 < r → (a < (AffineMap.lineMap a b) r ↔ a < b)
-- Mathlib.Algebra.Order.Group.CompleteLattice
ciSup_mul : ∀ {ι : Type u_1} {G : Type u_2} [inst : Group G] [inst_1 : ConditionallyCompleteLattice G] [Nonempty ι] {f : ι → G}
  [MulRightMono G], BddAbove (Set.range f) → ∀ (a : G), (⨆ i, f i) * a = ⨆ i, f i * a
-- Mathlib.Tactic.NormNum.Inv
Mathlib.Meta.NormNum.isInt_inv_neg_one : ∀ {α : Type u_1} [inst : DivisionRing α] {a : α},
  Mathlib.Meta.NormNum.IsInt a (Int.negOfNat 1) → Mathlib.Meta.NormNum.IsInt a⁻¹ (Int.negOfNat 1)
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_exact.inj : ∀ {lhs : Bool} {c₁ : Lean.Meta.Grind.AC.EqCnstr} {c₂ : Lean.Meta.Grind.AC.DiseqCnstr} {lhs_1 : Bool}
  {c₁_1 : Lean.Meta.Grind.AC.EqCnstr} {c₂_1 : Lean.Meta.Grind.AC.DiseqCnstr},
  Lean.Meta.Grind.AC.DiseqCnstrProof.simp_exact lhs c₁ c₂ =
      Lean.Meta.Grind.AC.DiseqCnstrProof.simp_exact lhs_1 c₁_1 c₂_1 →
    lhs = lhs_1 ∧ c₁ = c₁_1 ∧ c₂ = c₂_1
-- Mathlib.Analysis.InnerProductSpace.Basic
/-- Given two orthogonal vectors, their sum and difference have equal norms.  -/
norm_sub_eq_norm_add : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {v w : E}, inner 𝕜 v w = 0 → ‖w - v‖ = ‖w + v‖
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonTextEdit.fromJson : Lean.Json → Except String Lean.Lsp.TextEdit
-- Mathlib.Combinatorics.SimpleGraph.Metric
SimpleGraph.edist_ne_top_iff_reachable : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V}, G.edist u v ≠ ⊤ ↔ G.Reachable u v
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.singleton_add_singleton : ∀ {α : Type u_2} [inst : Add α] {a b : α}, {a} + {b} = {a + b}
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.prodAssoc_symm_apply : ∀ (k : Type u_1) (P₁ : Type u_2) (P₂ : Type u_3) (P₃ : Type u_4) {V₁ : Type u_6} {V₂ : Type u_7} {V₃ : Type u_8}
  [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂] [inst_3 : AddCommGroup V₃]
  [inst_4 : Module k V₁] [inst_5 : Module k V₂] [inst_6 : Module k V₃] [inst_7 : AddTorsor V₁ P₁]
  [inst_8 : AddTorsor V₂ P₂] [inst_9 : AddTorsor V₃ P₃] (p : P₁ × P₂ × P₃),
  (AffineEquiv.prodAssoc k P₁ P₂ P₃).symm p = ((p.1, p.2.1), p.2.2)
-- Mathlib.Algebra.Category.Ring.Basic
RingCat.instFullSemiRingCatForget₂RingHomCarrierCarrier : (CategoryTheory.forget₂ RingCat SemiRingCat).Full
-- Init.Data.Range.Polymorphic.Lemmas
_private.Init.Data.Range.Polymorphic.Lemmas.0.Std.Roc.size.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) →
    (x : Option α) → (Unit → motive none) → ((lower : α) → motive (some lower)) → motive x
-- Lean.Meta.IntInstTesters
Lean.Meta.DefEq.isInstHSubInt : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Data.Fin.SuccPred
Fin.range_succ : ∀ (n : ℕ), Set.range Fin.succ = {0}ᶜ
-- Lean.Parser.Do
Lean.Parser.Term.doReassignArrow.formatter : Lean.PrettyPrinter.Formatter
-- Lean.Meta.Tactic.Grind.AC.Util
Lean.Meta.Grind.AC.checkMaxSteps : Lean.Meta.Grind.GoalM Bool
-- Lean.Elab.ErrorUtils
/-- Make an oxford-comma-separated list of strings.

- `["eats"].toOxford == "eats"`
- `["eats", "shoots"].toOxford == "eats and shoots"`
- `["eats", "shoots", "leaves"] == "eats, shoots, and leaves"`
 -/
_private.Lean.Elab.ErrorUtils.0.List.toOxford : {α : Type u_1} → [Append α] → [Lean.HasOxfordStrings✝ α] → List α → α
-- Mathlib.Analysis.Analytic.OfScalars
/-- A convenience lemma restating the result of `ofScalars_radius_eq_inv_of_tendsto` under
the inverse ratio.  -/
FormalMultilinearSeries.ofScalars_radius_eq_of_tendsto : ∀ {𝕜 : Type u_1} (E : Type u_2) [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing E] [inst_2 : NormedAlgebra 𝕜 E]
  (c : ℕ → 𝕜) [NormOneClass E] {r : NNReal},
  r ≠ 0 →
    Filter.Tendsto (fun n => ‖c n‖ / ‖c n.succ‖) Filter.atTop (nhds ↑r) →
      (FormalMultilinearSeries.ofScalars E c).radius = ↑r
-- Mathlib.Topology.EMetricSpace.BoundedVariation
/-- If a function has bounded variation, then the variation on small open-closed
intervals to the right of any point tends to `0`.  -/
BoundedVariationOn.tendsto_eVariationOn_Ioc_zero : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] [inst_2 : TopologicalSpace α]
  [OrderTopology α] {f : α → E} {s : Set α},
  BoundedVariationOn f s →
    ∀ (x : α), Filter.Tendsto (fun y => eVariationOn f (s ∩ Set.Ioc x y)) (nhdsWithin x s) (nhds 0)
-- Mathlib.Data.Finset.Card
Finset.card_def : ∀ {α : Type u_1} (s : Finset α), s.card = s.val.card
-- Mathlib.RingTheory.Congruence.Defs
/-- The induced additive congruence from a `RingCon`.  -/
RingCon.toAddCon : {R : Type u_1} → [inst : Add R] → [inst_1 : Mul R] → RingCon R → AddCon R
-- Init.Data.List.Basic
List.append_nil : ∀ {α : Type u} (as : List α), as ++ [] = as
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Turn a morphism in `AddCommMonCat` back into an `AddMonoidHom`.  -/
AddCommMonCat.Hom.hom : {X Y : AddCommMonCat} → X.Hom Y → ↑X →+ ↑Y
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.coend.map.eq_1 : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J] {C : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} C]
  {F : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_2 : CategoryTheory.Limits.HasCoend F]
  {F' : CategoryTheory.Functor Jᵒᵖ (CategoryTheory.Functor J C)} [inst_3 : CategoryTheory.Limits.HasCoend F']
  (f : F ⟶ F'),
  CategoryTheory.Limits.coend.map f =
    CategoryTheory.Limits.coend.desc
      (fun x => CategoryTheory.CategoryStruct.comp ((f.app (Opposite.op x)).app x) (CategoryTheory.Limits.coend.ι F' x))
      ⋯
-- Mathlib.Order.Atoms
IsAtom.not_disjoint_iff_le : ∀ {α : Type u_2} [inst : SemilatticeInf α] [inst_1 : OrderBot α] {a b : α}, IsAtom a → (¬Disjoint a b ↔ a ≤ b)
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.denom_J : ∀ (τ : ℂ), UpperHalfPlane.denom UpperHalfPlane.J τ = 1
-- Mathlib.Algebra.Module.LinearMap.Polynomial
LinearMap.toMvPolynomial_add : ∀ {R : Type u_1} {M₁ : Type u_2} {M₂ : Type u_3} {ι₁ : Type u_4} {ι₂ : Type u_5} [inst : CommRing R]
  [inst_1 : AddCommGroup M₁] [inst_2 : AddCommGroup M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂]
  [inst_5 : Fintype ι₁] [inst_6 : Finite ι₂] [inst_7 : DecidableEq ι₁] (b₁ : Module.Basis ι₁ R M₁)
  (b₂ : Module.Basis ι₂ R M₂) (f g : M₁ →ₗ[R] M₂),
  LinearMap.toMvPolynomial b₁ b₂ (f + g) = LinearMap.toMvPolynomial b₁ b₂ f + LinearMap.toMvPolynomial b₁ b₂ g
-- Batteries.Data.Array.Merge
/-- `O(|xs|)`. Replace each run `[x₁, ⋯, xₙ]` of equal elements in `xs` with
`f ⋯ (f (f x₁ x₂) x₃) ⋯ xₙ`.
 -/
Array.mergeAdjacentDups : {α : Type u_1} → [eq : BEq α] → (α → α → α) → Array α → Array α
-- Mathlib.NumberTheory.Height.NumberField
/-- The absolute logarithmic height of an algebraic number. This is defined for elements of any
field of characteristic zero, with a junk value of `0` if the element is not algebraic.  -/
NumberField.absLogHeight₁ : {K : Type u_2} → [inst : Field K] → [CharZero K] → K → ℝ
-- Mathlib.Algebra.Algebra.Operations
/-- The elements of `I / J` are the `x` such that `x • J ⊆ I`.

In fact, we define `x ∈ I / J` to be `∀ y ∈ J, x * y ∈ I` (see `mem_div_iff_forall_mul_mem`),
which is equivalent to `x • J ⊆ I` (see `mem_div_iff_smul_subset`), but nicer to use in proofs.

This is the general form of the ideal quotient, traditionally written $I : J$.
 -/
Submodule.instDiv : {R : Type u} →
  [inst : CommSemiring R] → {A : Type v} → [inst_1 : CommSemiring A] → [inst_2 : Algebra R A] → Div (Submodule R A)
-- Init.Data.Range.Polymorphic.Nat
Std.PRange.instLinearlyUpwardEnumerableNat : Std.PRange.LinearlyUpwardEnumerable ℕ
-- Mathlib.Topology.EMetricSpace.Defs
/-- The extended pseudodistance on a subtype of a pseudoemetric space is the restriction of
the original pseudodistance, by definition.  -/
Subtype.edist_mk_mk : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {p : α → Prop} {x y : α} (hx : p x) (hy : p y),
  edist ⟨x, hx⟩ ⟨y, hy⟩ = edist x y
-- Mathlib.Algebra.Category.CommAlgCat.FiniteType
instFullFGAlgCatUliftFunctor : ∀ (R : Type u) [inst : CommRing R], (FGAlgCat.uliftFunctor R).Full
-- Mathlib.Analysis.Asymptotics.TVS
/-- A stronger version of `IsBigOTVS.congr` that requires the functions only agree along the
filter.  -/
Asymptotics.IsBigOTVS.congr' : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f₁ f₂ : α → E} {g₁ g₂ : α → F} {l : Filter α},
  f₁ =O[𝕜; l] g₁ → f₁ =ᶠ[l] f₂ → g₁ =ᶠ[l] g₂ → f₂ =O[𝕜; l] g₂
-- Mathlib.Algebra.GCDMonoid.Basic
lcm_eq_one_iff : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a b : α), lcm a b = 1 ↔ a ∣ 1 ∧ b ∣ 1
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Alias** of `Ideal.count_le_of_ideal_ge`. -/
count_le_of_ideal_ge : ∀ {T : Type u_4} [inst : CommRing T] [inst_1 : IsDedekindDomain T] {I J : Ideal T},
  I ≤ J →
    I ≠ ⊥ →
      ∀ (K : Ideal T),
        Multiset.count K (UniqueFactorizationMonoid.normalizedFactors J) ≤
          Multiset.count K (UniqueFactorizationMonoid.normalizedFactors I)
-- Mathlib.Analysis.Complex.CauchyIntegral
/-- `f : ℂ → E` is entire iff it's differentiable  -/
Complex.analyticOnNhd_univ_iff_differentiable : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] [CompleteSpace E] {f : ℂ → E},
  AnalyticOnNhd ℂ f Set.univ ↔ Differentiable ℂ f
-- Mathlib.MeasureTheory.Function.LpSpace.Basic
/-- Positive part of a function in `L^p`.  -/
MeasureTheory.Lp.posPart : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {p : ENNReal} → {μ : MeasureTheory.Measure α} → ↥(MeasureTheory.Lp ℝ p μ) → ↥(MeasureTheory.Lp ℝ p μ)
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_diff_of_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k fallback : α}, k ∈ m₂ → (m₁ \ m₂).getKeyD k fallback = fallback
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.isEmpty_inter_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  (h₁ : m₁.WF),
  m₂.WF →
    ((m₁.inter m₂ ⋯).isEmpty = true ↔
      ∀ (k : α), Std.DTreeMap.Internal.Impl.contains k m₁ = true → Std.DTreeMap.Internal.Impl.contains k m₂ = false)
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.bientails.rfl : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, P ⊣⊢ₛ P
-- Mathlib.CategoryTheory.Limits.HasLimits
CategoryTheory.Limits.limit.lift.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasLimit F] (c : CategoryTheory.Limits.Cone F),
  CategoryTheory.Limits.limit.lift F c = (CategoryTheory.Limits.limit.isLimit F).lift c
-- Lean.Meta.ArgsPacker
/-- Given expressions `e₁`, `e₂` with types `(x : A) → (y : B[x]) → R`
and `(z : C) → R`, returns an expression of type
```
(x : (A ⊗ B) ⊕ C) → R
```
 -/
Lean.Meta.ArgsPacker.uncurryND : Lean.Meta.ArgsPacker → Array Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.Data.Matrix.Mul
/-- For two vectors `w` and `v`, `vecMulVec w v i j` is defined to be `w i * v j`.
Put another way, `vecMulVec w v` is exactly `replicateCol ι w * replicateRow ι v` for
`Unique ι`; see `vecMulVec_eq`.  -/
Matrix.vecMulVec : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [Mul α] → (m → α) → (n → α) → Matrix m n α
-- Init.Internal.Order.Basic
Lean.Order.PartialOrder.rel_of_eq : ∀ {α : Sort u} [inst : Lean.Order.PartialOrder α] {x y : α}, x = y → Lean.Order.PartialOrder.rel x y
-- Mathlib.Algebra.CharP.Algebra
/-- If `R` has characteristic `0`, then so does `FractionRing R`.  -/
IsFractionRing.charZero : ∀ (R : Type u_3) [inst : CommRing R] [IsDomain R] [CharZero R], CharZero (FractionRing R)
-- Init.Data.SInt.Bitwise
Int8.toBitVec_and : ∀ (a b : Int8), (a &&& b).toBitVec = a.toBitVec &&& b.toBitVec
-- Mathlib.CategoryTheory.Shift.CommShift
CategoryTheory.Functor.map_shiftFunctorComm_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] {A : Type u_4} [inst_2 : AddCommMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] [inst_4 : CategoryTheory.HasShift D A] (F : CategoryTheory.Functor C D)
  [inst_5 : F.CommShift A] (X : C) (a b : A) {Z : D}
  (h : F.obj ((CategoryTheory.shiftFunctor C a).obj ((CategoryTheory.shiftFunctor C b).obj X)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorComm C a b).hom.app X)) h =
    CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.Functor.commShiftIso F b).hom.app ((CategoryTheory.shiftFunctor C a).obj X))
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.shiftFunctor D b).map ((CategoryTheory.Functor.commShiftIso F a).hom.app X))
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorComm D a b).hom.app (F.obj X))
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.shiftFunctor D a).map ((CategoryTheory.Functor.commShiftIso F b).inv.app X))
            (CategoryTheory.CategoryStruct.comp
              ((CategoryTheory.Functor.commShiftIso F a).inv.app ((CategoryTheory.shiftFunctor C b).obj X)) h))))
-- Mathlib.Algebra.Algebra.Spectrum.Pi
/-- The equivalence between pre-quasiregular elements of a product and the product of
pre-quasiregular elements.  -/
PreQuasiregular.toProd : (A : Type u_2) →
  (B : Type u_3) →
    [inst : NonUnitalSemiring A] →
      [inst_1 : NonUnitalSemiring B] → PreQuasiregular (A × B) ≃* PreQuasiregular A × PreQuasiregular B
-- Mathlib.Logic.Basic
not_forall₂ : ∀ {α : Sort u_1} {p : α → Prop} {P : (x : α) → p x → Prop}, (¬∀ (x : α) (h : p x), P x h) ↔ ∃ x, ∃ (h : p x), ¬P x h
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw₀.modify.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m m_1 : Std.DHashMap.Internal.Raw₀ α β),
  m = m_1 → ∀ (a : α) (f f_1 : β a → β a), f = f_1 → m.modify a f = m_1.modify a f_1
-- Lean.Meta.Match.CaseArraySizes
Lean.Meta.CaseArraySizesSubgoal.diseqs : Lean.Meta.CaseArraySizesSubgoal → Array Lean.FVarId
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem!_map_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] [inst : Inhabited γ] {f : α → β → γ} {k k' : α},
  m.getKey? k = some k' → (Std.HashMap.map f m)[k]! = (Option.map (f k') m[k]?).get!
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.range_tensorHom : ∀ {X₁ X₂ Y₁ Y₂ : SSet} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₂),
  SSet.Subcomplex.range (CategoryTheory.MonoidalCategoryStruct.tensorHom f₁ f₂) =
    (SSet.Subcomplex.range f₁).prod (SSet.Subcomplex.range f₂)
-- Mathlib.Data.Finset.Defs
Finset.instDecidableRelSSubset : {α : Type u_1} → [DecidableEq α] → DecidableRel fun x1 x2 => x1 ⊂ x2
-- Mathlib.AlgebraicTopology.SimplicialSet.Path
SSet.stdSimplex.spineId_arrow_apply_one : ∀ (n : ℕ) (i : Fin n), ((SSet.stdSimplex.spineId n).arrow i) 1 = i.succ
-- Mathlib.Topology.MetricSpace.Pseudo.Lemmas
Real.singleton_eq_inter_Icc : ∀ (b : ℝ), {b} = ⋂ r, ⋂ (_ : r > 0), Set.Icc (b - r) (b + r)
-- Lean.Elab.PreDefinition.FixedParams
_private.Lean.Elab.PreDefinition.FixedParams.0.Lean.Elab.FixedParamPerm.forallTelescopeImpl.go : {α : Type} →
  Lean.Elab.FixedParamPerm → (Array Lean.Expr → Lean.MetaM α) → ℕ → Lean.Expr → Array Lean.Expr → Lean.MetaM α
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
/-- A filter on the set of finite subsets of a type `β`. (Used for defining infinite topological
sums and products, as limits along the given filter of partial sums / products over finsets.)  -/
SummationFilter : Type u_4 → Type u_4
-- Mathlib.Data.QPF.Univariate.Basic
QPF.Fix.mk.eq_1 : ∀ {F : Type u → Type u} [q : QPF F] (x : F (QPF.Fix F)),
  QPF.Fix.mk x = Quot.mk (⇑QPF.Wsetoid) (PFunctor.W.mk ((QPF.P F).map QPF.fixToW (QPF.repr x)))
-- Mathlib.Data.Matrix.Mul
Matrix.mul_submatrix_one : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : Fintype n] [Finite o]
  [inst_2 : NonAssocSemiring α] [inst_3 : DecidableEq o] (e₁ : n ≃ o) (e₂ : l → o) (M : Matrix m n α),
  M * Matrix.submatrix 1 (⇑e₁) e₂ = M.submatrix id (⇑e₁.symm ∘ e₂)
-- Mathlib.Order.Filter.Lift
Filter.lift_assoc : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : Filter α} {g : Set α → Filter β} {h : Set β → Filter γ},
  Monotone g → (f.lift g).lift h = f.lift fun s => (g s).lift h
-- Mathlib.Order.Disjoint
Disjoint.eq_bot_of_le : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderBot α] {a b : α}, Disjoint a b → a ≤ b → a = ⊥
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.divConst_le_card : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {A B : Finset G}, A.divConst B ≤ ↑B.card
-- Mathlib.Data.Fintype.Card
Finite.surjective_iff_bijective : ∀ {α : Type u_1} [Finite α] {f : α → α}, Function.Surjective f ↔ Function.Bijective f
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.oddKernel_def' : ∀ (a x : ℝ),
  ↑(HurwitzZeta.oddKernel (↑a) x) =
    Complex.exp (-↑Real.pi * ↑a ^ 2 * ↑x) *
      (jacobiTheta₂' (↑a * Complex.I * ↑x) (Complex.I * ↑x) / (2 * ↑Real.pi * Complex.I) +
        ↑a * jacobiTheta₂ (↑a * Complex.I * ↑x) (Complex.I * ↑x))
-- Mathlib.Data.PFunctor.Univariate.Basic
PFunctor.Idx.inhabited : (P : PFunctor.{uA, uB}) → [inst : Inhabited P.A] → [Inhabited (P.B default)] → Inhabited P.Idx
-- Init.Data.Sum.Lemmas
Sum.getRight?_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} (f : α → β) (g : γ → δ) (x : α ⊕ γ),
  (Sum.map f g x).getRight? = Option.map g x.getRight?
-- Mathlib.Algebra.Polynomial.Div
Polynomial.divByMonic_zero : ∀ {R : Type u} [inst : Ring R] (p : Polynomial R), p /ₘ 0 = 0
-- Init.Data.Range.Polymorphic.Char
Char.instLawfulUpwardEnumerableLeast? : Std.PRange.LawfulUpwardEnumerableLeast? Char
-- Lean.Data.Options
_private.Lean.Data.Options.0.Lean.Options.map : Lean.Options → Lean.NameMap Lean.DataValue
-- Mathlib.Logic.Basic
ite_eq_iff : ∀ {α : Sort u_1} {P : Prop} [inst : Decidable P] {a b c : α}, (if P then a else b) = c ↔ P ∧ a = c ∨ ¬P ∧ b = c
-- Mathlib.Algebra.Group.End
_private.Mathlib.Algebra.Group.End.0.Equiv.Perm.zpow_aux : ∀ {α : Type u_4} {p : α → Prop} {f : Equiv.Perm α}, (∀ (x : α), p (f x) ↔ p x) → ∀ {n : ℤ} (x : α), p ((f ^ n) x) ↔ p x
-- Mathlib.Algebra.Group.Subgroup.Basic
AddSubgroup.characteristic_iff_comap_le : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G},
  H.Characteristic ↔ ∀ (ϕ : G ≃+ G), AddSubgroup.comap ϕ.toAddMonoidHom H ≤ H
-- Mathlib.Data.List.Basic
List.idxOf_cons_eq : ∀ {α : Type u} [inst : BEq α] [LawfulBEq α] {a b : α} (l : List α), b = a → List.idxOf a (b :: l) = 0
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {X Y : C} (φ : X ⟶ Y),
  ((t.triangleLTLTGELT a b h).map φ).hom₁ = (t.truncLT a).map φ
-- Init.Data.List.Basic
/-- If the head of the first list is smaller than the head of the second, then the first list is
lexicographically smaller than the second list.
 -/
List.Lex.rel : ∀ {α : Type u} {r : α → α → Prop} {a₁ : α} {l₁ : List α} {a₂ : α} {l₂ : List α},
  r a₁ a₂ → List.Lex r (a₁ :: l₁) (a₂ :: l₂)
-- Mathlib.Algebra.Order.Field.Basic
div_two_sub_self : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] (a : α), a / 2 - a = -(a / 2)