mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicTopology.SimplicialSet.StrictSegal
SSet.StrictSegal.mk.injEq : ∀ {X : SSet} (spineToSimplex : {n : ℕ} → X.Path n → X.obj (Opposite.op { len := n }))
  (spine_spineToSimplex : ∀ (n : ℕ), X.spine n ∘ spineToSimplex = id)
  (spineToSimplex_spine : ∀ (n : ℕ), spineToSimplex ∘ X.spine n = id)
  (spineToSimplex_1 : {n : ℕ} → X.Path n → X.obj (Opposite.op { len := n }))
  (spine_spineToSimplex_1 : ∀ (n : ℕ), X.spine n ∘ spineToSimplex_1 = id)
  (spineToSimplex_spine_1 : ∀ (n : ℕ), spineToSimplex_1 ∘ X.spine n = id),
  ({ spineToSimplex := spineToSimplex, spine_spineToSimplex := spine_spineToSimplex,
        spineToSimplex_spine := spineToSimplex_spine } =
      { spineToSimplex := spineToSimplex_1, spine_spineToSimplex := spine_spineToSimplex_1,
        spineToSimplex_spine := spineToSimplex_spine_1 }) =
    (spineToSimplex = spineToSimplex_1)
-- Mathlib.Topology.Algebra.StarSubalgebra
/-- The `elemental` generated by a normal element is commutative.  -/
StarAlgebra.elemental.instCommRingSubtypeMemStarSubalgebraOfT2SpaceOfIsStarNormal : {R : Type u_4} →
  {A : Type u_5} →
    [inst : CommRing R] →
      [inst_1 : StarRing R] →
        [inst_2 : TopologicalSpace A] →
          [inst_3 : Ring A] →
            [inst_4 : Algebra R A] →
              [inst_5 : StarRing A] →
                [inst_6 : StarModule R A] →
                  [inst_7 : IsSemitopologicalRing A] →
                    [inst_8 : ContinuousStar A] →
                      [T2Space A] → {x : A} → [IsStarNormal x] → CommRing ↥(StarAlgebra.elemental R x)
