mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Orthogonal
CategoryTheory.ObjectProperty.instIsTriangulatedClosed₂LeftOrthogonal : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [inst_1 : CategoryTheory.Limits.HasZeroObject C] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive]
  [inst_5 : CategoryTheory.Pretriangulated C], P.leftOrthogonal.IsTriangulatedClosed₂
-- Init.Data.UInt.Lemmas
UInt16.toBitVec_sub : ∀ {a b : UInt16}, (a - b).toBitVec = a.toBitVec - b.toBitVec
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.of_forall_getKey?_unit_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {m₁ m₂ : Std.DHashMap α fun x => Unit},
  (∀ (k : α), m₁.getKey? k = m₂.getKey? k) → m₁.Equiv m₂
-- Init.Data.Rat.Basic
Rat.instSub : Sub ℚ
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.Struct.neutral? : Lean.Meta.Grind.AC.Struct → Option Lean.Expr
-- Std.Internal.Parsec.String
_private.Std.Internal.Parsec.String.0.Std.Internal.Parsec.String.skipWs : {s : String} → s.Pos → s.Pos
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.FinTwo
Matrix.GeneralLinearGroup.isParabolic_conj_iff' : ∀ {R : Type u_1} [inst : CommRing R] (g h : GL (Fin 2) R), (g⁻¹ * h * g).IsParabolic ↔ h.IsParabolic
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.PreZeroHypercover.sigmaOfIsColimit.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S)
  {c : CategoryTheory.Limits.Cofan E.X} (hc : CategoryTheory.Limits.IsColimit c),
  E.sigmaOfIsColimit hc =
    { I₀ := PUnit.{w + 1}, X := fun x => c.pt, f := fun x => CategoryTheory.Limits.Cofan.IsColimit.desc hc E.f }
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Iso
CategoryTheory.Limits.pullback_fst_iso_of_right_iso : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_1 : CategoryTheory.IsIso g], CategoryTheory.IsIso (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Analysis.Complex.Trigonometric
Complex.sin_sq : ∀ (x : ℂ), Complex.sin x ^ 2 = 1 - Complex.cos x ^ 2
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitDisc.coe_neg : ∀ (z : Complex.UnitDisc), ↑(-z) = -↑z
-- Mathlib.CategoryTheory.Subobject.Basic
/-- An equality of subobjects gives an isomorphism of the corresponding objects.  -/
CategoryTheory.Subobject.isoOfEqMk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {B A : C} →
      (X : CategoryTheory.Subobject B) →
        (f : A ⟶ B) →
          [inst_1 : CategoryTheory.Mono f] →
            X = CategoryTheory.Subobject.mk f → (CategoryTheory.Subobject.underlying.obj X ≅ A)
-- Mathlib.Order.Defs.Unbundled
IsUpperSet.eq_1 : ∀ {α : Type u_1} [inst : LE α] (s : Set α), IsUpperSet s = ∀ ⦃a b : α⦄, a ≤ b → a ∈ s → b ∈ s
-- Mathlib.Order.Interval.Finset.Nat
Nat.mem_Ioc_succ : ∀ {a b : ℕ}, a ∈ Finset.Ioc b (b + 1) ↔ a = b + 1
-- Mathlib.Data.ENat.Lattice
instCompleteLinearOrderENat : CompleteLinearOrder ℕ∞
-- Mathlib.Logic.Basic
peirce : ∀ (a b : Prop), ((a → b) → a) → a
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.nthRoots_eq : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {n : ℕ} {ζ : R},
  IsPrimitiveRoot ζ n →
    ∀ {α a : R}, α ^ n = a → Polynomial.nthRoots n a = Multiset.map (fun x => ζ ^ x * α) (Multiset.range n)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexSingle
CochainComplex.HomComplex.Cocycle.fromSingleMk_postcomp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X : C} {K : CochainComplex C ℤ} {p q : ℤ} (f : X ⟶ K.X q) {n : ℤ}
  (h : p + n = q) (q' : ℤ) (hq' : q + 1 = q') (hf : CategoryTheory.CategoryStruct.comp f (K.d q q') = 0)
  {L : CochainComplex C ℤ} (g : K ⟶ L),
  CochainComplex.HomComplex.Cocycle.fromSingleMk (CategoryTheory.CategoryStruct.comp f (g.f q)) h q' hq' ⋯ =
    (CochainComplex.HomComplex.Cocycle.fromSingleMk f h q' hq' hf).postcomp g
