mathlib-initiative/mathlib-types huggingface dataset:
-- Aesop.Forward.SlotIndex
Aesop.instOrdSlotIndex : Ord Aesop.SlotIndex
-- Mathlib.Computability.Primrec.Basic
Primrec.option_some : ∀ {α : Type u_1} [inst : Primcodable α], Primrec some
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.equiv_rootD : ∀ {self : Batteries.UnionFind} {a : ℕ}, self.Equiv (self.rootD a) a
-- Mathlib.Topology.Sets.Opens
/-- The Galois coinsertion between sets and opens.  -/
TopologicalSpace.Opens.gi : {α : Type u_2} → [inst : TopologicalSpace α] → GaloisCoinsertion SetLike.coe TopologicalSpace.Opens.interior
-- Mathlib.GroupTheory.Coxeter.Basic
CoxeterSystem.lift_apply_simple : ∀ {B : Type u_1} {W : Type u_3} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W) {G : Type u_5}
  [inst_1 : Monoid G] {f : B → G} (hf : M.IsLiftable f) (i : B), (cs.lift ⟨f, hf⟩) (cs.simple i) = f i
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Pseudo
CategoryTheory.Pseudofunctor.StrongTrans.naturality_naturality_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] {F G : CategoryTheory.Pseudofunctor B CategoryTheory.Cat}
  (α : F ⟶ G) {a b : B} {f g : a ⟶ b} (η : f ≅ g) (X : ↑(F.obj a)),
  (α.naturality g).hom.toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((α.app b).toFunctor.map ((F.map₂ η.inv).toNatTrans.app X))
      (CategoryTheory.CategoryStruct.comp ((α.naturality f).hom.toNatTrans.app X)
        ((G.map₂ η.hom).toNatTrans.app ((α.app a).toFunctor.obj X)))
-- Mathlib.Algebra.Group.AddChar
AddChar.coe_toAddMonoidHom : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (ψ : AddChar A M),
  ⇑ψ.toAddMonoidHom = ⇑Additive.ofMul ∘ ⇑ψ
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.mk'_d_1_0 : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] (X₀ X₁ : V)
  (d₀ : X₀ ⟶ X₁)
  (succ' : {X₀ X₁ : V} → (f : X₀ ⟶ X₁) → (X₂ : V) ×' (d : X₁ ⟶ X₂) ×' CategoryTheory.CategoryStruct.comp f d = 0),
  (CochainComplex.mk' X₀ X₁ d₀ fun {X₀ X₁} => succ').d 0 1 = d₀
-- Mathlib.Tactic.ByContra
/-- If the target of the main goal is a proposition `p`,
`by_contra!` reduces the goal to proving `False` using the additional hypothesis `this : ¬ p`.
`by_contra! h` can be used to name the hypothesis `h : ¬ p`.
The hypothesis `¬ p` will be normalized using `push Not`.
For instance, `¬ a < b` will be changed to `b ≤ a`.
`by_contra!` can be used with `rcases` patterns.
For instance, `by_contra! rfl` on `⊢ s.Nonempty` will substitute the equality `s = ∅`,
and `by_contra! ⟨hp, hq⟩` on `⊢ ¬ p ∨ ¬ q` will introduce `hp : p` and `hq : q`.
`by_contra! h : q` will normalize negations in `¬ p`, normalize negations in `q`,
and then check that the two normalized forms are equal.
The resulting hypothesis is the pre-normalized form, `q`.
If the name `h` is not explicitly provided, then `this` will be used as name.
This tactic uses classical reasoning.
It is a variant on the tactic `by_contra`.
Examples:
```lean
example : 1 < 2 := by
  by_contra! h
  -- h : 2 ≤ 1 ⊢ False

example : 1 < 2 := by
  by_contra! h : ¬ 1 < 2
  -- h : ¬ 1 < 2 ⊢ False
```
 -/
Mathlib.Tactic.ByContra.byContra! : Lean.ParserDescr
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.CechNerveTerminalFrom.uniqueToWideCospanNone : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasTerminal C] →
      (ι : Type w) → (X Y : C) → Unique (Y ⟶ (CategoryTheory.CechNerveTerminalFrom.wideCospan ι X).obj none)
