mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Sites.MorphismProperty
CategoryTheory.MorphismProperty.ofArrows_mem_precoverage : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P : CategoryTheory.MorphismProperty C} {X : C}
  {ι : Type u_2} {Y : ι → C} {f : (i : ι) → Y i ⟶ X},
  CategoryTheory.Presieve.ofArrows Y f ∈ P.precoverage.coverings X ↔ ∀ (i : ι), P (f i)
-- Mathlib.Order.CompleteLattice.PiLex
_private.Mathlib.Order.CompleteLattice.PiLex.0.Pi.Lex.inf.eq_def : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → CompleteLinearOrder (α i)]
  [inst_2 : WellFoundedLT ι] (s : Set (Lex ((i : ι) → (fun i => α i) i))) (i : ι), Pi.Lex.inf✝ s i = ⨅ e, ↑e i
-- Mathlib.Topology.Algebra.Support
LocallyFinite.smul_left : ∀ {X : Type u_1} {M : Type u_7} {R : Type u_8} {ι : Type u_9} [inst : TopologicalSpace X] [inst_1 : Zero R]
  [inst_2 : Zero M] [inst_3 : SMulWithZero R M] {s : ι → X → R},
  (LocallyFinite fun i => Function.support (s i)) →
    ∀ (f : ι → X → M), LocallyFinite fun i => Function.support (s i • f i)
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.sInf_toSubsemigroup : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] (s : Set (NonUnitalSubring R)),
  (sInf s).toSubsemigroup = ⨅ t ∈ s, t.toSubsemigroup
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.below.add_left : ∀ {R : Type uR} [inst : Semiring R] {r : R → R → Prop} {motive : (a a_1 : R) → RingQuot.Rel r a a_1 → Prop} ⦃a b c : R⦄
  (a_1 : RingQuot.Rel r a b), RingQuot.Rel.below a_1 → motive a b a_1 → RingQuot.Rel.below ⋯
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.leadingCoeff_div : ∀ {R : Type u} [inst : Field R] {p q : Polynomial R},
  q.degree ≤ p.degree → (p / q).leadingCoeff = p.leadingCoeff / q.leadingCoeff
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.integrableOn_singleton_iff : ∀ {α : Type u_1} {ε' : Type u_4} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace ε']
  [inst_1 : ESeminormedAddMonoid ε'] {f : α → ε'} {x : α} [MeasurableSingletonClass α],
  autoParam (‖f x‖ₑ ≠ ⊤) MeasureTheory.integrableOn_singleton_iff._auto_1 →
    (MeasureTheory.IntegrableOn f {x} μ ↔ ‖f x‖ₑ = 0 ∨ μ {x} < ⊤)
-- Mathlib.LinearAlgebra.Matrix.Nondegenerate
Matrix.separatingLeft_transpose_iff : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_3} [inst : CommSemiring R] {M : Matrix m n R} [inst_1 : Finite m]
  [inst_2 : Finite n], M.transpose.SeparatingLeft ↔ M.SeparatingRight
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.cocycles₂_ext : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u_1, u, u} k G}
  {f₁ f₂ : ↥(groupCohomology.cocycles₂ A)}, (∀ (g h : G), f₁ (g, h) = f₂ (g, h)) → f₁ = f₂
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.im_sqrtd : ∀ {d : ℤ}, Zsqrtd.sqrtd.im = 1
-- Lean.Server.Rpc.Basic
Lean.Lsp.RpcRef.p : Lean.Lsp.RpcRef → USize
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Cofork.IsColimit.π_desc_assoc : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  {s t : CategoryTheory.Limits.Cofork f g} (hs : CategoryTheory.Limits.IsColimit s) {Z : C} (h : t.pt ⟶ Z),
  CategoryTheory.CategoryStruct.comp s.π (CategoryTheory.CategoryStruct.comp (hs.desc t) h) =
    CategoryTheory.CategoryStruct.comp t.π h
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentColorParams.mk.sizeOf_spec : ∀ (toWorkDoneProgressParams : Lean.Lsp.WorkDoneProgressParams) (toPartialResultParams : Lean.Lsp.PartialResultParams)
  (textDocument : Lean.Lsp.TextDocumentIdentifier),
  sizeOf
      { toWorkDoneProgressParams := toWorkDoneProgressParams, toPartialResultParams := toPartialResultParams,
        textDocument := textDocument } =
    1 + sizeOf toWorkDoneProgressParams + sizeOf toPartialResultParams + sizeOf textDocument
