mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.CStarAlgebra.Matrix
entry_norm_bound_of_unitary : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {U : Matrix n n 𝕜},
  U ∈ Matrix.unitaryGroup n 𝕜 → ∀ (i j : n), ‖U i j‖ ≤ 1
-- Mathlib.Data.PFun
PFun.mem_prodLift : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α →. β} {g : α →. γ} {x : α} {y : β × γ},
  y ∈ f.prodLift g x ↔ y.1 ∈ f x ∧ y.2 ∈ g x
-- Init.Data.List.Find
List.findIdx_append : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α},
  List.findIdx p (l₁ ++ l₂) = if List.findIdx p l₁ < l₁.length then List.findIdx p l₁ else List.findIdx p l₂ + l₁.length
-- Mathlib.CategoryTheory.Shift.Adjunction
/-- The commutation isomorphisms of `Adjunction.LeftAdjointCommShift.iso` are compatible with
the unit of the adjunction.
 -/
CategoryTheory.Adjunction.LeftAdjointCommShift.compatibilityUnit_iso : ∀ {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] {F : CategoryTheory.Functor C D} {G : CategoryTheory.Functor D C}
  (adj : F ⊣ G) {A : Type u_3} [inst_2 : AddGroup A] [inst_3 : CategoryTheory.HasShift C A]
  [inst_4 : CategoryTheory.HasShift D A] [inst_5 : G.CommShift A] (a : A),
  CategoryTheory.Adjunction.CommShift.CompatibilityUnit adj (CategoryTheory.Adjunction.LeftAdjointCommShift.iso adj a)
    (CategoryTheory.Functor.commShiftIso G a)
-- Mathlib.Data.List.Cycle
_private.Mathlib.Data.List.Cycle.0.List.prev.match_1.eq_3 : ∀ {α : Type u_1} (motive : (x : List α) → (x_1 : α) → x_1 ∈ x → Sort u_2) (y z : α) (xs : List α) (x : α)
  (h : x ∈ y :: z :: xs) (h_1 : (x : α) → (h : x ∈ []) → motive [] x h)
  (h_2 : (y x : α) → (x_1 : x ∈ [y]) → motive [y] x x_1)
  (h_3 : (y z : α) → (xs : List α) → (x : α) → (h : x ∈ y :: z :: xs) → motive (y :: z :: xs) x h),
  (match y :: z :: xs, x, h with
    | [], x, h => h_1 x h
    | [y], x, x_1 => h_2 y x x_1
    | y :: z :: xs, x, h => h_3 y z xs x h) =
    h_3 y z xs x h
