mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.Transvection.Basic
LinearEquiv.transvection_mem_transvections : ∀ {R : Type u_1} {V : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup V] [inst_2 : Module R V] {f : Module.Dual R V}
  {v : V} {hfv : f v = 0}, LinearEquiv.transvection hfv ∈ LinearEquiv.transvections R V
-- Mathlib.Algebra.Homology.ShortComplex.Basic
CategoryTheory.ShortComplex.map_f : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] (S : CategoryTheory.ShortComplex C)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms], (S.map F).f = F.map S.f
-- Mathlib.Algebra.Group.Idempotent
IsIdempotentElem.mul_self_mul : ∀ {M : Type u_4} [inst : Semigroup M] {x : M}, IsIdempotentElem x → ∀ (y : M), x * (x * y) = x * y
-- Batteries.Data.String.Lemmas
String.Legacy.Iterator.ValidFor.valid : ∀ {l r : List Char} {it : String.Legacy.Iterator}, String.Legacy.Iterator.ValidFor l r it → it.Valid
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.nsmul_mem_nsmul : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddMonoid α] {s : Finset α} {a : α} {n : ℕ}, a ∈ s → n • a ∈ n • s
-- Mathlib.LinearAlgebra.Semisimple
Module.End.IsSemisimple.sub_of_commute : ∀ {M : Type u_2} [inst : AddCommGroup M] {K : Type u_3} [inst_1 : Field K] [inst_2 : Module K M] {f g : Module.End K M}
  [FiniteDimensional K M] [PerfectField K], Commute f g → f.IsSemisimple → g.IsSemisimple → (f - g).IsSemisimple
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.opNNNorm_lsmul_apply_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {R : Type u_3} [inst_3 : SeminormedRing R] [inst_4 : NormedAlgebra 𝕜 R]
  [inst_5 : Module R E] [inst_6 : IsBoundedSMul R E] [inst_7 : IsScalarTower 𝕜 R E] (x : R),
  ‖(ContinuousLinearMap.lsmul 𝕜 R) x‖₊ ≤ ‖x‖₊
-- Mathlib.LinearAlgebra.Matrix.Vec
Matrix.vec_zero : ∀ {m : Type u_3} {n : Type u_2} {R : Type u_1} [inst : Zero R], Matrix.vec 0 = 0
-- Mathlib.Algebra.Polynomial.Smeval
Polynomial.smeval_one : ∀ (R : Type u_1) [inst : Semiring R] {S : Type u_2} [inst_1 : AddCommMonoid S] [inst_2 : Pow S ℕ]
  [inst_3 : MulActionWithZero R S] (x : S), Polynomial.smeval 1 x = 1 • x ^ 0
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
/-- The canonical map `Γ(X, Uₓ) ⊗[Γ(S, Uₛ)] Γ(T, Uₜ) ⟶ Γ(X ×ₛ T, pr₁ ⁻¹ Uₓ ∩ pr₂ ⁻¹ Uₜ)`.
This is an isomorphism under various circumstances.  -/
AlgebraicGeometry.pushoutSection : {X Y S T : AlgebraicGeometry.Scheme} →
  {f : T ⟶ S} →
    {g : Y ⟶ X} →
      {iX : X ⟶ S} →
        {iY : Y ⟶ T} →
          CategoryTheory.IsPullback g iY iX f →
            {US : S.Opens} →
              {UT : T.Opens} →
                {UX : X.Opens} →
                  (hUST : UT ≤ (TopologicalSpace.Opens.map f.base).obj US) →
                    (hUSX : UX ≤ (TopologicalSpace.Opens.map iX.base).obj US) →
                      {UY : Y.Opens} →
                        UY = (TopologicalSpace.Opens.map g.base).obj UX ⊓ (TopologicalSpace.Opens.map iY.base).obj UT →
                          (CategoryTheory.Limits.pushout (AlgebraicGeometry.Scheme.Hom.appLE iX US UX hUSX)
                              (AlgebraicGeometry.Scheme.Hom.appLE f US UT hUST) ⟶
                            Y.presheaf.obj (Opposite.op UY))
-- Init.Data.Vector.Basic
Vector.mk.sizeOf_spec : ∀ {α : Type u} {n : ℕ} [inst : SizeOf α] (toArray : Array α) (size_toArray : toArray.size = n),
  sizeOf (Vector.mk toArray size_toArray) = 1 + sizeOf toArray + sizeOf size_toArray
-- Mathlib.Algebra.MvPolynomial.NoZeroDivisors
MvPolynomial.totalDegree_mul_of_isDomain : ∀ {R : Type u_1} {σ : Type u_2} [inst : CommSemiring R] [NoZeroDivisors R] {f g : MvPolynomial σ R},
  f ≠ 0 → g ≠ 0 → (f * g).totalDegree = f.totalDegree + g.totalDegree
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.shiftShortComplexFunctorIso_inv_app_τ₃ : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] (n i i' : ℤ)
  (hi : n + i = i') (X : CochainComplex C ℤ),
  ((CochainComplex.shiftShortComplexFunctorIso C n i i' hi).inv.app X).τ₃ =
    (n.negOnePow •
        (CochainComplex.shiftEval C n ((ComplexShape.up ℤ).next i) ((ComplexShape.up ℤ).next i') ⋯).app X).inv
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
MultilinearMap.domDomCongrLinearEquiv'.eq_1 : ∀ (R : Type uR) (S : Type uS) {ι : Type uι} (M₁ : ι → Type v₁) (M₂ : Type v₂) [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₂] [inst_7 : SMulCommClass R S M₂] {ι' : Type u_1}
  (σ : ι ≃ ι'),
  MultilinearMap.domDomCongrLinearEquiv' R S M₁ M₂ σ =
    { toFun := fun f => { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ).symm, map_update_add' := ⋯, map_update_smul' := ⋯ },
      map_add' := ⋯, map_smul' := ⋯,
      invFun := fun f => { toFun := ⇑f ∘ ⇑(Equiv.piCongrLeft' M₁ σ), map_update_add' := ⋯, map_update_smul' := ⋯ },
      left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.Order.BooleanAlgebra.Basic
BooleanAlgebra.toBiheytingAlgebra : {α : Type u} → [BooleanAlgebra α] → BiheytingAlgebra α
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.maxKeyD_eq_getLastD_keys : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {fallback : α}, t.maxKeyD fallback = t.keys.getLastD fallback
-- Mathlib.Data.Finset.Sups
Finset.card_compls : ∀ {α : Type u_2} [inst : BooleanAlgebra α] (s : Finset α), s.compls.card = s.card
-- Mathlib.MeasureTheory.Function.ConvergenceInDistribution
MeasureTheory.TendstoInDistribution.congr_simp : ∀ {ι : Type u_1} {E : Type u_2} {Ω' : Type u_3} {Ω : ι → Type u_5} {m : (i : ι) → MeasurableSpace (Ω i)}
  {m' : MeasurableSpace Ω'} {mE : MeasurableSpace E} [inst : TopologicalSpace E] [inst_1 : OpensMeasurableSpace E]
  (X X_1 : (i : ι) → Ω i → E),
  X = X_1 →
    ∀ (l l_1 : Filter ι),
      l = l_1 →
        ∀ (Z Z_1 : Ω' → E),
          Z = Z_1 →
            ∀ (μ μ_1 : (i : ι) → MeasureTheory.Measure (Ω i)) (e_μ : μ = μ_1)
              [inst_2 : ∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)] (μ' μ'_1 : MeasureTheory.Measure Ω')
              (e_μ' : μ' = μ'_1) [inst_3 : MeasureTheory.IsProbabilityMeasure μ'],
              MeasureTheory.TendstoInDistribution X l Z μ μ' = MeasureTheory.TendstoInDistribution X_1 l_1 Z_1 μ_1 μ'_1
-- Mathlib.Data.W.Basic
WType.toSigma_ofSigma : ∀ {α : Type u_1} {β : α → Type u_2} (s : (a : α) × (β a → WType β)), (WType.ofSigma s).toSigma = s
-- Mathlib.Analysis.Complex.Asymptotics
Complex.isBigO_im_sub_im : ∀ {z : ℂ}, (fun w => w.im - z.im) =O[nhds z] fun w => w - z
-- Mathlib.Topology.Algebra.Constructions.DomMulAct
DomAddAct.map_mk_symm_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : Mᵈᵃᵃ),
  Filter.map (⇑DomAddAct.mk.symm) (nhds x) = nhds (DomAddAct.mk.symm x)
-- Lean.Data.Lsp.Extra
Lean.Lsp.RpcCallParams.mk : Lean.Lsp.TextDocumentPositionParams → UInt64 → Lean.Name → Lean.Json → Lean.Lsp.RpcCallParams
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
WithZero.exists_ne_zero_and_lt : ∀ {α : Type u_1} [inst : Preorder α] {x : WithZero α} [NoMinOrder α], x ≠ 0 → ∃ y, y ≠ 0 ∧ y < x
-- Lean.Message
Lean.AddMessageContext : (Type → Type) → Type
-- Mathlib.Data.FunLike.Basic
DFunLike.ne_iff : ∀ {F : Sort u_1} {α : Sort u_2} {β : α → Sort u_3} [i : DFunLike F α β] {f g : F}, f ≠ g ↔ ∃ a, f a ≠ g a
-- Init.Data.Nat.Mod
Nat.mod_mul : ∀ {a b x : ℕ}, x % (a * b) = x % a + a * (x / a % b)
-- Mathlib.Order.Category.BddLat
bddLat_dual_comp_forget_to_semilatSupCat : BddLat.dual.comp (CategoryTheory.forget₂ BddLat SemilatSupCat) =
  (CategoryTheory.forget₂ BddLat SemilatInfCat).comp SemilatInfCat.dual
-- Mathlib.Topology.Algebra.UniformConvergence
instAddGroupUniformOnFun : {α : Type u_1} → {β : Type u_2} → {𝔖 : Set (Set α)} → [AddGroup β] → AddGroup (UniformOnFun α β 𝔖)
-- Mathlib.Probability.Independence.Conditional
ProbabilityTheory.iCondIndepSet.condIndep_generateFrom_of_disjoint : ∀ {Ω : Type u_1} {ι : Type u_2} {m' mΩ : MeasurableSpace Ω} [inst : StandardBorelSpace Ω] {hm' : m' ≤ mΩ}
  {μ : MeasureTheory.Measure Ω} [inst_1 : MeasureTheory.IsFiniteMeasure μ] {s : ι → Set Ω},
  (∀ (n : ι), MeasurableSet (s n)) →
    ProbabilityTheory.iCondIndepSet m' hm' s μ →
      ∀ (S T : Set ι),
        Disjoint S T →
          ProbabilityTheory.CondIndep m' (MeasurableSpace.generateFrom {t | ∃ n ∈ S, s n = t})
            (MeasurableSpace.generateFrom {t | ∃ k ∈ T, s k = t}) hm' μ
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.tendsto_densityProcess_limitProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] {κ : ProbabilityTheory.Kernel α (γ × β)}
  {ν : ProbabilityTheory.Kernel α γ},
  κ.fst ≤ ν →
    ∀ [ProbabilityTheory.IsFiniteKernel ν] (a : α) {s : Set β},
      MeasurableSet s →
        ∀ᵐ (x : γ) ∂ν a,
          Filter.Tendsto (fun n => κ.densityProcess ν n a x s) Filter.atTop
            (nhds
              (MeasureTheory.Filtration.limitProcess (fun n x => κ.densityProcess ν n a x s)
                (ProbabilityTheory.countableFiltration γ) (ν a) x))
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_vecMul : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : NonUnitalSemiring α] [inst_1 : Fintype n]
  [inst_2 : Fintype m] (v : m → α) (M : Matrix m n α) (N : Matrix n o α),
  Matrix.vecMul (Matrix.vecMul v M) N = Matrix.vecMul v (M * N)
-- Mathlib.Computability.TuringMachine.ToPartrec
_private.Mathlib.Computability.TuringMachine.ToPartrec.0.Turing.PartrecToTM2.trNormal.match_1.eq_1 : ∀ (motive : Turing.ToPartrec.Code → Turing.PartrecToTM2.Cont' → Sort u_1) (k : Turing.PartrecToTM2.Cont')
  (h_1 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.zero' k)
  (h_2 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.succ k)
  (h_3 : (k : Turing.PartrecToTM2.Cont') → motive Turing.ToPartrec.Code.tail k)
  (h_4 : (f fs : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.cons fs) k)
  (h_5 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.comp g) k)
  (h_6 : (f g : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive (f.case g) k)
  (h_7 : (f : Turing.ToPartrec.Code) → (k : Turing.PartrecToTM2.Cont') → motive f.fix k),
  (match Turing.ToPartrec.Code.zero', k with
    | Turing.ToPartrec.Code.zero', k => h_1 k
    | Turing.ToPartrec.Code.succ, k => h_2 k
    | Turing.ToPartrec.Code.tail, k => h_3 k
    | f.cons fs, k => h_4 f fs k
    | f.comp g, k => h_5 f g k
    | f.case g, k => h_6 f g k
    | f.fix, k => h_7 f k) =
    h_1 k
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.coeOrderEmbedding_apply : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] (a : TwoSidedIdeal R), TwoSidedIdeal.coeOrderEmbedding a = ↑a
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.findM?.match_1.eq_1 : ∀ {α : Type} (motive : List α → Sort u_1) (h_1 : Unit → motive []) (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match [] with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_1 ()
-- Mathlib.Topology.Algebra.Ring.Basic
/-- A ring topology on a ring `R` is a topology for which addition, negation and multiplication
are continuous.  -/
RingTopology : (R : Type u) → [Ring R] → Type u
-- Mathlib.Analysis.Normed.Operator.Fredholm.Basic
ContinuousLinearMap.FredholmPackage.range_eq : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : AddCommGroup F] [inst_3 : Module 𝕜 E] [inst_4 : Module 𝕜 F] [inst_5 : TopologicalSpace E]
  [inst_6 : TopologicalSpace F] {u : E →L[𝕜] F} (pkg : u.FredholmPackage), (↑u).range = pkg.decCodom.X₁
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.not_divides_sq : ∀ {d : ℕ} [dnsq : Zsqrtd.Nonsquare d] (x y : ℕ), (x + 1) * (x + 1) ≠ d * (y + 1) * (y + 1)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.δ_liftCochain : ∀ {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 ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain M K n) (β : CochainComplex.HomComplex.Cochain M L m) (h : m + 1 = n)
  (n' : ℤ) (hn' : n + 1 = n'),
  CochainComplex.HomComplex.δ n n' (CochainComplex.mappingCocone.liftCochain φ α β h) =
    (CochainComplex.HomComplex.δ n n' α).comp (CochainComplex.mappingCocone.inl φ) ⋯ -
      (CochainComplex.HomComplex.δ m n β + α.comp (CochainComplex.HomComplex.Cochain.ofHom φ) ⋯).comp
        (↑(CochainComplex.mappingCocone.inr φ)) hn'
-- Mathlib.Order.CompleteLattice.Defs
sSup_le : ∀ {α : Type u_1} [inst : CompleteSemilatticeSup α] {s : Set α} {a : α}, (∀ b ∈ s, b ≤ a) → sSup s ≤ a
-- Mathlib.Topology.LocallyFinsupp
/-- This allows writing `D.support` instead of `Function.support D`  -/
Function.locallyFinsuppWithin.support : {X : Type u_1} →
  [inst : TopologicalSpace X] →
    {U : Set X} → {Y : Type u_2} → [inst_1 : Zero Y] → Function.locallyFinsuppWithin U Y → Set X
-- Mathlib.Order.Notation
/-- The bot (`⊥`, `\bot`) element 

Conventions for notations in identifiers:

 * The recommended spelling of `⊥` in identifiers is `bot`. -/
«term⊥» : Lean.ParserDescr
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- The **lower Lebesgue integral** of a function `f` with respect to a measure `μ`.  -/
MeasureTheory.«term∫⁻_In_,_∂_» : Lean.ParserDescr
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.target : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) (t : ↑unitInterval),
  F (t, 1) = x₁
-- Mathlib.NumberTheory.RamificationInertia.Ramification
Ideal.ramificationIdx'_spec : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S] {p : Ideal R} {P : Ideal S}
  {n : ℕ}, Ideal.map (algebraMap R S) p ≤ P ^ n → ¬Ideal.map (algebraMap R S) p ≤ P ^ (n + 1) → p.ramificationIdx' P = n
-- Mathlib.Topology.LocallyConstant.Algebra
LocallyConstant.instMul : {X : Type u_1} → {Y : Type u_2} → [inst : TopologicalSpace X] → [Mul Y] → Mul (LocallyConstant X Y)
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi_def : ∀ {ι : Type u_4} {α : ι → Type u_5} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)),
  MeasureTheory.Measure.pi μ = (MeasureTheory.OuterMeasure.pi fun i => (μ i).toOuterMeasure).toMeasure ⋯
-- Mathlib.RingTheory.GradedAlgebra.AlgHom
GradedAlgHom.coe_toAlgHom_injective : ∀ {R : Type u_1} {A : Type u_6} {B : Type u_7} {ι : Type u_10} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Semiring B] [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : DecidableEq ι] [inst_6 : AddMonoid ι]
  {𝒜 : ι → Submodule R A} {ℬ : ι → Submodule R B} [inst_7 : GradedAlgebra 𝒜] [inst_8 : GradedAlgebra ℬ],
  Function.Injective GradedAlgHom.toAlgHom
-- Mathlib.CategoryTheory.Yoneda
CategoryTheory.Functor.CorepresentableBy.id_homEquiv_apply : ∀ (X : Type v) (a : PUnit.{v + 1} ⟶ X),
  CategoryTheory.Functor.CorepresentableBy.id.homEquiv a = (CategoryTheory.ConcreteCategory.hom a) PUnit.unit
-- Mathlib.AlgebraicGeometry.Properties
AlgebraicGeometry.instIsIntegralSpecOfIsDomainCarrier : ∀ {R : CommRingCat} [IsDomain ↑R], AlgebraicGeometry.IsIntegral (AlgebraicGeometry.Spec R)
-- Mathlib.CategoryTheory.Limits.Final
/-- When `F : C ⥤ D` is final, we denote by `homToLift` an arbitrary choice of morphism
`d ⟶ F.obj (lift F d)`.
 -/
CategoryTheory.Functor.Final.homToLift : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (F : CategoryTheory.Functor C D) →
          [inst_2 : F.Final] → (d : D) → d ⟶ F.obj (CategoryTheory.Functor.Final.lift F d)
-- Mathlib.CategoryTheory.GradedObject
CategoryTheory.GradedObject.CofanMapObjFun.ιMapObj_iso_inv : ∀ {I : Type u_1} {J : Type u_2} {C : Type u_4} [inst : CategoryTheory.Category.{v_1, u_4} C]
  {X : CategoryTheory.GradedObject I C} {p : I → J} {j : J} [inst_1 : X.HasMap p] {c : X.CofanMapObjFun p j}
  (hc : CategoryTheory.Limits.IsColimit c) (i : I) (hi : p i = j),
  CategoryTheory.CategoryStruct.comp (X.ιMapObj p i j hi) (CategoryTheory.GradedObject.CofanMapObjFun.iso hc).inv =
    CategoryTheory.Limits.Cofan.inj c ⟨i, hi⟩
-- Mathlib.RingTheory.WittVector.FrobeniusFractionField
/-- The root of this polynomial determines the `n+1`st coefficient of our solution.  -/
WittVector.RecursionMain.succNthDefiningPoly : (p : ℕ) →
  [hp : Fact (Nat.Prime p)] →
    {k : Type u_1} →
      [inst : CommRing k] → [CharP k p] → (n : ℕ) → WittVector p k → WittVector p k → (Fin (n + 1) → k) → Polynomial k
-- Mathlib.Topology.Algebra.Module.Spaces.ContinuousLinearMap
/-- Post-composition by a *fixed* continuous linear map as a continuous linear map.

Note that in non-normed space it is not always true that composition is continuous
in both variables, so we have to fix one of them.  -/
ContinuousLinearMap.postcomp : {𝕜₁ : Type u_1} →
  {𝕜₂ : Type u_2} →
    {𝕜₃ : Type u_3} →
      [inst : NormedField 𝕜₁] →
        [inst_1 : NormedField 𝕜₂] →
          [inst_2 : NormedField 𝕜₃] →
            {σ : 𝕜₁ →+* 𝕜₂} →
              {τ : 𝕜₂ →+* 𝕜₃} →
                {ρ : 𝕜₁ →+* 𝕜₃} →
                  [RingHomCompTriple σ τ ρ] →
                    (E : Type u_4) →
                      {F : Type u_5} →
                        {G : Type u_6} →
                          [inst_4 : AddCommGroup E] →
                            [inst_5 : Module 𝕜₁ E] →
                              [inst_6 : AddCommGroup F] →
                                [inst_7 : Module 𝕜₂ F] →
                                  [inst_8 : AddCommGroup G] →
                                    [inst_9 : Module 𝕜₃ G] →
                                      [inst_10 : TopologicalSpace E] →
                                        [inst_11 : TopologicalSpace F] →
                                          [inst_12 : TopologicalSpace G] →
                                            [inst_13 : IsTopologicalAddGroup F] →
                                              [inst_14 : IsTopologicalAddGroup G] →
                                                [inst_15 : ContinuousConstSMul 𝕜₃ G] →
                                                  [inst_16 : ContinuousConstSMul 𝕜₂ F] →
                                                    (F →SL[τ] G) → (E →SL[σ] F) →SL[τ] E →SL[ρ] G
-- Init.Data.Rat.Lemmas
Rat.neg_sub : ∀ (a b : ℚ), -(a - b) = b - a
-- Mathlib.RingTheory.Valuation.Discrete.Basic
Valuation.IsUniformizer.ne_zero : ∀ {Γ : Type u_1} [inst : LinearOrderedCommGroupWithZero Γ] {A : Type u_2} [inst_1 : Ring A] {v : Valuation A Γ}
  [hv : v.IsRankOneDiscrete] {π : A}, v.IsUniformizer π → π ≠ 0
-- Init.Data.Array.Find
Array.find?_push_eq_some : ∀ {α : Type u_1} {a : α} {p : α → Bool} {b : α} {xs : Array α},
  Array.find? p (xs.push a) = some b ↔ Array.find? p xs = some b ∨ Array.find? p xs = none ∧ p a = true ∧ a = b
-- Mathlib.Combinatorics.SimpleGraph.Maps
SimpleGraph.Hom.subset_preimage_edgeSet : ∀ {V : Type u_1} {W : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph W} (f : G →g G'),
  G.edgeSet ⊆ Sym2.map ⇑f ⁻¹' G'.edgeSet
-- Mathlib.Topology.Algebra.Module.Basic
ContinuousSMul.of_nhds_zero : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : TopologicalSpace R] [inst_2 : TopologicalSpace M]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [IsTopologicalRing R] [IsTopologicalAddGroup M],
  Filter.Tendsto (fun p => p.1 • p.2) (nhds 0 ×ˢ nhds 0) (nhds 0) →
    (∀ (m : M), Filter.Tendsto (fun a => a • m) (nhds 0) (nhds 0)) →
      (∀ (a : R), Filter.Tendsto (fun m => a • m) (nhds 0) (nhds 0)) → ContinuousSMul R M
-- Mathlib.Topology.Order.Basic
OrderTopology.mk : ∀ {α : Type u_1} [t : TopologicalSpace α] [inst : Preorder α], t = Preorder.topology α → OrderTopology α
-- Mathlib.Data.Set.Prod
Set.mk_preimage_prod_left_fn_eq_if : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {s : Set α} {t : Set β} {b : β} [inst : DecidablePred fun x => x ∈ t]
  (f : γ → α), (fun a => (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.fst : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace β]
  [inst_1 : TopologicalSpace γ] {f : α → β × γ},
  MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => (f x).1
-- Std.Time.Internal.UnitVal
Std.Time.Internal.instTransOrdUnitVal : ∀ {x : ℚ}, Std.TransOrd (Std.Time.Internal.UnitVal x)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.mono_lift_of_mono_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W X Y : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct X Y] (f : W ⟶ X) (g : W ⟶ Y) [CategoryTheory.Mono f],
  CategoryTheory.Mono (CategoryTheory.Limits.prod.lift f g)
-- Mathlib.Algebra.Polynomial.Lifts
/-- We define the subsemiring of polynomials that lifts as the image of `RingHom.of (map f)`.  -/
Polynomial.lifts : {R : Type u} → [inst : Semiring R] → {S : Type v} → [inst_1 : Semiring S] → (R →+* S) → Subsemiring (Polynomial S)
-- Std.Data.DTreeMap.Raw.Basic
/-- Returns the key-value pair with the `n`-th smallest key, or panics if `n` is at least `t.size`.  -/
Std.DTreeMap.Raw.entryAtIdx! : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} → [Inhabited ((a : α) × β a)] → Std.DTreeMap.Raw α β cmp → ℕ → (a : α) × β a
-- Mathlib.Topology.UniformSpace.Defs
nhds_eq_comap_uniformity' : ∀ {α : Type ua} [inst : UniformSpace α] {x : α}, nhds x = Filter.comap (fun y => (y, x)) (uniformity α)
-- Mathlib.Algebra.Ring.Equiv
/-- `Equiv.cast (congrArg _ h)` as a ring equiv.

Note that unlike `Equiv.cast`, this takes an equality of indices rather than an equality of types,
to avoid having to deal with an equality of the algebraic structure itself.  -/
RingEquiv.cast : {ι : Type u_7} →
  {R : ι → Type u_8} → [inst : (i : ι) → Mul (R i)] → [inst_1 : (i : ι) → Add (R i)] → {i j : ι} → i = j → R i ≃+* R j
-- Mathlib.CategoryTheory.Functor.Const
CategoryTheory.Functor.const.opObjOp_inv_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} C]
  (X : C) (x : Jᵒᵖ),
  (CategoryTheory.Functor.const.opObjOp X).inv.app x =
    CategoryTheory.CategoryStruct.id (((CategoryTheory.Functor.const J).obj X).op.obj x)