-- Mathlib.AlgebraicGeometry.Morphisms.UniversallyOpen
AlgebraicGeometry.Scheme.Hom.isOpenMap : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.UniversallyOpen f], IsOpenMap ⇑f
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.mk_iUnion_le_lift : ∀ {α : Type u} {ι : Type v} (f : ι → Set α),
  Cardinal.lift.{v, u} (Cardinal.mk ↑(⋃ i, f i)) ≤
    Cardinal.lift.{u, v} (Cardinal.mk ι) * ⨆ i, Cardinal.lift.{v, u} (Cardinal.mk ↑(f i))
-- Mathlib.Algebra.Group.Prod
Prod.instLeftCancelSemigroup.eq_1 : ∀ {G : Type u_1} {H : Type u_2} [inst : LeftCancelSemigroup G] [inst_1 : LeftCancelSemigroup H],
  Prod.instLeftCancelSemigroup = { toSemigroup := Prod.instSemigroup, toIsLeftCancelMul := ⋯ }
-- Mathlib.Topology.Compactness.Compact
Filter.mem_cocompact' : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s ∈ Filter.cocompact X ↔ ∃ t, IsCompact t ∧ sᶜ ⊆ t
-- Mathlib.CategoryTheory.Monoidal.Cartesian.ShrinkYoneda
CategoryTheory.shrinkYonedaGrp_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C]
  [inst_2 : CategoryTheory.CartesianMonoidalCategory C] {X Y : CategoryTheory.Grp C} (f : X ⟶ Y),
  CategoryTheory.shrinkYonedaGrp.{w, v, u}.map f = GrpCat.shrinkFunctorMap (CategoryTheory.yonedaGrp.map f)
-- Mathlib.Analysis.InnerProductSpace.Projection.Basic
/-- **Alias** of `Submodule.orthogonalProjectionOnto_norm_le`.

---

The orthogonal projection has norm `≤ 1`.  -/
Submodule.orthogonalProjection_norm_le : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (K : Submodule 𝕜 E) [inst_3 : K.HasOrthogonalProjection], ‖K.orthogonalProjectionOnto‖ ≤ 1
-- Mathlib.Data.Countable.Defs
instCountableULift : ∀ {β : Type v} [Countable β], Countable (ULift.{u, v} β)
-- Mathlib.Order.SuccPred.Limit
SuccOrder.prelimitRecOn.eq_1 : ∀ {α : Type u_1} (b : α) {motive : α → Sort u_2} [inst : PartialOrder α] [inst_1 : SuccOrder α]
  [inst_2 : WellFoundedLT α] (succ : (a : α) → ¬IsMax a → motive a → motive (Order.succ a))
  (isSuccPrelimit : (a : α) → Order.IsSuccPrelimit a → ((b : α) → b < a → motive b) → motive a),
  SuccOrder.prelimitRecOn b succ isSuccPrelimit =
    ⋯.fix
      (fun a IH =>
        if h : Order.IsSuccPrelimit a then isSuccPrelimit a h IH
        else cast ⋯ (succ (Classical.choose ⋯) ⋯ (IH (Classical.choose ⋯) ⋯)))
      b
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_diff : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β},
  Std.ExtDHashMap.Const.getD (m₁ \ m₂) k fallback =
    if k ∈ m₂ then fallback else Std.ExtDHashMap.Const.getD m₁ k fallback
