mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Parser.Extension
Lean.Parser.ParserExtension.State.mk.injEq : ∀ (tokens : Lean.Parser.TokenTable) (kinds : Lean.Parser.SyntaxNodeKindSet) (categories : Lean.Parser.ParserCategories)
  (tokens_1 : Lean.Parser.TokenTable) (kinds_1 : Lean.Parser.SyntaxNodeKindSet)
  (categories_1 : Lean.Parser.ParserCategories),
  ({ tokens := tokens, kinds := kinds, categories := categories } =
      { tokens := tokens_1, kinds := kinds_1, categories := categories_1 }) =
    (tokens = tokens_1 ∧ kinds = kinds_1 ∧ categories = categories_1)
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
/-- Recursive definition for the Cantor normal form.  -/
Ordinal.CNF.ne_zero : ∀ {b o : Ordinal.{u_1}},
  o ≠ 0 → Ordinal.CNF b o = (Ordinal.log b o, o / b ^ Ordinal.log b o) :: Ordinal.CNF b (o % b ^ Ordinal.log b o)
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.one_gradedMul : ∀ {R : Type u_1} {ι : Type u_2} [inst : CommSemiring ι] [inst_1 : Module ι (Additive ℤˣ)] [inst_2 : DecidableEq ι]
  (𝒜 : ι → Type u_3) (ℬ : ι → Type u_4) [inst_3 : CommRing R] [inst_4 : (i : ι) → AddCommGroup (𝒜 i)]
  [inst_5 : (i : ι) → AddCommGroup (ℬ i)] [inst_6 : (i : ι) → Module R (𝒜 i)] [inst_7 : (i : ι) → Module R (ℬ i)]
  [inst_8 : DirectSum.GRing 𝒜] [inst_9 : DirectSum.GRing ℬ] [inst_10 : DirectSum.GAlgebra R 𝒜]
  [inst_11 : DirectSum.GAlgebra R ℬ] (x : TensorProduct R (DirectSum ι fun i => 𝒜 i) (DirectSum ι fun i => ℬ i)),
  ((TensorProduct.gradedMul R 𝒜 ℬ) 1) x = x
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- the `r`th page of a spectral sequence is an homological complex  -/
CategoryTheory.SpectralSequence.page : {C : Type u_1} →
  [inst : CategoryTheory.Category.{u_3, u_1} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {κ : Type u_2} →
        {c : ℤ → ComplexShape κ} →
          {r₀ : ℤ} →
            CategoryTheory.SpectralSequence C c r₀ →
              (r : ℤ) → autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence._auto_1 → HomologicalComplex C (c r)
-- Mathlib.Algebra.Lie.Weights.Basic
LieModule.Weight.isZero_iff_eq_zero : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [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 : LieRing.IsNilpotent L] [inst_8 : Nontrivial ↥(LieModule.genWeightSpace M 0)] {χ : LieModule.Weight R L M},
  χ.IsZero ↔ χ = 0
-- Mathlib.Tactic.SplitIfs
/-- Pops off the front of the list of names, or generates a fresh name if the
list is empty.
 -/
_private.Mathlib.Tactic.SplitIfs.0.Mathlib.Tactic.getNextName : IO.Ref (List (Lean.TSyntax `Lean.binderIdent)) → Lean.MetaM Lean.Name
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.weierstrassP_zero : ∀ (L : PeriodPair), L.weierstrassP 0 = 0
-- Mathlib.Combinatorics.Matroid.Minor.Contract
/-- A version of `contract_delete_comm` without the disjointness hypothesis,
and hence a less simple RHS.  -/
Matroid.contract_delete_comm' : ∀ {α : Type u_1} (M : Matroid α) (C D : Set α), (M.contract C).delete D = (M.delete (D \ C)).contract C
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.section_.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) [hf : CategoryTheory.IsSplitEpi f],
  CategoryTheory.section_ f = ⋯.some.section_
-- Init.Control.Lawful.Instances
_private.Init.Control.Lawful.Instances.0.ExceptT.bindCont.match_1.splitter : {ε α : Type u_1} →
  (motive : Except ε α → Sort u_2) →
    (x : Except ε α) → ((a : α) → motive (Except.ok a)) → ((e : ε) → motive (Except.error e)) → motive x
-- Mathlib.Topology.Connected.Basic
ConnectedSpace.mk : ∀ {α : Type u} [inst : TopologicalSpace α] [toPreconnectedSpace : PreconnectedSpace α], Nonempty α → ConnectedSpace α
-- Mathlib.Analysis.Matrix.Normed
Matrix.frobenius_nnnorm_replicateRow : ∀ {m : Type u_3} {α : Type u_5} {ι : Type u_7} [inst : Fintype m] [inst_1 : Unique ι]
  [inst_2 : SeminormedAddCommGroup α] (v : m → α), ‖Matrix.replicateRow ι v‖₊ = ‖WithLp.toLp 2 v‖₊
-- Std.Data.DTreeMap.Internal.Queries
Std.DTreeMap.Internal.Impl.minEntry!.eq_def : ∀ {α : Type u} {β : α → Type v} [inst : Inhabited ((a : α) × β a)] (x : Std.DTreeMap.Internal.Impl α β),
  x.minEntry! =
    match x with
    | Std.DTreeMap.Internal.Impl.leaf =>
      panicWithPosWithDecl "Std.Data.DTreeMap.Internal.Queries" "Std.DTreeMap.Internal.Impl.minEntry!" 367 13
        "Map is empty"
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => ⟨k, v⟩
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      l.minEntry!
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.C_dvd_iff_map_hom_eq_zero : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (q : R →+* S₁) (r : R),
  (∀ (r' : R), q r' = 0 ↔ r ∣ r') → ∀ (φ : MvPolynomial σ R), MvPolynomial.C r ∣ φ ↔ (MvPolynomial.map q) φ = 0
-- Aesop.Script.SpecificTactics
_private.Aesop.Script.SpecificTactics.0.Aesop.renameInaccessibleFVarsS.tacticBuilder : Lean.MVarId × Array Lean.FVarId → Aesop.Script.TacticBuilder
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If A ≠ B and C ≠ B then ∠ABC = 0 if and only if (dist A C) = abs ((dist A B) - (dist B C)).  -/
EuclideanGeometry.dist_eq_abs_sub_dist_iff_angle_eq_zero : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  p₁ ≠ p₂ → p₃ ≠ p₂ → (dist p₁ p₃ = |dist p₁ p₂ - dist p₃ p₂| ↔ EuclideanGeometry.angle p₁ p₂ p₃ = 0)
-- Mathlib.Algebra.Algebra.Rat
Rat.instSMulCommClass : ∀ {R : Type u_2} {S : Type u_3} [inst : DivisionRing S] [inst_1 : CharZero S] [inst_2 : SMul R S] [SMulCommClass R S S],
  SMulCommClass ℚ R S
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.instIsIsoIntπTruncGEOfIsStrictlyGE : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (K : CochainComplex C ℤ) [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : ∀ (i : ℤ), HomologicalComplex.HasHomology K i] (n : ℤ) [K.IsStrictlyGE n],
  CategoryTheory.IsIso (K.πTruncGE n)
-- Mathlib.Order.CompactlyGenerated.Basic
WellFoundedGT.finite_of_iSupIndep : ∀ {α : Type u_2} [inst : CompleteLattice α] [WellFoundedGT α] {ι : Type u_3} {t : ι → α},
  iSupIndep t → (∀ (i : ι), t i ≠ ⊥) → Finite ι
-- Mathlib.RingTheory.MvPowerSeries.Trunc
MvPowerSeries.trunc'_C : ∀ {σ : Type u_1} {R : Type u_2} [inst : DecidableEq σ] [inst_1 : CommSemiring R] (n : σ →₀ ℕ) (a : R),
  (MvPowerSeries.trunc' R n) (MvPowerSeries.C a) = MvPolynomial.C a
-- Mathlib.RingTheory.TensorProduct.MvPolynomial
/-- The tensor product of the polynomial algebra by an algebra
is algebraically equivalent to a polynomial algebra with
coefficients in that algebra  -/
MvPolynomial.scalarRTensorAlgEquiv : {R : Type u} →
  {N : Type v} →
    [inst : CommSemiring R] →
      {σ : Type u_1} →
        [inst_1 : CommSemiring N] → [inst_2 : Algebra R N] → TensorProduct R N (MvPolynomial σ R) ≃ₐ[N] MvPolynomial σ N
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- `Localization.mk` as a monoid hom.  -/
Localization.mkHom : {M : Type u_1} → [inst : CommMonoid M] → {S : Submonoid M} → M × ↥S →* Localization S
-- Mathlib.Order.Filter.Extr
IsMinFilter.bicomp_mono : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type x} [inst : Preorder β] [inst_1 : Preorder γ] {f : α → β}
  {l : Filter α} {a : α} [inst_2 : Preorder δ] {op : β → γ → δ},
  Relator.LiftFun (fun x1 x2 => x1 ≤ x2) (Relator.LiftFun (fun x1 x2 => x1 ≤ x2) fun x1 x2 => x1 ≤ x2) op op →
    IsMinFilter f l a → ∀ {g : α → γ}, IsMinFilter g l a → IsMinFilter (fun x => op (f x) (g x)) l a
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.SemiCartesianMonoidalCategory.instUniqueHomTensorUnit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.SemiCartesianMonoidalCategory C] →
      (X : C) → Unique (X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.theta_eq_sum_primesLE_log : ∀ (n : ℕ), Chebyshev.theta ↑n = ∑ p ∈ n.primesLE, Real.log ↑p
-- Mathlib.Analysis.SpecialFunctions.PolarCoord
Complex.polarCoord_apply : ∀ (a : ℂ), ↑Complex.polarCoord a = (‖a‖, a.arg)
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.vars_rename : ∀ {R : Type u} {σ : Type u_1} {τ : Type u_2} [inst : CommSemiring R] [inst_1 : DecidableEq τ] (f : σ → τ)
  (φ : MvPolynomial σ R), ((MvPolynomial.rename f) φ).vars ⊆ Finset.image f φ.vars
-- Init.Data.String.Lemmas.Iterate
_private.Init.Data.String.Lemmas.Iterate.0.String.Model.positionsFrom.eq_def : ∀ {s : String} (p : s.Pos),
  String.Model.positionsFrom p = if h : p.IsAtEnd then [] else ⟨p, h⟩ :: String.Model.positionsFrom (p.next h)
-- Mathlib.Probability.Process.Predictable
MeasureTheory.measurableSpace_le_predictable_of_measurableSet : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] [inst_1 : OrderBot ι]
  {𝓕 : MeasureTheory.Filtration ι m} {m' : MeasurableSpace (ι × Ω)},
  (∀ (A : Set Ω), MeasurableSet A → MeasurableSet ({⊥} ×ˢ A)) →
    (∀ (i : ι) (A : Set Ω), MeasurableSet A → MeasurableSet (Set.Ioi i ×ˢ A)) → 𝓕.predictable ≤ m'
-- Init.Prelude
/-- Natural numbers less than some upper bound.

In particular, a `Fin n` is a natural number `i` with the constraint that `i < n`. It is the
canonical type with `n` elements.
 -/
Fin : ℕ → Type
-- Init.Data.BitVec.Lemmas
BitVec.toInt_rotateRight : ∀ {w : ℕ} {x : BitVec w} {r : ℕ},
  (x.rotateRight r).toInt = (↑((x >>> (r % w)).toNat ||| (x <<< (w - r % w)).toNat)).bmod (2 ^ w)
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.fun_comp : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {N : Type u_3} [inst_1 : Zero N] {g : M → N} {f : α → M},
  Function.HasFiniteSupport f → g 0 = 0 → Function.HasFiniteSupport fun a => g (f a)
-- Mathlib.RingTheory.Localization.AtPrime.Basic
Localization.AtPrime.instIsScalarTowerOfIsLiesOverAlgebra : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_4} {B : Type u_5} [inst_1 : CommSemiring A]
  [inst_2 : CommSemiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B]
  (p : Ideal A) [inst_7 : p.IsPrime] (P : Ideal B) [inst_8 : P.IsPrime] [inst_9 : P.LiesOver p]
  [inst_10 : Algebra (Localization.AtPrime p) (Localization.AtPrime P)] [Localization.AtPrime.IsLiesOverAlgebra p P],
  IsScalarTower R (Localization.AtPrime p) (Localization.AtPrime P)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
Real.Angle.two_nsmul_neg_pi_div_two : 2 • ↑(-Real.pi / 2) = ↑Real.pi
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Basic
CategoryTheory.Limits.combineCones_pt_obj : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} J]
  {K : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} K]
  (F : CategoryTheory.Functor J (CategoryTheory.Functor K C))
  (c : (k : K) → CategoryTheory.Limits.LimitCone (F.flip.obj k)) (k : K),
  (CategoryTheory.Limits.combineCones F c).pt.obj k = (c k).cone.pt
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_rco_add_succ_right_eq_push : ∀ {m n : ℕ}, (m...m + n + 1).toArray = (m...m + n).toArray.push (m + n)
-- Mathlib.Algebra.Algebra.Unitization
Unitization.toProd_injective : ∀ {R : Type u_1} {A : Type u_2}, Function.Injective Unitization.toProd
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isLittleO_const_mul_right_iff' : ∀ {α : Type u_1} {E : Type u_3} {R : Type u_13} [inst : Norm E] [inst_1 : SeminormedRing R] {f : α → E} {l : Filter α}
  {g : α → R} {c : R}, IsUnit c → ((f =o[l] fun x => c * g x) ↔ f =o[l] g)
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.lpNorm_natCast_mul : ∀ {α : Type u_1} {m : MeasurableSpace α} {𝕜 : Type u_3} [inst : NormedField 𝕜] [NormedSpace ℝ 𝕜] (n : ℕ) (f : α → 𝕜)
  (p : ENNReal) (μ : MeasureTheory.Measure α), MeasureTheory.lpNorm (↑n * f) p μ = ↑n * MeasureTheory.lpNorm f p μ
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Generators.cotangentRestrict_mk : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {ι : Type w}
  (P : Algebra.Generators R S ι) {σ : Type u_1} {u : σ → ι} (hu : Function.Injective u) (x : ↥P.ker),
  ⇑((P.cotangentRestrict hu) (Algebra.Extension.Cotangent.mk x)) = fun j =>
    (MvPolynomial.aeval P.val) ((MvPolynomial.pderiv (u j)) ↑x)
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.Red.sizeof_of_step : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeGroup.Red.Step L₁ L₂ → sizeOf L₂ < sizeOf L₁
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.instContinuousSMul : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] [inst_7 : IsTopologicalAddGroup F] [inst_8 : ContinuousSMul 𝕜 F],
  ContinuousSMul 𝕜 (E [⋀^ι]→L[𝕜] F)
-- Mathlib.Algebra.Module.Projective
Module.instProjectiveULift : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_3} [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Projective R M], Module.Projective R (ULift.{w, u_3} M)
-- Mathlib.Order.Monotone.Basic
Nat.pow_monotoneOn : MonotoneOn (fun p => p.1 ^ p.2) {p | p.1 ≠ 0}
-- Batteries.Recycling.RBTree.Alter
_private.Batteries.Recycling.RBTree.Alter.0.RBTree.RBNode.alter.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (y : α) → motive (some y)),
  (match none with
    | none => h_1 ()
    | some y => h_2 y) =
    h_1 ()
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.HoCat.homEquivLeft_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C] {X Y : C}
  [inst_2 : HomotopicalAlgebra.IsCofibrant X] [inst_3 : HomotopicalAlgebra.IsCofibrant Y]
  [inst_4 : HomotopicalAlgebra.IsFibrant X] [inst_5 : HomotopicalAlgebra.IsFibrant Y] (f : X ⟶ Y),
  HomotopicalAlgebra.BifibrantObject.HoCat.homEquivRight.symm
      (HomotopicalAlgebra.BifibrantObject.toHoCat.map (HomotopicalAlgebra.BifibrantObject.homMk f)) =
    HomotopicalAlgebra.RightHomotopyClass.mk f
-- Batteries.Data.Array.Match
/-- Make prefix table from a pattern stream  -/
Array.mkPrefixTableOfStream : {α : Type u_1} → {σ : Type u_2} → [BEq α] → [Std.Stream σ α] → σ → Array.PrefixTable α
-- Mathlib.Geometry.Manifold.StructureGroupoid
instInfSetStructureGroupoid : {H : Type u_1} → [inst : TopologicalSpace H] → InfSet (StructureGroupoid H)
-- Mathlib.Algebra.Ring.Regular
/-- Left `Mul` by a `k : α` over `[Ring α]` is injective, if `k` is not a zero divisor.
The typeclass that restricts all terms of `α` to have this property is `NoZeroDivisors`.  -/
isLeftRegular_of_non_zero_divisor : ∀ {α : Type u_1} [inst : NonUnitalNonAssocRing α] (k : α), (∀ (x : α), k * x = 0 → x = 0) → IsLeftRegular k
-- Mathlib.GroupTheory.QuotientGroup.Defs
QuotientGroup.eq_iff_div_mem : ∀ {G : Type u_1} [inst : Group G] {N : Subgroup G} [nN : N.Normal] {x y : G}, ↑x = ↑y ↔ x / y ∈ N
-- Mathlib.Algebra.Homology.ShortComplex.Homology
CategoryTheory.ShortComplex.HomologyMapData.unop_right : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ : CategoryTheory.ShortComplex Cᵒᵖ} {φ : S₁ ⟶ S₂} {h₁ : S₁.HomologyData} {h₂ : S₂.HomologyData}
  (ψ : CategoryTheory.ShortComplex.HomologyMapData φ h₁ h₂), ψ.unop.right = ψ.left.unop
-- Mathlib.Order.BooleanAlgebra.Defs
BooleanAlgebra.toBot : {α : Type u} → [self : BooleanAlgebra α] → Bot α
-- Mathlib.Algebra.Order.Pi
/-- The product of a family of canonically ordered additive monoids is
a canonically ordered additive monoid.  -/
Pi.instCanonicallyOrderedAddForall : ∀ {ι : Type u_6} {Z : ι → Type u_7} [inst : (i : ι) → AddMonoid (Z i)] [inst_1 : (i : ι) → PartialOrder (Z i)]
  [∀ (i : ι), CanonicallyOrderedAdd (Z i)], CanonicallyOrderedAdd ((i : ι) → Z i)
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.MulticospanShape.mk.injEq : ∀ (L : Type w) (R : Type w') (fst snd : R → L) (L_1 : Type w) (R_1 : Type w') (fst_1 snd_1 : R_1 → L_1),
  ({ L := L, R := R, fst := fst, snd := snd } = { L := L_1, R := R_1, fst := fst_1, snd := snd_1 }) =
    (L = L_1 ∧ R = R_1 ∧ fst ≍ fst_1 ∧ snd ≍ snd_1)
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
/-- `S` acts on Hom(S, M) by `s • g = x ↦ g (x • s)`, this action defines an `S`-module structure on
Hom(S, M).
 -/
ModuleCat.CoextendScalars.isModule : {R : Type u₁} →
  {S : Type u₂} →
    [inst : Ring R] →
      [inst_1 : Ring S] →
        (f : R →+* S) →
          (M : Type v) →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : Module R M] → Module S (↑((ModuleCat.restrictScalars f).obj (ModuleCat.of S S)) →ₗ[R] M)
-- Mathlib.Data.Set.Prod
Set.pi_univ_ite : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Set ι) [inst : DecidablePred fun x => x ∈ s] (t : (i : ι) → Set (α i)),
  (Set.univ.pi fun i => if i ∈ s then t i else Set.univ) = s.pi t
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.instNegHom : {M N : AddCommGrpCat} → Neg (M ⟶ N)
-- Mathlib.Algebra.MonoidAlgebra.Degree
/-- An element `f : R[A]` is monic if its leading coefficient is one.  -/
AddMonoidAlgebra.Monic : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_5} →
      [inst : Semiring R] →
        [inst_1 : LinearOrder B] → [OrderBot B] → (A → B) → [Nonempty A] → AddMonoidAlgebra R A → Prop
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
/-- If `M` is canonically ordered, then the `weightedHomogeneousComponent` of weighted degree `0`
of a polynomial is its constant coefficient.  -/
MvPolynomial.weightedHomogeneousComponent_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : PartialOrder M] {w : σ → M} (φ : MvPolynomial σ R) [CanonicallyOrderedAdd M] [IsAddTorsionFree M],
  (∀ (i : σ), w i ≠ 0) → (MvPolynomial.weightedHomogeneousComponent w 0) φ = MvPolynomial.C (MvPolynomial.coeff 0 φ)
-- Init.Coe
CoeFun.mk : {α : Sort u} → {γ : outParam (α → Sort v)} → ((f : α) → γ f) → CoeFun α γ
-- Mathlib.CategoryTheory.MarkovCategory.Basic
/-- There is a unique morphism to the unit (it is terminal).  -/
CategoryTheory.MarkovCategory.instSubsingletonHomTensorUnit : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [CategoryTheory.MarkovCategory C] (X : C), Subsingleton (X ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit C)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.Iter.forIn_mapWithPostcondition : ∀ {α β β₂ γ : Type w} [inst : Std.Iterator α Id β] {ps : Std.Do.PostShape} {n : Type w → Type u_1}
  {o : Type w → Type u_2} [inst_1 : Monad n] [LawfulMonad n] [inst_3 : Monad o] [LawfulMonad o]
  [inst_5 : Std.Do.WPMonad o ps] [inst_6 : MonadLiftT n o] [LawfulMonadLiftT n o] [Std.Iterators.Finite α Id]
  [inst_9 : Std.IteratorLoop α Id o] [Std.LawfulIteratorLoop α Id o] {it : Std.Iter β}
  {f : β → Std.Iterators.PostconditionT n β₂} {init : γ} {g : β₂ → γ → o (ForInStep γ)} {P : Std.Do.Assertion ps}
  {Q : Std.Do.PostCond γ ps},
  ⦃P⦄
      forIn it init fun out acc => do
        let __do_lift ← liftM (f out).run
        g __do_lift acc ⦃Q⦄ →
    ⦃P⦄ forIn (Std.Iter.mapWithPostcondition f it) init g ⦃Q⦄
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.pure_imp_2 : ∀ {σs : List (Type u)} {φ₁ φ₂ : Prop}, ⌜φ₁ → φ₂⌝ ⊢ₛ ⌜φ₁⌝ → ⌜φ₂⌝
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
/-- Any morphism `Y ⟶ Z` is part of a distinguished triangle `X ⟶ Y ⟶ Z ⟶ X⟦1⟧`  -/
CategoryTheory.Pretriangulated.distinguished_cocone_triangle₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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] [hC : CategoryTheory.Pretriangulated C] {Y Z : C}
  (g : Y ⟶ Z),
  ∃ X f h, CategoryTheory.Pretriangulated.Triangle.mk f g h ∈ CategoryTheory.Pretriangulated.distinguishedTriangles
-- Mathlib.Algebra.CubicDiscriminant
Cubic.map.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring R] [inst_1 : Semiring S] (φ : R →+* S) (P : Cubic R),
  Cubic.map φ P = { a := φ P.a, b := φ P.b, c := φ P.c, d := φ P.d }
-- Mathlib.GroupTheory.OreLocalization.Basic
AddOreLocalization.zero.eq_1 : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] [inst_3 : Zero X], AddOreLocalization.zero = 0 -ₒ 0
-- Init.Meta
/-- `simp_arith` has been deprecated. It was a shorthand for `simp +arith +decide`.
Note that `+decide` is not needed for reducing arithmetic terms since simprocs have been added to Lean.
 -/
Lean.Parser.Tactic.simpArith : Lean.ParserDescr
-- Std.Data.HashSet.Lemmas
Std.HashSet.getD_diff_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k fallback : α},
  k ∉ m₂ → (m₁ \ m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Algebra.Group.End
Equiv.inv_mulRight : ∀ {α : Type u_4} [inst : Group α] (a : α), (Equiv.mulRight a)⁻¹ = Equiv.mulRight a⁻¹
-- Batteries.Data.BinomialHeap.Lemmas
Batteries.BinomialHeap.Imp.Heap.WF.size_eq : ∀ {α : Type u_1} {le : α → α → Bool} {n : ℕ} {s : Batteries.BinomialHeap.Imp.Heap α},
  Batteries.BinomialHeap.Imp.Heap.WF le n s → s.size = s.realSize
-- Mathlib.Algebra.Group.Prod
Prod.instSubsingletonAddUnits : ∀ {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst_1 : AddMonoid N] [Subsingleton (AddUnits M)]
  [Subsingleton (AddUnits N)], Subsingleton (AddUnits (M × N))
-- Mathlib.Algebra.Order.CompleteField
/-- **Alias** of `ConditionallyCompleteLinearOrderedField.inducedMap_nonneg`. -/
LinearOrderedField.inducedMap_nonneg : ∀ {α : Type u_2} {β : Type u_3} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] [inst_3 : Field β]
  [inst_4 : ConditionallyCompleteLinearOrder β] [IsStrictOrderedRing β] [Archimedean α] {a : α},
  0 ≤ a → 0 ≤ ConditionallyCompleteLinearOrderedField.inducedMap α β a
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.Compacts.map_id : ∀ {α : Type u_1} [inst : TopologicalSpace α] (K : TopologicalSpace.Compacts α), TopologicalSpace.Compacts.map id ⋯ K = K
-- Mathlib.GroupTheory.OrderOfElement
mem_powers_iff_mem_range_orderOf : ∀ {G : Type u_1} [inst : LeftCancelMonoid G] [Finite G] {x y : G} [inst_2 : DecidableEq G],
  y ∈ Submonoid.powers x ↔ y ∈ Finset.image (fun x_1 => x ^ x_1) (Finset.range (orderOf x))
-- Mathlib.Combinatorics.Matroid.Dual
Matroid.base_iff_dual_isBase_compl : ∀ {α : Type u_1} {M : Matroid α} {B : Set α},
  autoParam (B ⊆ M.E) Matroid.base_iff_dual_isBase_compl._auto_1 → (M.IsBase B ↔ M✶.IsBase (M.E \ B))
-- Mathlib.Data.Stream.Init
Stream'.composition : ∀ {α : Type u} {β : Type v} {δ : Type w} (g : Stream' (β → δ)) (f : Stream' (α → β)) (s : Stream' α),
  Stream'.pure Function.comp ⊛ g ⊛ f ⊛ s = g ⊛ (f ⊛ s)
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.intercalateTR.match_1.eq_1 : ∀ {α : Type u_1} (motive : List (List α) → Sort u_2) (h_1 : Unit → motive []) (h_2 : (x : List α) → motive [x])
  (h_3 : (x : List α) → (xs : List (List α)) → motive (x :: xs)),
  (match [] with
    | [] => h_1 ()
    | [x] => h_2 x
    | x :: xs => h_3 x xs) =
    h_1 ()
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.ι_colimitIsoOfIsLeftKanExtension_inv : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (F' : CategoryTheory.Functor D H) {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor C H}
  (α : F ⟶ L.comp F') [inst_3 : F'.IsLeftKanExtension α] [inst_4 : CategoryTheory.Limits.HasColimit F]
  [inst_5 : CategoryTheory.Limits.HasColimit F'] (i : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι F i) (F'.colimitIsoOfIsLeftKanExtension α).inv =
    CategoryTheory.CategoryStruct.comp (α.app i) (CategoryTheory.Limits.colimit.ι F' (L.obj i))