mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_insertEntry : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : PartialEquivBEq α] {l : List ((_ : α) × β)} {k a : α} {v : β}
  {h : Std.Internal.List.containsKey a (Std.Internal.List.insertEntry k v l) = true},
  Std.Internal.List.getValue a (Std.Internal.List.insertEntry k v l) h =
    if h' : (k == a) = true then v else Std.Internal.List.getValue a l ⋯
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_lt_rpow : ∀ {x y z : ℝ}, 0 ≤ x → x < y → 0 < z → x ^ z < y ^ z
-- Mathlib.Data.Real.Basic
Real.ringEquivCauchy_apply : ∀ (self : ℝ), Real.ringEquivCauchy self = self.cauchy
-- Std.Data.ExtDTreeMap.Basic
Std.ExtDTreeMap.instReflBEq : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.LawfulEqCmp cmp] [inst_1 : Std.TransCmp cmp]
  [inst_2 : (k : α) → BEq (β k)] [∀ (k : α), ReflBEq (β k)], ReflBEq (Std.ExtDTreeMap α β cmp)
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- The relative perfect closure of `F` in `E` is algebraic over `F`.  -/
perfectClosure.isAlgebraic : ∀ (F : Type u) (E : Type v) [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E],
  Algebra.IsAlgebraic F ↥(perfectClosure F E)
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.ofFun_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : Zero β], UniformFun.ofFun 0 = 0
-- Mathlib.Algebra.Order.Ring.Synonym
OrderDual.instNatCast : {R : Type u_1} → [NatCast R] → NatCast Rᵒᵈ
-- Mathlib.Order.Filter.Prod
Filter.prod_eq : ∀ {α : Type u_1} {β : Type u_2} {f : Filter α} {g : Filter β}, f ×ˢ g = (Filter.map Prod.mk f).seq g
-- Mathlib.CategoryTheory.Bicategory.Opposites
Bicategory.Opposite.op2_associator_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d),
  Bicategory.Opposite.op2 (CategoryTheory.Bicategory.associator f g h).inv =
    (CategoryTheory.Bicategory.associator h.op g.op f.op).symm.inv
-- Lean.Meta.Tactic.Grind.Parser
Lean.Parser.Command.initGrindNorm.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.CategoryTheory.Monad.Basic
CategoryTheory.ComonadHom.mk.sizeOf_spec : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M N : CategoryTheory.Comonad C} [inst_1 : SizeOf C]
  (toNatTrans : CategoryTheory.NatTrans M.toFunctor N.toFunctor)
  (app_ε :
    autoParam (∀ (X : C), CategoryTheory.CategoryStruct.comp (toNatTrans.app X) (N.ε.app X) = M.ε.app X)
      CategoryTheory.ComonadHom.app_ε._autoParam)
  (app_δ :
    autoParam
      (∀ (X : C),
        CategoryTheory.CategoryStruct.comp (toNatTrans.app X) (N.δ.app X) =
          CategoryTheory.CategoryStruct.comp (M.δ.app X)
            (CategoryTheory.CategoryStruct.comp (toNatTrans.app (M.obj X)) (N.map (toNatTrans.app X))))
      CategoryTheory.ComonadHom.app_δ._autoParam),
  sizeOf { toNatTrans := toNatTrans, app_ε := app_ε, app_δ := app_δ } = 1 + sizeOf toNatTrans
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.sInter_mul_subset : ∀ {α : Type u_2} [inst : Mul α] (S : Set (Set α)) (t : Set α), ⋂₀ S * t ⊆ ⋂ s ∈ S, s * t
-- Init.Data.Range.Polymorphic.Fin
Fin.instLeast?OfNatNat : Std.PRange.Least? (Fin 0)
-- Mathlib.Data.Finsupp.MonomialOrder
MonomialOrder.lex_lt_iff : ∀ {σ : Type u_1} [inst : LinearOrder σ] [inst_1 : WellFoundedGT σ] {c d : σ →₀ ℕ},
  MonomialOrder.lex.toSyn c < MonomialOrder.lex.toSyn d ↔ toLex c < toLex d
