mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
PiTensorProduct.lift_reindex_symm : ∀ {ι : Type u_1} {ι₂ : Type u_2} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7}
  [inst_1 : (i : ι) → AddCommMonoid (s i)] [inst_2 : (i : ι) → Module R (s i)] {E : Type u_9} [inst_3 : AddCommMonoid E]
  [inst_4 : Module R E] (e : ι ≃ ι₂) (φ : MultilinearMap R s E) (x : PiTensorProduct R fun i => s (e.symm i)),
  (PiTensorProduct.lift φ) ((PiTensorProduct.reindex R s e).symm x) =
    (PiTensorProduct.lift ((MultilinearMap.domDomCongrLinearEquiv' R R s E e) φ)) x
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
/-- `SL(2, ℝ)` acts on the upper half plane as an isometry.  -/
UpperHalfPlane.instIsIsometricSMulSpecialLinearGroupFinOfNatNatReal : IsIsometricSMul (Matrix.SpecialLinearGroup (Fin 2) ℝ) UpperHalfPlane
-- Mathlib.RingTheory.Smooth.Basic
Algebra.TensorProduct.productLeftAlgHom.congr_simp : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : CommSemiring C]
  [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C] (f f_1 : A →ₐ[S] C),
  f = f_1 →
    ∀ (g g_1 : B →ₐ[R] C),
      g = g_1 → Algebra.TensorProduct.productLeftAlgHom f g = Algebra.TensorProduct.productLeftAlgHom f_1 g_1
-- Mathlib.Order.Fin.Basic
Fin.natAdd_le_natAdd_iff : ∀ {n : ℕ} (m : ℕ) {i j : Fin n}, Fin.natAdd m i ≤ Fin.natAdd m j ↔ i ≤ j
-- Lean.Meta.Sym.SymM
/-- Runs an `AlphaShareCommonM` action over the `SymM` hash-consing state.
On a check violation, returns the cache accumulated before the failure as `.error`;
the terms hash-consed before the failure are kept in the state, since they
individually satisfy the invariants.
 -/
Lean.Meta.Sym.runShareCommonM : {α : Type} →
  Lean.Meta.Sym.AlphaShareCommonM α →
    Lean.Meta.Sym.AlphaShareCommon.Context → Lean.Meta.Sym.SymM (Except Lean.Meta.Sym.AlphaShareCommon.Cache α)
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.instAdd : {ι : Type u} → {β : ι → Type v} → [inst : (i : ι) → AddZeroClass (β i)] → Add (Π₀ (i : ι), β i)
-- Mathlib.AlgebraicTopology.ModelCategory.FibrantObjectHomotopy
/-- This is a trivial cofibration `X ⟶ resolutionObj X` where
`resolutionObj X` is a choice of a fibrant resolution of `X`.  -/
HomotopicalAlgebra.FibrantObject.HoCat.iResolutionObj : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : HomotopicalAlgebra.ModelCategory C] → (X : C) → X ⟶ HomotopicalAlgebra.FibrantObject.HoCat.resolutionObj X
-- Mathlib.Data.Multiset.Range
Multiset.self_mem_range_succ : ∀ (n : ℕ), n ∈ Multiset.range (n + 1)
-- Mathlib.Topology.Algebra.StarSubalgebra
/-- The `StarSubalgebra.inclusion` of a star subalgebra is an embedding.  -/
StarSubalgebra.isEmbedding_inclusion : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : StarRing A] [inst_6 : StarModule R A]
  {S₁ S₂ : StarSubalgebra R A} (h : S₁ ≤ S₂), Topology.IsEmbedding ⇑(StarSubalgebra.inclusion h)
-- Lean.Meta.WHNF
Lean.Meta.ReduceMatcherResult.notMatcher : Lean.Meta.ReduceMatcherResult
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.ext : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] {f g : ↥(lp E p)},
  ↑f = ↑g → f = g
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.add_assoc_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X : C}
  [inst_2 : CategoryTheory.AddMonObj M] (f : X ⟶ M) {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X M M).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.AddMonObj.add)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom f (CategoryTheory.CategoryStruct.id M))
          CategoryTheory.AddMonObj.add)
        (CategoryTheory.CategoryStruct.id M))
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)
-- Std.Async.Signal
/-- Set up a `Signal.Waiter` that waits for the specified `signum`.
This function only initializes but does not yet start listening for the signal.
 -/
