mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.GroupTheory.OrderOfElement
/-- If each prime factor of `orderOf y` has higher multiplicity in `orderOf x`, and `x` commutes
with `y`, then `x * y` has the same order as `x`.  -/
Commute.orderOf_mul_eq_left_of_forall_prime_mul_dvd : ∀ {G : Type u_1} [inst : Monoid G] {x y : G},
  Commute x y →
    IsOfFinOrder x → (∀ (p : ℕ), Nat.Prime p → p ∣ orderOf y → p * orderOf y ∣ orderOf x) → orderOf (x * y) = orderOf x
-- Init.Simproc
/-- A user-defined simplification procedure declaration. To activate this procedure in `simp` tactic,
we must provide it as an argument, or use the command `attribute` to set its `[simproc]` attribute.
 -/
Lean.Parser.«command_Simproc_decl_(_):=_» : Lean.ParserDescr
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.one_def : ∀ {k : Type u_1} {G : Type u_2} [inst : One G] [inst_1 : AddMonoidWithOne k], 1 = SkewMonoidAlgebra.single 1 1
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
ENNReal.rpow_intCast : ∀ (x : ENNReal) (n : ℤ), x ^ ↑n = x ^ n
-- Mathlib.AlgebraicGeometry.Morphisms.Etale
AlgebraicGeometry.Etale.instSmoothOfRelativeDimensionOfNatNat : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.Etale f],
  AlgebraicGeometry.SmoothOfRelativeDimension 0 f
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.prodFunctor_obj : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {D : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D] (FG : CategoryTheory.Functor A B × CategoryTheory.Functor C D),
  CategoryTheory.prodFunctor.obj FG = FG.1.prod FG.2
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.contains_insert : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k a : α}
  {v : β k}, (t.insert k v).contains a = (cmp k a == Ordering.eq || t.contains a)
-- Init.WF
PSigma.revLexAccessible : ∀ {α : Sort u} {β : Sort v} {r : α → α → Prop} {s : β → β → Prop} {b : β},
  Acc s b → (∀ (a : α), Acc r a) → ∀ (a : α), Acc (PSigma.RevLex r s) ⟨a, b⟩
-- Mathlib.Algebra.Lie.OfAssociative
LieModule.IsFaithful.injective_toEnd : ∀ {R : Type u} {L : Type v} {M : Type w} {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}
  [self : LieModule.IsFaithful R L M], Function.Injective ⇑(LieModule.toEnd R L M)
-- Mathlib.Topology.MetricSpace.Infsep
Set.Subsingleton.einfsep : ∀ {α : Type u_1} [inst : EDist α] {s : Set α}, s.Subsingleton → s.einfsep = ⊤
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Array
_private.Std.Data.Iterators.Lemmas.Producers.Monadic.Array.0.Std.Types.ListIterator.stepAsHetT_iterM.match_1.eq_2 : ∀ {β : Type u_1} (motive : List β → Sort u_2) (x : β) (xs : List β) (h_1 : Unit → motive [])
  (h_2 : (x : β) → (xs : List β) → motive (x :: xs)),
  (match x :: xs with
    | [] => h_1 ()
    | x :: xs => h_2 x xs) =
    h_2 x xs
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Option.getD.match_1.eq_2 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (h_1 : (x : α) → motive (some x)) (h_2 : Unit → motive none),
  (match none with
    | some x => h_1 x
    | none => h_2 ()) =
    h_2 ()
