mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Algebra.Basic
algebraMap.coe_sum : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : CommSemiring A] [inst_2 : Algebra R A] {ι : Type u_3}
  {s : Finset ι} (a : ι → R), ↑(∑ i ∈ s, a i) = ∑ i ∈ s, ↑(a i)
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.FundThmCalculus
intervalIntegral.FTCFilter.nhdsUIcc : ∀ {x a b : ℝ} [h : Fact (x ∈ Set.uIcc a b)],
  intervalIntegral.FTCFilter x (nhdsWithin x (Set.uIcc a b)) (nhdsWithin x (Set.uIcc a b))
-- Lean.SubExpr
Lean.SubExpr.instToJsonGoalsLocation : Lean.ToJson Lean.SubExpr.GoalsLocation
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.intNorm_coe : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K]
  (a : ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)),
  ↑(NumberField.mixedEmbedding.fundamentalCone.intNorm a) = NumberField.mixedEmbedding.norm ↑a
-- Mathlib.Order.FixedPoints
OrderHom.isLeast_lfp : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α), IsLeast (Function.fixedPoints ⇑f) (OrderHom.lfp f)
-- Mathlib.Analysis.Normed.Lp.PiLp
/-- `LinearEquiv.piCurry` for `PiLp`, as an isometry.  -/
LinearIsometryEquiv.piLpCurry : (𝕜 : Type u_1) →
  [inst : Semiring 𝕜] →
    {ι : Type u_5} →
      {κ : ι → Type u_6} →
        (p : ENNReal) →
          [inst_1 : Fact (1 ≤ p)] →
            [inst_2 : Fintype ι] →
              [inst_3 : (i : ι) → Fintype (κ i)] →
                (α : (i : ι) → κ i → Type u_7) →
                  [inst_4 : (i : ι) → (k : κ i) → SeminormedAddCommGroup (α i k)] →
                    [inst_5 : (i : ι) → (k : κ i) → Module 𝕜 (α i k)] →
                      (PiLp p fun i => α i.fst i.snd) ≃ₗᵢ[𝕜] PiLp p fun i => PiLp p (α i)
-- Mathlib.Algebra.Group.Basic
eq_of_mul_inv_eq_one : ∀ {α : Type u_1} [inst : DivisionMonoid α] {a b : α}, a * b⁻¹ = 1 → a = b
-- Std.Data.HashMap.Lemmas
Std.HashMap.mem_of_mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ} {k : α}, k ∈ Std.HashMap.filterMap f m → k ∈ m
-- Mathlib.Data.Num.ZNum
_private.Mathlib.Data.Num.ZNum.0.PosNum.sub'.match_1.eq_1 : ∀ (motive : PosNum → PosNum → Sort u_1) (a : PosNum) (h_1 : (a : PosNum) → motive a PosNum.one)
  (h_2 : (b : PosNum) → motive PosNum.one b) (h_3 : (a b : PosNum) → motive a.bit0 b.bit0)
  (h_4 : (a b : PosNum) → motive a.bit0 b.bit1) (h_5 : (a b : PosNum) → motive a.bit1 b.bit0)
  (h_6 : (a b : PosNum) → motive a.bit1 b.bit1),
  (match a, PosNum.one with
    | a, PosNum.one => h_1 a
    | PosNum.one, b => h_2 b
    | a.bit0, b.bit0 => h_3 a b
    | a.bit0, b.bit1 => h_4 a b
    | a.bit1, b.bit0 => h_5 a b
    | a.bit1, b.bit1 => h_6 a b) =
    h_1 a
-- Mathlib.CategoryTheory.Abelian.SerreClass.Basic
CategoryTheory.ObjectProperty.IsSerreClass.toContainsZero : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {inst_1 : CategoryTheory.Abelian C}
  {P : CategoryTheory.ObjectProperty C} [self : P.IsSerreClass], P.ContainsZero
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.atom_eq_eval : ∀ {M : Type u_3} [inst : AddMonoid M] (x : M), x = Mathlib.Tactic.Module.NF.eval [(1, x)]
-- Mathlib.LinearAlgebra.Matrix.Block
Matrix.det_toBlock : ∀ {m : Type u_3} {R : Type v} [inst : CommRing R] [inst_1 : DecidableEq m] [inst_2 : Fintype m] (M : Matrix m m R)
  (p : m → Prop) [inst_3 : DecidablePred p],
  M.det =
    (Matrix.fromBlocks (M.toBlock p p) (M.toBlock p fun j => ¬p j) (M.toBlock (fun j => ¬p j) p)
        (M.toBlock (fun j => ¬p j) fun j => ¬p j)).det