Std.Async.Signal.Waiter.mk : Std.Async.Signal → Bool → IO Std.Async.Signal.Waiter
-- Mathlib.Data.Finset.Prod
Finset.product_eq_empty : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, s ×ˢ t = ∅ ↔ s = ∅ ∨ t = ∅
-- Mathlib.Algebra.Order.Group.PosPart
negPart_lt : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : AddGroup α] {a b : α} [AddLeftMono α] [AddRightMono α],
  a⁻ < b ↔ -b < a ∧ 0 < b
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_comp_ε_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (self : X.ExtraDegeneracy) {Z : C} (h : X.right ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.s'
      (CategoryTheory.CategoryStruct.comp (X.hom.app (Opposite.op { len := 0 })) h) =
    h
-- Mathlib.Algebra.Homology.BifunctorFlip
HomologicalComplex.ι_mapBifunctorFlipIso_hom_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : TotalComplexShape c₂ c₁ c] [inst_10 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_11 : DecidableEq J]
  [inst_12 : K₁.HasMapBifunctor K₂ F c] (i₁ : I₁) (i₂ : I₂) (j : J) (hj : c₂.π c₁ c (i₂, i₁) = j) {Z : D}
  (h : (K₁.mapBifunctor K₂ F c).X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K₂.ιMapBifunctor K₁ F.flip c i₂ i₁ j hj)
      (CategoryTheory.CategoryStruct.comp ((K₁.mapBifunctorFlipIso K₂ F c).hom.f j) h) =
    CategoryTheory.CategoryStruct.comp (c₁.σ c₂ c i₁ i₂ • K₁.ιMapBifunctor K₂ F c i₁ i₂ j ⋯) h
-- Mathlib.Algebra.Module.Equiv.Defs
LinearEquiv.left_inv : ∀ {R : Type u_14} {S : Type u_15} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {σ' : S →+* R}
  [inst_2 : RingHomInvPair σ σ'] [inst_3 : RingHomInvPair σ' σ] {M : Type u_16} {M₂ : Type u_17}
  [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid M₂] [inst_6 : Module R M] [inst_7 : Module S M₂]
  (self : M ≃ₛₗ[σ] M₂), Function.LeftInverse self.invFun (↑self).toFun
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.quasiCompact_isStableUnderComposition : CategoryTheory.MorphismProperty.IsStableUnderComposition @AlgebraicGeometry.QuasiCompact
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_im : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), a.im.imJ = a.imJ
-- Mathlib.Data.Finset.Slice
Set.Sized.eq_1 : ∀ {α : Type u_1} (r : ℕ) (A : Set (Finset α)), Set.Sized r A = ∀ ⦃x : Finset α⦄, x ∈ A → x.card = r
-- Mathlib.Order.Lattice
right_eq_inf : ∀ {α : Type u} [inst : SemilatticeInf α] {a b : α}, b = a ⊓ b ↔ b ≤ a
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Represents
SimpleGraph.ConnectedComponent.Represents.disjoint_supp_of_notMem : ∀ {V : Type u} {G : SimpleGraph V} {C : Set G.ConnectedComponent} {s : Set V} {c : G.ConnectedComponent},
  SimpleGraph.ConnectedComponent.Represents s C → c ∉ C → Disjoint s c.supp
-- Mathlib.LinearAlgebra.Dimension.OrzechProperty
/-- A family of `finrank R M` vectors forms a basis if they span the whole space,
provided `R` satisfies the Orzech property.  -/
basisOfTopLeSpanOfCardEqFinrank : {R : Type u_1} →
  {M : Type u_2} →
    [inst : Semiring R] →
      [OrzechProperty R] →
        [inst_2 : AddCommMonoid M] →
          [inst_3 : Module R M] →
            {ι : Type u_3} →
              [inst_4 : Fintype ι] →
                (b : ι → M) →
                  ⊤ ≤ Submodule.span R (Set.range b) → Fintype.card ι = Module.finrank R M → Module.Basis ι R M
-- Mathlib.Algebra.Star.Unitary
/-- **Alias** of the reverse direction of `IsUnit.mem_unitary_iff_mul_star_self`. -/
IsUnit.mem_unitary_of_mul_star_self : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {u : R}, IsUnit u → u * star u = 1 → u ∈ unitary R
-- Mathlib.Algebra.Group.Action.Defs
smul_one_mul : ∀ {M : Type u_9} {N : Type u_10} [inst : MulOneClass N] [inst_1 : SMul M N] [IsScalarTower M N N] (x : M) (y : N),
  x • 1 * y = x • y
