mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Elements
/-- The initial object in `F.Elements` if `F` is corepresentable.  -/
CategoryTheory.Functor.Elements.initialOfCorepresentableBy : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {F : CategoryTheory.Functor C (Type u_1)} → {X : C} → F.CorepresentableBy X → F.Elements
-- Aesop.Nanos
Aesop.Nanos.nanos : Aesop.Nanos → ℕ
-- Mathlib.MeasureTheory.Integral.TorusIntegral
torusMap_zero_radius : ∀ {n : ℕ} (c : Fin n → ℂ), torusMap c 0 = Function.const (Fin n → ℝ) c
-- Mathlib.SetTheory.Ordinal.Basic
/-- To prove a result on ordinals, it suffices to prove it for order types of well-orders.  -/
Ordinal.inductionOnWellOrder : ∀ {motive : Ordinal.{u_1} → Prop} (o : Ordinal.{u_1}),
  (∀ (α : Type u_1) [inst : LinearOrder α] [inst_1 : WellFoundedLT α], motive (Ordinal.type fun x1 x2 => x1 < x2)) →
    motive o
-- Mathlib.MeasureTheory.Function.ContinuousMapDense
/-- Any function in `ℒp` can be approximated by bounded continuous functions when `0 < p < ∞`,
version in terms of `∫`.  -/
MeasureTheory.MemLp.exists_boundedContinuous_integral_rpow_sub_le : ∀ {α : Type u_1} [inst : TopologicalSpace α] [NormalSpace α] [inst_2 : MeasurableSpace α] [BorelSpace α] {E : Type u_2}
  [inst_4 : NormedAddCommGroup E] {μ : MeasureTheory.Measure α} [NormedSpace ℝ E] [μ.WeaklyRegular] {p : ℝ},
  0 < p →
    ∀ {f : α → E},
      MeasureTheory.MemLp f (ENNReal.ofReal p) μ →
        ∀ {ε : ℝ}, 0 < ε → ∃ g, ∫ (x : α), ‖f x - g x‖ ^ p ∂μ ≤ ε ∧ MeasureTheory.MemLp (⇑g) (ENNReal.ofReal p) μ
-- Mathlib.MeasureTheory.Measure.Restrict
indicator_ae_eq_zero_of_restrict_ae_eq_zero : ∀ {α : Type u_2} {β : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α} {f : α → β}
  [inst_1 : Zero β], MeasurableSet s → f =ᵐ[μ.restrict s] 0 → s.indicator f =ᵐ[μ] 0
-- Mathlib.Algebra.Order.Interval.Set.Monoid
Set.Ioc_add_bij : ∀ {M : Type u_1} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedCancelAddMonoid M] [ExistsAddOfLE M]
  (a b d : M), Set.BijOn (fun x => x + d) (Set.Ioc a b) (Set.Ioc (a + d) (b + d))
-- Mathlib.CategoryTheory.Monoidal.CommMon_
/-- The underlying object in the ambient monoidal category  -/
CategoryTheory.CommMon.X : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] → CategoryTheory.CommMon C → C
-- Mathlib.Algebra.MonoidAlgebra.Grading
AddMonoidAlgebra.single_mem_grade : ∀ {M : Type u_1} {R : Type u_4} [inst : CommSemiring R] (i : M) (r : R),
  AddMonoidAlgebra.single i r ∈ AddMonoidAlgebra.grade R i
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.add_of_left : ∀ {R : Type u} [inst : Semiring R] {p q : Polynomial R}, p.Monic → q.degree < p.degree → (p + q).Monic
-- Mathlib.Geometry.Manifold.Riemannian.Basic
/-- **Alias** of `setOfPred_riemannianEDist_lt_subset_nhds'`.

---

Any neighborhood of `x` contains all the points which are close enough to `x` for the
Riemannian distance, `ℝ≥0∞` version.  -/
setOf_riemannianEDist_lt_subset_nhds' : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {H : Type u_2} [inst_2 : TopologicalSpace H]
  (I : ModelWithCorners ℝ E H) {M : Type u_3} [inst_3 : TopologicalSpace M] [inst_4 : ChartedSpace H M]
  [inst_5 : Bundle.RiemannianBundle fun x => TangentSpace I x] [inst_6 : IsManifold I 1 M]
  [IsContinuousRiemannianBundle E fun x => TangentSpace I x] [RegularSpace M] {x : M} {s : Set M},
  s ∈ nhds x → ∃ c > 0, {y | Manifold.riemannianEDist I x y < c} ⊆ s
