mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.RCLike.Basic
RCLike.ofReal_sub : ∀ {K : Type u_1} [inst : RCLike K] (r s : ℝ), ↑(r - s) = ↑r - ↑s
-- Mathlib.AlgebraicGeometry.GammaSpecAdjunction
AlgebraicGeometry.LocallyRingedSpace.toΓSpecSheafedSpace_hom_c_app : ∀ (X : AlgebraicGeometry.LocallyRingedSpace)
  (X_1 :
    (TopologicalSpace.Opens
        ↑(AlgebraicGeometry.PrimeSpectrum.Top ↑(AlgebraicGeometry.LocallyRingedSpace.Γ.obj (Opposite.op X))))ᵒᵖ),
  X.toΓSpecSheafedSpace.hom.c.app X_1 =
    CategoryTheory.yoneda.preimage ((CategoryTheory.Functor.IsCoverDense.sheafYonedaHom X.toΓSpecCBasicOpens).app X_1)
-- Mathlib.CategoryTheory.Limits.Shapes.NormalMono.Equalizers
/-- The equalizer of `f` and `g` exists.  -/
CategoryTheory.NormalMonoCategory.hasLimit_parallelPair : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteProducts C] [CategoryTheory.Limits.HasKernels C]
  [CategoryTheory.IsNormalMonoCategory C] {X Y : C} (f g : X ⟶ Y),
  CategoryTheory.Limits.HasLimit (CategoryTheory.Limits.parallelPair f g)
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.markRecDecls.visit : {pu : Lean.Compiler.LCNF.Purity} →
  Array (Lean.Compiler.LCNF.Decl pu) →
    {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → StateM Lean.NameSet Unit
-- Mathlib.Topology.Instances.AddCircle.Defs
AddCircle.coe_fract : ∀ {𝕜 : Type u_1} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : FloorRing 𝕜] (x : 𝕜), ↑(Int.fract x) = ↑x
-- Init.Data.String.Lemmas.Pattern.Pred
String.Slice.Pattern.Model.CharPred.Decidable.isMatch_iff : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice} {pos : s.Pos},
  String.Slice.Pattern.Model.IsMatch p pos ↔
    ∃ (h : s.startPos ≠ s.endPos), pos = s.startPos.next h ∧ p (s.startPos.get h)
-- Mathlib.RingTheory.WittVector.Truncated
/-- `truncateFun n x` uses the first `n` entries of `x` to construct a `TruncatedWittVector`,
which has the same base `p` as `x`.
This function is bundled into a ring homomorphism in `WittVector.truncate`  -/
WittVector.truncateFun : {p : ℕ} → (n : ℕ) → {R : Type u_1} → WittVector p R → TruncatedWittVector p n R
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.eq_1 : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preregular C],
  CategoryTheory.regularTopology C = (CategoryTheory.regularCoverage C).toGrothendieck
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
AddMonoidAlgebra.mapDomainBialgHomEquiv.congr_simp : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : AddGroup G]
  [inst_3 : AddGroup H], AddMonoidAlgebra.mapDomainBialgHomEquiv = AddMonoidAlgebra.mapDomainBialgHomEquiv
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getThenInsertIfNew?_fst : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, (m.getThenInsertIfNew? k v).1 = m.get? k
-- Mathlib.CategoryTheory.Limits.IsLimit
/-- Constructing an equivalence `IsLimit c ≃ IsLimit d` from a natural isomorphism
between the underlying functors, and then an isomorphism between `c` transported along this and `d`.
 -/
CategoryTheory.Limits.IsLimit.equivOfNatIsoOfIso : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G : CategoryTheory.Functor J C} →
          (α : F ≅ G) →
            (c : CategoryTheory.Limits.Cone F) →
              (d : CategoryTheory.Limits.Cone G) →
                ((CategoryTheory.Limits.Cone.postcompose α.hom).obj c ≅ d) →
                  CategoryTheory.Limits.IsLimit c ≃ CategoryTheory.Limits.IsLimit d
