mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.find?_toArray_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, Array.find? (fun x => cmp x.fst k == Ordering.eq) t.toArray = none ↔ t.contains k = false
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Bounds
Real.cos_le_one_div_sqrt_sq_add_one : ∀ {x : ℝ}, -(3 * Real.pi / 2) ≤ x → x ≤ 3 * Real.pi / 2 → Real.cos x ≤ 1 / √(x ^ 2 + 1)
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.instContainsZeroInverseImageOfIsClosedUnderIsomorphismsOfPreservesZeroMorphismsOfHasZeroObject : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  (P : CategoryTheory.ObjectProperty C) [P.ContainsZero] [P.IsClosedUnderIsomorphisms]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms D]
  (F : CategoryTheory.Functor D C) [F.PreservesZeroMorphisms] [CategoryTheory.Limits.HasZeroObject D],
  (P.inverseImage F).ContainsZero
-- Lean.Util.LeanOptions
Lean.instReprLeanOption : Repr Lean.LeanOption
-- Mathlib.Algebra.Star.UnitaryStarAlgAut
StarAlgEquiv.mk.congr_simp : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B]
  (toStarRingEquiv toStarRingEquiv_1 : A ≃⋆+* B) (e_toStarRingEquiv : toStarRingEquiv = toStarRingEquiv_1)
  (map_smul' : ∀ (r : R) (a : A), toStarRingEquiv.toFun (r • a) = r • toStarRingEquiv.toFun a),
  { toStarRingEquiv := toStarRingEquiv, map_smul' := map_smul' } =
    { toStarRingEquiv := toStarRingEquiv_1, map_smul' := ⋯ }
-- Std.Data.Iterators.Lemmas.Producers.Empty
Std.Iter.foldM_empty : ∀ {m : Type u_1 → Type u_2} {β : Type u_3} {γ : Type u_1} [inst : Monad m] [LawfulMonad m] {init : γ} {f : γ → β → m γ},
  Std.Iter.foldM f init (Std.Iter.empty β) = pure init
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.map_add : ∀ {R : Type u_1} {S : Type u_5} {M : Type u_8} {M₃ : Type u_11} [inst : Semiring R] [inst_1 : Semiring S]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module S M₃] {σ : R →+* S}
  (f : M →ₛₗ[σ] M₃) (x y : M), f (x + y) = f x + f y
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
/-- `Π i, A i` has the subset topology from the restricted product.  -/
RestrictedProduct.isEmbedding_structureMap : ∀ {ι : Type u_1} {R : ι → Type u_2} {A : (i : ι) → Set (R i)} {𝓕 : Filter ι} [inst : (i : ι) → TopologicalSpace (R i)],
  Topology.IsEmbedding (RestrictedProduct.structureMap R A 𝓕)
-- Lean.Util.PPExt
Lean.PPFns.ppGoal : Lean.PPFns → Lean.PPContext → Lean.MVarId → IO Std.Format
-- Mathlib.Combinatorics.SimpleGraph.Walk.Subwalks
SimpleGraph.Walk.isSubwalk_of_append_left : ∀ {V : Type u_1} {G : SimpleGraph V} {v w u : V} {p₁ : G.Walk v w} {p₂ : G.Walk w u} {p₃ : G.Walk v u},
  p₃ = p₁.append p₂ → p₁.IsSubwalk p₃
-- Mathlib.RingTheory.Adjoin.Field
AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly_symm_toAlgHom : ∀ (F : Type u_1) [inst : Field F] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra F R] (x : R),
  ↑(AlgEquiv.adjoinSingletonEquivAdjoinRootMinpoly F x).symm = AdjoinRoot.Minpoly.toAdjoin F x