-- Mathlib.GroupTheory.Sylow
Sylow.smul_eq_iff_mem_normalizer : ∀ {p : ℕ} {G : Type u_1} [inst : Group G] {g : G} {P : Sylow p G}, g • P = P ↔ g ∈ Subgroup.normalizer ↑P
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_7 : HAdd Std.Time.Millisecond.Offset Std.Time.Second.Offset Std.Time.Millisecond.Offset
-- Mathlib.Analysis.Calculus.FDeriv.ContinuousAlternatingMap
ContinuousAlternatingMap.hasStrictFDerivAt_toContinuousMultilinearMap_comp_iff : ∀ {𝕜 : Type u_1} {ι : Type u_2} {E : Type u_3} {G : Type u_5} {H : Type u_6} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup G] [inst_4 : NormedSpace 𝕜 G]
  [inst_5 : NormedAddCommGroup H] [inst_6 : NormedSpace 𝕜 H] {f : E → G [⋀^ι]→L[𝕜] H} {f' : E →L[𝕜] G [⋀^ι]→L[𝕜] H}
  {x : E} [Finite ι],
  HasStrictFDerivAt (ContinuousAlternatingMap.toContinuousMultilinearMap ∘ f)
      (ContinuousAlternatingMap.toContinuousMultilinearMapCLM 𝕜 ∘SL f') x ↔
    HasStrictFDerivAt f f' x
-- Mathlib.Algebra.Group.Action.Faithful
FaithfulVAdd.mk : ∀ {G : Type u_4} {P : Type u_5} [inst : VAdd G P],
  (∀ {g₁ g₂ : G}, (∀ (p : P), g₁ +ᵥ p = g₂ +ᵥ p) → g₁ = g₂) → FaithfulVAdd G P
-- Mathlib.Analysis.Convex.Star
/-- If `x < y`, then `(Set.Ici y)ᶜ` is star convex at `x`.  -/
starConvex_compl_Ici : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : PartialOrder E] [IsOrderedAddMonoid E] [inst_5 : Module 𝕜 E] [IsStrictOrderedModule 𝕜 E]
  [PosSMulReflectLT 𝕜 E] {x y : E}, x < y → StarConvex 𝕜 x (Set.Ici y)ᶜ
-- Mathlib.CategoryTheory.Functor.Derived.LeftDerived
CategoryTheory.Functor.leftDerivedNatTrans_fac : ∀ {C : Type u_1} {D : Type u_3} {H : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} D] [inst_2 : CategoryTheory.Category.{v_5, u_2} H]
  (LF' LF : CategoryTheory.Functor D H) {F F' : CategoryTheory.Functor C H} {L : CategoryTheory.Functor C D}
  (α' : L.comp LF' ⟶ F') (α : L.comp LF ⟶ F) (W : CategoryTheory.MorphismProperty C) [inst_3 : L.IsLocalization W]
  [inst_4 : LF.IsLeftDerivedFunctor α W] (τ : F' ⟶ F),
  CategoryTheory.CategoryStruct.comp (L.whiskerLeft (LF'.leftDerivedNatTrans LF α' α W τ)) α =
    CategoryTheory.CategoryStruct.comp α' τ
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsPath.of_map : ∀ {V : Type u} {V' : Type v} {G : SimpleGraph V} {G' : SimpleGraph V'} {f : G →g G'} {u v : V} {p : G.Walk u v},
  (SimpleGraph.Walk.map f p).IsPath → p.IsPath
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.unitCompPartialBijectiveAux.eq_1 : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {i : CategoryTheory.Functor D C} [inst_2 : CategoryTheory.Reflective i] (A : C) (B : D),
  CategoryTheory.unitCompPartialBijectiveAux A B =
    ((CategoryTheory.reflectorAdjunction i).homEquiv A B).symm.trans
      (CategoryTheory.Functor.FullyFaithful.ofFullyFaithful i).homEquiv
-- Mathlib.Topology.Piecewise
continuousAt_update_same : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {x : α}
  [inst_2 : DecidableEq α] {y : β},
  ContinuousAt (Function.update f x y) x ↔ Filter.Tendsto f (nhdsWithin x {x}ᶜ) (nhds y)
-- Mathlib.AlgebraicTopology.SimplicialSet.TopAdj
SimplexCategory.toTopHomeo_naturality_apply : ∀ {n m : SimplexCategory} (f : n ⟶ m) (x : ↑(SSet.toTop.obj (SSet.stdSimplex.obj n))),
  m.toTopHomeo ((CategoryTheory.ConcreteCategory.hom (SSet.toTop.map (SSet.stdSimplex.map f))) x) =
    stdSimplex.map (⇑(CategoryTheory.ConcreteCategory.hom f)) (n.toTopHomeo x)
-- Std.Async.Signal
/-- Termination signal.

Notes:
- On Windows, watchers can be created for SIGTERM, but they never receive the signal.
 -/
Std.Async.Signal.sigterm : Std.Async.Signal
-- Mathlib.Order.SuccPred.Tree
/-- The type should have a bottom, the root.  -/
RootedTree.orderBot : (self : RootedTree) → OrderBot ↑self
-- Mathlib.GroupTheory.Coxeter.Length
CoxeterSystem.length_simple : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) (i : B),
  cs.length (cs.simple i) = 1
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- The relation on the free groupoid on the underlying *quiver* of C that
promotes the prefunctor `C ⥤q FreeGroupoid C` into a functor
`C ⥤ Quotient (FreeGroupoid.homRel C)`.  -/
CategoryTheory.FreeGroupoid.homRel : (C : Type u) → [inst : CategoryTheory.Category.{v, u} C] → HomRel (Quiver.FreeGroupoid C)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The sum of an antitone function and a strictly antitone function is
strictly antitone.  -/
Antitone.add_strictAnti : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] [AddLeftStrictMono α]
  [AddRightMono α] {f g : β → α}, Antitone f → StrictAnti g → StrictAnti fun x => f x + g x