-- Mathlib.CategoryTheory.Bicategory.Modification.Lax
CategoryTheory.Lax.LaxTrans.Hom.of : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.LaxFunctor B C} →
          {η θ : F ⟶ G} → CategoryTheory.Lax.LaxTrans.Modification η θ → CategoryTheory.Lax.LaxTrans.Hom η θ
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Closeds.noncompactSpace_iff : ∀ {α : Type u_1} [inst : UniformSpace α], NoncompactSpace (TopologicalSpace.Closeds α) ↔ NoncompactSpace α
-- Mathlib.LinearAlgebra.TensorProduct.Graded.External
TensorProduct.instModuleFstSnd : {R : Type u_1} →
  {ι : Type u_2} →
    (𝒜 : ι → Type u_3) →
      (ℬ : ι → Type u_4) →
        [inst : CommRing R] →
          [inst_1 : (i : ι) → AddCommGroup (𝒜 i)] →
            [inst_2 : (i : ι) → AddCommGroup (ℬ i)] →
              [inst_3 : (i : ι) → Module R (𝒜 i)] →
                [inst_4 : (i : ι) → Module R (ℬ i)] → (i : ι × ι) → Module R (TensorProduct R (𝒜 i.1) (ℬ i.2))
-- Mathlib.Computability.Encoding
Computability.inhabitedEncoding : Inhabited (Computability.Encoding Bool Bool)
-- Lean.Elab.Command.Scope
/-- The current state of all set options at this point in the scope. Note that this is the
full current set of options and does *not* simply contain the options set
while this scope has been active.
 -/
Lean.Elab.Command.Scope.opts : Lean.Elab.Command.Scope → Lean.Options
-- Mathlib.Data.Finset.SDiff
Finset.sdiff_idem : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s \ t) \ t = s \ t
-- Mathlib.Data.Matrix.Mul
/-- For any vector `a` in a nontrivial commutative ring with nontrivial index,
there exists a non-zero vector `b` such that `b ⬝ᵥ a = 0`. In other words,
there exists a non-zero orthogonal vector.  -/
exists_ne_zero_dotProduct_eq_zero : ∀ {m : Type u_2} {α : Type v} [inst : Fintype m] [inst_1 : CommRing α] [Nontrivial m] [Nontrivial α] (a : m → α),
  ∃ b, b ≠ 0 ∧ b ⬝ᵥ a = 0
-- Mathlib.Topology.Algebra.Group.Basic
nhds_mul : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [IsTopologicalGroup G] (x y : G),
  nhds (x * y) = nhds x * nhds y
-- Mathlib.MeasureTheory.Function.LpSeminorm.Basic
MeasureTheory.eLpNorm_measure_zero : ∀ {α : Type u_1} {ε : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} [inst : ENorm ε] {f : α → ε},
  MeasureTheory.eLpNorm f p 0 = 0
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.minKey?_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : β k → β k}, (t.modify k f).minKey? = t.minKey?
-- Mathlib.Computability.TuringMachine.Computable
/-- index type of stacks  -/
Turing.FinTM2.K : Turing.FinTM2 → Type
-- Mathlib.Algebra.Homology.ExactSequenceFour
CategoryTheory.ComposableArrows.Exact.opcyclesIsoCycles.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_2, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Balanced C] {n : ℕ} {S : CategoryTheory.ComposableArrows C (n + 3)} (hS : S.Exact) (k : ℕ)
  (hk : k ≤ n) [h₁ : (hS.sc k ⋯).HasRightHomology] [h₂ : (hS.sc (k + 1) ⋯).HasLeftHomology],
  hS.opcyclesIsoCycles k hk = hS.opcyclesIsoCycles k hk