-- Std.Do.PredTrans
Std.Do.PredTrans.instLawfulMonad : ∀ {ps : Std.Do.PostShape}, LawfulMonad (Std.Do.PredTrans ps)
-- Mathlib.Algebra.Homology.Embedding.AreComplementary
/-- If `ac : AreComplementary e₁ e₂` (with `e₁ : ComplexShape.Embedding c₁ c` and
`e₂ : ComplexShape.Embedding c₂ c`), and `i₂` belongs to `e₂.BoundaryGE`,
then this is the (unique) index `i₁` of `c₁` such that `ac.Boundary i₁ i₂`.  -/
ComplexShape.Embedding.AreComplementary.Boundary.indexOfBoundaryGE : {ι : Type u_1} →
  {ι₁ : Type u_2} →
    {ι₂ : Type u_3} →
      {c : ComplexShape ι} →
        {c₁ : ComplexShape ι₁} →
          {c₂ : ComplexShape ι₂} →
            {e₁ : c₁.Embedding c} → {e₂ : c₂.Embedding c} → e₁.AreComplementary e₂ → {i₂ : ι₂} → e₂.BoundaryGE i₂ → ι₁
-- Mathlib.Data.Complex.Basic
Complex.sub_im : ∀ (z w : ℂ), (z - w).im = z.im - w.im
-- Mathlib.Algebra.Group.Defs
SubNegMonoid.toSub : {G : Type u} → [self : SubNegMonoid G] → Sub G
-- Mathlib.Topology.Compactness.Compact
IsCompact.finite_of_discrete : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} [DiscreteTopology X], IsCompact s → s.Finite
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Mem_reverse : ∀ {α : Type u_1} {cmp : α → α → Ordering} {x : α} [Std.OrientedCmp cmp] {t : RBTree.RBNode α},
  RBTree.RBNode.Mem cmp x t.reverse ↔ RBTree.RBNode.Mem (flip cmp) x t
-- Mathlib.NumberTheory.ModularForms.Discriminant
_private.Mathlib.NumberTheory.ModularForms.Discriminant.0.ModularForm.csqrt_pow_24_eq : ∀ {z : ℂ}, z ≠ 0 → z.sqrt ^ 24 = z ^ 12
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.toListModel_getThenInsertIfNew? : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β} {a : α} {b : β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    (Std.DHashMap.Internal.toListModel (↑(Std.DHashMap.Internal.Raw₀.Const.getThenInsertIfNew? m a b).2).buckets).Perm
      (Std.Internal.List.insertEntryIfNew a b (Std.DHashMap.Internal.toListModel (↑m).buckets))
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.MonoidalCategory.tensor_associativity_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X₁ X₂ Y₁ Y₂ Z₁ Z₂ : C) {Z : C}
  (h :
    CategoryTheory.MonoidalCategoryStruct.tensorObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Z₁))
        (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Z₂)) ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerRight (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ Y₁ Y₂)
        (CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Z₂))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.tensorμ (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ Y₁)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj X₂ Y₂) Z₁ Z₂)
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategoryStruct.tensorHom
            (CategoryTheory.MonoidalCategoryStruct.associator X₁ Y₁ Z₁).hom
            (CategoryTheory.MonoidalCategoryStruct.associator X₂ Y₂ Z₂).hom)
          h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.associator (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Y₂)
          (CategoryTheory.MonoidalCategoryStruct.tensorObj Z₁ Z₂)).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (CategoryTheory.MonoidalCategoryStruct.tensorObj X₁ X₂)
          (CategoryTheory.MonoidalCategory.tensorμ Y₁ Y₂ Z₁ Z₂))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.tensorμ X₁ X₂ (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₁ Z₁)
            (CategoryTheory.MonoidalCategoryStruct.tensorObj Y₂ Z₂))
          h))
