mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.Homotopy
Homotopy.comm : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} {f g : C ⟶ D} (self : Homotopy f g) (i : ι),
  f.f i = (dNext i) self.hom + (prevD i) self.hom + g.f i
-- Mathlib.Tactic.ClickSuggestions.TryPremises
/-- Run `f` on the results of all tasks in the array of tasks, in an arbitrary order.

TODO?: use Lean's `Mutex` to avoid the polling loop?  -/
_private.Mathlib.Tactic.ClickSuggestions.TryPremises.0.Mathlib.Tactic.ClickSuggestions.foldTasksM : {α β : Type} → Array (Task β) → α → (α → β → Lean.MetaM α) → Lean.MetaM α
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.addSubmonoidMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (f : M →+ N) (M' : AddSubmonoid M),
  f.addSubmonoidMap M' = { toFun := fun x => ⟨f ↑x, ⋯⟩, map_zero' := ⋯, map_add' := ⋯ }
-- Std.Data.HashMap.IteratorLemmas
Std.HashMap.keysArray.eq_1 : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} (m : Std.HashMap α β), m.keysArray = m.inner.keysArray
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.repr.match_1.eq_1 : ∀ (motive : ONote → Sort u_1) (h_1 : Unit → motive ONote.zero)
  (h_2 : (e : ONote) → (n : ℕ+) → (a : ONote) → motive (e.oadd n a)),
  (match ONote.zero with
    | ONote.zero => h_1 ()
    | e.oadd n a => h_2 e n a) =
    h_1 ()
-- Mathlib.Algebra.Homology.TotalComplex
/-- The horizontal differential in the total complex on a given summand.  -/
HomologicalComplex₂.d₁ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {I₁ : Type u_2} →
        {I₂ : Type u_3} →
          {I₁₂ : Type u_4} →
            {c₁ : ComplexShape I₁} →
              {c₂ : ComplexShape I₂} →
                (K : HomologicalComplex₂ C c₁ c₂) →
                  (c₁₂ : ComplexShape I₁₂) →
                    [inst_2 : TotalComplexShape c₁ c₂ c₁₂] →
                      [DecidableEq I₁₂] →
                        [inst_4 : K.HasTotal c₁₂] →
                          (i₁ : I₁) →
                            (i₂ : I₂) → (i₁₂ : I₁₂) → (K.X i₁).X i₂ ⟶ K.toGradedObject.mapObj (c₁.π c₂ c₁₂) i₁₂
-- Init.Data.Array.Perm
/-- `Perm as bs` asserts that `as` and `bs` are permutations of each other.

This is a wrapper around `List.Perm`, and for now has much less API.
For more complicated verification, use `perm_iff_toList_perm` and the `List` API.
 -/
Array.«term_~_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.pi.instIsProbabilityMeasure : ∀ {ι : Type u_1} {α : ι → Type u_3} [inst : Fintype ι] [inst_1 : (i : ι) → MeasurableSpace (α i)]
  (μ : (i : ι) → MeasureTheory.Measure (α i)) [∀ (i : ι), MeasureTheory.IsProbabilityMeasure (μ i)],
  MeasureTheory.IsProbabilityMeasure (MeasureTheory.Measure.pi μ)