-- Mathlib.Order.Partition.Basic
/-- The representative of a part belongs to that part.  -/
Partition.rep_mem : ∀ {α : Type u_1} {u t : Set α} {P : Partition u} (ht : t ∈ P), P.rep ht ∈ t
-- Mathlib.Algebra.Group.Indicator
Set.mulIndicator_sdiff' : ∀ {α : Type u_1} {G : Type u_6} [inst : Group G] {s t : Set α},
  s ⊆ t → ∀ (f : α → G), (t \ s).mulIndicator f = t.mulIndicator f / s.mulIndicator f
-- Mathlib.SetTheory.Cardinal.Cofinality.Basic
Order.cof_eq_zero_iff : ∀ {α : Type u} [inst : Preorder α], Order.cof α = 0 ↔ IsEmpty α
-- Mathlib.Order.BooleanAlgebra.Basic
sdiff_eq : ∀ {α : Type u} {x y : α} [inst : BooleanAlgebra α], x \ y = x ⊓ yᶜ
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.TacticMVarKind.fieldAutoParam.inj : ∀ {fieldName structName fieldName_1 structName_1 : Lean.Name},
  Lean.Elab.Term.TacticMVarKind.fieldAutoParam fieldName structName =
      Lean.Elab.Term.TacticMVarKind.fieldAutoParam fieldName_1 structName_1 →
    fieldName = fieldName_1 ∧ structName = structName_1
-- Mathlib.Probability.Independence.Kernel.IndepFun
ProbabilityTheory.Kernel.iIndepFun.indepFun_mul_left₀ : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β} [inst : Mul β]
  [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), AEMeasurable (f i) (μ.bind ⇑κ)) →
      ∀ (i j k : ι), i ≠ k → j ≠ k → ProbabilityTheory.Kernel.IndepFun (f i * f j) (f k) κ μ
-- Mathlib.RingTheory.UniqueFactorizationDomain.Ideal
/-- **Alias** of `WfDvdMonoid.of_setOfPred_isPrincipal_wellFoundedOn_gt`.

---

The ascending chain condition on principal ideals in a domain is sufficient to prove that
the domain is `WfDvdMonoid`.  -/
WfDvdMonoid.of_setOf_isPrincipal_wellFoundedOn_gt : ∀ {α : Type u_1} [inst : CommSemiring α] [IsDomain α],
  ({I | Submodule.IsPrincipal I}.WellFoundedOn fun x1 x2 => x1 > x2) → WfDvdMonoid α
-- Init.Data.String.Lemmas.Order
String.Pos.lt_slice_iff : ∀ {s : String} {p₀ p₁ : s.Pos} {h : p₀ ≤ p₁} {p : (s.slice p₀ p₁ h).Pos} {q : s.Pos} {h₀ : p₀ ≤ q} {h₁ : q ≤ p₁},
  p < q.slice p₀ p₁ h₀ h₁ ↔ String.Pos.ofSlice p < q
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp.Kernels
SemiNormedGrp.explicitCokernel_hom_ext_iff : ∀ {X Y Z : SemiNormedGrp} {f : X ⟶ Y} {e₁ e₂ : SemiNormedGrp.explicitCokernel f ⟶ Z},
  e₁ = e₂ ↔
    CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelπ f) e₁ =
      CategoryTheory.CategoryStruct.comp (SemiNormedGrp.explicitCokernelπ f) e₂
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
_private.Mathlib.Combinatorics.SetFamily.AhlswedeZhang.0.Fintype.sum_div_mul_card_choose_card : ∀ (α : Type u_1) [inst : Fintype α] [Nonempty α],
  ∑ s, ↑(Fintype.card α) / ((↑(Fintype.card α) - ↑s.card) * ↑((Fintype.card α).choose s.card)) =
    ↑(Fintype.card α) * ∑ k ∈ Finset.range (Fintype.card α), (↑k)⁻¹ + 1
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.openCell_subset_complex`. -/
Topology.CWComplex.openCell_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.openCell n j ⊆ C
-- Lean.Meta.Tactic.Simp.SimpAll
Lean.Meta.SimpAll.Entry.mk.injEq : ∀ (fvarId : Lean.FVarId) (userName : Lean.Name) (id : Lean.Meta.Origin) (origType type proof : Lean.Expr)
  (fvarId_1 : Lean.FVarId) (userName_1 : Lean.Name) (id_1 : Lean.Meta.Origin) (origType_1 type_1 proof_1 : Lean.Expr),
  ({ fvarId := fvarId, userName := userName, id := id, origType := origType, type := type, proof := proof } =
      { fvarId := fvarId_1, userName := userName_1, id := id_1, origType := origType_1, type := type_1,
        proof := proof_1 }) =
    (fvarId = fvarId_1 ∧ userName = userName_1 ∧ id = id_1 ∧ origType = origType_1 ∧ type = type_1 ∧ proof = proof_1)
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- `rel'` as a ring congruence.  -/
LinearAlgebra.FreeProduct.ringCon' : {I : Type u} →
  [DecidableEq I] →
    (R : Type v) →
      [inst : CommSemiring R] →
        (A : I → Type w) →
          [inst_1 : (i : I) → Semiring (A i)] →
            [inst_2 : (i : I) → Algebra R (A i)] → RingCon (LinearAlgebra.FreeProduct.PowerAlgebra R A)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace.Gluing