-- Init.Data.List.Sort.Basic
_private.Init.Data.List.Sort.Basic.0.List.merge.eq_def : ∀ {α : Type u_1} (xs ys : List α) (le : α → α → Bool),
  xs.merge ys le =
    match xs, ys with
    | [], ys => ys
    | xs, [] => xs
    | x :: xs, y :: ys => if le x y = true then x :: xs.merge (y :: ys) le else y :: (x :: xs).merge ys le
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.isSome_max?_insert : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, (t.insert k).max?.isSome = true
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.handleInlayHintsDidChange : Lean.Lsp.DidChangeTextDocumentParams → StateT Lean.Server.FileWorker.InlayHintState Lean.Server.RequestM Unit
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- The boundary of the `n`-cell given by the index `i`. Use this instead of `map n i '' sphere 0 1`
whenever possible.  -/
Topology.RelCWComplex.cellFrontier : {X : Type u_1} →
  [t : TopologicalSpace X] →
    {C D : Set X} → [inst : Topology.RelCWComplex C D] → (n : ℕ) → Topology.RelCWComplex.cell C n → Set X
-- Mathlib.Order.Filter.Basic
/-- There is exactly one filter on an empty type.  -/
Filter.unique : {α : Type u} → [IsEmpty α] → Unique (Filter α)
-- Mathlib.Data.Finsupp.Weight
/-- The degree of a finsupp function.  -/
Finsupp.degree : {σ : Type u_1} → {R : Type u_4} → [inst : AddCommMonoid R] → (σ →₀ R) →+ R
-- Mathlib.Logic.Function.Defs
Function.diag_injective : ∀ {α : Type u_1}, Function.Injective Function.diag
-- Mathlib.CategoryTheory.Sites.ConcreteSheafification
CategoryTheory.plusPlusSheaf_map_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) (D : Type w)
  [inst_1 : CategoryTheory.Category.{w', w} D] {FD : D → D → Type u_1} {CD : D → Type t}
  [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)] [instCC : CategoryTheory.ConcreteCategory D FD]
  [inst_3 :
    ∀ {X : C} (S : J.Cover X),
      CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Limits.WalkingMulticospan S.shape)
        (CategoryTheory.forget D)]
  [inst_4 :
    ∀ (P : CategoryTheory.Functor Cᵒᵖ D) (X : C) (S : J.Cover X), CategoryTheory.Limits.HasMultiequalizer (S.index P)]
  [inst_5 : ∀ (X : C), CategoryTheory.Limits.HasColimitsOfShape (J.Cover X)ᵒᵖ D]
  [inst_6 : ∀ (X : C), CategoryTheory.Limits.PreservesColimitsOfShape (J.Cover X)ᵒᵖ (CategoryTheory.forget D)]
  [inst_7 : (CategoryTheory.forget D).ReflectsIsomorphisms] {X Y : CategoryTheory.Functor Cᵒᵖ D} (η : X ⟶ Y),
  ((CategoryTheory.plusPlusSheaf J D).map η).hom = J.sheafifyMap η
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKey?_insert_le_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {km kmi : α}, t.minKey? = some km → (t.insert k v).minKey?.get ⋯ = kmi → (cmp kmi km).isLE = true
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- This is a more convenient formulation to show that a `BinaryCofan` constructed using
`BinaryCofan.mk` is a colimit cocone.
 -/
CategoryTheory.Limits.BinaryCofan.isColimitMk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y W : C} →
      {inl : X ⟶ W} →
        {inr : Y ⟶ W} →
          (desc : (s : CategoryTheory.Limits.BinaryCofan X Y) → W ⟶ s.pt) →
            (∀ (s : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.CategoryStruct.comp inl (desc s) = s.inl) →
              (∀ (s : CategoryTheory.Limits.BinaryCofan X Y), CategoryTheory.CategoryStruct.comp inr (desc s) = s.inr) →
                (∀ (s : CategoryTheory.Limits.BinaryCofan X Y) (m : W ⟶ s.pt),
                    CategoryTheory.CategoryStruct.comp inl m = s.inl →
                      CategoryTheory.CategoryStruct.comp inr m = s.inr → m = desc s) →
                  CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.BinaryCofan.mk inl inr)