-- Mathlib.Order.Category.BddLat
BddLat.dual_map : ∀ {X Y : BddLat} (f : X ⟶ Y), BddLat.dual.map f = BddLat.ofHom (BoundedLatticeHom.dual (BddLat.Hom.hom f))
-- Mathlib.Data.Option.Basic
Option.guard_eq_some' : ∀ {p : Prop} [inst : Decidable p] (u : Unit), guard p = some u ↔ p
-- Mathlib.MeasureTheory.Measure.Typeclasses.ZeroOne
MeasureTheory.IsZeroOneMeasure.mk : ∀ {α : Type u_1} {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α},
  (∀ ⦃s : Set α⦄, MeasurableSet s → μ s = 0 ∨ μ s = 1) → MeasureTheory.IsZeroOneMeasure μ
-- Mathlib.Analysis.Analytic.ConvergenceRadius
_private.Mathlib.Analysis.Analytic.ConvergenceRadius.0.constFormalMultilinearSeries.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (x : ℕ) (h_1 : Unit → motive 0) (h_2 : (x : ℕ) → motive x),
  (x = 0 → False) →
    (match x with
      | 0 => h_1 ()
      | x => h_2 x) =
      h_2 x
-- Mathlib.Algebra.Group.Defs
add_neg_cancel_comm_assoc : ∀ {G : Type u_1} [inst : AddCommGroup G] (a b : G), a + (b + -a) = b
-- Mathlib.Data.Nat.Sqrt
Nat.add_one_sqrt_le_of_ne_zero : ∀ {n : ℕ}, n ≠ 0 → (n + 1).sqrt ≤ n
-- Mathlib.RingTheory.Coalgebra.CoassocSimps
/-- Simproc version of `rid_comp_map_assoc` that only fires when `f ≠ id`.  -/
CoassocSimps.rid_comp_map_assoc_simproc : Lean.Meta.Simp.Simproc
-- Std.Data.DHashMap.Internal.WF
_private.Std.Data.DHashMap.Internal.WF.0.Std.Internal.List.getEntry?.match_1.splitter : {α : Type u_2} →
  {β : α → Type u_1} →
    (motive : List ((a : α) × β a) → Sort u_3) →
      (x : List ((a : α) × β a)) →
        (Unit → motive []) → ((k : α) → (v : β k) → (l : List ((a : α) × β a)) → motive (⟨k, v⟩ :: l)) → motive x
-- Init.Data.Array.Lemmas
Array.getElem_append_right : ∀ {α : Type u_1} {i : ℕ} {xs ys : Array α} {h : i < (xs ++ ys).size} (hle : xs.size ≤ i),
  (xs ++ ys)[i] = ys[i - xs.size]
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.OuterMeasure.trim.eq_1 : ∀ {α : Type u_1} [inst : MeasurableSpace α] (m : MeasureTheory.OuterMeasure α),
  m.trim = MeasureTheory.inducedOuterMeasure (fun s x => m s) ⋯ ⋯