AlgebraicGeometry.SheafedSpace.GlueData.ι_jointly_surjective : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (D : AlgebraicGeometry.SheafedSpace.GlueData C)
  [inst_1 : CategoryTheory.Limits.HasLimits C] (x : ↑↑D.glued.toPresheafedSpace),
  ∃ i y, (CategoryTheory.ConcreteCategory.hom (D.ι i).hom.base) y = x
-- Mathlib.Analysis.InnerProductSpace.Harmonic.Basic
/-- Harmonic functions are two times continuously differentiable.
 -/
InnerProductSpace.HarmonicOnNhd.contDiffOn : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : FiniteDimensional ℝ E]
  {F : Type u_2} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace ℝ F] {f : E → F} {s : Set E},
  InnerProductSpace.HarmonicOnNhd f s → ContDiffOn ℝ 2 f s
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.instFiniteTensorUnit : (CategoryTheory.MonoidalCategoryStruct.tensorUnit SSet).Finite
-- Mathlib.Order.CompactlyGenerated.Basic
sSupIndep_iUnion_of_directed : ∀ {α : Type u_2} [inst : CompleteLattice α] [IsCompactlyGenerated α] {η : Type u_3} {s : η → Set α},
  Directed (fun x1 x2 => x1 ⊆ x2) s → (∀ (i : η), sSupIndep (s i)) → sSupIndep (⋃ i, s i)
-- Mathlib.CategoryTheory.LocallyDirected
/-- We say that a functor `F` to `Type*` is locally directed if for every `x ∈ F.obj k`, the
set of `F.obj` containing `x` is (co)directed.
That is, for each diagram
```
      x ∈ Fₖ
    ↗       ↖
xᵢ ∈ Fᵢ    xⱼ ∈ Fⱼ
```
there exists
```
xᵢ ∈ Fᵢ    xⱼ ∈ Fⱼ
    ↖       ↗
      xₗ ∈ Fₗ
```
that commutes with it.
 -/
