mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Factorizations.CM5b
CochainComplex.cm5b.instQuasiIsoIntP : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.EnoughInjectives C] {K L : CochainComplex C ℤ}, QuasiIso (CochainComplex.cm5b.p K L)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- A monad equipped with the ability to manipulate 1-morphisms.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₁ : (Type → Type) → Type
-- Mathlib.Order.Ideal
Order.Ideal.top_notMem_iff_ne_top : ∀ {P : Type u_1} [inst : LE P] [inst_1 : OrderTop P] {I : Order.Ideal P}, ⊤ ∉ I ↔ I ≠ ⊤
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgHom.mk.inj : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} {inst : CommSemiring R} {inst_1 : Semiring A} {inst_2 : Algebra R A}
  {inst_3 : Star A} {inst_4 : Semiring B} {inst_5 : Algebra R B} {inst_6 : Star B} {toAlgHom : A →ₐ[R] B}
  {map_star' : ∀ (x : A), (↑↑toAlgHom.toRingHom).toFun (star x) = star ((↑↑toAlgHom.toRingHom).toFun x)}
  {toAlgHom_1 : A →ₐ[R] B}
  {map_star'_1 : ∀ (x : A), (↑↑toAlgHom_1.toRingHom).toFun (star x) = star ((↑↑toAlgHom_1.toRingHom).toFun x)},
  { toAlgHom := toAlgHom, map_star' := map_star' } = { toAlgHom := toAlgHom_1, map_star' := map_star'_1 } →
    toAlgHom = toAlgHom_1
-- Mathlib.Analysis.Normed.Group.HomCompletion
NormedAddGroupHom.completion_sub : ∀ {G : Type u_1} [inst : SeminormedAddCommGroup G] {H : Type u_2} [inst_1 : SeminormedAddCommGroup H]
  (f g : NormedAddGroupHom G H), (f - g).completion = f.completion - g.completion
-- Mathlib.Data.Countable.Basic
ENat.instCountable : Countable ℕ∞
-- Mathlib.CategoryTheory.Preadditive.FreydCategory.RightFreyd
/-- The category `RightFreyd V` is preadditive.  -/
CategoryTheory.Preadditive.instRightFreyd : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    [inst_1 : CategoryTheory.Preadditive V] → CategoryTheory.Preadditive (CategoryTheory.Preadditive.RightFreyd V)
-- Aesop.Forward.PremiseIndex
Aesop.instOrdPremiseIndex.ord : Aesop.PremiseIndex → Aesop.PremiseIndex → Ordering
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.piCongr_toEquiv : ∀ {ι₁ : Type u_4} {ι₂ : Type u_5} {β₁ : ι₁ → Type u_6} {β₂ : ι₂ → Type u_7} [inst : (i₁ : ι₁) → UniformSpace (β₁ i₁)]
  [inst_1 : (i₂ : ι₂) → UniformSpace (β₂ i₂)] (e : ι₁ ≃ ι₂) (F : (i₁ : ι₁) → β₁ i₁ ≃ᵤ β₂ (e i₁)),
  (UniformEquiv.piCongr e F).toEquiv = (Equiv.piCongrRight fun i => (F i).toEquiv).trans (Equiv.piCongrLeft β₂ e)
-- Mathlib.RingTheory.Perfection
Perfection.ext : ∀ {R : Type u_1} [inst : CommSemiring R] {p : ℕ} [hp : Fact (Nat.Prime p)] [inst_1 : CharP R p] {f g : Perfection R p},
  (∀ (n : ℕ), (Perfection.coeff R p n) f = (Perfection.coeff R p n) g) → f = g
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddModObj.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] →
            {M : C} →
              [inst_4 : CategoryTheory.AddMonObj M] →
                {X : D} →
                  (vadd : CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj M X ⟶ X) →
                    autoParam
                        (CategoryTheory.CategoryStruct.comp
                            (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
                              CategoryTheory.AddMonObj.zero X)
                            vadd =
                          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso X).hom)
                        CategoryTheory.AddModObj.zero_vadd._autoParam →
                      autoParam
                          (CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
                                CategoryTheory.AddMonObj.add X)
                              vadd =
                            CategoryTheory.CategoryStruct.comp
                              (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso M M X).hom
                              (CategoryTheory.CategoryStruct.comp
                                (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight M vadd) vadd))
                          CategoryTheory.AddModObj.add_vadd._autoParam →
                        CategoryTheory.AddModObj M X
