mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transformObjPrecomposeObjSquare_iso_inv_app_fst_app : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B} {A₁ : Type u₄} {B₁ : Type u₅} {C₁ : Type u₆}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A₁] [inst_4 : CategoryTheory.Category.{v₅, u₅} B₁]
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C₁] {F₁ : CategoryTheory.Functor A₁ B₁} {G₁ : CategoryTheory.Functor C₁ B₁}
  {X : Type u₇} {Y : Type u₈} [inst_6 : CategoryTheory.Category.{v₇, u₇} X]
  [inst_7 : CategoryTheory.Category.{v₈, u₈} Y] (U : CategoryTheory.Functor X Y)
  (ψ : CategoryTheory.Limits.CatCospanTransform F G F₁ G₁)
  (X_1 : CategoryTheory.Limits.CategoricalPullback.CatCommSqOver F G Y) (x : X),
  ((CategoryTheory.CatCommSq.iso ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform Y).obj ψ)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F G).obj U)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.precompose F₁ G₁).obj U)
                  ((CategoryTheory.Limits.CategoricalPullback.CatCommSqOver.transform X).obj ψ)).inv.app
            X_1).fst.app
      x =
    CategoryTheory.CategoryStruct.id (ψ.left.obj (X_1.fst.obj (U.obj x)))
-- Init.Data.Bool
Bool.not_ite_eq_true_eq_false : ∀ {p : Prop} [h : Decidable p] {b c : Bool}, (¬if p then b = true else c = false) ↔ if p then b = false else c = true
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
/-- A choice of wide pullback.  -/
CategoryTheory.Limits.widePullback : {J : Type w} →
  {C : Type u} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (B : C) →
        (objs : J → C) → (arrows : (j : J) → objs j ⟶ B) → [CategoryTheory.Limits.HasWidePullback B objs arrows] → C
-- Mathlib.Algebra.Group.Shrink
Shrink.instAddSemigroup : {α : Type u_2} → [inst : Small.{v, u_2} α] → [AddSemigroup α] → AddSemigroup (Shrink.{v, u_2} α)
-- Mathlib.RingTheory.Kaehler.TensorProduct
KaehlerDifferential.instSMulCommClassTensorProduct_1 : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : CommRing A] [inst_4 : Algebra R A], SMulCommClass A S (TensorProduct R S Ω[A⁄R])
-- Mathlib.Probability.Distributions.Gaussian.Fernique
ProbabilityTheory.IsGaussian.integrable_id : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [ProbabilityTheory.IsGaussian μ] [CompleteSpace E] [SecondCountableTopology E],
  MeasureTheory.Integrable id μ
-- Mathlib.Data.Ordmap.Ordnode
/-- O(m * log(|m ∪ n| + 1)), m ≤ n. Difference of two sets.

```
diff {1, 2} {2, 3} = {1}
diff {1, 2, 3} {2} = {1, 3}
```  -/
Ordnode.diff : {α : Type u_1} → [inst : LE α] → [DecidableLE α] → Ordnode α → Ordnode α → Ordnode α
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constGetEntryGT!_eq : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α],
  t₁.WF →
    t₂.WF →
      t₁.Equiv t₂ →
        ∀ {k : α} [inst : Inhabited (α × β)],
          Std.DTreeMap.Internal.Impl.Const.getEntryGT! k t₁ = Std.DTreeMap.Internal.Impl.Const.getEntryGT! k t₂
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_ofNat' : ∀ (n : ℕ), (UInt32.ofNat n).toUInt16 = UInt16.ofNat n
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.HasUnifEigenvector.apply_eq_smul : ∀ {R : Type v} {M : Type w} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {f : Module.End R M}
  {μ : R} {x : M}, f.HasUnifEigenvector μ 1 x → f x = μ • x