-- Init.Data.String.Basic
_private.Init.Data.String.Basic.0.ByteArray.utf8Decode?.go.match_1.eq_2 : ∀ (motive : Option Char → Sort u_1) (c : Char) (h_1 : some c = none → motive none)
  (h_2 : (c_1 : Char) → some c = some c_1 → motive (some c_1)),
  (match h : some c with
    | none => h_1 h
    | some c_1 => h_2 c_1 h) =
    h_2 c ⋯
-- Mathlib.Algebra.Category.Ring.Basic
_private.Mathlib.Algebra.Category.Ring.Basic.0.SemiRingCat.Hom.mk.injEq : ∀ {R S : SemiRingCat} (hom' hom'_1 : ↑R →+* ↑S), ({ hom' := hom' } = { hom' := hom'_1 }) = (hom' = hom'_1)
-- Mathlib.CategoryTheory.Limits.Fubini
CategoryTheory.Limits.coconeOfCoconeCurry_ι_app : ∀ {J : Type u_1} {K : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} K] {C : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  (G : CategoryTheory.Functor (J × K) C)
  {D : CategoryTheory.Limits.DiagramOfCocones (CategoryTheory.Functor.curry.obj G)}
  (Q : (j : J) → CategoryTheory.Limits.IsColimit (D.obj j)) (c : CategoryTheory.Limits.Cocone G) (j : J),
  (CategoryTheory.Limits.coconeOfCoconeCurry G Q c).ι.app j =
    (Q j).desc { pt := c.pt, ι := { app := fun k => c.ι.app (j, k), naturality := ⋯ } }
-- Mathlib.RingTheory.FinitePresentation
/-- Induction principle for finitely presented ring homomorphisms.

For a property to hold for all finitely presented ring homs, it suffices for it to hold for
`Polynomial.C : R → R[X]`, surjective ring homs with finitely generated kernels, and to be closed
under composition.

Note that to state this conveniently for ring homs between rings of different universes, we carry
around two predicates `P` and `Q`, which should be "the same" apart from universes:
* `P`, for ring homs `(R : Type u) → (S : Type u)`.
* `Q`, for ring homs `(R : Type u) → (S : Type v)`.
 -/
RingHom.FinitePresentation.polynomial_induction : ∀ (P : (R : Type u) → [inst : CommRing R] → (S : Type u) → [inst_1 : CommRing S] → (R →+* S) → Prop)
  (Q : (R : Type u) → [inst : CommRing R] → (S : Type v) → [inst_1 : CommRing S] → (R →+* S) → Prop),
  (∀ (R : Type u) [inst : CommRing R], P R (Polynomial R) Polynomial.C) →
    (∀ (R : Type u) [inst : CommRing R] (S : Type v) [inst_1 : CommRing S] (f : R →+* S),
        Function.Surjective ⇑f → (RingHom.ker f).FG → Q R S f) →
      (∀ (R : Type u) [inst : CommRing R] (S : Type u) [inst_1 : CommRing S] (T : Type v) [inst_2 : CommRing T]
          (f : R →+* S) (g : S →+* T), P R S f → Q S T g → Q R T (g.comp f)) →
        ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] (f : R →+* S),
          f.FinitePresentation → Q R S f
-- Mathlib.Topology.DiscreteQuotient
LocallyConstant.lift_comp_proj : ∀ {α : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] (f : LocallyConstant X α),
  ⇑f.lift ∘ f.discreteQuotient.proj = ⇑f
-- Lean.DocString.Parser
/-- Parenthesizer for `ifVerso`—parenthesizes according to the underlying parenthesizers.
 -/
Lean.Doc.Parser.ifVerso.parenthesizer : Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer → Lean.PrettyPrinter.Parenthesizer
-- Mathlib.AlgebraicGeometry.Modules.Sheaf
AlgebraicGeometry.Scheme.Modules.instIsLeftAdjointRestrictFunctor : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [inst : AlgebraicGeometry.IsOpenImmersion f],
  (AlgebraicGeometry.Scheme.Modules.restrictFunctor f).IsLeftAdjoint