-- Mathlib.Algebra.Order.Field.Basic
div_pos_iff_of_pos_left : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α} [IsStrictOrderedRing α],
  0 < a → (0 < a / b ↔ 0 < b)
-- Mathlib.NumberTheory.MulChar.Basic
/-- The product of a character with its inverse is the trivial character.  -/
MulChar.inv_mul : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ : MulChar R R'), χ⁻¹ * χ = 1
-- Mathlib.Data.Set.Function
Set.surjOn_iff_exists_map_subtype : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β},
  Set.SurjOn f s t ↔ ∃ t' g, t ⊆ t' ∧ Function.Surjective g ∧ ∀ (x : ↑s), f ↑x = ↑(g x)
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_closure : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {s : Set M},
  Submodule.span R ↑(AddSubmonoid.closure s) = Submodule.span R s
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- The intersection of distinct prime powers in a Dedekind domain is the product of these
prime powers.
See `IsDedekindDomain.inf_pow_eq_prod_of_prime` for the version in terms of `Ideal R`.  -/
IsDedekindDomain.HeightOneSpectrum.inf_pow_eq_prod : ∀ {R : Type u_1} [inst : CommRing R] {ι : Type u_4} [IsDedekindDomain R] (s : Finset ι) (e : ι → ℕ)
  (f : ι → IsDedekindDomain.HeightOneSpectrum R),
  (∀ i ∈ s, ∀ j ∈ s, i ≠ j → f i ≠ f j) → (s.inf fun i => (f i).asIdeal ^ e i) = ∏ i ∈ s, (f i).asIdeal ^ e i
-- Mathlib.LinearAlgebra.Basis.Submodule
/-- Let `A` be a subgroup of an additive commutative group `M` that is also an `R`-module.
Construct a basis of `A` as a `ℤ`-basis from an `R`-basis of `E` that generates `A`.
 -/
Module.Basis.addSubgroupOfClosure : {M : Type u_7} →
  {R : Type u_8} →
    [inst : Ring R] →
      [Nontrivial R] →
        [IsAddTorsionFree R] →
          [inst_3 : AddCommGroup M] →
            [inst_4 : Module R M] →
              (A : AddSubgroup M) →
                {ι : Type u_9} →
                  (b : Module.Basis ι R M) →
                    A = AddSubgroup.closure (Set.range ⇑b) → Module.Basis ι ℤ ↥(AddSubgroup.toIntSubmodule A)
-- Mathlib.Algebra.Group.Fin.Basic
Fin.le_sub_one_iff : ∀ {n : ℕ} {k : Fin (n + 1)}, k ≤ k - 1 ↔ k = 0
-- Mathlib.MeasureTheory.Group.AEStabilizer
AddAction.stabilizer_le_aestabilizer : ∀ {G : Type u_1} {α : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G α] {x : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} [inst_2 : MeasureTheory.VAddInvariantMeasure G α μ] (s : Set α),
  AddAction.stabilizer G s ≤ AddAction.aestabilizer G μ s
-- Std.Data.HashMap.Lemmas
Std.HashMap.get?_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, (m₁ \ m₂).get? k = if k ∈ m₂ then none else m₁.get? k
-- Std.Sat.AIG.Basic
/-- The denotation of the sub-DAG in the `aig` at node `start` is false for all assignments.
 -/
