mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Enumerative.Composition
Composition.sizeUpTo_succ' : ∀ {n : ℕ} (c : Composition n) (i : Fin c.length), c.sizeUpTo (↑i + 1) = c.sizeUpTo ↑i + c.blocksFun i
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.Const.toListModel_modify : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {t : Std.DTreeMap.Internal.Impl α fun x => β} {a : α} {f : β → β},
  t.Balanced →
    t.Ordered →
      (Std.DTreeMap.Internal.Impl.Const.modify a f t).toListModel.Perm
        (Std.Internal.List.Const.modifyKey a f t.toListModel)
-- Init.Data.Format.Basic
_private.Init.Data.Format.Basic.0.Std.Format.State.mk.sizeOf_spec : ∀ (out : String) (column : ℕ), sizeOf { out := out, column := column } = 1 + sizeOf out + sizeOf column
-- Mathlib.Analysis.Normed.Module.FiniteDimension
AffineEquiv.toContinuousAffineEquiv_symm_apply : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type v} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type w} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : CompleteSpace 𝕜] {PE : Type u_1} {PF : Type u_2} [inst_6 : MetricSpace PE] [inst_7 : NormedAddTorsor E PE]
  [inst_8 : MetricSpace PF] [inst_9 : NormedAddTorsor F PF] [inst_10 : FiniteDimensional 𝕜 E] (f : PE ≃ᴬ[𝕜] PF),
  AffineEquiv.toContinuousAffineEquiv.symm f = ↑f
-- Init.Data.Array.BasicAux
_private.Init.Data.Array.BasicAux.0.List.size_toArrayAux : ∀ {α : Type u_1} {as : List α} {bs : Array α}, (as.toArrayAux bs).size = as.length + bs.size
-- Mathlib.Data.Num.Basic
/-- `castPosNum` casts a `PosNum` into any type which has `1` and `+`.  -/
castPosNum : {α : Type u_1} → [One α] → [Add α] → PosNum → α
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_sub : ∀ (a b : UInt8), (a - b).toUInt64 = (a.toUInt64 - b.toUInt64) % 256
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- If `F` and `G` are naturally isomorphic, then `F.mapCocone c` being a colimit implies
`G.mapCocone c` is also a colimit.
 -/
CategoryTheory.Limits.IsColimit.mapCoconeEquiv : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {D : Type u₄} →
          [inst_2 : CategoryTheory.Category.{v₄, u₄} D] →
            {K : CategoryTheory.Functor J C} →
              {F G : CategoryTheory.Functor C D} →
                (F ≅ G) →
                  {c : CategoryTheory.Limits.Cocone K} →
                    CategoryTheory.Limits.IsColimit (F.mapCocone c) → CategoryTheory.Limits.IsColimit (G.mapCocone c)
-- Lean.Meta.Tactic.Cases
Lean.Meta.GeneralizeIndicesSubgoal.indicesFVarIds : Lean.Meta.GeneralizeIndicesSubgoal → Array Lean.FVarId
-- Mathlib.GroupTheory.Coxeter.Inversion
CoxeterSystem.leftInvSeq.eq_1 : ∀ {B : Type u_1} {W : Type u_2} [inst : Group W] {M : CoxeterMatrix B} (cs : CoxeterSystem M W), cs.leftInvSeq [] = []
-- Mathlib.Analysis.Asymptotics.TVS
/-- **Alias** of the forward direction of `Asymptotics.isLittleOTVS_iff_smallSets`. -/
Asymptotics.IsLittleOTVS.eventually_smallSets : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} {g : α → F},
  f =o[𝕜; l] g →
    ∀ U ∈ nhds 0,
      ∀ᶠ (V : Set F) in (nhds 0).smallSets,
        ∀ (ε : NNReal), ε ≠ 0 → ∀ᶠ (x : α) in l, egauge 𝕜 U (f x) ≤ ↑ε * egauge 𝕜 V (g x)