-- Mathlib.RingTheory.Finiteness.Basic
/-- **Alias** of `Module.Finite.shrink`. -/
Module.Finite.Module.finite_shrink : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Finite R M]
  [inst_4 : Small.{u, u_4} M], Module.Finite R (Shrink.{u, u_4} M)
-- Mathlib.RingTheory.WittVector.Defs
/-- `x.coeff n` is the `n`th coefficient of the Witt vector `x`.

This concept does not have a standard name in the literature.
 -/
WittVector.coeff : {p : ℕ} → {R : Type u_1} → WittVector p R → ℕ → R
-- Mathlib.Topology.Algebra.InfiniteSum.UniformOn
SummableUniformly.exists : ∀ {α : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : AddCommMonoid α] {f : ι → β → α} [inst_1 : UniformSpace α],
  SummableUniformly f → ∃ g, HasSumUniformly f g
-- Mathlib.Topology.MetricSpace.IsometricSMul
IsometryEquiv.mulRight_symm : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [inst_2 : IsIsometricSMul Gᵐᵒᵖ G] (x : G),
  (IsometryEquiv.mulRight x).symm = IsometryEquiv.mulRight x⁻¹
-- Mathlib.Order.Interval.Set.Pi
Set.image_mulSingle_Ico : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)]
  [inst_2 : (i : ι) → One (α i)] (i : ι) (a b : α i),
  Pi.mulSingle i '' Set.Ico a b = Set.Ico (Pi.mulSingle i a) (Pi.mulSingle i b)
-- Batteries.Data.List.Perm
_private.Batteries.Data.List.Perm.0.cond.match_1.splitter : (motive : Bool → Sort u_1) → (c : Bool) → (Unit → motive true) → (Unit → motive false) → motive c
-- Mathlib.Analysis.Convex.Segment
segment_same : ∀ (𝕜 : Type u_1) {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [ZeroLEOneClass 𝕜] [inst_4 : Module 𝕜 E] (x : E), segment 𝕜 x x = {x}
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasurableEmbedding.integrableAtFilter_map_iff : ∀ {α : Type u_1} {β : Type u_2} {ε : Type u_3} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {l : Filter α} [inst_2 : MeasurableSpace β] {e : α → β},
  MeasurableEmbedding e →
    ∀ {f : β → ε},
      MeasureTheory.IntegrableAtFilter f (Filter.map e l) (MeasureTheory.Measure.map e μ) ↔
        MeasureTheory.IntegrableAtFilter (f ∘ e) l μ
-- Mathlib.Topology.AlexandrovDiscrete
AlexandrovDiscrete.sup : ∀ {α : Type u_3} {t₁ t₂ : TopologicalSpace α}, AlexandrovDiscrete α → AlexandrovDiscrete α → AlexandrovDiscrete α
-- Mathlib.CategoryTheory.Subobject.Lattice
/-- The "wide cospan" diagram, with a small indexing type, constructed from a set of subobjects.
(This is just the diagram of all the subobjects pasted together, but using `WellPowered C`
to make the diagram small.)
 -/
CategoryTheory.Subobject.wideCospan : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.LocallySmall.{w, v₁, u₁} C] →
      [inst_2 : CategoryTheory.WellPowered.{w, v₁, u₁} C] →
        {A : C} →
          (s : Set (CategoryTheory.Subobject A)) →
            CategoryTheory.Functor
              (CategoryTheory.Limits.WidePullbackShape ↑(⇑(equivShrink (CategoryTheory.Subobject A)) '' s)) C