Std.Sat.AIG.UnsatAt : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → (aig : Std.Sat.AIG α) → (start : ℕ) → Bool → start < aig.decls.size → Prop
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
ContMDiffOn.sub : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {I : ModelWithCorners 𝕜 E H} {n : WithTop ℕ∞}
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] {E' : Type u_5}
  [inst_7 : NormedAddCommGroup E'] [inst_8 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_9 : TopologicalSpace H']
  {I' : ModelWithCorners 𝕜 E' H'} {M : Type u_7} [inst_10 : TopologicalSpace M] [inst_11 : ChartedSpace H' M]
  [LieAddGroup I n G] {f g : M → G} {s : Set M},
  ContMDiffOn I' I n f s → ContMDiffOn I' I n g s → ContMDiffOn I' I n (fun x => f x - g x) s
-- Mathlib.Analysis.BoxIntegral.Partition.Basic
BoxIntegral.Prepartition.IsPartition.restrict : ∀ {ι : Type u_1} {I J : BoxIntegral.Box ι} {π : BoxIntegral.Prepartition I},
  π.IsPartition → J ≤ I → (π.restrict J).IsPartition
-- Mathlib.CategoryTheory.Join.Pseudofunctor
CategoryTheory.Join.pseudofunctorRight_mapId_inv_toNatTrans_app : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : CategoryTheory.Cat) (x : CategoryTheory.Join C ↑D),
  ((CategoryTheory.Join.pseudofunctorRight C).mapId D).inv.toNatTrans.app x =
    match x with
    | CategoryTheory.Join.left x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.left x)
    | CategoryTheory.Join.right x => CategoryTheory.CategoryStruct.id (CategoryTheory.Join.right x)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.intCast_apply : ∀ {𝕜₂ : Type u_2} [inst : NormedField 𝕜₂] {F : Type u_4} [inst_1 : AddCommGroup F] [inst_2 : TopologicalSpace F]
  [inst_3 : Module 𝕜₂ F] [inst_4 : IsTopologicalAddGroup F] (n : ℤ) (x : F), ↑n x = n • x
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the forward direction of `lt_inv'`. -/
lt_inv_of_lt_inv : ∀ {α : Type u} [inst : Group α] [inst_1 : LT α] [MulLeftStrictMono α] {a b : α} [MulRightStrictMono α],
  a < b⁻¹ → b < a⁻¹