-- Mathlib.Order.CompleteLattice.Basic
le_iInf_const : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] {a : α}, a ≤ ⨅ x, a
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplices
SSet.S.existsUnique_n : ∀ {X : SSet} (x : X.S), ∃! y, y.subcomplex = x.subcomplex
-- Mathlib.RepresentationTheory.Continuous.TopRep
TopRep.hom_comp : ∀ {k : Type u} {G : Type v} [inst : TopologicalSpace k] [inst_1 : Ring k] [inst_2 : Monoid G] (A B C : TopRep k G)
  (f : A ⟶ B) (g : B ⟶ C),
  TopRep.Hom.hom (CategoryTheory.CategoryStruct.comp f g) = (TopRep.Hom.hom g).comp (TopRep.Hom.hom f)
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.ModEq.zsmul_add : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b : G} (z : ℤ), a ≡ b [PMOD p] → z • p + a ≡ b [PMOD p]
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit
_private.Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesColimit.0.SSet.isColimitCoconeN.fac : ∀ {X : SSet} (s : CategoryTheory.Limits.Cocone X.functorN) (x : X.N),
  CategoryTheory.CategoryStruct.comp x.subcomplex.ι (SSet.isColimitCoconeN.desc✝ s) = s.ι.app x
-- Lean.Meta.NatInstTesters
Lean.Meta.DefEq.isInstMulNat : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.BigOperators.Group.Finset.Powerset
/-- A product over `Finset.powersetCard` which only depends on the size of the sets is constant.  -/
Finset.prod_powersetCard : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid β] (n : ℕ) (s : Finset α) (f : ℕ → β),
  ∏ t ∈ Finset.powersetCard n s, f t.card = f n ^ s.card.choose n
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get?_eq_none : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {a : α}, a ∉ t → t.get? a = none
-- Mathlib.Algebra.Group.Even
Additive.instDecidablePredEven : {α : Type u_2} → [inst : Mul α] → [DecidablePred IsSquare] → DecidablePred Even
-- Mathlib.RingTheory.PowerSeries.Ideal
PowerSeries.spanFinrank_le_spanFinrank_map_constantCoeff_add_one_of_X_mem : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal (PowerSeries R)},
  PowerSeries.X ∈ I → Submodule.spanFinrank I ≤ Submodule.spanFinrank (Ideal.map PowerSeries.constantCoeff I) + 1
-- Mathlib.Combinatorics.SimpleGraph.Ends.Properties
/-- A locally finite preconnected infinite graph has at least one end.  -/
SimpleGraph.nonempty_ends_of_infinite : ∀ {V : Type} (G : SimpleGraph V) [G.LocallyFinite] [Fact G.Preconnected] [Infinite V], G.end.Nonempty
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τl : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  (self : CategoryTheory.Bicategory.Adj.Hom₂ α β),
  (CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) self.τl = self.τr
-- Mathlib.AlgebraicTopology.SimplicialSet.ProdStdSimplex
SSet.prodStdSimplex.objEquiv_naturality : ∀ {p q m n : ℕ} (f : { len := m } ⟶ { len := n })
  (z :
    (CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
          (SSet.stdSimplex.obj { len := q })).obj
      (Opposite.op { len := n })),
  (SSet.prodStdSimplex.objEquiv z).comp (SimplexCategory.Hom.toOrderHom f) =
    SSet.prodStdSimplex.objEquiv
      ((CategoryTheory.ConcreteCategory.hom
          ((CategoryTheory.MonoidalCategoryStruct.tensorObj (SSet.stdSimplex.obj { len := p })
                (SSet.stdSimplex.obj { len := q })).map
            f.op))
        z)
-- Init.Data.UInt.Lemmas
UInt32.toBitVec_ofNatTruncate_of_le : ∀ {n : ℕ},
  UInt32.size ≤ n → (UInt32.ofNatClamp n).toBitVec = (UInt32.size - 1)#'UInt32.toBitVec_ofNatClamp_of_le._proof_1
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.tsum_one : ∀ {α : Type u_4}, ∑' (x : α), 1 = ↑(ENat.card α)
-- Mathlib.Logic.Denumerable
_private.Mathlib.Logic.Denumerable.0.Encodable.decodeSum.match_1.eq_2 : ∀ (motive : Bool → ℕ → Sort u_1) (x : Bool) (m : ℕ) (h_1 : (m : ℕ) → motive false m)
  (h_2 : (x : Bool) → (m : ℕ) → motive x m),
  (x = false → False) →
    (match x, m with
      | false, m => h_1 m
      | x, m => h_2 x m) =
      h_2 x m