-- Mathlib.Algebra.Group.Basic
zero_sub_zero_sub : ∀ {α : Type u_1} [inst : SubtractionMonoid α] (a : α), 0 - (0 - a) = a
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.toNonUnitalRingHom_eq_coe : ∀ {R : Type u_4} {S : Type u_5} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R ≃+* S), f.toNonUnitalRingHom = ↑f
-- Mathlib.Topology.Order.Category.FrameAdjunction
/-- The frame homomorphism from a complete lattice `L` to the complete lattice of sets of
points of `L`.  -/
Locale.openOfElementHom : (L : Type u_1) → [inst : CompleteLattice L] → FrameHom L (Set (Locale.PT L))
-- Mathlib.Algebra.Category.Ring.Adjunctions
/-- The free functor `Type u ⥤ CommRingCat` sending a type `X` to the multivariable (commutative)
polynomials with variables `x : X`.
 -/
CommRingCat.free : CategoryTheory.Functor (Type u) CommRingCat
-- Std.Tactic.BVDecide.LRAT.Internal.LRATCheckerSound
Std.Tactic.BVDecide.LRAT.Internal.delCaseSound : ∀ {α : Type u_1} {β : Type u_2} {σ : Type u_3} [inst : DecidableEq α]
  [inst_1 : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] [inst_2 : Std.Tactic.BVDecide.LRAT.Internal.Entails α σ]
  [inst_3 : Std.Tactic.BVDecide.LRAT.Internal.Formula α β σ] (f : σ),
  Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd f →
    Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd f →
      ∀ (ids : Array ℕ) (restPrf : List (Std.Tactic.BVDecide.LRAT.Action β α)),
        (∀ a ∈ restPrf, Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction a) →
          (Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRupAdd
                (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f ids) →
              Std.Tactic.BVDecide.LRAT.Internal.Formula.ReadyForRatAdd
                  (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f ids) →
                (∀ a ∈ restPrf, Std.Tactic.BVDecide.LRAT.Internal.WellFormedAction a) →
                  Std.Tactic.BVDecide.LRAT.Internal.lratChecker (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f ids)
                        restPrf =
                      Std.Tactic.BVDecide.LRAT.Internal.Result.success →
                    Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α
                      (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f ids)) →
            Std.Tactic.BVDecide.LRAT.Internal.lratChecker (Std.Tactic.BVDecide.LRAT.Internal.Formula.delete f ids)
                  restPrf =
                Std.Tactic.BVDecide.LRAT.Internal.Result.success →
              Std.Tactic.BVDecide.LRAT.Internal.Unsatisfiable α f
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.logEmbeddingEquiv_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (x : (NumberField.RingOfIntegers K)ˣ),
  ↑((NumberField.Units.logEmbeddingEquiv K) (Additive.ofMul ↑x)) = (NumberField.Units.logEmbedding K) (Additive.ofMul x)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.Iso.prod_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {P Q : C} {S T : D} (f : P ≅ Q) (g : S ≅ T), (f.prod g).inv = CategoryTheory.Prod.mkHom f.inv g.inv
-- Batteries.Data.RunningStats
/-- Sample standard deviation of running data stream (square root of sample variance).  -/
Batteries.RunningStats.sampleStandardDeviation : Batteries.RunningStats → Float
-- Lean.Elab.Tactic.Basic
Lean.Elab.Tactic.EvalTacticFailure.state : Lean.Elab.Tactic.EvalTacticFailure → Lean.Elab.Tactic.SavedState
-- Mathlib.Algebra.Order.Monoid.Prod
Prod.Lex.isOrderedCancelMonoid : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : PartialOrder α] [IsOrderedCancelMonoid α]
  [inst_3 : CommMonoid β] [inst_4 : PartialOrder β] [IsOrderedCancelMonoid β], IsOrderedCancelMonoid (Lex (α × β))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.maxKeyD_eq_fallback : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {fallback : α}, t.isEmpty = true → t.maxKeyD fallback = fallback
-- Lean.Meta.Tactic.Grind.Types
/-- Marks `e` as a case-split that does not need to be performed anymore.
Remark: we currently use this feature to disable `match`-case-splits.
Remark: we also use this feature to record the case-splits that have already been performed.
 -/