-- Lean.Server.FileWorker.SemanticHighlighting
Lean.Server.FileWorker.AbsoluteLspSemanticToken.mk.injEq : ∀ (pos tailPos : Lean.Lsp.Position) (type : Lean.Lsp.SemanticTokenType) (priority : ℕ)
  (pos_1 tailPos_1 : Lean.Lsp.Position) (type_1 : Lean.Lsp.SemanticTokenType) (priority_1 : ℕ),
  ({ pos := pos, tailPos := tailPos, type := type, priority := priority } =
      { pos := pos_1, tailPos := tailPos_1, type := type_1, priority := priority_1 }) =
    (pos = pos_1 ∧ tailPos = tailPos_1 ∧ type = type_1 ∧ priority = priority_1)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.getD_eq_getValueCastD : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [instBEq : BEq α] [inst_1 : Std.LawfulBEqOrd α] [Std.TransOrd α]
  [inst_3 : Std.LawfulEqOrd α] {k : α} {t : Std.DTreeMap.Internal.Impl α β} {fallback : β k},
  t.Ordered → t.getD k fallback = Std.Internal.List.getValueCastD k t.toListModel fallback
-- Std.Data.Iterators.Lemmas.Producers.Vector
Vector.iter_equiv_iter_toList : ∀ {n : ℕ} {α : Type w} {xs : Vector α n}, xs.iter.Equiv xs.toList.iter
-- Mathlib.NumberTheory.MulChar.Basic
/-- **Alias** of `MulChar.domRestrictHom`.

---

The restriction of a `MulChar` to a submonoid as an homomorphism.
 -/
MulChar.restrictHom : {R : Type u_1} →
  [inst : CommMonoid R] →
    {S : Type u_3} →
      [inst_1 : SetLike S R] →
        [inst_2 : SubmonoidClass S R] →
          (T : S) → (R'' : Type u_4) → [inst_3 : CommMonoidWithZero R''] → MulChar R R'' →* MulChar (↥T) R''
-- Mathlib.AlgebraicGeometry.Cover.Over
AlgebraicGeometry.Scheme.Cover.Over.isOver_map : ∀ {S : AlgebraicGeometry.Scheme} {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme}
  {inst : P.IsStableUnderBaseChange} {inst_1 : AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving P}
  {X : AlgebraicGeometry.Scheme} {inst_2 : X.Over S}
  {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X}
  [self : AlgebraicGeometry.Scheme.Cover.Over S 𝒰] (j : 𝒰.I₀), AlgebraicGeometry.Scheme.Hom.IsOver (𝒰.f j) S
-- Mathlib.Algebra.Polynomial.Div
_private.Mathlib.Algebra.Polynomial.Div.0.Polynomial.divModByMonicAux.match_1.splitter : {R : Type u_1} →
  [inst : Ring R] →
    (motive : Polynomial R → (x : Polynomial R) → x.Monic → Sort u_2) →
      (x x_1 : Polynomial R) →
        (x_2 : x_1.Monic) → ((p q : Polynomial R) → (hq : q.Monic) → motive p q hq) → motive x x_1 x_2