-- Mathlib.LinearAlgebra.Reflection
Submodule.mem_invtSubmodule_reflection_iff : ∀ {R : Type u_1} {M : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {x : M}
  {f : Module.Dual R M} [IsDomain R] [NeZero 2] [Module.IsTorsionFree R M] (h : f x = 2) {p : Submodule R M},
  Disjoint p (R ∙ x) → (p ∈ Module.End.invtSubmodule ↑(Module.reflection h) ↔ p ≤ LinearMap.ker f)
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
/-- The second simplicial identity  -/
CategoryTheory.SimplicialObject.δ_comp_σ_of_le_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.SimplicialObject C) {n : ℕ}
  {i : Fin (n + 2)} {j : Fin (n + 1)},
  i ≤ j.castSucc →
    ∀ {Z : C} (h : X.obj (Opposite.op { len := n + 1 }) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (X.σ j.succ) (CategoryTheory.CategoryStruct.comp (X.δ i.castSucc) h) =
        CategoryTheory.CategoryStruct.comp (X.δ i) (CategoryTheory.CategoryStruct.comp (X.σ j) h)
-- Mathlib.GroupTheory.Torsion
CommMonoid.primaryComponent.eq_1 : ∀ (G : Type u_1) [inst : CommMonoid G] (p : ℕ),
  CommMonoid.primaryComponent G p = { carrier := {g | ∃ k, g ^ p ^ k = 1}, mul_mem' := ⋯, one_mem' := ⋯ }
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
/-- Auxiliary function for `reflTransSymm`.  -/
Path.Homotopy.reflTransSymmAux : ↑unitInterval × ↑unitInterval → ℝ
-- Mathlib.Data.Finsupp.Basic
Finsupp.subtypeDomain_piecewise : ∀ {α : Type u_1} {M : Type u_12} [inst : Zero M] {P : α → Prop} [inst_1 : DecidablePred P] (f : Subtype P →₀ M)
  (g : { a // ¬P a } →₀ M), Finsupp.subtypeDomain P (f.piecewise g) = f
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
PositiveLinearMap.preGNS_norm_sq : ∀ {A : Type u_1} [inst : NonUnitalCStarAlgebra A] [inst_1 : PartialOrder A] (f : A →ₚ[ℂ] ℂ) [inst_2 : StarOrderedRing A]
  (a : f.PreGNS), ↑‖a‖ ^ 2 = f (star (f.ofPreGNS a) * f.ofPreGNS a)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKeyD_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp},
  t.WF →
    ∀ {k k' fallback : α} {f : β → β},
      (Std.DTreeMap.Raw.Const.modify t k f).getKeyD k' fallback =
        if cmp k k' = Ordering.eq then if k ∈ t then k else fallback else t.getKeyD k' fallback
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CodeDecl.sset.sizeOf_spec : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (i offset : ℕ) (y : Lean.FVarId) (ty : Lean.Expr)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.CodeDecl._auto_7),
  sizeOf (Lean.Compiler.LCNF.CodeDecl.sset fvarId i offset y ty h) =
    1 + sizeOf fvarId + sizeOf i + sizeOf offset + sizeOf y + sizeOf ty + sizeOf h
-- Mathlib.RingTheory.Finiteness.Finsupp
FreeAbelianGroup.instFiniteInt : ∀ {σ : Type u_1} [Finite σ], Module.Finite ℤ (FreeAbelianGroup σ)
-- Mathlib.NumberTheory.MulChar.Basic
MulChar.equivToUnitHom_mul_apply : ∀ {R : Type u_1} [inst : CommMonoid R] {R' : Type u_2} [inst_1 : CommMonoidWithZero R'] (χ₁ χ₂ : MulChar R R') (a : Rˣ),
  (MulChar.equivToUnitHom (χ₁ * χ₂)) a = (MulChar.equivToUnitHom χ₁) a * (MulChar.equivToUnitHom χ₂) a
-- Mathlib.Data.Set.Lattice
Set.sigmaToiUnion_surjective : ∀ {α : Type u_1} {β : Type u_2} (t : α → Set β), Function.Surjective (Set.sigmaToiUnion t)
-- Std.Sync.Semaphore
_private.Std.Sync.Semaphore.0.Std.SemaphoreState.waiters : Std.SemaphoreState✝ → Std.Queue (IO.Promise Unit)
-- Mathlib.Algebra.Homology.DerivedCategory.HomologySequence
DerivedCategory.HomologySequence.epi_homologyMap_mor₁_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C],
  ∀ T ∈ CategoryTheory.Pretriangulated.distinguishedTriangles,
    ∀ (n₀ : ℤ),
      CategoryTheory.Epi ((DerivedCategory.homologyFunctor C n₀).map T.mor₁) ↔
        (DerivedCategory.homologyFunctor C n₀).map T.mor₂ = 0
-- Mathlib.LinearAlgebra.CrossProduct
/-- The cross product of two vectors in $R^3$ for $R$ a commutative ring.  -/
Matrix.«term_⨯₃_» : Lean.TrailingParserDescr
-- Mathlib.Order.Lattice
/-- The infimum is a lower bound on the first argument  -/
SemilatticeInf.inf_le_left : ∀ {α : Type u} [self : SemilatticeInf α] (a b : α), SemilatticeInf.inf a b ≤ a
-- Mathlib.Order.Filter.Extr
IsMaxFilter.congr : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder β] {f g : α → β} {a : α} {l : Filter α},
  IsMaxFilter f l a → f =ᶠ[l] g → f a = g a → IsMaxFilter g l a
-- Mathlib.Algebra.Group.Basic
eq_iff_eq_of_sub_eq_sub : ∀ {G : Type u_3} [inst : AddGroup G] {a b c d : G}, a - b = c - d → (a = b ↔ c = d)
-- Mathlib.LinearAlgebra.PiTensorProduct.Basic
/-- Induct using scaled versions of `PiTensorProduct.tprod`.  -/
PiTensorProduct.induction_on : ∀ {ι : Type u_1} {R : Type u_4} [inst : CommSemiring R] {s : ι → Type u_7} [inst_1 : (i : ι) → AddCommMonoid (s i)]
  [inst_2 : (i : ι) → Module R (s i)] {motive : (PiTensorProduct R fun i => s i) → Prop}
  (z : PiTensorProduct R fun i => s i),
  (∀ (r : R) (f : (i : ι) → s i), motive (r • (PiTensorProduct.tprod R) f)) →
    (∀ (x y : PiTensorProduct R fun i => s i), motive x → motive y → motive (x + y)) → motive z
-- Init.Data.Int.DivMod.Lemmas
Int.mul_le_of_le_ediv : ∀ {a b c : ℤ}, 0 < c → a ≤ b / c → a * c ≤ b
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonVersionedTextDocumentIdentifier : Lean.ToJson Lean.Lsp.VersionedTextDocumentIdentifier
-- Mathlib.Data.Ordmap.Ordnode
_private.Mathlib.Data.Ordmap.Ordnode.0.Ordnode.ofAscListAux₁.match_3.eq_2 : ∀ {α : Type u_1} (xs : List α) (motive : Ordnode α × { l' // l'.length ≤ xs.length } → Sort u_2) (l : Ordnode α) (y : α)
  (ys : List α) (h : (y :: ys).length ≤ xs.length)
  (h_1 : (t : Ordnode α) → (property : [].length ≤ xs.length) → motive (t, ⟨[], property⟩))
  (h_2 : (l : Ordnode α) → (y : α) → (ys : List α) → (h : (y :: ys).length ≤ xs.length) → motive (l, ⟨y :: ys, h⟩)),
  (match (l, ⟨y :: ys, h⟩) with
    | (t, ⟨[], property⟩) => h_1 t property
    | (l, ⟨y :: ys, h⟩) => h_2 l y ys h) =
    h_2 l y ys h
-- Lean.Elab.Import
Lean.Elab.HeaderSyntax.imports : Lean.Elab.HeaderSyntax → optParam Bool true → Array Lean.Import
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.whiskerRight_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] {F G F' : CategoryTheory.Functor C D} {α : F ⟶ G} {X : C},
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight α F').app X =
    CategoryTheory.MonoidalCategoryStruct.whiskerRight (α.app X) (F'.obj X)
-- Mathlib.Analysis.Normed.Operator.Bilinear
/-- `ContinuousLinearMap.smulRight` as a continuous trilinear map:
`smulRightL (c : StrongDual 𝕜 E) (f : F) (x : E) = c x • f`.

This is also known as a rank-one operator.
See also `InnerProductSpace.rankOne` for the rank-one operator on Hilbert spaces.  -/
ContinuousLinearMap.smulRightL : (𝕜 : Type u_1) →
  (E : Type u_4) →
    (Fₗ : Type u_7) →
      [inst : SeminormedAddCommGroup E] →
        [inst_1 : SeminormedAddCommGroup Fₗ] →
          [inst_2 : NontriviallyNormedField 𝕜] →
            [inst_3 : NormedSpace 𝕜 E] → [inst_4 : NormedSpace 𝕜 Fₗ] → StrongDual 𝕜 E →L[𝕜] Fₗ →L[𝕜] E →L[𝕜] Fₗ
-- Mathlib.Order.Category.CompleteLat
/-- `OrderDual` as a functor.  -/
CompleteLat.dual : CategoryTheory.Functor CompleteLat CompleteLat
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The identity of an object in `Φ.LeftResolution X₂`.  -/
CategoryTheory.LocalizerMorphism.LeftResolution.Hom.id : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} → {X₂ : C₂} → (L : Φ.LeftResolution X₂) → L.Hom L
-- Mathlib.Combinatorics.SimpleGraph.Copy
SimpleGraph.Copy.injective' : ∀ {α : Type u_4} {β : Type u_5} {A : SimpleGraph α} {B : SimpleGraph β} (self : A.Copy B),
  Function.Injective ⇑self.toHom
-- Mathlib.Algebra.Order.Archimedean.Real.Basic
Real.iInf_of_not_bddBelow : ∀ {ι : Sort u_1} {f : ι → ℝ}, ¬BddBelow (Set.range f) → ⨅ i, f i = 0
-- Mathlib.RingTheory.OreLocalization.Basic
OreLocalization.instAdd : {R : Type u_1} →
  [inst : Monoid R] →
    {S : Submonoid R} →
      [inst_1 : OreLocalization.OreSet S] →
        {X : Type u_2} → [inst_2 : AddMonoid X] → [inst_3 : DistribMulAction R X] → Add (OreLocalization S X)
-- Mathlib.Algebra.Homology.HomotopyCategory.Pretriangulated
/-- The standard triangle `K ⟶ L ⟶ mappingCone φ ⟶ K⟦(1 : ℤ)⟧` in `CochainComplex C ℤ`
attached to a morphism `φ : K ⟶ L`. It involves `φ`, `inr φ : L ⟶ mappingCone φ` and
the morphism induced by the `1`-cocycle `-mappingCone.fst φ`.  -/
CochainComplex.mappingCone.triangle : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [CategoryTheory.Limits.HasBinaryBiproducts C] →
        {K L : CochainComplex C ℤ} → (K ⟶ L) → CategoryTheory.Pretriangulated.Triangle (CochainComplex C ℤ)
-- Std.Data.DHashMap.IteratorLemmas
Std.DHashMap.toList_iter : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap α β}, m.iter.toList = m.toList
-- Init.Data.Nat.Basic
/-- Alias for `Nat.le_total`.  -/
Nat.le_or_le : ∀ (m n : ℕ), m ≤ n ∨ n ≤ m
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.LowDegree
groupCohomology.H2π_eq_iff : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A : Rep.{u, u, u} k G} (x y : ↥(groupCohomology.cocycles₂ A)),
  (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π A)) x =
      (CategoryTheory.ConcreteCategory.hom (groupCohomology.H2π A)) y ↔
    ⇑x - ⇑y ∈ groupCohomology.coboundaries₂ A
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
/-- The five lemma.  -/
CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {R₁ R₂ : CategoryTheory.ComposableArrows C 4},
  R₁.Exact →
    R₂.Exact →
      ∀ (φ : R₁ ⟶ R₂),
        CategoryTheory.Epi
            (CategoryTheory.ComposableArrows.app' φ 0
              CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_2) →
          CategoryTheory.IsIso
              (CategoryTheory.ComposableArrows.app' φ 1
                CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_4) →
            CategoryTheory.IsIso
                (CategoryTheory.ComposableArrows.app' φ 3
                  CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_6) →
              CategoryTheory.Mono
                  (CategoryTheory.ComposableArrows.app' φ 4
                    CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_7) →
                CategoryTheory.IsIso
                  (CategoryTheory.ComposableArrows.app' φ 2
                    CategoryTheory.Abelian.isIso_of_epi_of_isIso_of_isIso_of_mono._proof_9)