Lean.Meta.Grind.markCaseSplitAsResolved : Lean.Expr → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Order.Category.HeytAlg
HeytAlg.Hom.ext : ∀ {X Y : HeytAlg} {x y : X.Hom Y}, x.hom' = y.hom' → x = y
-- Mathlib.Tactic.Linarith.Preprocessing
/-- `findSquares s e` collects all terms of the form `a ^ 2` and `a * a` that appear in `e`
and adds them to the set `s`.
A pair `(i, true)` is added to `s` when `atoms[i]^2` appears in `e`,
and `(i, false)` is added to `s` when `atoms[i]*atoms[i]` appears in `e`.  -/
Mathlib.Tactic.Linarith.findSquares : Std.TreeSet (ℕ × Bool) compare → Lean.Expr → Mathlib.Tactic.AtomM (Std.TreeSet (ℕ × Bool) compare)
-- Init.Data.Array.MapIdx
Array.mapIdx_eq_push_iff : ∀ {α : Type u_1} {β : Type u_2} {f : ℕ → α → β} {ys : Array β} {xs : Array α} {b : β},
  Array.mapIdx f xs = ys.push b ↔ ∃ a zs, xs = zs.push a ∧ Array.mapIdx f zs = ys ∧ f zs.size a = b
-- Mathlib.MeasureTheory.Measure.Decomposition.Exhaustion
/-- A measurable set such that `μ.restrict (μ.sigmaFiniteSetWRT' ν)` is sigma-finite and
`ν (μ.sigmaFiniteSetWRT' ν)` has maximal measure among such sets.  -/
MeasureTheory.Measure.sigmaFiniteSetWRT' : {α : Type u_1} →
  {mα : MeasurableSpace α} →
    MeasureTheory.Measure α → (ν : MeasureTheory.Measure α) → [MeasureTheory.IsFiniteMeasure ν] → Set α
-- Mathlib.CategoryTheory.Monoidal.Grp
/-- Constructor for morphisms in `AddGrp C`.  -/
CategoryTheory.AddGrp.homMk' : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] →
      {A B : CategoryTheory.AddGrp C} → (A.toAddMon ⟶ B.toAddMon) → (A ⟶ B)
-- Mathlib.CategoryTheory.LocallyCartesianClosed.Over
CategoryTheory.ChosenPullbacksAlong.Over.rightUnitor_inv_left_snd_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.ChosenPullbacks C] {X : C}
  (Y : CategoryTheory.Over X) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.rightUnitor Y).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.snd Y.hom (CategoryTheory.CategoryStruct.id X)) h) =
    CategoryTheory.CategoryStruct.comp Y.hom h
-- Mathlib.Algebra.Group.InjSurj
Function.Surjective.commGroup.eq_1 : ∀ {M₁ : Type u_1} {M₂ : Type u_2} [inst : Mul M₂] [inst_1 : One M₂] [inst_2 : Pow M₂ ℕ] [inst_3 : Inv M₂]
  [inst_4 : Div M₂] [inst_5 : Pow M₂ ℤ] [inst_6 : CommGroup M₁] (f : M₁ → M₂) (hf : Function.Surjective f)
  (one : f 1 = 1) (mul : ∀ (x y : M₁), f (x * y) = f x * f y) (inv : ∀ (x : M₁), f x⁻¹ = (f x)⁻¹)
  (div : ∀ (x y : M₁), f (x / y) = f x / f y) (npow : ∀ (x : M₁) (n : ℕ), f (x ^ n) = f x ^ n)
  (zpow : ∀ (x : M₁) (n : ℤ), f (x ^ n) = f x ^ n),
  Function.Surjective.commGroup f hf one mul inv div npow zpow =
    { toGroup := Function.Surjective.group f hf one mul inv div npow zpow, mul_comm := ⋯ }
-- Mathlib.Algebra.Algebra.Operations
Submodule.le_div_iff_mul_le : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : CommSemiring A] [inst_2 : Algebra R A]
  {I J K : Submodule R A}, I ≤ J / K ↔ I * K ≤ J
-- Lean.Expr
/-- Expression metavariable Id    -/
Lean.MVarId : Type
-- Mathlib.Algebra.Order.Ring.WithTop
WithTop.mul_left_strictMono : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] {a : WithTop α} [inst_2 : Preorder α]
  [MulPosStrictMono α], 0 < a → a ≠ ⊤ → StrictMono fun x => x * a