-- Init.Data.SInt.Basic
instXorOpISize : XorOp ISize
-- Mathlib.Order.Filter.Interval
Filter.Tendsto.Icc : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] {l₁ l₂ : Filter α} [Filter.TendstoIxxClass Set.Icc l₁ l₂]
  {lb : Filter β} {u₁ u₂ : β → α},
  Filter.Tendsto u₁ lb l₁ → Filter.Tendsto u₂ lb l₁ → Filter.Tendsto (fun x => Set.Icc (u₁ x) (u₂ x)) lb l₂.smallSets
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SolverTerms.nil : Lean.Meta.Grind.SolverTerms
-- Init.Data.List.Perm
List.isPerm_iff : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {l₁ l₂ : List α}, l₁.isPerm l₂ = true ↔ l₁.Perm l₂
-- Mathlib.GroupTheory.FiniteIndexNormalSubgroup
FiniteIndexNormalAddSubgroup.mem_toAddSubgroup_iff : ∀ {G : Type u_1} [inst : AddGroup G] {H : FiniteIndexNormalAddSubgroup G} {g : G}, g ∈ H.toAddSubgroup ↔ g ∈ H
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_lt_iff : ∀ {α β : Type u_1} {r : α → α → Prop} {s : β → β → Prop} [inst : IsWellOrder α r] [inst_1 : IsWellOrder β s],
  Ordinal.type r < Ordinal.type s ↔ Nonempty (PrincipalSeg r s)
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
IsIntegral.neg_iff : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] {x : B},
  IsIntegral R (-x) ↔ IsIntegral R x
-- Mathlib.Data.PFunctor.Univariate.M
PFunctor.MIntl.mk.injEq : ∀ {F : PFunctor.{uA, uB}} (approx : (n : ℕ) → PFunctor.Approx.CofixA F n) (consistent : PFunctor.Approx.AllAgree approx)
  (approx_1 : (n : ℕ) → PFunctor.Approx.CofixA F n) (consistent_1 : PFunctor.Approx.AllAgree approx_1),
  ({ approx := approx, consistent := consistent } = { approx := approx_1, consistent := consistent_1 }) =
    (approx = approx_1)
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- A difference `r -ₒ s` is equal to its expansion by an
arbitrary translation `t` if `t + s ∈ S`.  -/
AddOreLocalization.expand : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] (r : X) (s : ↥S) (t : R) (hst : t + ↑s ∈ S), r -ₒ s = (t +ᵥ r) -ₒ ⟨t + ↑s, hst⟩
-- Mathlib.Logic.Equiv.Defs
/-- Turn an element of a type `F` satisfying `EquivLike F α β` into an actual
`Equiv`. This is declared as the default coercion from `F` to `α ≃ β`.  -/
EquivLike.toEquiv : {α : Sort u} → {β : Sort v} → {F : Sort u_1} → [EquivLike F α β] → F → α ≃ β
-- Mathlib.Order.Fin.Tuple
Fin.consOrderIso_symm_apply : ∀ {n : ℕ} (α : Fin (n + 1) → Type u_2) [inst : (i : Fin (n + 1)) → LE (α i)] (f : (i : Fin (n + 1)) → α i),
  (RelIso.symm (Fin.consOrderIso α)) f = (f 0, Fin.tail f)
