mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single.congr_simp : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι)
  (x x_1 : G i), x = x_1 → RestrictedProduct.single A i x = RestrictedProduct.single A i x_1
-- Mathlib.FieldTheory.Finite.Basic
FiniteField.prod_univ_units_id_eq_neg_one : ∀ {K : Type u_1} [inst : CommRing K] [IsDomain K] [inst_2 : Fintype Kˣ], ∏ x, x = -1
-- Init.Data.List.Lemmas
List.getLast?_reverse : ∀ {α : Type u_1} {l : List α}, l.reverse.getLast? = l.head?
-- Init.Data.Sum.Basic
Sum.not_liftRel_inr_inl : ∀ {α : Type u_1} {γ : Type u_2} {r : α → γ → Prop} {β : Type u_3} {δ : Type u_4} {s : β → δ → Prop} {b : β} {c : γ},
  ¬Sum.LiftRel r s (Sum.inr b) (Sum.inl c)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Ramification
NumberField.InfinitePlace.smul_apply : ∀ {k : Type u_1} [inst : Field k] {K : Type u_2} [inst_1 : Field K] [inst_2 : Algebra k K] (σ : Gal(K/k))
  (w : NumberField.InfinitePlace K) (x : K), (σ • w) x = w (σ.symm x)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.exists_max_root : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] [inst_2 : LinearOrder R] (p : Polynomial R),
  p ≠ 0 → ∃ x₀, ∀ (x : R), p.IsRoot x → x ≤ x₀
-- Mathlib.Order.Filter.Finite
Set.Finite.eventuallyLE_iInter : ∀ {α : Type u} {l : Filter α} {ι : Type u_2} {s : Set ι},
  s.Finite → ∀ {f g : ι → Set α}, (∀ i ∈ s, f i ≤ᶠ[l] g i) → ⋂ i ∈ s, f i ≤ᶠ[l] ⋂ i ∈ s, g i
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.id_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  (A : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.CategoryStruct.id A).hom₁ = CategoryTheory.CategoryStruct.id A.obj₁
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.mem_doubleCoset : ∀ {α : Type u_2} [inst : Mul α] {s t : Set α} {a b : α},
  b ∈ DoubleCoset.doubleCoset a s t ↔ ∃ x ∈ s, ∃ y ∈ t, b = x * a * y
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.map_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n : ℤ} {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_1, u_2} D]
  [inst_3 : CategoryTheory.Preadditive D] (z : CochainComplex.HomComplex.Cochain K L n) (Φ : CategoryTheory.Functor C D)
  [inst_4 : Φ.Additive], (-z).map Φ = -z.map Φ
-- Init.Core
instSubsingletonSquash : ∀ {α : Sort u_1}, Subsingleton (Squash α)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.all_eq_all_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String}, s.all pat = s.toSlice.all pat
-- Mathlib.Data.Multiset.Sections
Multiset.sections_zero : ∀ {α : Type u_1}, Multiset.Sections 0 = {0}
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.getHSMulIntInst : Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM Lean.Expr
-- Init.Omega.IntList
/-- Apply "balanced mod" to each entry in an `IntList`.  -/
Lean.Omega.IntList.bmod : Lean.Omega.IntList → ℕ → Lean.Omega.IntList
-- Init.Data.Sum.Lemmas
Sum.getRight?.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (b : β), (Sum.inr b).getRight? = some b
-- Mathlib.Algebra.Lie.TensorProduct
/-- A pair of Lie module morphisms `f : M → P` and `g : N → Q`, induce a Lie module morphism:
`M ⊗ N → P ⊗ Q`.  -/
TensorProduct.LieModule.map : {R : Type u} →
  [inst : CommRing R] →
    {L : Type v} →
      {M : Type w} →
        {N : Type w₁} →
          {P : Type w₂} →
            {Q : Type w₃} →
              [inst_1 : LieRing L] →
                [inst_2 : LieAlgebra R L] →
                  [inst_3 : AddCommGroup M] →
                    [inst_4 : Module R M] →
                      [inst_5 : LieRingModule L M] →
                        [inst_6 : LieModule R L M] →
                          [inst_7 : AddCommGroup N] →
                            [inst_8 : Module R N] →
                              [inst_9 : LieRingModule L N] →
                                [inst_10 : LieModule R L N] →
                                  [inst_11 : AddCommGroup P] →
                                    [inst_12 : Module R P] →
                                      [inst_13 : LieRingModule L P] →
                                        [inst_14 : LieModule R L P] →
                                          [inst_15 : AddCommGroup Q] →
                                            [inst_16 : Module R Q] →
                                              [inst_17 : LieRingModule L Q] →
                                                [inst_18 : LieModule R L Q] →
                                                  (M →ₗ⁅R,L⁆ P) →
                                                    (N →ₗ⁅R,L⁆ Q) → TensorProduct R M N →ₗ⁅R,L⁆ TensorProduct R P Q