-- Mathlib.Combinatorics.Quiver.Symmetric
Quiver.Symmetrify.lift_spec : ∀ {V : Type u_2} [inst : Quiver V] {V' : Type u_4} [inst_1 : Quiver V'] [inst_2 : Quiver.HasReverse V'] (φ : V ⥤q V'),
  Quiver.Symmetrify.of ⋙q Quiver.Symmetrify.lift φ = φ
-- Mathlib.LinearAlgebra.Eigenspace.Matrix
Module.End.HasEigenvalue.nonempty : ∀ {R : Type u_1} {n : Type u_2} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing R] {A : Matrix n n R}
  {μ : R}, Module.End.HasEigenvalue (Matrix.toLin' A) μ → Nonempty n
-- Lean.Meta.SynthInstance
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessResult.mk.injEq : ∀ (type cacheKeyType : Lean.Expr) (kind : Lean.Meta.PreprocessKind✝) (type_1 cacheKeyType_1 : Lean.Expr)
  (kind_1 : Lean.Meta.PreprocessKind✝),
  ({ type := type, cacheKeyType := cacheKeyType, kind := kind } =
      { type := type_1, cacheKeyType := cacheKeyType_1, kind := kind_1 }) =
    (type = type_1 ∧ cacheKeyType = cacheKeyType_1 ∧ kind = kind_1)
-- Mathlib.Data.Nat.PrimeFin
Nat.Primes.countable : Countable Nat.Primes
-- Aesop.Forward.State
/-- Remove `hyp` from `slot` and all later slots. For each mapping
`s ↦ e ↦ (ms, hs)` in `imap`, if `s ≥ slot`, then `hyp` is removed from `hs` and
any matches containing `hyp` are removed from `ms`.  -/
Aesop.InstMap.eraseHyp : Aesop.InstMap → Lean.FVarId → Aesop.SlotIndex → Aesop.InstMap
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.uniformity_def : ∀ {α : Type u_1} [inst : UniformSpace α],
  uniformity (TopologicalSpace.Closeds α) =
    Filter.comap (Prod.map SetLike.coe SetLike.coe) ((uniformity α).lift' hausdorffEntourage)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Three
/-- If `λ` does not divide `x`, then `λ ^ 4` divides `x ^ 3 - 1` or `x ^ 3 + 1`.  -/
IsCyclotomicExtension.Rat.Three.lambda_pow_four_dvd_cube_sub_one_or_add_one_of_lambda_not_dvd : ∀ {K : Type u_1} [inst : Field K] {ζ : K} (hζ : IsPrimitiveRoot ζ 3) [inst_1 : NumberField K]
  [IsCyclotomicExtension {3} ℚ K] {x : NumberField.RingOfIntegers K},
  ¬hζ.toInteger - 1 ∣ x → (hζ.toInteger - 1) ^ 4 ∣ x ^ 3 - 1 ∨ (hζ.toInteger - 1) ^ 4 ∣ x ^ 3 + 1
-- Mathlib.Computability.TuringMachine.ToPartrec
Turing.PartrecToTM2.Cont'.brecOn.eq : ∀ {motive : Turing.PartrecToTM2.Cont' → Sort u} (t : Turing.PartrecToTM2.Cont')
  (F_1 : (t : Turing.PartrecToTM2.Cont') → Turing.PartrecToTM2.Cont'.below t → motive t),
  Turing.PartrecToTM2.Cont'.brecOn t F_1 = F_1 t (Turing.PartrecToTM2.Cont'.brecOn.go t F_1).2
-- Init.Data.List.Sort.Impl
/-- Auxiliary for `splitAtRev`: `splitAtRev.go xs n acc = ((take n xs).reverse ++ acc, drop n xs)`.  -/
_private.Init.Data.List.Sort.Impl.0.List.MergeSort.Internal.splitRevAt.go : {α : Type u_1} → List α → ℕ → List α → List α × List α
-- Mathlib.Order.Heyting.Boundary
Coheyting.boundary_hnot_hnot : ∀ {α : Type u_1} [inst : CoheytingAlgebra α] (a : α), Coheyting.boundary (￢￢a) = Coheyting.boundary (￢a)
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.OplaxTrans.homCategory_comp_as_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} {X Y Z : F ⟶ G} (Γ : CategoryTheory.Lax.OplaxTrans.Hom X Y)
  (Δ : CategoryTheory.Lax.OplaxTrans.Hom Y Z) (a : B),
  (CategoryTheory.CategoryStruct.comp Γ Δ).as.app a = CategoryTheory.CategoryStruct.comp (Γ.as.app a) (Δ.as.app a)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLEGT
/-- The isomorphism `t.truncGT a ≅ t.truncGE b` when `a + 1 = b`.  -/
CategoryTheory.Triangulated.TStructure.truncGTIsoTruncGE : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        [inst_3 : CategoryTheory.HasShift C ℤ] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [inst_5 : CategoryTheory.Pretriangulated C] →
              (t : CategoryTheory.Triangulated.TStructure C) → (a b : ℤ) → a + 1 = b → (t.truncGT a ≅ t.truncGE b)
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.ofTwoCocycle.mk.injEq : ∀ {R : Type u_5} {L : Type u_6} {M : Type u_7} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  {c : ↥(LieModule.Cohomology.twoCocycle R L M)} (carrier carrier_1 : L × M),
  ({ carrier := carrier } = { carrier := carrier_1 }) = (carrier = carrier_1)
-- Mathlib.Topology.SmallInductiveDimension
/-- **Alias** of `hasSmallInductiveDimensionLT_one_iff`. -/
HasSmallInductiveDimensionLT_one_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X],
  HasSmallInductiveDimensionLT X 1 ↔ TopologicalSpace.IsTopologicalBasis {s | IsClopen s}
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.diag2_smul_single_i₂ : ∀ {F : Type u_1} [inst : Field F] {a : F} (ha : a ≠ 0),
  Matrix.SpecialLinearGroup.diag2 a ha • Pi.single 1 1 = a⁻¹ • Pi.single 1 1
