mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.RuleTac.Apply
Aesop.RuleTac.applyExpr : Lean.MVarId →
  Lean.Expr →
    Lean.Term → Option (Array Aesop.Substitution) → Lean.Meta.TransparencyMode → Aesop.BaseM Aesop.RuleTacOutput
-- Mathlib.Data.Complex.Basic
Complex.equivRealProd.eq_1 : Complex.equivRealProd =
  { toFun := fun z => (z.re, z.im), invFun := fun p => { re := p.1, im := p.2 },
    left_inv := Complex.equivRealProd._proof_1, right_inv := Complex.equivRealProd._proof_2 }
-- Mathlib.LinearAlgebra.LinearDisjoint
/-- The `Submodule.LinearDisjoint.not_linearIndependent_pair_of_commute_of_flat_right`
for commutative rings.  -/
Submodule.LinearDisjoint.not_linearIndependent_pair_of_flat_right : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M N : Submodule R S},
  M.LinearDisjoint N → ∀ [Nontrivial R] [Module.Flat R ↥N] (a b : ↥(M ⊓ N)), ¬LinearIndependent R ![a, b]
-- Mathlib.LinearAlgebra.Multilinear.Curry
MultilinearMap.currySum_add : ∀ {R : Type uR} {ι : Type uι} {ι' : Type uι'} {M₂ : Type v₂} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₂]
  [inst_2 : Module R M₂] {N : ι ⊕ ι' → Type u_1} [inst_3 : (i : ι ⊕ ι') → AddCommMonoid (N i)]
  [inst_4 : (i : ι ⊕ ι') → Module R (N i)] (f₁ f₂ : MultilinearMap R N M₂),
  (f₁ + f₂).currySum = f₁.currySum + f₂.currySum
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.dual_coloops : ∀ {α : Type u_1} {M : Matroid α}, M✶.coloops = M.loops
-- Init.Data.Option.Lemmas
Option.toList_none : ∀ (α : Type u_1), none.toList = []
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `neg_lt_neg_iff`. -/
lt_of_neg_lt_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a b : α} [AddRightStrictMono α],
  -a < -b → b < a
-- Init.Notation
/-- `if c then t else e` is notation for `ite c t e`, "if-then-else", which decides to
return `t` or `e` depending on whether `c` is true or false. The explicit argument
`c : Prop` does not have any actual computational content, but there is an additional
`[Decidable c]` argument synthesized by typeclass inference which actually
determines how to evaluate `c` to true or false. Write `if h : c then t else e`
instead for a "dependent if-then-else" `dite`, which allows `t`/`e` to use the fact
that `c` is true/false.
 -/
termIfThenElse : Lean.ParserDescr
-- Init.Notation
/-- The list whose first element is `head`, where `tail` is the rest of the list.
Usually written `head :: tail`.


Conventions for notations in identifiers:

 * The recommended spelling of `::` in identifiers is `cons`. -/
«term_::_» : Lean.TrailingParserDescr
-- Std.Data.DHashMap.RawDef
/-- The number of mappings present in the hash map  -/
Std.DHashMap.Raw.size : {α : Type u} → {β : α → Type v} → Std.DHashMap.Raw α β → ℕ
-- Mathlib.NumberTheory.Cyclotomic.Discriminant
/-- If `p` is a prime and `IsCyclotomicExtension {p ^ (k + 1)} K L`, then the discriminant of
`hζ.powerBasis K` is `(-1) ^ ((p ^ (k + 1).totient) / 2) * p ^ (p ^ k * ((p - 1) * (k + 1) - 1))`
if `Irreducible (cyclotomic (p ^ (k + 1)) K))`, and `p ^ (k + 1) ≠ 2`.  -/
IsCyclotomicExtension.discr_prime_pow_ne_two : ∀ {p k : ℕ} {K : Type u} {L : Type v} {ζ : L} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsCyclotomicExtension {p ^ (k + 1)} K L] [hp : Fact (Nat.Prime p)] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K) →
    p ^ (k + 1) ≠ 2 →
      Algebra.discr K ⇑(IsPrimitiveRoot.powerBasis K hζ).basis =
        (-1) ^ ((p ^ (k + 1)).totient / 2) * ↑p ^ (p ^ k * ((p - 1) * (k + 1) - 1))