-- Mathlib.Probability.Decision.BayesEstimator
ProbabilityTheory.lintegral_iInf_posterior_le_bayesRisk : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_3} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} {ℓ : Θ → 𝓨 → ENNReal} [inst : StandardBorelSpace Θ] [inst_1 : Nonempty Θ],
  Measurable (Function.uncurry ℓ) →
    ∀ (P : ProbabilityTheory.Kernel Θ 𝓧) [inst_2 : ProbabilityTheory.IsFiniteKernel P] (π : MeasureTheory.Measure Θ)
      [inst_3 : MeasureTheory.IsFiniteMeasure π],
      ∫⁻ (x : 𝓧), ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(ProbabilityTheory.posterior P π) x ∂π.bind ⇑P ≤
        ProbabilityTheory.bayesRisk ℓ P π
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.Equiv.instTrans : {α : Type u} → {β : Type v} → Trans Std.HashMap.Raw.Equiv Std.HashMap.Raw.Equiv Std.HashMap.Raw.Equiv
-- Init.Data.Array.Attach
Array.pmap_eq_empty_iff : ∀ {α : Type u_1} {β : Type u_2} {p : α → Prop} {f : (a : α) → p a → β} {xs : Array α} {H : ∀ a ∈ xs, p a},
  Array.pmap f xs H = #[] ↔ xs = #[]
-- Mathlib.Data.PNat.Factors
instOrderBotPrimeMultiset : OrderBot PrimeMultiset
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unique
ContinuousMapZero.toNNReal_mul_add_neg_mul_add_mul_neg_eq : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : Zero X] (f g : ContinuousMapZero X ℝ),
  (f * g).toNNReal + (-f).toNNReal * g.toNNReal + f.toNNReal * (-g).toNNReal =
    (-(f * g)).toNNReal + f.toNNReal * g.toNNReal + (-f).toNNReal * (-g).toNNReal
-- Mathlib.RingTheory.NormalClosure
/-- This is a local instance since it is only used in this file to construct `Ring.NormalClosure`.
 -/
Ring.instAlgebraSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : IsDomain R] →
          [inst_3 : IsDomain S] →
            [inst_4 : Algebra R S] →
              [inst_5 : Module.IsTorsionFree R S] →
                Algebra S
                  ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S)
                      (AlgebraicClosure (FractionRing S)))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Equiv.isEmpty_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → m₁.Equiv m₂ → m₁.isEmpty = m₂.isEmpty
-- Lean.Elab.Command.Scope
Lean.Elab.Command.Scope.mk.sizeOf_spec : ∀ (header : String) (opts : Lean.Options) (currNamespace : Lean.Name) (openDecls : List Lean.OpenDecl)
  (levelNames : List Lean.Name) (varDecls : Array (Lean.TSyntax `Lean.Parser.Term.bracketedBinder))
  (varUIds : Array Lean.Name) (includedVars omittedVars : List Lean.Name) (isNoncomputable isPublic isMeta : Bool)
  (attrs : List (Lean.TSyntax `Lean.Parser.Term.attrInstance)),
  sizeOf
      { header := header, opts := opts, currNamespace := currNamespace, openDecls := openDecls,
        levelNames := levelNames, varDecls := varDecls, varUIds := varUIds, includedVars := includedVars,
        omittedVars := omittedVars, isNoncomputable := isNoncomputable, isPublic := isPublic, isMeta := isMeta,
        attrs := attrs } =
    1 + sizeOf header + sizeOf opts + sizeOf currNamespace + sizeOf openDecls + sizeOf levelNames + sizeOf varDecls +
                  sizeOf varUIds +
                sizeOf includedVars +
              sizeOf omittedVars +
            sizeOf isNoncomputable +
          sizeOf isPublic +
        sizeOf isMeta +
      sizeOf attrs
-- Mathlib.Order.SuccPred.Basic
Order.le_succ_bot_iff : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] {a : α} [inst_2 : OrderBot α],
  a ≤ Order.succ ⊥ ↔ a = ⊥ ∨ a = Order.succ ⊥