CategoryTheory.Functor.IsLocallyDirected : {J : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} J] → CategoryTheory.Functor J (Type u_2) → Prop
-- Mathlib.Data.Set.Semiring
SetSemiring.instNoZeroDivisors : ∀ {α : Type u_1} [inst : Mul α], NoZeroDivisors (SetSemiring α)
-- Mathlib.LinearAlgebra.TensorProduct.Decomposition
DirectSum.val_decomposeTensorEquiv_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (ℳ : ι → Submodule R M) (N : Type u_5) [inst_3 : AddCommMonoid N] [inst_4 : Module R N] [inst_5 : DecidableEq ι]
  [inst_6 : DirectSum.Decomposition ℳ] {i : ι} (x : TensorProduct R (↥(ℳ i)) N),
  ↑((DirectSum.decomposeTensorEquiv ℳ N i) x) = (LinearMap.rTensor N (ℳ i).subtype) x
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- `LimitCone F` contains a cone over `F` together with the information that it is a limit.  -/
CategoryTheory.Limits.LimitCone : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} → [inst_1 : CategoryTheory.Category.{v, u} C] → CategoryTheory.Functor J C → Type (max (max u u₁) v)
-- Mathlib.Tactic.Module
_private.Mathlib.Tactic.Module.0.Mathlib.Tactic.Module.qNF.add.eq_def : ∀ {u v : Lean.Level} {M : Q(Type v)} {R : Q(Type u)} (iR : Q(Semiring «$R»)) (x x_1 : Mathlib.Tactic.Module.qNF R M),
  Mathlib.Tactic.Module.qNF.add iR x x_1 =
    match x, x_1 with
    | [], l => l
    | l, [] => l
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ =>
      if k₁ < k₂ then ((a₁, x₁), k₁) ::ᵣ Mathlib.Tactic.Module.qNF.add iR t₁ (((a₂, x₂), k₂) ::ᵣ t₂)
      else
        if k₁ = k₂ then ((q(«$a₁» + «$a₂»), x₁), k₁) ::ᵣ Mathlib.Tactic.Module.qNF.add iR t₁ t₂
        else ((a₂, x₂), k₂) ::ᵣ Mathlib.Tactic.Module.qNF.add iR (((a₁, x₁), k₁) ::ᵣ t₁) t₂
-- Mathlib.MeasureTheory.Measure.FiniteMeasure
MeasureTheory.FiniteMeasure.tendsto_of_forall_integral_tendsto : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : TopologicalSpace Ω] [inst_2 : OpensMeasurableSpace Ω]
  {γ : Type u_2} {F : Filter γ} {μs : γ → MeasureTheory.FiniteMeasure Ω} {μ : MeasureTheory.FiniteMeasure Ω},
  (∀ (f : BoundedContinuousFunction Ω ℝ),
      Filter.Tendsto (fun i => ∫ (x : Ω), f x ∂↑(μs i)) F (nhds (∫ (x : Ω), f x ∂↑μ))) →
    Filter.Tendsto μs F (nhds μ)
-- Mathlib.CategoryTheory.Presentable.Retracts
CategoryTheory.Retract.isCardinalPresentable : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (h : CategoryTheory.Retract Y X) (κ : Cardinal.{w})
  [inst_1 : Fact κ.IsRegular] [CategoryTheory.IsCardinalPresentable X κ], CategoryTheory.IsCardinalPresentable Y κ
-- Mathlib.Topology.Algebra.Support
/-- In a compact space `α`, any function has compact support.  -/
HasCompactMulSupport.of_compactSpace : ∀ {α : Type u_2} {γ : Type u_5} [inst : TopologicalSpace α] [inst_1 : One γ] [CompactSpace α] (f : α → γ),
  HasCompactMulSupport f
-- Mathlib.Data.Seq.Defs
Stream'.Seq.coeMLList : {α : Type u} → Coe (MLList Id α) (Stream'.Seq α)
-- Init.Data.Int.DivMod.Lemmas
Int.fdiv_eq_tdiv_of_nonneg : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → a.fdiv b = a.tdiv b
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getKey?_eq_getKey? : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α}, m.getKey? a = Std.Internal.List.getKey? a (Std.DHashMap.Internal.toListModel (↑m).buckets)
-- Mathlib.RingTheory.Extension.Generators
/-- A section of `R[X] → S`.  -/
Algebra.Generators.σ' : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] → [inst_2 : Algebra R S] → Algebra.Generators R S ι → S → MvPolynomial ι R
-- Mathlib.GroupTheory.Subgroup.Center
IsConj.eq_of_left_mem_center : ∀ {M : Type u_2} [inst : Monoid M] {g h : M}, IsConj g h → g ∈ Set.center M → g = h
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.replicateRow_cons : ∀ {α : Type u} {m : ℕ} {ι : Type u_1} (x : α) (u : Fin m → α),
  Matrix.replicateRow ι (Matrix.vecCons x u) = Matrix.of fun x_1 => Matrix.vecCons x u