-- Mathlib.Topology.Covering.Basic
IsCoveringMapOn.eq_1 : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X) (s : Set X),
  IsCoveringMapOn f s = ∀ x ∈ s, IsEvenlyCovered f x ↑(f ⁻¹' {x})
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
/-- The connecting homomorphism of the spectral object.  -/
CategoryTheory.Triangulated.SpectralObject.δ' : {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] →
                  (self : CategoryTheory.Triangulated.SpectralObject C ι) →
                    (CategoryTheory.ComposableArrows.functorArrows ι 1 2 2
                            CategoryTheory.Triangulated.SpectralObject._proof_2
                            CategoryTheory.Triangulated.SpectralObject._proof_4).comp
                        self.ω₁ ⟶
                      (CategoryTheory.ComposableArrows.functorArrows ι 0 1 2
                            CategoryTheory.Triangulated.SpectralObject._proof_6
                            CategoryTheory.Triangulated.SpectralObject._proof_2).comp
                        (self.ω₁.comp (CategoryTheory.shiftFunctor C 1))
-- Mathlib.MeasureTheory.Function.L2Space
MeasureTheory.L2.innerProductSpace : {α : Type u_1} →
  {E : Type u_2} →
    {𝕜 : Type u_4} →
      [inst : RCLike 𝕜] →
        {m : MeasurableSpace α} →
          {μ : MeasureTheory.Measure α} →
            [inst_1 : NormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → InnerProductSpace 𝕜 ↥(MeasureTheory.Lp E 2 μ)
-- Mathlib.Topology.Constructions.SumProd
continuousAt_fst : ∀ {X : Type u} {Y : Type v} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {p : X × Y},
  ContinuousAt Prod.fst p
-- Mathlib.Tactic.Conv
/-- `conv in pat => cs` runs the `conv` tactic sequence `cs`
on the first subexpression matching the pattern `pat` in the target.
The converted expression becomes the new target subgoal, like `conv => cs`.

The arguments `in` are the same as those as the in `pattern`.
In fact, `conv in pat => cs` is a macro for `conv => pattern pat; cs`.

The syntax also supports the `occs` clause. Example:
```lean
conv in (occs := *) x + y => rw [add_comm]
```
 -/
Mathlib.Tactic.Conv.«convConvIn__=>_» : Lean.ParserDescr
-- Mathlib.Topology.Algebra.TopologicallyNilpotent
/-- The topological nilradical of a ring with a linear topology  -/
topologicalNilradical : (R : Type u_1) → [inst : TopologicalSpace R] → [inst_1 : CommRing R] → [IsLinearTopology R R] → Ideal R
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.CompactOpens.isOpen' : ∀ {α : Type u_4} [inst : TopologicalSpace α] (self : TopologicalSpace.CompactOpens α), IsOpen self.carrier
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
NonUnitalSubsemiring.closure_le_centralizer_centralizer : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] (s : Set R),
  NonUnitalSubsemiring.closure s ≤ NonUnitalSubsemiring.centralizer ↑(NonUnitalSubsemiring.centralizer s)
-- Lean.DocString.Parser
/-- Match an arbitrary Parser and return the consumed String in a `Syntax.atom`.  -/
Lean.Doc.Parser.asStringFn : Lean.Parser.ParserFn → optParam Bool false → optParam (String → String) id → Lean.Parser.ParserFn
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.cycleGraph_isContained_iff : ∀ {V : Type u_1} {G : SimpleGraph V} {n : ℕ},
  2 < n → ((SimpleGraph.cycleGraph n).IsContained G ↔ ∃ v p, p.IsCycle ∧ p.length = n)
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.trNum.eq_1 : Turing.PartrecToTM2.trNum Num.zero = []
-- Mathlib.Analysis.Convex.StdSimplex
instPathConnectedSpaceElemForallRealStdSimplexOfNonempty : ∀ (ι : Type u_1) [inst : Fintype ι] [Nonempty ι], PathConnectedSpace ↑(stdSimplex ℝ ι)
-- Mathlib.CategoryTheory.Limits.Shapes.WideEqualizers
/-- This is a helper construction that can be useful when verifying that a category has all
coequalizers. Given `F : WalkingParallelFamily ⥤ C`, which is really the same as
`parallelFamily (fun j ↦ F.map (line j))`, and a cotrident on `fun j ↦ F.map (line j)` we get a
cocone on `F`.

If you're thinking about using this, have a look at
`hasWideCoequalizers_of_hasColimit_parallelFamily`, which you may find to be an easier way
of achieving your goal.  -/
CategoryTheory.Limits.Cocone.ofCotrident : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      {F : CategoryTheory.Functor (CategoryTheory.Limits.WalkingParallelFamily J) C} →
        (CategoryTheory.Limits.Cotrident fun j => F.map (CategoryTheory.Limits.WalkingParallelFamily.Hom.line j)) →
          CategoryTheory.Limits.Cocone F
-- Mathlib.CategoryTheory.Retract
CategoryTheory.Retract.map_r : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {X Y : C} (h : CategoryTheory.Retract X Y) (F : CategoryTheory.Functor C D), (h.map F).r = F.map h.r
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.Measure.toSignedMeasure_apply : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) [hμ : MeasureTheory.IsFiniteMeasure μ]
  (i : Set α), μ.toSignedMeasure i = if MeasurableSet i then μ.real i else 0