-- Mathlib.Data.TypeVec
TypeVec.snd_diag : ∀ {n : ℕ} {α : TypeVec.{u_1} n}, TypeVec.comp TypeVec.prod.snd TypeVec.prod.diag = TypeVec.id
-- Std.Data.Iterators.Lemmas.Consumers.Monadic.Collect
Std.IterM.Equiv.toList_eq : ∀ {β α₁ α₂ : Type w} {m : Type w → Type w'} [inst : Monad m] [inst_1 : LawfulMonad m] [inst_2 : Std.Iterator α₁ m β]
  [inst_3 : Std.Iterator α₂ m β] [Std.Iterators.Finite α₁ m] [Std.Iterators.Finite α₂ m] {ita : Std.IterM m β}
  {itb : Std.IterM m β}, ita.Equiv itb → ita.toList = itb.toList
-- Aesop.Stats.Basic
Aesop.RuleStats.rule : Aesop.RuleStats → Aesop.DisplayRuleName
-- Mathlib.Algebra.Vertex.HVertexOperator
HVertexOperator.ext : ∀ {Γ : Type u_1} [inst : PartialOrder Γ] {R : Type u_2} {V : Type u_3} {W : Type u_4} [inst_1 : CommRing R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddCommGroup W] [inst_5 : Module R W]
  (A B : HVertexOperator Γ R V W), (∀ (v : V), A v = B v) → A = B
-- Std.Http.Data.Version
Std.Http.instInhabitedVersion.default : Std.Http.Version
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- The functor that turns a type into a codiscrete category is right adjoint to the objects
functor.  -/
CategoryTheory.Codiscrete.adj : CategoryTheory.Cat.objects ⊣ CategoryTheory.Codiscrete.functorToCat
-- Mathlib.Order.Category.Frm
/-- Turn a morphism in `Frm` back into a `FrameHom`.  -/
Frm.Hom.hom : {X Y : Frm} → X.Hom Y → FrameHom ↑X ↑Y
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioo_eq_empty_iff : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α] [DenselyOrdered α],
  Finset.Ioo a b = ∅ ↔ ¬a < b
-- Mathlib.Data.Finset.Sigma
Finset.filter_sigma : ∀ {ι : Type u_1} {α : ι → Type u_2} (s : Finset ι) (t : (i : ι) → Finset (α i)) (p : (i : ι) × α i → Prop)
  [inst : DecidablePred p], Finset.filter p (s.sigma t) = s.sigma fun i => {x ∈ t i | p ⟨i, x⟩}
-- Mathlib.CategoryTheory.Sites.Hypercover.One
/-- If `E : J.OneHypercover S` and `F : Sheaf J A`, then `F.obj (op S)` is
a multiequalizer of suitable maps `F.obj (op (E.X i)) ⟶ F.obj (op (E.Y j))`
induced by `E.p₁ j` and `E.p₂ j`.  -/
CategoryTheory.GrothendieckTopology.OneHypercover.isLimitMultifork : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : Type u_1} →
      [inst_1 : CategoryTheory.Category.{v_1, u_1} A] →
        {J : CategoryTheory.GrothendieckTopology C} →
          {S : C} →
            (E : J.OneHypercover S) → (F : CategoryTheory.Sheaf J A) → CategoryTheory.Limits.IsLimit (E.multifork F.obj)
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.RicSliceData : (α : Type u) → Type v → [Ord α] → Type (max u v)
-- Mathlib.Topology.Algebra.Module.Spaces.WeakDual
WeakDual.coeFn_continuous : ∀ {𝕜 : Type u_2} {E : Type u_4} [inst : CommSemiring 𝕜] [inst_1 : TopologicalSpace 𝕜] [inst_2 : ContinuousAdd 𝕜]
  [inst_3 : ContinuousConstSMul 𝕜 𝕜] [inst_4 : AddCommMonoid E] [inst_5 : Module 𝕜 E] [inst_6 : TopologicalSpace E],
  Continuous fun x y => x y
-- Init.Data.UInt.Lemmas
UInt32.lt_iff_toFin_lt : ∀ {a b : UInt32}, a < b ↔ a.toFin < b.toFin
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_from_nat : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : ℕ → α}, Measurable f
-- Mathlib.Analysis.Asymptotics.LinearGrowth
Eventually.linearGrowthSup_le : ∀ {u : ℕ → EReal} {a : EReal}, (∀ᶠ (n : ℕ) in Filter.atTop, u n ≤ a * ↑n) → LinearGrowth.linearGrowthSup u ≤ a
-- Mathlib.Algebra.Order.Interval.Basic
instInvNonemptyInterval.eq_1 : ∀ {α : Type u_2} [inst : CommGroup α] [inst_1 : PartialOrder α] [inst_2 : IsOrderedMonoid α],
  instInvNonemptyInterval = { inv := fun s => { fst := s.toProd.2⁻¹, snd := s.toProd.1⁻¹, fst_le_snd := ⋯ } }