-- Mathlib.RingTheory.AdicCompletion.Basic
IsAdicComplete.lift.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : Type u_5} [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : IsAdicComplete I N]
  (f : (n : ℕ) → M →ₗ[R] N ⧸ I ^ n • ⊤) (h : ∀ {m n : ℕ} (hle : m ≤ n), Submodule.factorPow I N hle ∘ₗ f n = f m),
  IsAdicComplete.lift I f h = ↑(AdicCompletion.ofLinearEquiv I N).symm ∘ₗ AdicCompletion.lift I f ⋯
-- Mathlib.Analysis.Normed.Lp.lpSpace
lp.norm_toNorm : ∀ {α : Type u_3} {E : α → Type u_4} [inst : (i : α) → NormedAddCommGroup (E i)] {p : ENNReal} {x : ↥(lp E p)},
  ‖lp.toNorm x‖ = ‖x‖
-- Mathlib.Logic.Equiv.List
List.countable : ∀ {α : Type u_2} [Countable α], Countable (List α)
-- Init.Data.Int.Linear
Int.Internal.Linear.le_combine_coeff : ∀ (ctx : Int.Internal.Linear.Context) (p₁ p₂ p₃ : Int.Internal.Linear.Poly) (k : ℤ),
  Int.Internal.Linear.le_combine_coeff_cert p₁ p₂ p₃ k = true →
    Int.Internal.Linear.Poly.denote' ctx p₁ ≤ 0 →
      Int.Internal.Linear.Poly.denote' ctx p₂ ≤ 0 → Int.Internal.Linear.Poly.denote' ctx p₃ ≤ 0
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.attachCodeDecls.go.match_1.eq_9 : ∀ {pu : Lean.Compiler.LCNF.Purity} (motive : Lean.Compiler.LCNF.CodeDecl pu → Sort u_1) (fvarId : Lean.FVarId) (n : ℕ)
  (check persistent : Bool) (objs? : Option ℕ) (h : pu = Lean.Compiler.LCNF.Purity.impure)
  (h_1 : (decl : Lean.Compiler.LCNF.LetDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.let decl))
  (h_2 :
    (decl : Lean.Compiler.LCNF.FunDecl pu) →
      (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.CodeDecl.fun decl h))
  (h_3 : (decl : Lean.Compiler.LCNF.FunDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.jp decl))
  (h_4 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.Compiler.LCNF.Arg pu) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h))
  (h_5 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.FVarId) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h))
  (h_6 :
    (fvarId : Lean.FVarId) →
      (idx offset : ℕ) →
        (y : Lean.FVarId) →
          (ty : Lean.Expr) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h))
  (h_7 :
    (fvarId : Lean.FVarId) →
      (cidx : ℕ) →
        (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h))
  (h_8 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
            motive (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h))
  (h_9 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (objs? : Option ℕ) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h))
  (h_10 :
    (fvarId : Lean.FVarId) →
      (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.del fvarId h)),
  (match Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h with
    | Lean.Compiler.LCNF.CodeDecl.let decl => h_1 decl
    | Lean.Compiler.LCNF.CodeDecl.fun decl h => h_2 decl h
    | Lean.Compiler.LCNF.CodeDecl.jp decl => h_3 decl
    | Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h => h_4 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h => h_5 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h => h_6 fvarId idx offset y ty h
    | Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h => h_7 fvarId cidx h
    | Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h => h_8 fvarId n check persistent h
    | Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h => h_9 fvarId n check persistent objs? h
    | Lean.Compiler.LCNF.CodeDecl.del fvarId h => h_10 fvarId h) =
    h_9 fvarId n check persistent objs? h