-- Mathlib.Tactic.Linter.TextBased
/-- Lint a collection of input strings for a semicolon preceded by a space.  -/
_private.Mathlib.Tactic.Linter.TextBased.0.Mathlib.Linter.TextBased.semicolonLinter : Mathlib.Linter.TextBased.TextbasedLinter✝
-- Mathlib.Combinatorics.Colex
Finset.Colex.toColex_lt_toColex_iff_exists_forall_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Finset α},
  toColex s < toColex t ↔ ∃ a ∈ t, a ∉ s ∧ ∀ b ∈ s, b ∉ t → b < a
-- Mathlib.CategoryTheory.Abelian.Projective.Resolution
/-- Auxiliary construction for `lift`.  -/
CategoryTheory.ProjectiveResolution.liftFSucc : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      {Y Z : C} →
        (P : CategoryTheory.ProjectiveResolution Y) →
          (Q : CategoryTheory.ProjectiveResolution Z) →
            (n : ℕ) →
              (g : P.complex.X n ⟶ Q.complex.X n) →
                (g' : P.complex.X (n + 1) ⟶ Q.complex.X (n + 1)) →
                  CategoryTheory.CategoryStruct.comp g' (Q.complex.d (n + 1) n) =
                      CategoryTheory.CategoryStruct.comp (P.complex.d (n + 1) n) g →
                    (g'' : P.complex.X (n + 2) ⟶ Q.complex.X (n + 2)) ×'
                      CategoryTheory.CategoryStruct.comp g'' (Q.complex.d (n + 2) (n + 1)) =
                        CategoryTheory.CategoryStruct.comp (P.complex.d (n + 2) (n + 1)) g'
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.ofList_eq_insertMany_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {l : List α},
  Std.ExtHashSet.ofList l = ∅.insertMany l
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackComparison_comp_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z : C} {D : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} D] (G : CategoryTheory.Functor C D) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst_2 : CategoryTheory.Limits.HasPullback f g] [inst_3 : CategoryTheory.Limits.HasPullback (G.map f) (G.map g)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G f g)
      (CategoryTheory.Limits.pullback.fst (G.map f) (G.map g)) =
    G.map (CategoryTheory.Limits.pullback.fst f g)
-- Mathlib.Algebra.Group.Units.Equiv
AddUnits.addLeft_apply : ∀ {M : Type u_3} [inst : AddMonoid M] (u : AddUnits M), ⇑u.addLeft = fun x => ↑u + x
-- Init.Data.UInt.Bitwise
UInt16.toFin_not : ∀ (a : UInt16), (~~~a).toFin = a.toFin.rev
-- Mathlib.Tactic.Explode.Datatypes
Mathlib.Explode.Entry.mk.inj : ∀ {type : Lean.MessageData} {line : Option ℕ} {depth : ℕ} {status : Mathlib.Explode.Status} {thm : Lean.MessageData}
  {deps : List (Option ℕ)} {useAsDep : Bool} {type_1 : Lean.MessageData} {line_1 : Option ℕ} {depth_1 : ℕ}
  {status_1 : Mathlib.Explode.Status} {thm_1 : Lean.MessageData} {deps_1 : List (Option ℕ)} {useAsDep_1 : Bool},
  { type := type, line := line, depth := depth, status := status, thm := thm, deps := deps, useAsDep := useAsDep } =
      { type := type_1, line := line_1, depth := depth_1, status := status_1, thm := thm_1, deps := deps_1,
        useAsDep := useAsDep_1 } →
    type = type_1 ∧
      line = line_1 ∧ depth = depth_1 ∧ status = status_1 ∧ thm = thm_1 ∧ deps = deps_1 ∧ useAsDep = useAsDep_1