-- Mathlib.Algebra.GCDMonoid.Finset
Finset.lcm_mono : ∀ {α : Type u_2} {β : Type u_3} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] {s₁ s₂ : Finset β}
  {f : β → α}, s₁ ⊆ s₂ → s₁.lcm f ∣ s₂.lcm f
-- Mathlib.Data.Set.Finite.Basic
Set.Subsingleton.finite : ∀ {α : Type u} {s : Set α}, s.Subsingleton → s.Finite
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.coe_coeffs_map : ∀ {R : Type u} {S₁ : Type v} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : CommSemiring S₁] (f : R →+* S₁)
  (p : MvPolynomial σ R), ↑((MvPolynomial.map f) p).coeffs ⊆ ⇑f '' ↑p.coeffs
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
/-- Simple function seen as simple function of a larger `MeasurableSpace`.  -/
MeasureTheory.SimpleFunc.toLargerSpace : {β : Type u_6} →
  {γ : Type u_7} → {m m0 : MeasurableSpace β} → m ≤ m0 → MeasureTheory.SimpleFunc β γ → MeasureTheory.SimpleFunc β γ
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.brecOn.eq : ∀ {motive_1 : Lean.IR.IRType → Sort u} {motive_2 : Array Lean.IR.IRType → Sort u}
  {motive_3 : List Lean.IR.IRType → Sort u} (t : Lean.IR.IRType) (F_1 : (t : Lean.IR.IRType) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.IR.IRType) → Lean.IR.IRType.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.IR.IRType) → Lean.IR.IRType.below_2 t → motive_3 t),
  t.brecOn F_1 F_2 F_3 = F_1 t (Lean.IR.IRType.brecOn.go t F_1 F_2 F_3).2
-- Mathlib.Analysis.Complex.OperatorNorm
Complex.ofRealCLM_nnnorm : ‖Complex.ofRealCLM‖₊ = 1
-- Mathlib.Tactic.Linarith.Preprocessing
/-- `removeNe` case splits on any proof `h : a ≠ b` in the input, turning it into `a < b ∨ a > b`,
by calling `linarith.removeNeAux`, provided the type has a `LinearOrder` instance.
This produces `2^n` branches when there are `n` such hypotheses in the input.
 -/
Mathlib.Tactic.Linarith.removeNe : Mathlib.Tactic.Linarith.GlobalBranchingPreprocessor
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isSome_max?_of_isSome_max?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).max?.isSome = true → t.max?.isSome = true
-- Std.Do.SPred.SPred
Std.Do.SPred.and_cons : ∀ {σs : List (Type u)} {σ : Type u} {s : σ} {P Q : Std.Do.SPred (σ :: σs)}, spred(P ∧ Q) s = spred(P s ∧ Q s)
-- Mathlib.Topology.Algebra.MulAction
/-- If an action is continuous, then composing this action with a continuous homomorphism gives
again a continuous action.  -/
MulAction.continuousSMul_compHom : ∀ {M : Type u_1} {X : Type u_2} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X] [inst_2 : Monoid M]
  [inst_3 : MulAction M X] [ContinuousSMul M X] {N : Type u_5} [inst_5 : TopologicalSpace N] [inst_6 : Monoid N]
  {f : N →* M}, Continuous ⇑f → ContinuousSMul N X
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.eq_1 : ∀ (M : Type u_1), Mᵈᵃᵃ = Mᵃᵒᵖ
-- Mathlib.AlgebraicGeometry.PullbackCarrier
AlgebraicGeometry.Scheme.exists_preimage_of_isPullback : ∀ {P X Y Z : AlgebraicGeometry.Scheme} {fst : P ⟶ X} {snd : P ⟶ Y} {f : X ⟶ Z} {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g → ∀ (x : ↥X) (y : ↥Y), f x = g y → ∃ p, fst p = x ∧ snd p = y
-- Mathlib.CategoryTheory.Sites.Sheafification
/-- A sheaf `P` is isomorphic to its own sheafification.  -/
CategoryTheory.sheafificationIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {D : Type u_1} →
        [inst_1 : CategoryTheory.Category.{v_1, u_1} D] →
          [inst_2 : CategoryTheory.HasWeakSheafify J D] →
            (P : CategoryTheory.Sheaf J D) → P ≅ (CategoryTheory.presheafToSheaf J D).obj P.obj
-- Init.Data.List.Nat.Range
List.not_mem_range_self : ∀ {n : ℕ}, n ∉ List.range n
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.BraidedCategory.yang_baxter : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y Z : C),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Y Z).inv
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Y).hom Z)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y X Z).hom
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Y (β_ X Z).hom)
            (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Y Z X).inv
              (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ Y Z).hom X)
                (CategoryTheory.MonoidalCategoryStruct.associator Z Y X).hom))))) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerLeft X (β_ Y Z).hom)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator X Z Y).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.whiskerRight (β_ X Z).hom Y)
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.associator Z X Y).hom
            (CategoryTheory.MonoidalCategoryStruct.whiskerLeft Z (β_ X Y).hom))))