-- Init.Data.UInt.Bitwise
UInt16.toBitVec_shiftRight : ∀ (a b : UInt16), (a >>> b).toBitVec = a.toBitVec >>> (b.toBitVec % 16)
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.bot_ne_ofNat : ∀ {α : Type u} [inst : AddMonoidWithOne α] (n : ℕ) [inst_1 : n.AtLeastTwo], ⊥ ≠ OfNat.ofNat n
-- Mathlib.RingTheory.PowerSeries.Order
/-- The order of a formal power series is at least `n` if
the `i`th coefficient is `0` for all `i < n`.  -/
PowerSeries.le_order : ∀ {R : Type u_1} [inst : Semiring R] (φ : PowerSeries R) (n : ℕ∞),
  (∀ (i : ℕ), ↑i < n → (PowerSeries.coeff i) φ = 0) → n ≤ φ.order
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.neg_Iic : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : PartialOrder α] [IsOrderedAddMonoid α] (a : α),
  -Set.Iic a = Set.Ici (-a)
-- Mathlib.Combinatorics.Quiver.Covering
/-- A prefunctor induces a map of `Quiver.Star` at every vertex.  -/
Prefunctor.star : {U : Type u_1} →
  [inst : Quiver U] →
    {V : Type u_2} → [inst_1 : Quiver V] → (φ : U ⥤q V) → (u : U) → Quiver.Star u → Quiver.Star (φ.obj u)
-- Init.Data.Nat.Lemmas
Nat.dvd_iff_le_div_mul : ∀ (n d : ℕ), d ∣ n ↔ n ≤ n / d * d
-- Batteries.Data.List.Lemmas
_private.Batteries.Data.List.Lemmas.0.List.max!.match_1.splitter : {α : Type u_1} →
  (motive : Option α → Sort u_2) → (x : Option α) → (Unit → motive none) → ((x : α) → motive (some x)) → motive x
-- Mathlib.Data.Multiset.Lattice
Multiset.inf_coe : ∀ {α : Type u_1} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (l : List α),
  (↑l).inf = List.foldr (fun x1 x2 => x1 ⊓ x2) ⊤ l
-- Mathlib.Order.CompleteLattice.Basic
binary_relation_sSup_iff : ∀ {α : Type u_8} {β : Type u_9} (s : Set (α → β → Prop)) {a : α} {b : β}, sSup s a b ↔ ∃ r ∈ s, r a b
-- Mathlib.CategoryTheory.WithTerminal.Lemmas
CategoryTheory.WithTerminal.instIsCofilteredOfIsCofilteredOrEmpty : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [CategoryTheory.IsCofilteredOrEmpty C],
  CategoryTheory.IsCofiltered (CategoryTheory.WithTerminal C)
-- Mathlib.Algebra.Polynomial.Degree.SmallDegree
Polynomial.degree_linear_le : ∀ {R : Type u} {a b : R} [inst : Semiring R], (Polynomial.C a * Polynomial.X + Polynomial.C b).degree ≤ 1
-- Mathlib.Algebra.Group.Hom.Basic
ZeroHom.neg_comp : ∀ {M : Type u_2} {N : Type u_3} {P : Type u_4} [inst : Zero M] [inst_1 : Zero N] [inst_2 : NegZeroClass P]
  (g : ZeroHom N P) (f : ZeroHom M N), (-g).comp f = -g.comp f
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.isFun : {pu : Lean.Compiler.LCNF.Purity} → Lean.Compiler.LCNF.Code pu → Bool
-- Lean.Elab.App
/-- Instance implicit arguments collected so far.  -/
Lean.Elab.Term.ElabElim.State.instMVars : Lean.Elab.Term.ElabElim.State → Array Lean.MVarId
-- Mathlib.Analysis.CStarAlgebra.Matrix
/-- The natural star algebra equivalence between matrices and continuous linear endomorphisms
of Euclidean space induced by the orthonormal basis `EuclideanSpace.basisFun`.