-- Mathlib.Data.Num.Lemmas
Num.cast_inj : ∀ {α : Type u_1} [inst : Semiring α] [inst_1 : PartialOrder α] [IsStrictOrderedRing α] {m n : Num}, ↑m = ↑n ↔ m = n
-- Mathlib.Order.ScottContinuity
/-- Eta-expanded form of `ScottContinuousOn.image_comp` -/
ScottContinuousOn.fun_image_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ]
  {D : Set (Set α)} {f : α → β} {g : β → γ},
  (∀ (a b : α), a ≤ b → {a, b} ∈ D) →
    ScottContinuousOn ((fun x => f '' x) '' D) g → ScottContinuousOn D f → ScottContinuousOn D fun x => g (f x)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The proposition that the function commutes with the actions.  -/
LinearMap.map_smul' : ∀ {R : Type u_14} {S : Type u_15} [inst : Semiring R] [inst_1 : Semiring S] {σ : R →+* S} {M : Type u_16}
  {M₂ : Type u_17} [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module S M₂]
  (self : M →ₛₗ[σ] M₂) (m : R) (x : M), self.toFun (m • x) = σ m • self.toFun x
-- Mathlib.GroupTheory.Perm.Fin
Fin.succAbove_cycleRange : ∀ {n : ℕ} (i j : Fin n), i.succ.succAbove (i.cycleRange j) = (Equiv.swap 0 i.succ) j.succ
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.StrongTrans.whiskerLeft_naturality_id_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {G H : CategoryTheory.OplaxFunctor B C} (θ : CategoryTheory.Oplax.StrongTrans G H) {a : B} {a' : C} (f : a' ⟶ G.obj a)
  {Z : a' ⟶ H.obj a}
  (h :
    CategoryTheory.CategoryStruct.comp f
        (CategoryTheory.CategoryStruct.comp (θ.app a) (CategoryTheory.CategoryStruct.id (H.obj a))) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (θ.naturality (CategoryTheory.CategoryStruct.id a)).hom)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerLeft (θ.app a) (H.mapId a))) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.whiskerRight (G.mapId a) (θ.app a)))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.leftUnitor (θ.app a)).hom)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.rightUnitor (θ.app a)).inv) h))
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.tendsto_sub_atTop_nat : ∀ (k : ℕ), Filter.Tendsto (fun a => a - k) Filter.atTop Filter.atTop
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.StronglyMeasurable.pow : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Monoid β]
  [ContinuousMul β], MeasureTheory.StronglyMeasurable f → ∀ (n : ℕ), MeasureTheory.StronglyMeasurable (f ^ n)
-- Std.Data.HashMap.Lemmas
Std.HashMap.size_alter_eq_self_of_not_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {k : α}
  {f : Option β → Option β}, k ∉ m → (f m[k]?).isNone = true → (m.alter k f).size = m.size
-- Mathlib.Topology.ContinuousMap.StoneWeierstrass
ContinuousMap.elemental_id_eq_top : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] (s : Set 𝕜) [inst_1 : CompactSpace ↑s],
  StarAlgebra.elemental 𝕜 (ContinuousMap.restrict s (ContinuousMap.id 𝕜)) = ⊤