-- Mathlib.LinearAlgebra.TensorProduct.Map
/-- Given a linear map `f : N → P`, `f ⊗ M` is injective if and only if `M ⊗ f` is injective.  -/
LinearMap.lTensor_inj_iff_rTensor_inj : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N →ₗ[R] P),
  Function.Injective ⇑(LinearMap.lTensor M f) ↔ Function.Injective ⇑(LinearMap.rTensor M f)
-- Lean.CoreM
_private.Lean.CoreM.0.Lean.DeclNameGenerator.idxs : Lean.DeclNameGenerator → List ℕ
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mapComp_hom_app_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X Y Z : T} (f : X ⟶ Y) (g : Y ⟶ Z)
  (X_1 : CategoryTheory.Over X),
  ((CategoryTheory.Over.mapComp f g).hom.app X_1).left = CategoryTheory.CategoryStruct.id X_1.left
-- Init.Data.String.Lemmas.Pattern.Basic
String.Slice.Pattern.Model.isRevMatch_ofSliceFrom_iff : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.Model.PatternModel pat] {s : String.Slice} {p : s.Pos}
  {pos : (s.sliceFrom p).Pos},
  String.Slice.Pattern.Model.IsRevMatch pat (String.Slice.Pos.ofSliceFrom pos) ↔
    String.Slice.Pattern.Model.IsRevMatch pat pos
-- Lean.Meta.Tactic.Grind.Types
/-- Registers a new solver extension for `grind`.
Solver extensions can only be registered during initialization.
Reason: We do not use any synchronization primitive to access `solverExtensionsRef`.
 -/
Lean.Meta.Grind.registerSolverExtension : {σ : Type} → IO σ → IO (Lean.Meta.Grind.SolverExtension σ)
-- Mathlib.Topology.Order.DenselyOrdered
/-- The closure of the interval `(a, b]` is the closed interval `[a, b]`.  -/
closure_Ioc : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [DenselyOrdered α] {a b : α},
  a ≠ b → closure (Set.Ioc a b) = Set.Icc a b
-- Mathlib.Geometry.Euclidean.Inversion.Basic
EuclideanGeometry.inversion_def : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P], EuclideanGeometry.inversion = fun c R x => (R / dist x c) ^ 2 • (x -ᵥ c) +ᵥ c
-- Mathlib.Order.Basic
/-- **Alias** of `le_of_eq_of_le''`. -/
Eq.trans_ge : ∀ {α : Type u_1} {a b c : α} [inst : LE α], a = b → c ≤ b → c ≤ a
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.instLawfulBEqPoly : LawfulBEq Lean.Grind.CommRing.Poly
-- Mathlib.Algebra.Lie.TraceForm
_private.Mathlib.Algebra.Lie.TraceForm.0.termφ : Lean.ParserDescr
-- Init.Data.List.Lemmas
List.mem_nil_iff : ∀ {α : Type u_1} (a : α), a ∈ [] ↔ False
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.mem_iSup : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Sort u_9}
  (p : ι → Submodule R M) {m : M}, m ∈ ⨆ i, p i ↔ ∀ (N : Submodule R M), (∀ (i : ι), p i ≤ N) → m ∈ N
-- Mathlib.Algebra.Group.Finsupp
Finsupp.mapRange.addMonoidHom_comp : ∀ {ι : Type u_1} {M : Type u_3} {N : Type u_4} {O : Type u_5} [inst : AddCommMonoid M] [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid O] (f : N →+ O) (g : M →+ N),
  Finsupp.mapRange.addMonoidHom (f.comp g) = (Finsupp.mapRange.addMonoidHom f).comp (Finsupp.mapRange.addMonoidHom g)
