mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (Ω₀ Ω : C) (truth : Ω₀ ⟶ Ω)
  (mono_truth : autoParam (CategoryTheory.Mono truth) CategoryTheory.Subobject.Classifier.mono_truth._autoParam)
  (χ₀ : (U : C) → U ⟶ Ω₀) (χ : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω)
  (isPullback :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m], CategoryTheory.IsPullback m (χ₀ U) (χ m) truth)
  (uniq :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] {χ₀' : U ⟶ Ω₀} {χ' : X ⟶ Ω},
      CategoryTheory.IsPullback m χ₀' χ' truth → χ' = χ m)
  (Ω₀_1 Ω_1 : C) (truth_1 : Ω₀_1 ⟶ Ω_1)
  (mono_truth_1 : autoParam (CategoryTheory.Mono truth_1) CategoryTheory.Subobject.Classifier.mono_truth._autoParam)
  (χ₀_1 : (U : C) → U ⟶ Ω₀_1) (χ_1 : {U X : C} → (m : U ⟶ X) → [CategoryTheory.Mono m] → X ⟶ Ω_1)
  (isPullback_1 :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m], CategoryTheory.IsPullback m (χ₀_1 U) (χ_1 m) truth_1)
  (uniq_1 :
    ∀ {U X : C} (m : U ⟶ X) [inst_1 : CategoryTheory.Mono m] {χ₀' : U ⟶ Ω₀_1} {χ' : X ⟶ Ω_1},
      CategoryTheory.IsPullback m χ₀' χ' truth_1 → χ' = χ_1 m),
  ({ Ω₀ := Ω₀, Ω := Ω, truth := truth, mono_truth := mono_truth, χ₀ := χ₀, χ := χ, isPullback := isPullback,
        uniq := uniq } =
      { Ω₀ := Ω₀_1, Ω := Ω_1, truth := truth_1, mono_truth := mono_truth_1, χ₀ := χ₀_1, χ := χ_1,
        isPullback := isPullback_1, uniq := uniq_1 }) =
    (Ω₀ = Ω₀_1 ∧ Ω = Ω_1 ∧ truth ≍ truth_1 ∧ χ₀ ≍ χ₀_1 ∧ χ ≍ χ_1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.forIn_eq_forIn_keysArray : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {δ : Type w}
  {m' : Type w → Type w'} [inst : Monad m'] [LawfulMonad m'] {f : α → δ → m' (ForInStep δ)} {init : δ},
  Std.DHashMap.forIn (fun a x d => f a d) init m = forIn m.keysArray init f
-- Init.Data.Option.Lemmas
Option.map_id_fun : ∀ {α : Type u}, Option.map id = id
-- Mathlib.CategoryTheory.Adjunction.PartialAdjoint
/-- Given `F : D ⥤ C`, this is `F.partialLeftAdjoint` on morphisms.  -/
CategoryTheory.Functor.partialLeftAdjointMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor D C) →
          {X Y : F.PartialLeftAdjointSource} → (X ⟶ Y) → (F.partialLeftAdjointObj X ⟶ F.partialLeftAdjointObj Y)
-- Mathlib.Algebra.Homology.Augment
/-- We can "augment" a chain complex by inserting an arbitrary object in degree zero
(shifting everything else up), along with a suitable differential.
 -/
ChainComplex.augment : {V : Type u} →
  [inst : CategoryTheory.Category.{v, u} V] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
      (C : ChainComplex V ℕ) →
        {X : V} → (f : C.X 0 ⟶ X) → CategoryTheory.CategoryStruct.comp (C.d 1 0) f = 0 → ChainComplex V ℕ
-- Mathlib.Topology.Defs.Induced
/-- A function between topological spaces is an embedding if it is injective,
and for all `s : Set X`, `s` is open iff it is the preimage of an open set.  -/
Topology.IsEmbedding : {X : Type u_1} → {Y : Type u_2} → [tX : TopologicalSpace X] → [tY : TopologicalSpace Y] → (X → Y) → Prop
-- Mathlib.Data.Finsupp.Basic
Finsupp.prod_subtypeDomain_index : ∀ {α : Type u_1} {M : Type u_5} {N : Type u_6} [inst : Zero M] {p : α → Prop} [inst_1 : CommMonoid N] {v : α →₀ M}
  {h : α → M → N}, (∀ x ∈ v.support, p x) → ((Finsupp.subtypeDomain p v).prod fun a b => h (↑a) b) = v.prod h
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
cfcₙ_predicate_zero : ∀ (R : Type u_1) {A : Type u_2} {p : A → Prop} [inst : CommSemiring R] [inst_1 : Nontrivial R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalSemiring R] [inst_5 : ContinuousStar R] [inst_6 : NonUnitalRing A]
  [inst_7 : StarRing A] [inst_8 : TopologicalSpace A] [inst_9 : Module R A] [inst_10 : IsScalarTower R A A]
  [inst_11 : SMulCommClass R A A] [instCFCₙ : NonUnitalContinuousFunctionalCalculus R A p], p 0
-- Init.Data.Bool
Bool.xor_assoc : ∀ (x y z : Bool), (x ^^ y ^^ z) = (x ^^ (y ^^ z))
-- Mathlib.Tactic.NormNum.Result
Mathlib.Meta.NormNum.IsNat.to_isInt : ∀ {α : Type u_1} [inst : Ring α] {a : α} {n : ℕ},
  Mathlib.Meta.NormNum.IsNat a n → Mathlib.Meta.NormNum.IsInt a (Int.ofNat n)
-- Mathlib.Order.OmegaCompletePartialOrder
/-- **Alias** of `OmegaCompletePartialOrder.Chain.zip_apply`. -/
OmegaCompletePartialOrder.Chain.zip_coe : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (c₀ : OmegaCompletePartialOrder.Chain α)
  (c₁ : OmegaCompletePartialOrder.Chain β) (n : ℕ), (c₀.zip c₁) n = (c₀ n, c₁ n)
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.smul_def : ∀ {S : Type u'} {R : Type u} {M : Type v} [inst : SMul R M] [inst_1 : SetLike S M] [hS : SMulMemClass S R M] (s : S)
  (r : R) (x : ↥s), r • x = ⟨r • ↑x, ⋯⟩
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.Arrow.precompRelation_g₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {S : J.Cover X} (I : S.Arrow) {Z : C} (g : Z ⟶ I.Y),
  (I.precompRelation g).g₁ = CategoryTheory.CategoryStruct.id (I.precomp g).Y
-- Mathlib.Combinatorics.Matroid.Map
Matroid.comapOn_isBase_iff_of_bijOn : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {N : Matroid β} {E B : Set α},
  Set.BijOn f E N.E → ((N.comapOn E f).IsBase B ↔ N.IsBase (f '' B) ∧ B ⊆ E)
-- Mathlib.Order.RelClasses
WellFounded.asymmetric₃ : ∀ {α : Sort u_1} {r : α → α → Prop}, WellFounded r → ∀ (a b c : α), r a b → r b c → ¬r c a
-- Batteries.Data.List.Lemmas
List.idxsOf_cons : ∀ {α : Type u_1} {x : α} {xs : List α} {y : α} {s : ℕ} [inst : BEq α],
  List.idxsOf y (x :: xs) s = if (x == y) = true then s :: List.idxsOf y xs (s + 1) else List.idxsOf y xs (s + 1)
-- Mathlib.RingTheory.SimpleModule.Basic
LinearEquiv.isSemisimpleModule_iff : ∀ {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_5}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] (e : M ≃ₗ[R] N), IsSemisimpleModule R M ↔ IsSemisimpleModule R N
-- Mathlib.AlgebraicTopology.Quasicategory.Nerve
/-- By virtue of satisfying the `StrictSegal` condition, the nerve of a
category is a `Quasicategory`.  -/
CategoryTheory.Nerve.quasicategory : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C], (CategoryTheory.nerve C).Quasicategory
-- Mathlib.ModelTheory.ElementarySubstructures
/-- The substructure `M` of the structure `M` is elementary.  -/
FirstOrder.Language.ElementarySubstructure.instTop : {L : FirstOrder.Language} → {M : Type u_1} → [inst : L.Structure M] → Top (L.ElementarySubstructure M)
-- Mathlib.SetTheory.Cardinal.HasCardinalLT
hasCardinalLT_iUnion : ∀ {ι : Type u_1} {X : Type u_2} (S : ι → Set X) {κ : Cardinal.{u_3}} [Fact κ.IsRegular],
  HasCardinalLT ι κ → (∀ (i : ι), HasCardinalLT (↑(S i)) κ) → HasCardinalLT (↑(⋃ i, S i)) κ
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- In an open set, the iterated derivative within this set coincides with the global iterated
derivative.  -/
iteratedFDerivWithin_of_isOpen : ∀ {𝕜 : 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 : ℕ), IsOpen s → Set.EqOn (iteratedFDerivWithin 𝕜 n f s) (iteratedFDeriv 𝕜 n f) s
-- Mathlib.MeasureTheory.OuterMeasure.Operations
MeasureTheory.OuterMeasure.top_apply' : ∀ {α : Type u_1} (s : Set α), ⊤ s = ⨅ (_ : s = ∅), 0
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findM?.eq_1 : ∀ {m : Type → Type u} [inst : Monad m] {α : Type} (p : α → m Bool), List.findM? p [] = pure none
-- Mathlib.Order.Interval.Set.Basic
Set.mem_Ico_of_Ioo : ∀ {α : Type u_1} [inst : Preorder α] {a b x : α}, x ∈ Set.Ioo a b → x ∈ Set.Ico a b
-- Init.Data.List.Nat.Pairwise
List.pairwise_iff_getElem : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α},
  List.Pairwise R l ↔ ∀ (i j : ℕ) (_hi : i < l.length) (_hj : j < l.length), i < j → R l[i] l[j]
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.ConnectedComponent.map_comp : ∀ {V : Type u} {V' : Type v} {V'' : Type w} {G : SimpleGraph V} {G' : SimpleGraph V'} {G'' : SimpleGraph V''}
  (C : G.ConnectedComponent) (φ : G →g G') (ψ : G' →g G''),
  SimpleGraph.ConnectedComponent.map ψ (SimpleGraph.ConnectedComponent.map φ C) =
    SimpleGraph.ConnectedComponent.map (ψ.comp φ) C
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBy_le_torsionBy_of_dvd : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (a b : R),
  a ∣ b → Submodule.torsionBy R M a ≤ Submodule.torsionBy R M b
-- Mathlib.Order.Bounds.Basic
isLeast_bot_iff : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α} [inst_1 : OrderBot α], IsLeast s ⊥ ↔ ⊥ ∈ s
-- Batteries.Data.List.Perm
List.Perm.idxBij_idxBij_symm : ∀ {α : Type u_1} [inst : BEq α] [inst_1 : LawfulBEq α] {xs ys : List α} (h : xs.Perm ys) {i : Fin ys.length},
  h.idxBij (⋯.idxBij i) = i