-- Mathlib.Order.Hom.Lattice
LatticeHom.coe_comp_inf_hom' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : Lattice α] [inst_1 : Lattice β] [inst_2 : Lattice γ]
  (f : LatticeHom β γ) (g : LatticeHom α β),
  { toFun := ⇑f ∘ ⇑g, map_inf' := ⋯ } = { toFun := ⇑f, map_inf' := ⋯ }.comp { toFun := ⇑g, map_inf' := ⋯ }
-- Mathlib.Data.Nat.Factorization.Basic
Nat.factorization_eq_card_pow_dvd : ∀ (n : ℕ) {p : ℕ}, Nat.Prime p → n.factorization p = {i ∈ Finset.Ico 1 n | p ^ i ∣ n}.card
-- Mathlib.AlgebraicGeometry.ResidueField
AlgebraicGeometry.Scheme.residueFieldCongr_trans_hom : ∀ (X : AlgebraicGeometry.Scheme) {x y z : ↥X} (e : x = y) (e' : y = z),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.residueFieldCongr e).hom
      (AlgebraicGeometry.Scheme.residueFieldCongr e').hom =
    (AlgebraicGeometry.Scheme.residueFieldCongr ⋯).hom
-- Mathlib.RingTheory.TensorProduct.Pi
/-- The canonical map `A ⊗[R] (∀ i, B i) →ₐ[S] ∀ i, A ⊗[R] B i`. This is an isomorphism
if `ι` is finite (see `Algebra.TensorProduct.piRight`).  -/
Algebra.TensorProduct.piRightHom : (R : Type u_1) →
  (S : Type u_2) →
    (A : Type u_3) →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] →
            [inst_3 : Semiring A] →
              [inst_4 : Algebra R A] →
                [inst_5 : Algebra S A] →
                  [inst_6 : IsScalarTower R S A] →
                    {ι : Type u_4} →
                      (B : ι → Type u_5) →
                        [inst_7 : (i : ι) → Semiring (B i)] →
                          [inst_8 : (i : ι) → Algebra R (B i)] →
                            TensorProduct R A ((i : ι) → B i) →ₐ[S] (i : ι) → TensorProduct R A (B i)
-- Init.Data.UInt.Lemmas
UInt32.toUInt16_mul : ∀ (a b : UInt32), (a * b).toUInt16 = a.toUInt16 * b.toUInt16
-- Mathlib.FieldTheory.Extension
AlgHom.domRestrict.congr_simp : ∀ {A : Type u_3} (B : Type u_4) {C : Type u_5} {D : Type u_6} [inst : CommSemiring A] [inst_1 : CommSemiring C]
  [inst_2 : CommSemiring D] [inst_3 : Algebra A C] [inst_4 : Algebra A D] [inst_5 : CommSemiring B]
  [inst_6 : Algebra A B] [inst_7 : Algebra B C] [inst_8 : IsScalarTower A B C] (f f_1 : C →ₐ[A] D),
  f = f_1 → AlgHom.domRestrict B f = AlgHom.domRestrict B f_1
-- Mathlib.Dynamics.PeriodicPts.Defs
AddAction.zsmul_add_period_vadd : ∀ {α : Type v} {G : Type u} [inst : AddGroup G] [inst_1 : AddAction G α] (i : ℤ) (g : G) (a : α),
  (i + ↑(AddAction.period g a)) • g +ᵥ a = i • g +ᵥ a
-- Mathlib.Data.Set.Card
Set.ncard_def : ∀ {α : Type u_1} (s : Set α), s.ncard = s.encard.toNat
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic
_private.Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Basic.0.IsProperLinearSet.setOfFloorPos : {ι : Type u_3} → {s : Set (ι → ℕ)} → IsProperLinearSet s → [Finite ι] → Set (ι → ℕ)
-- Mathlib.Order.Max
IsMax.mono : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, IsMax a → a ≤ b → IsMax b
-- Mathlib.CategoryTheory.MorphismProperty.Representable
/-- Assume that
1. `C` has binary products,
2. `D` has pullbacks, binary products and a terminal object, and
3. `F : C ⥤ D` is full and preserves binary products.

For an object `X` in a category `D`, if the diagonal morphism `X ⟶ X × X` is relatively
representable, then every morphism of the form `F.obj a ⟶ X` is relatively representable with
respect to `F`.
 -/
CategoryTheory.Functor.relativelyRepresentable.of_diag : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [CategoryTheory.Limits.HasBinaryProducts C] [CategoryTheory.Limits.HasPullbacks D]
  [inst_4 : CategoryTheory.Limits.HasBinaryProducts D] [CategoryTheory.Limits.HasTerminal D] [F.Full]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete CategoryTheory.Limits.WalkingPair) F] {X : D},
  F.relativelyRepresentable (CategoryTheory.Limits.diag X) → ∀ ⦃a : C⦄ (g : F.obj a ⟶ X), F.relativelyRepresentable g
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.comp_f : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} {C₁ C₂ C₃ : HomologicalComplex V c}
  (f : C₁ ⟶ C₂) (g : C₂ ⟶ C₃) (i : ι),
  (CategoryTheory.CategoryStruct.comp f g).f i = CategoryTheory.CategoryStruct.comp (f.f i) (g.f i)
-- Lean.LibrarySuggestions.SymbolFrequency
/-- A global `IO.Ref` containing the local symbol frequency map. This is initialized on first use.
 -/
_private.Lean.LibrarySuggestions.SymbolFrequency.0.Lean.LibrarySuggestions.localSymbolFrequencyMapRef : IO.Ref (Option (Lean.NameMap ℕ))
-- Mathlib.Data.Finsupp.Encodable
instEncodableFinsuppOfDecidableNeOfNat : {α : Type u_1} →
  {β : Type u_2} → [Encodable α] → [Encodable β] → [inst : Zero β] → [(x : β) → Decidable (x ≠ 0)] → Encodable (α →₀ β)
-- Mathlib.CategoryTheory.Sigma.Basic
CategoryTheory.Sigma.SigmaHom.mk.injEq : ∀ {I : Type w₁} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {i : I} {X Y : C i}
  (a a_1 : X ⟶ Y), (CategoryTheory.Sigma.SigmaHom.mk a = CategoryTheory.Sigma.SigmaHom.mk a_1) = (a = a_1)
-- Lean.Elab.BuiltinTerm
Lean.Elab.Term.elabProp : Lean.Elab.Term.TermElab
-- Mathlib.MeasureTheory.Measure.WithDensity
/-- The Lebesgue integral of `g` with respect to the measure `μ.withDensity f` coincides with
the integral of `f * g`. This version assumes that `g` is almost everywhere measurable. For a
version without conditions on `g` but requiring that `f` is almost everywhere finite, see
`lintegral_withDensity_eq_lintegral_mul_non_measurable`  -/
MeasureTheory.lintegral_withDensity_eq_lintegral_mul₀' : ∀ {α : Type u_1} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → ENNReal},
  AEMeasurable f μ →
    ∀ {g : α → ENNReal}, AEMeasurable g (μ.withDensity f) → ∫⁻ (a : α), g a ∂μ.withDensity f = ∫⁻ (a : α), (f * g) a ∂μ
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.toArray_filter! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} {f : (a : α) → β a → Bool},
  t.WF → (Std.DTreeMap.Internal.Impl.filter! f t).toArray = Array.filter (fun p => f p.fst p.snd) t.toArray
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
CategoryTheory.EffectiveEpiFamilyStruct.mk : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {B : C} →
      {α : Type u_2} →
        {X : α → C} →
          {π : (a : α) → X a ⟶ B} →
            (desc :
                {W : C} →
                  (e : (a : α) → X a ⟶ W) →
                    (∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
                        CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
                          CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂)) →
                      (B ⟶ W)) →
              (∀ {W : C} (e : (a : α) → X a ⟶ W)
                  (h :
                    ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
                      CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
                        CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
                  (a : α), CategoryTheory.CategoryStruct.comp (π a) (desc e ⋯) = e a) →
                (∀ {W : C} (e : (a : α) → X a ⟶ W)
                    (h :
                      ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
                        CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
                          CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
                    (m : B ⟶ W), (∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) → m = desc e ⋯) →
                  CategoryTheory.EffectiveEpiFamilyStruct X π
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.mapₗ_apply_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {Z : Type u_6} (R : Type u_7) [inst_1 : Semiring R]
  [inst_2 : AddCommMonoid Y] [inst_3 : Module R Y] [inst_4 : AddCommMonoid Z] [inst_5 : Module R Z] (f : Y →ₗ[R] Z)
  (g : LocallyConstant X Y) (a : X), ((LocallyConstant.mapₗ R f) g) a = f (g a)
-- Mathlib.Topology.Instances.RealVectorSpace
AddMonoidHom.coe_toRealLinearMap : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E]
  [inst_3 : ContinuousSMul ℝ E] {F : Type u_2} [inst_4 : AddCommGroup F] [inst_5 : Module ℝ F]
  [inst_6 : TopologicalSpace F] [inst_7 : ContinuousSMul ℝ F] [inst_8 : T2Space F] (f : E →+ F) (hf : Continuous ⇑f),
  ⇑(f.toRealLinearMap hf) = ⇑f
-- Mathlib.CategoryTheory.Action.Limits
/-- `F.mapAction : Action V G ⥤ Action W G` preserves finite limits if
`V` has finite limits and `F` preserves finite limits.  -/
Action.Functor.instPreservesFiniteLimitsMapActionOfHasFiniteLimits : ∀ {V : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} V] {W : Type u_3}
  [inst_1 : CategoryTheory.Category.{v_2, u_3} W] (F : CategoryTheory.Functor V W) (G : Type u_4) [inst_2 : Monoid G]
  [CategoryTheory.Limits.PreservesFiniteLimits F] [CategoryTheory.Limits.HasFiniteLimits V],
  CategoryTheory.Limits.PreservesFiniteLimits (F.mapAction G)
-- Mathlib.Algebra.Star.SelfAdjoint
IsSelfAdjoint.smul_iff : ∀ {R : Type u_1} {A : Type u_2} [inst : Monoid R] [inst_1 : StarMul R] [inst_2 : Star A] [inst_3 : MulAction R A]
  [StarModule R A] {r : R}, IsSelfAdjoint r → IsUnit r → ∀ {x : A}, IsSelfAdjoint (r • x) ↔ IsSelfAdjoint x
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Energy
/-- The energy of a partition, also known as index. Auxiliary quantity for Szemerédi's regularity
lemma.  -/
Finpartition.energy : {α : Type u_1} →
  [inst : DecidableEq α] → {s : Finset α} → Finpartition s → (G : SimpleGraph α) → [DecidableRel G.Adj] → ℚ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.PolarCoord
NumberField.mixedEmbedding.volume_preserving_mixedSpaceToRealMixedSpace_symm : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K],
  MeasureTheory.MeasurePreserving (⇑(NumberField.mixedEmbedding.mixedSpaceToRealMixedSpace K).symm) MeasureTheory.volume
    MeasureTheory.volume
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_addNat_Iic_addNat : ∀ {n : ℕ} (m : ℕ) (i : Fin n), (fun x => x.addNat m) ⁻¹' Set.Iic (i.addNat m) = Set.Iic i
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rio.toArray_eq_toArray_rco : ∀ {α : Type u} {r : Std.Rio α} [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.Least? α]
  [inst_3 : Std.PRange.UpwardEnumerable α] [inst_4 : Std.PRange.LawfulUpwardEnumerable α]
  [Std.PRange.LawfulUpwardEnumerableLT α] [inst_6 : Std.PRange.LawfulUpwardEnumerableLeast? α]
  [inst_7 : Std.Rxo.IsAlwaysFinite α], r.toArray = (Std.PRange.UpwardEnumerable.least...r.upper).toArray
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.getKeyD_eq : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp]
  {k fallback : α}, t₁.WF → t₂.WF → t₁.Equiv t₂ → t₁.getKeyD k fallback = t₂.getKeyD k fallback
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.ExceptT.run_bind.match_1.eq_2 : ∀ {ε α : Type u_1} (motive : Except ε α → Sort u_2) (e : ε) (h_1 : (x : α) → motive (Except.ok x))
  (h_2 : (e : ε) → motive (Except.error e)),
  (match Except.error e with
    | Except.ok x => h_1 x
    | Except.error e => h_2 e) =
    h_2 e
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
mfderiv_id : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {x : M},
  mfderiv% id x = ContinuousLinearMap.id 𝕜 (TangentSpace I x)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentHighlightParams.mk.injEq : ∀ (toTextDocumentPositionParams toTextDocumentPositionParams_1 : Lean.Lsp.TextDocumentPositionParams),
  ({ toTextDocumentPositionParams := toTextDocumentPositionParams } =
      { toTextDocumentPositionParams := toTextDocumentPositionParams_1 }) =
    (toTextDocumentPositionParams = toTextDocumentPositionParams_1)
-- Mathlib.Algebra.Group.Action.Pointwise.Finset
Finset.isScalarTower'' : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : DecidableEq γ] [inst_1 : DecidableEq β] [inst_2 : SMul α β]
  [inst_3 : SMul α γ] [inst_4 : SMul β γ] [IsScalarTower α β γ], IsScalarTower (Finset α) (Finset β) (Finset γ)
-- Mathlib.Topology.Separation.Regular
regularSpace_iInf : ∀ {ι : Sort u_3} {X : Type u_4} {t : ι → TopologicalSpace X}, (∀ (i : ι), RegularSpace X) → RegularSpace X
-- Mathlib.LinearAlgebra.RootSystem.Finite.CanonicalBilinear
/-- A version of SGA3 XXI Lemma 1.2.1 (10).  -/
RootPairing.rootForm_self_smul_coroot : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [inst_5 : Fintype ι]
  (i : ι), (P.RootForm (P.root i)) (P.root i) • P.coroot i = 2 • P.Polarization (P.root i)
-- Mathlib.Algebra.Polynomial.Expand
Polynomial.natDegree_expand : ∀ {R : Type u} [inst : CommSemiring R] (p : ℕ) (f : Polynomial R),
  ((Polynomial.expand R p) f).natDegree = f.natDegree * p
-- Mathlib.FieldTheory.PurelyInseparable.AdjoinPthRoots
AdjoinPthRoots.root_pow : ∀ {k : Type u_1} [inst : Field k] (p : ℕ) [ExpChar k p] (x : k),
  (AdjoinPthRoots.root k) x ^ p = (algebraMap k (AdjoinPthRoots k)) x
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.getD_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  {k : α} {fallback : β}, k ∉ t₁ → Std.DTreeMap.Const.getD (t₁ ∪ t₂) k fallback = Std.DTreeMap.Const.getD t₂ k fallback
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.instLeAtTopSymmetricIoo : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G]
  [inst_3 : LocallyFiniteOrder G] [NoTopOrder G] [NoBotOrder G], (SummationFilter.symmetricIoo G).LeAtTop
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.degrees_C : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (a : R), (MvPolynomial.C a).degrees = 0
-- Mathlib.Data.Option.NAry
Option.map₂_map_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {δ : Type u_4} {a : Option α} {b : Option β} (f : γ → β → δ) (g : α → γ),
  Option.map₂ f (Option.map g a) b = Option.map₂ (fun a b => f (g a) b) a b
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.isoOfIsoLift_hom_inv_id : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ≅ b) [inst_2 : p.IsHomLift f φ.hom],
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.IsHomLift.isoOfIsoLift p f φ).inv =
    CategoryTheory.CategoryStruct.id R
-- Init.Data.List.Lemmas
List.forall_mem_append : ∀ {α : Type u_1} {p : α → Prop} {l₁ l₂ : List α}, (∀ x ∈ l₁ ++ l₂, p x) ↔ (∀ x ∈ l₁, p x) ∧ ∀ x ∈ l₂, p x
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.toArray_toList : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β},
  m.WF → (Std.DHashMap.Raw.Const.toList m).toArray = Std.DHashMap.Raw.Const.toArray m
-- Mathlib.CategoryTheory.Preadditive.HomOrthogonal
CategoryTheory.HomOrthogonal.matrixDecompositionAddEquiv_symm_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {ι : Type u_1} {s : ι → C}
  [inst_1 : CategoryTheory.Preadditive C] [inst_2 : CategoryTheory.Limits.HasFiniteBiproducts C]
  (o : CategoryTheory.HomOrthogonal s) {α β : Type} [inst_3 : Finite α] [inst_4 : Finite β] {f : α → ι} {g : β → ι}
  (z : (i : ι) → Matrix (↑(g ⁻¹' {i})) (↑(f ⁻¹' {i})) (CategoryTheory.End (s i))),
  o.matrixDecompositionAddEquiv.symm z =
    CategoryTheory.Limits.biproduct.matrix fun j k =>
      if h : f j = g k then CategoryTheory.CategoryStruct.comp (z (f j) ⟨k, ⋯⟩ ⟨j, ⋯⟩) (CategoryTheory.eqToHom ⋯) else 0
-- Std.Async.Signal
_private.Std.Async.Signal.0.Std.Async.Signal.Waiter.ofNative.sizeOf_spec : ∀ (native : Std.Internal.UV.Signal), sizeOf { native := native } = 1 + sizeOf native
-- Mathlib.Order.Hom.CompleteLattice
/-- The underlying function of a sSupHom.  -/
sSupHom.toFun : {α : Type u_8} → {β : Type u_9} → [inst : SupSet α] → [inst_1 : SupSet β] → sSupHom α β → α → β
-- Mathlib.CategoryTheory.Limits.Shapes.Biproducts
CategoryTheory.Limits.Bicone.instIsSplitEpiπ : ∀ {J : Type w} {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {F : J → C} (B : CategoryTheory.Limits.Bicone F) (j : J),
  CategoryTheory.IsSplitEpi (B.π j)
-- Mathlib.Order.Hom.Lex
/-- A relation is isomorphic to the lexicographic sum of elements not greater than `x` and elements
greater than `x`.  -/
RelIso.sumLexComplRight : {α : Type u_1} →
  (r : α → α → Prop) →
    (x : α) →
      [IsTrans α r] →
        [Std.Trichotomous r] → [DecidableRel r] → Sum.Lex (Subrel r fun x_1 => ¬r x x_1) (Subrel r (r x)) ≃r r
-- Mathlib.Analysis.InnerProductSpace.Projection.Reflection
/-- Reflection is involutive.  -/
Submodule.reflection_mul_reflection : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], K.reflection * K.reflection = 1
-- Mathlib.Data.Fintype.Sigma
Set.biUnion_finsetSigma_univ' : ∀ {ι : Type u_1} {α : Type u_2} {κ : ι → Type u_3} [inst : (i : ι) → Fintype (κ i)] (s : Finset ι)
  (f : (i : ι) → κ i → Set α), ⋃ i ∈ s, ⋃ j, f i j = ⋃ ij ∈ s.sigma fun x => Finset.univ, f ij.fst ij.snd
