mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Flip arguments in `f : ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G')` to get
`G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'`  -/
ContinuousMultilinearMap.flipLinear : {𝕜 : Type u} →
  {ι : Type v} →
    {E : ι → Type wE} →
      {G : Type wG} →
        {G' : Type wG'} →
          [inst : NontriviallyNormedField 𝕜] →
            [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
              [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
                [inst_3 : SeminormedAddCommGroup G] →
                  [inst_4 : NormedSpace 𝕜 G] →
                    [inst_5 : SeminormedAddCommGroup G'] →
                      [inst_6 : NormedSpace 𝕜 G'] →
                        [Fintype ι] →
                          ContinuousMultilinearMap 𝕜 E (G →L[𝕜] G') → G →L[𝕜] ContinuousMultilinearMap 𝕜 E G'
-- Mathlib.Algebra.Category.Semigrp.Basic
Semigrp.hom_id : ∀ {X : Semigrp}, Semigrp.Hom.hom (CategoryTheory.CategoryStruct.id X) = MulHom.id ↑X
-- Init.Data.String.Lemmas.FindPos
String.Pos.prev_eq_iff : ∀ {s : String} {p q : s.Pos} {h : p ≠ s.startPos}, p.prev h = q ↔ q < p ∧ ∀ q' < p, q' ≤ q
-- Mathlib.Geometry.Diffeology.Basic
ContDiff.dSmooth : ∀ {X : Type u_1} [inst : DiffeologicalSpace X] {Y : Type u_2} [inst_1 : NormedAddCommGroup X] [inst_2 : NormedSpace ℝ X]
  [Diffeology.IsContDiffCompatible X] [inst_4 : NormedAddCommGroup Y] [inst_5 : NormedSpace ℝ Y]
  [inst_6 : DiffeologicalSpace Y] [Diffeology.IsContDiffCompatible Y] {f : X → Y},
  ContDiff ℝ (↑⊤) f → Diffeology.DSmooth f
-- Mathlib.Algebra.Ring.IsFormallyReal
IsSumNonzeroSq.below : {R : Type u_1} →
  [inst : Mul R] →
    [inst_1 : Add R] →
      [inst_2 : Zero R] → {motive : (a : R) → IsSumNonzeroSq a → Prop} → {a : R} → IsSumNonzeroSq a → Prop
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_zero : ⌈0⌉ₑ = 0
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.congr_symm : ∀ {R : Type uR} {S : Type uS} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD} [inst : CommSemiring R]
  [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A] [inst_5 : Algebra S A]
  [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B] [inst_9 : Semiring C]
  [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C] [inst_13 : Semiring D]
  [inst_14 : Algebra R D] (f : A ≃ₐ[S] C) (g : B ≃ₐ[R] D),
  Algebra.TensorProduct.congr f.symm g.symm = (Algebra.TensorProduct.congr f g).symm
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_insertMany_list_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {l : List (α × β)} {k k' : α},
  (k == k') = true →
    ∀ {v fallback : β},
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l → Std.DHashMap.Const.getD (Std.DHashMap.Const.insertMany m l) k' fallback = v
-- Mathlib.AlgebraicGeometry.Normalization
/-- The inclusion from the structure presheaf of `Y` to the integral closure of `Y` in `X`.  -/
AlgebraicGeometry.Scheme.Hom.normalizationDiagramMap : {X Y : AlgebraicGeometry.Scheme} → (f : X ⟶ Y) → Y.presheaf ⟶ AlgebraicGeometry.Scheme.Hom.normalizationDiagram f
-- Init.Data.Int.Order
Int.sign_nonneg_iff : ∀ {x : ℤ}, 0 ≤ x.sign ↔ 0 ≤ x
-- Mathlib.Topology.Closure
closure_closure : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, closure (closure s) = closure s
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, panicking if the map is
empty.
 -/
Std.ExtDTreeMap.Const.maxEntry! : {α : Type u} →
  {cmp : α → α → Ordering} →
    {β : Type v} → [Std.TransCmp cmp] → [Inhabited (α × β)] → Std.ExtDTreeMap α (fun x => β) cmp → α × β
-- Mathlib.Order.Filter.Interval
Filter.tendsto_Ioo_Iio_Iio : ∀ {α : Type u_1} [inst : Preorder α] {a : α},
  Filter.TendstoIxxClass Set.Ioo (Filter.principal (Set.Iio a)) (Filter.principal (Set.Iio a))
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Isometric
nnnorm_apply_le_nnnorm_cfc : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : outParam (A → Prop)} [inst : RCLike 𝕜] [inst_1 : NormedRing A]
  [inst_2 : StarRing A] [inst_3 : NormedAlgebra 𝕜 A] [inst_4 : IsometricContinuousFunctionalCalculus 𝕜 A p] (f : 𝕜 → 𝕜)
  (a : A) ⦃x : 𝕜⦄,
  x ∈ spectrum 𝕜 a →
    autoParam (ContinuousOn f (spectrum 𝕜 a)) nnnorm_apply_le_nnnorm_cfc._auto_1 →
      autoParam (p a) nnnorm_apply_le_nnnorm_cfc._auto_3 → ‖f x‖₊ ≤ ‖cfc f a‖₊
-- Mathlib.RingTheory.Ideal.Norm.RelNorm
Ideal.relNorm_map_algEquiv : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] {S : Type u_3} [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : IsIntegrallyClosed R] [inst_5 : IsIntegrallyClosed S] [inst_6 : Algebra R S] [inst_7 : Module.Finite R S]
  [inst_8 : Module.IsTorsionFree R S] [inst_9 : IsDedekindDomain R] [inst_10 : IsDedekindDomain S] {T : Type u_4}
  [inst_11 : CommRing T] [inst_12 : IsDedekindDomain T] [inst_13 : IsIntegrallyClosed T] [inst_14 : Algebra R T]
  [inst_15 : Module.Finite R T] [inst_16 : Module.IsTorsionFree R T] (σ : S ≃ₐ[R] T) (I : Ideal S),
  (Ideal.relNorm R) (Ideal.map σ I) = (Ideal.relNorm R) I
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instNeg : {α : Type u_1} → [Neg α] → Neg (Lex α)
-- Mathlib.NumberTheory.ModularForms.SlashInvariantForms
/-- Every `SlashInvariantForm` `f` satisfies ` f (γ • z) = (denom γ z) ^ k * f z`.  -/
SlashInvariantForm.slash_action_eqn'' : ∀ {F : Type u_1} {Γ : Subgroup (GL (Fin 2) ℝ)} [inst : FunLike F UpperHalfPlane ℂ] {k : ℤ} [Γ.HasDetOne]
  [SlashInvariantFormClass F Γ k] (f : F) {γ : GL (Fin 2) ℝ},
  γ ∈ Γ → ∀ (z : UpperHalfPlane), f (γ • z) = UpperHalfPlane.denom γ ↑z ^ k * f z
-- Mathlib.Data.Fintype.EquivFin
Infinite.of_surjective : ∀ {α : Sort u_4} {β : Sort u_5} [Infinite β] (f : α → β), Function.Surjective f → Infinite α
-- Mathlib.GroupTheory.Coset.Defs
QuotientAddGroup.rightRel_eq : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), ⇑(QuotientAddGroup.rightRel s) = fun x y => y + -x ∈ s
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.contains_insertManyIfNewUnit!_list : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} [Std.TransOrd α] [inst : BEq α]
  [Std.LawfulBEqOrd α],
  t.WF →
    ∀ {l : List α} {k : α},
      Std.DTreeMap.Internal.Impl.contains k ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t l) =
        (Std.DTreeMap.Internal.Impl.contains k t || l.contains k)
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- The canonical morphism from `G` applied to the colimit of `F ⋙ G`
to `G` applied to the colimit of `F`.
 -/
CategoryTheory.Limits.colimit.post : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        (F : CategoryTheory.Functor J C) →
          {D : Type u'} →
            [inst_2 : CategoryTheory.Category.{v', u'} D] →
              [inst_3 : CategoryTheory.Limits.HasColimit F] →
                (G : CategoryTheory.Functor C D) →
                  [inst_4 : CategoryTheory.Limits.HasColimit (F.comp G)] →
                    CategoryTheory.Limits.colimit (F.comp G) ⟶ G.obj (CategoryTheory.Limits.colimit F)
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₁ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) {X_1 Y : CategoryTheory.ComposableArrows ι 2} (φ : X_1 ⟶ Y),
  (X.ω₂.map φ).hom₁ = X.ω₁.map (CategoryTheory.ComposableArrows.homMk₁ (φ.app 0) (φ.app 1) ⋯)
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.mk_le_mk_of_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B A₁ A₂ : C} {f₁ : A₁ ⟶ B} {f₂ : A₂ ⟶ B}
  [inst_1 : CategoryTheory.Mono f₁] [inst_2 : CategoryTheory.Mono f₂] (g : A₁ ⟶ A₂),
  CategoryTheory.CategoryStruct.comp g f₂ = f₁ → CategoryTheory.Subobject.mk f₁ ≤ CategoryTheory.Subobject.mk f₂
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.ParameterInformationLabel.range.inj : ∀ {startUtf16Offset endUtf16Offset startUtf16Offset_1 endUtf16Offset_1 : ℕ},
  Lean.Lsp.ParameterInformationLabel.range startUtf16Offset endUtf16Offset =
      Lean.Lsp.ParameterInformationLabel.range startUtf16Offset_1 endUtf16Offset_1 →
    startUtf16Offset = startUtf16Offset_1 ∧ endUtf16Offset = endUtf16Offset_1
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instCommMonoid : {α : Type u_1} → [CommMonoid α] → CommMonoid (Colex α)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.balanceL!.match_5.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr)),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr => h_2 ls lk lv ll lr) =
    h_1 ()
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- The tail of a multiseries, i.e. the last entry of the tuple returned by `destruct`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.tail : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl
-- Mathlib.Data.Fintype.Option
/-- A type is a `Fintype` if its successor (using `Option`) is a `Fintype`.  -/
fintypeOfOptionEquiv : {α : Type u_1} → {β : Type u_2} → [Fintype α] → α ≃ Option β → Fintype β
-- Mathlib.Algebra.Free
FreeAddSemigroup.traverse_pure' : ∀ {α β : Type u} {m : Type u → Type u} [inst : Applicative m] (F : α → m β), traverse F ∘ pure = fun x => pure <$> F x
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
/-- The typeclass saying that `P : ObjectProperty C` is stable under finite products.  -/
CategoryTheory.ObjectProperty.IsClosedUnderFiniteProducts : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.Algebra.Group.Defs
ZPow.mk : {G : Type u} → (ℤ → G → G) → ZPow G
-- Mathlib.Topology.EMetricSpace.Defs
uniformity_basis_edist_le' : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (ε' : ENNReal),
  0 < ε' → (uniformity α).HasBasis (fun ε => ε ∈ Set.Ioo 0 ε') fun ε => {p | edist p.1 p.2 ≤ ε}