-- Mathlib.Data.ENat.Basic
ENat.lift_natCast : ∀ (n : ℕ), (↑n).lift ⋯ = n
-- Mathlib.Geometry.Euclidean.Angle.Oriented.RightAngle
/-- The sine of an angle in a right-angled triangle multiplied by the hypotenuse equals the
opposite side.  -/
EuclideanGeometry.sin_oangle_left_mul_dist_of_oangle_eq_pi_div_two : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] [hd2 : Fact (Module.finrank ℝ V = 2)] [inst_4 : Module.Oriented ℝ V (Fin 2)]
  {p₁ p₂ p₃ : P},
  EuclideanGeometry.oangle p₁ p₂ p₃ = ↑(Real.pi / 2) → (EuclideanGeometry.oangle p₃ p₁ p₂).sin * dist p₁ p₃ = dist p₃ p₂
-- Lean.Meta.ACLt
_private.Lean.Meta.ACLt.0.Lean.Meta.ACLt.main.allChildrenLt : Lean.Meta.ACLt.ReduceMode → Lean.Expr → Lean.Expr → Lean.MetaM Bool
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.or_false : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, P ∨ ⌜False⌝ ⊣⊢ₛ P
-- Init.Control.Lawful.Instances
instLawfulFunctorOption : LawfulFunctor Option
-- Mathlib.CategoryTheory.Retract
/-- a retract determines a split epimorphism.  -/
CategoryTheory.Retract.splitEpi : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → {X Y : C} → (h : CategoryTheory.Retract X Y) → CategoryTheory.SplitEpi h.r
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.leftKanExtensionCompIsoOfPreserves_hom_fac_app : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) [inst_4 : G.PreservesLeftKanExtension F L] [inst_5 : L.HasLeftKanExtension F]
  (a : A),
  CategoryTheory.CategoryStruct.comp (G.map ((L.leftKanExtensionUnit F).app a))
      ((G.leftKanExtensionCompIsoOfPreserves F L).hom.app (L.obj a)) =
    (L.leftKanExtensionUnit (F.comp G)).app a
-- Mathlib.Topology.Algebra.Group.Basic
/-- **Alias** of the forward direction of `continuousOn_neg_iff`. -/
ContinuousOn.of_neg : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : InvolutiveNeg G] [ContinuousNeg G]
  [inst_3 : TopologicalSpace α] {f : α → G} {s : Set α}, ContinuousOn (-f) s → ContinuousOn f s
-- Lean.Meta.Hint
Lean.Meta.Hint.DiffGranularity.word.sizeOf_spec : sizeOf Lean.Meta.Hint.DiffGranularity.word = 1
-- Mathlib.Topology.Category.TopCat.OpenNhds
TopologicalSpace.OpenNhds.apply_mk : ∀ {X : TopCat} {x : ↑X} {U V : TopologicalSpace.OpenNhds x} (f : U ⟶ V) (y : ↑X) (hy : y ∈ ↑U), f ⟨y, hy⟩ = ⟨y, ⋯⟩
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- `padicValRat` defines the valuation of a rational `q` to be the valuation of `q.num` minus the
valuation of `q.den`. If `q = 0` or `p = 1`, then `padicValRat p q` defaults to `0`.  -/
padicValRat : ℕ → ℚ → ℤ
-- Mathlib.Data.Part
Part.mul_mem_mul : ∀ {α : Type u_1} [inst : Mul α] (a b : Part α) (ma mb : α), ma ∈ a → mb ∈ b → ma * mb ∈ a * b
-- Lean.Meta.Basic
Lean.Meta.getPPContext : Lean.MetaM Lean.PPContext
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.preservesFiniteLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  CategoryTheory.Limits.PreservesFiniteLimits L
-- Mathlib.Order.SuccPred.Tree
/-- The type should have a predecessor for every element, its parent.  -/
RootedTree.predOrder : (self : RootedTree) → PredOrder ↑self
-- Mathlib.Data.ZMod.Basic
ZMod.castHom_injective : ∀ {n : ℕ} (R : Type u_1) [inst : Ring R] [inst_1 : CharP R n], Function.Injective ⇑(ZMod.castHom ⋯ R)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.smul_eval : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (x : σ → R) (p : MvPolynomial σ R) (s : R),
  (MvPolynomial.eval x) (s • p) = s * (MvPolynomial.eval x) p
