mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.UnifyEq
/-- Helper method for methods such as `Cases.unifyEqs?`.
Given the given goal `mvarId` containing the local hypothesis `eqFVarId`, it performs the following operations:

- If `eqFVarId` is a heterogeneous equality, tries to convert it to a homogeneous one.
- If `eqFVarId` is a homogeneous equality of the form `a = b`, it tries
   - If `a` and `b` are definitionally equal, clear it
   - Normalize `a` and `b` using the current reducibility setting.
   - If `a` (`b`) is a free variable not occurring in `b` (`a`), replace it everywhere.
   - If `a` and `b` are distinct constructors, return `none` to indicate that the goal has been closed.
   - If `a` and `b` are the same constructor, apply `injection`, the result contains the number of new equalities introduced in the goal.
   - It also tries to apply the given `acyclic` method to try to close the goal.
     Remark: It is a parameter because `simp` uses `unifyEq?`, and `acyclic` depends on `simp`.
 -/
Lean.Meta.unifyEq? : Lean.MVarId →
  Lean.FVarId →
    optParam Lean.Meta.FVarSubst { } →
      (optParam (Lean.MVarId → Lean.Expr → Lean.MetaM Bool) fun x x_1 => pure false) →
        optParam (Option Lean.Name) none → Lean.MetaM (Option Lean.Meta.UnifyEqResult)
-- Mathlib.CategoryTheory.Monoidal.FunctorCategory
CategoryTheory.Monoidal.rightUnitor_inv_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 : CategoryTheory.Functor C D} {X : C},
  (CategoryTheory.MonoidalCategoryStruct.rightUnitor F).inv.app X =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj X)).inv
-- Mathlib.Algebra.Homology.HomotopyCofiber
/-- The `d` field of the homological complex `homotopyCofiber φ`.  -/
HomologicalComplex.homotopyCofiber.d : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {ι : Type u_2} →
        {c : ComplexShape ι} →
          {F G : HomologicalComplex C c} →
            (φ : F ⟶ G) →
              [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
                [inst_3 : DecidableRel c.Rel] →
                  (i j : ι) → HomologicalComplex.homotopyCofiber.X φ i ⟶ HomologicalComplex.homotopyCofiber.X φ j
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.div_pos : ∀ {b c : Ordinal.{u_4}}, c ≠ 0 → (0 < b / c ↔ c ≤ b)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.modify.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α]
  (m m_1 : Std.DHashMap.Raw α β), m = m_1 → ∀ (a : α) (f f_1 : β a → β a), f = f_1 → m.modify a f = m_1.modify a f_1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey?_diff_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∉ m₁ → (m₁ \ m₂).getKey? k = none
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- **Alias** of `Order.cof_le`. -/
Ordinal.lt_cof_type : ∀ {α : Type u} [inst : Preorder α] {s : Set α}, IsCofinal s → Order.cof α ≤ Cardinal.mk ↑s
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.Hom.w_assoc : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (φ : f ⟶ g) {Z : T}
  (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left φ) (CategoryTheory.CategoryStruct.comp g.hom h) =
    CategoryTheory.CategoryStruct.comp f.hom h
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.IsAddFundamentalDomain.lintegral_eq_tsum' : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] [inst_2 : MeasurableSpace α] {s : Set α}
  {μ : MeasureTheory.Measure α} [MeasurableConstVAdd G α] [MeasureTheory.VAddInvariantMeasure G α μ] [Countable G],
  MeasureTheory.IsAddFundamentalDomain G s μ →
    ∀ (f : α → ENNReal), ∫⁻ (x : α), f x ∂μ = ∑' (g : G), ∫⁻ (x : α) in s, f (-g +ᵥ x) ∂μ
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_erase_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Inhabited α] {k : α}, (t.erase k).getKey! k = default
-- Mathlib.Data.Set.Finite.List
List.finite_length_eq : ∀ (α : Type u_1) [Finite α] (n : ℕ), {l | l.length = n}.Finite
-- Mathlib.Tactic.Linter.HaveILetI
/-- Run the `letI` tactic, with a try this suggestion when the goal is a `Prop`.  -/
_private.Mathlib.Tactic.Linter.HaveILetI.0.Mathlib.Linter.HaveILetI.runLetI : Lean.Syntax →
  Lean.TSyntax `Lean.Parser.Term.letConfig → Lean.TSyntax `Lean.Parser.Term.letDecl → Lean.Elab.Tactic.TacticM Unit