-- Mathlib.Data.Bundle
/-- The base map `f : B' → B` lifts to a canonical map on the total spaces.  -/
Bundle.Pullback.lift : {B : Type u_1} →
  {F : Type u_2} →
    {E : B → Type u_3} → {B' : Type u_4} → (f : B' → B) → Bundle.TotalSpace F (f *ᵖ E) → Bundle.TotalSpace F E
-- Mathlib.Logic.Equiv.Defs
/-- The backward map of an equivalence.

Do NOT use `e.invFun` directly. Use the coercion of `e.symm` instead.  -/
Equiv.invFun : {α : Sort u_1} → {β : Sort u_2} → α ≃ β → β → α
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.SupportsStmt.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} (S : Finset Λ) (a : Γ → σ → Γ) (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1.SupportsStmt S (Turing.TM1.Stmt.write a q) = Turing.TM1.SupportsStmt S q
-- Mathlib.LinearAlgebra.Matrix.Notation
Matrix.vecMul_empty : ∀ {α : Type u} {n' : Type uₙ} [inst : NonUnitalNonAssocSemiring α] [inst_1 : Fintype n'] (v : n' → α)
  (B : Matrix n' (Fin 0) α), Matrix.vecMul v B = ![]
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
/-- If `p` is a prime in a Noetherian ring `R`, there exists a `p`-primary ideal `I`
spanned by `p.height` elements.  -/
Ideal.exists_finset_card_eq_height_of_isNoetherianRing : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] (p : Ideal R) [p.IsPrime],
  ∃ s, p ∈ (Ideal.span ↑s).minimalPrimes ∧ ↑s.card = p.height
-- Mathlib.Tactic.Widget.StringDiagram
/-- The indices of the variable.  -/
Mathlib.Tactic.Widget.StringDiagram.PenroseVar.indices : Mathlib.Tactic.Widget.StringDiagram.PenroseVar → List ℕ
-- Mathlib.Algebra.Group.Commute.Units
AddUnits.leftOfAdd.eq_1 : ∀ {M : Type u_1} [inst : AddMonoid M] (u : AddUnits M) (a b : M) (hu : a + b = ↑u) (hc : AddCommute a b),
  u.leftOfAdd a b hu hc = { val := a, neg := b + ↑(-u), val_neg := ⋯, neg_val := ⋯ }
-- Lean.Meta.Tactic.NormCast
/-- A simp set which lifts coercions to the top level.  -/
Lean.Meta.NormCast.NormCastExtension.up : Lean.Meta.NormCast.NormCastExtension → Lean.Meta.SimpExtension
-- Mathlib.Algebra.BigOperators.Group.List.Basic
/-- This is the `List.prod` version of `mul_inv_rev`  -/
List.prod_inv_reverse : ∀ {G : Type u_7} [inst : Group G] (L : List G), L.prod⁻¹ = (List.map (fun x => x⁻¹) L).reverse.prod
-- Mathlib.CategoryTheory.Localization.Predicate
/-- When `L : C ⥤ D` is a localization functor for `W : MorphismProperty C` and
`F : C ⥤ E` is a functor, we shall say that `F' : D ⥤ E` lifts `F` if the obvious diagram
is commutative up to an isomorphism.  -/
CategoryTheory.Localization.Lifting : {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] →
        {E : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            CategoryTheory.Functor C D →
              CategoryTheory.MorphismProperty C →
                CategoryTheory.Functor C E → CategoryTheory.Functor D E → Type (max u_1 v_3)
-- Mathlib.NumberTheory.Height.NumberField
/-- The set of `a : 𝓞 K` such that `mulHeight₁ (a / n) = mulHeight ![a, n]` is bounded
(for some given nonzero `n : ℕ`) is finite.  -/
NumberField.finite_setOfPred_mulHeight_nat_le : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {n : ℕ},
  n ≠ 0 → ∀ (B : ℝ), {a | Height.mulHeight ![↑a, ↑n] ≤ B}.Finite
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.ClassifyResult.commRing : ℕ → Lean.Meta.Sym.Arith.ClassifyResult
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.HasRightCalculusOfFractions.exists_rightFraction : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {W : CategoryTheory.MorphismProperty C}
  [self : W.HasRightCalculusOfFractions] ⦃X Y : C⦄ (φ : W.LeftFraction X Y),
  ∃ ψ, CategoryTheory.CategoryStruct.comp ψ.s φ.f = CategoryTheory.CategoryStruct.comp ψ.f φ.s
-- Mathlib.SetTheory.Ordinal.CantorNormalForm
Ordinal.CNF.rec_pos : ∀ (b : Ordinal.{u_2}) {o : Ordinal.{u_2}} {C : Ordinal.{u_2} → Sort u_1} (ho : o ≠ 0) (H0 : C 0)
  (H : (o : Ordinal.{u_2}) → o ≠ 0 → C (o % b ^ Ordinal.log b o) → C o),
  Ordinal.CNF.rec b H0 H o = H o ho (Ordinal.CNF.rec b H0 H (o % b ^ Ordinal.log b o))
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.prod.inl.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] (X Y : C)
  [inst_2 : CategoryTheory.Limits.HasBinaryProduct X Y],
  CategoryTheory.Limits.prod.inl X Y = CategoryTheory.Limits.prod.lift (CategoryTheory.CategoryStruct.id X) 0
-- Mathlib.Data.Nat.Basic
Nat.succ_injective : Function.Injective Nat.succ
-- Mathlib.Analysis.Convex.Topology
/-- The closed interior of a simplex is compact.  -/
Affine.Simplex.isCompact_closedInterior : ∀ {𝕜 : Type u_4} {V : Type u_5} {P : Type u_6} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : TopologicalSpace 𝕜] [OrderClosedTopology 𝕜] [CompactIccSpace 𝕜] [ContinuousAdd 𝕜] [inst_7 : AddCommGroup V]
  [inst_8 : TopologicalSpace V] [IsTopologicalAddGroup V] [inst_10 : Module 𝕜 V] [ContinuousSMul 𝕜 V]
  [inst_12 : AddTorsor V P] [inst_13 : TopologicalSpace P] [IsTopologicalAddTorsor P] {n : ℕ}
  (s : Affine.Simplex 𝕜 P n), IsCompact s.closedInterior
-- Mathlib.Analysis.Asymptotics.TVS
LinearMap.isBigOTVS_rev_comp : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {l : Filter α} {f : α → E} (g : E →ₗ[𝕜] F),
  Filter.comap (⇑g) (nhds 0) ≤ nhds 0 → f =O[𝕜; l] (⇑g ∘ f)
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.unopFunctor_map : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) {X Y : CategoryTheory.Comma L.op R.op} (f : X ⟶ Y),
  (CategoryTheory.Comma.unopFunctor L R).map f = Opposite.op { left := f.right.unop, right := f.left.unop, w := ⋯ }