-- Mathlib.CategoryTheory.MorphismProperty.Limits
/-- `P.universally` holds for a morphism `f : X ⟶ Y` iff `P` holds for all `X ×[Y] Y' ⟶ Y'`.  -/
CategoryTheory.MorphismProperty.universally : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.MorphismProperty C → CategoryTheory.MorphismProperty C
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.IsPlausibleStep.outerSkip : ∀ {α α₂ β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m (Std.IterM m β)] [inst_1 : Std.Iterator α₂ m β]
  {it₁ it₁' : Std.IterM m (Std.IterM m β)},
  it₁.IsPlausibleStep (Std.IterStep.skip it₁') →
    Std.Iterators.Types.Flatten.IsPlausibleStep { internalState := { it₁ := it₁, it₂ := none } }
      (Std.IterStep.skip { internalState := { it₁ := it₁', it₂ := none } })
-- Mathlib.FieldTheory.IsAlgClosed.AlgebraicClosure
AlgebraicClosure.finEquivRoots.congr_simp : ∀ {k : Type u} [inst : Field k] {K : Type u_1} [inst_1 : Field K] [inst_2 : DecidableEq K] {i : k →+* K}
  {f : AlgebraicClosure.Monics k} (hf : (Polynomial.map i ↑f).Splits),
  AlgebraicClosure.finEquivRoots hf = AlgebraicClosure.finEquivRoots hf
-- Mathlib.CategoryTheory.Triangulated.Opposite.OpOp
CategoryTheory.Pretriangulated.instIsTriangulatedOppositeUnopUnop : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Limits.HasZeroObject C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C],
  (CategoryTheory.unopUnop C).IsTriangulated
-- Mathlib.Algebra.Group.Action.Pretransitive
/-- There is `g` such that `g +ᵥ x = y`.  -/
AddAction.IsPretransitive.exists_vadd_eq : ∀ {M : Type u_5} {α : Type u_6} {inst : VAdd M α} [self : AddAction.IsPretransitive M α] (x y : α), ∃ g, g +ᵥ x = y
-- Mathlib.Topology.Spectral.Prespectral
/-- Let `f : X → Y` be an open embedding of topological spaces.
If `Y` is a prespectral space (i.e., the quasi-compact opens of `Y` form a basis),
then `X` is also a prespectral space.  -/
Topology.IsOpenEmbedding.prespectralSpace : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [PrespectralSpace Y]
  {f : X → Y}, Topology.IsOpenEmbedding f → PrespectralSpace X
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
BoundedContinuousFunction.toLp_inj : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} (μ : MeasureTheory.Measure α)
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] [inst_4 : MeasureTheory.IsFiniteMeasure μ] {𝕜 : Type u_3}
  [inst_5 : Fact (1 ≤ p)] [inst_6 : NormedRing 𝕜] [inst_7 : Module 𝕜 E] [inst_8 : IsBoundedSMul 𝕜 E]
  {f g : BoundedContinuousFunction α E} [μ.IsOpenPosMeasure],
  (BoundedContinuousFunction.toLp p μ 𝕜) f = (BoundedContinuousFunction.toLp p μ 𝕜) g ↔ f = g
-- Lean.Meta.Tactic.UnifyEq
Lean.Meta.UnifyEqResult.mk.injEq : ∀ (mvarId : Lean.MVarId) (subst : Lean.Meta.FVarSubst) (numNewEqs : ℕ) (mvarId_1 : Lean.MVarId)
  (subst_1 : Lean.Meta.FVarSubst) (numNewEqs_1 : ℕ),
  ({ mvarId := mvarId, subst := subst, numNewEqs := numNewEqs } =
      { mvarId := mvarId_1, subst := subst_1, numNewEqs := numNewEqs_1 }) =
    (mvarId = mvarId_1 ∧ subst = subst_1 ∧ numNewEqs = numNewEqs_1)
-- Init.Data.Array.Lemmas
Array.size_zip : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {ys : Array β}, (xs.zip ys).size = min xs.size ys.size
-- Mathlib.Algebra.Homology.Factorizations.CM5a
_private.Mathlib.Algebra.Homology.Factorizations.CM5a.0.CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.instMonoFHomologyShortComplexOfHomologyMapInt : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {K L : CochainComplex C ℤ} (f : K ⟶ L) [inst_2 : CategoryTheory.EnoughInjectives C] (n : ℤ)
  [CategoryTheory.Mono (HomologicalComplex.homologyMap f n)],
  CategoryTheory.Mono (CochainComplex.Plus.modelCategoryQuillen.cm5a_cof.step₂.homologyShortComplex✝ f n).f
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Real.strictMonoOn_arcsin : StrictMonoOn Real.arcsin (Set.Icc (-1) 1)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.zsmul_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (n : ℤ) (f : M₁ ⟶ M₂) (X : Cᵒᵖ), (n • f).app X = n • f.app X
-- Mathlib.Algebra.Ring.Defs
mul_ite_zero : ∀ {α : Type u} [inst : MulZeroClass α] (P : Prop) [inst_1 : Decidable P] (a b : α),
  (a * if P then b else 0) = if P then a * b else 0
-- Mathlib.MeasureTheory.MeasurableSpace.Basic
MeasurableSpace.le_map_comap : ∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {g : β → α},
  m ≤ MeasurableSpace.map g (MeasurableSpace.comap g m)
-- Batteries.Data.String.Lemmas
String.utf8Len_eq_zero : ∀ {l : List Char}, String.utf8Len l = 0 ↔ l = []
-- Mathlib.Algebra.GroupWithZero.Defs
CommGroupWithZero.toNontrivial : ∀ {G₀ : Type u_2} [self : CommGroupWithZero G₀], Nontrivial G₀
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.L1.SimpleFunc.coe_posPart : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} (f : ↥(α →₁ₛ[μ] ℝ)),
  ↑(MeasureTheory.L1.SimpleFunc.posPart f) = MeasureTheory.Lp.posPart ↑f
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The natural isomorphism `t.truncGELE a b ≅ t.truncLEGE a b`.  -/
CategoryTheory.Triangulated.TStructure.truncGELEIsoLEGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                [CategoryTheory.IsTriangulated C] → (a b : ℤ) → t.truncGELE a b ≅ t.truncLEGE a b
-- Lean.Meta.LazyDiscrTree
/-- This evaluates all lazy entries in a trie and updates `values`, `starIdx`, and `children`
accordingly.
 -/
Lean.Meta.LazyDiscrTree.evalLazyEntries : {α : Type} →
  Array α →
    Lean.Meta.LazyDiscrTree.TrieIndex →
      Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex →
        Array (Lean.Meta.LazyDiscrTree.LazyEntry α) →
          Lean.Meta.LazyDiscrTree.MatchM α
            (Array α ×
              Lean.Meta.LazyDiscrTree.TrieIndex ×
                Std.HashMap Lean.Meta.LazyDiscrTree.Key Lean.Meta.LazyDiscrTree.TrieIndex)
-- Mathlib.RepresentationTheory.Action
MonoidAlgebra.uniqueLinearEquiv.congr_simp : ∀ (R : Type u_1) {S : Type u_2} (M : Type u_3) [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  [inst_3 : One M] [inst_4 : Subsingleton M], MonoidAlgebra.uniqueLinearEquiv R M = MonoidAlgebra.uniqueLinearEquiv R M
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `NonUnitalRing` instance along a surjective function.  -/
Function.Surjective.nonUnitalRing : {R : Type u_1} →
  {S : Type u_2} →
    (f : R → S) →
      Function.Surjective f →
        [inst : Add S] →
          [inst_1 : Mul S] →
            [inst_2 : Zero S] →
              [inst_3 : Neg S] →
                [inst_4 : Sub S] →
                  [inst_5 : SMul ℕ S] →
                    [inst_6 : SMul ℤ S] →
                      [inst_7 : NonUnitalRing R] →
                        f 0 = 0 →
                          (∀ (x y : R), f (x + y) = f x + f y) →
                            (∀ (x y : R), f (x * y) = f x * f y) →
                              (∀ (x : R), f (-x) = -f x) →
                                (∀ (x y : R), f (x - y) = f x - f y) →
                                  (∀ (n : ℕ) (x : R), f (n • x) = n • f x) →
                                    (∀ (n : ℤ) (x : R), f (n • x) = n • f x) → NonUnitalRing S
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.toFun_smul : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} [inst : SMul M β] (c : M) (f : UniformFun α β),
  UniformFun.toFun (c • f) = c • UniformFun.toFun f
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.tacticMvcgen_trivial_extensible : Lean.ParserDescr
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.isEmpty_filterMap_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {γ : Type w} {t : Std.DTreeMap α (fun x => β) cmp}
  [Std.TransCmp cmp] {f : α → β → Option γ},
  (Std.DTreeMap.filterMap f t).isEmpty = true ↔
    ∀ (k : α) (h : k ∈ t), f (t.getKey k h) (Std.DTreeMap.Const.get t k h) = none
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic (2 ^ (k + 1)) K)` (in particular for `K = ℚ`), then the norm of
`ζ ^ (2 ^ k) - 1` is `(-2) ^ (2 ^ k)`.  -/
IsPrimitiveRoot.norm_pow_sub_one_two : ∀ {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L] {k : ℕ},
  IsPrimitiveRoot ζ (2 ^ (k + 1)) →
    ∀ [IsCyclotomicExtension {2 ^ (k + 1)} K L],
      Irreducible (Polynomial.cyclotomic (2 ^ (k + 1)) K) → (Algebra.norm K) (ζ ^ 2 ^ k - 1) = (-2) ^ 2 ^ k
-- Mathlib.ModelTheory.Order
FirstOrder.Language.instIsUniversalPreorderTheory : ∀ (L : FirstOrder.Language) [inst : L.IsOrdered], L.preorderTheory.IsUniversal
-- Mathlib.Algebra.FreeMonoid.Basic
/-- Define an additive action of `FreeAddMonoid α` on `β`.  -/
FreeAddMonoid.mkAddAction : {α : Type u_1} → {β : Type u_2} → (α → β → β) → AddAction (FreeAddMonoid α) β
-- Mathlib.CategoryTheory.Generator.Basic
CategoryTheory.isCoseparator_pi_of_isCoseparator : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [CategoryTheory.Limits.HasZeroMorphisms C] {β : Type w}
  (f : β → C) [inst_2 : CategoryTheory.Limits.HasProduct f] (b : β),
  CategoryTheory.IsCoseparator (f b) → CategoryTheory.IsCoseparator (∏ᶜ f)
-- Mathlib.FieldTheory.PurelyInseparable.Exponent
/-- Action of `iterateFrobeniusₛₗ` on the top field.  -/
IsPurelyInseparable.algebraMap_iterateFrobeniusₛₗ : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : IsPurelyInseparable.HasExponent K L] (p : ℕ) [inst_4 : ExpChar K p] [inst_5 : Field F]
  [inst_6 : Algebra F K] [inst_7 : Algebra F L] [inst_8 : IsScalarTower F K L] [inst_9 : ExpChar F p] {n : ℕ}
  (hn : IsPurelyInseparable.exponent K L ≤ n) (a : L),
  (algebraMap K L) ((IsPurelyInseparable.iterateFrobeniusₛₗ F K L p hn) a) = a ^ p ^ n
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.descend : {α : Type} → {m : Type → Type} → [MonadWithReaderOf Lean.SubExpr m] → Lean.Expr → ℕ → m α → m α
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.instInhabitedAnswer : Inhabited Lean.Meta.SynthInstance.Answer
-- Std.Data.Internal.List.Associative
Std.Internal.List.length_filter_not_contains_eq_length_left : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] {l₁ : List ((a : α) × β a)} {l₂ : List α},
  Std.Internal.List.DistinctKeys l₁ →
    (∀ (a : α), Std.Internal.List.containsKey a l₁ = true → l₂.contains a = false) →
      (List.filter (fun p => !l₂.contains p.fst) l₁).length = l₁.length
-- Mathlib.MeasureTheory.Covering.VitaliFamily
VitaliFamily.mem_filterAt_iff : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m0 : MeasurableSpace X} {μ : MeasureTheory.Measure X}
  (v : VitaliFamily μ) {x : X} {s : Set (Set X)},
  s ∈ v.filterAt x ↔ ∃ ε > 0, ∀ t ∈ v.setsAt x, t ⊆ Metric.closedBall x ε → t ∈ s
-- Mathlib.Analysis.Normed.Ring.InfiniteSum
/-- The Cauchy product formula for the product of two infinite sums indexed by `ℕ`,
expressed by summing on `Finset.antidiagonal`.
See also `tsum_mul_tsum_eq_tsum_sum_antidiagonal` if `f` and `g` are
*not* absolutely summable, and `tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm'`
when the space is not complete.  -/
tsum_mul_tsum_eq_tsum_sum_antidiagonal_of_summable_norm : ∀ {R : Type u_1} [inst : NormedRing R] [CompleteSpace R] {f g : ℕ → R},
  (Summable fun x => ‖f x‖) →
    (Summable fun x => ‖g x‖) →
      (∑' (n : ℕ), f n) * ∑' (n : ℕ), g n = ∑' (n : ℕ), ∑ kl ∈ Finset.HasAntidiagonal.antidiagonal n, f kl.1 * g kl.2
-- Mathlib.NumberTheory.LSeries.SumCoeff
/-- If the partial sums `∑ k ∈ Icc 1 n, ‖f k‖` are `O(n ^ r)` for some real `0 ≤ r`, then the
L-series `LSeries f` converges at `s : ℂ` for all `s` such that `r < s.re`.  -/
LSeriesSummable_of_sum_norm_bigO : ∀ {f : ℕ → ℂ} {r : ℝ} {s : ℂ},
  ((fun n => ∑ k ∈ Finset.Icc 1 n, ‖f k‖) =O[Filter.atTop] fun n => ↑n ^ r) → 0 ≤ r → r < s.re → LSeriesSummable f s
-- Mathlib.CategoryTheory.Monoidal.Types.Basic
CategoryTheory.whiskerLeft_apply : ∀ (X : Type u) {Y Z : Type u} (f : Y ⟶ Z) (p : CategoryTheory.MonoidalCategoryStruct.tensorObj X Y),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X f)) p =
    (p.1, (CategoryTheory.ConcreteCategory.hom f) p.2)