-- Init.Data.UInt.Lemmas
Fin.mk_uSizeToNat : ∀ (n : USize), ⟨n.toNat, ⋯⟩ = n.toFin
-- Mathlib.Order.Interval.Finset.Defs
/-- `x ∈ finsetIic a ↔ x ≤ a`  -/
LocallyFiniteOrderBot.finset_mem_Iic : ∀ {α : Type u_1} {inst : Preorder α} [self : LocallyFiniteOrderBot α] (a x : α),
  x ∈ LocallyFiniteOrderBot.finsetIic a ↔ x ≤ a
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.iIndepFun.cond : ∀ {ι : Type u_6} {Ω : Type u_7} {α : Type u_8} {β : Type u_9} {mΩ : MeasurableSpace Ω} {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure Ω} {X : ι → Ω → α} {Y : ι → Ω → β} {t : ι → Set β} [Finite ι],
  (∀ (i : ι), Measurable (Y i)) →
    ProbabilityTheory.iIndepFun (fun i ω => (X i ω, Y i ω)) μ →
      (∀ (i : ι), μ (Y i ⁻¹' t i) ≠ 0) →
        (∀ (i : ι), MeasurableSet (t i)) → ProbabilityTheory.iIndepFun X μ[|⋂ i, Y i ⁻¹' t i]
-- Mathlib.Data.Nat.Cast.Prod
Prod.fst_ofNat : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoidWithOne α] [inst_1 : AddMonoidWithOne β] (n : ℕ)
  [inst_2 : n.AtLeastTwo], (OfNat.ofNat n).1 = OfNat.ofNat n
-- Init.Data.List.Lemmas
List.set_comm : ∀ {α : Type u_1} (a b : α) {i j : ℕ} {l : List α}, i ≠ j → (l.set i a).set j b = (l.set j b).set i a
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.forgetToPresheafModuleCatObj_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat} (X : Cᵒᵖ)
  (hX : CategoryTheory.Limits.IsInitial X) (M : PresheafOfModules R) (Y : Cᵒᵖ),
  (PresheafOfModules.forgetToPresheafModuleCatObj X hX M).obj Y =
    PresheafOfModules.forgetToPresheafModuleCatObjObj X hX M Y
-- Mathlib.Analysis.Asymptotics.Defs
/-- **Alias** of the forward direction of `Asymptotics.isBigO_norm_left`. -/
Asymptotics.IsBigO.of_norm_left : ∀ {α : Type u_1} {F : Type u_4} {E' : Type u_6} [inst : Norm F] [inst_1 : SeminormedAddCommGroup E'] {g : α → F}
  {f' : α → E'} {l : Filter α}, (fun x => ‖f' x‖) =O[l] g → f' =O[l] g
-- Mathlib.Data.Nat.Init
Nat.leRecOn_succ : ∀ {C : ℕ → Sort u_1} {n m : ℕ} (h1 : n ≤ m) {h2 : n ≤ m + 1} {next : {k : ℕ} → C k → C (k + 1)} (x : C n),
  Nat.leRecOn h2 next x = next (Nat.leRecOn h1 (fun {k} => next) x)
-- Mathlib.Data.Set.Lattice
Set.ofPred_forall : ∀ {β : Type u_2} {ι : Sort u_5} (p : ι → β → Prop), {x | ∀ (i : ι), p i x} = ⋂ i, {x | p i x}
-- Init.Data.Nat.Fold
Nat.any_congr : ∀ {n m : ℕ} (w : n = m) (f : (i : ℕ) → i < n → Bool), n.any f = m.any fun i h => f i ⋯
-- Mathlib.Algebra.BigOperators.RingEquiv
RingEquiv.map_prod : ∀ {α : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] (g : R ≃+* S)
  (f : α → R) (s : Finset α), g (∏ x ∈ s, f x) = ∏ x ∈ s, g (f x)
-- Init.Data.Nat.ToString
Nat.ofDigitChars_eq_foldl : ∀ {b : ℕ} {l : List Char} {init : ℕ},
  b.ofDigitChars l init = List.foldl (fun sofar c => b * sofar + (c.toNat - '0'.toNat)) init l
-- Mathlib.Algebra.Polynomial.Bivariate
Polynomial.Bivariate.aveal_eq_map_swap : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] (x : A)
  (p : Polynomial (Polynomial R)),
  (Polynomial.aeval (Polynomial.C x)) p = (Polynomial.mapAlgHom (Polynomial.aeval x)) (Polynomial.Bivariate.swap p)
-- Mathlib.Order.CompleteLatticeIntervals
Set.Iic.instCompleteLattice : {α : Type u_2} → [inst : CompleteLattice α] → {a : α} → CompleteLattice ↑(Set.Iic a)
-- Mathlib.AlgebraicGeometry.Gluing
/-- The glue data associated with an open cover.
The canonical isomorphism `𝒰.gluedCover.glued ⟶ X` is provided by `𝒰.fromGlued`.  -/
AlgebraicGeometry.Scheme.Cover.gluedCover : {X : AlgebraicGeometry.Scheme} → X.OpenCover → AlgebraicGeometry.Scheme.GlueData
-- Mathlib.RingTheory.DedekindDomain.Different
Submodule.traceDual_bot : ∀ {A : Type u_1} {K : Type u_2} {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L], Submodule.traceDual A K ⊥ = ⊤
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.instCoeTCContinuousLinearMap : {R : Type u_1} →
  {R₂ : Type u_2} →
    {E : Type u_5} →
      {E₂ : Type u_6} →
        [inst : Semiring R] →
          [inst_1 : Semiring R₂] →
            {σ₁₂ : R →+* R₂} →
              {σ₂₁ : R₂ →+* R} →
                [inst_2 : RingHomInvPair σ₁₂ σ₂₁] →
                  [inst_3 : RingHomInvPair σ₂₁ σ₁₂] →
                    [inst_4 : SeminormedAddCommGroup E] →
                      [inst_5 : SeminormedAddCommGroup E₂] →
                        [inst_6 : Module R E] → [inst_7 : Module R₂ E₂] → CoeTC (E ≃ₛₗᵢ[σ₁₂] E₂) (E →SL[σ₁₂] E₂)
-- Mathlib.Order.PropInstances
Prop.bot_eq_false : ⊥ = False
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.SimpKind.simpAll : Lean.Elab.Tactic.SimpKind
-- Mathlib.NumberTheory.Height.NumberField
NumberField.instNorthcottRealMulHeight₁ : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K], Northcott Height.mulHeight₁
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_empty : ∀ {α : Type u} {β : α → Type v}, Std.DTreeMap.Internal.Impl.empty.size = 0
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
CategoryTheory.Limits.CofanTypes.sigma_ι_snd : ∀ {C : Type u} (F : C → Type v) (x : CategoryTheory.Discrete C) (x_1 : (CategoryTheory.Discrete.functor F).obj x),
  ((CategoryTheory.Limits.CofanTypes.sigma F).ι x x_1).snd = x_1
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mrangeRestrict_mker : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N),
  AddMonoidHom.mker f.mrangeRestrict = AddMonoidHom.mker f