-- Mathlib.CategoryTheory.ObjectProperty.Shift
CategoryTheory.ObjectProperty.instCommShiftFullSubcategoryLift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    (P : CategoryTheory.ObjectProperty C) →
      {A : Type u_2} →
        [inst_1 : AddMonoid A] →
          [inst_2 : CategoryTheory.HasShift C A] →
            {E : Type u_3} →
              [inst_3 : CategoryTheory.Category.{v_2, u_3} E] →
                [inst_4 : CategoryTheory.HasShift E A] →
                  [inst_5 : P.IsStableUnderShift A] →
                    (F : CategoryTheory.Functor E C) →
                      (hF : ∀ (X : E), P (F.obj X)) → [F.CommShift A] → (P.lift F hF).CommShift A
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.veblen_opow_eq_opow_iff : ∀ {o a : Ordinal.{u}}, Ordinal.veblen o (Ordinal.omega0 ^ a) = Ordinal.omega0 ^ a ↔ Ordinal.veblen o a = a
-- Lean.Compiler.IR.Basic
Lean.IR.FnBody.sset.sizeOf_spec : ∀ (x : Lean.IR.VarId) (i offset : ℕ) (y : Lean.IR.VarId) (ty : Lean.IR.IRType) (b : Lean.IR.FnBody),
  sizeOf (Lean.IR.FnBody.sset x i offset y ty b) =
    1 + sizeOf x + sizeOf i + sizeOf offset + sizeOf y + sizeOf ty + sizeOf b
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr.0.Std.Tactic.BVDecide.BVExpr.bitblast.go.match_17.eq_6 : ∀ (motive : (w : ℕ) → Std.Tactic.BVDecide.BVExpr w → Sort u_1) (w w_1 n : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w_1)
  (h : w = w_1 * n) (h_1 : (w a : ℕ) → motive w (Std.Tactic.BVDecide.BVExpr.var a))
  (h_2 : (w : ℕ) → (val : BitVec w) → motive w (Std.Tactic.BVDecide.BVExpr.const val))
  (h_3 :
    (w : ℕ) →
      (lhsExpr : Std.Tactic.BVDecide.BVExpr w) →
        (op : Std.Tactic.BVDecide.BVBinOp) →
          (rhsExpr : Std.Tactic.BVDecide.BVExpr w) → motive w (lhsExpr.bin op rhsExpr))
  (h_4 :
    (w : ℕ) →
      (op : Std.Tactic.BVDecide.BVUnOp) →
        (expr : Std.Tactic.BVDecide.BVExpr w) → motive w (Std.Tactic.BVDecide.BVExpr.un op expr))
  (h_5 :
    (w l r : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr l) →
        (rhs : Std.Tactic.BVDecide.BVExpr r) → (h : w = l + r) → motive w (lhs.append rhs h))
  (h_6 :
    (w w_2 n : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w_2) →
        (h : w = w_2 * n) → motive w (Std.Tactic.BVDecide.BVExpr.replicate n expr h))
  (h_7 :
    (len w start : ℕ) →
      (expr : Std.Tactic.BVDecide.BVExpr w) → motive len (Std.Tactic.BVDecide.BVExpr.extract start len expr))
  (h_8 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftLeft rhs))
  (h_9 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.shiftRight rhs))
  (h_10 :
    (w n : ℕ) →
      (lhs : Std.Tactic.BVDecide.BVExpr w) → (rhs : Std.Tactic.BVDecide.BVExpr n) → motive w (lhs.arithShiftRight rhs)),
  (match w, Std.Tactic.BVDecide.BVExpr.replicate n expr h with
    | w, Std.Tactic.BVDecide.BVExpr.var a => h_1 w a
    | w, Std.Tactic.BVDecide.BVExpr.const val => h_2 w val
    | w, lhsExpr.bin op rhsExpr => h_3 w lhsExpr op rhsExpr
    | w, Std.Tactic.BVDecide.BVExpr.un op expr => h_4 w op expr
    | w, lhs.append rhs h => h_5 w l r lhs rhs h
    | w, Std.Tactic.BVDecide.BVExpr.replicate n expr h => h_6 w w_2 n expr h
    | len, Std.Tactic.BVDecide.BVExpr.extract start .(len) expr => h_7 len w start expr
    | w, lhs.shiftLeft rhs => h_8 w n lhs rhs
    | w, lhs.shiftRight rhs => h_9 w n lhs rhs
    | w, lhs.arithShiftRight rhs => h_10 w n lhs rhs) =
    h_6 w w_1 n expr h