-- Mathlib.Algebra.Group.Equiv.Defs
AddEquiv.self_comp_symm : ∀ {M : Type u_4} {N : Type u_5} [inst : Add M] [inst_1 : Add N] (e : M ≃+ N), ⇑e ∘ ⇑e.symm = id
-- Mathlib.Analysis.Convex.Integral
/-- If `μ` is a non-zero finite measure on `α`, `s` is a convex set in `E`, and `f` is an integrable
function sending `μ`-a.e. points to `s`, then the average value of `f` belongs to `closure s`:
`⨍ x, f x ∂μ ∈ s`. See also `Convex.centerMass_mem` for a finite sum version of this lemma.  -/
Convex.set_average_mem_closure : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [CompleteSpace E] {μ : MeasureTheory.Measure α} {s : Set E} {t : Set α} {f : α → E},
  Convex ℝ s →
    μ t ≠ 0 →
      μ t ≠ ⊤ →
        (∀ᵐ (x : α) ∂μ.restrict t, f x ∈ s) → MeasureTheory.IntegrableOn f t μ → ⨍ (x : α) in t, f x ∂μ ∈ closure s
-- Mathlib.AlgebraicTopology.Quasicategory.InnerFibration
SSet.innerHornInclusions_le_J : SSet.innerHornInclusions ≤ SSet.modelCategoryQuillen.J
-- Mathlib.Data.Sigma.Basic
Sigma.mk.inj_iff : ∀ {α : Type u_1} {β : α → Type u_4} {a₁ a₂ : α} {b₁ : β a₁} {b₂ : β a₂}, ⟨a₁, b₁⟩ = ⟨a₂, b₂⟩ ↔ a₁ = a₂ ∧ b₁ ≍ b₂
-- Mathlib.Algebra.Homology.LeftResolution.Basic
/-- a functor which sends `X : A` to an object `F.obj X` with an epimorphism
`π.app X : ι.obj (F.obj X) ⟶ X`  -/
CategoryTheory.Abelian.LeftResolution.F : {A : Type u_1} →
  {C : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_2} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_1} A] →
        {ι : CategoryTheory.Functor C A} → CategoryTheory.Abelian.LeftResolution ι → CategoryTheory.Functor A C
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.coe_of : ∀ {X : Type u_1} (to_prod : X × X), (Bipointed.of to_prod).X = X
-- Mathlib.Data.Ordmap.Ordnode
/-- O(log n). Remove an element from the set equivalent to `x`. Does nothing if there
is no such element.