-- Mathlib.Data.Set.Function
Equiv.bijOn' : ∀ {α : Type u_1} {β : Type u_2} (e : α ≃ β) {s : Set α} {t : Set β},
  Set.MapsTo (⇑e) s t → Set.MapsTo (⇑e.symm) t s → Set.BijOn (⇑e) s t
-- Mathlib.Algebra.GroupWithZero.Range
MonoidWithZeroHom.valueGroup_eq_range : ∀ {A : Type u_1} {B : Type u_2} [inst : GroupWithZero A] [inst_1 : GroupWithZero B] (f : A →*₀ B),
  Units.val '' ↑f.valueGroup = Set.range ⇑f \ {0}
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey!_mem : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α], t ≠ ∅ → t.maxKey! ∈ t
-- Mathlib.Topology.Algebra.PontryaginDual
PontryaginDual.one_apply : ∀ {A : Type u_1} [inst : Monoid A] [inst_1 : TopologicalSpace A] (a : A), 1 a = 1
-- Mathlib.CategoryTheory.Monad.EquivMon
/-- To every `Monad C` we associated a monoid object in `C ⥤ C`.  -/
CategoryTheory.Monad.toMon : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → CategoryTheory.Monad C → CategoryTheory.Mon (CategoryTheory.Functor C C)
-- Mathlib.CategoryTheory.Limits.Shapes.WidePullbacks
CategoryTheory.Limits.instInhabitedWidePushoutShape : (J : Type w) → Inhabited (CategoryTheory.Limits.WidePushoutShape J)
-- Init.Data.Nat.Coprime
Nat.exists_coprime' : ∀ {m n : ℕ}, 0 < m.gcd n → ∃ g m' n', 0 < g ∧ m'.Coprime n' ∧ m = m' * g ∧ n = n' * g
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Rotation
Orientation.rotation_map : ∀ {V : Type u_1} {V' : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : NormedAddCommGroup V']
  [inst_2 : InnerProductSpace ℝ V] [inst_3 : InnerProductSpace ℝ V'] [inst_4 : Fact (Module.finrank ℝ V = 2)]
  [inst_5 : Fact (Module.finrank ℝ V' = 2)] (o : Orientation ℝ V (Fin 2)) (θ : Real.Angle) (f : V ≃ₗᵢ[ℝ] V') (x : V'),
  (((Orientation.map (Fin 2) f.toLinearEquiv) o).rotation θ) x = f ((o.rotation θ) (f.symm x))
-- Lean.Meta.SynthInstance
Lean.Meta.SynthInstance.MkTableKey.State : Type