-- Mathlib.Topology.Covering.Basic
IsEvenlyCovered.toTrivialization.congr_simp : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X} {I : Type u_3}
  [inst_2 : TopologicalSpace I] {x : X} [inst_3 : Nonempty I] (h : IsEvenlyCovered f x I),
  h.toTrivialization = h.toTrivialization
-- Init.Data.String.Lemmas.Pattern.String.Basic
String.Slice.Pattern.Model.ForwardStringSearcher.isLongestRevMatch_iff_isLongestRevMatch_toSlice : ∀ {pat : String} {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsLongestRevMatch pat pos ↔ String.Slice.Pattern.Model.IsLongestRevMatch pat.toSlice pos
-- Mathlib.Topology.UniformSpace.OfCompactT2
/-- The unique uniform structure inducing a given compact topological structure.  -/
uniformSpaceOfCompactR1 : {γ : Type u_1} → [inst : TopologicalSpace γ] → [CompactSpace γ] → [R1Space γ] → UniformSpace γ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKeyD_diff_of_not_mem_left : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k fallback : α}, k ∉ t₁ → (t₁ \ t₂).getKeyD k fallback = fallback
-- Mathlib.Topology.Category.Profinite.Nobeling.ZeroLimit
Profinite.NobelingProof.GoodProducts.linearIndependent_iff_union_smaller : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] [inst_1 : WellFoundedLT I] {o : Ordinal.{u}},
  Order.IsSuccLimit o →
    Profinite.NobelingProof.contained C o →
      (LinearIndependent ℤ (Profinite.NobelingProof.GoodProducts.eval C) ↔
        LinearIndependent ℤ fun (p : ↑(⋃ e, Profinite.NobelingProof.GoodProducts.smaller C ↑e)) => ↑p)
-- Mathlib.CategoryTheory.Elements
/-- The type of objects for the category of elements of a functor `F : C ⥤ Type`
is a pair `(X : C, x : F.obj X)`.
 -/
CategoryTheory.Functor.Elements : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor C (Type w) → Type (max u w)
-- Mathlib.Topology.Algebra.NonUnitalAlgebra
NonUnitalSubalgebra.topologicalClosure_map_le : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : TopologicalSpace A]
  [inst_2 : NonUnitalSemiring A] [inst_3 : Module R A] [inst_4 : ContinuousConstSMul R A]
  [inst_5 : IsSemitopologicalSemiring A] [inst_6 : TopologicalSpace B] [inst_7 : NonUnitalSemiring B]
  [inst_8 : Module R B] [inst_9 : IsTopologicalSemiring B] [inst_10 : ContinuousConstSMul R B]
  (s : NonUnitalSubalgebra R A) {φ : A →ₙₐ[R] B},
  IsClosedMap ⇑φ → (NonUnitalSubalgebra.map φ s).topologicalClosure ≤ NonUnitalSubalgebra.map φ s.topologicalClosure
-- Mathlib.Analysis.SpecialFunctions.ExpDeriv
ContDiff.cexp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAlgebra 𝕜 ℂ] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : E → ℂ} {n : WithTop ℕ∞},
  ContDiff 𝕜 n f → ContDiff 𝕜 n fun x => Complex.exp (f x)
-- Mathlib.Analysis.Calculus.Deriv.Inv
HasDerivAt.fun_div : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} {𝕜' : Type u_1} [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {c d : 𝕜 → 𝕜'} {c' d' : 𝕜'},
  HasDerivAt c c' x → HasDerivAt d d' x → d x ≠ 0 → HasDerivAt (fun y => c y / d y) ((c' * d x - c x * d') / d x ^ 2) x
-- Mathlib.Algebra.GroupWithZero.Basic
isReduced_of_noZeroDivisors : ∀ {M₀ : Type u_1} [inst : MonoidWithZero M₀] [NoZeroDivisors M₀], IsReduced M₀
-- Mathlib.CategoryTheory.Triangulated.Rotate
CategoryTheory.Pretriangulated.invRotCompRot_hom_app_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  (X : CategoryTheory.Pretriangulated.Triangle C),
  (CategoryTheory.Pretriangulated.invRotCompRot.hom.app X).hom₃ =
    (CategoryTheory.shiftFunctorCompIsoId C (-1) 1 ⋯).hom.app X.obj₃
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.dropLast.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (head : α) → motive [head]) (h_3 : (a : α) → (as : List α) → motive (a :: as)),
  (as = [] → False) →
    (match a :: as with
      | [] => h_1 ()
      | [head] => h_2 head
      | a :: as => h_3 a as) =
      h_3 a as