-- Mathlib.Probability.Kernel.Disintegration.MeasurableStieltjes
ProbabilityTheory.isMeasurableRatCDF_toRatCDF : ∀ {α : Type u_1} {f : α → ℚ → ℝ} [inst : MeasurableSpace α],
  Measurable f → ProbabilityTheory.IsMeasurableRatCDF (ProbabilityTheory.toRatCDF f)
-- Aesop.Forward.RuleInfo
Aesop.Slot.mk : Option (Array Lean.Meta.DiscrTree.Key) →
  Aesop.SlotIndex →
    Aesop.PremiseIndex →
      Std.HashSet Aesop.PremiseIndex → Std.HashSet Aesop.PremiseIndex → Array Aesop.PremiseIndex → Aesop.Slot
-- Mathlib.RingTheory.Valuation.Integers
/-- The `v.integer`-submodule of `R` of elements whose valuation is less than a certain unit.  -/
Valuation.ltSubmodule : {R : Type u} →
  {Γ₀ : Type v} →
    [inst : Ring R] →
      [inst_1 : LinearOrderedCommGroupWithZero Γ₀] → (v : Valuation R Γ₀) → Γ₀ˣ → Submodule (↥v.integer) R
-- Batteries.Data.List.Lemmas
List.getElem_findIdxs_lt : ∀ {i : ℕ} {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ} (h : i < (List.findIdxs p xs s).length),
  (List.findIdxs p xs s)[i] < xs.length + s