-- Mathlib.Algebra.Order.Hom.MonoidWithZero
/-- Copy of an `OrderMonoidWithZeroHom` with a new `toFun` equal to the old one. Useful to fix
definitional equalities.  -/
OrderMonoidWithZeroHom.copy : {α : Type u_2} →
  {β : Type u_3} →
    [inst : Preorder α] →
      [inst_1 : Preorder β] →
        [inst_2 : MulZeroOneClass α] → [inst_3 : MulZeroOneClass β] → (f : α →*₀o β) → (f' : α → β) → f' = ⇑f → α →*o β
-- Mathlib.CategoryTheory.Sites.Point.Basic
CategoryTheory.GrothendieckTopology.Point.presheafFiber_map_shrinkYoneda_map_shrinkYonedaCompPresheafFiberIso_inv_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} (Φ : J.Point)
  [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X Y : C} (f : X ⟶ Y) (x : Φ.fiber.obj X),
  (CategoryTheory.ConcreteCategory.hom (Φ.presheafFiber.map (CategoryTheory.shrinkYoneda.{w, v, u}.map f)))
      ((CategoryTheory.ConcreteCategory.hom (Φ.shrinkYonedaCompPresheafFiberIso.inv.app X)) x) =
    (CategoryTheory.ConcreteCategory.hom (Φ.toPresheafFiber X x (CategoryTheory.shrinkYoneda.{w, v, u}.obj Y)))
      (CategoryTheory.shrinkYonedaObjObjEquiv.symm f)
-- Init.Prelude
Nat.div.go : (y : ℕ) → 0 < y → (fuel x : ℕ) → x < fuel → ℕ
-- Mathlib.Tactic.Choose
/-- * `choose a b h h' using hyp` takes a hypothesis `hyp` of the form
  `∀ (x : X) (y : Y), ∃ (a : A) (b : B), P x y a b ∧ Q x y a b`
  for some `P Q : X → Y → A → B → Prop` and outputs
  into context a function `a : X → Y → A`, `b : X → Y → B` and two assumptions:
  `h : ∀ (x : X) (y : Y), P x y (a x y) (b x y)` and
  `h' : ∀ (x : X) (y : Y), Q x y (a x y) (b x y)`. It also works with dependent versions.

* `choose! a b h h' using hyp` does the same, except that it will remove dependency of
  the functions on propositional arguments if possible. For example if `Y` is a proposition
  and `A` and `B` are nonempty in the above example then we will instead get
  `a : X → A`, `b : X → B`, and the assumptions
  `h : ∀ (x : X) (y : Y), P x y (a x) (b x)` and
  `h' : ∀ (x : X) (y : Y), Q x y (a x) (b x)`.

The `using hyp` part can be omitted,
which will effectively cause `choose` to start with an `intro hyp`.

Like `intro`, the `choose` tactic supports type annotations to specify the expected type
of the introduced variables. This is useful for documentation and for catching mistakes early:
```
example (h : ∃ n : ℕ, n > 0) : True := by
  choose (n : ℕ) (hn : n > 0) using h
  trivial
```
If the provided type does not match the actual type, an error is raised.

Examples:

```
example (h : ∀ n m : ℕ, ∃ i j, m = n + i ∨ m + j = n) : True := by
  choose i j h using h
  guard_hyp i : ℕ → ℕ → ℕ
  guard_hyp j : ℕ → ℕ → ℕ
  guard_hyp h : ∀ (n m : ℕ), m = n + i n m ∨ m + j n m = n
  trivial
```

```
example (h : ∀ i : ℕ, i < 7 → ∃ j, i < j ∧ j < i+i) : True := by
  choose! f h h' using h
  guard_hyp f : ℕ → ℕ
  guard_hyp h : ∀ (i : ℕ), i < 7 → i < f i
  guard_hyp h' : ∀ (i : ℕ), i < 7 → f i < i + i
  trivial
```
 -/
Mathlib.Tactic.Choose.choose : Lean.ParserDescr
-- Mathlib.MeasureTheory.Group.AddCircle
AddCircle.volume_of_add_preimage_eq : ∀ {T : ℝ} [hT : Fact (0 < T)] (s I : Set (AddCircle T)) (u x : AddCircle T),
  IsOfFinAddOrder u →
    u +ᵥ s =ᵐ[MeasureTheory.volume] s →
      I =ᵐ[MeasureTheory.volume] Metric.ball x (T / (2 * ↑(addOrderOf u))) →
        MeasureTheory.volume s = addOrderOf u • MeasureTheory.volume (s ∩ I)