-- Mathlib.Data.FinEnum
FinEnum.Finset.enum.eq_def : ∀ {α : Type u} [inst : DecidableEq α] (x : List α),
  FinEnum.Finset.enum x =
    match x with
    | [] => [∅]
    | x :: xs => do
      let r ← FinEnum.Finset.enum xs
      [r, insert x r]
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get!_inter_of_not_mem_right : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} [inst_2 : Inhabited β], k ∉ m₂ → (m₁ ∩ m₂).get! k = default
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintInfo.paddingRight : Lean.Elab.InlayHintInfo → Bool
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.mk_proj_snd' : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  [inst_2 : TopologicalSpace Z] (e : Bundle.Trivialization F proj) {x : Z},
  proj x ∈ e.baseSet → (proj x, (↑e x).2) = ↑e x
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.instLawfulBEqPolyCnstr : LawfulBEq Nat.Internal.Linear.PolyCnstr
-- Mathlib.Algebra.DualQuaternion
Quaternion.snd_imI_dualNumberEquiv_symm : ∀ {R : Type u_1} [inst : CommRing R] (d : DualNumber (Quaternion R)),
  TrivSqZeroExt.snd (Quaternion.dualNumberEquiv.symm d).imI = (TrivSqZeroExt.snd d).imI
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaAddMonObjIsoOfRepresentableBy.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (X : C) (F : CategoryTheory.Functor Cᵒᵖ AddMonCat) (α : (F.comp (CategoryTheory.forget AddMonCat)).RepresentableBy X),
  CategoryTheory.yonedaAddMonObjIsoOfRepresentableBy X F α =
    CategoryTheory.NatIso.ofComponents
      (fun Y =>
        (let __Equiv := α.homEquiv';
          { toEquiv := __Equiv, map_add' := ⋯ }).toAddMonCatIso)
      ⋯
-- Aesop.Stats.Extension
Aesop.StatsExtension : Type
-- Init.Data.SInt.Lemmas
Int16.lt_or_eq_of_le : ∀ {a b : Int16}, a ≤ b → a < b ∨ a = b
-- Mathlib.AlgebraicTopology.DoldKan.NCompGamma
/-- The natural transformation `N₂ ⋙ Γ₂ ⟶ 𝟭 (SimplicialObject C)`.  -/
AlgebraicTopology.DoldKan.Γ₂N₂.natTrans : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasFiniteCoproducts C] →
        AlgebraicTopology.DoldKan.N₂.comp AlgebraicTopology.DoldKan.Γ₂ ⟶
          CategoryTheory.Functor.id (CategoryTheory.Idempotents.Karoubi (CategoryTheory.SimplicialObject C))
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- The signs involved in the symmetry isomorphism of the total complex.  -/
ComplexShape.σ : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) →
          (c₁₂ : ComplexShape I₁₂) →
            [inst : TotalComplexShape c₁ c₂ c₁₂] →
              [inst_1 : TotalComplexShape c₂ c₁ c₁₂] → [TotalComplexShapeSymmetry c₁ c₂ c₁₂] → I₁ → I₂ → ℤˣ
-- Mathlib.Algebra.Free
FreeMagma.recOnMul.eq_1 : ∀ {α : Type u} {C : FreeMagma α → Sort l} (x : FreeMagma α) (ih1 : (x : α) → C (FreeMagma.of x))
  (ih2 : (x y : FreeMagma α) → C x → C y → C (x * y)), x.recOnMul ih1 ih2 = FreeMagma.recOn x ih1 ih2
-- Mathlib.CategoryTheory.Sites.SheafCohomology.Basic
CategoryTheory.Sheaf.H.equiv₀.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_2 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (F : CategoryTheory.Sheaf J AddCommGrpCat)
  {T : C} (hT : CategoryTheory.Limits.IsTerminal T),
  CategoryTheory.Sheaf.H.equiv₀ F hT =
    CategoryTheory.Abelian.Ext.addEquiv₀.trans
      (((CategoryTheory.constantSheafAdj J AddCommGrpCat hT).homAddEquiv (AddCommGrpCat.of (ULift.{w, 0} ℤ)) F).trans
        (((CategoryTheory.sheafSections J AddCommGrpCat).obj (Opposite.op T)).obj F).uliftZMultiplesAddEquiv)
-- Mathlib.Algebra.BigOperators.Finprod
finsum_of_infinite_support : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M},
  (Function.support f).Infinite → ∑ᶠ (i : α), f i = 0
-- Mathlib.Order.Filter.AtTopBot.Finite
/-- If `u` is a sequence which is unbounded below,
then after any point, it reaches a value strictly smaller than all previous values.
 -/
Filter.low_scores : ∀ {β : Type u_4} [inst : LinearOrder β] [NoMinOrder β] {u : ℕ → β},
  Filter.Tendsto u Filter.atTop Filter.atBot → ∀ (N : ℕ), ∃ n ≥ N, ∀ k < n, u n < u k
-- Init.Data.Iterators.Combinators.Monadic.FilterMap
/-- If `it` is an iterator, then `it.filterM f` is another iterator that applies a monadic
predicate `f` to all values emitted by `it` and emits them only if they are accepted by `f`.

The base iterator `it` being monadic in `m`, `f` can return values in any monad `n` for which a
`MonadLiftT m n` instance is available.

If `f` is pure, then the simpler variant `it.filter` can be used instead.

**Marble diagram (without monadic effects):**

```text
it             ---a--b--c--d-e--⊥
it.filterM     ---a-----c-------⊥
```

(given that `f a = f c = pure true` and `f b = f d = d e = pure false`)

**Termination properties:**

