mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_add_self : ∀ (R : Type u_1) {V : Type u_2} [inst : Ring R] [inst_1 : Invertible 2] [inst_2 : AddCommGroup V] [inst_3 : Module R V]
  (x y : V), midpoint R x y + midpoint R x y = x + y
-- Mathlib.Topology.Compactness.Compact
/-- **Tychonoff's theorem** formulated using `Set.pi`: product of compact sets is compact.  -/
isCompact_univ_pi : ∀ {ι : Type u_1} {X : ι → Type u_2} [inst : (i : ι) → TopologicalSpace (X i)] {s : (i : ι) → Set (X i)},
  (∀ (i : ι), IsCompact (s i)) → IsCompact (Set.univ.pi s)
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.coeFnAddMonoidHom_apply : ∀ {α : Type u_3} {E : α → Type u_4} {p : ENNReal} [inst : (i : α) → NormedAddCommGroup (E i)] (x : ↥(lp E p)),
  (lp.coeFnAddMonoidHom E p) x = ↑x
-- Mathlib.Analysis.Normed.Group.Quotient
QuotientAddGroup.norm_eq_infDist : ∀ {M : Type u_1} [inst : SeminormedAddCommGroup M] {S : AddSubgroup M} (x : M ⧸ S), ‖x‖ = Metric.infDist 0 {m | ↑m = x}
-- Mathlib.Algebra.Homology.DerivedCategory.FullyFaithful
DerivedCategory.instFaithfulSingleFunctor : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] (n : ℤ), (DerivedCategory.singleFunctor C n).Faithful
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.IsIndContained.rfl : ∀ {V : Type u_1} {G : SimpleGraph V}, G.IsIndContained G
-- Mathlib.Algebra.Quaternion
/-- The additive equivalence between a quaternion algebra over `R` and `R × R × R × R`.  -/
QuaternionAlgebra.addEquivProd : {R : Type u_3} → [inst : Add R] → (c₁ c₂ c₃ : R) → QuaternionAlgebra R c₁ c₂ c₃ ≃+ R × R × R × R
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHom_associator : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] (c₁ c₂ c₃ : C) (d : D),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d
        (CategoryTheory.MonoidalCategoryStruct.associator c₁ c₂ c₃).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c₁
            (CategoryTheory.MonoidalCategoryStruct.tensorObj c₂ c₃)).hom
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso
            (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionObj d c₁) c₂ c₃).hom) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d
          (CategoryTheory.MonoidalCategoryStruct.tensorObj c₁ c₂) c₃).hom
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso d c₁ c₂).hom c₃)
-- Std.Data.Internal.List.Associative
Std.Internal.List.isEmpty_alterKey_eq_isEmpty_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {k : α} {f : Option (β k) → Option (β k)}
  {l : List ((a : α) × β a)},
  (Std.Internal.List.alterKey k f l).isEmpty =
    ((Std.Internal.List.eraseKey k l).isEmpty && (f (Std.Internal.List.getValueCast? k l)).isNone)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Zipper.toList_prependMap_done : ∀ {α : Type u} {β : α → Type v} (t : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Zipper.prependMap t Std.DTreeMap.Internal.Zipper.done).toList = t.toList
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- If `f₀ : X ⟶ Y` is homotopic to `f₁` relative to a path object `P`,
and `f₁` is homotopic to `f₂` relative to a good path object `P'`,
then `f₀` is homotopic to `f₂` relative to the path object `P.trans P'`
when `Y` is fibrant.  -/
HomotopicalAlgebra.PathObject.RightHomotopy.trans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      [inst_1 : HomotopicalAlgebra.ModelCategory C] →
        {P : HomotopicalAlgebra.PathObject Y} →
          [inst_2 : HomotopicalAlgebra.IsFibrant Y] →
            {f₀ f₁ f₂ : X ⟶ Y} →
              P.RightHomotopy f₀ f₁ →
                {P' : HomotopicalAlgebra.PathObject Y} →
                  [inst_3 : P'.IsGood] →
                    P'.RightHomotopy f₁ f₂ →
                      [CategoryTheory.Limits.HasPullback P.p₁ P'.p₀] → (P.trans P').RightHomotopy f₀ f₂
-- Mathlib.Geometry.Euclidean.Incenter
Affine.Simplex.isTangentAt_insphere_iff_eq_touchpoint : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} [inst_4 : NeZero n] {s : Affine.Simplex ℝ P n} {i : Fin (n + 1)} {p : P},
  s.insphere.IsTangentAt p (affineSpan ℝ (Set.range (s.faceOpposite i).points)) ↔ p = s.touchpoint ∅ i
-- Mathlib.MeasureTheory.Covering.DensityTheorem
IsUnifLocDoublingMeasure.vitaliFamily.congr_simp : ∀ {α : Type u_2} [inst : PseudoMetricSpace α] [inst_1 : MeasurableSpace α] (μ : MeasureTheory.Measure α)
  [inst_2 : IsUnifLocDoublingMeasure μ] [inst_3 : SecondCountableTopology α] [inst_4 : BorelSpace α]
  [inst_5 : MeasureTheory.IsLocallyFiniteMeasure μ] (K K_1 : ℝ),
  K = K_1 → IsUnifLocDoublingMeasure.vitaliFamily μ K = IsUnifLocDoublingMeasure.vitaliFamily μ K_1
-- Std.Time.Notation.Spec
_private.Std.Time.Notation.Spec.0.Std.Time.convertZoneName : Std.Time.ZoneName → Lean.MacroM (Lean.TSyntax `term)
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_add : ∀ (R : Type u_1) [inst : Semiring R] (p q : Polynomial R) {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
  [inst_3 : Module R S] (x : S), (p + q).smeval x = p.smeval x + q.smeval x
-- Mathlib.Topology.Spectral.ConstructibleTopology
IsCompact.isOpen_constructibleTopology_of_isClosed : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsCompact sᶜ → IsClosed s → IsOpen s
-- Mathlib.Computability.PartrecBasis
Nat.Partrec'.cons : ∀ {n m : ℕ} {f : List.Vector ℕ n → ℕ} {g : List.Vector ℕ n → List.Vector ℕ m},
  Nat.Partrec' ↑f → Nat.Partrec'.Vec g → Nat.Partrec'.Vec fun v => f v ::ᵥ g v
-- Mathlib.NumberTheory.LSeries.ZMod
/-- First form of functional equation for completed L-functions (odd case).

Private because it is superseded by `completedLFunction_one_sub_odd` below, which is valid for a
much wider range of `s`.
 -/
_private.Mathlib.NumberTheory.LSeries.ZMod.0.ZMod.completedLFunction_one_sub_of_one_lt_odd : ∀ {N : ℕ} [inst : NeZero N] {Φ : ZMod N → ℂ},
  Function.Odd Φ →
    ∀ {s : ℂ},
      1 < s.re → ZMod.completedLFunction Φ (1 - s) = ↑N ^ (s - 1) * Complex.I * ZMod.completedLFunction (ZMod.dft Φ) s
-- Mathlib.Order.Interval.Finset.Defs
/-- Left-open right-infinite interval  -/
LocallyFiniteOrderTop.finsetIoi : {α : Type u_1} → {inst : Preorder α} → [self : LocallyFiniteOrderTop α] → α → Finset α
-- Mathlib.Control.Monad.Cont
LawfulMonadCont.callCC_bind_left : ∀ {m : Type u → Type v} {inst : Monad m} {inst_1 : MonadCont m} [self : LawfulMonadCont m] {α : Type u} (β : Type u)
  (x : α) (dead : MonadCont.Label α m β → β → m α), (MonadCont.callCC fun f => MonadCont.goto f x >>= dead f) = pure x
-- Mathlib.Topology.ContinuousMap.Basic
/-- `Prod.fst : (x, y) ↦ x` as a bundled continuous map.  -/
ContinuousMap.fst : {α : Type u_1} → {β : Type u_2} → [inst : TopologicalSpace α] → [inst_1 : TopologicalSpace β] → C(α × β, α)
-- Mathlib.Data.PFun
PFun.mem_preimage : ∀ {α : Type u_1} {β : Type u_2} (f : α →. β) (s : Set β) (x : α), x ∈ f.preimage s ↔ ∃ y ∈ s, y ∈ f x
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
/-- If `p ≠ 0` and `p ≠ 1`, then `padicValNat p p` is `1`.  -/
padicValNat.self : ∀ {p : ℕ}, 1 < p → padicValNat p p = 1
-- Init.Data.List.Lemmas
/-- Variant of `map_const` using a lambda rather than `Function.const`.  -/
List.map_const' : ∀ {α : Type u_1} {β : Type u_2} {l : List α} {b : β}, List.map (fun x => b) l = List.replicate l.length b
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of a monotone function and a strictly monotone function is
strictly monotone.  -/
Monotone.add_strictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] [AddLeftStrictMono α]
  [AddRightMono α] {f g : β → α}, Monotone f → StrictMono g → StrictMono fun x => f x + g x
-- Init.Data.Array.Basic
Array.mapFinIdxM.map : {α : Type u} →
  {β : Type v} →
    {m : Type v → Type w} →
      [Monad m] →
        (as : Array α) → ((i : ℕ) → α → i < as.size → m β) → (i j : ℕ) → i + j = as.size → Array β → m (Array β)
-- Lean.Util.LeanOptions
Lean.instInhabitedLeanOptions : Inhabited Lean.LeanOptions
-- Mathlib.Algebra.Lie.Quotient
LieSubmodule.Quotient.mk_eq_zero' : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : AddCommGroup M]
  [inst_3 : Module R M] [inst_4 : LieRingModule L M] {N : LieSubmodule R L M} {m : M},
  LieSubmodule.Quotient.mk m = 0 ↔ m ∈ N
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
/-- **Alias** of `Finsupp.finsetSum_apply`. -/
Finsupp.finset_sum_apply : ∀ {α : Type u_1} {ι : Type u_2} {N : Type u_10} [inst : AddCommMonoid N] (S : Finset ι) (f : ι → α →₀ N) (a : α),
  (∑ i ∈ S, f i) a = ∑ i ∈ S, (f i) a
-- Lean.PrettyPrinter.Delaborator.Basic
Lean.PrettyPrinter.Delaborator.delabLevel : Lean.Level → ℕ → Lean.PrettyPrinter.Delaborator.DelabM Lean.Syntax.Level
-- Mathlib.Data.Set.Functor
/-- **Alias** of `Set.image_image_val_eq_domRestrict_image`. -/
Set.image_image_val_eq_restrict_image : ∀ {α : Type u} {β : Set α} {γ : Set ↑β} {δ : Type u_1} {f : α → δ}, f '' Subtype.val '' γ = β.domRestrict f '' γ
-- Mathlib.Algebra.Category.AlgCat.Monoidal
AlgCat.hom_inv_rightUnitor : ∀ {R : Type u} [inst : CommRing R] {M : AlgCat R},
  AlgCat.Hom.hom (CategoryTheory.MonoidalCategoryStruct.rightUnitor M).inv =
    ↑(Algebra.TensorProduct.rid (↑(CategoryTheory.MonoidalCategoryStruct.tensorUnit (AlgCat R))) R ↑M).symm
-- Mathlib.FieldTheory.Separable
Polynomial.card_rootSet_eq_natDegree : ∀ {F : Type u} [inst : Field F] {K : Type v} [inst_1 : Field K] [inst_2 : Algebra F K] {p : Polynomial F},
  p.Separable → (Polynomial.map (algebraMap F K) p).Splits → Fintype.card ↑(p.rootSet K) = p.natDegree
-- Mathlib.Condensed.Light.TopCatAdjunction
/-- The unit of the adjunction `lightCondSetToTopCat ⊣ topCatToLightCondSet`  -/
LightCondSet.topCatAdjunctionUnit : (X : LightCondSet) → X ⟶ X.toTopCat.toLightCondSet
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_hom : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{u_4, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : data.HasFirstPageComputation] [inst_4 : X.HasSpectralSequence data] (pq : κ) (i₁ i₂ : ι)
  (hi₁ : i₁ = data.i₁ pq) (hi₂ : i₂ = data.i₂ pq) (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq)
  (hn₁ : autoParam (n₀ + 1 = n₁) CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_hom._auto_1)
  (hn₂ : autoParam (n₁ + 1 = n₂) CategoryTheory.Abelian.SpectralObject.spectralSequenceFirstPageXIso_hom._auto_3),
  (X.spectralSequenceFirstPageXIso data pq i₁ i₂ hi₁ hi₂ n₁ hn₁').hom =
    CategoryTheory.CategoryStruct.comp
      (X.spectralSequencePageXIso data r₀ ⋯ pq i₁ i₁ i₂ i₂ ⋯ hi₁ hi₂ ⋯ n₀ n₁ n₂ hn₁' ⋯ ⋯).hom
      (X.EIsoH (CategoryTheory.homOfLE ⋯) n₀ n₁ n₂ hn₁ hn₂).hom
-- Mathlib.Data.Rat.Cast.Lemmas
Rat.cast_pow : ∀ {α : Type u_1} [inst : DivisionRing α] (p : ℚ) (n : ℕ), ↑(p ^ n) = ↑p ^ n
-- Mathlib.Analysis.BoxIntegral.Partition.Additive
BoxIntegral.BoxAdditiveMap.map_split_add : ∀ {ι : Type u_1} {M : Type u_2} [inst : AddCommMonoid M] {I₀ : WithTop (BoxIntegral.Box ι)} {I : BoxIntegral.Box ι}
  (f : BoxIntegral.BoxAdditiveMap ι M I₀),
  ↑I ≤ I₀ → ∀ (i : ι) (x : ℝ), Option.elim' 0 (⇑f) (I.splitLower i x) + Option.elim' 0 (⇑f) (I.splitUpper i x) = f I
-- Mathlib.Data.List.Cycle
Cycle.prev_reverse_eq_next' : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α) (hs : s.reverse.Nodup) (x : α) (hx : x ∈ s.reverse),
  s.reverse.prev hs x hx = s.next ⋯ x ⋯
-- Mathlib.Algebra.Ring.Subring.MulOpposite
Subring.unop_op : ∀ {R : Type u_2} [inst : NonAssocRing R] (S : Subring R), S.op.unop = S
-- Mathlib.NumberTheory.Cyclotomic.PrimitiveRoots
/-- If `Irreducible (cyclotomic (p ^ (k + 1)) K)` (in particular for `K = ℚ`) and `p` is a prime,
then the norm of `ζ ^ (p ^ s) - 1` is `p ^ (p ^ s)` if `p ≠ 2`.  -/
IsPrimitiveRoot.norm_pow_sub_one_of_prime_ne_two : ∀ {p : ℕ} {K : Type u} {L : Type v} [inst : Field L] {ζ : L} [inst_1 : Field K] [inst_2 : Algebra K L] {k : ℕ},
  IsPrimitiveRoot ζ (p ^ (k + 1)) →
    ∀ [hpri : Fact (Nat.Prime p)] [IsCyclotomicExtension {p ^ (k + 1)} K L],
      Irreducible (Polynomial.cyclotomic (p ^ (k + 1)) K) →
        ∀ {s : ℕ}, s ≤ k → p ≠ 2 → (Algebra.norm K) (ζ ^ p ^ s - 1) = ↑p ^ p ^ s
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.homMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X}
  (h h_1 : f.obj.left ⟶ g.obj.left) (e_h : h = h_1) (w : CategoryTheory.CategoryStruct.comp h g.arrow = f.arrow),
  CategoryTheory.MonoOver.homMk h w = CategoryTheory.MonoOver.homMk h_1 ⋯
-- Mathlib.AlgebraicGeometry.Birational.Birational
AlgebraicGeometry.Scheme.PartialIso.mk.inj : ∀ {X Y : AlgebraicGeometry.Scheme} {source : X.Opens} {dense_source : Dense ↑source} {target : Y.Opens}
  {dense_target : Dense ↑target} {iso : ↑source ≅ ↑target} {source_1 : X.Opens} {dense_source_1 : Dense ↑source_1}
  {target_1 : Y.Opens} {dense_target_1 : Dense ↑target_1} {iso_1 : ↑source_1 ≅ ↑target_1},
  { source := source, dense_source := dense_source, target := target, dense_target := dense_target, iso := iso } =
      { source := source_1, dense_source := dense_source_1, target := target_1, dense_target := dense_target_1,
        iso := iso_1 } →
    source = source_1 ∧ target = target_1 ∧ iso ≍ iso_1
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.instBoundedOrder : {α : Type u_1} → [inst : TopologicalSpace α] → [CompactSpace α] → BoundedOrder (TopologicalSpace.CompactOpens α)
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithInitial.comp.eq_3 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (x : CategoryTheory.WithInitial C) (_X : C),
  CategoryTheory.WithInitial.comp =
    match (motive := (x x_1 x_2 : CategoryTheory.WithInitial C) → x.Hom x_1 → x_1.Hom x_2 → x.Hom x_2) x,
      CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.star with
    | CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.of _Z => fun f g =>
      CategoryTheory.CategoryStruct.comp f g
    | CategoryTheory.WithInitial.star, x, CategoryTheory.WithInitial.of _X => fun _f _g => PUnit.unit
    | x, CategoryTheory.WithInitial.of _X, CategoryTheory.WithInitial.star => fun _f g => PEmpty.elim g
    | CategoryTheory.WithInitial.of _Y, CategoryTheory.WithInitial.star, x => fun f _g => PEmpty.elim f
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star => fun x x_1 =>
      PUnit.unit
-- Mathlib.Analysis.Normed.Ring.Basic
norm_natAbs : ∀ {α : Type u_2} [inst : SeminormedRing α] (z : ℤ), ‖↑z.natAbs‖ = ‖↑z‖
-- Mathlib.Computability.ContextFreeGrammar
ContextFreeRule.rewrites_of_exists_parts : ∀ {T : Type u_1} {N : Type u_2} (r : ContextFreeRule T N) (p q : List (Symbol T N)),
  r.Rewrites (p ++ [Symbol.nonterminal r.input] ++ q) (p ++ r.output ++ q)
-- Mathlib.MeasureTheory.Measure.Regular
MeasureTheory.Measure.Regular.smul_nnreal : ∀ {α : Type u_1} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} [inst_1 : TopologicalSpace α] [μ.Regular]
  (c : NNReal), (c • μ).Regular
-- Mathlib.Algebra.FreeAlgebra
FreeAlgebra.Rel.below.add_scalar : ∀ {R : Type u_1} {X : Type u_2} [inst : CommSemiring R]
  {motive : (a a_1 : FreeAlgebra.Pre R X) → FreeAlgebra.Rel R X a a_1 → Prop} {r s : R}, FreeAlgebra.Rel.below ⋯
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α},
  Std.ExtDHashMap.Const.get? (m₁ \ m₂) k = if k ∈ m₂ then none else Std.ExtDHashMap.Const.get? m₁ k
-- Lean.DocString.Extension
Lean.ModuleDoc.doc : Lean.ModuleDoc → String
-- Mathlib.Geometry.Convex.Cone.Dual
PointedCone.dual_sUnion : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] {N : Type u_3} [inst_5 : AddCommMonoid N] [inst_6 : Module R N]
  {p : M →ₗ[R] N →ₗ[R] R} (S : Set (Set M)), PointedCone.dual p (⋃₀ S) = sInf (PointedCone.dual p '' S)
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
/-- **Alias** of `Nat.isSemilinearSet_setOfPred_mulVec_eq`.

---

Matrix version of `isSemilinearSet_setOfPred_eq`.  -/
Nat.isSemilinearSet_setOf_mulVec_eq : ∀ {ι : Type u_3} {κ : Type u_4} [inst : Fintype κ] (u v : ι → ℕ) (A B : Matrix ι κ ℕ),
  IsSemilinearSet {x | u + A.mulVec x = v + B.mulVec x}
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Pos.skipWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String} {pos : s.Pos},
  pos.toSlice.skipWhile pat = (pos.skipWhile pat).toSlice
-- Mathlib.Geometry.Manifold.MFDeriv.NormedSpace
/-- **Alias** of `mvfderiv`.

---

`mvfderiv I J f x` is the `mfderiv` of a vector-valued function `f` on `M` at `x`,
but taking values in the target normed space directly.
The difference to `mfderiv` is explained in the module-docstring for
`Mathlib/Geometry/Manifold/MFDeriv/NormedSpace.lean`.

Future: this could be generalised to functions into additive torsors over abelian Lie groups.
 -/
extDerivFun : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_3} →
            [inst_3 : TopologicalSpace H] →
              (I : ModelWithCorners 𝕜 E H) →
                {M : Type u_4} →
                  [inst_4 : TopologicalSpace M] →
                    [inst_5 : ChartedSpace H M] →
                      {F : Type u_8} →
                        [inst_6 : NormedAddCommGroup F] →
                          [inst_7 : NormedSpace 𝕜 F] → (M → F) → (x : M) → TangentSpace I x →L[𝕜] F
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.prod_eq_prod_iff_single : ∀ {ι : Type u_1} {M : Type u_3} {s : Finset ι} [inst : CommMonoid M] [IsRightCancelMul M] {f g : ι → M} {i : ι},
  i ∈ s → (∀ j ∈ s, j ≠ i → f j = g j) → (∏ j ∈ s, f j = ∏ j ∈ s, g j ↔ f i = g i)
-- Mathlib.LinearAlgebra.QuadraticForm.IsometryEquiv
QuadraticMap.IsometryEquiv.toIsometry_apply : ∀ {R : Type u_2} {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_9} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid N] [inst_4 : Module R M₁] [inst_5 : Module R M₂]
  [inst_6 : Module R N] {Q₁ : QuadraticMap R M₁ N} {Q₂ : QuadraticMap R M₂ N} (g : Q₁.IsometryEquiv Q₂) (x : M₁),
  g.toIsometry x = g x
-- Mathlib.AlgebraicTopology.ModelCategory.LeftHomotopy
/-- If `f₀` is homotopic to `f₁` relative to a precylinder `P`,
and `f₁` is homotopic to `f₂` relative to `P'`, then
`f₀` is homotopic to `f₂` relative to `P.trans P'`.  -/
HomotopicalAlgebra.Precylinder.LeftHomotopy.trans : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      {P : HomotopicalAlgebra.Precylinder X} →
        {Y : C} →
          {f₀ f₁ f₂ : X ⟶ Y} →
            P.LeftHomotopy f₀ f₁ →
              {P' : HomotopicalAlgebra.Precylinder X} →
                P'.LeftHomotopy f₁ f₂ →
                  [inst_1 : CategoryTheory.Limits.HasPushout P.i₁ P'.i₀] → (P.trans P').LeftHomotopy f₀ f₂
-- Mathlib.CategoryTheory.Sites.Types
CategoryTheory.typeEquiv_functor_obj_obj_obj : ∀ (α : Type u) (Y : Type uᵒᵖ), (CategoryTheory.typeEquiv.functor.obj α).obj.obj Y = (Opposite.unop Y ⟶ α)
-- Mathlib.Combinatorics.Additive.DoublingConst
Finset.cast_mulConst : ∀ {G : Type u_1} [inst : Group G] [inst_1 : DecidableEq G] {𝕜 : Type u_3} [inst_2 : Semifield 𝕜] [CharZero 𝕜]
  (A B : Finset G), ↑(A.mulConst B) = ↑(A * B).card / ↑A.card
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aevalTower_toAlgHom : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S : Type u_2} {A : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring A] [inst_3 : Algebra S R] [inst_4 : Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (x : R),
  (MvPolynomial.aevalTower g y) ((IsScalarTower.toAlgHom S R (MvPolynomial σ R)) x) = g x
-- Mathlib.CategoryTheory.Action.Concrete
/-- If `H` and `N` are subgroups of a group `G` with `N` normal, there is a canonical
group homomorphism `H ⧸ N ⊓ H` to the `G`-endomorphisms of `G ⧸ N`.  -/
Action.FintypeCat.quotientToEndHom : {G : Type u_1} →
  [inst : Group G] →
    (H N : Subgroup G) →
      [inst_1 : Fintype (G ⧸ N)] →
        [inst_2 : N.Normal] →
          ↥H ⧸ N.subgroupOf H →* CategoryTheory.End (Action.FintypeCat.ofMulAction G (FintypeCat.of (G ⧸ N)))
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [inst : Std.TransCmp cmp] (h₁ : t₁.WF)
  (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ ∩ t₂}, (t₁ ∩ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.Algebra.Quaternion
Quaternion.imI_star : ∀ {R : Type u_3} [inst : CommRing R] (a : Quaternion R), (star a).imI = -a.imI
-- Mathlib.Tactic.GCongr.Core
Mathlib.Tactic.GCongr.GCongrHyp.mk.injEq : ∀ (lhsIdx rhsIdx hypIdx : ℕ) (hypsPos : List (Option ℕ)) (isContra : Bool) (lhsIdx_1 rhsIdx_1 hypIdx_1 : ℕ)
  (hypsPos_1 : List (Option ℕ)) (isContra_1 : Bool),
  ({ lhsIdx := lhsIdx, rhsIdx := rhsIdx, hypIdx := hypIdx, hypsPos := hypsPos, isContra := isContra } =
      { lhsIdx := lhsIdx_1, rhsIdx := rhsIdx_1, hypIdx := hypIdx_1, hypsPos := hypsPos_1, isContra := isContra_1 }) =
    (lhsIdx = lhsIdx_1 ∧ rhsIdx = rhsIdx_1 ∧ hypIdx = hypIdx_1 ∧ hypsPos = hypsPos_1 ∧ isContra = isContra_1)
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.monic_X_pow_add : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R} {n : ℕ}, p.degree < ↑n → (Polynomial.X ^ n + p).Monic
-- Init.Data.Int.Pow
Int.two_pow_pred_sub_two_pow' : ∀ {w : ℕ}, 0 < w → 2 ^ (w - 1) - 2 ^ w = -2 ^ (w - 1)
-- Mathlib.CategoryTheory.Monoidal.Comon_
/-- Comonoid objects in a braided category form a monoidal category.

This definition is via transporting back and forth to monoids in the opposite category.
 -/
CategoryTheory.Comon.monoidal : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [CategoryTheory.BraidedCategory C] → CategoryTheory.MonoidalCategory (CategoryTheory.Comon C)
-- Mathlib.RingTheory.Congruence.Defs
RingCon.instAddCommGroupQuotient : {R : Type u_1} → [inst : AddCommGroup R] → [inst_1 : Mul R] → (c : RingCon R) → AddCommGroup c.Quotient
-- Mathlib.Algebra.Order.Group.Cyclic
LinearOrderedCommGroup.Subgroup.genLTOne_unique_of_zpowers_eq : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] {g1 g2 : G},
  g1 < 1 → g2 < 1 → Subgroup.zpowers g1 = Subgroup.zpowers g2 → g1 = g2
-- Mathlib.Algebra.Divisibility.Basic
/-- Right divisibility relation. `RightDvd a b` means `a` right-divides `b`,
i.e., `∃ c, b = c * a`.  -/
«term_∣ᵣ_» : Lean.TrailingParserDescr
-- Mathlib.Algebra.Torsor.Basic
Set.vadd_set_vsub_vadd_set : ∀ {G : Type u_1} {P : Type u_2} [inst : AddCommGroup G] [inst_1 : AddTorsor G P] (v : G) (s t : Set P),
  (v +ᵥ s) -ᵥ (v +ᵥ t) = s -ᵥ t
-- Mathlib.CategoryTheory.MorphismProperty.IsInvertedBy
CategoryTheory.MorphismProperty.IsInvertedBy.of_comp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} C₃]
  (W : CategoryTheory.MorphismProperty C₁) (F : CategoryTheory.Functor C₁ C₂),
  W.IsInvertedBy F → ∀ (G : CategoryTheory.Functor C₂ C₃), W.IsInvertedBy (F.comp G)