-- Mathlib.RingTheory.MvPowerSeries.Evaluation
MvPowerSeries.HasEval.mk : ∀ {σ : Type u_1} {S : Type u_3} [inst : CommRing S] [inst_1 : TopologicalSpace S] {a : σ → S},
  (∀ (s : σ), IsTopologicallyNilpotent (a s)) → Filter.Tendsto a Filter.cofinite (nhds 0) → MvPowerSeries.HasEval a
-- Mathlib.GroupTheory.Sylow
/-- Sylow `p`-subgroups are in bijection with cosets of the normalizer of a Sylow `p`-subgroup  -/
Sylow.equivQuotientNormalizer : {p : ℕ} →
  {G : Type u_1} →
    [inst : Group G] →
      [Fact (Nat.Prime p)] → [Finite (Sylow p G)] → (P : Sylow p G) → Sylow p G ≃ G ⧸ Subgroup.normalizer ↑P
-- Mathlib.Order.Lattice
inf_eq_inf_iff_left : ∀ {α : Type u} [inst : SemilatticeInf α] {a b c : α}, a ⊓ b = a ⊓ c ↔ a ⊓ c ≤ b ∧ a ⊓ b ≤ c
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.one : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop} (j : J),
  RingCat.Colimits.Relation.below ⋯
-- Init.System.FilePath
/-- The file extension expected for executable binaries on the current platform, or `""` if there is no
such extension.
 -/
System.FilePath.exeExtension : String
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.partialMatch_iff : ∀ {pat s : ByteArray} {needlePos stackPos : ℕ},
  String.Slice.Pattern.Model.ForwardSliceSearcher.PartialMatch✝ pat s needlePos stackPos ↔
    ∃ (h₁ : stackPos ≤ s.size) (h₂ : needlePos ≤ pat.size) (h₃ : needlePos ≤ stackPos),
      ∀ (j : ℕ) (hj : j < needlePos), pat[j] = s[stackPos - needlePos + j]
-- Mathlib.Algebra.Group.Invertible.Defs
invOf_mul_self : ∀ {α : Type u} [inst : Mul α] [inst_1 : One α] (a : α) [inst_2 : Invertible a], ⅟a * a = 1
-- Mathlib.Tactic.GRewrite.Core
_private.Mathlib.Tactic.GRewrite.Core.0.Mathlib.Tactic.GRewrite.State.mk.injEq : ∀ (cache : Std.HashSet (Option Lean.Expr × Lean.Expr × Bool)) (progress : Mathlib.Tactic.GRewrite.Progress✝)
  (cache_1 : Std.HashSet (Option Lean.Expr × Lean.Expr × Bool)) (progress_1 : Mathlib.Tactic.GRewrite.Progress✝),
  ({ cache := cache, progress := progress } = { cache := cache_1, progress := progress_1 }) =
    (cache = cache_1 ∧ progress = progress_1)
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.InitResults.mk.injEq : ∀ {α : Type} (tree : Lean.Meta.LazyDiscrTree.PreDiscrTree α) (errors : Array Lean.Meta.LazyDiscrTree.ImportFailure)
  (tree_1 : Lean.Meta.LazyDiscrTree.PreDiscrTree α) (errors_1 : Array Lean.Meta.LazyDiscrTree.ImportFailure),
  ({ tree := tree, errors := errors } = { tree := tree_1, errors := errors_1 }) = (tree = tree_1 ∧ errors = errors_1)
-- Mathlib.Algebra.Category.Grp.Zero
AddCommGrpCat.isZero_of_subsingleton : ∀ (G : AddCommGrpCat) [Subsingleton ↑G], CategoryTheory.Limits.IsZero G
-- Init.Util
dbgTrace : {α : Type u} → String → (Unit → α) → α
-- Mathlib.Order.Cover
Set.empty_covBy_singleton : ∀ {α : Type u_1} (a : α), ∅ ⋖ {a}
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_center_left : ∀ {G : Type u_1} [inst : Group G] (H : Subgroup G), ⁅Subgroup.center G, H⁆ = ⊥
-- Mathlib.Order.Category.HeytAlg
/-- Turn a morphism in `HeytAlg` back into a `HeytingHom`.  -/
HeytAlg.Hom.hom : {X Y : HeytAlg} → X.Hom Y → HeytingHom ↑X ↑Y
-- Mathlib.RepresentationTheory.Basic
/-- **Alias** of `Representation.coeff_of_leftRegular_of_generator`. -/
Representation.apply_eq_of_leftRegular_eq_of_generator : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [inst_1 : Group G] (g : G),
  (∀ (x : G), x ∈ Subgroup.zpowers g) →
    ∀ (x : MonoidAlgebra k G), ((Representation.leftRegular k G) g) x = x → ∀ (γ : G), x.coeff γ = x.coeff g