-- Mathlib.Algebra.Order.IsBotOne
isBot_one : ∀ {α : Type u_1} [inst : LE α] [inst_1 : One α] [IsBotOneClass α], IsBot 1
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Oplax right unity.  -/
CategoryTheory.OplaxFunctor.map₂_rightUnitor_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] (self : CategoryTheory.OplaxFunctor B CategoryTheory.Cat)
  {a b : B} (f : a ⟶ b) (X : ↑(self.obj a)),
  (self.map₂ (CategoryTheory.Bicategory.rightUnitor f).hom).toNatTrans.app X =
    CategoryTheory.CategoryStruct.comp ((self.mapComp f (CategoryTheory.CategoryStruct.id b)).toNatTrans.app X)
      ((self.mapId b).toNatTrans.app ((self.map f).toFunctor.obj X))
-- Std.Data.ExtTreeMap.Basic
/-- Tries to retrieve the smallest key that is greater than the given key,
panicking if no such key exists.
 -/
Std.ExtTreeMap.getKeyGT! : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → [Std.TransCmp cmp] → [Inhabited α] → Std.ExtTreeMap α β cmp → α → α
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMon_obj_X : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.LaxBraided] (A : CategoryTheory.CommMon C),
  (F.mapCommMon.obj A).X = F.obj A.X
-- Lean.Elab.PreDefinition.Structural.BRecOn
/-- `below` is a free variable with type of the form `I.below indParams motive indices major`,
where `I` is the name of an inductive datatype.