-- Init.Data.Range.Polymorphic.UInt
UInt16.instLawfulHasSize_2 : Std.Rxi.LawfulHasSize UInt16
-- Init.PropLemmas
exists_eq : ∀ {α : Sort u_1} {a' : α}, ∃ a, a = a'
-- Std.Internal.UV.TCP
/-- Binds a TCP socket to a specific address.
 -/
Std.Internal.UV.TCP.Socket.bind : Std.Internal.UV.TCP.Socket → Std.Net.SocketAddress → IO Unit
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.add.match_1.splitter : (motive : ONote → ONote → Sort u_1) →
  (x x_1 : ONote) →
    ((o : ONote) → motive ONote.zero o) →
      ((e : ONote) → (n : ℕ+) → (a o : ONote) → motive (e.oadd n a) o) → motive x x_1
-- Mathlib.Topology.Category.TopCat.Opens
/-- The FrameHom sending an open in `Y` to its preimage in `X`  -/
TopCat.Hom.frameHom : {X Y : TopCat} → (X ⟶ Y) → FrameHom (TopologicalSpace.Opens ↑Y) (TopologicalSpace.Opens ↑X)
-- Mathlib.RingTheory.IntegralClosure.IsIntegralClosure.Basic
IsIntegral.multiset_prod : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {s : Multiset A},
  (∀ x ∈ s, IsIntegral R x) → IsIntegral R s.prod
-- Mathlib.Topology.MetricSpace.Pseudo.Basic
/-- A compact set is separable.  -/
IsCompact.isSeparable : ∀ {α : Type u_2} [inst : TopologicalSpace α] [TopologicalSpace.PseudoMetrizableSpace α] {s : Set α},
  IsCompact s → TopologicalSpace.IsSeparable s
-- Mathlib.Analysis.Fourier.FourierTransformDeriv
/-- Variant of `hasFTaylorSeriesUpTo_fourierIntegral` in which the smoothness index is restricted
to `ℕ∞` (and so are the inequalities in the assumption `hf`). Avoids normcasting in some
applications.  -/
VectorFourier.hasFTaylorSeriesUpTo_fourierIntegral' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {V : Type u_2} {W : Type u_3}
  [inst_2 : NormedAddCommGroup V] [inst_3 : NormedSpace ℝ V] [inst_4 : NormedAddCommGroup W] [inst_5 : NormedSpace ℝ W]
  (L : V →L[ℝ] W →L[ℝ] ℝ) {f : V → E} [inst_6 : MeasurableSpace V] [BorelSpace V] {μ : MeasureTheory.Measure V}
  [SecondCountableTopology V] {N : ℕ∞},
  (∀ (n : ℕ), ↑n ≤ N → MeasureTheory.Integrable (fun v => ‖v‖ ^ n * ‖f v‖) μ) →
    MeasureTheory.AEStronglyMeasurable f μ →
      HasFTaylorSeriesUpTo (↑N)
        (VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L) f) fun w n =>
        VectorFourier.fourierIntegral Real.fourierChar μ (ContinuousLinearMap.toLinearMap₁₂ L)
          (fun v => VectorFourier.fourierPowSMulRight L f v n) w
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Cofan.mk_ι_app : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f : β → C} (P : C) (p : (b : β) → f b ⟶ P)
  (X : CategoryTheory.Discrete β), (CategoryTheory.Limits.Cofan.mk P p).ι.app X = p X.as
-- Mathlib.Tactic.DeriveEncodable
_private.Mathlib.Tactic.DeriveEncodable.0.Mathlib.Deriving.Encodable.mkFromSMatch : Lean.Elab.Deriving.Context → Lean.InductiveVal → Array Lean.Name → Lean.Elab.TermElabM Lean.Term
-- Mathlib.Topology.Inseparable
StableUnderSpecialization.preimage : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y} {s : Set Y},
  StableUnderSpecialization s → Continuous f → StableUnderSpecialization (f ⁻¹' s)
-- Init.Data.SInt.IntToBitVec
Int8.toBitVec32_toISize : ∀ (n : Int8) (h : System.Platform.numBits = 32), n.toISize.toBitVec32 h = BitVec.signExtend 32 n.toBitVec
-- Mathlib.Algebra.RingQuot
/-- The quotient map from an `S`-algebra to its quotient, as a homomorphism of `S`-algebras.
 -/
RingQuot.mkAlgHom : (S : Type u_1) →
  [inst : CommSemiring S] →
    {A : Type u_2} → [inst_1 : Semiring A] → [inst_2 : Algebra S A] → (s : A → A → Prop) → A →ₐ[S] RingQuot s
-- Lean.Elab.ConfigEval.MetaInstances
Lean.Elab.ConfigEval.instEvalTermEtaStructMode : Lean.Elab.ConfigEval.EvalTerm Lean.Meta.EtaStructMode
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqDiagnosticRelatedInformation.beq : Lean.Lsp.DiagnosticRelatedInformation → Lean.Lsp.DiagnosticRelatedInformation → Bool
-- Mathlib.Topology.UniformSpace.Pi
Pi.uniformSpace_comap_precomp : ∀ {ι : Type u_1} {ι' : Type u_2} {β : Type u_3} [inst : UniformSpace β] (φ : ι' → ι),
  UniformSpace.comap (fun x => x ∘ φ) (Pi.uniformSpace fun x => β) =
    ⨅ i', UniformSpace.comap (Function.eval (φ i')) inst