-- Mathlib.Order.SuccPred.WithBot
WithBot.succ_mono : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : OrderBot α] [inst_2 : SuccOrder α], Monotone WithBot.succ
-- Mathlib.Topology.CWComplex.Classical.Basic
Topology.RelCWComplex.closedCell_subset_complex : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D] (n : ℕ)
  (j : Topology.RelCWComplex.cell C n), Topology.RelCWComplex.closedCell n j ⊆ C
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The cokernel of `δ : H^{n-1}(g) ⟶ H^n(g)`. In the documentation,
this may be shortened as `opZ^n₁(f, g)`.  -/
CategoryTheory.Abelian.SpectralObject.opcycles : {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.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι → {i j k : ι} → (i ⟶ j) → (j ⟶ k) → ℤ → C
-- Lean.Elab.BuiltinNotation
_private.Lean.Elab.BuiltinNotation.0.Lean.Elab.Term.expandCDot?.mkVarFrom : Lean.Syntax → String → Lean.MacroM Lean.Ident
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.baseChange_slope : ∀ {R : Type r} {S : Type s} {F : Type u} {K : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Field F]
  [inst_3 : Field K] {W' : WeierstrassCurve.Affine R} [inst_4 : Algebra R S] [inst_5 : DecidableEq F]
  [inst_6 : DecidableEq K] [inst_7 : Algebra R F] [inst_8 : Algebra S F] [IsScalarTower R S F] [inst_10 : Algebra R K]
  [inst_11 : Algebra S K] [IsScalarTower R S K] (f : F →ₐ[S] K) (x₁ x₂ y₁ y₂ : F),
  (W'.baseChange K).slope (f x₁) (f x₂) (f y₁) (f y₂) = f ((W'.baseChange F).slope x₁ x₂ y₁ y₂)
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.linearEquivAt_apply : ∀ (R : Type u_1) {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] (b : B)
  (hb : b ∈ e.baseSet), ⇑(Bundle.Pretrivialization.linearEquivAt R e b hb) = fun y => (↑e ⟨b, y⟩).2
-- Mathlib.Geometry.Manifold.Algebra.SmoothFunctions
/-- Coercion to a function as an `AlgHom`.  -/
ContMDiffMap.coeFnAlgHom : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {H : Type u_4} →
            [inst_3 : TopologicalSpace H] →
              {I : ModelWithCorners 𝕜 E H} →
                {N : Type u_6} →
                  [inst_4 : TopologicalSpace N] →
                    [inst_5 : ChartedSpace H N] →
                      {n : WithTop ℕ∞} →
                        {A : Type u_10} →
                          [inst_6 : NormedRing A] →
                            [inst_7 : NormedAlgebra 𝕜 A] →
                              [inst_8 : ContMDiffRing (modelWithCornersSelf 𝕜 A) n A] →
                                ContMDiffMap I (modelWithCornersSelf 𝕜 A) N A n →ₐ[𝕜] N → A
-- Mathlib.Algebra.Group.Pi.Lemmas
AddHom.pi_injective : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → Add (f i)] {γ : Type w} [Nonempty I] [inst_2 : Add γ]
  (g : (i : I) → γ →ₙ+ f i), (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(AddHom.pi g)
-- Lean.Declaration
Lean.instInhabitedOpaqueVal : Inhabited Lean.OpaqueVal
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.coeff_pow_nsmul_degree : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] (f : MvPolynomial σ R) (n : ℕ),
  MvPolynomial.coeff (n • m.degree f) (f ^ n) = m.leadingCoeff f ^ n
-- Mathlib.Topology.Defs.Filter
/-- The "neighbourhood within" filter for sets. Elements of `𝓝[t] s` are sets containing the
intersection of `t` and a neighbourhood of `s`.  -/
nhdsSetWithin : {X : Type u_1} → [TopologicalSpace X] → Set X → Set X → Filter X
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.IsAdmissible.mk : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α} {s : Set α},
  IsLeast s x →
    f '' s ⊆ s →
      (∀ (c : NonemptyChain α), ↑c ⊆ s → ChainCompletePartialOrder.cSup c ∈ s) →
        ChainCompletePartialOrder.IsAdmissible x f s
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_toUInt16 : ∀ (n : UInt8), n.toUInt16.toUInt64 = n.toUInt64
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The functor `(Φ.op.RightResolution X₂)ᵒᵖ ⥤ Φ.LeftResolution X₂.unop`.  -/
CategoryTheory.LocalizerMorphism.RightResolution.unopFunctor : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) →
              (X₂ : C₂ᵒᵖ) → CategoryTheory.Functor (Φ.op.RightResolution X₂)ᵒᵖ (Φ.LeftResolution (Opposite.unop X₂))