-- Init.Data.Vector.Lemmas
Vector.back?_mk : ∀ {α : Type u_1} {n : ℕ} {xs : Array α} (h : xs.size = n), (Vector.mk xs h).back? = xs.back?
-- Mathlib.Combinatorics.Additive.ErdosGinzburgZiv
_private.Mathlib.Combinatorics.Additive.ErdosGinzburgZiv.0.f₂.eq_1 : ∀ {ι : Type u_1} {p : ℕ} [inst : Fact (Nat.Prime p)] (s : Finset ι) (a : ι → ZMod p),
  f₂✝ s a = ∑ i, a ↑i • MvPolynomial.X i ^ (p - 1)
-- Mathlib.LinearAlgebra.Matrix.Kronecker
Matrix.smul_kronecker : ∀ {R : Type u_1} {α : Type u_3} {l : Type u_9} {m : Type u_10} {n : Type u_11} {p : Type u_12} [inst : Mul α]
  [inst_1 : SMul R α] [IsScalarTower R α α] (r : R) (A : Matrix l m α) (B : Matrix n p α),
  Matrix.kroneckerMap (fun x1 x2 => x1 * x2) (r • A) B = r • Matrix.kroneckerMap (fun x1 x2 => x1 * x2) A B
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.single_apply : ∀ (p : ENNReal) (𝕜 : Type u_1) {ι : Type u_2} [inst : DecidableEq ι] [inst_1 : Zero 𝕜] (i : ι) (a : 𝕜) (j : ι),
  (PiLp.single p i a).ofLp j = if j = i then a else 0
-- Init.Data.Nat.Lemmas
Nat.add_sub_cancel_right : ∀ (n m : ℕ), n + m - m = n
-- Mathlib.Tactic.Widget.LibraryRewrite
Mathlib.Tactic.LibraryRewrite.RewriteLemma.mk.sizeOf_spec : ∀ (name : Lean.Name) (symm : Bool), sizeOf { name := name, symm := symm } = 1 + sizeOf name + sizeOf symm
-- Lean.Server.Rpc.RequestHandling
Lean.Server.userRpcProcedures : Lean.MapDeclarationExtension Lean.Name
-- Mathlib.Computability.Partrec
Computable.pred : Computable Nat.pred
-- Init.Data.Format.Syntax
Lean.Syntax.instToFormat : Std.ToFormat Lean.Syntax
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.instIsMonHomComp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N O : C}
  [inst_2 : CategoryTheory.MonObj M] [inst_3 : CategoryTheory.MonObj N] [inst_4 : CategoryTheory.MonObj O] (f : M ⟶ N)
  (g : N ⟶ O) [CategoryTheory.IsMonHom f] [CategoryTheory.IsMonHom g],
  CategoryTheory.IsMonHom (CategoryTheory.CategoryStruct.comp f g)
-- Mathlib.Analysis.Normed.Group.Basic
NormedGroup.uniformity_basis_dist : ∀ {E : Type u_5} [inst : SeminormedGroup E], (uniformity E).HasBasis (fun ε => 0 < ε) fun ε => {p | ‖p.1⁻¹ * p.2‖ < ε}
-- Mathlib.Data.Int.NatPrime
Int.succ_dvd_or_succ_dvd_of_succ_sum_dvd_mul : ∀ {p : ℕ},
  Nat.Prime p →
    ∀ {m n : ℤ} {k l : ℕ},
      ↑(p ^ k) ∣ m → ↑(p ^ l) ∣ n → ↑(p ^ (k + l + 1)) ∣ m * n → ↑(p ^ (k + 1)) ∣ m ∨ ↑(p ^ (l + 1)) ∣ n