-- Mathlib.Algebra.Category.MonCat.FilteredColimits
CommMonCat.FilteredColimits.forget_preservesFilteredColimits : CategoryTheory.Limits.PreservesFilteredColimits (CategoryTheory.forget CommMonCat)
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.sInf_toSubring : ∀ {K : Type u} [inst : DivisionRing K] (s : Set (Subfield K)), (sInf s).toSubring = ⨅ t ∈ s, t.toSubring
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.negDblY_eq' : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} {P : Fin 3 → R},
  W'.Equation P →
    W'.negDblY P * P 2 ^ 2 =
      -(MvPolynomial.eval P) W'.polynomialX *
          ((MvPolynomial.eval P) W'.polynomialX ^ 2 -
                  W'.a₁ * (MvPolynomial.eval P) W'.polynomialX * P 2 * (P 1 - W'.negY P) -
                W'.a₂ * P 2 ^ 2 * (P 1 - W'.negY P) ^ 2 -
              2 * P 0 * P 2 * (P 1 - W'.negY P) ^ 2 -
            P 0 * P 2 * (P 1 - W'.negY P) ^ 2) +
        P 1 * P 2 ^ 2 * (P 1 - W'.negY P) ^ 3
-- Mathlib.Data.Set.Pairwise.Lattice
/-- **Alias** of `Set.biUnion_sdiff_biUnion_eq`. -/
Set.biUnion_diff_biUnion_eq : ∀ {α : Type u_1} {ι : Type u_2} {s t : Set ι} {f : ι → Set α},
  (s ∪ t).PairwiseDisjoint f → (⋃ i ∈ s, f i) \ ⋃ i ∈ t, f i = ⋃ i ∈ s \ t, f i
-- Mathlib.Data.Complex.Basic
Complex.im_mul_ofReal : ∀ (z : ℂ) (r : ℝ), (z * ↑r).im = z.im * r
-- Mathlib.Analysis.Convex.Continuous
ConvexOn.exists_lipschitzOnWith_of_isBounded : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {x₀ : E} {r r' : ℝ},
  ConvexOn ℝ (Metric.ball x₀ r) f →
    r' < r → Bornology.IsBounded (f '' Metric.ball x₀ r) → ∃ K, LipschitzOnWith K f (Metric.ball x₀ r')
-- Mathlib.Tactic.WLOG
/-- The `reductionGoal` requires showing that the case `h : ¬ P` can be reduced to the case where
`P` holds. It has two additional assumptions in its context:

* `h : ¬ P`: the assumption that `P` does not hold
* `H`: the statement that in the original context `P` suffices to prove the goal.
 -/
Mathlib.Tactic.WLOGResult.reductionGoal : Mathlib.Tactic.WLOGResult → Lean.MVarId
-- Mathlib.RingTheory.Coalgebra.Convolution
LinearMap.instSMulCommClassWithConvId : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} {C : Type u_5} [inst : CommSemiring R]
  [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A] [inst_3 : SMulCommClass R A A]
  [inst_4 : IsScalarTower R A A] [inst_5 : AddCommMonoid C] [inst_6 : Module R C] [inst_7 : CoalgebraStruct R C]
  [inst_8 : Monoid S] [inst_9 : DistribMulAction S A] [inst_10 : SMulCommClass R S A] [SMulCommClass S A A],
  SMulCommClass S (WithConv (C →ₗ[R] A)) (WithConv (C →ₗ[R] A))
-- Std.Data.HashMap.Lemmas
Std.HashMap.getD_eq_fallback_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α}
  {fallback : β}, m.contains a = false → m.getD a fallback = fallback
-- Mathlib.CategoryTheory.Triangulated.SpectralObject
CategoryTheory.Triangulated.SpectralObject.ω₂_map_hom₃ : ∀ {C : Type u_1} {ι : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] [inst_2 : CategoryTheory.Limits.HasZeroObject C]
  [inst_3 : CategoryTheory.HasShift C ℤ] [inst_4 : CategoryTheory.Preadditive C]
  [inst_5 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_6 : CategoryTheory.Pretriangulated C]
  (X : CategoryTheory.Triangulated.SpectralObject C ι) {X_1 Y : CategoryTheory.ComposableArrows ι 2} (φ : X_1 ⟶ Y),
  (X.ω₂.map φ).hom₃ = X.ω₁.map (CategoryTheory.ComposableArrows.homMk₁ (φ.app 1) (φ.app ⟨2, ⋯⟩) ⋯)
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.isoWhiskerRight_twice : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] {B : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} B] {H K : CategoryTheory.Functor B C} (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (α : H ≅ K),
  CategoryTheory.Functor.isoWhiskerRight (CategoryTheory.Functor.isoWhiskerRight α F) G =
    H.associator F G ≪≫ CategoryTheory.Functor.isoWhiskerRight α (F.comp G) ≪≫ (K.associator F G).symm
-- Mathlib.Topology.ContinuousMap.Interval
/-- The concatenation of two continuous maps defined on adjacent intervals. If the values of the
functions on the common bound do not agree, this is defined as an arbitrarily chosen constant
map. See `concatCM` for the corresponding map on the subtype of compatible function pairs.  -/
ContinuousMap.concat : {α : Type u_1} →
  [inst : LinearOrder α] →
    [inst_1 : TopologicalSpace α] →
      [OrderTopology α] →
        {a b c : α} →
          [Fact (a ≤ b)] →
            [Fact (b ≤ c)] →
              {E : Type u_2} →
                [inst_5 : TopologicalSpace E] → C(↑(Set.Icc a b), E) → C(↑(Set.Icc b c), E) → C(↑(Set.Icc a c), E)
-- Mathlib.NumberTheory.JacobiSum.Basic
/-- If `1` is the trivial multiplicative character on a finite field `F`, then `J(1,1) = #F-2`.  -/
jacobiSum_one_one : ∀ {F : Type u_1} {R : Type u_2} [inst : Field F] [inst_1 : Fintype F] [inst_2 : CommRing R],
  jacobiSum 1 1 = ↑(Fintype.card F) - 2
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.Equivalence.mapAddGrp_counitIso : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (e : C ≌ D) [inst_4 : e.functor.Monoidal] [inst_5 : e.inverse.Monoidal],
  e.mapAddGrp.counitIso =
    CategoryTheory.Functor.mapAddGrpCompIso.symm ≪≫
      CategoryTheory.Functor.mapAddGrpNatIso e.counitIso ≪≫ CategoryTheory.Functor.mapAddGrpIdIso
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- Uniform space structure on `C(α, β)`.

The uniformity comes from `α →ᵤ[{K | IsCompact K}] β` (i.e., `UniformOnFun α β {K | IsCompact K}`)
which defines topology of uniform convergence on compact sets.
We use `ContinuousMap.tendsto_iff_forall_isCompact_tendstoUniformlyOn`
to show that the induced topology agrees with the compact-open topology
and replace the topology with `compactOpen` to avoid non-defeq diamonds,
see Note [forgetful inheritance].  -/
ContinuousMap.compactConvergenceUniformSpace : {α : Type u₁} → {β : Type u₂} → [inst : TopologicalSpace α] → [inst_1 : UniformSpace β] → UniformSpace C(α, β)
-- Mathlib.Algebra.Star.SelfAdjoint
IsStarNormal.neg : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : StarAddMonoid R] {x : R} [IsStarNormal x], IsStarNormal (-x)
-- Mathlib.NumberTheory.Zsqrtd.GaussianInt
GaussianInt.abs_natCast_norm : ∀ (x : GaussianInt), ↑(Zsqrtd.norm x).natAbs = Zsqrtd.norm x
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.trans_apply : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} {C : Type u_5} [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] [inst_8 : Add C]
  [inst_9 : Mul C] [inst_10 : SMul R C] [inst_11 : Star C] (e₁ : A ≃⋆ₐ[R] B) (e₂ : B ≃⋆ₐ[R] C) (x : A),
  (e₁.trans e₂) x = e₂ (e₁ x)
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertMin.match_3.congr_eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Sort u_3)
  (t : Std.DTreeMap.Internal.Impl α β) (hr : t.Balanced)
  (h_1 : (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr)
  (hr_1 : Std.DTreeMap.Internal.Impl.leaf.Balanced),
  t = Std.DTreeMap.Internal.Impl.leaf →
    hr ≍ hr_1 →
      (match t, hr with
        | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr
        | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hr => h_2 sz k' v' l' r' hr) ≍
        h_1 hr_1
-- Mathlib.Algebra.Ring.Action.Rat
NNRat.instIsScalarTowerRight : ∀ {R : Type u_1} [inst : DivisionSemiring R], IsScalarTower ℚ≥0 R R
-- Mathlib.Data.Rat.Cast.Defs
NNRat.cast_div_of_ne_zero : ∀ {α : Type u_3} [inst : DivisionSemiring α] {q r : ℚ≥0}, ↑q.den ≠ 0 → ↑r.num ≠ 0 → ↑(q / r) = ↑q / ↑r
-- Mathlib.Analysis.Calculus.Deriv.Basic
norm_deriv_eq_norm_fderiv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : NormedAddCommGroup F]
  [inst_2 : NormedSpace 𝕜 F] {f : 𝕜 → F} {x : 𝕜}, ‖deriv f x‖ = ‖fderiv 𝕜 f x‖