For example, when trying to show that the following function terminates using structural recursion
```lean
def addAdjacent : List Nat → List Nat
| []       => []
| [a]      => [a]
| a::b::as => (a+b) :: addAdjacent as
```
when we are visiting `addAdjacent as` at `replaceRecApps`, `below` has type
`@List.below Nat (fun (x : List Nat) => List Nat) (a::b::as)`
The motive `fun (x : List Nat) => List Nat` depends on the actual function we are trying to compute.
So, we first replace it with a fresh variable `C` at `withBelowDict`.
Recall that `brecOn` implements course-of-values recursion, and `below` can be viewed as a dictionary
of the "previous values".
We search this dictionary using the auxiliary function `toBelowAux`.
The dictionary is built using the `PProd` (`And` for inductive predicates).
We keep searching it until we find `C recArg`, where `C` is the auxiliary fresh variable created at `withBelowDict`.   -/
Lean.Elab.Structural.toBelow : Lean.Expr → ℕ → Lean.Elab.Structural.Positions → ℕ → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
Set.powersetCard.permOfDisjoint.congr_simp : ∀ {m n : ℕ} {I : Type u_2} [inst : LinearOrder I] {s s_1 : ↑(Set.powersetCard I m)} (e_s : s = s_1)
  {t t_1 : ↑(Set.powersetCard I n)} (e_t : t = t_1) (h : Disjoint ↑s ↑t),
  Set.powersetCard.permOfDisjoint h = Set.powersetCard.permOfDisjoint ⋯
-- Init.Data.List.Find
/-- Indexing a list at the position `idxOf x` recovers `x`, provided `x` occurs
in the list.  -/
List.getElem_idxOf : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {x : α} {xs : List α} (h : List.idxOf x xs < xs.length),
  xs[List.idxOf x xs] = x
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_eraseKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α},
  Std.Internal.List.DistinctKeys l →
    Std.Internal.List.getKey? a (Std.Internal.List.eraseKey k l) =
      if (k == a) = true then none else Std.Internal.List.getKey? a l
-- Mathlib.Data.Set.UnionLift
Set.liftCover_coe : ∀ {α : Type u_1} {ι : Sort u_3} {β : Sort u_2} {S : ι → Set α} {f : (i : ι) → ↑(S i) → β}
  {hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩} {hS : Set.iUnion S = Set.univ}
  {i : ι} (x : ↑(S i)), Set.liftCover S f hf hS ↑x = f i x
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Complex.sin_add_pi : ∀ (x : ℂ), Complex.sin (x + ↑Real.pi) = -Complex.sin x
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- If all the elements of a set `s` commute, then `closure s` is a non-unital commutative
semiring.  -/
NonUnitalSubsemiring.isMulCommutative_closure : ∀ {R : Type u_1} [inst : NonUnitalSemiring R] {s : Set R},
  (∀ x ∈ s, ∀ y ∈ s, x * y = y * x) → IsMulCommutative ↥(NonUnitalSubsemiring.closure s)
-- Mathlib.NumberTheory.Zsqrtd.Basic
_private.Mathlib.NumberTheory.Zsqrtd.Basic.0.Zsqrtd.Nonneg.match_1.eq_1 : ∀ {d : ℕ} (motive : ℤ√↑d → Sort u_1) (a b : ℤ) (h_1 : (a b : ℤ) → motive { re := a, im := b }),
  (match { re := a, im := b } with
    | { re := a, im := b } => h_1 a b) =
    h_1 a b
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.filter.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α]
  (f f_1 : α → β → Bool),
  f = f_1 → ∀ (m m_1 : Std.ExtHashMap α β), m = m_1 → Std.ExtHashMap.filter f m = Std.ExtHashMap.filter f_1 m_1
-- Lean.Meta.Sym.Canon
_private.Lean.Meta.Sym.Canon.0.Lean.Meta.Sym.Canon.canon.canonMatch : Lean.Expr → Lean.Meta.Sym.Canon.CanonM✝ Lean.Expr
-- Init.Guard
/-- Tactic to check equality of two expressions.
* `guard_expr e = e'` checks that `e` and `e'` are defeq at reducible transparency.
* `guard_expr e =~ e'` checks that `e` and `e'` are defeq at default transparency.
* `guard_expr e =ₛ e'` checks that `e` and `e'` are syntactically equal.
* `guard_expr e =ₐ e'` checks that `e` and `e'` are alpha-equivalent.

Both `e` and `e'` are elaborated then have their metavariables instantiated before the equality
check. Their types are unified (using `isDefEqGuarded`) before synthetic metavariables are
processed, which helps with default instance handling.
 -/