-- Lean.Expr
/-- Return `true` if the given expression is a constant of the given name.
Examples:
- `` (.const `Nat []).isConstOf `Nat `` is `true`
- `` (.const `Nat []).isConstOf `False `` is `false`
 -/
Lean.Expr.isConstOf : Lean.Expr → Lean.Name → Bool
-- Init.Data.Array.Basic
Array.ext : ∀ {α : Type u} {xs ys : Array α},
  xs.size = ys.size → (∀ (i : ℕ) (hi₁ : i < xs.size) (hi₂ : i < ys.size), xs[i] = ys[i]) → xs = ys
-- Init.Data.SInt.Lemmas
Int8.add_comm : ∀ (a b : Int8), a + b = b + a
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.throw_StateT : ∀ {m : Type u → Type v} {Pred EPred : Type u} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {ε : Type u_1}
  {α σ : Type u} {epost : EPred} [inst_4 : MonadExceptOf ε m] (err : ε) (post : α → σ → Pred),
  ⦃ Std.Internal.Do.wp (MonadLift.monadLift (MonadExceptOf.throw err)) post epost ⦄ MonadExceptOf.throw err ⦃ post;
    epost ⦄
-- Mathlib.CategoryTheory.ShrinkYoneda
CategoryTheory.shrinkYoneda_map_app_shrinkYonedaObjObjEquiv_symm : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.LocallySmall.{w, v, u} C] {X X' : C}
  {Y : Cᵒᵖ} (f : Opposite.unop Y ⟶ X) (g : X ⟶ X'),
  (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.shrinkYoneda.{w, v, u}.map g).app Y))
      (CategoryTheory.shrinkYonedaObjObjEquiv.symm f) =
    CategoryTheory.shrinkYonedaObjObjEquiv.symm (CategoryTheory.CategoryStruct.comp f g)
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagationsData.brecOn.eq : ∀ {motive : Lean.Meta.Grind.PendingSolverPropagationsData✝ → Sort u}
  (t : Lean.Meta.Grind.PendingSolverPropagationsData✝)
  (F_1 :
    (t : Lean.Meta.Grind.PendingSolverPropagationsData✝) →
      Lean.Meta.Grind.PendingSolverPropagationsData.below✝ t → motive t),
  Lean.Meta.Grind.PendingSolverPropagationsData.brecOn✝ t F_1 =
    F_1 t (Lean.Meta.Grind.PendingSolverPropagationsData.brecOn.go✝ t F_1).2
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
/-- **Alias** of the reverse direction of `Additive.toMul_lt`. -/
Additive.toMul_strictMono : ∀ {α : Type u_1} [inst : Preorder α] {a b : Additive α}, a < b → Additive.toMul a < Additive.toMul b
-- Plausible.Shrinkable
Plausible.BitVec.shrinkable : {n : ℕ} → Plausible.Shrinkable (BitVec n)
-- Mathlib.Data.Finsupp.Lex
Finsupp.lex_lt_of_lt : ∀ {α : Type u_1} {N : Type u_2} [inst : Zero N] [inst_1 : PartialOrder N] (r : α → α → Prop) [IsStrictOrder α r]
  {x y : α →₀ N}, x < y → Pi.Lex r (fun {i} x1 x2 => x1 < x2) ⇑x ⇑y
-- Mathlib.Data.Ordmap.Ordset
Ordset.instSingleton : {α : Type u_1} → [inst : Preorder α] → Singleton α (Ordset α)
-- Mathlib.Algebra.Module.LinearMap.Defs
LinearMap.instFunLike : {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} → FunLike (M →ₛₗ[σ] M₃) M M₃
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.get_getKey? : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a : α} {h : (m.getKey? a).isSome = true}, (m.getKey? a).get h = m.getKey a ⋯
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.Code.dec.injEq : ∀ {pu : Lean.Compiler.LCNF.Purity} (fvarId : Lean.FVarId) (n : ℕ) (check persistent : Bool) (objs? : Option ℕ)
  (k : Lean.Compiler.LCNF.Code pu)
  (h : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_17) (fvarId_1 : Lean.FVarId)
  (n_1 : ℕ) (check_1 persistent_1 : Bool) (objs?_1 : Option ℕ) (k_1 : Lean.Compiler.LCNF.Code pu)
  (h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.impure) Lean.Compiler.LCNF.Alt._auto_17),
  (Lean.Compiler.LCNF.Code.dec fvarId n check persistent objs? k h =
      Lean.Compiler.LCNF.Code.dec fvarId_1 n_1 check_1 persistent_1 objs?_1 k_1 h_1) =
    (fvarId = fvarId_1 ∧ n = n_1 ∧ check = check_1 ∧ persistent = persistent_1 ∧ objs? = objs?_1 ∧ k = k_1)