-- Mathlib.Algebra.Star.Pointwise
/-- The set `(star s : Set α)` is defined as `{x | star x ∈ s}` in the scope `Pointwise`.
In the usual case where `star` is involutive, it is equal to `{star s | x ∈ s}`, see
`Set.image_star`.  -/
Set.star : {α : Type u_1} → [Star α] → Star (Set α)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.convMul_algHom_single_one : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  [inst_3 : Monoid M] (f g : WithConv (MonoidAlgebra R M →ₐ[R] A)) (x : M),
  (f * g).ofConv (MonoidAlgebra.single x 1) = f.ofConv (MonoidAlgebra.single x 1) * g.ofConv (MonoidAlgebra.single x 1)
-- Mathlib.Order.BooleanSubalgebra
BooleanSubalgebra.map_inf_le : ∀ {α : Type u_2} {β : Type u_3} [inst : BooleanAlgebra α] [inst_1 : BooleanAlgebra β] (L M : BooleanSubalgebra α)
  (f : BoundedLatticeHom α β), BooleanSubalgebra.map f (L ⊓ M) ≤ BooleanSubalgebra.map f L ⊓ BooleanSubalgebra.map f M
-- Mathlib.Algebra.DirectSum.Ring
DirectSum.toSemiring.congr_simp : ∀ {ι : Type u_1} [inst : DecidableEq ι] {A : ι → Type u_2} {R : Type u_3} [inst_1 : (i : ι) → AddCommMonoid (A i)]
  [inst_2 : AddMonoid ι] [inst_3 : DirectSum.GSemiring A] [inst_4 : Semiring R] (f f_1 : (i : ι) → A i →+ R)
  (e_f : f = f_1) (hone : (f 0) GradedMonoid.GOne.one = 1)
  (hmul : ∀ {i j : ι} (ai : A i) (aj : A j), (f (i + j)) (GradedMonoid.GMul.mul ai aj) = (f i) ai * (f j) aj),
  DirectSum.toSemiring f hone hmul = DirectSum.toSemiring f_1 ⋯ ⋯
-- Mathlib.Algebra.Homology.Embedding.IsSupported
HomologicalComplex.IsStrictlySupportedOutside.mk : ∀ {ι : 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'},
  (∀ (i : ι), CategoryTheory.Limits.IsZero (K.X (e.f i))) → K.IsStrictlySupportedOutside e
-- Lean.Meta.Match.SimpH
_private.Lean.Meta.Match.SimpH.0.Lean.Meta.Match.SimpH.State.mk : Lean.MVarId → List Lean.FVarId → List Lean.FVarId → List Lean.FVarId → Lean.Meta.Match.SimpH.State✝
-- Std.Time.Date.Unit.Week
Std.Time.Week.instOfNatOrdinal : {n : ℕ} → OfNat Std.Time.Week.Ordinal n
-- Mathlib.Order.Birkhoff
OrderEmbedding.birkhoffFinset_sup : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : Fintype α] [inst_2 : DecidablePred SupIrred]
  [inst_3 : DecidableEq α] (a b : α),
  OrderEmbedding.birkhoffFinset (a ⊔ b) = OrderEmbedding.birkhoffFinset a ∪ OrderEmbedding.birkhoffFinset b