-- Mathlib.Algebra.Order.Group.Synonym
Lex.instSub.eq_1 : ∀ {α : Type u_1} [inst : Sub α], Lex.instSub = inst
-- Mathlib.Analysis.Normed.Algebra.Exponential
NormedSpace.exp_zero : ∀ {𝔸 : Type u_2} [inst : Ring 𝔸] [inst_1 : TopologicalSpace 𝔸] [inst_2 : IsTopologicalRing 𝔸], NormedSpace.exp 0 = 1
-- Mathlib.Combinatorics.SimpleGraph.Acyclic
SimpleGraph.IsAcyclic.of_comap : ∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} (f : V' ↪ V), G.IsAcyclic → (SimpleGraph.comap (⇑f) G).IsAcyclic
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get_insertMany_empty_list_of_mem : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} [Std.TransOrd α] {l : List (α × β)} {k k' : α},
  compare k k' = Ordering.eq →
    ∀ {v : β},
      List.Pairwise (fun a b => ¬compare a.1 b.1 = Ordering.eq) l →
        (k, v) ∈ l →
          ∀
            {h :
              Std.DTreeMap.Internal.Impl.contains k'
                  ↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯) =
                true},
            Std.DTreeMap.Internal.Impl.Const.get
                (↑(Std.DTreeMap.Internal.Impl.Const.insertMany Std.DTreeMap.Internal.Impl.empty l ⋯)) k' h =
              v
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.zipWithM'.match_1.eq_1 : ∀ {α : Type u_1} {β : Type u_2} (motive : List α → List β → Sort u_3) (x : α) (xs : List α) (y : β) (ys : List β)
  (h_1 : (x : α) → (xs : List α) → (y : β) → (ys : List β) → motive (x :: xs) (y :: ys))
  (h_2 : (x : List α) → (x_1 : List β) → motive x x_1),
  (match x :: xs, y :: ys with
    | x :: xs, y :: ys => h_1 x xs y ys
    | x, x_1 => h_2 x x_1) =
    h_1 x xs y ys
-- Mathlib.InformationTheory.Hamming
/-- Corresponds to `norm_eq_zero`.  -/
hammingNorm_eq_zero : ∀ {ι : Type u_2} {β : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → DecidableEq (β i)]
  [inst_2 : (i : ι) → Zero (β i)] {x : (i : ι) → β i}, hammingNorm x = 0 ↔ x = 0
-- Mathlib.LinearAlgebra.FreeProduct.Basic
/-- `lof R A i 1 = 1` for all `i`.  -/
LinearAlgebra.FreeProduct.lof_map_one : ∀ {I : Type u} [inst : DecidableEq I] (R : Type v) [inst_1 : CommSemiring R] (A : I → Type w)
  [inst_2 : (i : I) → Semiring (A i)] [inst_3 : (i : I) → Algebra R (A i)] (i : I),
  (LinearAlgebra.FreeProduct.lof R A i) 1 = 1
-- Mathlib.Algebra.GCDMonoid.Multiset
Multiset.gcd_cons : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : NormalizedGCDMonoid α] (a : α) (s : Multiset α),
  (a ::ₘ s).gcd = gcd a s.gcd
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.get!_erase_self : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α], (↑m).WF → ∀ {k : α} [inst_3 : Inhabited (β k)], (m.erase k).get! k = default
-- Mathlib.Topology.Algebra.IsUniformGroup.Defs
uniformContinuous_const_zsmul : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : AddGroup α] [IsUniformAddGroup α] (n : ℤ),
  UniformContinuous fun x => n • x
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.rnDeriv_self : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ : ProbabilityTheory.Kernel α γ)
  [ProbabilityTheory.IsFiniteKernel κ] (a : α), κ.rnDeriv κ a =ᵐ[κ a] 1
-- Mathlib.Computability.PartrecCode
_private.Mathlib.Computability.PartrecCode.0.Nat.Partrec.Code.ofNatCode.match_3.splitter : (motive : ℕ → Sort u_1) →
  (x : ℕ) →
    (Unit → motive 0) →
      (Unit → motive 1) → (Unit → motive 2) → (Unit → motive 3) → ((n : ℕ) → motive n.succ.succ.succ.succ) → motive x