```
erase 1 {1, 2, 3} = {2, 3}
erase 4 {1, 2, 3} = {1, 2, 3}
```

Using a preorder on `ℕ × ℕ` that only compares the first coordinate:

```
erase (1, 1) {(0, 1), (1, 2)} = {(0, 1)}
erase (3, 1) {(0, 1), (1, 2)} = {(0, 1), (1, 2)}
```  -/
Ordnode.erase : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → α → Ordnode α → Ordnode α
-- Lean.Meta.Match.Basic
Lean.Meta.Match.Example.replaceFVarId : Lean.FVarId → Lean.Meta.Match.Example → Lean.Meta.Match.Example → Lean.Meta.Match.Example
-- Mathlib.GroupTheory.Index
AddSubgroup.card_eq_one : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G}, Nat.card ↥H = 1 ↔ H = ⊥
-- Mathlib.LinearAlgebra.CliffordAlgebra.CategoryTheory
/-- The "clifford algebra" functor, sending a quadratic `R`-module `V` to the clifford algebra on
`V`.

This is `CliffordAlgebra.map` through the lens of category theory.  -/
QuadraticModuleCat.cliffordAlgebra : {R : Type u} → [inst : CommRing R] → CategoryTheory.Functor (QuadraticModuleCat R) (AlgCat R)
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.shiftFunctorAdd'_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (t : CategoryTheory.TwistShiftData C A) (i j k : A) (h : i + j = k)
  (X : t.Category),
  (CategoryTheory.shiftFunctorAdd' t.Category i j k h).hom.app X =
    ↑(t.z i j) •
      CategoryTheory.CategoryStruct.comp ((t.shiftIso k).hom.app X)
        (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctorAdd' C i j k h).hom.app X)
          (CategoryTheory.CategoryStruct.comp ((CategoryTheory.shiftFunctor C j).map ((t.shiftIso i).inv.app X))
            ((t.shiftIso j).inv.app ((CategoryTheory.shiftFunctor t.Category i).obj X))))
-- Init.Data.Int.Order
Int.not_lt_of_ge : ∀ {a b : ℤ}, b ≤ a → ¬a < b
-- Mathlib.Analysis.SpecialFunctions.Arsinh
Real.hasStrictDerivAt_arsinh : ∀ (x : ℝ), HasStrictDerivAt Real.arsinh (√(1 + x ^ 2))⁻¹ x
-- Mathlib.Topology.DerivedSet
/-- The relative derived set operator viewed as a monotone self-map of `Set X`.  -/
relDerivedSet : {X : Type u_1} → [TopologicalSpace X] → Set X →o Set X
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroObjects
/-- The (unique) isomorphism between any terminal object and the zero object.  -/
CategoryTheory.Limits.HasZeroObject.zeroIsoIsTerminal : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] → {X : C} → CategoryTheory.Limits.IsTerminal X → (0 ≅ X)
-- Lean.Language.Basic
/-- Snapshot type without child nodes.  -/
Lean.Language.SnapshotLeaf : Type
-- Lean.Widget.InteractiveGoal
_private.Lean.Widget.InteractiveGoal.0.Lean.Widget.InteractiveGoalCore.pretty.addLine : Std.Format → Std.Format
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.withBotDegree_le_withBotDegree_iff_of_ne_zero : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R)
  {g : MvPolynomial σ R},
  g ≠ 0 →
    (m.toWithBotSyn (m.withBotDegree f) ≤ m.toWithBotSyn (m.withBotDegree g) ↔
      m.toSyn (m.degree f) ≤ m.toSyn (m.degree g))