-- Mathlib.Data.Subtype
Function.extend_val_apply' : ∀ {β : Sort u_2} {γ : Sort u_3} {p : β → Prop} {g : { x // p x } → γ} {j : β → γ} {b : β},
  ¬p b → Function.extend Subtype.val g j b = j b
-- Mathlib.Algebra.Module.Congruence.Defs
SMulCon.ker.eq_1 : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_3} {N : Type u_4} [inst : SMul R M] [inst_1 : SMul S N] {φ : R → S}
  (f : M →ₑ[φ] N), SMulCon.ker f = { toSetoid := Setoid.ker ⇑f, smul := ⋯ }
-- Lean.DocString.Types
Lean.Doc.Inline.footnote.injEq : ∀ {i : Type u} (name : String) (content : Array (Lean.Doc.Inline i)) (name_1 : String)
  (content_1 : Array (Lean.Doc.Inline i)),
  (Lean.Doc.Inline.footnote name content = Lean.Doc.Inline.footnote name_1 content_1) =
    (name = name_1 ∧ content = content_1)
-- Mathlib.Logic.Equiv.Set
Equiv.swap_bijOn_self : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Set α}, (a ∈ s ↔ b ∈ s) → Set.BijOn (⇑(Equiv.swap a b)) s s
-- Mathlib.NumberTheory.Cyclotomic.Basic
IntermediateField.isCyclotomicExtension_lcm_sup : ∀ (K : Type w) (L : Type z) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (n₁ n₂ : ℕ)
  (F₁ F₂ : IntermediateField K L) [h₁ : IsCyclotomicExtension {n₁} K ↥F₁] [h₂ : IsCyclotomicExtension {n₂} K ↥F₂]
  [NeZero n₁] [NeZero n₂], IsCyclotomicExtension {n₁.lcm n₂} K ↥(F₁ ⊔ F₂)
