mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.BoxIntegral.DivergenceTheorem
/-- If `f : ℝⁿ⁺¹ → E` is differentiable on a closed rectangular box `I` with derivative `f'`, then
the partial derivative `fun x ↦ f' x (Pi.single i 1)` is Henstock-Kurzweil integrable with integral
equal to the difference of integrals of `f` over the faces `x i = I.upper i` and `x i = I.lower i`.

More precisely, we use a non-standard generalization of the Henstock-Kurzweil integral and
we allow `f` to be non-differentiable (but still continuous) at a countable set of points.

TODO: If `n > 0`, then the condition at `x ∈ s` can be replaced by a much weaker estimate but this
requires either better integrability theorems, or usage of a filter depending on the countable set
`s` (we need to ensure that none of the faces of a partition contain a point from `s`).  -/
BoxIntegral.hasIntegral_GP_pderiv : ∀ {E : Type u} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {n : ℕ} [CompleteSpace E]
  (I : BoxIntegral.Box (Fin (n + 1))) (f : (Fin (n + 1) → ℝ) → E) (f' : (Fin (n + 1) → ℝ) → (Fin (n + 1) → ℝ) →L[ℝ] E)
  (s : Set (Fin (n + 1) → ℝ)),
  s.Countable →
    (∀ x ∈ s, ContinuousWithinAt f (BoxIntegral.Box.Icc I) x) →
      (∀ x ∈ BoxIntegral.Box.Icc I \ s, HasFDerivWithinAt f (f' x) (BoxIntegral.Box.Icc I) x) →
        ∀ (i : Fin (n + 1)),
          BoxIntegral.HasIntegral I BoxIntegral.IntegrationParams.GP (fun x => (f' x) (Pi.single i 1))
            BoxIntegral.BoxAdditiveMap.volume
            (BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP (fun x => f (i.insertNth (I.upper i) x))
                BoxIntegral.BoxAdditiveMap.volume -
              BoxIntegral.integral (I.face i) BoxIntegral.IntegrationParams.GP (fun x => f (i.insertNth (I.lower i) x))
                BoxIntegral.BoxAdditiveMap.volume)
-- Std.Internal.UV.TCP
/-- Enables the Nagle algorithm for a TCP socket.
 -/
Std.Internal.UV.TCP.Socket.noDelay : Std.Internal.UV.TCP.Socket → IO Unit
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.diagonal_hadamard_eq_diagonal_iff : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : MulZeroClass α] {A : Matrix n n α} {d e : n → α},
  (Matrix.diagonal d).hadamard A = Matrix.diagonal e ↔ d * A.diag = e
-- Mathlib.LinearAlgebra.CliffordAlgebra.Equivs
CliffordAlgebraRing.reverse_apply : ∀ {R : Type u_1} [inst : CommRing R] (x : CliffordAlgebra 0), CliffordAlgebra.reverse x = x
-- Mathlib.CategoryTheory.MorphismProperty.Local
CategoryTheory.MorphismProperty.IsLocalAtTarget.of_isPullback : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.MorphismProperty C}
  {K : CategoryTheory.Precoverage C} [P.IsLocalAtTarget K] {X Y : C} {f : X ⟶ Y} (𝒰 : K.ZeroHypercover Y) {X' : C}
  (i : 𝒰.I₀) {fst : X' ⟶ X} {snd : X' ⟶ 𝒰.X i}, CategoryTheory.IsPullback fst snd f (𝒰.f i) → P f → P snd
-- Lean.Elab.Tactic.Grind.Main
Lean.Elab.Tactic.evalLia : Lean.Elab.Tactic.Tactic
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.Grpd.freeForgetAdjunction_homEquiv_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{u, u} C] {D : Type u} [inst_1 : CategoryTheory.Groupoid D]
  (F : CategoryTheory.Functor (CategoryTheory.FreeGroupoid C) D),
  ((CategoryTheory.Grpd.freeForgetAdjunction.homEquiv (CategoryTheory.Cat.of C) (CategoryTheory.Grpd.of D))
        F).toFunctor =
    (CategoryTheory.FreeGroupoid.of C).comp F
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.maxKey_insert : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v).maxKey ⋯ = t.maxKey?.elim k fun k' => if (cmp k' k).isLE = true then k else k'
-- Mathlib.GroupTheory.GroupAction.Quotient
MulAction.coe_quotient_smul : ∀ {G : Type u} {X : Type v} [inst : Group G] {H : Subgroup G} [inst_1 : H.Normal] [inst_2 : SMul G X]
  [inst_3 : MulAction (G ⧸ H) X] [IsScalarTower G (G ⧸ H) X] (g : G) (x : X), ↑g • x = g • x
-- Mathlib.Combinatorics.SimpleGraph.Prod
SimpleGraph.Walk.ofBoxProdLeft.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {G : SimpleGraph α} {H : SimpleGraph β} [inst : DecidableEq β]
  [inst_1 : DecidableRel G.Adj] {x : α × β}, SimpleGraph.Walk.nil.ofBoxProdLeft = SimpleGraph.Walk.nil
-- Mathlib.Order.Filter.IsBounded
Monotone.isBoundedUnder_ge_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] {l : Filter γ} {u : γ → α}
  {v : α → β},
  Monotone v → Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l u → Filter.IsBoundedUnder (fun x1 x2 => x2 ≤ x1) l (v ∘ u)