-- Mathlib.CategoryTheory.Preadditive.Biproducts
/-- If the (coproduct-like) biproduct comparison for `F`, `X` and `Y` is an epimorphism, then
`F` preserves the biproduct of `X` and `Y`. For the converse, see `mapBiprod`.  -/
CategoryTheory.Limits.preservesBinaryBiproduct_of_epi_biprodComparison' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] [inst_3 : CategoryTheory.Preadditive D] (F : CategoryTheory.Functor C D)
  [inst_4 : F.PreservesZeroMorphisms] {X Y : C} [inst_5 : CategoryTheory.Limits.HasBinaryBiproduct X Y]
  [inst_6 : CategoryTheory.Limits.HasBinaryBiproduct (F.obj X) (F.obj Y)]
  [CategoryTheory.Epi (F.biprodComparison' X Y)], CategoryTheory.Limits.PreservesBinaryBiproduct X Y F
-- Mathlib.Algebra.Order.Module.Archimedean
FiniteArchimedeanClass.ball_lt_closedBall : ∀ {M : Type u_1} [inst : AddCommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedAddMonoid M] (K : Type u_2)
  [inst_3 : Ring K] [inst_4 : LinearOrder K] [inst_5 : IsOrderedRing K] [inst_6 : Archimedean K] [inst_7 : Module K M]
  [inst_8 : PosSMulMono K M] {c : FiniteArchimedeanClass M},
  FiniteArchimedeanClass.ball K c < FiniteArchimedeanClass.closedBall K c
-- Mathlib.Analysis.Normed.Group.InfiniteSum
cauchySeq_finset_of_norm_bounded : ∀ {ι : Type u_1} {E : Type u_3} [inst : SeminormedAddCommGroup E] {f : ι → E} {g : ι → ℝ},
  Summable g → (∀ (i : ι), ‖f i‖ ≤ g i) → CauchySeq fun s => ∑ i ∈ s, f i
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.forward.eq_2 : ∀ (x : String.Legacy.Iterator) (n : ℕ), x.forward n.succ = x.next.forward n
-- Mathlib.Algebra.Algebra.Operations
Submodule.mem_span_mul_finite_of_mem_mul : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] {P Q : Submodule R A}
  {x : A}, x ∈ P * Q → ∃ T T', ↑T ⊆ ↑P ∧ ↑T' ⊆ ↑Q ∧ x ∈ Submodule.span R (↑T * ↑T')
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
Unitization.starLift_range_le : ∀ {R : Type u_1} {A : Type u_2} {C : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A]
  [inst_2 : StarRing R] [inst_3 : StarRing A] [inst_4 : Module R A] [inst_5 : SMulCommClass R A A]
  [inst_6 : IsScalarTower R A A] [inst_7 : StarModule R A] [inst_8 : Semiring C] [inst_9 : StarRing C]
  [inst_10 : Algebra R C] [inst_11 : StarModule R C] {f : A →⋆ₙₐ[R] C} {S : StarSubalgebra R C},
  (Unitization.starLift f).range ≤ S ↔ NonUnitalStarAlgHom.range f ≤ S.toNonUnitalStarSubalgebra
-- Lean.Meta.Tactic.Grind.Types
/-- Next local declaration index to process.  -/
Lean.Meta.Grind.GoalState.nextDeclIdx : Lean.Meta.Grind.GoalState → ℕ
-- Mathlib.Geometry.Convex.ConvexSpace.Prod
Prod.fst_convexCombPair : ∀ {R : Type u_2} [inst : Semiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {X : Type u_3}
  {Y : Type u_4} [inst_3 : Convexity.ConvexSpace R X] [inst_4 : Convexity.ConvexSpace R Y] (a b : R) (ha : 0 ≤ a)
  (hb : 0 ≤ b) (hab : a + b = 1) (x y : X × Y),
  (Convexity.convexCombPair a b ha hb hab x y).1 = Convexity.convexCombPair a b ha hb hab x.1 y.1
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.State.ctx : Lean.Meta.SimpAll.State → Lean.Meta.Simp.Context
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteGrp.ofHom_hom : ∀ {A B : ProfiniteGrp.{u}} (f : A ⟶ B), ProfiniteGrp.ofHom (ProfiniteGrp.Hom.hom f) = f
-- Mathlib.Combinatorics.Enumerative.IncidenceAlgebra
IncidenceAlgebra.instModule : {𝕜 : Type u_2} →
  {𝕝 : Type u_3} →
    {α : Type u_5} →
      [inst : Preorder α] →
        [inst_1 : LocallyFiniteOrder α] →
          [inst_2 : DecidableEq α] →
            [inst_3 : Semiring 𝕜] →
              [inst_4 : Semiring 𝕝] → [Module 𝕜 𝕝] → Module (IncidenceAlgebra 𝕜 α) (IncidenceAlgebra 𝕝 α)
-- Mathlib.RingTheory.PowerSeries.Substitution
PowerSeries.subst_C : ∀ {τ : Type u_3} {S : Type u_4} [inst : CommRing S] {a : MvPowerSeries τ S} (r : S),
  PowerSeries.subst a (PowerSeries.C r) = MvPowerSeries.C r
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.ShortComplex.p_fromOpcycles_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) [inst_2 : S.HasRightHomology] {Z : C} (h : S.X₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp S.pOpcycles (CategoryTheory.CategoryStruct.comp S.fromOpcycles h) =
    CategoryTheory.CategoryStruct.comp S.g h
-- Mathlib.Order.WithBot
WithBot.strictMono_map_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMono (WithBot.map f) ↔ StrictMono f
-- Mathlib.LinearAlgebra.Complex.Module
Complex.lift_symm_apply_coe : ∀ {A : Type u_1} [inst : Ring A] [inst_1 : Algebra ℝ A] (F : ℂ →ₐ[ℝ] A), ↑(Complex.lift.symm F) = F Complex.I
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.coe_pow : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MonoidWithZero α] [inst_2 : NoZeroDivisors α] [inst_3 : Nontrivial α]
  (a : α) (n : ℕ), ↑(a ^ n) = ↑a ^ n
-- Mathlib.Analysis.Calculus.ContDiff.Operations
contDiff_neg : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {F : Type uF} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {n : WithTop ℕ∞}, ContDiff 𝕜 n fun p => -p
-- Mathlib.CategoryTheory.Abelian.Injective.Ext
CategoryTheory.InjectiveResolution.extEquivCohomologyClass_neg : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] {X Y : C} (R : CategoryTheory.InjectiveResolution Y) {n : ℕ}
  (x : CategoryTheory.Abelian.Ext X Y n), R.extEquivCohomologyClass (-x) = -R.extEquivCohomologyClass x
-- Mathlib.Analysis.Normed.Group.Defs
SeminormedGroup.mk : {E : Type u_8} →
  [toNorm : Norm E] →
    [toGroup : Group E] →
      [toPseudoMetricSpace : PseudoMetricSpace E] →
        autoParam (∀ (x y : E), dist x y = ‖x⁻¹ * y‖) SeminormedGroup.dist_eq._autoParam → SeminormedGroup E
-- Mathlib.Geometry.Manifold.Instances.Real
EuclideanQuadrant.convex : ∀ {n : ℕ}, Convex ℝ {x | ∀ (i : Fin n), 0 ≤ x.ofLp i}
-- Mathlib.LinearAlgebra.Matrix.SesquilinearForm
Matrix.toLinearMapₛₗ₂'_symm : ∀ {R : Type u_1} {R₁ : Type u_2} {S₁ : Type u_3} {R₂ : Type u_4} {S₂ : Type u_5} {N₂ : Type u_10} {n : Type u_11}
  {m : Type u_12} [inst : CommSemiring R] [inst_1 : AddCommMonoid N₂] [inst_2 : Module R N₂] [inst_3 : Semiring R₁]
  [inst_4 : Semiring R₂] [inst_5 : Semiring S₁] [inst_6 : Semiring S₂] [inst_7 : Module S₁ N₂] [inst_8 : Module S₂ N₂]
  [inst_9 : SMulCommClass S₁ R N₂] [inst_10 : SMulCommClass S₂ R N₂] [inst_11 : SMulCommClass S₂ S₁ N₂] (σ₁ : R₁ →+* S₁)
  (σ₂ : R₂ →+* S₂) [inst_12 : Fintype n] [inst_13 : Fintype m] [inst_14 : DecidableEq n] [inst_15 : DecidableEq m],
  (Matrix.toLinearMapₛₗ₂' R σ₁ σ₂).symm = LinearMap.toMatrixₛₗ₂' R
-- Mathlib.FieldTheory.Finite.GaloisField
FiniteField.unitsMap_norm_surjective : ∀ (K : Type u_1) (K' : Type u_2) [inst : Field K] [inst_1 : Field K'] [inst_2 : Algebra K K'] [Finite K'],
  Function.Surjective ⇑(Units.map (Algebra.norm K))
-- Mathlib.Analysis.Complex.ValueDistribution.FirstMainTheorem
/-- Helper lemma for the first part of the First Main Theorem: Away from zero, the difference between
the characteristic functions of `f` and `f⁻¹` equals `log ‖meromorphicTrailingCoeffAt f 0‖`.
 -/
ValueDistribution.characteristic_sub_characteristic_inv_of_ne_zero : ∀ {f : ℂ → ℂ} {R : ℝ},
  Meromorphic f →
    R ≠ 0 →
      ValueDistribution.characteristic f ⊤ R - ValueDistribution.characteristic f⁻¹ ⊤ R =
        Real.log ‖meromorphicTrailingCoeffAt f 0‖
-- Init.Grind.Ring.CommSolver
_private.Init.Grind.Ring.CommSolver.0.Lean.Grind.CommRing.Poly.pow.match_1.splitter : (motive : ℕ → Sort u_1) →
  (k : ℕ) → (Unit → motive 0) → (Unit → motive 1) → ((k : ℕ) → (k = 0 → False) → motive k.succ) → motive k
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Reindex a categorical product via an equivalence of the index types.  -/
CategoryTheory.Limits.Pi.reindex : {β : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {γ : Type w'} →
        (ε : β ≃ γ) →
          (f : γ → C) →
            [inst_1 : CategoryTheory.Limits.HasProduct f] →
              [inst_2 : CategoryTheory.Limits.HasProduct (f ∘ ⇑ε)] → ∏ᶜ f ∘ ⇑ε ≅ ∏ᶜ f
-- Mathlib.Topology.Sets.VietorisTopology
Continuous.compacts_map : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β}
  (hf : Continuous f), Continuous (TopologicalSpace.Compacts.map f hf)
-- Mathlib.Algebra.Star.Subalgebra
StarSubalgebra.map_le_iff_le_comap : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : Semiring A]
  [inst_3 : StarRing A] [inst_4 : Algebra R A] [inst_5 : StarModule R A] [inst_6 : Semiring B] [inst_7 : StarRing B]
  [inst_8 : Algebra R B] [inst_9 : StarModule R B] {S : StarSubalgebra R A} {f : A →⋆ₐ[R] B} {U : StarSubalgebra R B},
  StarSubalgebra.map f S ≤ U ↔ S ≤ StarSubalgebra.comap f U
-- Mathlib.Data.Finset.Lattice.Fold
/-- **Alias** of `Finset.apply_sup_eq_sup_comp_of_linearOrder`. -/
Finset.comp_sup_eq_sup_comp_of_is_total : ∀ {α : Type u_2} {β : Type u_3} {ι : Type u_5} [inst : LinearOrder α] [inst_1 : OrderBot α] {s : Finset ι} {f : ι → α}
  [inst_2 : SemilatticeSup β] [inst_3 : OrderBot β] (g : α → β), Monotone g → g ⊥ = ⊥ → g (s.sup f) = s.sup (g ∘ f)
-- Mathlib.RingTheory.Localization.InvSubmonoid
/-- There is an equivalence of monoids between the image of `M` and `invSubmonoid`.  -/
IsLocalization.equivInvSubmonoid : {R : Type u_1} →
  [inst : CommRing R] →
    (M : Submonoid R) →
      (S : Type u_2) →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            [IsLocalization M S] → ↥(Submonoid.map (algebraMap R S) M) ≃* ↥(IsLocalization.invSubmonoid M S)
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.leadingCoeff_mul : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A] [inst_4 : Add B] [AddLeftStrictMono B]
  [AddRightStrictMono B] [NoZeroDivisors R],
  Function.Injective D →
    (∀ (a1 a2 : A), D (a1 + a2) = D a1 + D a2) →
      AddMonoidAlgebra.leadingCoeff D (p * q) = AddMonoidAlgebra.leadingCoeff D p * AddMonoidAlgebra.leadingCoeff D q
-- Mathlib.Order.RelSeries
/-- A relation series with length `n` if the relation is infinite dimensional  -/
RelSeries.withLength : {α : Type u_1} → (r : SetRel α α) → [r.InfiniteDimensional] → ℕ → RelSeries r
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.lift_braiding_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {T X Y : C} (f : T ⟶ X) (g : T ⟶ Y) {Z : C}
  (h : CategoryTheory.MonoidalCategoryStruct.tensorObj Y X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift f g)
      (CategoryTheory.CategoryStruct.comp (β_ X Y).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.lift g f) h
-- Init.Data.Vector.Zip
Vector.zipWith_comm_of_comm : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} {f : α → α → β},
  (∀ (x y : α), f x y = f y x) → ∀ {xs ys : Vector α n}, Vector.zipWith f xs ys = Vector.zipWith f ys xs