-- Mathlib.Order.UpperLower.Relative
IsRelLowerSet.sInter : ∀ {α : Type u_1} {P : α → Prop} [inst : LE α] {S : Set (Set α)},
  S.Nonempty → (∀ s ∈ S, IsRelLowerSet s P) → IsRelLowerSet (⋂₀ S) P
-- Mathlib.Algebra.Algebra.Equiv
AlgEquiv.instCoeOutRingEquiv : {R : Type uR} →
  {A₁ : Type uA₁} →
    {A₂ : Type uA₂} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A₁] →
          [inst_2 : Semiring A₂] → [inst_3 : Algebra R A₁] → [inst_4 : Algebra R A₂] → CoeOut (A₁ ≃ₐ[R] A₂) (A₁ ≃+* A₂)
-- Mathlib.Algebra.Order.SuccPred
Order.le_two_iff : ∀ {α : Type u_1} {x : α} [inst : LinearOrder α] [inst_1 : AddMonoidWithOne α] [SuccAddOrder α] [IsBotZeroClass α]
  [NeZero 1] [NoMaxOrder α], x ≤ 2 ↔ x = 0 ∨ x = 1 ∨ x = 2
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.RootsExtrema
Polynomial.Chebyshev.eval_T_real_mem_Icc : ∀ (n : ℤ) {x : ℝ}, x ∈ Set.Icc (-1) 1 → Polynomial.eval x (Polynomial.Chebyshev.T ℝ n) ∈ Set.Icc (-1) 1
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
edist_lt_coe : ∀ {α : Type u} [inst : PseudoMetricSpace α] {x y : α} {c : NNReal}, edist x y < ↑c ↔ nndist x y < c
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.isSome_maxKey?_eq_not_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp],
  t.maxKey?.isSome = !t.isEmpty