-- Mathlib.Data.Finset.NoncommProd
Multiset.map_noncommSum_aux : ∀ {F : Type u_1} {α : Type u_3} {β : Type u_4} [inst : AddMonoid α] [inst_1 : AddMonoid β] [inst_2 : FunLike F α β]
  [AddHomClass F α β] (s : Multiset α),
  {x | x ∈ s}.Pairwise AddCommute → ∀ (f : F), {x | x ∈ Multiset.map (⇑f) s}.Pairwise AddCommute
-- Mathlib.Algebra.Category.ModuleCat.Images
ModuleCat.imageIsoRange_hom_subtype_assoc : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H) {Z : ModuleCat R} (h : ModuleCat.of R ↑H ⟶ Z),
  CategoryTheory.CategoryStruct.comp (ModuleCat.imageIsoRange f).hom
      (CategoryTheory.CategoryStruct.comp (ModuleCat.ofHom (ModuleCat.Hom.hom f).range.subtype) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.image.ι f) h
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.one_lt_negOnePow_mul_eval_T_real : ∀ {n : ℤ}, n ≠ 0 → ∀ {x : ℝ}, x < -1 → 1 < ↑↑n.negOnePow * Polynomial.eval x (Polynomial.Chebyshev.T ℝ n)
-- Mathlib.Data.Set.Image
Set.nonempty_of_nonempty_preimage : ∀ {α : Type u_1} {β : Type u_2} {s : Set β} {f : α → β}, (f ⁻¹' s).Nonempty → s.Nonempty
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Reverse
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Reverse.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastReverse.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          (motive : aig.RefVec w → Sort u_1) →
            (s : aig.RefVec w) →
              ((refs : Vector Std.Sat.AIG.Fanin w) →
                  (hrefs : ∀ {i : ℕ} (h : i < w), refs[i].gate < aig.decls.size) →
                    motive { refs := refs, hrefs := hrefs }) →
                motive s
-- Batteries.Data.Fin.Lemmas
Fin.isNone_findSomeRev?_iff : ∀ {n : ℕ} {α : Type u_1} {f : Fin n → Option α}, (Fin.findSomeRev? f).isNone = true ↔ ∀ (i : Fin n), (f i).isNone = true
-- Mathlib.InformationTheory.Hamming
hammingDist_comp : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)] {γ : ι → Type u_4}
  [inst_2 : (i : ι) → DecidableEq (γ i)] (f : (i : ι) → γ i → β i) {x y : (i : ι) → γ i},
  (∀ (i : ι), Function.Injective (f i)) → (hammingDist (fun i => f i (x i)) fun i => f i (y i)) = hammingDist x y