-- Mathlib.Logic.Equiv.Prod
Equiv.sumPiEquivProdPi_apply : ∀ {ι : Type u_10} {ι' : Type u_11} (π : ι ⊕ ι' → Type u_9) (f : (i : ι ⊕ ι') → π i),
  (Equiv.sumPiEquivProdPi π) f = (fun i => f (Sum.inl i), fun i' => f (Sum.inr i'))
-- Mathlib.GroupTheory.Index
AddSubgroup.finiteIndex_of_finite : ∀ {G : Type u_1} [inst : AddGroup G] {H : AddSubgroup G} [Finite G], H.FiniteIndex
-- Mathlib.Algebra.Module.LinearMap.Prod
IsLinearMap.isLinearMap_add : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsLinearMap R fun x => x.1 + x.2
-- Mathlib.Algebra.Quaternion
Quaternion.equivTuple_symm_apply : ∀ (R : Type u_1) [inst : Zero R] [inst_1 : One R] [inst_2 : Neg R] (a : Fin 4 → R),
  (Quaternion.equivTuple R).symm a = { re := a 0, imI := a 1, imJ := a 2, imK := a 3 }
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
/-- The functor induced by the identity is the identity.  -/
CategoryTheory.FreeGroupoid.mapId : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    CategoryTheory.FreeGroupoid.map (CategoryTheory.Functor.id C) ≅
      CategoryTheory.Functor.id (CategoryTheory.FreeGroupoid C)
-- Mathlib.Analysis.Normed.Group.Hom
NormedAddGroupHom.smulCommClass : ∀ {V₁ : Type u_2} {V₂ : Type u_3} [inst : SeminormedAddCommGroup V₁] [inst_1 : SeminormedAddCommGroup V₂] {R : Type u_5}
  {R' : Type u_6} [inst_2 : MonoidWithZero R] [inst_3 : DistribMulAction R V₂] [inst_4 : PseudoMetricSpace R]
  [inst_5 : IsBoundedSMul R V₂] [inst_6 : MonoidWithZero R'] [inst_7 : DistribMulAction R' V₂]
  [inst_8 : PseudoMetricSpace R'] [inst_9 : IsBoundedSMul R' V₂] [SMulCommClass R R' V₂],
  SMulCommClass R R' (NormedAddGroupHom V₁ V₂)
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.comp : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] {N : Type u_3} [inst_1 : Zero N] {g : M → N} {f : α → M},
  Function.HasFiniteSupport f → g 0 = 0 → Function.HasFiniteSupport (g ∘ f)
-- Mathlib.Algebra.Algebra.Operations
Submodule.map_op_pow : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A)
  (n : ℕ), Submodule.map (↑(MulOpposite.opLinearEquiv R)) (M ^ n) = Submodule.map (↑(MulOpposite.opLinearEquiv R)) M ^ n
-- Mathlib.Data.Seq.Computation
/-- `pure a` is the computation that immediately terminates with result `a`.  -/
Computation.pure : {α : Type u} → α → Computation α
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
/-- Constructor for objects of the category `Functor.RightExtension L F`.  -/
CategoryTheory.Functor.RightExtension.mk : {C : Type u_1} →
  {H : Type u_3} →
    {D : Type u_4} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_3, u_3} H] →
          [inst_2 : CategoryTheory.Category.{v_4, u_4} D] →
            (F' : CategoryTheory.Functor D H) →
              {L : CategoryTheory.Functor C D} → {F : CategoryTheory.Functor C H} → (L.comp F' ⟶ F) → L.RightExtension F
-- Mathlib.Data.Setoid.Basic
/-- The supremum of a set S of equivalence relations is the equivalence closure of the binary
relation `there exists r ∈ S relating x and y`.  -/
Setoid.sSup_eq_eqvGen : ∀ {α : Type u_1} (S : Set (Setoid α)), sSup S = Relation.EqvGen.setoid fun x y => ∃ r ∈ S, r x y
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.coeffLinearEquiv_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]
  (a : AddMonoidAlgebra S M), (AddMonoidAlgebra.coeffLinearEquiv R) a = a.coeff
-- Mathlib.Topology.UniformSpace.Equiv
/-- A uniform isomorphism `e : α ≃ᵤ β` lifts to subtypes `{ a : α // p a } ≃ᵤ { b : β // q b }`
provided `p = q ∘ e`.  -/
UniformEquiv.subtype : {α : Type u} →
  {β : Type u_1} →
    [inst : UniformSpace α] →
      [inst_1 : UniformSpace β] →
        {p : α → Prop} → {q : β → Prop} → (e : α ≃ᵤ β) → (∀ (a : α), p a ↔ q (e a)) → { a // p a } ≃ᵤ { b // q b }
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.edgeSet_concat : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} (p : G.Walk u v) (h : G.Adj v w),
  (p.concat h).edgeSet = insert s(v, w) p.edgeSet
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- If `s` is not in `-ℕ`, then `sinZeta a (1 - s)` is an explicit multiple of
`hurwitzZetaOdd s`.  -/
HurwitzZeta.sinZeta_one_sub : ∀ (a : UnitAddCircle) {s : ℂ},
  (∀ (n : ℕ), s ≠ -↑n) →
    HurwitzZeta.sinZeta a (1 - s) =
      2 * (2 * ↑Real.pi) ^ (-s) * Complex.Gamma s * Complex.sin (↑Real.pi * s / 2) * HurwitzZeta.hurwitzZetaOdd a s
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.go.eq_1 : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) (x : α) (i j : ℕ),
  List.minIdxOn.go✝ f x i j [] = i
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.add : Int.Internal.Linear.Expr → Int.Internal.Linear.Expr → Int.Internal.Linear.Expr
-- Mathlib.Data.Nat.Prime.Basic
Nat.Prime.even_iff : ∀ {p : ℕ}, Nat.Prime p → (Even p ↔ p = 2)
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.preservesEpimorphisms_π₂ : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasColimitsOfShape CategoryTheory.Limits.WalkingSpan C],
  CategoryTheory.ShortComplex.π₂.PreservesEpimorphisms