-- Mathlib.Order.Interval.Set.Fin
Fin.image_rev : ∀ {n : ℕ} (s : Set (Fin n)), Fin.rev '' s = Fin.rev ⁻¹' s
-- Mathlib.CategoryTheory.Noetherian
/-- A category is Artinian if it is essentially small and all objects are Artinian.  -/
CategoryTheory.Artinian : (C : Type u_1) → [CategoryTheory.Category.{v_1, u_1} C] → Prop
-- Mathlib.LinearAlgebra.Ray
instNonemptyRayOfNontrivial : ∀ {R : Type u_1} [inst : CommSemiring R] [inst_1 : PartialOrder R] [inst_2 : IsStrictOrderedRing R] {M : Type u_2}
  [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [Nontrivial M], Nonempty (Module.Ray R M)
-- Mathlib.Topology.ContinuousOn
Topology.IsEmbedding.continuousOn_iff : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : TopologicalSpace γ] {f : α → β} {g : β → γ},
  Topology.IsEmbedding g → ∀ {s : Set α}, ContinuousOn f s ↔ ContinuousOn (g ∘ f) s
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Code.action.injEq : ∀ (action action_1 : Lean.Syntax),
  (Lean.Elab.Term.Do.Code.action action = Lean.Elab.Term.Do.Code.action action_1) = (action = action_1)
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- **Alias** of `MonoidHom.pi_injective`. -/
Pi.monoidHom_injective : ∀ {I : Type u} {f : I → Type v} [inst : (i : I) → MulOneClass (f i)] {γ : Type w} [Nonempty I] [inst_2 : MulOneClass γ]
  (g : (i : I) → γ →* f i), (∀ (i : I), Function.Injective ⇑(g i)) → Function.Injective ⇑(MonoidHom.pi g)
-- Mathlib.LinearAlgebra.Matrix.Swap
Matrix.transpose_swap : ∀ {R : Type u_1} {n : Type u_2} [inst : Zero R] [inst_1 : One R] [inst_2 : DecidableEq n] (i j : n),
  (Matrix.swap R i j).transpose = Matrix.swap R i j
-- Init.Data.Order.PackageFactories
Std.Packages.PartialOrderOfLEArgs.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (toPreorderOfLEArgs : Std.Packages.PreorderOfLEArgs α)
  (le_antisymm :
    autoParam
      (let this := toPreorderOfLEArgs.le;
      ∀ (a b : α), a ≤ b → b ≤ a → a = b)
      Std.Packages.PartialOrderOfLEArgs.le_antisymm._autoParam),
  sizeOf { toPreorderOfLEArgs := toPreorderOfLEArgs, le_antisymm := le_antisymm } = 1 + sizeOf toPreorderOfLEArgs
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
/-- While `RingHomSurjective σ₂₃` is not a strict requirement, there are obstructions to
this without any assumption on `σ₂₃` (in particular, on the dimension of the extension of `𝕜₃` over
`σ₂₃(𝕜₂)`), and in the only common case, which is when `σ₂₃` is conjugation, this type class is
guaranteed. Likewise, it would suffice if `RingHomIsometric` were replaced with the weaker
`Continuous σ₂₃`, but we opt for this because we have these type classes available.  -/
ContinuousLinearMapWOT.continuous_postcomp : ∀ {𝕜₁ : Type u_5} {𝕜₂ : Type u_6} {𝕜₃ : Type u_7} {E : Type u_9} {F : Type u_10} {G : Type u_11} [inst : NormedField 𝕜₁]
  [inst_1 : NormedField 𝕜₂] [inst_2 : NormedField 𝕜₃] {σ₁₂ : 𝕜₁ →+* 𝕜₂} {σ₁₃ : 𝕜₁ →+* 𝕜₃} {σ₂₃ : 𝕜₂ →+* 𝕜₃}
  [inst_3 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] [inst_4 : AddCommGroup E] [inst_5 : TopologicalSpace E]
  [inst_6 : Module 𝕜₁ E] [inst_7 : AddCommGroup F] [inst_8 : TopologicalSpace F] [inst_9 : Module 𝕜₂ F]
  [inst_10 : AddCommGroup G] [inst_11 : TopologicalSpace G] [inst_12 : Module 𝕜₃ G] [inst_13 : IsTopologicalAddGroup F]
  [inst_14 : ContinuousConstSMul 𝕜₂ F] [inst_15 : IsTopologicalAddGroup G] [inst_16 : ContinuousConstSMul 𝕜₃ G]
  [RingHomSurjective σ₂₃] [RingHomIsometric σ₂₃] (g : F →SWOT[σ₂₃] G), Continuous fun f => g.comp f