-- Mathlib.AlgebraicTopology.ModelCategory.Transport
/-- Transport of a model category structure on a category `D` via an equivalence of
categories `e : C ≌ D`. We assume that the category `C` is already endowed
with a `CategoryWithFibrations` instance (and similarly for cofibrations and weak
equivalences), and that the three properties of morphisms (fibrations, cofibrations,
weak equivalences) in `C` coincide with the inverse images by `e.functor : C ⥤ D`
of the corresponding properties of morphisms in `D`.  -/
HomotopicalAlgebra.ModelCategory.transport : {C : Type u_1} →
  {D : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        [inst_2 : HomotopicalAlgebra.ModelCategory D] →
          [inst_3 : HomotopicalAlgebra.CategoryWithCofibrations C] →
            [inst_4 : HomotopicalAlgebra.CategoryWithFibrations C] →
              [inst_5 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] →
                (e : C ≌ D) →
                  HomotopicalAlgebra.cofibrations C = (HomotopicalAlgebra.cofibrations D).inverseImage e.functor →
                    HomotopicalAlgebra.fibrations C = (HomotopicalAlgebra.fibrations D).inverseImage e.functor →
                      HomotopicalAlgebra.weakEquivalences C =
                          (HomotopicalAlgebra.weakEquivalences D).inverseImage e.functor →
                        HomotopicalAlgebra.ModelCategory C
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- If `α` is a weakly locally compact σ-compact space
(e.g., a proper pseudometric space or a compact spaces)
and the uniformity on `β` is pseudometrizable,
then the uniformity on `C(α, β)` is pseudometrizable too.
 -/
ContinuousMap.instIsCountablyGeneratedProdUniformityOfWeaklyLocallyCompactSpaceOfSigmaCompactSpace : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] [WeaklyLocallyCompactSpace α]
  [SigmaCompactSpace α] [(uniformity β).IsCountablyGenerated], (uniformity C(α, β)).IsCountablyGenerated