-- Init.Data.List.Attach
List.head_attachWith : ∀ {α : Type u_1} {P : α → Prop} {xs : List α} {H : ∀ a ∈ xs, P a} (h : xs.attachWith P H ≠ []),
  (xs.attachWith P H).head h = ⟨xs.head ⋯, ⋯⟩
-- Mathlib.CategoryTheory.Triangulated.Pretriangulated
CategoryTheory.Pretriangulated.instHasFiniteProducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [hC : CategoryTheory.Pretriangulated C],
  CategoryTheory.Limits.HasFiniteProducts C
-- Init.Data.AC
Lean.Data.AC.sort.loop.eq_2 : ∀ (a : List ℕ) (x_2 : ℕ) (xs : List ℕ),
  Lean.Data.AC.sort.loop a (x_2 :: xs) = Lean.Data.AC.sort.loop (Lean.Data.AC.insert x_2 a) xs
-- Mathlib.Tactic.ClickSuggestions.Util
/-- A global constant.  -/
Mathlib.Tactic.ClickSuggestions.Premise.const : Lean.Name → Mathlib.Tactic.ClickSuggestions.Premise
-- Mathlib.Data.PEquiv
/-- A `PEquiv` is a partial equivalence, a representation of a bijection between a subset
  of `α` and a subset of `β`. See also `PartialEquiv` for a version that requires `toFun` and
`invFun` to be globally defined functions and has `source` and `target` sets as extra fields.  -/
«term_≃._» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Idempotents.FunctorExtension
CategoryTheory.Idempotents.FunctorExtension₁.map_app_f : ∀ {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]
  {F G : CategoryTheory.Functor C (CategoryTheory.Idempotents.Karoubi D)} (φ : F ⟶ G)
  (P : CategoryTheory.Idempotents.Karoubi C),
  ((CategoryTheory.Idempotents.FunctorExtension₁.map φ).app P).f =
    CategoryTheory.CategoryStruct.comp (F.map P.p).f (φ.app P.X).f
-- Mathlib.MeasureTheory.Function.FactorsThrough
/-- If a function `g` is strongly measurable with respect to the pullback along some function `f`,
then there exists some strongly measurable function `h : Y → Z` such that `g = h ∘ f`.  -/
MeasureTheory.StronglyMeasurable.exists_eq_measurable_comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [mY : MeasurableSpace Y] {f : X → Y} {g : X → Z} [Nonempty Z]
  [inst : TopologicalSpace Z] [TopologicalSpace.IsCompletelyMetrizableSpace Z],
  MeasureTheory.StronglyMeasurable g → ∃ h, MeasureTheory.StronglyMeasurable h ∧ g = h ∘ f
-- Mathlib.Algebra.Module.Presentation.Basic
/-- the image in `M` of each variable  -/
Module.Relations.Solution.var : {A : Type u} →
  [inst : Ring A] →
    {relations : Module.Relations A} →
      {M : Type v} → [inst_1 : AddCommGroup M] → [inst_2 : Module A M] → relations.Solution M → relations.G → M