-- Mathlib.Control.Monad.Cont
ContT.instMonadLiftOfMonad : {r : Type u} → {m : Type u → Type v} → [Monad m] → MonadLift m (ContT r m)
-- Mathlib.Algebra.Order.Group.PiLex
Pi.Lex.isOrderedAddCancelMonoid : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [inst_1 : (i : ι) → AddCommMonoid (α i)]
  [inst_2 : (i : ι) → PartialOrder (α i)] [∀ (i : ι), IsOrderedCancelAddMonoid (α i)],
  IsOrderedCancelAddMonoid (Lex ((i : ι) → α i))
-- Mathlib.Tactic.Push
_private.Mathlib.Tactic.Push.0.Mathlib.Tactic.Push.instEvalExprConfig : Lean.Elab.ConfigEval.EvalExpr Mathlib.Tactic.Push.Config
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.mapFst_hom_app : ∀ {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] {A' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] {B' : Type u₅} [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  {T' : Type u₆} [inst_5 : CategoryTheory.Category.{v₆, u₆} T'] {L : CategoryTheory.Functor A T}
  {R : CategoryTheory.Functor B T} {L' : CategoryTheory.Functor A' T'} {R' : CategoryTheory.Functor B' T'}
  {F₁ : CategoryTheory.Functor A A'} {F₂ : CategoryTheory.Functor B B'} {F : CategoryTheory.Functor T T'}
  (α : F₁.comp L' ⟶ L.comp F) (β : R.comp F ⟶ F₂.comp R') (X : CategoryTheory.Comma L R),
  (CategoryTheory.Comma.mapFst α β).hom.app X = CategoryTheory.CategoryStruct.id (F₁.obj X.left)
-- Mathlib.RingTheory.Kaehler.Basic
Derivation.liftKaehlerDifferential_comp : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {M : Type u_1}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : Module S M] [inst_6 : IsScalarTower R S M]
  (D : Derivation R S M), D.liftKaehlerDifferential.compDer (KaehlerDifferential.D R S) = D
-- Init.Data.UInt.Bitwise
UInt32.shiftLeft_add_of_toNat_lt : ∀ {a b c : UInt32}, b.toNat + c.toNat < 32 → a <<< (b + c) = a <<< b <<< c
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.setENode.unsafe_1 : (e : Lean.Expr) →
  (n : Lean.Meta.Grind.ENode) →
    (s : Lean.Meta.Grind.Goal) → Lean.Meta.Grind.CongrTable (Lean.PersistentHashMap.insert s.enodeMap { expr := e } n)
-- Mathlib.RingTheory.Spectrum.Prime.Topology
PrimeSpectrum.isBasis_basic_opens : ∀ {R : Type u} [inst : CommSemiring R], TopologicalSpace.Opens.IsBasis (Set.range PrimeSpectrum.basicOpen)
-- Mathlib.RingTheory.PowerSeries.Substitution
/-- **Alias** of `PowerSeries.HasSubst.substInv`. -/
PowerSeries.hasSubst_substInv : ∀ {R : Type u_2} [inst : CommRing R] (P : PowerSeries R) [inst_1 : Invertible ((PowerSeries.coeff 1) P)],
  PowerSeries.HasSubst P.substInv
-- Mathlib.Data.Nat.Choose.Central
/-- An exponential lower bound on the central binomial coefficient.
This bound is weaker than `Nat.four_pow_lt_mul_centralBinom`, but it is of historical interest
because it appears in Erdős's proof of Bertrand's postulate.
 -/
Nat.four_pow_le_two_mul_self_mul_centralBinom : ∀ (n : ℕ), 0 < n → 4 ^ n ≤ 2 * n * n.centralBinom
-- Lean.Meta.Tactic.ElimInfo
Lean.Meta.addCustomEliminatorEntry : Lean.Meta.CustomEliminators → Lean.Meta.CustomEliminator → Lean.Meta.CustomEliminators
-- Mathlib.GroupTheory.Coxeter.Inversion
_private.Mathlib.GroupTheory.Coxeter.Inversion.0.CoxeterSystem.rightInvSeq.match_1.splitter : {B : Type u_1} →
  (motive : List B → Sort u_2) →
    (ω : List B) → (Unit → motive []) → ((i : B) → (ω : List B) → motive (i :: ω)) → motive ω
-- Mathlib.Analysis.Fourier.AddCircleMulti
UnitAddTorus.coeFn_mFourierLp : ∀ {d : Type u_1} [inst : Fintype d] (p : ENNReal) [inst_1 : Fact (1 ≤ p)] (n : d → ℤ),
  ↑↑(UnitAddTorus.mFourierLp p n) =ᵐ[MeasureTheory.volume] ⇑(UnitAddTorus.mFourier n)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_diff!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β k},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.diff! m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.natCast_eq_map_iff : ∀ {α : Type u} {β : Type v} [inst : AddMonoidWithOne α] {f : β → α} {n : ℕ} {a : WithBot β},
  ↑n = WithBot.map f a ↔ ∃ x, a = ↑x ∧ f x = ↑n