-- Mathlib.AlgebraicTopology.SimplicialSet.Boundary
SSet.boundary_obj_eq_univ : ∀ (m n : ℕ),
  autoParam (m < n) SSet.boundary_obj_eq_univ._auto_1 → (SSet.boundary n).obj (Opposite.op { len := m }) = Set.univ
-- Std.Http.Data.URI.Basic
/-- Host component of a URI, supporting domain names and IP addresses.

Reference: https://www.rfc-editor.org/rfc/rfc3986.html#section-3.2.2
 -/
Std.Http.URI.Host : Type
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.RightAngle
/-- An angle in a non-degenerate right-angled triangle is less than `π / 2`, version subtracting
vectors.  -/
InnerProductGeometry.angle_sub_lt_pi_div_two_of_inner_eq_zero : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] {x y : V},
  inner ℝ x y = 0 → x ≠ 0 → InnerProductGeometry.angle x (x - y) < Real.pi / 2
-- Mathlib.Analysis.Calculus.Deriv.Basic
derivWithin.eq_1 : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] (f : 𝕜 → F) (s : Set 𝕜) (x : 𝕜), derivWithin f s x = (fderivWithin 𝕜 f s x) 1
-- Mathlib.Data.Finset.Powerset
Finset.powersetCard_succ_insert : ∀ {α : Type u_1} [inst : DecidableEq α] {x : α} {s : Finset α},
  x ∉ s →
    ∀ (n : ℕ),
      Finset.powersetCard n.succ (insert x s) =
        Finset.powersetCard n.succ s ∪ Finset.image (insert x) (Finset.powersetCard n s)