This is a more-bundled version of `Matrix.toEuclideanLin`, for the special case of square matrices,
followed by a more-bundled version of `LinearMap.toContinuousLinearMap`.  -/
Matrix.toEuclideanCLM : {𝕜 : Type u_1} →
  {n : Type u_3} →
    [inst : RCLike 𝕜] →
      [inst_1 : Fintype n] → [DecidableEq n] → Matrix n n 𝕜 ≃⋆ₐ[𝕜] EuclideanSpace 𝕜 n →L[𝕜] EuclideanSpace 𝕜 n
-- Mathlib.Analysis.Convex.Join
convexJoin_assoc : ∀ {𝕜 : Type u_2} {E : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] (s t u : Set E),
  convexJoin 𝕜 (convexJoin 𝕜 s t) u = convexJoin 𝕜 s (convexJoin 𝕜 t u)
-- Mathlib.Topology.EMetricSpace.Lipschitz
LipschitzWith.zero_iff : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {β : Type u_1} [inst_1 : EMetricSpace β] (f : α → β),
  LipschitzWith 0 f ↔ ∀ (x y : α), f x = f y
-- Mathlib.RingTheory.PicardGroup
CommRing.Pic.inv_eq_dual : ∀ {R : Type u} [inst : CommSemiring R] (M : CommRing.Pic R), M⁻¹ = CommRing.Pic.mk R (Module.Dual R M.AsModule)
-- Mathlib.Topology.NhdsWithin
map_nhdsSet_subtype_val : ∀ {α : Type u_1} [inst : TopologicalSpace α] {s : Set α} (t : Set ↑s),
  Filter.map Subtype.val (nhdsSet t) = nhdsSetWithin (Subtype.val '' t) s
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- Transport evidence that a left extension is a Kan extension across an isomorphism
of extensions.  -/
CategoryTheory.Bicategory.LeftExtension.IsKan.ofIsoKan : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c : B} →
      {f : a ⟶ b} → {g : a ⟶ c} → {s t : CategoryTheory.Bicategory.LeftExtension f g} → s.IsKan → (s ≅ t) → t.IsKan
-- Mathlib.RingTheory.MvPolynomial.Basic
/-- The submodule of polynomials of total degree less than or equal to `m`.  -/
MvPolynomial.restrictTotalDegree : (σ : Type u) → (R : Type v) → [inst : CommSemiring R] → ℕ → Submodule R (MvPolynomial σ R)
-- Mathlib.Algebra.FreeMonoid.Basic
FreeAddMonoid.instAddCancelMonoid.eq_1 : ∀ {α : Type u_1},
  FreeAddMonoid.instAddCancelMonoid =
    { add := fun x y => FreeAddMonoid.ofList (FreeAddMonoid.toList x ++ FreeAddMonoid.toList y), add_assoc := ⋯,
      zero := FreeAddMonoid.ofList [], zero_add := ⋯, add_zero := ⋯, nsmul := nsmulRecAuto, nsmul_zero := ⋯,
      nsmul_succ := ⋯, toIsLeftCancelAdd := ⋯, toIsRightCancelAdd := ⋯ }
-- Mathlib.Analysis.Complex.HasPrimitives
/-- **Morera's theorem for the complex plane** A continuous function on `ℂ` whose integrals on
rectangles vanish, has primitives.
 -/
Complex.IsConservativeOn.isExactOn_univ : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : ℂ → E} [CompleteSpace E],
  Continuous f → Complex.IsConservativeOn f Set.univ → Complex.IsExactOn f Set.univ
-- Batteries.Data.List.Basic
/-- If `a` relates to `b` and `b::l` is a chain, then `a :: b :: l` is also a chain.  -/
List.Chain.cons : ∀ {α : Type u_1} {R : α → α → Prop} {b : α} {l : List α} {a : α}, R a b → List.Chain R b l → List.Chain R a (b :: l)
-- Mathlib.AlgebraicGeometry.Scheme
/-- Pretty printer for coercing schemes to types.  -/
AlgebraicGeometry.Scheme.delabAdjoinNotation : Lean.PrettyPrinter.Delaborator.Delab