-- Mathlib.NumberTheory.NumberField.CMField
NumberField.IsCMField.equivInfinitePlace_symm_apply : ∀ (K : Type u_1) [inst : Field K] [inst_1 : CharZero K] [inst_2 : NumberField.IsCMField K] [inst_3 : NumberField K]
  (w : NumberField.InfinitePlace ↥(NumberField.maximalRealSubfield K)) (x : ↥(NumberField.maximalRealSubfield K)),
  ((NumberField.IsCMField.equivInfinitePlace K).symm w) ((algebraMap (↥(NumberField.maximalRealSubfield K)) K) x) = w x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.subset_mul_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : MulOneClass α] {s : Finset α} (t : Finset α), 1 ∈ s → t ⊆ s * t
-- Lean.Elab.Exception
Lean.Elab.throwAbortTactic : {α : Type u_1} → {m : Type u_1 → Type u_2} → [MonadExcept Lean.Exception m] → m α
-- Mathlib.Algebra.BigOperators.Associated
/-- **Alias** of `Associates.finsetProd_mk`. -/
Associates.finset_prod_mk : ∀ {ι : Type u_1} {M : Type u_2} [inst : CommMonoid M] {p : Finset ι} {f : ι → M},
  ∏ i ∈ p, Associates.mk (f i) = Associates.mk (∏ i ∈ p, f i)
-- Lean.LibrarySuggestions.SymbolFrequency
/-- A global `IO.Ref` containing the symbol frequency map. This is initialized on first use.  -/
_private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.LibrarySuggestions.symbolFrequencyMapRef : IO.Ref (Option (Lean.NameMap ℕ))
-- Mathlib.RingTheory.LocalRing.MaximalIdeal.Basic
IsLocalRing.isField_iff_maximalIdeal_eq : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : IsLocalRing R], IsField R ↔ IsLocalRing.maximalIdeal R = ⊥