-- Init.Control.Lawful.MonadLift.Instances
Id.instLawfulMonadLiftTOfLawfulMonad : ∀ {m : Type u → Type v} [inst : Monad m] [LawfulMonad m], LawfulMonadLiftT Id m
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.replicate.injEq : ∀ {w w' : ℕ} (n : ℕ) (expr : Std.Tactic.BVDecide.BVExpr w) (h : w' = w * n) (w_1 n_1 : ℕ)
  (expr_1 : Std.Tactic.BVDecide.BVExpr w_1) (h_1 : w' = w_1 * n_1),
  (Std.Tactic.BVDecide.BVExpr.replicate n expr h = Std.Tactic.BVDecide.BVExpr.replicate n_1 expr_1 h_1) =
    (w = w_1 ∧ n = n_1 ∧ expr ≍ expr_1)
-- Mathlib.Analysis.Normed.Module.RCLike.Basic
RCLike.norm_coe_norm : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] {z : E}, ‖↑‖z‖‖ = ‖z‖
-- Mathlib.Data.Prod.Basic
Prod.map_iterate : ∀ {α : Type u_1} {β : Type u_2} (f : α → α) (g : β → β) (n : ℕ), (Prod.map f g)^[n] = Prod.map f^[n] g^[n]
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.intercalate.go.eq_2 : ∀ (acc s : String), String.intercalate.go✝ acc s [] = acc
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
WeierstrassCurve.Projective.addXYZ_Z : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (P Q : Fin 3 → R), W'.addXYZ P Q 2 = W'.addZ P Q
-- Init.Data.String.Iterator
/-- The string being iterated over.  -/
String.Legacy.Iterator.s : String.Legacy.Iterator → String
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.coe_le_coe : ∀ {X : Type u_1} {R : Type u_2} [inst : Zero R] [inst_1 : Add R] [inst_2 : LE R] {d d' : PseudoMetric X R},
  ⇑d ≤ ⇑d' ↔ d ≤ d'
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeAddGroup.Red.Step.sublist : ∀ {α : Type u} {L₁ L₂ : List (α × Bool)}, FreeAddGroup.Red.Step L₁ L₂ → L₂.Sublist L₁
-- Mathlib.CategoryTheory.NatTrans
/-- The naturality square for a given morphism.  -/
CategoryTheory.NatTrans.naturality : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (self : CategoryTheory.NatTrans F G) ⦃X Y : C⦄ (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp (F.map f) (self.app Y) = CategoryTheory.CategoryStruct.comp (self.app X) (G.map f)
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.eq_inv_iff_mul_eq_one : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] {φ ψ : MvPowerSeries σ k},
  MvPowerSeries.constantCoeff ψ ≠ 0 → (φ = ψ⁻¹ ↔ φ * ψ = 1)
-- Mathlib.Data.Set.Insert
/-- **Alias** of the reverse direction of `Set.singleton_inter_eq_empty`. -/
Set.singleton_inter_of_notMem : ∀ {α : Type u_1} {s : Set α} {a : α}, a ∉ s → {a} ∩ s = ∅
-- Mathlib.Order.ConditionallyCompleteLattice.Defs
conditionallyCompleteLatticeOfsInf.eq_1 : ∀ (α : Type u_5) [H1 : PartialOrder α] [H2 : InfSet α] (bddBelow_pair : ∀ (a b : α), BddAbove {a, b})
  (bddAbove_pair : ∀ (a b : α), BddBelow {a, b})
  (isLUB_sSup : ∀ (s : Set α), BddBelow s → s.Nonempty → IsGLB s (sInf s)),
  conditionallyCompleteLatticeOfsInf α bddBelow_pair bddAbove_pair isLUB_sSup =
    { toLattice := Lattice.ofIsLUBofIsGLB (fun a b => sInf (upperBounds {a, b})) (fun a b => sInf {a, b}) ⋯ ⋯,
      sSup := fun s => sInf (upperBounds s), toInfSet := H2, isLUB_csSup := ⋯, isGLB_csInf := ⋯ }
-- Lean.Parser.Term.Basic
Lean.Parser.Term.optIdent.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.expMapBasis_nonneg : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : NumberField.mixedEmbedding.realSpace K)
  (w : NumberField.InfinitePlace K), 0 ≤ ↑NumberField.mixedEmbedding.fundamentalCone.expMapBasis x w
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
/-- The data which allows to construct an `E₂`-cohomological spectral sequence
indexed by `ℤ × Fin l` from a spectral object indexed by `Fin (l + 1)`.  -/
CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalFin : (l : ℕ) →
  CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore (Fin (l + 1))
    (fun r => ComplexShape.spectralSequenceFin l (r, 1 - r)) 2