-- Init.Data.Option.Lemmas
Option.right_lt_of_merge_lt : ∀ {α : Type u_1} [inst : LT α] {f : α → α → α},
  (∀ (a b c : α), f a b < c → b < c) → ∀ {o₁ o₂ o₃ : Option α}, Option.merge f o₁ o₂ < o₃ → o₂ < o₃
-- Lean.Data.Lsp.InitShutdown
Lean.Lsp.LogConfig.mk.injEq : ∀ (logDir? : Option System.FilePath) (allowedMethods? disallowedMethods? : Option (Std.HashSet String))
  (logDir?_1 : Option System.FilePath) (allowedMethods?_1 disallowedMethods?_1 : Option (Std.HashSet String)),
  ({ logDir? := logDir?, allowedMethods? := allowedMethods?, disallowedMethods? := disallowedMethods? } =
      { logDir? := logDir?_1, allowedMethods? := allowedMethods?_1, disallowedMethods? := disallowedMethods?_1 }) =
    (logDir? = logDir?_1 ∧ allowedMethods? = allowedMethods?_1 ∧ disallowedMethods? = disallowedMethods?_1)
-- Mathlib.LinearAlgebra.Finsupp.LinearCombination
/-- A version of `Finsupp.range_linearCombination` which is useful for going in the other
direction  -/
Finsupp.span_eq_range_linearCombination : ∀ {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (s : Set M),
  Submodule.span R s = (Finsupp.linearCombination R Subtype.val).range
-- Mathlib.Data.Set.Image
Set.range_insert : ∀ {α : Type u_1} {β : Type u_2} {x : α} {s : Set α} (f : ↑(insert x s) → β),
  Set.range f = insert (f ⟨x, ⋯⟩) (Set.range fun y => f ⟨↑y, ⋯⟩)
-- Mathlib.Order.SuccPred.Limit
Order.IsPredPrelimit.isMin : ∀ {α : Type u_1} {a : α} [inst : Preorder α] [inst_1 : PredOrder α], Order.IsPredPrelimit (Order.pred a) → IsMin a
-- Mathlib.AlgebraicTopology.DoldKan.Decomposition
AlgebraicTopology.DoldKan.MorphComponents.id_φ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.SimplicialObject C) (n : ℕ),
  (AlgebraicTopology.DoldKan.MorphComponents.id X n).φ =
    CategoryTheory.CategoryStruct.id (X.obj (Opposite.op { len := n + 1 }))