-- Mathlib.Algebra.Field.Defs
/-- Every nonzero element of a group with zero is invertible.  -/
DivisionSemiring.mul_inv_cancel : ∀ {K : Type u_2} [self : DivisionSemiring K] (a : K), a ≠ 0 → a * a⁻¹ = 1
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.map_comp_inr : ∀ {N₁ : Type u_4} {G₁ : Type u_5} {N₂ : Type u_6} {G₂ : Type u_7} [inst : Group N₁] [inst_1 : Group G₁]
  [inst_2 : Group N₂] [inst_3 : Group G₂] {φ₁ : G₁ →* MulAut N₁} {φ₂ : G₂ →* MulAut N₂} (fn : N₁ →* N₂) (fg : G₁ →* G₂)
  (h : ∀ (g : G₁), fn.comp (MulEquiv.toMonoidHom (φ₁ g)) = (MulEquiv.toMonoidHom (φ₂ (fg g))).comp fn),
  (SemidirectProduct.map fn fg h).comp SemidirectProduct.inr = SemidirectProduct.inr.comp fg
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- Extract a slice from a `BitVec`.
 -/
Std.Tactic.BVDecide.BVExpr.extract : {w : ℕ} → ℕ → (len : ℕ) → Std.Tactic.BVDecide.BVExpr w → Std.Tactic.BVDecide.BVExpr len
-- Mathlib.Algebra.Field.Subfield.Basic
/-- Sum of elements in a `Subfield` indexed by a `Finset` is in the `Subfield`.  -/
Subfield.sum_mem : ∀ {K : Type u} [inst : DivisionRing K] (s : Subfield K) {ι : Type u_1} {t : Finset ι} {f : ι → K},
  (∀ c ∈ t, f c ∈ s) → ∑ i ∈ t, f i ∈ s