-- Init.Data.SInt.Lemmas
ISize.lt_of_le_of_lt : ∀ {a b c : ISize}, a ≤ b → b < c → a < c
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKey?_eq_some_iff_mem_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {km : α}, t.maxKey? = some km ↔ km ∈ t ∧ ∀ k ∈ t, (cmp k km).isLE = true
-- Mathlib.CategoryTheory.Limits.Shapes.Products
/-- Any isomorphism is the projection from a single object product.  -/
CategoryTheory.Limits.Cofan.isColimitMkOfUnique : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      (e : X ≅ Y) →
        (J : Type u_1) → [Unique J] → CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.Cofan.mk Y fun x => e.hom)
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- **Alias** of the forward direction of `Bornology.isVonNBounded_iff_tendsto_smallSets_nhds`. -/
Bornology.IsVonNBounded.tendsto_smallSets_nhds : ∀ {𝕜 : Type u_6} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {S : Set E},
  Bornology.IsVonNBounded 𝕜 S → Filter.Tendsto (fun x => x • S) (nhds 0) (nhds 0).smallSets
-- Mathlib.Algebra.Lie.Basis.Basic
_private.Mathlib.Algebra.Lie.Basis.Basic.0.LieAlgebra.Basis.cartan_borelLower_borelUpper_le : ∀ {ι : Type u_1} {R : Type u_2} {L : Type u_3} [inst : Finite ι] [inst_1 : CommRing R] [inst_2 : LieRing L]
  [inst_3 : LieAlgebra R L] {H : LieSubalgebra R L} (b : LieAlgebra.Basis ι H) [inst_4 : Fintype ι] [IsDomain R]
  [CharZero R],
  ![H.toLieSubmodule, b.borelLower, b.borelUpper] ≤
    ![LieAlgebra.rootSpace H 0, ⨆ n, ⨆ (_ : n ≠ 0), LieAlgebra.rootSpace H (∑ i, n i • ⇑((-b.baseSupp) i)),
      ⨆ n, ⨆ (_ : n ≠ 0), LieAlgebra.rootSpace H (∑ i, n i • ⇑(b.baseSupp i))]
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.eval_single : ∀ (b e x : Ordinal.{u_1}), (Ordinal.CNF.eval b fun₀ | e => x) = b ^ e * x
-- Mathlib.CategoryTheory.Functor.FunctorHom
CategoryTheory.Functor.HomObj.map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {F G : CategoryTheory.Functor C D} {A A' : CategoryTheory.Functor C (Type w)} (f : A' ⟶ A) (x : F.HomObj G A) (Δ : C)
  (a : A'.obj Δ),
  (CategoryTheory.Functor.HomObj.map f x).app Δ a = x.app Δ ((CategoryTheory.ConcreteCategory.hom (f.app Δ)) a)
-- Mathlib.RingTheory.FractionalIdeal.Basic
Submodule.copy.congr_simp : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (p p_1 : Submodule R M)
  (e_p : p = p_1) (s s_1 : Set M) (e_s : s = s_1) (hs : s = ↑p), p.copy s hs = p_1.copy s_1 ⋯
-- Mathlib.FieldTheory.CardinalEmb
Field.Emb.Cardinal.equivSucc_coherence : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E]
  [rank_inf : Fact (Cardinal.aleph0 ≤ Module.rank F E)] [inst_3 : Algebra.IsAlgebraic F E]
  (i : WithTop (Module.rank F E).ord.ToType)
  (f : ↥(Field.Emb.Cardinal.filtration (Order.succ i)) →ₐ[F] AlgebraicClosure E),
  ((Field.Emb.Cardinal.equivSucc i) f).1 = Field.Emb.Cardinal.embFunctor F E ⋯ f