-- Mathlib.Analysis.Seminorm
Seminorm.bddAbove_range_iff : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E] {ι : Sort u_12}
  {p : ι → Seminorm 𝕜 E}, BddAbove (Set.range p) ↔ ∀ (x : E), BddAbove (Set.range fun i => (p i) x)
-- Mathlib.GroupTheory.PGroup
IsPGroup.card : ∀ {G : Type u_1} [inst : Group G], IsPGroup (Nat.card G) G
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Basic
CategoryTheory.isPullback_iff_isLimit_binaryFan_of_isThin : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [Quiver.IsThin C] {P X Y Z : C} {fst : P ⟶ X} {snd : P ⟶ Y}
  {f : X ⟶ Z} {g : Y ⟶ Z},
  CategoryTheory.IsPullback fst snd f g ↔
    Nonempty (CategoryTheory.Limits.IsLimit (CategoryTheory.Limits.BinaryFan.mk fst snd))
-- Std.Data.HashSet.IteratorLemmas
Std.HashSet.Raw.toList_iter : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → m.iter.toList = m.toList
-- Mathlib.RingTheory.IntegralClosure.IsIntegral.Basic
isIntegral_algEquiv : ∀ {R : Type u_1} [inst : CommRing R] {A : Type u_5} {B : Type u_6} [inst_1 : Ring A] [inst_2 : Ring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] (f : A ≃ₐ[R] B) {x : A}, IsIntegral R (f x) ↔ IsIntegral R x
-- Mathlib.Topology.Homeomorph.Lemmas
/-- If `h : X → Y` is a homeomorphism, `h⁻¹(s)` is σ-compact iff `s` is.  -/
Homeomorph.isSigmaCompact_preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {s : Set Y} (h : X ≃ₜ Y),
  IsSigmaCompact (⇑h ⁻¹' s) ↔ IsSigmaCompact s
-- Mathlib.Algebra.Star.SelfAdjoint
IsStarNormal.star : ∀ {R : Type u_1} [inst : Mul R] [inst_1 : StarMul R] {x : R} [IsStarNormal x], IsStarNormal (star x)
-- Std.Async.System
Std.Async.System.UserId.mk.injEq : ∀ (toNat toNat_1 : ℕ), ({ toNat := toNat } = { toNat := toNat_1 }) = (toNat = toNat_1)
-- Mathlib.Algebra.Order.Archimedean.Basic
existsUnique_sub_zpow_mem_Ioc : ∀ {G : Type u_1} [inst : CommGroup G] [inst_1 : LinearOrder G] [IsOrderedMonoid G] [MulArchimedean G] {a : G},
  1 < a → ∀ (b c : G), ∃! m, b / a ^ m ∈ Set.Ioc c (c * a)
-- Lean.Parser.Basic
Lean.Parser.satisfySymbolFn : (String → Bool) → List String → Lean.Parser.ParserFn
-- Lean.Compiler.LCNF.Basic
/-- Projecting objects out of a value.
 -/
Lean.Compiler.LCNF.LetValue.oproj : {pu : Lean.Compiler.LCNF.Purity} →
  ℕ →
    Lean.FVarId →
      autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.LetValue._auto_7 →
        Lean.Compiler.LCNF.LetValue pu