-- Mathlib.RingTheory.MvPolynomial.WeightedHomogeneous
MvPolynomial.weightedTotalDegree.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] {σ : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : SemilatticeSup M] [inst_3 : OrderBot M] (w : σ → M) (p : MvPolynomial σ R),
  MvPolynomial.weightedTotalDegree w p = p.support.sup fun s => (Finsupp.weight w) s
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Chebyshev.ChebyshevGauss
Polynomial.Chebyshev.sumZeroes_sum : ∀ (n : ℕ) {ι : Type u_1} (s : Finset ι) (P : ι → Polynomial ℝ),
  Polynomial.Chebyshev.sumZeroes n (∑ i ∈ s, P i) = ∑ i ∈ s, Polynomial.Chebyshev.sumZeroes n (P i)
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.fieldIdx.formatter : Lean.PrettyPrinter.Formatter
-- Mathlib.Analysis.Calculus.Deriv.Shift
derivWithin_comp_sub_const : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] (f : 𝕜 → F) (a : 𝕜) (s : Set 𝕜) (x : 𝕜),
  derivWithin (fun x => f (x - a)) s x = derivWithin f (-a +ᵥ s) (x - a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKeyD_le_minKeyD_erase! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k : α},
      (Std.DTreeMap.Internal.Impl.erase! k t).isEmpty = false →
        ∀ {fallback : α},
          (compare (t.minKeyD fallback) ((Std.DTreeMap.Internal.Impl.erase! k t).minKeyD fallback)).isLE = true
-- Mathlib.Algebra.Group.Subgroup.Ker
AddMonoidHom.mem_ker : ∀ {G : Type u_1} [inst : AddGroup G] {M : Type u_7} [inst_1 : AddZeroClass M] {f : G →+ M} {x : G}, x ∈ f.ker ↔ f x = 0
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.guard.sizeOf_spec : ∀ (e : Lean.Expr), sizeOf (Lean.Meta.Grind.EMatchTheoremConstraint.guard e) = 1 + sizeOf e
-- Mathlib.Data.Finset.Grade
Finset.covBy_insert : ∀ {α : Type u_1} {s : Finset α} {a : α} [inst : DecidableEq α], a ∉ s → s ⋖ insert a s
-- Mathlib.AlgebraicTopology.CechNerve
CategoryTheory.Arrow.augmentedCechNerve_hom_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f : CategoryTheory.Arrow C)
  [inst_1 : ∀ (n : ℕ), CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom]
  (x : SimplexCategoryᵒᵖ), f.augmentedCechNerve.hom.app x = CategoryTheory.Limits.WidePullback.base fun x => f.hom
-- Init.Coe
/-- Coerces a value of type `α` to type `β`. Accessible by the notation `↑x`,
or by double type ascription `((x : α) : β)`.  -/
CoeTail.coe : {α : semiOutParam (Sort u)} → {β : Sort v} → [self : CoeTail α β] → α → β
-- Mathlib.Data.Set.Card
Set.pred_ncard_le_ncard_sdiff_singleton : ∀ {α : Type u_1} (s : Set α) (a : α), s.ncard - 1 ≤ (s \ {a}).ncard
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k₁ k₂ : α} (h : (k₁ == k₂) = true) (h₁ : k₁ ∈ m), m.getKey k₁ h₁ = m.getKey k₂ ⋯
-- Init.Prelude
_private.Init.Prelude.0.noConfusion_of_Nat.aux : ∀ (a : ℕ), Bool.rec False True (a.beq a)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.mem_congr : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {a b : α}, (a == b) = true → (a ∈ m ↔ b ∈ m)
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBSet.find?_congr : ∀ {α : Type u_1} {cmp : α → α → Ordering} {v₁ v₂ : α} [Std.TransCmp cmp] (t : RBTree.RBSet α cmp),
  cmp v₁ v₂ = Ordering.eq → t.find? v₁ = t.find? v₂