-- Mathlib.Algebra.Homology.BifunctorHomotopy
HomologicalComplex.mapBifunctorMapHomotopy.ιMapBifunctor_hom₂ : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} {I₁ : Type u_4} {I₂ : Type u_5} {J : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_3} D] [inst_3 : CategoryTheory.Preadditive C₁]
  [inst_4 : CategoryTheory.Preadditive C₂] [inst_5 : CategoryTheory.Preadditive D] {c₁ : ComplexShape I₁}
  {c₂ : ComplexShape I₂} {K₁ L₁ : HomologicalComplex C₁ c₁} (f₁ : K₁ ⟶ L₁) {K₂ L₂ : HomologicalComplex C₂ c₂}
  {f₂ f₂' : K₂ ⟶ L₂} (h₂ : Homotopy f₂ f₂') (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D))
  [inst_6 : F.Additive] [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).Additive] (c : ComplexShape J) [inst_8 : DecidableEq J]
  [inst_9 : TotalComplexShape c₁ c₂ c] [inst_10 : K₁.HasMapBifunctor K₂ F c] [inst_11 : L₁.HasMapBifunctor L₂ F c]
  (i₁ : I₁) (i₂ i₂' : I₂) (j j' : J) (h : c₁.π c₂ c (i₁, i₂') = j),
  c₂.prev i₂' = i₂ →
    CategoryTheory.CategoryStruct.comp (K₁.ιMapBifunctor K₂ F c i₁ i₂' j h)
        (HomologicalComplex.mapBifunctorMapHomotopy.hom₂ f₁ h₂ F c j j') =
      c₁.ε₂ c₂ c (i₁, i₂) •
        CategoryTheory.CategoryStruct.comp ((F.map (f₁.f i₁)).app (K₂.X i₂'))
          (CategoryTheory.CategoryStruct.comp ((F.obj (L₁.X i₁)).map (h₂.hom i₂' i₂))
            (L₁.ιMapBifunctorOrZero L₂ F c i₁ i₂ j'))
-- Mathlib.Analysis.Complex.Norm
Complex.isCauSeq_re : ∀ (f : CauSeq ℂ fun x => ‖x‖), IsCauSeq abs fun n => (↑f n).re
-- Mathlib.AlgebraicGeometry.IdealSheaf.Subscheme
AlgebraicGeometry.Scheme.IdealSheafData.subschemeι_apply : ∀ {X : AlgebraicGeometry.Scheme} (I : X.IdealSheafData) (x : ↥I.subscheme), I.subschemeι x = ↑x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Defs
/-- Any object at the top left of a pullback square is
isomorphic to the pullback provided by the `HasLimit` API.  -/
CategoryTheory.IsPushout.isoPushout : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {Z X Y P : C} →
      {f : Z ⟶ X} →
        {g : Z ⟶ Y} →
          {inl : X ⟶ P} →
            {inr : Y ⟶ P} →
              CategoryTheory.IsPushout f g inl inr →
                [inst_1 : CategoryTheory.Limits.HasPushout f g] → P ≅ CategoryTheory.Limits.pushout f g
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.equiv_empty_iff_isEmpty : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m.WF → (m.Equiv ∅ ↔ m.isEmpty = true)
-- Mathlib.Algebra.Category.Grp.Zero
AddCommGrpCat.hasZeroObject : CategoryTheory.Limits.HasZeroObject AddCommGrpCat
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prod_dist_eq_of_L1 : ∀ {α : Type u_2} {β : Type u_3} [inst : SeminormedAddCommGroup α] [inst_1 : SeminormedAddCommGroup β]
  (x y : WithLp 1 (α × β)), dist x y = dist x.fst y.fst + dist x.snd y.snd
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasFDerivAtFilter.const_smul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E →L[𝕜] F} {L : Filter (E × E)} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F]
  [inst_7 : SMulCommClass 𝕜 R F] [inst_8 : ContinuousConstSMul R F],
  HasFDerivAtFilter f f' L → ∀ (c : R), HasFDerivAtFilter (c • f) (c • f') L
-- Init.Data.Array.Range
Array.find?_range_eq_some : ∀ {n i : ℕ} {p : ℕ → Bool},
  Array.find? p (Array.range n) = some i ↔ p i = true ∧ i ∈ Array.range n ∧ ∀ j < i, (!p j) = true
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace.ResidueField
/-- The residue field of `X` at a point `x` is the residue field of the stalk of `X`
at `x`.  -/
AlgebraicGeometry.LocallyRingedSpace.residueField : (X : AlgebraicGeometry.LocallyRingedSpace) → ↑X.toTopCat → CommRingCat
-- Init.Data.List.FinRange
List.ofFnM_succ : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] [LawfulMonad m] {f : Fin (n + 1) → m α},
  List.ofFnM f = do
    let a ← f 0
    let as ← List.ofFnM fun i => f i.succ
    pure (a :: as)
-- Mathlib.Topology.Compactness.LocallyCompact
/-- In a weakly locally compact space,
the filters `𝓝 x` and `cocompact X` are disjoint for all `X`.  -/
disjoint_nhds_cocompact : ∀ {X : Type u_1} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] (x : X),
  Disjoint (nhds x) (Filter.cocompact X)
-- Mathlib.Algebra.Ring.Ext
AddMonoidWithOne.ext : ∀ {R : Type u} ⦃inst₁ inst₂ : AddMonoidWithOne R⦄, HAdd.hAdd = HAdd.hAdd → One.one = One.one → inst₁ = inst₂
-- Aesop.Search.Expansion.Simp
Aesop.simpGoal : Lean.MVarId →
  Lean.Meta.Simp.Context →
    Lean.Meta.Simp.SimprocsArray →
      optParam (Option Lean.Meta.Simp.Discharge) none →
        optParam Bool true →
          optParam (Array Lean.FVarId) #[] → optParam Lean.Meta.Simp.Stats { } → Lean.MetaM Aesop.SimpResult
-- Mathlib.LinearAlgebra.Finsupp.Supported
Finsupp.single_mem_supported : ∀ {α : Type u_1} {M : Type u_2} (R : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  {s : Set α} {a : α} (b : M), a ∈ s → (fun₀ | a => b) ∈ Finsupp.supported M R s
-- Mathlib.MeasureTheory.Function.AEEqFun
/-- A measurable representative of an `AEEqFun` [f]  -/
MeasureTheory.AEEqFun.instCoeFun : {α : Type u_1} →
  {β : Type u_2} →
    [inst : MeasurableSpace α] →
      {μ : MeasureTheory.Measure α} → [inst_1 : TopologicalSpace β] → CoeFun (α →ₘ[μ] β) fun x => α → β
-- Mathlib.Probability.Kernel.MeasurableLIntegral
Measurable.setLIntegral_kernel : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {κ : ProbabilityTheory.Kernel α β}
  [ProbabilityTheory.IsSFiniteKernel κ] {f : β → ENNReal},
  Measurable f → ∀ {s : Set β}, MeasurableSet s → Measurable fun a => ∫⁻ (b : β) in s, f b ∂κ a
-- Std.Data.DHashMap.Internal.RawLemmas
_private.Std.Data.DHashMap.Internal.RawLemmas.0.List.forIn'_cons.match_1.eq_1 : ∀ {β : Type u_1} (motive : ForInStep β → Sort u_2) (b : β) (h_1 : (b : β) → motive (ForInStep.done b))
  (h_2 : (b : β) → motive (ForInStep.yield b)),
  (match ForInStep.done b with
    | ForInStep.done b => h_1 b
    | ForInStep.yield b => h_2 b) =
    h_1 b
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
_private.Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense.0.CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift_map : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {J₀ : CategoryTheory.GrothendieckTopology C₀}
  {J : CategoryTheory.GrothendieckTopology C} {A : Type u'} [inst_2 : CategoryTheory.Category.{v', u'} A]
  [inst_3 : CategoryTheory.Functor.IsDenseSubsite J₀ J F] {data : (X : C) → F.OneHypercoverDenseData J₀ J X}
  {G : CategoryTheory.Functor Cᵒᵖ A} (hG₀ : CategoryTheory.Presheaf.IsSheaf J₀ (F.op.comp G))
  (hG : (X : C) → CategoryTheory.Limits.IsLimit ((data X).toOneHypercover.multifork G)) {X : C} {S : J.Cover X}
  (s : CategoryTheory.Limits.Multifork (S.index G)) (i : (data X).I₀),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.lift✝ hG₀ hG s)
      (G.map ((data X).f i).op) =
    CategoryTheory.Functor.OneHypercoverDenseData.isSheaf_iff.liftAux✝ hG₀ s i
-- Init.Data.Option.Instances
Option.some_inj : ∀ {α : Type u_1} {a b : α}, some a = some b ↔ a = b
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.irreducible_mul_leadingCoeff_inv : ∀ {K : Type u_1} [inst : DivisionRing K] {p : Polynomial K},
  Irreducible (p * Polynomial.C p.leadingCoeff⁻¹) ↔ Irreducible p
-- Std.Data.DTreeMap.Basic
/-- Check if all elements satisfy the predicate, short-circuiting if a predicate fails.  -/
Std.DTreeMap.all : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → Std.DTreeMap α β cmp → ((a : α) → β a → Bool) → Bool
-- Mathlib.Topology.Bornology.Basic
Bornology.isBounded_biUnion_finset : ∀ {ι : Type u_1} {α : Type u_2} [inst : Bornology α] (s : Finset ι) {f : ι → Set α},
  Bornology.IsBounded (⋃ i ∈ s, f i) ↔ ∀ i ∈ s, Bornology.IsBounded (f i)
-- Init.Control.Lawful.MonadAttach.Instances
instLawfulMonadAttachExceptTOfLawfulMonad : ∀ {m : Type (max u_1 u_2) → Type u_3} {ε : Type (max u_1 u_2)} [inst : Monad m] [LawfulMonad m] [inst_2 : MonadAttach m]
  [LawfulMonadAttach m], LawfulMonadAttach (ExceptT ε m)
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.prod.map_map_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A₁ A₂ A₃ B₁ B₂ B₃ : C}
  [inst_1 : CategoryTheory.Limits.HasBinaryProduct A₁ B₁] [inst_2 : CategoryTheory.Limits.HasBinaryProduct A₂ B₂]
  [inst_3 : CategoryTheory.Limits.HasBinaryProduct A₃ B₃] (f : A₁ ⟶ A₂) (g : B₁ ⟶ B₂) (h : A₂ ⟶ A₃) (k : B₂ ⟶ B₃)
  {Z : C} (h_1 : A₃ ⨯ B₃ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map f g)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.map h k) h_1) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.prod.map (CategoryTheory.CategoryStruct.comp f h) (CategoryTheory.CategoryStruct.comp g k))
      h_1
-- Mathlib.Data.Num.Lemmas
Num.zneg_toZNum : ∀ (n : Num), -n.toZNum = n.toZNumNeg
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearIsometryEquiv.symm_conjStarAlgEquiv_apply_apply : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] {K : Type u_6} [inst_4 : NormedAddCommGroup K] [inst_5 : InnerProductSpace 𝕜 K]
  [inst_6 : CompleteSpace K] (e : H ≃ₗᵢ[𝕜] K) (f : K →L[𝕜] K) (x : H), (e.conjStarAlgEquiv.symm f) x = e.symm (f (e x))
-- Aesop.Forward.State
Aesop.InstMap.mk.inj : ∀ {map map_1 : Lean.PHashMap Aesop.SlotIndex (Aesop.EMap (Lean.PHashSet Aesop.Match × Lean.PHashSet Aesop.Hyp))},
  { map := map } = { map := map_1 } → map = map_1
-- Std.Data.HashMap.Lemmas
Std.HashMap.map_fst_toArray_eq_keysArray : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α],
  Array.map Prod.fst m.toArray = m.keysArray