-- Mathlib.RingTheory.Ideal.Oka
/-- A variant of `forall_of_forall_prime` with a different spelling of the condition `hmax`.  -/
Ideal.IsOka.forall_of_forall_prime' : ∀ {R : Type u_1} [inst : CommSemiring R] {P : Ideal R → Prop},
  Ideal.IsOka P →
    (∀ C ⊆ {I | ¬P I}, IsChain (fun x1 x2 => x1 ≤ x2) C → ∀ x ∈ C, P (sSup C) → ∃ I ∈ C, P I) →
      (∀ (I : Ideal R), I.IsPrime → P I) → ∀ (I : Ideal R), P I
-- Mathlib.Algebra.Order.Archimedean.Basic
existsUnique_div_zpow_mem_Ico : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G},
  1 < a → ∀ (b c : G), ∃! m, b / a ^ m ∈ Set.Ico c (c * a)
-- Mathlib.Analysis.Normed.Algebra.Spectrum
/-- If `S` is a closed subalgebra of a Banach algebra `A`, then for any `x : S`, the spectrum of `x`
is the spectrum of `↑x : A` along with the connected components of the complement of the spectrum of
`↑x : A` which contain an element of the spectrum of `x : S`.  -/
Subalgebra.spectrum_sUnion_connectedComponentIn : ∀ {𝕜 : Type u_3} {A : Type u_4} {SA : Type u_5} [inst : NormedRing A] [CompleteSpace A] [inst_2 : SetLike SA A]
  [inst_3 : SubringClass SA A] [inst_4 : NormedField 𝕜] [inst_5 : NormedAlgebra 𝕜 A] [instSMulMem : SMulMemClass SA 𝕜 A]
  (S : SA) [hS : IsClosed ↑S] (x : ↥S),
  spectrum 𝕜 x = spectrum 𝕜 ↑x ∪ ⋃ z ∈ spectrum 𝕜 x \ spectrum 𝕜 ↑x, connectedComponentIn (spectrum 𝕜 ↑x)ᶜ z
-- Mathlib.Data.Int.Init
Int.natCast_pred_of_pos : ∀ {n : ℕ}, 0 < n → ↑(n - 1) = ↑n - 1
-- Lean.Environment
/-- `ConstantInfo` variant that allows for asynchronous filling of components via tasks.  -/
Lean.AsyncConstantInfo : Type
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] [inst_2 : BEq α] [Std.LawfulBEqCmp cmp] {l : List ((a : α) × β a)} {k : α}
  [inst_4 : Inhabited (β k)], (List.map Sigma.fst l).contains k = false → (t.insertMany l).get! k = t.get! k