-- Std.Time.Format.Basic
/-- A modifier that renders some data into text.
 -/
Std.Time.FormatPart.modifier : Std.Time.Modifier → Std.Time.FormatPart
-- Mathlib.Tactic.Zify
Mathlib.Tactic.Zify.natCast_ne : ∀ (a b : ℕ), a ≠ b ↔ ↑a ≠ ↑b
-- Mathlib.MeasureTheory.Group.Arithmetic
List.aemeasurable_fun_sum : ∀ {M : Type u_2} {α : Type u_3} [inst : AddMonoid M] [inst_1 : MeasurableSpace M] [MeasurableAdd₂ M]
  {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (l : List (α → M)),
  (∀ f ∈ l, AEMeasurable f μ) → AEMeasurable (fun x => (List.map (fun f => f x) l).sum) μ
-- Mathlib.RingTheory.HahnSeries.Valuation
HahnSeries.addVal_apply_of_ne : ∀ {Γ : Type u_1} {R : Type u_2} [inst : AddCancelCommMonoid Γ] [inst_1 : LinearOrder Γ]
  [inst_2 : IsOrderedCancelAddMonoid Γ] [inst_3 : Ring R] [inst_4 : IsDomain R] {x : HahnSeries Γ R},
  x ≠ 0 → (HahnSeries.addVal Γ R) x = ↑x.order
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.ArgReorder.brecOn_3.go : {motive_1 : Mathlib.Tactic.Translate.ArgReorder → Sort u} →
  {motive_2 : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u} →
    {motive_3 : List (ℕ × Mathlib.Tactic.Translate.ArgReorder) → Sort u} →
      {motive_4 : ℕ × Mathlib.Tactic.Translate.ArgReorder → Sort u} →
        (t : ℕ × Mathlib.Tactic.Translate.ArgReorder) →
          ((t : Mathlib.Tactic.Translate.ArgReorder) → t.below → motive_1 t) →
            ((t : Array (ℕ × Mathlib.Tactic.Translate.ArgReorder)) →
                Mathlib.Tactic.Translate.ArgReorder.below_1 t → motive_2 t) →
              ((t : List (ℕ × Mathlib.Tactic.Translate.ArgReorder)) →
                  Mathlib.Tactic.Translate.ArgReorder.below_2 t → motive_3 t) →
                ((t : ℕ × Mathlib.Tactic.Translate.ArgReorder) →
                    Mathlib.Tactic.Translate.ArgReorder.below_3 t → motive_4 t) →
                  motive_4 t ×' Mathlib.Tactic.Translate.ArgReorder.below_3 t
-- Lean.Compiler.IR.Basic
Lean.IR.Decl.extern : Lean.IR.FunId → Array Lean.IR.Param → Lean.IR.IRType → Lean.ExternAttrData → Lean.IR.Decl
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
/-- The 2nd object in the complex of inhomogeneous cochains of `A : Rep k G` is isomorphic
to `Fun(G², A)` as a `k`-module.  -/
groupCohomology.cochainsIso₂ : {k G : Type u} →
  [inst : CommRing k] →
    [inst_1 : Group G] →
      (A : Rep.{u, u, u} k G) → (groupCohomology.inhomogeneousCochains A).X 2 ≅ ModuleCat.of k (G × G → ↑A)
-- Mathlib.Computability.RecursiveIn
/-- If every element of `O` is `RecursiveIn O'`, then any function which is
`RecursiveIn O` is also `RecursiveIn O'`.  -/
RecursiveIn.subst : ∀ {α : Type u_1} {σ : Type u_4} [inst : Primcodable α] [inst_1 : Primcodable σ] {O O' : Set (ℕ →. ℕ)} {f : α →. σ},
  RecursiveIn O f → (∀ g ∈ O, RecursiveIn O' g) → RecursiveIn O' f
-- Init.Data.Option.Attach
Option.isNone_unattach : ∀ {α : Type u_1} {p : α → Prop} {o : Option { x // p x }}, o.unattach.isNone = o.isNone
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.submatrix_hadamard : ∀ {α : Type u_1} {m : Type u_2} {n : Type u_3} {l : Type u_5} {o : Type u_6} [inst : Mul α] (A B : Matrix m n α)
  (e : l → m) (f : o → n), (A.hadamard B).submatrix e f = (A.submatrix e f).hadamard (B.submatrix e f)
-- Std.Http.Data.URI.Basic
Std.Http.URI.instInhabitedPort : Inhabited Std.Http.URI.Port
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
/-- The canonical map `P ⟶ L₂.X₁`.  -/
CategoryTheory.ShortComplex.SnakeInput.φ₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] → (S : CategoryTheory.ShortComplex.SnakeInput C) → S.P ⟶ S.L₂.X₁
-- Mathlib.Order.Ideal
Order.Ideal.principal_top : ∀ {P : Type u_1} [inst : Preorder P] [inst_1 : OrderTop P], Order.Ideal.principal ⊤ = ⊤
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.mapDomainRingEquiv.eq_1 : ∀ (R : Type u_3) {M : Type u_6} {N : Type u_7} [inst : Semiring R] [inst_1 : Monoid M] [inst_2 : Monoid N] (e : M ≃* N),
  MonoidAlgebra.mapDomainRingEquiv R e =
    RingEquiv.ofRingHom (MonoidAlgebra.mapDomainRingHom R ↑e) (MonoidAlgebra.mapDomainRingHom R ↑e.symm) ⋯ ⋯
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_val : ∀ {α : Type u_1} [inst : DecidableEq α] (s₁ s₂ : Finset α), (s₁ ∩ s₂).val = s₁.val ∩ s₂.val
-- Mathlib.Algebra.Group.Idempotent
/-- An element `a` is said to be idempotent if `a * a = a`.  -/
IsIdempotentElem : {M : Type u_1} → [Mul M] → M → Prop
-- Mathlib.Topology.Homotopy.HomotopyGroup
/-- Group structure on `HomotopyGroup` obtained by pulling back path composition along the
`i`th direction. The group structures for two different `i j : N` distribute over each
other, and therefore are equal by the Eckmann-Hilton argument.  -/
HomotopyGroup.auxGroup : {N : Type u_1} →
  {X : Type u_2} → [inst : TopologicalSpace X] → {x : X} → [DecidableEq N] → N → Group (HomotopyGroup N X x)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Grp.trivial_X : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  (CategoryTheory.Grp.trivial C).X = CategoryTheory.MonoidalCategoryStruct.tensorUnit C
-- Mathlib.Algebra.Polynomial.OfFn
/-- `ofFn n v` has `natDegree` smaller than `n`.  -/
Polynomial.ofFn_natDegree_lt : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : DecidableEq R] {n : ℕ},
  1 ≤ n → ∀ (v : Fin n → R), ((Polynomial.ofFn n) v).natDegree < n
-- Mathlib.Data.ZMod.Basic
ZMod.forall : ∀ {n : ℕ} {P : ZMod n → Prop}, (∀ (x : ZMod n), P x) ↔ ∀ (x : ℤ), P ↑x
-- Mathlib.RingTheory.DividedPowers.SubDPIdeal
DividedPowers.SubDPIdeal.mk.inj : ∀ {A : Type u_1} {inst : CommSemiring A} {I : Ideal A} {hI : DividedPowers I} {carrier : Ideal A}
  {isSubideal : carrier ≤ I} {dpow_mem : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier, hI.dpow n j ∈ carrier} {carrier_1 : Ideal A}
  {isSubideal_1 : carrier_1 ≤ I} {dpow_mem_1 : ∀ (n : ℕ), n ≠ 0 → ∀ j ∈ carrier_1, hI.dpow n j ∈ carrier_1},
  { carrier := carrier, isSubideal := isSubideal, dpow_mem := dpow_mem } =
      { carrier := carrier_1, isSubideal := isSubideal_1, dpow_mem := dpow_mem_1 } →
    carrier = carrier_1
-- Mathlib.Tactic.FunProp.Types
Mathlib.Meta.FunProp.instInhabitedGeneralTheorems.default : Mathlib.Meta.FunProp.GeneralTheorems