-- Mathlib.Topology.NhdsKer
/-- This name was used to be used for the `Iff` version,
see `nhdsKer_subset_nhdsKer_iff_nhdsSet`.
 -/
nhdsKer_subset_nhdsKer : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s t : Set X}, s ⊆ t → nhdsKer s ⊆ nhdsKer t
-- Mathlib.ModelTheory.Order
FirstOrder.Language.dlo_isExtensionPair : ∀ (M : Type w) [inst : FirstOrder.Language.order.Structure M] [M ⊨ FirstOrder.Language.order.linearOrderTheory]
  (N : Type w') [inst_2 : FirstOrder.Language.order.Structure N] [N ⊨ FirstOrder.Language.order.dlo] [Nonempty N],
  FirstOrder.Language.order.IsExtensionPair M N
-- Mathlib.Data.QPF.Multivariate.Constructions.Const
MvQPF.Const.get_map : ∀ {n : ℕ} {A : Type u} {α β : TypeVec.{u} n} (f : α.Arrow β) (x : MvQPF.Const n A α), (MvFunctor.map f x).get = x.get
-- Mathlib.Algebra.BigOperators.Finprod
finsum_eq_sum_of_support_subset_of_finite : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] (f : α → M) {s : Set α},
  Function.support f ⊆ s → ∀ (hs : s.Finite), ∑ᶠ (i : α), f i = ∑ i ∈ hs.toFinset, f i