-- Mathlib.Algebra.Homology.Embedding.TruncLE
/-- `(K.truncLE'ToRestriction e).f i` is an isomorphism when `¬ e.BoundaryLE i`.  -/
HomologicalComplex.isIso_truncLE'ToRestriction : ∀ {ι : 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.HasZeroMorphisms C]
  (K : HomologicalComplex C c') (e : c.Embedding c') [inst_2 : e.IsTruncLE] [inst_3 : ∀ (i' : ι'), K.HasHomology i']
  (i : ι), ¬e.BoundaryLE i → CategoryTheory.IsIso ((K.truncLE'ToRestriction e).f i)
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.isRightRegular_iff_nonsingular : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n R}
  [IsCancelAdd R], IsRightRegular A ↔ A.Nonsingular
-- Mathlib.Topology.UnitInterval
iccHomeoI_symm_apply_coe : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [inst_4 : IsTopologicalRing 𝕜] (a b : 𝕜) (h : a < b) (x : ↑(Set.Icc 0 1)),
  ↑((iccHomeoI a b h).symm x) = (b - a) * ↑x + a
-- Mathlib.CategoryTheory.DifferentialObject
CategoryTheory.DifferentialObject.isoApp_refl : ∀ {S : Type u_1} [inst : AddMonoidWithOne S] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.HasShift C S]
  (X : CategoryTheory.DifferentialObject S C),
  CategoryTheory.DifferentialObject.isoApp (CategoryTheory.Iso.refl X) = CategoryTheory.Iso.refl X.obj
-- Mathlib.RingTheory.Polynomial.Basic
/-- For every polynomial `p` in the span of a set `s : Set R[X]`, there exists a polynomial of
`p' ∈ s` with higher degree. See also `Polynomial.exists_degree_le_of_mem_span_of_finite`.  -/
Polynomial.exists_degree_le_of_mem_span : ∀ {R : Type u} [inst : Semiring R] {s : Set (Polynomial R)} {p : Polynomial R},
  s.Nonempty → p ∈ Submodule.span R s → ∃ p' ∈ s, p.degree ≤ p'.degree
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_mul_add_lt_opow_mul : ∀ {b u w x v : Ordinal.{u_1}}, w < b ^ u → v < x → b ^ u * v + w < b ^ u * x
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioc_atTop_atTop : ∀ {α : Type u_1} [inst : Preorder α], Filter.TendstoIxxClass Set.Ioc Filter.atTop Filter.atTop
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length_take_le : ∀ {α : Type u} {s : Stream'.Seq α} {n : ℕ}, (Stream'.Seq.take n s).length ≤ n
-- Mathlib.Algebra.Polynomial.Degree.TrailingDegree
Polynomial.natTrailingDegree_monomial_le : ∀ {R : Type u} {a : R} {n : ℕ} [inst : Semiring R], ((Polynomial.monomial n) a).natTrailingDegree ≤ n
-- Std.Data.DTreeMap.Raw.Basic
/-- Checks if a mapping for the given key exists and returns the key-value pair if it does, otherwise panics.
The key in the returned pair will be `BEq` to the input `a`.
 -/
Std.DTreeMap.Raw.getEntry! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Inhabited ((a : α) × β a)] → Std.DTreeMap.Raw α β cmp → α → (a : α) × β a
-- Mathlib.RingTheory.AdicCompletion.Basic
AdicCompletion.range_eval : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) (M : Type u_4) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (n : ℕ), (AdicCompletion.eval I M n).range = ⊤
-- Mathlib.Algebra.Order.Quantale
/-- Addition is distributive over join in a quantale  -/
IsAddQuantale.sSup_add_distrib : ∀ {α : Type u_1} {inst : AddSemigroup α} {inst_1 : CompleteLattice α} [self : IsAddQuantale α] (s : Set α) (y : α),
  sSup s + y = ⨆ x ∈ s, x + y
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.noConfusionType : Sort v✝ → Std.Tactic.BVDecide.BVBinOp → Std.Tactic.BVDecide.BVBinOp → Sort v✝
-- Mathlib.CategoryTheory.Abelian.Projective.Ext
CategoryTheory.ProjectiveResolution.extMk_eq_zero_iff : ∀ {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)
  (p : ℕ), p + 1 = n → (R.extMk f m hm hf = 0 ↔ ∃ g, CategoryTheory.CategoryStruct.comp (R.complex.d n p) g = f)
-- Mathlib.Algebra.Homology.SingleHomology
HomologicalComplex.singleObjCyclesSelfIso_inv_iCycles_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {ι : Type u_1} [inst_3 : DecidableEq ι] (c : ComplexShape ι) (j : ι)
  (A : C) {Z : C} (h : ((HomologicalComplex.single C c j).obj A).X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjCyclesSelfIso c j A).inv
      (CategoryTheory.CategoryStruct.comp (((HomologicalComplex.single C c j).obj A).iCycles j) h) =
    CategoryTheory.CategoryStruct.comp (HomologicalComplex.singleObjXSelf c j A).inv h
-- Mathlib.Topology.Homotopy.Path
Path.Homotopic.Quotient.mk_symm : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} (P : Path x₀ x₁),
  Path.Homotopic.Quotient.mk P.symm = (Path.Homotopic.Quotient.mk P).symm
-- Mathlib.LinearAlgebra.Projectivization.Action
Matrix.ProjectiveSpecialLinearGroup.toPermHom_injective : ∀ {K : Type u_1} [inst : Field K] {ι : Type u_3} [inst_1 : Fintype ι] [inst_2 : DecidableEq ι],
  Function.Injective ⇑Projectivization.PSLAction.toPermHom