-- Mathlib.MeasureTheory.Function.LpSeminorm.TriangleInequality
MeasureTheory.MemLp.sub : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} [inst : NormedAddCommGroup E] {p : ENNReal}
  {μ : MeasureTheory.Measure α} {f g : α → E},
  MeasureTheory.MemLp f p μ → MeasureTheory.MemLp g p μ → MeasureTheory.MemLp (f - g) p μ
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintLabel.name : String → Lean.Lsp.InlayHintLabel
-- Mathlib.Algebra.Star.LinearMap
LinearMap.intrinsicStar_zero : ∀ {R : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Semiring R] [inst_1 : InvolutiveStar R]
  [inst_2 : AddCommMonoid E] [inst_3 : Module R E] [inst_4 : StarAddMonoid E] [inst_5 : StarModule R E]
  [inst_6 : AddCommMonoid F] [inst_7 : Module R F] [inst_8 : StarAddMonoid F] [inst_9 : StarModule R F], star 0 = 0
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get_insertMany_list_of_not_mem_of_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {l : List α} {k k' : α},
  cmp k k' = Ordering.eq →
    ∀ {h' : k' ∈ t.insertMany l},
      k ∉ t → List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → k ∈ l → (t.insertMany l).get k' h' = k
-- Init.Data.Array.Lemmas
Array.set_append_left : ∀ {α : Type u_1} {xs ys : Array α} {i : ℕ} {x : α} (h : i < xs.size), (xs ++ ys).set i x ⋯ = xs.set i x h ++ ys
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.ElementarilyEquivalent.theory_model : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type u_1} [inst : L.Structure M] [inst_1 : L.Structure N] {T : L.Theory}
  [MT : M ⊨ T], L.ElementarilyEquivalent M N → N ⊨ T
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueProds.mk : ∀ {G : Type u_1} [inst : Mul G],
  (∀ {A B : Finset G},
      1 < A.card * B.card → ∃ p1 ∈ A ×ˢ B, ∃ p2 ∈ A ×ˢ B, p1 ≠ p2 ∧ UniqueMul A B p1.1 p1.2 ∧ UniqueMul A B p2.1 p2.2) →
    TwoUniqueProds G
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.minView.match_3.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l : Std.DTreeMap.Internal.Impl α β) →
      l.Balanced → Std.DTreeMap.Internal.Impl.BalancedAtRoot l.size r.size → Sort u_3)
  (size : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hl : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced)
  (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size r.size)
  (h_1 :
    (hl : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr : Std.DTreeMap.Internal.Impl.BalancedAtRoot Std.DTreeMap.Internal.Impl.leaf.size r.size) →
        motive Std.DTreeMap.Internal.Impl.leaf hl hlr)
  (h_2 :
    (size : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hl : (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalancedAtRoot (Std.DTreeMap.Internal.Impl.inner size k' v' l' r').size
                    r.size) →
                motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r') hl hlr),
  (match Std.DTreeMap.Internal.Impl.inner size k' v' l' r', hl, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hl, hlr => h_1 hl hlr
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r', hl, hlr => h_2 size k' v' l' r' hl hlr) =
    h_2 size k' v' l' r' hl hlr
-- Init.Data.Vector.Lemmas
Vector.getElem_eq_getElem_reverse : ∀ {α : Type u_1} {n : ℕ} {xs : Vector α n} {i : ℕ} (h : i < n), xs[i] = xs.reverse[n - 1 - i]
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.instIsAnisotropicOfLinearOrderedCommRing : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : Fintype ι] [inst_1 : AddCommGroup M]
  [inst_2 : AddCommGroup N] [inst_3 : CommRing R] [inst_4 : LinearOrder R] [IsStrictOrderedRing R] [inst_6 : Module R M]
  [inst_7 : Module R N] (P : RootPairing ι R M N), P.IsAnisotropic
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.instVAdd.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] {K : Type u_5} [inst_1 : VAdd K β],
  MeasureTheory.SimpleFunc.instVAdd = { vadd := fun k f => MeasureTheory.SimpleFunc.map (fun x => k +ᵥ x) f }
-- Mathlib.SetTheory.ZFC.PSet
/-- Two pre-sets are extensionally equivalent if every element of the first family is extensionally
equivalent to some element of the second family and vice-versa.  -/
PSet.Equiv : PSet.{u_1} → PSet.{u_2} → Prop
-- Mathlib.Algebra.Ring.InjSurj
/-- Pushforward a `RightDistribClass` instance along a surjective function.  -/
Function.Surjective.rightDistribClass : ∀ {R : Type u_1} {S : Type u_2} (f : R → S),
  Function.Surjective f →
    ∀ [inst : Add S] [inst_1 : Mul S] [inst_2 : Mul R] [inst_3 : Add R] [RightDistribClass R],
      (∀ (x y : R), f (x + y) = f x + f y) → (∀ (x y : R), f (x * y) = f x * f y) → RightDistribClass S
-- Mathlib.Algebra.Order.Archimedean.Class
FiniteMulArchimedeanClass.congrOrderIso_symm : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {N : Type u_2}
  [inst_3 : CommGroup N] [inst_4 : LinearOrder N] [inst_5 : IsOrderedMonoid N]
  (e : MulArchimedeanClass M ≃o MulArchimedeanClass N),
  (FiniteMulArchimedeanClass.congrOrderIso e).symm = FiniteMulArchimedeanClass.congrOrderIso e.symm
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.PositiveCompacts.coe_mk : ∀ {α : Type u_1} [inst : TopologicalSpace α] (s : TopologicalSpace.Compacts α) (h : (interior s.carrier).Nonempty),
  ↑{ toCompacts := s, interior_nonempty' := h } = ↑s
-- Init.Data.UInt.Bitwise
UInt32.toUInt16_or : ∀ (a b : UInt32), (a ||| b).toUInt16 = a.toUInt16 ||| b.toUInt16
-- Mathlib.Algebra.Prime.Defs
irreducible_iff_prime : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [IsCancelMulZero M] [DecompositionMonoid M] {a : M},
  Irreducible a ↔ Prime a
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
ContDiffOn.cosh : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {n : WithTop ℕ∞},
  ContDiffOn ℝ n f s → ContDiffOn ℝ n (fun x => Real.cosh (f x)) s
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
/-- The `v`-adic absolute value on `K` extends the `v`-adic absolute value on `R`.  -/
IsDedekindDomain.HeightOneSpectrum.adicAbv_of_algebraMap : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {K : Type u_2} [inst_2 : Field K]
  [inst_3 : Algebra R K] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R) {b : NNReal}
  (hb : 1 < b) (r : R), (v.adicAbv hb) ((algebraMap R K) r) = (v.intAdicAbv hb) r
-- Mathlib.Probability.Distributions.Gaussian.Real
ProbabilityTheory.gaussianReal.eq_1 : ∀ (μ : ℝ) (v : NNReal),
  ProbabilityTheory.gaussianReal μ v =
    if v = 0 then MeasureTheory.Measure.dirac μ
    else MeasureTheory.volume.withDensity (ProbabilityTheory.gaussianPDF μ v)
-- Mathlib.MeasureTheory.Group.FundamentalDomain
MeasureTheory.addFundamentalFrontier_subset : ∀ {G : Type u_1} {α : Type u_3} [inst : AddGroup G] [inst_1 : AddAction G α] {s : Set α},
  MeasureTheory.addFundamentalFrontier G s ⊆ s
-- Mathlib.Topology.Constructions
continuous_uliftUp : ∀ {X : Type u} [inst : TopologicalSpace X], Continuous ULift.up
-- Mathlib.CategoryTheory.Subfunctor.Basic
CategoryTheory.Subfunctor.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F : CategoryTheory.Functor C (Type w)}
  (obj : (U : C) → Set (F.obj U))
  (map : ∀ {U V : C} (i : U ⟶ V), obj U ⊆ ⇑(CategoryTheory.ConcreteCategory.hom (F.map i)) ⁻¹' obj V)
  (obj_1 : (U : C) → Set (F.obj U))
  (map_1 : ∀ {U V : C} (i : U ⟶ V), obj_1 U ⊆ ⇑(CategoryTheory.ConcreteCategory.hom (F.map i)) ⁻¹' obj_1 V),
  ({ obj := obj, map := map } = { obj := obj_1, map := map_1 }) = (obj = obj_1)
-- Std.Time.Format
/-- Parses a `String` in the lean date time format with identifier and returns a `DateTime` object.
 -/
Std.Time.DateTime.fromLeanDateTimeWithIdentifierString : String → Except String Std.Time.DateTime
-- Mathlib.Algebra.DirectSum.LinearMap
LinearMap.trace_eq_sum_trace_restrict' : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {N : ι → Submodule R M} [inst_3 : DecidableEq ι] [∀ (i : ι), Module.Finite R ↥(N i)]
  [∀ (i : ι), Module.Free R ↥(N i)],
  DirectSum.IsInternal N →
    ∀ (hN : {i | N i ≠ ⊥}.Finite) {f : M →ₗ[R] M} (hf : ∀ (i : ι), Set.MapsTo ⇑f ↑(N i) ↑(N i)),
      (LinearMap.trace R M) f = ∑ i ∈ hN.toFinset, (LinearMap.trace R ↥(N i)) (f.restrict ⋯)
-- Mathlib.Algebra.Polynomial.Degree.Operations
Polynomial.zero_notMem_multiset_map_X_sub_C : ∀ {R : Type u} [inst : Ring R] [Nontrivial R] {α : Type u_1} (m : Multiset α) (f : α → R),
  0 ∉ Multiset.map (fun a => Polynomial.X - Polynomial.C (f a)) m
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMonObj.add_zero_hom_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M : C}
  [inst_2 : CategoryTheory.AddMonObj M] {Z : C} (f : Z ⟶ M) {Z_1 : C} (h : M ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.AddMonObj.zero)
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor Z).hom
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Algebra.Order.Floor.Extended
ENat.ceil_add_toENNReal : ∀ (r : ENNReal) (n : ℕ∞), ⌈r + ↑n⌉ₑ = ⌈r⌉ₑ + n
-- Init.Data.UInt.Lemmas
UInt32.lt_iff_le_and_ne : ∀ {a b : UInt32}, a < b ↔ a ≤ b ∧ a ≠ b