-- Mathlib.Algebra.Group.Pointwise.Set.Finite
Set.infinite_inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {s : Set α}, s⁻¹.Infinite ↔ s.Infinite
-- Mathlib.RingTheory.Extension.Generators
/-- Giving a hom between two families of generators is equivalent to
giving an algebra homomorphism between the polynomial rings.  -/
Algebra.Generators.Hom.equivAlgHom : {R : Type u} →
  {S : Type v} →
    {ι : Type w} →
      [inst : CommRing R] →
        [inst_1 : CommRing S] →
          [inst_2 : Algebra R S] →
            {P : Algebra.Generators R S ι} →
              {R' : Type u_1} →
                {S' : Type u_2} →
                  {ι' : Type u_3} →
                    [inst_3 : CommRing R'] →
                      [inst_4 : CommRing S'] →
                        [inst_5 : Algebra R' S'] →
                          {P' : Algebra.Generators R' S' ι'} →
                            [inst_6 : Algebra R R'] →
                              [inst_7 : Algebra S S'] →
                                [inst_8 : Algebra R S'] →
                                  [IsScalarTower R R' S'] →
                                    [IsScalarTower R S S'] →
                                      P.Hom P' ≃
                                        { f //
                                          ∀ (x : P.Ring),
                                            (MvPolynomial.aeval P'.val) (f x) =
                                              (algebraMap S S') ((MvPolynomial.aeval P.val) x) }
-- Mathlib.CategoryTheory.Monoidal.Free.Coherence
_private.Mathlib.CategoryTheory.Monoidal.Free.Coherence.0.CategoryTheory.FreeMonoidalCategory.inclusionObj.match_1.eq_1 : ∀ {C : Type u_1} (motive : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C → Sort u_2)
  (h_1 : Unit → motive CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.unit)
  (h_2 : (n : CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject C) → (a : C) → motive (n.tensor a)),
  (match CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.unit with
    | CategoryTheory.FreeMonoidalCategory.NormalMonoidalObject.unit => h_1 ()
    | n.tensor a => h_2 n a) =
    h_1 ()
-- Mathlib.Algebra.Homology.ShortComplex.Abelian
CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.π_comp_isoHomology_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex C) {kf : CategoryTheory.Limits.KernelFork S.g}
  {cc : CategoryTheory.Limits.CokernelCofork S.f} (hkf : CategoryTheory.Limits.IsLimit kf)
  (hcc : CategoryTheory.Limits.IsColimit cc) {H : C} {π : kf.pt ⟶ H} {ι : H ⟶ cc.pt}
  (fac :
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι kf) (CategoryTheory.Limits.Cofork.π cc) =
      CategoryTheory.CategoryStruct.comp π ι)
  [inst_2 : CategoryTheory.Epi π] [inst_3 : CategoryTheory.Mono ι],
  CategoryTheory.CategoryStruct.comp π
      (CategoryTheory.ShortComplex.HomologyData.ofEpiMonoFactorisation.isoHomology S hkf hcc fac).hom =
    CategoryTheory.CategoryStruct.comp (S.isoCyclesOfIsLimit hkf).hom S.homologyπ
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.maxEntry?.match_1.congr_eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α fun x => β) (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β) →
                  (l_1 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1 →
                      motive
                        (Std.DTreeMap.Internal.Impl.inner size k v l
                          (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r_1)))
  (size : ℕ) (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β),
  x = Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) →
    (match x with
      | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
      | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf => h_2 size k v l
      | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1) =>
        h_3 size k v l r size_2 k_2 v_2 l_2 r_1 h) ≍
      h_3 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.toFun_eq_coe : ∀ {M : Type u_4} {N : Type u_5} [inst : MulOne M] [inst_1 : MulOne N] (f : M →* N), (↑f).toFun = ⇑f
-- Mathlib.Algebra.Star.MonoidHom
StarMulEquiv.coe_ofBijective : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : Star A] [inst_3 : Star B] {f : A →⋆* B}
  (hf : Function.Bijective ⇑f), ⇑(StarMulEquiv.ofBijective f hf) = ⇑f
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- Express `dist` in terms of `edist`  -/
dist_edist : ∀ {α : Type u} [inst : PseudoMetricSpace α] (x y : α), dist x y = (edist x y).toReal
-- Mathlib.Order.Category.Frm
/-- Typecheck a `FrameHom` as a morphism in `Frm`.  -/
Frm.ofHom : {X Y : Type u} →
  [inst : Order.Frame X] →
    [inst_1 : Order.Frame Y] → FrameHom X Y → ({ carrier := X, str := inst } ⟶ { carrier := Y, str := inst_1 })
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.approx_le_approx_of_U_sub_C : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} {c₁ c₂ : Urysohns.CU P},
  c₁.U ⊆ c₂.C → ∀ (n₁ n₂ : ℕ) (x : X), Urysohns.CU.approx n₂ c₂ x ≤ Urysohns.CU.approx n₁ c₁ x
-- Lean.PrettyPrinter.Delaborator.Options
Lean.getPPMatch : Lean.Options → Bool
-- Mathlib.Algebra.Group.Commute.Defs
AddCommute.all : ∀ {S : Type u_3} [inst : AddCommMagma S] (a b : S), AddCommute a b
-- Mathlib.CategoryTheory.FiberedCategory.Grothendieck
CategoryTheory.Pseudofunctor.CoGrothendieck.comp_const : ∀ {𝒮 : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮ᵒᵖ) CategoryTheory.Cat) (S : 𝒮),
  (CategoryTheory.Pseudofunctor.CoGrothendieck.ι F S).comp (CategoryTheory.Pseudofunctor.CoGrothendieck.forget F) =
    (CategoryTheory.Functor.const ↑(F.obj { as := Opposite.op S })).obj S
-- Aesop.Index.Basic
Aesop.IndexMatchResult.mk.injEq : ∀ {α : Type} (rule : α) (locations : Array Aesop.IndexMatchLocation)
  (patternSubsts? : Option (Array Aesop.Substitution)) (rule_1 : α) (locations_1 : Array Aesop.IndexMatchLocation)
  (patternSubsts?_1 : Option (Array Aesop.Substitution)),
  ({ rule := rule, locations := locations, patternSubsts? := patternSubsts? } =
      { rule := rule_1, locations := locations_1, patternSubsts? := patternSubsts?_1 }) =
    (rule = rule_1 ∧ locations = locations_1 ∧ patternSubsts? = patternSubsts?_1)
-- Mathlib.Order.WithBotTop
WithBotTop.coe_lt_coe : ∀ {ι : Type u_1} [inst : LT ι] {a b : ι}, WithBotTop.coe a < WithBotTop.coe b ↔ a < b
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_subset_Iio_self : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ico a b ⊆ Set.Iio b
-- Mathlib.RepresentationTheory.Equiv
Representation.finsuppTensorLeft_symm_apply_single : ∀ {G : Type v} [inst : Monoid G] {V : Type v'} [inst_1 : AddCommMonoid V] {W : Type w'} [inst_2 : AddCommMonoid W]
  {k : Type u} [inst_3 : CommSemiring k] [inst_4 : Module k V] [inst_5 : Module k W] (σ : Representation k G V)
  (ρ : Representation k G W) {α : Type w'} [inst_6 : DecidableEq α] (i : α) (v : V) (w : W),
  ((σ.finsuppTensorLeft ρ α).symm fun₀ | i => v ⊗ₜ[k] w) = (fun₀ | i => v) ⊗ₜ[k] w
-- Mathlib.Algebra.Ring.Subring.Defs
Subring.mem_mk : ∀ {R : Type u} [inst : NonAssocRing R] {S : Subsemiring R} {x : R} (h : ∀ {x : R}, x ∈ S.carrier → -x ∈ S.carrier),
  x ∈ { toSubsemiring := S, neg_mem' := h } ↔ x ∈ S
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.not_infinitePos_add_infiniteNeg : ∀ {x y : ℝ*}, ¬x.InfinitePos → y.InfiniteNeg → (x + y).InfiniteNeg
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup'_inf_distrib_left : ∀ {α : Type u_2} {ι : Type u_5} [inst : DistribLattice α] {s : Finset ι} (hs : s.Nonempty) (f : ι → α) (a : α),
  a ⊓ s.sup' hs f = s.sup' hs fun i => a ⊓ f i
-- Lean.Elab.DocString
/-- An expander for commands in docstrings.
 -/
Lean.Doc.DocCommandExpander : Type
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.neg_contLinear : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : TopologicalSpace V]
  [inst_10 : IsTopologicalAddTorsor P] (f : P →ᴬ[R] W), (-f).contLinear = -f.contLinear
-- Mathlib.Analysis.Complex.HasPrimitives
_private.Mathlib.Analysis.Complex.HasPrimitives.0.Complex.mem_ball_of_map_im_aux₁ : ∀ {c : ℂ} {r a b₁ b₂ : ℝ},
  ↑a + ↑b₁ * Complex.I ∈ Metric.ball c r →
    ↑a + ↑b₂ * Complex.I ∈ Metric.ball c r → (fun y => ↑a + ↑y * Complex.I) '' Set.uIcc b₁ b₂ ⊆ Metric.ball c r
-- Mathlib.Topology.Algebra.InfiniteSum.Order
Summable.le_tsum : ∀ {ι : Type u_1} {α : Type u_3} {L : SummationFilter ι} [inst : AddCommMonoid α] [inst_1 : Preorder α]
  [IsOrderedAddMonoid α] [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} [L.NeBot] [L.LeAtTop],
  Summable f L → ∀ (i : ι), (∀ (j : ι), j ≠ i → 0 ≤ f j) → f i ≤ ∑'[L] (i : ι), f i
-- Mathlib.FieldTheory.Finite.Basic
Subfield.card_bot : ∀ (F : Type u_3) [inst : Field F] (p : ℕ) [Fact (Nat.Prime p)] [CharP F p], Nat.card ↥⊥ = p
-- Lean.Server.Rpc.Basic
Lean.Server.instRpcEncodableWithRpcRefOfTypeName.rpcDecode : {α : Type} →
  [TypeName α] → Lean.Json → ExceptT String (ReaderT Lean.Server.RpcObjectStore Id) (Lean.Server.WithRpcRef α)
-- Mathlib.Analysis.SpecialFunctions.Exp
ContinuousWithinAt.cexp : ∀ {α : Type u_1} [inst : TopologicalSpace α] {f : α → ℂ} {s : Set α} {x : α},
  ContinuousWithinAt f s x → ContinuousWithinAt (fun y => Complex.exp (f y)) s x
-- Mathlib.RingTheory.PowerSeries.WellKnown
_private.Mathlib.RingTheory.PowerSeries.WellKnown.0.PowerSeries.invOneSubPow.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (d : ℕ) (h_1 : Unit → motive 0) (h_2 : (d : ℕ) → motive d.succ),
  (match d.succ with
    | 0 => h_1 ()
    | d.succ => h_2 d) =
    h_2 d