-- Mathlib.Topology.Algebra.Module.FiniteDimension
LinearMap.coe_toContinuousLinearMap' : ∀ {𝕜 : Type u} [hnorm : NontriviallyNormedField 𝕜] {E : Type v} [inst : AddCommGroup E] [inst_1 : Module 𝕜 E]
  [inst_2 : TopologicalSpace E] [inst_3 : IsTopologicalAddGroup E] [inst_4 : ContinuousSMul 𝕜 E] {F' : Type x}
  [inst_5 : AddCommGroup F'] [inst_6 : Module 𝕜 F'] [inst_7 : TopologicalSpace F'] [inst_8 : IsTopologicalAddGroup F']
  [inst_9 : ContinuousSMul 𝕜 F'] [inst_10 : CompleteSpace 𝕜] [inst_11 : T2Space E] [inst_12 : FiniteDimensional 𝕜 E]
  (f : E →ₗ[𝕜] F'), ⇑(LinearMap.toContinuousLinearMap f) = ⇑f
-- Init.Data.BitVec.Lemmas
BitVec.toInt_lt : ∀ {w : ℕ} {x : BitVec w}, x.toInt < 2 ^ (w - 1)
-- Mathlib.Data.Num.Lemmas
Int.snumCoe : Coe SNum ℤ
-- Lean.Parser.Term
Lean.Parser.Term.pipeCompletion.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.RingTheory.Perfection
PreTilt.valAux_mul : ∀ {K : Type u₁} [inst : Field K] {v : Valuation K NNReal} {O : Type u₂} [inst_1 : CommRing O] [inst_2 : Algebra O K],
  v.Integers O →
    ∀ {p : ℕ} [inst_3 : Fact (Nat.Prime p)] [inst_4 : Fact ¬IsUnit ↑p] (f g : PreTilt O p),
      PreTilt.valAux K v O p (f * g) = PreTilt.valAux K v O p f * PreTilt.valAux K v O p g
-- Lean.Elab.SetOption
/-- Elaborates `id` as an identifier representing an option name with value given by `val`, adding
appropriate info to the infotrees.

Validates that `val` has the correct type for values of the option `id`, and returns the updated
`Options`. Does **not** update the options in the monad `m`.
 -/
Lean.Elab.elabSetOption : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadOptions m] →
      [Lean.MonadError m] →
        [MonadLiftT (EIO Lean.Exception) m] →
          [Lean.Elab.MonadInfoTree m] → Lean.Syntax → Lean.Syntax → m (Lean.Options × Lean.OptionDecl)
-- Std.Time.Date.Unit.Month
Std.Time.Month.instNegOffset : Neg Std.Time.Month.Offset
-- Std.Sync.Mutex
/-- Mutual exclusion primitive (a lock).

If you want to guard shared state, use `Mutex α` instead.
 -/
Std.BaseMutex : Type
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.mem_toArray_iff_getKey?_eq_some_and_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp] {k : α}
  {v : β}, (k, v) ∈ Std.DTreeMap.Const.toArray t ↔ t.getKey? k = some k ∧ Std.DTreeMap.Const.get? t k = some v
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.piFinTwo_symm_apply : ∀ (R : Type u_2) [inst : Semiring R] (M : Fin 2 → Type u_4) [inst_1 : (i : Fin 2) → AddCommMonoid (M i)]
  [inst_2 : (i : Fin 2) → Module R (M i)] [inst_3 : (i : Fin 2) → TopologicalSpace (M i)],
  ⇑(ContinuousLinearEquiv.piFinTwo R M).symm = fun p => Fin.cons p.1 (Fin.cons p.2 finZeroElim)
-- Mathlib.MeasureTheory.Measure.Dirac
/-- Dirac delta measures at two points are equal if and only if the two points are equal,
assuming the measurable space separates points.  -/
MeasureTheory.dirac_eq_dirac_iff : ∀ {α : Type u_1} [inst : MeasurableSpace α] [MeasurableSpace.SeparatesPoints α] {x y : α},
  MeasureTheory.Measure.dirac x = MeasureTheory.Measure.dirac y ↔ x = y
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.allM_filterMap : ∀ {α β β' : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [inst_3 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m] {it : Std.IterM m β}
  {f : β → Option β'} {p : β' → m (ULift.{w, 0} Bool)},
  Std.IterM.allM p (Std.IterM.filterMap f it) =
    Std.IterM.allM
      (fun x =>
        match f x with
        | some fx => p fx
        | none => pure { down := true })
      it
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv_counitIso_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (X : CategoryTheory.Endofunctor.Coalgebra G),
  ((CategoryTheory.Endofunctor.Adjunction.algebraCoalgebraEquiv adj).counitIso.inv.app X).f =
    CategoryTheory.CategoryStruct.id X.V
-- Mathlib.Algebra.Algebra.Unitization
Unitization.inr_star : ∀ {R : Type u_1} {A : Type u_2} [inst : AddMonoid R] [inst_1 : StarAddMonoid R] [inst_2 : Star A] (a : A),
  ↑(star a) = star ↑a
-- Mathlib.Data.Int.Bitwise
Int.shiftLeft_natCast : ∀ (m n : ℕ), ↑m <<< ↑n = ↑(m <<< n)
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The Riemann Zeta Function does not vanish on the half-plane `re s > 1`.  -/
riemannZeta_ne_zero_of_one_lt_re : ∀ {s : ℂ}, 1 < s.re → riemannZeta s ≠ 0
-- Mathlib.RingTheory.DividedPowers.Padic
_private.Mathlib.RingTheory.DividedPowers.Padic.0.PadicInt.dpow'.eq_1 : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (m : ℕ) (x : ℚ_[p]), PadicInt.dpow'✝ p m x = Ring.inverse ↑m.factorial * x ^ m
-- Mathlib.Analysis.Calculus.ContDiff.Defs
/-- An analytic function is automatically `C^ω` in a complete space  -/
AnalyticOn.contDiffOn_of_completeSpace : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {f : E → F} {n : WithTop ℕ∞} [CompleteSpace F], AnalyticOn 𝕜 f s → ContDiffOn 𝕜 n f s
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.add_oreDiv : ∀ {R : Type u_1} [inst : Monoid R] {S : Submonoid R} [inst_1 : OreLocalization.OreSet S] {X : Type u_2}
  [inst_2 : AddMonoid X] [inst_3 : DistribMulAction R X] {r r' : X} {s : ↥S}, r /ₒ s + r' /ₒ s = (r + r') /ₒ s
-- Mathlib.Order.Fin.Tuple
finSuccAboveOrderIso_symm_apply_last : ∀ {n : ℕ} (x : { x // x ≠ Fin.last n }), (finSuccAboveOrderIso (Fin.last n)).symm x = (↑x).castLT ⋯
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.Injective.State.mk : Lean.Meta.Grind.InjectiveTheoremsArray →
  Lean.PHashMap Lean.Meta.Sym.ExprPtr Lean.Meta.Grind.InjectiveInfo → Lean.Meta.Grind.Injective.State
-- Init.Data.Array.Lemmas
Array.getElem?_range : ∀ {n i : ℕ}, (Array.range n)[i]? = if i < n then some i else none
-- Mathlib.Algebra.Homology.SpectralObject.EpiMono
CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp : ∀ {C : Type u_1} {ι' : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : Preorder ι'] (X' : CategoryTheory.Abelian.SpectralObject C ι') (i₀ i₁ i₂ i₃ i₄ i₅ : ι') (hi₀₁ : i₀ ≤ i₁)
  (hi₁₂ : i₁ ≤ i₂) (hi₂₃ : i₂ ≤ i₃) (hi₃₄ : i₃ ≤ i₄) (hi₄₅ : i₄ ≤ i₅) (n₀ n₁ n₂ : ℤ)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.mapFourδ₁Toδ₀'_comp._auto_3),
  CategoryTheory.CategoryStruct.comp (X'.mapFourδ₁Toδ₀' i₀ i₁ i₃ i₄ i₅ hi₀₁ ⋯ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂)
      (X'.mapFourδ₁Toδ₀' i₁ i₂ i₃ i₄ i₅ hi₁₂ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂) =
    X'.mapFourδ₁Toδ₀' i₀ i₂ i₃ i₄ i₅ ⋯ hi₂₃ hi₃₄ hi₄₅ n₀ n₁ n₂ hn₁ hn₂
-- Mathlib.GroupTheory.Perm.List
List.formPerm_eq_one_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (l : List α), l.Nodup → (l.formPerm = 1 ↔ l.length ≤ 1)
-- Mathlib.MeasureTheory.Measure.Prod
/-- The binary product of measures. They are defined for arbitrary measures, but we basically
prove all properties under the assumption that at least one of them is s-finite.  -/
MeasureTheory.Measure.prod : {α : Type u_4} →
  {β : Type u_5} →
    [inst : MeasurableSpace α] →
      [inst_1 : MeasurableSpace β] → MeasureTheory.Measure α → MeasureTheory.Measure β → MeasureTheory.Measure (α × β)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.mk_one : ∀ {M : Type u_1} [inst : Monoid M], Associates.mk 1 = 1
-- Mathlib.CategoryTheory.IsoCat
/-- Composition of isomorphisms of categories.  -/
CategoryTheory.IsoCat.trans : {C : Type u_1} →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            CategoryTheory.IsoCat C D → CategoryTheory.IsoCat D E → CategoryTheory.IsoCat C E
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_isStrictlyPositive_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  (f : R → R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) cfc_isStrictlyPositive_iff._auto_1 →
    autoParam (p a) cfc_isStrictlyPositive_iff._auto_3 → (IsStrictlyPositive (cfc f a) ↔ ∀ x ∈ spectrum R a, 0 < f x)
-- Mathlib.Data.W.Constructions
WType.Natα.succ : WType.Natα
-- Mathlib.Algebra.Group.Submonoid.BigOperators
/-- **Alias** of `SubmonoidClass.coe_finsetProd`. -/
SubmonoidClass.coe_finset_prod : ∀ {B : Type u_3} {S : B} {ι : Type u_4} {M : Type u_5} [inst : CommMonoid M] [inst_1 : SetLike B M]
  [inst_2 : SubmonoidClass B M] (f : ι → ↥S) (s : Finset ι), ↑(∏ i ∈ s, f i) = ∏ i ∈ s, ↑(f i)
-- Mathlib.Algebra.Group.Defs
Group.mk : {G : Type u} → [toDivInvMonoid : DivInvMonoid G] → (∀ (a : G), a⁻¹ * a = 1) → Group G
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.image.isoStrongEpiMono_hom_comp_ι : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasStrongEpiMonoFactorisations C] {X Y : C} {f : X ⟶ Y} {I' : C} (e : X ⟶ I')
  (m : I' ⟶ Y) (comm : CategoryTheory.CategoryStruct.comp e m = f) [inst_2 : CategoryTheory.StrongEpi e]
  [inst_3 : CategoryTheory.Mono m],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.isoStrongEpiMono e m comm).hom
      (CategoryTheory.Limits.image.ι f) =
    m
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.ext_iff : ∀ {R : Type u} {S : Type u₁} [inst : Monoid R] [inst_1 : Monoid S] {φ : R →* S} {A : Type v} {B : Type w}
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : DistribMulAction R A] [inst_4 : NonUnitalNonAssocSemiring B]
  [inst_5 : DistribMulAction S B] {f g : A →ₛₙₐ[φ] B}, f = g ↔ ∀ (x : A), f x = g x
-- Mathlib.CategoryTheory.Monoidal.Category
/-- The left unitor as a natural isomorphism.  -/
CategoryTheory.MonoidalCategory.leftUnitorNatIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      CategoryTheory.MonoidalCategory.tensorUnitLeft C ≅ CategoryTheory.Functor.id C
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_insertList_of_contains_right : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l toInsert : List ((_ : α) × β)} {k : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.DistinctKeys toInsert →
      ∀ (contains : Std.Internal.List.containsKey k toInsert = true)
        {h : Std.Internal.List.containsKey k (Std.Internal.List.insertList l toInsert) = true},
        Std.Internal.List.getValue k (Std.Internal.List.insertList l toInsert) h =
          Std.Internal.List.getValue k toInsert contains
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent
_private.Mathlib.Analysis.SpecialFunctions.Trigonometric.Cotangent.0.iteratedDerivWithin_cotTerm_bounded_uniformly : ∀ {k : ℕ} {K : Set ℂ} (A B : ℝ) (hB : 0 < B),
  K ⊆ UpperHalfPlane.coe '' UpperHalfPlane.verticalStrip A B →
    ∀ (n : ℕ) {a : ℂ},
      a ∈ K →
        ‖iteratedDerivWithin k (fun z => cotTerm z n) UpperHalfPlane.upperHalfPlaneSet a‖ ≤
          cotTermUpperBound✝ k A B hB n
-- Mathlib.Data.Multiset.Bind
Multiset.bind_assoc : ∀ {α : Type u_1} {β : Type v} {γ : Type u_2} {s : Multiset α} {f : α → Multiset β} {g : β → Multiset γ},
  (s.bind f).bind g = s.bind fun a => (f a).bind g
-- Mathlib.Topology.Order.Compact
IsCompact.exists_isLocalMax_mem_open : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIciTopology α] {f : β → α} {s t : Set β} {z : β},
  IsCompact t → s ⊆ t → ContinuousOn f t → z ∈ t → (∀ z' ∈ t \ s, f z' < f z) → IsOpen s → ∃ x ∈ s, IsLocalMax f x
-- Mathlib.Combinatorics.Enumerative.DyckWord
DyckWord.firstReturn_lt_length : ∀ {p : DyckWord}, p ≠ 0 → p.firstReturn < (↑p).length
-- Mathlib.Algebra.Group.TypeTags.Hom
MonoidHom.toAdditive_apply_apply : ∀ {α : Type u_3} {β : Type u_4} [inst : MulOneClass α] [inst_1 : MulOneClass β] (f : α →* β) (a : Additive α),
  (MonoidHom.toAdditive f) a = Additive.ofMul (f (Additive.toMul a))
-- Init.Data.Nat.Gcd
Nat.gcd_add_mul_left_right : ∀ (m n k : ℕ), m.gcd (n + m * k) = m.gcd n
-- Mathlib.Algebra.Category.ModuleCat.Adjunctions
CategoryTheory.Free.lift_map_single : ∀ (R : Type u_1) [inst : CommRing R] {C : Type u} [inst_1 : CategoryTheory.Category.{v, u} C] {D : Type u}
  [inst_2 : CategoryTheory.Category.{v, u} D] [inst_3 : CategoryTheory.Preadditive D]
  [inst_4 : CategoryTheory.Linear R D] (F : CategoryTheory.Functor C D) {X Y : C} (f : X ⟶ Y) (r : R),
  ((CategoryTheory.Free.lift R F).map fun₀ | f => r) = r • F.map f
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- The codomain of the measure that will decrease during the induction in the `C : R → R[X]` case
of Chevalley's theorem with complexity bound.  -/
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.DegreeType : ℕ → Type
-- Mathlib.Combinatorics.Young.YoungDiagram
YoungDiagram.transposeOrderIso_symm_apply : ∀ (μ : YoungDiagram), (RelIso.symm YoungDiagram.transposeOrderIso) μ = μ.transpose
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem_diff : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂)[k] = t₁[k]
-- Mathlib.CategoryTheory.Sums.Associator
CategoryTheory.sum.inlCompAssociator_inv_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (X : C ⊕ D),
  (CategoryTheory.sum.inlCompAssociator C D E).inv.app X =
    CategoryTheory.CategoryStruct.id
      (((CategoryTheory.Sum.inl_ C (D ⊕ E)).sum'
            ((CategoryTheory.Sum.inl_ D E).comp (CategoryTheory.Sum.inr_ C (D ⊕ E)))).obj
        X)
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.flip_w : ∀ (u : PNat.XgcdType), u.flip.w = u.z
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_le : ∀ {a b : UInt16}, a.toUInt8 ≤ b.toUInt8 ↔ a % 256 ≤ b % 256