-- Mathlib.Algebra.ContinuedFractions.TerminatedStable
GenContFract.contsAux_stable_of_terminated : ∀ {K : Type u_1} {g : GenContFract K} {n m : ℕ} [inst : DivisionRing K],
  n < m → g.TerminatedAt n → g.contsAux m = g.contsAux (n + 1)
-- Init.Data.UInt.Lemmas
USize.ofInt.eq_1 : ∀ (x : ℤ), USize.ofInt x = USize.ofNat (x % 2 ^ System.Platform.numBits).toNat
-- Lean.Parser.Command
/-- `namespace <id>` opens a section with label `<id>` that influences naming and name resolution inside
the section:
* Declarations names are prefixed: `def seventeen : ℕ := 17` inside a namespace `Nat` is given the
  full name `Nat.seventeen`.
* Names introduced by `export` declarations are also prefixed by the identifier.
* All names starting with `<id>.` become available in the namespace without the prefix. These names
  are preferred over names introduced by outer namespaces or `open`.
* Within a namespace, declarations can be `protected`, which excludes them from the effects of
  opening the namespace.

As with `section`, namespaces can be nested and the scope of a namespace is terminated by a
corresponding `end <id>` or the end of the file.

`namespace` also acts like `section` in delimiting the scope of `variable`, `open`, and other scoped commands.
 -/
Lean.Parser.Command.namespace : Lean.Parser.Parser
-- Mathlib.LinearAlgebra.Multilinear.Basis
/-- Two multilinear maps indexed by a `Fintype` are equal if they are equal when all arguments
are basis vectors.  -/
Module.Basis.ext_multilinear : ∀ {ι : Type u_1} {R : Type u_2} [inst : CommSemiring R] {M : ι → Type u_3} [inst_1 : (i : ι) → AddCommMonoid (M i)]
  [inst_2 : (i : ι) → Module R (M i)] {N : Type u_4} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [Finite ι]
  {f g : MultilinearMap R M N} {ιM : ι → Type u_5} (e : (i : ι) → Module.Basis (ιM i) R (M i)),
  (∀ (v : (i : ι) → ιM i), (f fun i => (e i) (v i)) = g fun i => (e i) (v i)) → f = g
-- Mathlib.LinearAlgebra.Basis.Cardinality
/-- Over any ring `R`, if `b` is an infinite basis for a module `M`,
and `s` is a maximal linearly independent set,
then the cardinality of `b` is bounded by the cardinality of `s`.
 -/
infinite_basis_le_maximal_linearIndependent : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [Nontrivial R] [inst_3 : Module R M]
  {ι : Type w} (b : Module.Basis ι R M) [Infinite ι] {κ : Type w} (v : κ → M) (i : LinearIndependent R v),
  i.Maximal → Cardinal.mk ι ≤ Cardinal.mk κ
-- Init.Data.UInt.Lemmas
UInt8.ofNat_uInt16ToNat : ∀ (n : UInt16), UInt8.ofNat n.toNat = n.toUInt8
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
_private.Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE.0.CategoryTheory.Triangulated.TStructure.TruncAux.isLE_triangleFunctor_obj_obj₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} 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) (n : ℤ) (A : C),
  t.IsLE ((CategoryTheory.Triangulated.TStructure.TruncAux.triangleFunctor✝ t n).obj A).obj₁ (n - 1)
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
/-- Determinant of 1x1 matrix  -/
Matrix.det_fin_one : ∀ {R : Type v} [inst : CommRing R] (A : Matrix (Fin 1) (Fin 1) R), A.det = A 0 0
-- Mathlib.Data.Nat.BinaryRec
Nat.testBit_bit_zero : ∀ (b : Bool) (n : ℕ), (Nat.bit b n).testBit 0 = b
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- If `f` and `g` are isomorphic arrows, then a mono factorisation of `f`
gives a mono factorisation of `g`  -/
CategoryTheory.Limits.MonoFactorisation.ofArrowIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      CategoryTheory.Limits.MonoFactorisation f.hom →
        (sq : f ⟶ g) → [CategoryTheory.IsIso sq] → CategoryTheory.Limits.MonoFactorisation g.hom