-- Init.Data.Vector.Find
Vector.find?_map : ∀ {β α : Type} {n : ℕ} {p : α → Bool} {f : β → α} {xs : Vector β n},
  Vector.find? p (Vector.map f xs) = Option.map f (Vector.find? (p ∘ f) xs)
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.pOpcycles_extendOpcyclesIso_hom_assoc : ∀ {ι : 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.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {j : ι} {j' : ι'}
  (hj' : e.f j = j') [inst_3 : K.HasHomology j] [inst_4 : (K.extend e).HasHomology j'] {Z : C} (h : K.opcycles j ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((K.extend e).pOpcycles j')
      (CategoryTheory.CategoryStruct.comp (K.extendOpcyclesIso e hj').hom h) =
    CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom (CategoryTheory.CategoryStruct.comp (K.pOpcycles j) h)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.diff!_congr : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ m₃ m₄ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF → m₂.WF → m₃.WF → m₄.WF → m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁.diff! m₂).Equiv (m₃.diff! m₄)
-- Mathlib.Data.Num.Basic
Num.instLT : LT Num
-- Mathlib.GroupTheory.GroupAction.Pointwise
Set.MapsTo.smul_set : ∀ {M : Type u_1} {α : Type u_2} {β : Type u_3} {F : Type u_4} [inst : SMul M α] [inst_1 : SMul M β]
  [inst_2 : FunLike F α β] [MulActionHomClass F M α β] {f : F} {s : Set α} {t : Set β},
  Set.MapsTo (⇑f) s t → ∀ (c : M), Set.MapsTo (⇑f) (c • s) (c • t)
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.opow_add_one : ∀ (a b : Ordinal.{u_1}), a ^ (b + 1) = a ^ b * a
-- Mathlib.Algebra.Category.ModuleCat.Presheaf.Submodule
/-- A family of submodules `N X` of `M.obj X`, for a presheaf of modules `M`, stable
under the restriction maps of `M`. This defines a subobject of `M` in `PresheafOfModules R`.  -/
PresheafOfModules.Submodule : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {R : CategoryTheory.Functor Cᵒᵖ RingCat} → PresheafOfModules R → Type (max u₁ v)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_single : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : DecidableEq n] [inst_1 : DecidableEq m] [inst_2 : AddMonoid α]
  [inst_3 : StarAddMonoid α] (i : m) (j : n) (a : α), (Matrix.single i j a).conjTranspose = Matrix.single j i (star a)
-- Lean.Meta.Tactic.Simp.Arith.Nat.Basic
Lean.Meta.Simp.Arith.Nat.ToLinear.addAsVar : Lean.Expr → Lean.Meta.Simp.Arith.Nat.ToLinear.M Lean.Meta.Simp.Arith.Nat.LinearExpr
-- Mathlib.Data.W.Cardinal
/-- `#(WType β)` is the least cardinal `κ` such that `sum (fun a : α ↦ κ ^ #(β a)) ≤ κ`  -/
WType.cardinalMk_le_of_le' : ∀ {α : Type u} {β : α → Type v} {κ : Cardinal.{max u v}},
  (Cardinal.sum fun a => κ ^ Cardinal.lift.{u, v} (Cardinal.mk (β a))) ≤ κ → Cardinal.mk (WType β) ≤ κ
-- Mathlib.Topology.Sets.Closeds
TopologicalSpace.Closeds.mem_singleton : ∀ {α : Type u_2} [inst : TopologicalSpace α] [inst_1 : T1Space α] {a b : α}, a ∈ {b} ↔ a = b
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitDiagInfo.lctx : Lean.Meta.Grind.SplitDiagInfo → Lean.LocalContext
-- Mathlib.Tactic.CrossRefAttribute
/-- The syntax for a "stacks" database identifier in a `@[stacks]` attribute.  -/
Mathlib.CrossRef.stacksTagDBStacks : Lean.ParserDescr
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.eval_assoc : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {τ : Type u_2} (f : σ → MvPolynomial τ R) (g : τ → R)
  (p : MvPolynomial σ R),
  (MvPolynomial.eval (⇑(MvPolynomial.eval g) ∘ f)) p = (MvPolynomial.eval g) (MvPolynomial.eval₂ MvPolynomial.C f p)
-- Mathlib.LinearAlgebra.QuadraticForm.TensorProduct.Isometries
QuadraticForm.tensorRId_apply : ∀ {R : Type uR} {M₁ : Type uM₁} [inst : CommRing R] [inst_1 : AddCommGroup M₁] [inst_2 : Module R M₁]
  [inst_3 : Invertible 2] (Q₁ : QuadraticForm R M₁) (x : TensorProduct R M₁ R),
  Q₁.tensorRId x = (TensorProduct.rid R M₁) x
-- Mathlib.Geometry.Euclidean.Inversion.Basic
/-- Inversion in a sphere in an affine space. This map sends each point `x` to the point `y` such
that `y -ᵥ c = (R / dist x c) ^ 2 • (x -ᵥ c)`, where `c` and `R` are the center and the radius the
sphere.  -/
EuclideanGeometry.inversion : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [InnerProductSpace ℝ V] → [inst_2 : MetricSpace P] → [NormedAddTorsor V P] → P → ℝ → P → P
-- Mathlib.Data.ZMod.Basic
/-- `unitOfCoprime` makes an element of `(ZMod n)ˣ` given
a natural number `x` and a proof that `x` is coprime to `n`  -/
ZMod.unitOfCoprime : {n : ℕ} → (x : ℕ) → x.Coprime n → (ZMod n)ˣ
-- Mathlib.Algebra.Group.Action.Faithful
FaithfulSMul.mk : ∀ {M : Type u_4} {α : Type u_5} [inst : SMul M α],
  (∀ {m₁ m₂ : M}, (∀ (a : α), m₁ • a = m₂ • a) → m₁ = m₂) → FaithfulSMul M α
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.minD_eq_headD_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {fallback : α},
  t.minD fallback = t.toList.headD fallback
-- Mathlib.Combinatorics.Additive.Dissociation
addDissociated_empty : ∀ {α : Type u_1} [inst : AddCommGroup α], AddDissociated ∅
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_add : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (x y : M →₀ R),
  AddMonoidAlgebra.ofCoeff (x + y) = AddMonoidAlgebra.ofCoeff x + AddMonoidAlgebra.ofCoeff y
-- Aesop.Tree.Data
Aesop.GoalOrigin.copied : Aesop.GoalId → Aesop.GoalId → Aesop.GoalOrigin
-- Mathlib.Order.SuccPred.Relation
/-- For `m ≤ n`, `(n, m)` is in the reflexive-transitive closure of `~` if `succ i ~ i`
for all `i` between `n` and `m`.  -/
reflTransGen_of_succ_of_ge : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : SuccOrder α] [IsSuccArchimedean α] (r : α → α → Prop) {n m : α},
  (∀ i ∈ Set.Ico m n, r (Order.succ i) i) → m ≤ n → Relation.ReflTransGen r n m