-- Lean.Declaration
Lean.InductiveType.mk.sizeOf_spec : ∀ (name : Lean.Name) (type : Lean.Expr) (ctors : List Lean.Constructor),
  sizeOf { name := name, type := type, ctors := ctors } = 1 + sizeOf name + sizeOf type + sizeOf ctors
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
IntervalIntegrable.sum : ∀ {ι : Type u_1} {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {ε : Type u_8} [inst : TopologicalSpace ε]
  [inst_1 : ENormedAddCommMonoid ε] [ContinuousAdd ε] (s : Finset ι) {f : ι → ℝ → ε},
  (∀ i ∈ s, IntervalIntegrable (f i) μ a b) → IntervalIntegrable (∑ i ∈ s, f i) μ a b
-- Init.Data.Order.LemmasExtra
Std.instCommutativeMinOfLawfulOrderLeftLeaningMinOfIsLinearOrder : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Min α] [Std.LawfulOrderLeftLeaningMin α] [Std.IsLinearOrder α],
  Std.Commutative min
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.FamilyOfElements.IsAmalgamation.of_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P Q : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R : CategoryTheory.Presieve X} (f : P ⟶ Q) [CategoryTheory.Mono f] {x : CategoryTheory.Presieve.FamilyOfElements P R}
  {t : P.obj (Opposite.op X)},
  (x.map f).IsAmalgamation ((CategoryTheory.ConcreteCategory.hom (f.app (Opposite.op X))) t) → x.IsAmalgamation t
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- An intermediate field is closed under inverses.  -/
IntermediateField.inv_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  {x : L}, x ∈ S → x⁻¹ ∈ S
-- Mathlib.RingTheory.Ideal.Operations
Ideal.isCoprime_tfae : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R},
  [IsCoprime I J, Codisjoint I J, I + J = 1, ∃ i ∈ I, ∃ j ∈ J, i + j = 1, I ⊔ J = ⊤].TFAE