-- Aesop.Tree.Data
Aesop.Rapp.setId : Aesop.RappId → Aesop.Rapp → Aesop.Rapp
-- Init.Data.List.TakeDrop
List.drop_eq_extract : ∀ {α : Type u_1} {l : List α} {k : ℕ}, List.drop k l = l.extract k
-- Mathlib.Algebra.Order.Ring.Abs
Even.pow_abs : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [IsOrderedRing α] {n : ℕ}, Even n → ∀ (a : α), |a| ^ n = a ^ n
-- Mathlib.RingTheory.Localization.Integral
Invertible.mk.congr_simp : ∀ {α : Type u} [inst : Mul α] [inst_1 : One α] {a : α} (invOf invOf_1 : α) (e_invOf : invOf = invOf_1)
  (invOf_mul_self : invOf * a = 1) (mul_invOf_self : a * invOf = 1),
  { invOf := invOf, invOf_mul_self := invOf_mul_self, mul_invOf_self := mul_invOf_self } =
    { invOf := invOf_1, invOf_mul_self := ⋯, mul_invOf_self := ⋯ }
-- Mathlib.Topology.ContinuousOn
continuousOn_of_forall_continuousAt : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β} {s : Set α},
  (∀ x ∈ s, ContinuousAt f x) → ContinuousOn f s
-- Mathlib.Analysis.Normed.Ring.Basic
SubringClass.toSeminormedCommRing : {S : Type u_5} →
  {R : Type u_6} →
    [inst : SetLike S R] → [inst_1 : SeminormedCommRing R] → [_h : SubringClass S R] → (s : S) → SeminormedCommRing ↥s
-- Mathlib.Order.Filter.Extr
inf_eq_of_min : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf β] [inst_1 : OrderTop β] {D : α → β} {s : Finset α}
  [inst_2 : Nonempty α] {b : β}, b ∈ Set.range D → Function.invFun D b ∈ s → (∀ a ∈ s, b ≤ D a) → s.inf D = b
-- Mathlib.LinearAlgebra.Matrix.Transvection
/-- Inductive step for the reduction: if one knows that any size `r` matrix can be reduced to
diagonal form by elementary operations, then one deduces it for matrices over `Fin r ⊕ Unit`.  -/
Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal_induction : ∀ {𝕜 : Type u_3} [inst : Field 𝕜] {r : ℕ},
  (∀ (M : Matrix (Fin r) (Fin r) 𝕜),
      ∃ L₀ L₀' D₀,
        (List.map Matrix.TransvectionStruct.toMatrix L₀).prod * M *
            (List.map Matrix.TransvectionStruct.toMatrix L₀').prod =
          Matrix.diagonal D₀) →
    ∀ (M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜),
      ∃ L L' D,
        (List.map Matrix.TransvectionStruct.toMatrix L).prod * M *
            (List.map Matrix.TransvectionStruct.toMatrix L').prod =
          Matrix.diagonal D
-- Mathlib.Order.Closure
/-- Send an element to a closed element (by taking the closure).  -/
ClosureOperator.toCloseds : {α : Type u_1} → [inst : Preorder α] → (c : ClosureOperator α) → α → c.Closeds
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k a : α} {v : β} {h₁ : a ∈ t.insert k v},
  Std.DTreeMap.Const.get (t.insert k v) a h₁ = if h₂ : cmp k a = Ordering.eq then v else Std.DTreeMap.Const.get t a ⋯