Lean.Parser.Tactic.guardExpr : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Notation
/-- The type of normal ordinal notations.

It would have been nicer to define this right in the inductive type, but `NF o` requires `repr`
which requires `ONote`, so all these things would have to be defined at once, which messes up the VM
representation.  -/
NONote : Type
-- Mathlib.Analysis.SpecialFunctions.Artanh
Real.artanh_nonpos : ∀ {x : ℝ}, x ≤ 0 → Real.artanh x ≤ 0
-- Lean.Data.Lsp.Internal
Lean.Lsp.instToJsonLeanILeanHeaderSetupInfoParams : Lean.ToJson Lean.Lsp.LeanILeanHeaderSetupInfoParams
-- Mathlib.Data.List.Pairwise
List.Pairwise.rel_head_of_rel_head_head : ∀ {α : Type u_1} {R : α → α → Prop} {l : List α} {a : α},
  List.Pairwise R l → ∀ (ha : a ∈ l), R (l.head ⋯) (l.head ⋯) → R (l.head ⋯) a
-- Mathlib.Analysis.Normed.Group.Basic
abs_norm' : ∀ {E : Type u_5} [inst : SeminormedGroup E] (z : E), |‖z‖| = ‖z‖
-- Mathlib.Algebra.Homology.ShortComplex.LeftHomology
CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork_f' : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  (S : CategoryTheory.ShortComplex C) (hf : S.f = 0) (c : CategoryTheory.Limits.KernelFork S.g)
  (hc : CategoryTheory.Limits.IsLimit c),
  (CategoryTheory.ShortComplex.LeftHomologyData.ofIsLimitKernelFork S hf c hc).f' = 0
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.instAdditiveRestrictScalars : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] (f : R →+* S), (ModuleCat.restrictScalars f).Additive
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The additive subsemigroup `M` of the magma `M`.  -/
AddSubsemigroup.instTop : {M : Type u_1} → [inst : Add M] → Top (AddSubsemigroup M)
-- Mathlib.Algebra.GroupWithZero.Hom
/-- Turn an element of a type `F` satisfying `MonoidWithZeroHomClass F α β` into an actual
`MonoidWithZeroHom`.  -/
MonoidWithZeroHom.ofClass : {F : Type u_1} →
  {α : Type u_2} →
    {β : Type u_3} →
      [inst : MulZeroOneClass α] →
        [inst_1 : MulZeroOneClass β] → [inst_2 : FunLike F α β] → [MonoidWithZeroHomClass F α β] → F → α →*₀ β
-- Mathlib.InformationTheory.Hamming
hammingNorm_smul_le_hammingNorm : ∀ {α : Type u_1} {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → Zero (β i)] [inst_3 : Zero α] [inst_4 : (i : ι) → SMulWithZero α (β i)] {k : α}
  {x : (i : ι) → β i}, hammingNorm (k • x) ≤ hammingNorm x
-- Mathlib.Algebra.Algebra.Tower
/-- A variant of `Submodule.span_image` for `algebraMap`.  -/
Submodule.span_algebraMap_image : ∀ {R : Type u} {S : Type v} [inst : CommSemiring R] [inst_1 : Semiring S] [inst_2 : Algebra R S] (a : Set R),
  Submodule.span R (⇑(algebraMap R S) '' a) = Submodule.map (Algebra.linearMap R S) (Submodule.span R a)
-- Mathlib.Data.ZMod.Basic
ZMod.cast.eq_1 : ∀ {R : Type u_1} [inst : AddGroupWithOne R], ZMod.cast = Int.cast
-- Mathlib.CategoryTheory.Limits.FinallySmall
CategoryTheory.FinallySmall.mk : ∀ {J : Type u} [inst : CategoryTheory.Category.{v, u} J], (∃ S x F, F.Final) → CategoryTheory.FinallySmall J