-- Mathlib.GroupTheory.MonoidLocalization.Finite
/-- The Grothendieck group of a finitely generated monoid is finitely generated.  -/
Algebra.GrothendieckAddGroup.instFG : ∀ {M : Type u_1} [inst : AddCommMonoid M] [AddMonoid.FG M], AddMonoid.FG (Algebra.GrothendieckAddGroup M)
-- Mathlib.LinearAlgebra.Complex.Module
nonpos_iff_realPart_imaginaryPart : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : StarRing A] [inst_2 : PartialOrder A] [StarOrderedRing A]
  [inst_4 : Module ℂ A] [inst_5 : StarModule ℂ A] {a : A}, a ≤ 0 ↔ realPart a ≤ 0 ∧ imaginaryPart a = 0
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.toSubmodule_eq_bot : ∀ {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), ↑N = ⊥ ↔ N = ⊥
-- Init.Data.Vector.Algebra
Vector.smul_add : ∀ {β : Type u_1} {α : Type u_2} {n : ℕ} [inst : Add β] [inst_1 : SMul α β],
  (∀ (c : α) (x y : β), c • (x + y) = c • x + c • y) → ∀ (c : α) (xs ys : Vector β n), c • (xs + ys) = c • xs + c • ys
-- Mathlib.Algebra.Ring.Subsemiring.MulOpposite
Subsemiring.unop_op : ∀ {R : Type u_2} [inst : NonAssocSemiring R] (S : Subsemiring R), S.op.unop = S
-- Mathlib.Topology.Algebra.Module.Spaces.WeakBilin
/-- Map `F` into the topological dual of `E` with the weak topology induced by `F`
 -/