-- Mathlib.Order.WithBot
/-- **Alias** of the reverse direction of `WithBot.unbot_le_unbot_iff`. -/
WithBot.unbot_mono : ∀ {α : Type u_1} [inst : LE α] {x y : WithBot α} (hx : x ≠ ⊥) (hy : y ≠ ⊥), x ≤ y → x.unbot hx ≤ y.unbot hy
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.strictAntiOn_rpow_Ioi_of_exponent_neg : ∀ {r : ℝ}, r < 0 → StrictAntiOn (fun x => x ^ r) (Set.Ioi 0)
-- Mathlib.Order.Defs.Unbundled
/-- A version of `antisymm` with `r` explicit.

This lemma matches the lemmas from lean core in `Init.Algebra.Classes`, but is missing there.  -/
antisymm_of : ∀ {α : Sort u_1} (r : α → α → Prop) [Std.Antisymm r] {a b : α}, r a b → r b a → a = b
-- Mathlib.FieldTheory.PurelyInseparable.Basic
isPurelyInseparable_iff : ∀ {F : Type u_1} {E : Type u_2} [inst : CommRing F] [inst_1 : Ring E] [inst_2 : Algebra F E],
  IsPurelyInseparable F E ↔ ∀ (x : E), IsIntegral F x ∧ (IsSeparable F x → x ∈ (algebraMap F E).range)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.cancelVar : ℤ → Lean.Grind.CommRing.Var → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly