mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctorAssociatorX_hom_D₂_assoc : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₁₂ : Type u_3} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_5, u_3} C₁₂] [inst_5 : CategoryTheory.Category.{v_6, u_4} C₂₃]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_8 : CategoryTheory.Limits.HasZeroMorphisms C₃] [inst_9 : CategoryTheory.Preadditive C₁₂]
  [inst_10 : CategoryTheory.Preadditive C₂₃] [inst_11 : CategoryTheory.Preadditive C₄]
  {F₁₂ : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ C₁₂)}
  {G : CategoryTheory.Functor C₁₂ (CategoryTheory.Functor C₃ C₄)}
  {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} [inst_12 : F₁₂.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F₁₂.obj X₁).PreservesZeroMorphisms] [inst_14 : G.Additive]
  [inst_15 : ∀ (X₁₂ : C₁₂), (G.obj X₁₂).PreservesZeroMorphisms] [inst_16 : G₂₃.PreservesZeroMorphisms]
  [inst_17 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_18 : F.PreservesZeroMorphisms]
  [inst_19 : ∀ (X₁ : C₁), (F.obj X₁).Additive]
  (associator : CategoryTheory.bifunctorComp₁₂ F₁₂ G ≅ CategoryTheory.bifunctorComp₂₃ F G₂₃) {ι₁ : Type u_7}
  {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10} {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_20 : DecidableEq ι₄]
  {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂} {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁)
  (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃) (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃)
  (c₄ : ComplexShape ι₄) [inst_21 : TotalComplexShape c₁ c₂ c₁₂] [inst_22 : TotalComplexShape c₁₂ c₃ c₄]
  [inst_23 : TotalComplexShape c₂ c₃ c₂₃] [inst_24 : TotalComplexShape c₁ c₂₃ c₄], ⋯
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainBialgHom_comp : ∀ {R : Type u_1} {M : Type u_8} {N : Type u_9} {O : Type u_10} [inst : CommSemiring R] [inst_1 : Monoid M]
  [inst_2 : Monoid N] [inst_3 : Monoid O] (f : N →* O) (g : M →* N),
  MonoidAlgebra.mapDomainBialgHom R (f.comp g) =
    (MonoidAlgebra.mapDomainBialgHom R f).comp (MonoidAlgebra.mapDomainBialgHom R g)
-- Mathlib.Topology.Order.Compact
cocompact_eq_atBot : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [NoMinOrder α] [OrderTop α] [ClosedIicTopology α]
  [CompactIccSpace α], Filter.cocompact α = Filter.atBot
-- Lean.Data.Lsp.Extra
Lean.Lsp.WaitForDiagnosticsParams.uri : Lean.Lsp.WaitForDiagnosticsParams → Lean.Lsp.DocumentUri
-- Lean.Parser.Attr
Lean.Parser.Priority.numPrio : Lean.Parser.Parser
-- Lean.Meta.KExprMap
/-- A mapping that identifies definitionally equal expressions.
We implement it as a mapping from `HeadIndex` to `AssocList Expr α`.

Remark: this map may be quite inefficient if there are many `HeadIndex` collisions.
 -/
Lean.Meta.KExprMap : Type → Type
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.coe_of : ∀ (R : Type u) [inst : Group R], ↑(GrpCat.of R) = R
-- Mathlib.Data.Finmap
Finmap.mem_lookup_union_middle : ∀ {α : Type u} {β : α → Type v} [inst : DecidableEq α] {a : α} {b : β a} {s₁ s₂ s₃ : Finmap β},
  b ∈ Finmap.lookup a (s₁ ∪ s₃) → a ∉ s₂ → b ∈ Finmap.lookup a (s₁ ∪ s₂ ∪ s₃)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.getKey?_union_of_not_mem_left : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {k : α}, k ∉ t₁ → (t₁ ∪ t₂).getKey? k = t₂.getKey? k
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The underlying function.  -/
AddActionHom.toFun : {M : Type u_8} →
  {N : Type u_9} →
    {φ : M → N} → {X : Type u_10} → [inst : VAdd M X] → {Y : Type u_11} → [inst_1 : VAdd N Y] → (X →ₑ[φ] Y) → X → Y
-- Mathlib.Topology.Covering.Basic
IsCoveringMap.eq_1 : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] (f : E → X),
  IsCoveringMap f = ∀ (x : X), IsEvenlyCovered f x ↑(f ⁻¹' {x})
-- Mathlib.Algebra.Order.Archimedean.Class
MulArchimedeanClass.mk_right_le_mk_mul : ∀ {M : Type u_1} [inst : CommGroup M] [inst_1 : LinearOrder M] [inst_2 : IsOrderedMonoid M] {a b : M},
  MulArchimedeanClass.mk b ≤ MulArchimedeanClass.mk a → MulArchimedeanClass.mk b ≤ MulArchimedeanClass.mk (a * b)
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Integral
/-- The continuous functional calculus commutes with integration.
This version assumes joint continuity of `f`, see `cfc_integral'` for a statement
with weaker assumptions.  -/
cfc_integral : ∀ {X : Type u_1} {𝕜 : Type u_2} {A : Type u_3} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : MeasurableSpace X]
  {μ : MeasureTheory.Measure X} [inst_2 : NormedRing A] [inst_3 : StarRing A] [inst_4 : NormedAlgebra 𝕜 A]
  [inst_5 : ContinuousFunctionalCalculus 𝕜 A p] [CompleteSpace A] [inst_7 : NormedSpace ℝ A]
  [inst_8 : TopologicalSpace X] [OpensMeasurableSpace X] (f : X → 𝕜 → 𝕜) (bound : X → ℝ) (a : A)
  [SecondCountableTopologyEither X C(↑(spectrum 𝕜 a), 𝕜)],
  ContinuousOn (Function.uncurry f) (Set.univ ×ˢ spectrum 𝕜 a) →
    (∀ᵐ (x : X) ∂μ, ∀ z ∈ spectrum 𝕜 a, ‖f x z‖ ≤ bound x) →
      MeasureTheory.HasFiniteIntegral bound μ →
        autoParam (p a) cfc_integral._auto_1 → cfc (fun r => ∫ (x : X), f x r ∂μ) a = ∫ (x : X), cfc (f x) a ∂μ
-- Mathlib.Topology.Separation.Regular
T3Space.mk : ∀ {X : Type u} [inst : TopologicalSpace X] [toT0Space : T0Space X] [toRegularSpace : RegularSpace X], T3Space X
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.mkMetric'.tendsto_pre : ∀ {X : Type u_2} [inst : EMetricSpace X] (m : Set X → ENNReal) (s : Set X),
  Filter.Tendsto (fun r => (MeasureTheory.OuterMeasure.mkMetric'.pre m r) s) (nhdsWithin 0 (Set.Ioi 0))
    (nhds ((MeasureTheory.OuterMeasure.mkMetric' m) s))
-- Mathlib.CategoryTheory.Elements
CategoryTheory.Functor.Elements.precomp_obj_fst : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{u_2, u_1} D]
  (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D (Type w)) (x : (F.comp G).Elements),
  ((CategoryTheory.Functor.Elements.precomp F G).obj x).fst = F.obj x.fst
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.some_maxKey_eq_maxKey? : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β} {he : l.isEmpty = false},
  some (l.maxKey he) = l.maxKey?
-- Mathlib.Data.Part
Part.instInv : {α : Type u_1} → [Inv α] → Inv (Part α)
-- Batteries.Data.UInt
UInt64.compare_eq_toNat_compare_toNat : ∀ (x y : UInt64), compare x y = compare x.toNat y.toNat
-- Lean.DocString.Types
Lean.Doc.Inline.math.injEq : ∀ {i : Type u} (mode : Lean.Doc.MathMode) (string : String) (mode_1 : Lean.Doc.MathMode) (string_1 : String),
  (Lean.Doc.Inline.math mode string = Lean.Doc.Inline.math mode_1 string_1) = (mode = mode_1 ∧ string = string_1)
-- Mathlib.Topology.CWComplex.Classical.Finite
Topology.RelCWComplex.FiniteDimensional.mk : ∀ {X : Type u} [inst : TopologicalSpace X] {C D : Set X} [inst_1 : Topology.RelCWComplex C D],
  (∀ᶠ (n : ℕ) in Filter.atTop, IsEmpty (Topology.RelCWComplex.cell C n)) → Topology.RelCWComplex.FiniteDimensional C
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Sheaf.objSupIsoProdEqLocus_inv_snd : ∀ {X : TopCat} (F : TopCat.Sheaf CommRingCat X) (U V : TopologicalSpace.Opens ↑X)
  (x :
    ↑(CommRingCat.of
        ↥(((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp
                (RingHom.fst ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V)))).eqLocus
            ((CommRingCat.Hom.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op)).comp
              (RingHom.snd ↑(F.obj.obj (Opposite.op U)) ↑(F.obj.obj (Opposite.op V))))))),
  (CategoryTheory.ConcreteCategory.hom (F.obj.map (CategoryTheory.homOfLE ⋯).op))
      ((CategoryTheory.ConcreteCategory.hom (F.objSupIsoProdEqLocus U V).inv) x) =
    (↑x).2
-- Mathlib.CategoryTheory.WithTerminal.Cone
CategoryTheory.WithInitial.coconeEquiv_counitIso_inv_app_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type w} [inst_1 : CategoryTheory.Category.{w', w} J]
  {X : C} {K : CategoryTheory.Functor J (CategoryTheory.Under X)}
  (X_1 : CategoryTheory.Limits.Cocone (CategoryTheory.WithInitial.liftFromUnder.obj K)),
  (CategoryTheory.WithInitial.coconeEquiv.counitIso.inv.app X_1).hom = CategoryTheory.CategoryStruct.id X_1.pt
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.π.congr_simp : ∀ {I : Type u} (C C_1 : Set (I → Bool)),
  C = C_1 →
    ∀ (J J_1 : I → Prop),
      J = J_1 →
        ∀ {inst : (i : I) → Decidable (J i)} [inst_1 : (i : I) → Decidable (J_1 i)] (a a_1 : I → Bool),
          a = a_1 → Profinite.NobelingProof.π C J a = Profinite.NobelingProof.π C_1 J_1 a_1
-- Init.Data.List.Range
List.mem_range' : ∀ {s step m n : ℕ}, m ∈ List.range' s n step ↔ ∃ i < n, m = s + step * i
-- Mathlib.Algebra.BigOperators.Finsupp.Basic
Finsupp.sum_sub_index : ∀ {α : Type u_1} {γ : Type u_3} {β : Type u_7} [inst : AddGroup β] [inst_1 : AddCommGroup γ] {f g : α →₀ β}
  {h : α → β → γ}, (∀ (a : α) (b₁ b₂ : β), h a (b₁ - b₂) = h a b₁ - h a b₂) → (f - g).sum h = f.sum h - g.sum h
-- Mathlib.Condensed.Light.Small
CategoryTheory.sheafCompose.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} A]
  {B : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} B] (J : CategoryTheory.GrothendieckTopology C)
  (F F_1 : CategoryTheory.Functor A B) (e_F : F = F_1) [inst_3 : J.HasSheafCompose F],
  CategoryTheory.sheafCompose J F = CategoryTheory.sheafCompose J F_1
-- Mathlib.CategoryTheory.Sites.Descent.DescentData
CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso_inv_app_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat) {ι : Type t} (S : C)
  {X : ι → C} {f : (i : ι) → X i ⟶ S} (X_1 : F.DescentData f) (i : ι),
  ((CategoryTheory.Pseudofunctor.DescentData.pullFunctorIdIso F S).inv.app X_1).hom i =
    (F.mapId { as := Opposite.op (X i) }).inv.toNatTrans.app (X_1.obj i)
-- Mathlib.LinearAlgebra.RootSystem.Finite.Nondegenerate
RootPairing.smul_coroot_eq_of_root_add_root_eq : ∀ {ι : 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 : Module R M] [inst_5 : Module R N] (P : RootPairing ι R M N)
  [P.IsAnisotropic] [IsDomain R] [Module.IsTorsionFree R N] {i j k : ι} {m n : R},
  m • P.root i + n • P.root j = P.root k →
    (m * m * P.pairing i j + m * n * (P.pairing i j * P.pairing j i) + n * n * P.pairing j i) • P.coroot k =
      m • P.pairing i j • P.coroot i + n • P.pairing j i • P.coroot j
-- Mathlib.Algebra.Module.CharacterModule
rTensor_injective_iff_lcomp_surjective : ∀ {R : Type uR} [inst : CommRing R] {A : Type uA} [inst_1 : AddCommGroup A] {A' : Type u_1} [inst_2 : AddCommGroup A']
  {B : Type uB} [inst_3 : AddCommGroup B] [inst_4 : Module R A] [inst_5 : Module R A'] [inst_6 : Module R B]
  {f : A →ₗ[R] A'},
  Function.Injective ⇑(LinearMap.rTensor B f) ↔ Function.Surjective ⇑(LinearMap.lcomp R (CharacterModule B) f)
-- Init.Data.BitVec.Bitblast
BitVec.ushiftRightRec_succ : ∀ {w₁ w₂ n : ℕ} (x : BitVec w₁) (y : BitVec w₂),
  x.ushiftRightRec y (n + 1) = x.ushiftRightRec y n >>> (y &&& BitVec.twoPow w₂ (n + 1))
-- Mathlib.Algebra.Order.Floor.Ring
Int.map_floor : ∀ {F : Type u_1} {R : Type u_2} {S : Type u_3} [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : Ring S]
  [inst_3 : LinearOrder S] [inst_4 : FloorRing R] [inst_5 : FloorRing S] [inst_6 : FunLike F R S] [RingHomClass F R S]
  (f : F), StrictMono ⇑f → ∀ (a : R), ⌊f a⌋ = ⌊a⌋
-- Mathlib.RingTheory.Regular.Flat
RingTheory.Sequence.IsWeaklyRegular.of_isLocalization : ∀ {R : Type u_1} (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] (T : Submonoid R)
  [IsLocalization T S] {rs : List R},
  RingTheory.Sequence.IsWeaklyRegular R rs → RingTheory.Sequence.IsWeaklyRegular S (List.map (⇑(algebraMap R S)) rs)
-- Mathlib.RepresentationTheory.Coinduced
/-- If `φ : G →* H` and `A : Rep k G` then `coind' φ A`, the coinduction of `A` along `φ`,
is defined as an `H`-action on `Hom_{k[G]}(k[H], A)`. If `f : k[H] → A` is `G`-equivariant
then `(h • f) (r • h₁) := r • f (h₁ * h)`, where `r : k`.
 -/
Representation.coind' : {k : Type u} →
  {G : Type v} →
    {H : Type w} →
      [inst : CommRing k] →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] →
            (φ : G →* H) → (A : Rep.{max u w, u, v} k G) → Representation k H (Rep.res φ (Rep.leftRegular k H) ⟶ A)
-- Lean.Parser.Command
Lean.Parser.Command.openHiding.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Tactic.Linarith.NNRealPreprocessor
/-- `isNNRealProp tp` is true iff `tp` is an inequality or equality between nonnegative real numbers
or the negation thereof.
 -/
Mathlib.Tactic.Linarith.isNNRealProp : Lean.Expr → Lean.MetaM Bool
-- Mathlib.LinearAlgebra.Matrix.PosDef
Matrix.PosDef.diag_pos : ∀ {n : Type u_2} {R : Type u_3} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : StarRing R] [Nontrivial R]
  {A : Matrix n n R}, A.PosDef → ∀ {i : n}, 0 < A i i
-- Mathlib.Geometry.Manifold.Algebra.LieGroup
/-- An additive Lie group is an additive topological group. This is not an instance
for technical reasons, see note [Design choices about smooth algebraic structures].  -/
topologicalAddGroup_of_lieAddGroup : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {H : Type u_2} [inst_1 : TopologicalSpace H] {E : Type u_3}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] (I : ModelWithCorners 𝕜 E H) (n : WithTop ℕ∞)
  {G : Type u_4} [inst_4 : TopologicalSpace G] [inst_5 : ChartedSpace H G] [inst_6 : AddGroup G] [LieAddGroup I n G],
  IsTopologicalAddGroup G
-- Mathlib.Topology.Algebra.Category.ProfiniteGrp.Basic
ProfiniteAddGrp.instFaithfulProfiniteForget₂ContinuousAddMonoidHomCarrierToTopTotallyDisconnectedSpaceToProfiniteContinuousMap : (CategoryTheory.forget₂ ProfiniteAddGrp.{u_1} Profinite).Faithful
-- Init.Data.String.Slice
String.Slice.RevSplitIterator.operating.inj : ∀ {σ : String.Slice → Type} {ρ : Type} {pat : ρ} {s : String.Slice}
  {inst : String.Slice.Pattern.ToBackwardSearcher pat σ} {currPos : s.Pos}
  {searcher : Std.Iter (String.Slice.Pattern.SearchStep s)} {currPos_1 : s.Pos}
  {searcher_1 : Std.Iter (String.Slice.Pattern.SearchStep s)},
  String.Slice.RevSplitIterator.operating currPos searcher =
      String.Slice.RevSplitIterator.operating currPos_1 searcher_1 →
    currPos = currPos_1 ∧ searcher = searcher_1
-- Mathlib.CategoryTheory.Sites.Hypercover.ZeroFamily
CategoryTheory.PreZeroHypercoverFamily.mk : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    (property : ⦃X : C⦄ → CategoryTheory.ObjectProperty (CategoryTheory.PreZeroHypercover X)) →
      (∀ {X : C} {E : CategoryTheory.PreZeroHypercover X}, property E ↔ property E.shrink) →
        CategoryTheory.PreZeroHypercoverFamily C
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.zero_ne_one_cert.eq_1 : ∀ (p : Lean.Grind.Linarith.Poly),
  Lean.Grind.Linarith.zero_ne_one_cert p = (p == Lean.Grind.Linarith.Poly.add 1 0 Lean.Grind.Linarith.Poly.nil)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ \ t₂}, (t₁ \ t₂).getKey k h_mem = t₁.getKey k ⋯
-- Aesop.Forward.Match.Types
/-- The match.  -/
Aesop.ForwardRuleMatch.match : Aesop.ForwardRuleMatch → Aesop.CompleteMatch
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.image_source_inter_eq' : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set X), ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' s
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.minEntry?.match_1.eq_1 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l : Std.DTreeMap.Internal.Impl α β) →
            (size_1 : ℕ) →
              (k_1 : α) →
                (v_1 : β k_1) →
                  (l_1 r : Std.DTreeMap.Internal.Impl α β) →
                    l = Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r →
                      (r_1 : Std.DTreeMap.Internal.Impl α β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v
                            (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) r_1)),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r => h_2 size k v r
    | Std.DTreeMap.Internal.Impl.inner size k v (l@h:(Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)) r_1 =>
      h_3 size k v l size_1 k_1 v_1 l_1 r h r_1) =
    h_1 ()
-- Mathlib.LinearAlgebra.AffineSpace.AffineMap
AffineMap.neg_linear : ∀ {k : Type u_1} {V1 : Type u_2} {P1 : Type u_3} {V2 : Type u_4} [inst : Ring k] [inst_1 : AddCommGroup V1]
  [inst_2 : Module k V1] [inst_3 : AddTorsor V1 P1] [inst_4 : AddCommGroup V2] [inst_5 : Module k V2] (f : P1 →ᵃ[k] V2),
  (-f).linear = -f.linear
-- Mathlib.LinearAlgebra.Dimension.Free
/-- Two finite and free modules are isomorphic if they have the same (finite) rank.  -/
FiniteDimensional.nonempty_linearEquiv_of_finrank_eq : ∀ {R : Type u} {M : Type v} {M' : Type v'} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [Module.Free R M] [inst_4 : AddCommMonoid M'] [inst_5 : Module R M'] [Module.Free R M'] [StrongRankCondition R]
  [Module.Finite R M] [Module.Finite R M'], Module.finrank R M = Module.finrank R M' → Nonempty (M ≃ₗ[R] M')
-- Mathlib.RingTheory.SimpleModule.Basic
RingEquiv.isSemisimpleRing_iff : ∀ {R : Type u_2} {S : Type u_3} [inst : Ring R] [inst_1 : Ring S] (e : R ≃+* S), IsSemisimpleRing R ↔ IsSemisimpleRing S
-- Init.Data.ToString.Basic
instToStringExcept : {ε : Type u_1} → {α : Type u_2} → [ToString ε] → [ToString α] → ToString (Except ε α)
-- Mathlib.RingTheory.Polynomial.Pochhammer
ascPochhammer_nat_eval_succ : ∀ (r n : ℕ), n * Polynomial.eval (n + 1) (ascPochhammer ℕ r) = (n + r) * Polynomial.eval n (ascPochhammer ℕ r)
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.mk_lt_mk_iff_of_comm : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X A₁ A₂ : C} {i₁ : A₁ ⟶ X} {i₂ : A₂ ⟶ X}
  [inst_1 : CategoryTheory.Mono i₁] [inst_2 : CategoryTheory.Mono i₂] (f : A₁ ⟶ A₂),
  CategoryTheory.CategoryStruct.comp f i₂ = i₁ →
    (CategoryTheory.Subobject.mk i₁ < CategoryTheory.Subobject.mk i₂ ↔ ¬CategoryTheory.IsIso f)
-- Mathlib.Data.List.Forall2
Relator.BiUnique.forall₂ : ∀ {α : Type u_1} {β : Type u_2} {R : α → β → Prop}, Relator.BiUnique R → Relator.BiUnique (List.Forall₂ R)
-- Mathlib.Combinatorics.SimpleGraph.LapMatrix
SimpleGraph.lapMatrix_mulVec_const_eq_zero : ∀ {V : Type u_1} {R : Type u_2} [inst : Fintype V] (G : SimpleGraph V) [inst_1 : DecidableRel G.Adj]
  [inst_2 : DecidableEq V] [inst_3 : NonAssocRing R], ((SimpleGraph.lapMatrix R G).mulVec fun x => 1) = 0
-- Mathlib.Analysis.Complex.Hadamard
Complex.HadamardThreeLines.F.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) [inst_1 : NormedSpace ℂ E] (ε : ℝ) (z : ℂ),
  Complex.HadamardThreeLines.F f ε z = Complex.HadamardThreeLines.invInterpStrip f z ε • f z
-- Mathlib.MeasureTheory.OuterMeasure.Induced
MeasureTheory.le_extend : ∀ {α : Type u_2} {P : α → Prop} (m : (s : α) → P s → ENNReal) {s : α} (h : P s), m s h ≤ MeasureTheory.extend m s
-- Mathlib.Topology.Order.Monotone
/-- An antitone function continuous at the supremum of a nonempty set sends this supremum to
the infimum of the image of this set.  -/
AntitoneOn.map_csSup_of_continuousWithinAt : ∀ {α : Type u_1} {β : Type u_2} [inst : ConditionallyCompleteLinearOrder α] [inst_1 : TopologicalSpace α]
  [OrderTopology α] [inst_3 : ConditionallyCompleteLinearOrder β] [inst_4 : TopologicalSpace β] [OrderClosedTopology β]
  {f : α → β} {A : Set α},
  ContinuousWithinAt f A (sSup A) →
    AntitoneOn f A →
      A.Nonempty →
        autoParam (BddAbove A) AntitoneOn.map_csSup_of_continuousWithinAt._auto_1 → f (sSup A) = sInf (f '' A)
-- Mathlib.Algebra.Group.Submonoid.Operations
AddMonoidHom.mrange_id : ∀ {M : Type u_1} [inst : AddZeroClass M], AddMonoidHom.mrange (AddMonoidHom.id M) = ⊤
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_6 : HSub Std.Time.Millisecond.Offset Std.Time.Nanosecond.Offset Std.Time.Nanosecond.Offset
-- Mathlib.Data.List.Shortlex
List.shortlex_nil_or_eq_nil : ∀ {α : Type u_1} {r : α → α → Prop} (s : List α), List.Shortlex r [] s ∨ s = []
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.contains'.match_1.eq_3 : ∀ (motive : Ordering → Sort u_1) (h_1 : Unit → motive Ordering.lt) (h_2 : Unit → motive Ordering.gt)
  (h_3 : Unit → motive Ordering.eq),
  (match Ordering.eq with
    | Ordering.lt => h_1 ()
    | Ordering.gt => h_2 ()
    | Ordering.eq => h_3 ()) =
    h_3 ()
-- Batteries.Data.List.Lemmas
List.disjoint_nil_right : ∀ {α : Type u_1} (l : List α), l.Disjoint []
-- Mathlib.Algebra.BigOperators.Group.List.Lemmas
List.sum_isAddUnit : ∀ {M : Type u_4} [inst : AddMonoid M] {L : List M}, (∀ m ∈ L, IsAddUnit m) → IsAddUnit L.sum
-- Mathlib.Probability.Process.Adapted
MeasureTheory.IsProgressive.finsetSum : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {f : MeasureTheory.Filtration ι m}
  {β : Type u_3} {mi : MeasurableSpace ι} {mβ : MeasurableSpace β} {γ : Type u_4} [inst_1 : AddCommMonoid β]
  [MeasurableAdd₂ β] {U : γ → ι → Ω → β} {s : Finset γ},
  (∀ c ∈ s, MeasureTheory.IsProgressive f (U c)) → MeasureTheory.IsProgressive f fun i ω => ∑ c ∈ s, U c i ω
-- Mathlib.Data.List.Infix
List.mem_of_mem_dropSlice : ∀ {α : Type u_1} {n m : ℕ} {l : List α} {a : α}, a ∈ List.dropSlice n m l → a ∈ l
-- Mathlib.Geometry.Manifold.Algebra.Monoid
contMDiffAt_finsetSum : ∀ {ι : Type u_1} {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {n : WithTop ℕ∞} {H : Type u_3}
  [inst_1 : TopologicalSpace H] {E : Type u_4} [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E]
  {I : ModelWithCorners 𝕜 E H} {G : Type u_5} [inst_4 : AddCommMonoid G] [inst_5 : TopologicalSpace G]
  [inst_6 : ChartedSpace H G] [ContMDiffAdd I n G] {E' : Type u_6} [inst_8 : NormedAddCommGroup E']
  [inst_9 : NormedSpace 𝕜 E'] {H' : Type u_7} [inst_10 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M : Type u_8} [inst_11 : TopologicalSpace M] [inst_12 : ChartedSpace H' M] {x : M} {t : Finset ι} {f : ι → M → G},
  (∀ i ∈ t, ContMDiffAt I' I n (f i) x) → ContMDiffAt I' I n (fun x => ∑ i ∈ t, f i x) x
-- Init.Control.Lawful.MonadLift.Basic
/-- Lifting preserves `pure`  -/
LawfulMonadLift.monadLift_pure : ∀ {m : semiOutParam (Type u → Type v)} {n : Type u → Type w} {inst : Monad m} {inst_1 : Monad n}
  {inst_2 : MonadLift m n} [self : LawfulMonadLift m n] {α : Type u} (a : α), MonadLift.monadLift (pure a) = pure a