-- Mathlib.Algebra.Group.Int.Units
Int.units_natAbs : ∀ (u : ℤˣ), (↑u).natAbs = 1
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_add_opow_of_isPrincipal_add`. -/
Ordinal.principal_add_opow_of_principal_add : ∀ {a : Ordinal.{u_1}},
  Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) a →
    ∀ (b : Ordinal.{u_1}), Ordinal.IsPrincipal (fun x1 x2 => x1 + x2) (a ^ b)
-- Init.Data.Array.Zip
Array.zip_eq_append_iff : ∀ {α : Type u_1} {β : Type u_2} {xs ys : Array (α × β)} {as : Array α} {bs : Array β},
  as.zip bs = xs ++ ys ↔
    ∃ as₁ as₂ bs₁ bs₂, as₁.size = bs₁.size ∧ as = as₁ ++ as₂ ∧ bs = bs₁ ++ bs₂ ∧ xs = as₁.zip bs₁ ∧ ys = as₂.zip bs₂
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DefinitionParams.mk.injEq : ∀ (toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1)
-- Mathlib.Order.Interval.Finset.Basic
/-- A function from a locally finite partial order is antitone if and only if it is antitone when
restricted to pairs satisfying `a ⋖ b`.  -/
antitone_iff_forall_covBy : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [LocallyFiniteOrder α] [inst_2 : Preorder β] (f : α → β),
  Antitone f ↔ ∀ (a b : α), a ⋖ b → f b ≤ f a
-- Mathlib.Topology.UniformSpace.UniformConvergence
/-- A sequence of functions `Fₙ` converges uniformly to a limiting function `f` with respect to a
filter `p` if, for any entourage of the diagonal `u`, one has `p`-eventually
`(f x, Fₙ x) ∈ u` for all `x`.  -/
TendstoUniformly : {α : Type u_1} → {β : Type u_2} → {ι : Type u_4} → [UniformSpace β] → (ι → α → β) → (α → β) → Filter ι → Prop
-- Mathlib.CategoryTheory.Types.Basic
/-- The underlying function.  -/
TypeCat.Fun.toFun : {X : Type u_1} → {Y : Type u_2} → TypeCat.Fun X Y → X → Y
-- Mathlib.Order.Completion
DedekindCut.right_principal : ∀ {α : Type u_1} [inst : Preorder α] (a : α), (DedekindCut.principal a).right = Set.Ici a
-- Mathlib.FieldTheory.Minpoly.IsConjRoot
/-- If `y` is a conjugate root of `x`, then `x` is also a conjugate root of `y`.
 -/
IsConjRoot.symm : ∀ {R : Type u_1} {A : Type u_5} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] {x y : A},
  IsConjRoot R x y → IsConjRoot R y x
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.Subgraph.nontrivial_verts_of_degree_ne_zero : ∀ {V : Type u} {G : SimpleGraph V} {G' : G.Subgraph} {v : V} [inst : Fintype ↑(G'.neighborSet v)],
  G'.degree v ≠ 0 → Nontrivial ↑G'.verts
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.casesOn_of_add : ∀ {α : Type u_1} {motive : FreeAddMonoid α → Sort u_6} (x : α) (xs : FreeAddMonoid α) (zero : motive 0)
  (of_add : (x : α) → (xs : FreeAddMonoid α) → motive (FreeAddMonoid.of x + xs)),
  FreeAddMonoid.casesOn (FreeAddMonoid.of x + xs) zero of_add = of_add x xs
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.ChosenPullback
CategoryTheory.Limits.ChosenPullback.LiftStruct.f_p_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ S : C} {f₁ : X₁ ⟶ S} {f₂ : X₂ ⟶ S}
  {h : CategoryTheory.Limits.ChosenPullback f₁ f₂} {Y : C} {g₁ : Y ⟶ X₁} {g₂ : Y ⟶ X₂} {b : Y ⟶ S}
  (self : h.LiftStruct g₁ g₂ b) {Z : C} (h_1 : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.f (CategoryTheory.CategoryStruct.comp h.p h_1) =
    CategoryTheory.CategoryStruct.comp b h_1
-- Lean.Meta.Injective
Lean.Meta.mkInjectiveEqTheoremNameFor : Lean.Name → Lean.Name
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_minKey? : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {km : α}, t.minKey? = some km → Std.DTreeMap.Internal.Impl.contains km t = true
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabBadCDot : Lean.Elab.Term.TermElab
-- Init.Data.Range.Lemmas
_private.Init.Data.Range.Lemmas.0.Std.Legacy.Range.forM.loop.eq_1 : ∀ {m : Type u_1 → Type u_2} [inst : Monad m] (range : Std.Legacy.Range) (f : ℕ → m PUnit.{u_1 + 1}) (i : ℕ),
  Std.Legacy.Range.forM.loop✝ range f i =
    if i < range.stop then do
      f i
      have this : 0 < range.step := ⋯
      Std.Legacy.Range.forM.loop✝ range f (i + range.step)
    else pure PUnit.unit
-- Mathlib.RingTheory.Coalgebra.MonoidAlgebra
MonoidAlgebra.instCoalgebra.eq_1 : ∀ (R : Type u_1) [inst : CommSemiring R] (A : Type u_2) [inst_1 : Semiring A] (X : Type u_3) [inst_2 : Module R A]
  [inst_3 : Coalgebra R A], MonoidAlgebra.instCoalgebra R A X = Equiv.coalgebra R MonoidAlgebra.coeffEquiv
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_union_of_contains_right : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {m₁ m₂ : Std.DTreeMap.Internal.Impl α fun x => β} [inst : Std.TransOrd α]
  (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α} (h : Std.DTreeMap.Internal.Impl.contains k m₂ = true),
  Std.DTreeMap.Internal.Impl.Const.get (m₁.union m₂ ⋯ ⋯) k ⋯ = Std.DTreeMap.Internal.Impl.Const.get m₂ k h
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
HasFTaylorSeriesUpTo.fderiv : ∀ {𝕜 : 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] {n : WithTop ℕ∞}
  {f : E → F} {p : E → FormalMultilinearSeries 𝕜 E F},
  HasFTaylorSeriesUpTo n f p → ∀ (m : ℕ), ↑m < n → ∀ (x : E), HasFDerivAt (fun y => p y m) (p x m.succ).curryLeft x
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
/-- A bicone for `F` which is both a limit cone and a colimit cocone.  -/
CategoryTheory.Limits.biproduct.bicone : {J : Type w} →
  {C : Type uC} →
    [inst : CategoryTheory.Category.{uC', uC} C] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
        (F : J → C) → [CategoryTheory.Limits.HasBiproduct F] → CategoryTheory.Limits.Bicone F
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {k : α}, List.find? (fun x => x.fst == k) (↑m).toList = none ↔ m.contains k = false
-- Std.Http.Protocol.H1
_private.Std.Http.Protocol.H1.0.Std.Http.Protocol.H1.Machine.BodyMode.chunked.sizeOf_spec : sizeOf Std.Http.Protocol.H1.Machine.BodyMode.chunked✝ = 1
-- Mathlib.Algebra.Algebra.Pi
AlgEquiv.piCongrLeft'_symm_apply : ∀ {R : Type u_3} {ι : Type u_4} {A₁ : ι → Type u_5} [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A₁ i)]
  [inst_2 : (i : ι) → Algebra R (A₁ i)] {ι' : Type u_8} (e : ι ≃ ι') (x : (i : ι') → A₁ (e.symm i)),
  (AlgEquiv.piCongrLeft' R A₁ e).symm x = (Equiv.piCongrLeft' A₁ e).symm x
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.brecOn.go : {motive_1 : Lean.Elab.Term.Do.Code → Sort u} →
  {motive_2 : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
    {motive_3 : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
      {motive_4 : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) → Sort u} →
        {motive_5 : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) → Sort u} →
          {motive_6 : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code → Sort u} →
            {motive_7 : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code → Sort u} →
              (t : Lean.Elab.Term.Do.Code) →
                ((t : Lean.Elab.Term.Do.Code) → t.below → motive_1 t) →
                  ((t : Array (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                      Lean.Elab.Term.Do.Code.below_1 t → motive_2 t) →
                    ((t : Array (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                        Lean.Elab.Term.Do.Code.below_2 t → motive_3 t) →
                      ((t : List (Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code)) →
                          Lean.Elab.Term.Do.Code.below_3 t → motive_4 t) →
                        ((t : List (Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code)) →
                            Lean.Elab.Term.Do.Code.below_4 t → motive_5 t) →
                          ((t : Lean.Elab.Term.Do.Alt Lean.Elab.Term.Do.Code) →
                              Lean.Elab.Term.Do.Code.below_5 t → motive_6 t) →
                            ((t : Lean.Elab.Term.Do.AltExpr Lean.Elab.Term.Do.Code) →
                                Lean.Elab.Term.Do.Code.below_6 t → motive_7 t) →
                              motive_1 t ×' t.below
-- Mathlib.Data.NNReal.Defs
NNReal.smulCommClass_right : ∀ {M : Type u_1} {N : Type u_2} [inst : MulAction ℝ N] [inst_1 : SMul M N] [SMulCommClass M ℝ N],
  SMulCommClass M NNReal N
-- Batteries.Data.List.Basic
List.rotate'.eq_3 : ∀ {α : Type u_1} (a : α) (l : List α) (n : ℕ), (a :: l).rotate' n.succ = (l ++ [a]).rotate' n
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.ext : ∀ {V : Type u} {x y : SimpleGraph V}, x.Adj = y.Adj → x = y
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- Truncated cosimplicial objects.  -/
CategoryTheory.CosimplicialObject.Truncated : (C : Type u) → [CategoryTheory.Category.{v, u} C] → ℕ → Type (max v u)
-- Init.Data.Int.Linear
Int.Internal.Linear.cooper_dvd_right_split_dvd2_cert.eq_1 : ∀ (p₂ p₃ : Int.Internal.Linear.Poly) (d : ℤ) (k : ℕ) (d' : ℤ) (p' : Int.Internal.Linear.Poly),
  Int.Internal.Linear.cooper_dvd_right_split_dvd2_cert p₂ p₃ d k d' p' =
    (d'.beq' (p₂.leadCoeff * d)).and'
      (p'.beq'
        ((Int.Internal.Linear.Poly.combine_mul_k (-p₃.leadCoeff) p₂.leadCoeff p₂.tail p₃.tail).addConst_k
          (-p₃.leadCoeff * ↑k)))
-- Mathlib.Algebra.Ring.Subsemiring.Defs
/-- A subsemiring of a `NonAssocCommSemiring` inherits a `NonAssocCommSemiring` structure  -/
SubsemiringClass.toNonAssocCommSemiring : {S : Type v} →
  (s : S) →
    {R : Type u_1} →
      [inst : NonAssocCommSemiring R] → [inst_1 : SetLike S R] → [SubsemiringClass S R] → NonAssocCommSemiring ↥s
-- Mathlib.Data.Multiset.Lattice
Multiset.sup_singleton : ∀ {α : Type u_1} [inst : SemilatticeSup α] [inst_1 : OrderBot α] {a : α}, {a}.sup = a