-- Lean.Elab.MutualInductive
/-- Create a local declaration for each inductive type in `rs`, and execute `x params indFVars`, where `params` are the inductive type parameters and
`indFVars` are the new local declarations.
We use the parameters of rs[0].
Note that this method is executed after we executed `checkHeaders` and established all
parameters are compatible.
 -/
_private.Lean.Elab.MutualInductive.0.Lean.Elab.Command.withInductiveLocalDecls : {α : Type} →
  Array Lean.Elab.Command.PreElabHeaderResult →
    (Array Lean.Expr → Array Lean.Expr → Lean.Elab.TermElabM α) → Lean.Elab.TermElabM α
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
/-- **Alias** of `ContinuousLinearMap.toLinearMap_smul`. -/
ContinuousLinearMap.coe_smul : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] {M₂ : Type u_6} [inst_4 : TopologicalSpace M₂]
  [inst_5 : AddCommMonoid M₂] [inst_6 : Module R₁ M₁] [inst_7 : Module R₂ M₂] {S₂ : Type u_9}
  [inst_8 : DistribSMul S₂ M₂] [inst_9 : SMulCommClass R₂ S₂ M₂] [inst_10 : ContinuousConstSMul S₂ M₂] (c : S₂)
  (f : M₁ →SL[σ₁₂] M₂), ↑(c • f) = c • ↑f
-- Mathlib.Order.Ideal
Order.Ideal.instIsCoatomic : ∀ {P : Type u_1} [inst : LE P] [inst_1 : OrderTop P], IsCoatomic (Order.Ideal P)
-- Mathlib.Algebra.Notation.Prod
Prod.mk_one_one : ∀ {M : Type u_3} {N : Type u_4} [inst : One M] [inst_1 : One N], (1, 1) = 1
-- Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
LinearIndependent.span_eq_top_of_card_eq_finrank : ∀ {K : Type u} {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {ι : Type u_1}
  [inst_3 : Fintype ι] [Nonempty ι] {b : ι → V},
  LinearIndependent K b → Fintype.card ι = Module.finrank K V → Submodule.span K (Set.range b) = ⊤
-- Mathlib.MeasureTheory.Measure.ProbabilityMeasure
ProbabilityMeasure.toFiniteMeasure_normalize_eq_self : ∀ {Ω : Type u_1} [inst : Nonempty Ω] {m0 : MeasurableSpace Ω} (μ : MeasureTheory.ProbabilityMeasure Ω),
  μ.toFiniteMeasure.normalize = μ
-- Std.Data.HashSet.Lemmas
Std.HashSet.Equiv.of_toList_perm : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α}, m₁.toList.Perm m₂.toList → m₁.Equiv m₂
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.nat_lt_ofENat : ∀ {m : ℕ} {n : ℕ∞}, ↑m < ↑n ↔ ↑m < n
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.map_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} (R : CategoryTheory.Presieve X),
  CategoryTheory.Presieve.map (CategoryTheory.Functor.id C) R = R
-- Mathlib.Data.Num.Basic
/-- Subtraction of `PosNum`s, where if `a < b`, then `a - b = 1`.  -/
PosNum.sub : PosNum → PosNum → PosNum
-- Mathlib.RingTheory.Extension.Cotangent.Basic
Algebra.Extension.CotangentSpace.map_sub_map : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {P : Algebra.Extension R S}
  {R' : Type u'} {S' : Type v'} [inst_3 : CommRing R'] [inst_4 : CommRing S'] [inst_5 : Algebra R' S']
  {P' : Algebra.Extension R' S'} [inst_6 : Algebra R R'] [inst_7 : Algebra S S'] [inst_8 : Algebra R S']
  [inst_9 : IsScalarTower R R' S'] [inst_10 : IsScalarTower R S S'] (f g : P.Hom P'),
  Algebra.Extension.CotangentSpace.map f - Algebra.Extension.CotangentSpace.map g = ↑S P'.cotangentComplex ∘ₗ f.sub g
-- Std.Data.Internal.List.Associative
Std.Internal.List.minKeyD_le_minKeyD_erase : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      (Std.Internal.List.eraseKey k l).isEmpty = false →
        ∀ {fallback : α},
          (compare (Std.Internal.List.minKeyD l fallback)
                (Std.Internal.List.minKeyD (Std.Internal.List.eraseKey k l) fallback)).isLE =
            true