-- Mathlib.Combinatorics.SimpleGraph.Star
SimpleGraph.isUniversal_starGraph_self : ∀ {V : Type u_1} {r : V}, (SimpleGraph.starGraph r).IsUniversal r
-- Mathlib.Topology.Order
isClosed_iSup_iff : ∀ {α : Type u} {ι : Sort v} {t : ι → TopologicalSpace α} {s : Set α}, IsClosed s ↔ ∀ (i : ι), IsClosed s
-- Init.Data.List.Attach
List.reverse_pmap : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : List α} (H : ∀ a ∈ xs, P a),
  (List.pmap f xs H).reverse = List.pmap f xs.reverse ⋯
-- Mathlib.Analysis.Normed.Group.Basic
norm_zero : ∀ {E : Type u_5} [inst : SeminormedAddGroup E], ‖0‖ = 0
-- Mathlib.Algebra.Regular.Defs
IsRightRegular.eq_1 : ∀ {R : Type u_1} [inst : Mul R] (c : R), IsRightRegular c = Function.Injective fun x => x * c
-- Mathlib.NumberTheory.PrimeCounting
Nat.surjective_primeCounting' : Function.Surjective Nat.primeCounting'
-- Mathlib.Algebra.Polynomial.Splits
/-- If `f` is a monic polynomial that splits, then `f.nextCoeff` equals the negative of the sum
of the roots.  -/
Polynomial.Splits.nextCoeff_eq_neg_sum_roots_of_monic : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R} [inst_1 : IsDomain R],
  f.Splits → f.Monic → f.nextCoeff = -f.roots.sum
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
/-- In an ordered commutative monoid, if each factor `f i` of one nontrivial finite product is
strictly less than the corresponding factor `g i` of another nontrivial finite product, then
`s.prod f < s.prod g`.  -/
Finset.prod_lt_prod_of_nonempty' : ∀ {ι : Type u_1} {M : Type u_4} [inst : CommMonoid M] [inst_1 : Preorder M] [IsOrderedCancelMonoid M] {f g : ι → M}
  {s : Finset ι} [MulLeftStrictMono M], s.Nonempty → (∀ i ∈ s, f i < g i) → ∏ i ∈ s, f i < ∏ i ∈ s, g i