* `Finite` instance: only if `it` is finite
* `Productive` instance: only if `it` is finite`

For certain mapping functions `f`, the resulting iterator will be finite (or productive) even though
no `Finite` (or `Productive`) instance is provided. For example, if `f` is an `ExceptT` monad and
will always fail, then `it.filterWithPostcondition` will be finite -- and productive -- even if `it`
isn't. In such cases, the termination proof needs to be done manually.

**Performance:**

For each value emitted by the base iterator `it`, this combinator calls `f`.
 -/
Std.IterM.filterM : {α β : Type w} →
  {m : Type w → Type w'} →
    {n : Type w → Type w''} →
      [Std.Iterator α m β] →
        [inst : Monad n] →
          [inst_1 : MonadAttach n] →
            [inst_2 : MonadLiftT m n] → (f : β → n (ULift.{w, 0} Bool)) → Std.IterM m β → Std.IterM n β
-- Init.Data.String.Slice
_private.Init.Data.String.Slice.0.String.Slice.SplitIterator.instIteratorIdSubslice.match_5.splitter : {ρ : Type} →
  {σ : String.Slice → Type} →
    {pat : ρ} →
      [inst : String.Slice.Pattern.ToForwardSearcher pat σ] →
        {s : String.Slice} →
          (motive : Std.IterM Id s.Subslice → Sort u_1) →
            (x : Std.IterM Id s.Subslice) →
              ((currPos : s.Pos) →
                  (searcher : Std.Iter (String.Slice.Pattern.SearchStep s)) →
                    motive { internalState := String.Slice.SplitIterator.operating currPos searcher }) →
                (Unit → motive { internalState := String.Slice.SplitIterator.atEnd }) → motive x
-- Mathlib.Algebra.Group.Opposite
AddOpposite.addSemiconjBy_op : ∀ {α : Type u_1} [inst : Add α] {a x y : α},
  AddSemiconjBy (AddOpposite.op a) (AddOpposite.op y) (AddOpposite.op x) ↔ AddSemiconjBy a x y
-- Lean.Elab.Do.Control
/-- Plan for embedding a non-tail-resumptive body inside `origCont` via a monad-transformer stack.  -/
Lean.Elab.Do.EffectForwarder : Type
-- Std.Sync.Channel
Std.CloseableChannel.Error.noConfusionType : Sort v✝ → Std.CloseableChannel.Error → Std.CloseableChannel.Error → Sort v✝
-- Aesop.Frontend.Tactic
Aesop.Frontend.elabOptions : Lean.Syntax → Lean.Elab.TermElabM Aesop.Options
-- Mathlib.Topology.UniformSpace.Equicontinuity
equicontinuousAt_restrict_iff : ∀ {ι : Type u_1} {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] (F : ι → X → α)
  {S : Set X} (x₀ : ↑S), EquicontinuousAt (S.domRestrict ∘ F) x₀ ↔ EquicontinuousWithinAt F S ↑x₀
-- Mathlib.Tactic.FunProp.Decl
/-- Basic information about function property

To use `funProp` to prove a function property `P : (α→β)→Prop` one has to provide `FunPropDecl`.
 -/
Mathlib.Meta.FunProp.FunPropDecl : Type
-- Init.Data.List.ToArray
Array.getLast?_toList : ∀ {α : Type u_1} (xs : Array α), xs.toList.getLast? = xs.back?
-- Init.Data.Nat.Basic
Nat.sub_le_add_right_sub : ∀ (a i j : ℕ), a - i ≤ a + j - i
-- Mathlib.RingTheory.Valuation.ValuationRing
/-- The valuation ring `A` is isomorphic to the ring of integers of its associated valuation.  -/
ValuationRing.equivInteger : (A : Type u) →
  [inst : CommRing A] →
    (K : Type v) →
      [inst_1 : Field K] →
        [inst_2 : Algebra A K] →
          [inst_3 : IsDomain A] →
            [inst_4 : ValuationRing A] → [inst_5 : IsFractionRing A K] → A ≃+* ↥(ValuationRing.valuation A K).integer
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- The Gromov-Hausdorff distance between two nonempty compact metric spaces, equal by definition to
the distance of the equivalence classes of these spaces in the Gromov-Hausdorff space.  -/
GromovHausdorff.ghDist : (X : Type u) →
  (Y : Type v) →
    [inst : MetricSpace X] →
      [Nonempty X] → [CompactSpace X] → [inst : MetricSpace Y] → [Nonempty Y] → [CompactSpace Y] → ℝ
-- Mathlib.Analysis.InnerProductSpace.Laplacian
/-- The Laplacian commutes with left composition by continuous linear equivalences.  -/
InnerProductSpace.laplacian_CLE_comp_left : ∀ {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ 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] {f : E → F} {l : F ≃L[ℝ] G},
  Laplacian.laplacian (⇑l ∘ f) = ⇑l ∘ Laplacian.laplacian f
-- Mathlib.Algebra.Exact.Basic
LinearEquiv.conj_symm_exact_iff_exact : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {N' : Type u_5} {P : Type u_6} [inst : Semiring R]
  [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid N'] [inst_4 : AddCommMonoid P]
  [inst_5 : Module R M] [inst_6 : Module R N] [inst_7 : Module R N'] [inst_8 : Module R P] (f : M →ₗ[R] N)
  (g : N →ₗ[R] P) (e : N' ≃ₗ[R] N), Function.Exact ⇑(↑e.symm ∘ₗ f) ⇑(g ∘ₗ ↑e) ↔ Function.Exact ⇑f ⇑g
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.desc.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  (α : CochainComplex.HomComplex.Cochain K M 0) (β : CochainComplex.HomComplex.Cocycle L M 1)
  (hαβ :
    CochainComplex.HomComplex.δ 0 1 α +
        (CochainComplex.HomComplex.Cochain.ofHom φ).comp (↑β) CochainComplex.mappingCocone.desc._proof_2 =
      0),
  CochainComplex.mappingCocone.desc φ α β hαβ =
    (CochainComplex.mappingCocone.descCocycle φ α β CochainComplex.mappingCocone.desc._proof_2 ⋯).homOf
-- Lean.Language.Basic
/-- Lifts a typed snapshot inside a task to a `SnapshotTree` task via `ToSnapshotTree`.  -/
Lean.Language.SnapshotTask.transform : {α : Type} →
  [Lean.Language.ToSnapshotTree α] →
    Lean.Language.SnapshotTask α → Lean.Language.ToSnapshotTreeM (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)
-- Mathlib.NumberTheory.Modular
/-- The points on the bottom "arc" of the fundamental domain are in the closure
of the open fundamental domain.  -/
_private.Mathlib.NumberTheory.Modular.0.ModularGroup.mem_closure_of_arc : ∀ {x : UpperHalfPlane}, ‖↑x‖ = 1 → |x.re| ≤ 1 / 2 → x ∈ closure ModularGroup.fdo
-- Mathlib.Algebra.Ring.Commute
Commute.sub_right : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {a b c : R}, Commute a b → Commute a c → Commute a (b - c)
-- Mathlib.Topology.Algebra.SeparationQuotient.Section
SeparationQuotient.postcomp_mkCLM_surjective : ∀ {K : Type u_1} (E : Type u_2) [inst : DivisionRing K] [inst_1 : AddCommGroup E] [inst_2 : Module K E]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalAddGroup E] [inst_5 : ContinuousConstSMul K E] {L : Type u_3}
  [inst_6 : Semiring L] (σ : L →+* K) (F : Type u_4) [inst_7 : AddCommMonoid F] [inst_8 : Module L F]
  [inst_9 : TopologicalSpace F], Function.Surjective (SeparationQuotient.mkCLM K E).comp
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.empty_isBasis_iff : ∀ {α : Type u_2} {M : Matroid α} {X : Set α}, M.IsBasis ∅ X ↔ X ⊆ M.closure ∅
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.inv_eq_symplectic_inv : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R],
  ∀ A ∈ Matrix.symplecticGroup l R, A⁻¹ = -Matrix.J l R * A.transpose * Matrix.J l R
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.mem_sInf : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  (T : Set (CategoryTheory.Pretopology C)) {X : C} (S : CategoryTheory.Presieve X),
  S ∈ (sInf T).coverings X ↔ ∀ t ∈ T, S ∈ t.coverings X
-- Batteries.Data.List.Lemmas
/-- **Alias** of `List.modify_eq_set_getElem?`. -/
List.modify_eq_set_get? : ∀ {α : Type u_1} (f : α → α) (n : ℕ) (l : List α), l.modify n f = ((fun a => l.set n (f a)) <$> l[n]?).getD l
-- Mathlib.Algebra.Order.GroupWithZero.Defs
mulPosMono_iff_mulPosReflectLT : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : Zero α] [inst_2 : LinearOrder α], MulPosMono α ↔ MulPosReflectLT α
-- Mathlib.CategoryTheory.Iso
CategoryTheory.asIso'_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (f : Y ⟶ X) [inst_1 : CategoryTheory.IsIso f],
  (CategoryTheory.asIso' f).hom = CategoryTheory.inv f
-- Mathlib.Tactic.Ring.Common
Mathlib.Tactic.Ring.Common.coeff_mul : ∀ {a₃ c₂ k : ℕ} (a₁ a₂ : ℕ), a₃ = c₂ * k → a₁ ^ a₂ * a₃ = a₁ ^ a₂ * c₂ * k
-- Mathlib.Data.Set.Lattice
Set.iInter_congr_Prop : ∀ {α : Type u_1} {p q : Prop} {f₁ : p → Set α} {f₂ : q → Set α} (pq : p ↔ q),
  (∀ (x : q), f₁ ⋯ = f₂ x) → Set.iInter f₁ = Set.iInter f₂
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.addContent_biUnion : ∀ {α : Type u_1} {C : Set (Set α)} {G : Type u_2} [inst : AddCommMonoid G] {m : MeasureTheory.AddContent G C}
  {ι : Type u_3} {a : Finset ι} {f : ι → Set α},
  (∀ i ∈ a, f i ∈ C) → (↑a).PairwiseDisjoint f → ⋃ i ∈ a, f i ∈ C → m (⋃ i ∈ a, f i) = ∑ i ∈ a, m (f i)
-- Mathlib.Analysis.Asymptotics.ExpGrowth
ExpGrowth.expGrowthSup_const : ∀ {b : ENNReal}, b ≠ 0 → b ≠ ⊤ → (ExpGrowth.expGrowthSup fun x => b) = 0
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.instZeroHom : (X Y : SemiNormedGrp₁) → Zero (X ⟶ Y)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.Opens.topIso.eq_1 : ∀ {X : AlgebraicGeometry.Scheme} (U : X.Opens),
  U.topIso = CategoryTheory.Functor.mapIso X.presheaf (CategoryTheory.eqToIso ⋯).op
-- Mathlib.Logic.Equiv.Defs
/-- `Perm α` is the type of bijections from `α` to itself.  -/
Equiv.Perm : Sort u_1 → Sort (max 1 u_1)
-- Mathlib.Algebra.DirectSum.Module
DirectSum.component_comp_lof : ∀ (R : Type u) [inst : Semiring R] {ι : Type v} {M : ι → Type w} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] [inst_3 : DecidableEq ι] (i j : ι),
  DirectSum.component R ι M i ∘ₗ DirectSum.lof R ι M j = if h : j = i then h ▸ LinearMap.id else 0
-- Mathlib.Combinatorics.SimpleGraph.Bipartite
/-- `G` is bipartite in sets `s` and `t` iff `s` and `t` are disjoint and if vertices `v` and `w`
are adjacent in `G` then `v ∈ s` and `w ∈ t`, or `v ∈ t` and `w ∈ s`.  -/
SimpleGraph.IsBipartiteWith : {V : Type u_1} → SimpleGraph V → Set V → Set V → Prop
-- Mathlib.Data.Set.Piecewise
Set.piecewise_eqOn_compl : ∀ {α : Type u_1} {β : Type u_2} (s : Set α) [inst : (j : α) → Decidable (j ∈ s)] (f g : α → β),
  Set.EqOn (s.piecewise f g) g sᶜ
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.orthogonalProjectionOnto_apply_eq_sum : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {U : Submodule 𝕜 E} [inst_4 : U.HasOrthogonalProjection]
  (b : OrthonormalBasis ι 𝕜 ↥U) (x : E), U.orthogonalProjectionOnto x = ∑ i, inner 𝕜 (↑(b i)) x • b i
-- Mathlib.Algebra.CubicDiscriminant
Cubic.splits_iff_card_roots : ∀ {F : Type u_3} {K : Type u_4} {P : Cubic F} [inst : Field F] [inst_1 : Field K] {φ : F →+* K},
  P.a ≠ 0 → ((Polynomial.map φ P.toPoly).Splits ↔ (Cubic.map φ P).roots.card = 3)
-- Mathlib.RingTheory.MatrixAlgebra
/-- (Implementation detail)

The equivalence, ignoring the algebra structure, `(A ⊗[R] Matrix n n R) ≃ Matrix n n A`.
 -/
MatrixEquivTensor.equiv : (n : Type u_3) →
  (R : Type u_5) →
    (A : Type u_7) →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] → [DecidableEq n] → [Fintype n] → TensorProduct R A (Matrix n n R) ≃ Matrix n n A
-- Init.Data.List.Sublist
List.prefix_iff_exists_append_eq : ∀ {α : Type u_1} {l₁ l₂ : List α}, l₁ <+: l₂ ↔ ∃ l₃, l₁ ++ l₃ = l₂
-- Init.Internal.Order.Basic
Lean.Order.PProd.monotone_snd : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} [inst : Lean.Order.PartialOrder α] [inst_1 : Lean.Order.PartialOrder β]
  [inst_2 : Lean.Order.PartialOrder γ] {f : γ → α ×' β}, Lean.Order.monotone f → Lean.Order.monotone fun x => (f x).snd
-- Mathlib.LinearAlgebra.Matrix.BilinearForm
LinearMap.BilinForm.separatingLeft_toMatrix'_iff : ∀ {R₂ : Type u_3} [inst : CommRing R₂] {ι : Type u_6} [inst_1 : DecidableEq ι] [inst_2 : Fintype ι]
  {B : LinearMap.BilinForm R₂ (ι → R₂)}, (LinearMap.BilinForm.toMatrix' B).SeparatingLeft ↔ LinearMap.SeparatingLeft B
-- Mathlib.NumberTheory.ArithmeticFunction.Misc
ArithmeticFunction.cardDistinctFactors_zero : ArithmeticFunction.cardDistinctFactors 0 = 0
-- Mathlib.Algebra.Group.Hom.Defs
instCoeTCMonoidHomOfMonoidHomClass.eq_1 : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : MulOne M] [inst_1 : MulOne N] [inst_2 : FunLike F M N]
  [inst_3 : MonoidHomClass F M N], instCoeTCMonoidHomOfMonoidHomClass = { coe := MonoidHomClass.toMonoidHom }
-- Mathlib.NumberTheory.SelbergSieve
/-- We consider a special class of upper bound sieves called the Λ² sieve. This class is
parameterised by a sequence of real numbers. We will later choose a set of weights that minimises
the main term, under a constraint that lets us control the error term.  -/
BoundingSieve.lambdaSquared : (ℕ → ℝ) → ℕ → ℝ
-- Mathlib.Analysis.CStarAlgebra.Unitary.Connected
/-- Any ball of radius `δ < 2` in the unitary group of a unital C⋆-algebra is path connected.  -/
Unitary.isPathConnected_ball : ∀ {A : Type u_1} [inst : CStarAlgebra A] (u : ↥(unitary A)) (δ : ℝ), 0 < δ → δ < 2 → IsPathConnected (Metric.ball u δ)
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.stmts₁.eq_3 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (a : Γ → σ → σ) (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.stmts₁ (Turing.TM1.Stmt.load a q) = insert (Turing.TM1.Stmt.load a q) (Turing.TM1.stmts₁ q)
-- Mathlib.Data.Nat.Cast.Order.Field
/-- Natural division is always less than division in the field.  -/
Nat.cast_div_le : ∀ {α : Type u_1} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] {m n : ℕ}, ↑(m / n) ≤ ↑m / ↑n
-- Mathlib.Tactic.Ring.RingNF
Mathlib.Tactic.RingNF.mul_assoc_rev : ∀ {R : Type u_1} [inst : CommSemiring R] (a b c : R), a * (b * c) = a * b * c
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get?_union : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] (h₁ : m₁.WF) (h₂ : m₂.WF) {k : α}, (m₁.union m₂ ⋯ ⋯).get? k = (m₂.get? k).or (m₁.get? k)
-- Init.Data.Option.Attach
Option.toArray_unattach : ∀ {α : Type u_1} {p : α → Prop} {o : Option { x // p x }}, o.unattach.toArray = o.toArray.unattach
-- Mathlib.Data.List.Map2
List.map₂Right'_nil_left : ∀ {α : Type u} {β : Type v} {γ : Type w} (f : Option α → β → γ) (bs : List β),
  List.map₂Right' f [] bs = (List.map (f none) bs, [])
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub_eq_empty : ∀ {α : Type u_2} [inst : Sub α] {s t : Set α}, s - t = ∅ ↔ s = ∅ ∨ t = ∅
-- Init.Data.String.Defs
_private.Init.Data.String.Defs.0.String.Pos.Raw.IsValid.mk : ∀ {s : String} {off : String.Pos.Raw},
  off ≤ s.rawEndPos → (s.toByteArray.extract 0 off.byteIdx).IsValidUTF8 → String.Pos.Raw.IsValid s off
-- Mathlib.Topology.Order.Basic
/-- For a function taking values in a second countable space, the set of points `x` for
which the image under `f` of `(x, ∞)` is separated below from `f x` is countable. We give
here a version relative to a set `t`.  -/
countable_image_gt_image_Ioi_within : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α]
  [inst_3 : LinearOrder β] [SecondCountableTopology α] (t : Set β) (f : β → α),
  {x | x ∈ t ∧ ∃ z < f x, ∀ y ∈ t, x < y → f y ≤ z}.Countable
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.mono_left : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x y : Filter α} {z : Filter β},
  Filter.Tendsto f x z → y ≤ x → Filter.Tendsto f y z
-- Mathlib.NumberTheory.Divisors
Int.divisorsAntidiag_neg : ∀ {z : ℤ},
  (-z).divisorsAntidiag =
    Finset.map ((Function.Embedding.refl ℤ).prodMap (Equiv.toEmbedding (Equiv.neg ℤ))) z.divisorsAntidiag
-- Mathlib.Tactic.Explode.Datatypes
/-- What `Status` this entry has - this only affects how `│`s are displayed.  -/
Mathlib.Explode.Entry.status : Mathlib.Explode.Entry → Mathlib.Explode.Status
-- Mathlib.NumberTheory.Divisors
Int.one_mem_divisors : ∀ {z : ℤ}, 1 ∈ z.divisors ↔ z ≠ 0
-- Mathlib.Algebra.MonoidAlgebra.Module
MonoidAlgebra.supportedEquivFinsupp_apply_apply : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Module R S]
  (s : Set M) (x : ↥(MonoidAlgebra.supported R S s)) (a : { x // x ∈ s }),
  ((MonoidAlgebra.supportedEquivFinsupp s) x) a = (↑x).coeff ↑a
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.coe_mk' : ∀ {R : Type u} [inst : NonAssocRing R] (s : Set R) (sm : Submonoid R) (sa : AddSubgroup R) (hm : ↑sm = s)
  (ha : ↑sa = s), ↑(Subring.mk' s sm sa hm ha) = s
-- Mathlib.Tactic.PNatToNat
/-- `pnat_to_nat` shifts all `PNat`s in the context to `Nat`, rewriting propositions about them.
A typical use case is `pnat_to_nat; lia`.  -/
Mathlib.Tactic.PNatToNat.tacticPnat_to_nat : Lean.ParserDescr
-- Mathlib.Tactic.GRewrite.Core
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.Progress.matchedOutOfScope.inj : ∀ {lctx lctx_1 : Lean.LocalContext},
  Mathlib.Tactic.GRewrite.Progress.matchedOutOfScope✝ lctx =
      Mathlib.Tactic.GRewrite.Progress.matchedOutOfScope✝ lctx_1 →
    lctx = lctx_1
-- Mathlib.Tactic.Translate.Reorder
Mathlib.Tactic.Translate.translateReorder.quot : Lean.ParserDescr