-- Mathlib.Algebra.BigOperators.Fin
Fin.sum_univ_four : ∀ {M : Type u_2} [inst : AddCommMonoid M] (f : Fin 4 → M), ∑ i, f i = f 0 + f 1 + f 2 + f 3
-- Std.Data.Iterators.Lemmas.Combinators.Zip
_private.Std.Data.Iterators.Lemmas.Combinators.Zip.0.Std.Iter.atIdxSlow?.match_1.splitter : {α β : Type u_1} →
  [inst : Std.Iterator α Id β] →
    (it : Std.Iter β) →
      (motive :
          (n : ℕ) →
            ((a' : Std.Iter β) →
                (b' : ℕ) →
                  InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                      (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, n⟩ →
                    Option β) →
              Sort u_2) →
        (n : ℕ) →
          (recur :
              (a' : Std.Iter β) →
                (b' : ℕ) →
                  InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                      (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, n⟩ →
                    Option β) →
            ((recur :
                  (a' : Std.Iter β) →
                    (b' : ℕ) →
                      InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                          (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, 0⟩ →
                        Option β) →
                motive 0 recur) →
              ((k : ℕ) →
                  (recur :
                      (a' : Std.Iter β) →
                        (b' : ℕ) →
                          InvImage (Prod.Lex WellFoundedRelation.rel Std.IterM.TerminationMeasures.Productive.Rel)
                              (fun p => (p.snd, p.fst.finitelyManySkips!)) ⟨a', b'⟩ ⟨it, k + 1⟩ →
                            Option β) →
                    motive k.succ recur) →
                motive n recur
-- Init.Core
not_of_not_imp : ∀ {b a : Prop}, ¬(a → b) → ¬b
-- Init.Data.Array.Lemmas
_private.Init.Data.Array.Lemmas.0.Array.filterMapM.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (b : β) (h_1 : (b : β) → motive (some b)) (h_2 : Unit → motive none),
  (match some b with
    | some b => h_1 b
    | none => h_2 ()) =
    h_1 b
-- Mathlib.Data.Multiset.Bind
Multiset.map_swap_product : ∀ {α : Type u_1} {β : Type v} (s : Multiset α) (t : Multiset β), Multiset.map Prod.swap (s ×ˢ t) = t ×ˢ s
-- Lean.MetavarContext
Lean.MetavarContext.LevelMVarToParam.State.nextParamIdx : Lean.MetavarContext.LevelMVarToParam.State → ℕ
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKeyD_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k k' fallback : α} {f : β k → β k},
  (t.modify k f).getKeyD k' fallback =
    if cmp k k' = Ordering.eq then if k ∈ t then k else fallback else t.getKeyD k' fallback
-- Mathlib.Algebra.Order.SuccPred
strictMonoOn_of_lt_add_one : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] [inst_2 : Add α] [inst_3 : One α]
  [inst_4 : SuccAddOrder α] [IsSuccArchimedean α] {s : Set α} {f : α → β},
  s.OrdConnected → (∀ (a : α), ¬IsMax a → a ∈ s → a + 1 ∈ s → f a < f (a + 1)) → StrictMonoOn f s
-- Mathlib.CategoryTheory.Sites.LocallyFullyFaithful
CategoryTheory.Sieve.equalizer_self : ∀ {C : Type uC} [inst : CategoryTheory.Category.{vC, uC} C] {U V : C} (f : U ⟶ V),
  CategoryTheory.Sieve.equalizer f f = ⊤
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.whiskerLeft_actionHomLeft_assoc : ∀ {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 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) {c' c'' : C} (f : c' ⟶ c'') (d : D) {Z : D}
  (h :
    CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj
        (CategoryTheory.MonoidalCategoryStruct.tensorObj c c'') d ⟶
      Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft c f) d)
      h =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c' d).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomLeft f d))
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionAssocIso c c'' d).inv h))
-- Batteries.Data.UnionFind.Lemmas
Batteries.UnionFind.arr_push : ∀ {m : Batteries.UnionFind}, m.push.arr = m.arr.push { parent := m.arr.size, rank := 0 }
-- Mathlib.RingTheory.Ideal.Maps
/-- If `f : R ≃+* S` is a ring isomorphism and `I : Ideal R`, then `map f.symm I = comap f I`.  -/
Ideal.map_symm : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {I : Ideal S} (f : R ≃+* S),
  Ideal.map f.symm I = Ideal.comap f I
-- Mathlib.Order.Filter.Basic
Filter.sup_principal : ∀ {α : Type u} {s t : Set α}, Filter.principal s ⊔ Filter.principal t = Filter.principal (s ∪ t)
-- Init.Prelude
Lean.instInhabitedSyntax : Inhabited Lean.Syntax
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.relabel_id : ∀ {α : Type u_1} {x : Std.Sat.CNF α}, Std.Sat.CNF.relabel id x = x
-- Mathlib.AlgebraicTopology.SimplicialObject.Split
CategoryTheory.SimplicialObject.Splitting.IndexSet.id.eq_1 : ∀ (Δ : SimplexCategoryᵒᵖ),
  CategoryTheory.SimplicialObject.Splitting.IndexSet.id Δ = ⟨Δ, ⟨CategoryTheory.CategoryStruct.id (Opposite.unop Δ), ⋯⟩⟩
-- Mathlib.Combinatorics.Matroid.Rank.Cardinal
/-- A class stating that cardinality-valued rank is well-defined
(i.e. all bases are equicardinal) for a matroid `M` and its minors.
Notably, this holds for `Finitary` matroids; see `Matroid.invariantCardinalRank_of_finitary`.  -/
Matroid.InvariantCardinalRank : {α : Type u} → Matroid α → Prop
-- Mathlib.Analysis.Convex.Deriv
/-- If a function `f` is continuous on a convex set `D ⊆ ℝ`, is twice differentiable on its
interior, and `f''` is nonpositive on the interior, then `f` is concave on `D`.  -/
concaveOn_of_deriv2_nonpos : ∀ {D : Set ℝ},
  Convex ℝ D →
    ∀ {f : ℝ → ℝ},
      ContinuousOn f D →
        DifferentiableOn ℝ f (interior D) →
          DifferentiableOn ℝ (deriv f) (interior D) → (∀ x ∈ interior D, deriv^[2] f x ≤ 0) → ConcaveOn ℝ D f
-- Mathlib.RingTheory.PowerSeries.Exp
PowerSeries.exp.eq_1 : ∀ (A : Type u_1) [inst : Ring A] [inst_1 : Algebra ℚ A],
  PowerSeries.exp A = PowerSeries.mk fun n => (algebraMap ℚ A) (1 / ↑n.factorial)
-- Aesop.RuleSet.Member
Aesop.instInhabitedLocalRuleSetMember.default : Aesop.LocalRuleSetMember
-- Mathlib.CategoryTheory.Join.Opposites
CategoryTheory.Join.opEquiv_functor_obj_op_left : ∀ {C : Type u₁} (D : Type u₂) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (c : C),
  (CategoryTheory.Join.opEquiv C D).functor.obj (Opposite.op (CategoryTheory.Join.left c)) =
    CategoryTheory.Join.right (Opposite.op c)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKeyD_filter : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  [inst_2 : LawfulBEq α] {f : (a : α) → β a → Bool} {k fallback : α} (h : (↑m).WF),
  (Std.DHashMap.Internal.Raw₀.filter f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x h' => f x (m.get x ⋯)).getD fallback
-- Aesop.RuleTac.RuleTerm
Aesop.ElabRuleTerm.ofElaboratedTerm : Lean.Term → Lean.Expr → Aesop.ElabRuleTerm
-- Mathlib.MeasureTheory.VectorMeasure.Variation.Defs
/-- The variation of a `VectorMeasure` as an `ℝ≥0∞`-valued `VectorMeasure`.  -/
MeasureTheory.VectorMeasure.ennrealVariation : {X : Type u_1} →
  {mX : MeasurableSpace X} →
    {V : Type u_2} →
      [inst : TopologicalSpace V] →
        [inst_1 : ENormedAddCommMonoid V] →
          [T2Space V] → MeasureTheory.VectorMeasure X V → MeasureTheory.VectorMeasure X ENNReal
-- Init.Data.Dyadic.Inv
/-- If `y : Dyadic` has precision at most `prec` and a rational `q` lies in the half-open
interval `[y.toRat, y.toRat + 2 ^ (-prec))`, then `y` is the floor of `q` at precision
`prec`, i.e. `y = q.toDyadic prec`.
 -/
Dyadic.eq_toDyadic_of_precision_le : ∀ {q : ℚ} {y : Dyadic} {prec : ℤ},
  y.precision ≤ some prec → y.toRat ≤ q → q < y.toRat + 2 ^ (-prec) → y = q.toDyadic prec
-- Mathlib.LinearAlgebra.Prod
LinearMap.coprod_zero_left : ∀ {R : Type u} {M : Type v} {M₂ : Type w} {M₃ : Type y} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃] [inst_4 : Module R M] [inst_5 : Module R M₂]
  [inst_6 : Module R M₃] (g : M₂ →ₗ[R] M₃), LinearMap.coprod 0 g = g ∘ₗ LinearMap.snd R M M₂
-- Mathlib.GroupTheory.Complement
Subgroup.isComplement_subgroup_right_iff_bijective : ∀ {G : Type u_1} [inst : Group G] {H : Subgroup G} {S : Set G},
  Subgroup.IsComplement S ↑H ↔ Function.Bijective (S.domRestrict QuotientGroup.mk)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.isNone_maxKey?_eq_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp],
  t.maxKey?.isNone = t.isEmpty
-- Mathlib.CategoryTheory.IsConnected
CategoryTheory.Zigzag.of_hom_inv : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {j₁ j₂ j₃ : J} (f₁₂ : j₁ ⟶ j₂) (f₃₂ : j₃ ⟶ j₂),
  CategoryTheory.Zigzag j₁ j₃
-- Mathlib.SetTheory.ZFC.Ordinal
Ordinal.mem_toZFSet_iff : ∀ {o : Ordinal.{u_1}} {x : ZFSet.{u_1}}, x ∈ o.toZFSet ↔ ∃ a < o, a.toZFSet = x
-- Mathlib.Analysis.Complex.UpperHalfPlane.Metric
UpperHalfPlane.image_coe_closedBall : ∀ (z : UpperHalfPlane) (r : ℝ),
  UpperHalfPlane.coe '' Metric.closedBall z r = Metric.closedBall (↑(z.center r)) (z.im * Real.sinh r)
-- Lean.Elab.DeclModifiers
/-- The docstring.  -/
Lean.Elab.ExpandDeclIdResult.docString? : Lean.Elab.ExpandDeclIdResult → Option (Lean.TSyntax `Lean.Parser.Command.docComment)
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- Structure groupoids are stable under composition.  -/
StructureGroupoid.trans' : ∀ {H : Type u_2} [inst : TopologicalSpace H] (self : StructureGroupoid H) (e e' : OpenPartialHomeomorph H H),
  e ∈ self.members → e' ∈ self.members → e.trans e' ∈ self.members
-- Mathlib.Data.ENat.Basic
ENat.natCast_one : ↑1 = 1
-- Mathlib.Logic.Small.Set
small_iInter' : ∀ {α : Type u1} {ι : Type u4} [Nonempty ι] (s : ι → Set α) [∀ (i : ι), Small.{u, u1} ↑(s i)], Small.{u, u1} ↑(⋂ i, s i)
-- Mathlib.GroupTheory.Coprod.Basic
AddMonoid.Coprod.swap_swap : ∀ {M : Type u_1} {N : Type u_2} [inst : AddZeroClass M] [inst_1 : AddZeroClass N] (x : AddMonoid.Coprod M N),
  (AddMonoid.Coprod.swap N M) ((AddMonoid.Coprod.swap M N) x) = x
-- Mathlib.RingTheory.Localization.AtPrime.Basic
/-- A predicate expressing that `Localization.AtPrime P` is an algebra over `Localization.AtPrime p`
in the natural way when `P` lies over `p`.  -/
Localization.AtPrime.IsLiesOverAlgebra : {A : Type u_4} →
  {B : Type u_5} →
    [inst : CommSemiring A] →
      [inst_1 : CommSemiring B] →
        [inst_2 : Algebra A B] →
          (p : Ideal A) →
            [inst_3 : p.IsPrime] →
              (P : Ideal B) →
                [inst_4 : P.IsPrime] →
                  [P.LiesOver p] → [Algebra (Localization.AtPrime p) (Localization.AtPrime P)] → Prop
-- Mathlib.CategoryTheory.Localization.Resolution
CategoryTheory.LocalizerMorphism.RightResolution.id_f : ∀ {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₂}
  (R : Φ.RightResolution X₂), (CategoryTheory.CategoryStruct.id R).f = CategoryTheory.CategoryStruct.id R.X₁
-- Mathlib.GroupTheory.CoprodI
Monoid.CoprodI.Word.prod_smul : ∀ {ι : Type u_1} {M : ι → Type u_2} [inst : (i : ι) → Monoid (M i)] [inst_1 : DecidableEq ι]
  [inst_2 : (i : ι) → DecidableEq (M i)] (m : Monoid.CoprodI M) (w : Monoid.CoprodI.Word M), (m • w).prod = m * w.prod
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceLErase.match_5.eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (rs : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β)
  (motive :
    (l_1 : Std.DTreeMap.Internal.Impl α β) →
      l_1.Balanced →
        Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l_1.size (Std.DTreeMap.Internal.Impl.inner rs k v l r).size →
          Sort u_3)
  (ls : ℕ) (lk : α) (lv : β lk) (ll lr : Std.DTreeMap.Internal.Impl α β)
  (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced)
  (hlr :
    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
      (Std.DTreeMap.Internal.Impl.inner rs k v l r).size)
  (h_1 :
    (hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
      (hlr :
          Std.DTreeMap.Internal.Impl.BalanceLErasePrecond Std.DTreeMap.Internal.Impl.leaf.size
            (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
        motive Std.DTreeMap.Internal.Impl.leaf hlb hlr)
  (h_2 :
    (ls : ℕ) →
      (lk : α) →
        (lv : β lk) →
          (ll lr : Std.DTreeMap.Internal.Impl α β) →
            (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced) →
              (hlr :
                  Std.DTreeMap.Internal.Impl.BalanceLErasePrecond (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                    (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) hlb hlr),
  (match Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr, hlb, hlr with
    | Std.DTreeMap.Internal.Impl.leaf, hlb, hlr => h_1 hlb hlr
    | Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr, hlb, hlr => h_2 ls lk lv ll lr hlb hlr) =
    h_2 ls lk lv ll lr hlb hlr
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
tsub_add_eq_add_tsub : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α} [AddLeftReflectLE α], b ≤ a → a - b + c = a + c - b
-- Mathlib.RingTheory.Regular.IsSMulRegular
IsSMulRegular.isSMulRegular_on_quot_iff_smul_top_inf_eq_smul : ∀ {R : Type u_1} {M : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (N : Submodule R M)
  {r : R}, IsSMulRegular M r → (IsSMulRegular (M ⧸ N) r ↔ r • ⊤ ⊓ N ≤ r • N)
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenAddSubgroup.mem_inf : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] {U V : OpenAddSubgroup G} {x : G},
  x ∈ U ⊓ V ↔ x ∈ U ∧ x ∈ V
-- Mathlib.Topology.Homotopy.Lifting
IsCoveringMap.map_liftPathQuotient : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {p : E → X}
  (cov : IsCoveringMap p) {x y : X} (γ : Path.Homotopic.Quotient x y) (e : ↑(p ⁻¹' {x})),
  (cov.liftPathQuotient γ e).map { toFun := p, continuous_toFun := ⋯ } = γ.cast ⋯ ⋯
-- Mathlib.AlgebraicGeometry.EllipticCurve.Weierstrass
WeierstrassCurve.b₂.eq_1 : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R), W.b₂ = W.a₁ ^ 2 + 4 * W.a₂
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.AEStronglyMeasurable
MeasureTheory.AEStronglyMeasurable.div : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {m m₀ : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  {f g : α → β} [inst_1 : Group β] [IsTopologicalGroup β],
  MeasureTheory.AEStronglyMeasurable f μ →
    MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (f / g) μ
-- Mathlib.Algebra.Group.Defs
/-- A `DivisionMonoid` which `IsMulCommutative` is a `DivisionCommMonoid`.

This is primarily used to deduce the bundled version from the unbundled one for commutative
subobjects in a noncommutative ambient type. As such this is only available inside the
`IsMulCommutative` scope so as to avoid deleterious effects to type class synthesis for bundled
commutativity.

See note [commutative subobjects].  -/
IsMulCommutative.instDivisionCommMonoid : {M : Type u_2} → [inst : DivisionMonoid M] → [IsMulCommutative M] → DivisionCommMonoid M
-- Mathlib.Algebra.Group.Hom.Defs
/-- Group homomorphisms preserve division.  -/
map_mul_inv : ∀ {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : Group G] [inst_2 : DivisionMonoid H]
  [MonoidHomClass F G H] (f : F) (a b : G), f (a * b⁻¹) = f a * (f b)⁻¹
-- Lean.Data.PersistentArray
Lean.PersistentArray.setAux : {α : Type u} → Lean.PersistentArrayNode α → USize → USize → α → Lean.PersistentArrayNode α
-- Std.Async.Basic
Std.Async.instMonadAwaitExceptTOfMonad : {m t : Type → Type} → {n : Type} → [Monad m] → [Std.Async.MonadAwait t m] → Std.Async.MonadAwait t (ExceptT n m)
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.instIsAffineTerminalScheme : AlgebraicGeometry.IsAffine (⊤_ AlgebraicGeometry.Scheme)
-- Std.Http.Data.Headers
/-- Folds over all key-value pairs in the headers.
 -/
Std.Http.Headers.fold : {α : Type u_1} → Std.Http.Headers → α → (α → Std.Http.Header.Name → Std.Http.Header.Value → α) → α
-- Mathlib.CategoryTheory.Idempotents.HomologicalComplex
CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence_counitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {ι : Type u_2}
  (c : ComplexShape ι),
  (CategoryTheory.Idempotents.karoubiHomologicalComplexEquivalence C c).counitIso =
    CategoryTheory.Idempotents.KaroubiHomologicalComplexEquivalence.counitIso
-- Init.Data.Iterators.Consumers.Partial
Std.Iter.Partial.mk : {α β : Type w} → Std.Iter β → Std.Iter.Partial β
-- Mathlib.Tactic.DSimpPercent
/-- `dsimp% […] t` runs `dsimp […]` on term `t`.
If `t` is a proof, then it runs `dsimp […]` on the type of `t` instead.

For instance, instead of
```
have foo := ...
dsimp at foo
rw [foo]
```
one can write `rw [dsimp% foo]`.
 -/
Mathlib.Tactic.dsimpPercent : Lean.ParserDescr
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.instModule : (R : Type uR) →
  [inst : CommRing R] → (A : Type uA) → [inst_1 : AddCommGroup A] → [Module R A] → Module R (CharacterModule A)
-- Mathlib.Topology.MetricSpace.Thickening
/-- A set is contained in its own (open) thickening.  -/
Metric.self_subset_thickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {δ : ℝ}, 0 < δ → ∀ (E : Set α), E ⊆ Metric.thickening δ E
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
CategoryTheory.instEffectiveEpiOfIsRegularEpi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {B X : C} {f : X ⟶ B} [h : CategoryTheory.IsRegularEpi f],
  CategoryTheory.EffectiveEpi f
-- Mathlib.RingTheory.RingHom.QuasiFinite
RingHom.QuasiFinite.comp : ∀ {T : Type u_3} [inst : CommRing T] {R : Type u_4} {S : Type u_5} [inst_1 : CommRing R] [inst_2 : CommRing S]
  {f : S →+* T} {g : R →+* S}, f.QuasiFinite → g.QuasiFinite → (f.comp g).QuasiFinite
-- Mathlib.Data.Seq.Basic
Stream'.Seq.length'_eq_zero_iff_nil : ∀ {α : Type u} (s : Stream'.Seq α), s.length' = 0 ↔ s = Stream'.Seq.nil
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.continuous_integral : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  Continuous fun f => ∫ᵛ (a : X), ↑↑f a ∂[B; μ]
-- Mathlib.Order.Filter.Basic
Filter.frequently_inf_principal : ∀ {α : Type u} {f : Filter α} {s : Set α} {p : α → Prop},
  (∃ᶠ (x : α) in f ⊓ Filter.principal s, p x) ↔ ∃ᶠ (x : α) in f, x ∈ s ∧ p x