WeakBilin.eval : {𝕜 : Type u_2} →
  {E : Type u_4} →
    {F : Type u_5} →
      [inst : TopologicalSpace 𝕜] →
        [inst_1 : CommSemiring 𝕜] →
          [inst_2 : AddCommMonoid E] →
            [inst_3 : Module 𝕜 E] →
              [inst_4 : AddCommMonoid F] →
                [inst_5 : Module 𝕜 F] →
                  (B : E →ₗ[𝕜] F →ₗ[𝕜] 𝕜) →
                    [inst_6 : ContinuousAdd 𝕜] → [inst_7 : ContinuousConstSMul 𝕜 𝕜] → F →ₗ[𝕜] StrongDual 𝕜 (WeakBilin B)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey?_insertManyIfNewUnit_list_of_not_mem_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeMap α Unit cmp} [Std.TransCmp cmp] [inst : BEq α]
  [Std.LawfulBEqCmp cmp] {l : List α} {k : α}, k ∉ t → l.contains k = false → (t.insertManyIfNewUnit l).getKey? k = none
-- Std.Data.String.ToNat
_private.Std.Data.String.ToNat.0.NoRepetition.mk : ∀ {α : Type u} {a : α} {l : List α}, ¬[a, a] <:+: l → NoRepetition✝ a l
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.expandModuleHierarchyImportedBy : ℕ → Lean.Lsp.DocumentUri → Lean.Lsp.Ipc.IpcM (Option Lean.Lsp.Ipc.ModuleHierarchy × ℕ)
-- Mathlib.LinearAlgebra.AffineSpace.Midpoint
midpoint_neg_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 : V), midpoint R (-x) x = 0
-- Init.Data.List.Erase
List.length_eraseP : ∀ {α : Type u_1} {p : α → Bool} {l : List α},
  (List.eraseP p l).length = if l.any p = true then l.length - 1 else l.length
-- Lean.Meta.Tactic.Grind.EMatchTheorem
/-- Helper type for generating suggestions for `grind` parameters  -/
Lean.Meta.Grind.MinIndexableMode : Type
-- Mathlib.Combinatorics.Quiver.SingleObj
/-- The single object in `SingleObj α`.  -/
Quiver.SingleObj.star : (α : Type u_1) → Quiver.SingleObj α
-- Init.Core
mt : ∀ {a b : Prop}, (a → b) → ¬b → ¬a
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.ext_iff : ∀ {X Y : AddGrpCat} {f g : X ⟶ Y},
  f = g ↔ ∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x
-- Mathlib.Analysis.Calculus.FDeriv.Bilinear
ContinuousLinearMap.hasStrictFDerivAt_of_bilinear : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {G' : Type u_5} [inst_7 : NormedAddCommGroup G']
  [inst_8 : NormedSpace 𝕜 G'] (B : E →L[𝕜] F →L[𝕜] G) {f : G' → E} {g : G' → F} {f' : G' →L[𝕜] E} {g' : G' →L[𝕜] F}
  {x : G'},
  HasStrictFDerivAt f f' x →
    HasStrictFDerivAt g g' x →
      HasStrictFDerivAt (fun y => (B (f y)) (g y))
        (((ContinuousLinearMap.precompR G' B) (f x)) g' + ((ContinuousLinearMap.precompL G' B) f') (g x)) x
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.TStructure
CategoryTheory.HasExt.instHasSmallLocalizedShiftedHomHomologicalComplexIntUpQuasiIsoOfIsGEOfIsLEOfNat : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] [CategoryTheory.HasExt C]
  (K L : CochainComplex C ℤ) [K.IsGE 0] [K.IsLE 0] [L.IsGE 0] [L.IsLE 0],
  CategoryTheory.Localization.HasSmallLocalizedShiftedHom (HomologicalComplex.quasiIso C (ComplexShape.up ℤ)) ℤ K L
-- Mathlib.Algebra.Order.Interval.Basic
NonemptyInterval.instPow : {α : Type u_2} →
  [inst : Monoid α] → [inst_1 : Preorder α] → [MulLeftMono α] → [MulRightMono α] → Pow (NonemptyInterval α) ℕ
-- Mathlib.Logic.Function.Defs
Function.dcomp_eq_comp : ∀ {α : Sort u_3} {β : Sort u_4} {γ : Sort u_5} (f : β → γ) (g : α → β), (fun {x} => f) ∘' g = f ∘ g
-- Mathlib.Algebra.Order.GroupWithZero.Synonym
Lex.instGroupWithZero : {α : Type u_1} → [GroupWithZero α] → GroupWithZero (Lex α)
-- Mathlib.Algebra.Algebra.Opposite
/-- An algebra homomorphism `f : A →ₐ[R] B` such that `f x` commutes with `f y` for all `x, y` defines
an algebra homomorphism to `Bᵐᵒᵖ`.  -/
AlgHom.toOpposite : {R : Type u_1} →
  {A : Type u_3} →
    {B : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Semiring B] →
            [inst_3 : Algebra R A] →
              [inst_4 : Algebra R B] → (f : A →ₐ[R] B) → (∀ (x y : A), Commute (f x) (f y)) → A →ₐ[R] Bᵐᵒᵖ
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.Sentence.realize_sup : ∀ {L : FirstOrder.Language} (M : Type w) [inst : L.Structure M] {φ ψ : L.Sentence}, M ⊨ φ ⊔ ψ ↔ M ⊨ φ ∨ M ⊨ ψ
-- Std.Data.HashMap.IteratorLemmas
_private.Std.Data.HashMap.IteratorLemmas.0.Std.HashMap.keys_inner : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap α β}, m.inner.keys = m.keys
-- Mathlib.Analysis.Calculus.FDeriv.Prod
fderivWithin_pi : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {x : E} {s : Set E} {ι : Type u_6} {F' : ι → Type u_7}
  [inst_3 : (i : ι) → NormedAddCommGroup (F' i)] [inst_4 : (i : ι) → NormedSpace 𝕜 (F' i)] {φ : (i : ι) → E → F' i},
  (∀ (i : ι), DifferentiableWithinAt 𝕜 (φ i) s x) →
    UniqueDiffWithinAt 𝕜 s x →
      fderivWithin 𝕜 (fun x i => φ i x) s x = ContinuousLinearMap.pi fun i => fderivWithin 𝕜 (φ i) s x
-- Mathlib.Algebra.Notation.Prod
Prod.star_def : ∀ {R : Type u_6} {S : Type u_7} [inst : Star R] [inst_1 : Star S] (x : R × S), star x = (star x.1, star x.2)
-- Mathlib.CategoryTheory.Preadditive.Injective.Basic
CategoryTheory.Injective.iso_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : C} (i : P ≅ Q),
  CategoryTheory.Injective P ↔ CategoryTheory.Injective Q
-- Mathlib.Topology.Algebra.GroupWithZero
tendsto_inv_iff₀ : ∀ {α : Type u_1} {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : TopologicalSpace G₀] [ContinuousInv₀ G₀] {x : G₀}
  {l : Filter α} {f : α → G₀}, x ≠ 0 → (Filter.Tendsto (fun x => (f x)⁻¹) l (nhds x⁻¹) ↔ Filter.Tendsto f l (nhds x))
-- Mathlib.Combinatorics.Matroid.Circuit
/-- A version of `Matroid.dep_iff_superset_isCircuit` that has the ground-set hypothesis
as part of the equivalence, rather than a hypothesis.  -/
Matroid.dep_iff_superset_isCircuit' : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.Dep X ↔ (∃ C ⊆ X, M.IsCircuit C) ∧ X ⊆ M.E
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.instFaithfulCommMonForget₂CommMon : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C], (CategoryTheory.CommGrp.forget₂CommMon C).Faithful
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValue_modifyKey : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : EquivBEq α] {k k' : α} {f : β → β} (l : List ((_ : α) × β)),
  Std.Internal.List.DistinctKeys l →
    ∀ (h : Std.Internal.List.containsKey k' (Std.Internal.List.Const.modifyKey k f l) = true),
      Std.Internal.List.getValue k' (Std.Internal.List.Const.modifyKey k f l) h =
        if heq : (k == k') = true then f (Std.Internal.List.getValue k l ⋯) else Std.Internal.List.getValue k' l ⋯