-- Mathlib.Geometry.RingedSpace.OpenImmersion
AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.app_invApp_assoc : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (f : X ⟶ Y) [H : AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion f]
  (U : TopologicalSpace.Opens ↑Y.toTopCat) {Z : CommRingCat}
  (h :
    Y.presheaf.obj
        (Opposite.op
          ((AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.opensFunctor f).obj
            ((TopologicalSpace.Opens.map f.base).obj U))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp (f.c.app (Opposite.op U))
      (CategoryTheory.CategoryStruct.comp
        (AlgebraicGeometry.LocallyRingedSpace.IsOpenImmersion.invApp f ((TopologicalSpace.Opens.map f.base).obj U)) h) =
    CategoryTheory.CategoryStruct.comp (Y.presheaf.map (CategoryTheory.homOfLE ⋯).op) h
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.support_zpowers_of_mem_cycleFactorsFinset_le : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α} {c : ↥g.cycleFactorsFinset}
  (v : ↥(Subgroup.zpowers ↑c)), (↑v).support ⊆ g.support
-- Lean.Declaration
Lean.QuotKind.ind.sizeOf_spec : sizeOf Lean.QuotKind.ind = 1
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec32_abs : ∀ (a : ISize) (h : System.Platform.numBits = 32), a.abs.toBitVec32 h = (a.toBitVec32 h).abs
-- Mathlib.Algebra.Category.Grp.Basic
/-- Universe lift functor for additive commutative groups.  -/
AddCommGrpCat.uliftFunctor : CategoryTheory.Functor AddCommGrpCat AddCommGrpCat
-- Init.Data.String.TakeDrop
/-- Creates a string slice that contains the longest prefix of `s` in which `pat` matched
\(potentially repeatedly\).

This is a cheap operation because it does not allocate a new string to hold the result.
To convert the result into a string, use `String.Slice.copy`.

This function is generic over all currently supported patterns.

Examples:

* `"red green blue".takeWhile Char.isLower == "red".toSlice`

* `"red green blue".takeWhile 'r' == "r".toSlice`

* `"red red green blue".takeWhile "red " == "red red ".toSlice`

* `"red green blue".takeWhile (fun (_ : Char) => true) == "red green blue".toSlice`
 -/
String.takeWhile : {ρ : Type} → String → (pat : ρ) → [String.Slice.Pattern.ForwardPattern pat] → String.Slice
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- **Alias** of `MeasureTheory.measure_sdiff_add_inter`. -/
MeasureTheory.measure_diff_add_inter : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasurableSet t → μ (s \ t) + μ (s ∩ t) = μ s
-- Mathlib.RingTheory.Length
/-- The length of a module, defined as the krull dimension of its submodule lattice.  -/
Module.length : (R : Type u_1) → (M : Type u_2) → [inst : Ring R] → [inst_1 : AddCommGroup M] → [Module R M] → ℕ∞
-- Std.Time.Format.Basic
_private.Std.Time.Format.Basic.0.Std.Time.GenericFormat.DateBuilder.F : Std.Time.GenericFormat.DateBuilder✝ → Option (Std.Time.Internal.Bounded.LE 1 5)
-- Mathlib.Data.List.Fold
List.foldr_cons_eq_foldr_apply : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {f : α → β → β} {a : α} {b : β} [hf : LeftCommutative f],
  List.foldr f b (a :: l) = List.foldr f (f a b) l
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem!_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  [inst_1 : Inhabited β], k ∉ t₂ → (t₁ ∪ t₂)[k]! = t₁[k]!
-- Mathlib.FieldTheory.Separable
/-- If a non-zero polynomial splits, then it has no repeated roots on that field
if and only if it is separable.  -/
Polynomial.nodup_roots_iff_of_splits : ∀ {F : Type u} [inst : Field F] {f : Polynomial F}, f ≠ 0 → f.Splits → (f.roots.Nodup ↔ f.Separable)
-- Init.Tactics
/-- `letI` behaves like `let`, but inlines the value instead of producing a `let` term.  -/
Lean.Parser.Tactic.tacticLetI__ : Lean.ParserDescr
-- Mathlib.NumberTheory.ModularForms.Cusps
Subgroup.strictWidthInfty_pos_iff : ∀ {𝒢 : Subgroup (GL (Fin 2) ℝ)} [DiscreteTopology ↥𝒢.strictPeriods] [𝒢.HasDetPlusMinusOne],
  0 < 𝒢.strictWidthInfty ↔ IsCusp OnePoint.infty 𝒢