-- Mathlib.Topology.Algebra.Monoid
ContinuousMap.mulRight_mul : ∀ {X : Type u_6} [inst : Semigroup X] [inst_1 : TopologicalSpace X] [inst_2 : SeparatelyContinuousMul X] (x y : X),
  ContinuousMap.mulRight (x * y) = (ContinuousMap.mulRight y).comp (ContinuousMap.mulRight x)
-- Mathlib.NumberTheory.LSeries.Dirichlet
/-- The `LSeries` associated to the arithmetic function `ζ` converges at `s` if and only if
`re s > 1`.  -/
ArithmeticFunction.LSeriesSummable_zeta_iff : ∀ {s : ℂ}, LSeriesSummable (fun x => ↑(ArithmeticFunction.zeta x)) s ↔ 1 < s.re
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.map_surjective : ∀ {α : Type u_1} {β : Type u_2} {f : α → β}, Function.Surjective ⇑(FreeAddMonoid.map f) ↔ Function.Surjective f
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
OrderDual.instConditionallyCompleteLinearOrder : (α : Type u_5) → [ConditionallyCompleteLinearOrder α] → ConditionallyCompleteLinearOrder αᵒᵈ
-- Mathlib.Algebra.Group.Defs
_private.Mathlib.Algebra.Group.Defs.0.neg_eq_of_add : ∀ {G : Type u_1} [inst : AddGroup G] {a b : G}, a + b = 0 → -a = b
-- Mathlib.Algebra.Module.Presentation.Tautological
Module.Presentation.tautological.R.add.inj : ∀ {A : Type u} {M : Type v} {m₁ m₂ m₁_1 m₂_1 : M},
  Module.Presentation.tautological.R.add m₁ m₂ = Module.Presentation.tautological.R.add m₁_1 m₂_1 →
    m₁ = m₁_1 ∧ m₂ = m₂_1
-- Mathlib.Order.CompleteLattice.Basic
iSup_unique : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] [inst_1 : Unique ι] (f : ι → α), ⨆ i, f i = f default
-- Mathlib.Data.Multiset.Powerset
Multiset.powerset_mono : ∀ {α : Type u_1}, Monotone Multiset.powerset
-- Mathlib.Data.Finset.NatDivisors
/-- A variant of `Nat.divisors_mul` with a more structured RHS.  -/
Nat.Coprime.divisors_mul : ∀ {m n : ℕ} (hmn : m.Coprime n),
  (m * n).divisors = Finset.map { toFun := fun p => (↑p).1 * (↑p).2, inj' := ⋯ } (m.divisors ×ˢ n.divisors).attach
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.primitiveRootsPowEquiv_symm_apply_coe : ∀ {R : Type u_4} [inst : CommRing R] [inst_1 : IsDomain R] {a b n : ℕ} (h : a * b ≡ 1 [MOD n])
  (x : ↥(primitiveRoots n R)), ↑((IsPrimitiveRoot.primitiveRootsPowEquiv h).symm x) = ↑x ^ b
-- Mathlib.Algebra.Algebra.Pi
Pi.algebraMap_apply : ∀ (ι : Type u_1) {R : Type u_2} (A : ι → Type u_3) [inst : CommSemiring R] [inst_1 : (i : ι) → Semiring (A i)]
  [inst_2 : (i : ι) → Algebra R (A i)] (a : R) (i : ι), (algebraMap R ((i : ι) → A i)) a i = (algebraMap R (A i)) a
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.instZero : {ι : Type u_1} → {M : ι → Type u_5} → [(i : ι) → Zero (M i)] → Zero ((i : ι) → M i)