-- Mathlib.AlgebraicTopology.RelativeCellComplex.AttachCells
HomotopicalAlgebra.AttachCells.hom_ext : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {α : Type t} {A B : α → C} {g : (a : α) → A a ⟶ B a}
  {X₁ X₂ : C} {f : X₁ ⟶ X₂} (c : HomotopicalAlgebra.AttachCells g f) {Z : C} {φ φ' : X₂ ⟶ Z},
  CategoryTheory.CategoryStruct.comp f φ = CategoryTheory.CategoryStruct.comp f φ' →
    (∀ (i : c.ι), CategoryTheory.CategoryStruct.comp (c.cell i) φ = CategoryTheory.CategoryStruct.comp (c.cell i) φ') →
      φ = φ'
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.coreflection_apply : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) (i : ι) (f : N),
  (P.coreflection i) f = f - (P.root' i) f • P.coroot i
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.forget_map : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y), AlgebraicGeometry.Scheme.forget.map f = TypeCat.ofHom ⇑f
-- Mathlib.Analysis.RCLike.Basic
RCLike.re_le_norm : ∀ {K : Type u_1} [inst : RCLike K] (z : K), RCLike.re z ≤ ‖z‖
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.zpow'_one : ∀ {α : Type u_1} [inst : GroupWithZero α] (a : α), Mathlib.Tactic.FieldSimp.zpow' a 1 = a
-- Mathlib.Data.Ordmap.Invariants
_private.Mathlib.Data.Ordmap.Invariants.0.Ordnode.node4L.match_1.eq_1 : ∀ {α : Type u_1} (motive : Ordnode α → α → Ordnode α → α → Ordnode α → Sort u_2) (l : Ordnode α) (x : α) (size : ℕ)
  (ml : Ordnode α) (y : α) (mr : Ordnode α) (z : α) (r : Ordnode α)
  (h_1 :
    (l : Ordnode α) →
      (x : α) →
        (size : ℕ) →
          (ml : Ordnode α) →
            (y : α) → (mr : Ordnode α) → (z : α) → (r : Ordnode α) → motive l x (Ordnode.node size ml y mr) z r)
  (h_2 : (l : Ordnode α) → (x z : α) → (r : Ordnode α) → motive l x Ordnode.nil z r),
  (match l, x, Ordnode.node size ml y mr, z, r with
    | l, x, Ordnode.node size ml y mr, z, r => h_1 l x size ml y mr z r
    | l, x, Ordnode.nil, z, r => h_2 l x z r) =
    h_1 l x size ml y mr z r
-- Mathlib.Data.Nat.Prime.Int
Int.prime_two : Prime 2
-- Mathlib.Topology.Category.FinTopCat
/-- A bundled finite topological space.  -/
FinTopCat : Type (u + 1)
-- Mathlib.Algebra.Order.Monoid.Lex
/-- Given ordered additive monoids M, N, the natural projection
ordered homomorphism from M × N to N.  -/
OrderAddMonoidHom.snd : (α : Type u_1) →
  (β : Type u_2) →
    [inst : AddMonoid α] → [inst_1 : PartialOrder α] → [inst_2 : AddMonoid β] → [inst_3 : Preorder β] → α × β →+o β
-- Mathlib.Data.Finset.Lattice.Basic
Finset.inter_subset_left : ∀ {α : Type u_1} [inst : DecidableEq α] {s₁ s₂ : Finset α}, s₁ ∩ s₂ ⊆ s₁
-- Mathlib.NumberTheory.Padics.Complex
PadicAlgCl.coe_eq : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)], Coe.coe = ⇑(algebraMap ℚ_[p] (PadicAlgCl p))
-- Mathlib.RingTheory.AdicCompletion.Basic
IsHausdorff.mk : ∀ {R : Type u_1} [inst : CommRing R] {I : Ideal R} {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  (∀ (x : M), (∀ (n : ℕ), x ≡ 0 [SMOD I ^ n • ⊤]) → x = 0) → IsHausdorff I M
-- Mathlib.CategoryTheory.Endofunctor.Algebra
CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso_inv_app_f : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C C} (adj : F ⊣ G)
  (X : CategoryTheory.Endofunctor.Coalgebra G),
  ((CategoryTheory.Endofunctor.Adjunction.AlgCoalgEquiv.counitIso adj).inv.app X).f =
    CategoryTheory.CategoryStruct.id X.V
-- Lean.Meta.Eqns
Lean.Meta.backward.eqns.nonrecursive : Lean.Option Bool
-- Mathlib.Order.RelClasses
isWellFounded_iff : ∀ (α : Type u) (r : α → α → Prop), IsWellFounded α r ↔ WellFounded r
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.constVSub_apply : ∀ (k : Type u_1) {P₁ : Type u_2} {V₁ : Type u_6} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁]
  [inst_3 : AddTorsor V₁ P₁] (p x : P₁), (AffineEquiv.constVSub k p) x = p -ᵥ x
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- The left homology data on a short complex equipped with a splitting.  -/
CategoryTheory.ShortComplex.Splitting.leftHomologyData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} → [CategoryTheory.Limits.HasZeroObject C] → S.Splitting → S.LeftHomologyData
-- Mathlib.Topology.Algebra.ConstMulAction
IsOpen.vadd : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : AddGroup G] [inst_2 : AddAction G α]
  [ContinuousConstVAdd G α] {s : Set α}, IsOpen s → ∀ (c : G), IsOpen (c +ᵥ s)
-- Init.Data.UInt.Lemmas
UInt16.mul_one : ∀ (a : UInt16), a * 1 = a
-- Mathlib.SetTheory.Ordinal.Basic
Cardinal.ord_mono : Monotone Cardinal.ord
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getD_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' : α} {fallback : β k'} {f : β k → β k},
  (t.modify k f).getD k' fallback =
    if heq : cmp k k' = Ordering.eq then (Option.map (cast ⋯) (Option.map f (t.get? k))).getD fallback
    else t.getD k' fallback
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
/-- `HasFTaylorSeriesUpTo n f p` registers the fact that `p 0 = f` and `p (m+1)` is a
derivative of `p m` for `m < n`, and is continuous for `m ≤ n`. This is a predicate analogous to
`HasFDerivAt` but for higher-order derivatives.

Notice that `p` does not sum up to `f` on the diagonal (`FormalMultilinearSeries.sum`), even if
`f` is analytic and `n = ∞`: an addition `1/m!` factor on the `m`th term is necessary for that.  -/
HasFTaylorSeriesUpTo : {𝕜 : Type u} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type uE} →
      [inst_1 : NormedAddCommGroup E] →
        [inst_2 : NormedSpace 𝕜 E] →
          {F : Type uF} →
            [inst_3 : NormedAddCommGroup F] →
              [inst_4 : NormedSpace 𝕜 F] → WithTop ℕ∞ → (E → F) → (E → FormalMultilinearSeries 𝕜 E F) → Prop
-- Mathlib.Topology.EMetricSpace.PairReduction
PairReduction.pairSet_subset : ∀ {T : Type u_1} [inst : PseudoEMetricSpace T] {a c : ENNReal} {J : Finset T} [inst_1 : DecidableEq T],
  PairReduction.pairSet J a c ⊆ J ×ˢ J
-- Init.Data.Option.Lemmas
Option.or_eq_some_iff : ∀ {α : Type u_1} {o o' : Option α} {a : α}, o.or o' = some a ↔ o = some a ∨ o = none ∧ o' = some a
-- Mathlib.Data.PNat.Basic
/-- We now define a long list of structures on `ℕ+` induced by
similar structures on `ℕ`. Most of these behave in a completely
obvious way, but there are a few things to be said about
subtraction, division and powers.
 -/
PNat.coe_inj : ∀ {m n : ℕ+}, ↑m = ↑n ↔ m = n
-- Mathlib.Algebra.Group.Submonoid.Membership
/-- Logarithms from powers to natural numbers.  -/
Submonoid.log : {M : Type u_1} → [inst : Monoid M] → [DecidableEq M] → {n : M} → ↥(Submonoid.powers n) → ℕ
-- Mathlib.Topology.Order.LiminfLimsup
/-- Let `u : ι → α → β` be a sequence of antitone functions `α → β` indexed by `ι`. Suppose that for
all `i : ι`, `u i` tends to `c` at infinity, and that furthermore the limsup of `i ↦ u i r` along
the cofinite filter tends to the same `c` as `r` tends to infinity.
Then the supremum function `r ↦ ⨆ i, u i r` also tends to `c` at infinity.  -/
tendsto_iSup_of_tendsto_limsup : ∀ {ι : Type u_1} {α : Type u_7} {β : Type u_8} [inst : ConditionallyCompleteLattice α] [inst_1 : CompleteLinearOrder β]
  [inst_2 : TopologicalSpace β] [OrderTopology β] {u : ι → α → β} {c : β},
  (∀ (i : ι), Filter.Tendsto (u i) Filter.atTop (nhds c)) →
    Filter.Tendsto (fun r => Filter.limsup (fun i => u i r) Filter.cofinite) Filter.atTop (nhds c) →
      (∀ (i : ι), Antitone (u i)) → Filter.Tendsto (fun r => ⨆ i, u i r) Filter.atTop (nhds c)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LitValue.str.inj : ∀ {val val_1 : String}, Lean.Compiler.LCNF.LitValue.str val = Lean.Compiler.LCNF.LitValue.str val_1 → val = val_1
-- Init.Data.Range.Polymorphic.Instances
Std.Rxo.instIsAlwaysFiniteOfLawfulHasSize : ∀ {α : Type u_1} [inst : LT α] [inst_1 : Std.PRange.UpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerable α]
  [inst_3 : Std.Rxo.HasSize α] [Std.Rxo.LawfulHasSize α], Std.Rxo.IsAlwaysFinite α
-- Init.Data.SInt.Bitwise
Int16.shiftLeft_zero : ∀ {a : Int16}, a <<< 0 = a
-- Init.Data.Range.Polymorphic.SInt
Int16.instRxcHasSize.eq_1 : Int16.instRxcHasSize = { size := fun lo hi => (hi.toInt + 1 - lo.toInt).toNat }
-- Mathlib.Tactic.CategoryTheory.Bicategory.Datatypes
Mathlib.Tactic.Bicategory.structuralIsoOfExpr_comp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (η' : f ≅ g),
  η'.hom = η → ∀ (θ : g ⟶ h) (θ' : g ≅ h), θ'.hom = θ → (η' ≪≫ θ').hom = CategoryTheory.CategoryStruct.comp η θ
-- Mathlib.Algebra.Order.Floor.Ring
Int.fract_add : ∀ {R : Type u_2} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : FloorRing R] (a b : R),
  ∃ z, Int.fract (a + b) - Int.fract a - Int.fract b = ↑z
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.FunctorObjIndex.w_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} {f : (i : I) → A i ⟶ B i} {S X : C}
  {πX : X ⟶ S} (self : CategoryTheory.SmallObject.FunctorObjIndex f πX) {Z : C} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp self.t (CategoryTheory.CategoryStruct.comp πX h) =
    CategoryTheory.CategoryStruct.comp (f self.i) (CategoryTheory.CategoryStruct.comp self.b h)