mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.MeanInequalities
/-- **AM-GM inequality - equality condition**: This theorem provides the equality condition for the
weighted version of the AM-GM inequality for real-valued nonnegative functions.

The condition is that all elements of `z` with a nonzero weight are equal to their center of mass
`∑ i ∈ s, w i * z i`; see `geom_mean_eq_arith_mean_weighted_iff_of_nonneg` for a version that
compares the elements to each other instead.  -/
Real.geom_mean_eq_arith_mean_weighted_iff_of_nonneg' : ∀ {ι : Type u} (s : Finset ι) (w z : ι → ℝ),
  (∀ i ∈ s, 0 ≤ w i) →
    ∑ i ∈ s, w i = 1 →
      (∀ i ∈ s, 0 ≤ z i) → (∏ i ∈ s, z i ^ w i = ∑ i ∈ s, w i * z i ↔ ∀ j ∈ s, w j ≠ 0 → z j = ∑ i ∈ s, w i * z i)
-- Mathlib.MeasureTheory.Group.AEStabilizer
/-- A.e. stabilizer of a set under a group action.  -/
MulAction.aestabilizer : (G : Type u_1) →
  {α : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G α] →
        {x : MeasurableSpace α} →
          (μ : MeasureTheory.Measure α) → [MeasureTheory.SMulInvariantMeasure G α μ] → Set α → Subgroup G
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.UnsatProof.eq.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.EqCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.UnsatProof.eq c = Lean.Meta.Grind.Arith.Cutsat.UnsatProof.eq c_1) = (c = c_1)
-- Mathlib.Algebra.Order.BigOperators.Group.Finset
Finset.sum_nonpos : ∀ {ι : Type u_1} {N : Type u_5} [inst : AddCommMonoid N] [inst_1 : Preorder N] {f : ι → N} {s : Finset ι}
  [AddLeftMono N], (∀ i ∈ s, f i ≤ 0) → ∑ i ∈ s, f i ≤ 0
-- Mathlib.CategoryTheory.Limits.ExactFunctor
CategoryTheory.LeftExactFunctor.whiskeringLeft_map_app : ∀ (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] {F G : C ⥤ₗ D} (η : F ⟶ G) (H : D ⥤ₗ E),
  ((CategoryTheory.LeftExactFunctor.whiskeringLeft C D E).map η).app H =
    CategoryTheory.ObjectProperty.homMk (((CategoryTheory.Functor.whiskeringLeft C D E).map η.hom).app H.obj)
-- Init.Data.List.Monadic
_private.Init.Data.List.Monadic.0.List.forIn'.loop.match_5.eq_2 : ∀ {α : Type u_1} {β : Type u_3} (as : List α) (motive : (x : List α) → β → (∃ bs, bs ++ x = as) → Sort u_2) (a : α)
  (as' : List α) (b : β) (h : ∃ bs, bs ++ a :: as' = as) (h_1 : (b : β) → (x : ∃ bs, bs ++ [] = as) → motive [] b x)
  (h_2 : (a : α) → (as' : List α) → (b : β) → (h : ∃ bs, bs ++ a :: as' = as) → motive (a :: as') b h),
  (match a :: as', b, h with
    | [], b, x => h_1 b x
    | a :: as', b, h => h_2 a as' b h) =
    h_2 a as' b h
-- Mathlib.Data.Nat.Factorization.Induction
Nat.prime_composite_induction : ∀ {motive : ℕ → Prop},
  motive 0 →
    motive 1 →
      (∀ (p : ℕ), Nat.Prime p → motive p) →
        (∀ (a : ℕ), 2 ≤ a → motive a → ∀ (b : ℕ), 2 ≤ b → motive b → motive (a * b)) → ∀ (n : ℕ), motive n
-- Mathlib.Data.ULift
ULift.ext : ∀ {α : Type u} (x y : ULift.{u_1, u} α), x.down = y.down → x = y
-- Mathlib.Topology.NhdsSet
hasBasis_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] (s : Set X), (nhdsSet s).HasBasis (fun U => IsOpen U ∧ s ⊆ U) fun U => U
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.maxKey_modify_eq_maxKey : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] {k : α} {f : β → β} {he : t.modify k f ≠ ∅}, (t.modify k f).maxKey he = t.maxKey ⋯
-- Mathlib.CategoryTheory.Adjunction.Reflective
CategoryTheory.instIsLeftAdjointOfCoreflective : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (j : CategoryTheory.Functor C D) [CategoryTheory.Coreflective j], j.IsLeftAdjoint
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.ball_zero_eq : ∀ {n : Type u_7} [inst : Fintype n] (r : ℝ), 0 ≤ r → Metric.ball 0 r = {x | ∑ i, x.ofLp i ^ 2 < r ^ 2}
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
OneHom.withBotMap.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : One M] [inst_1 : One N] (f : OneHom M N),
  f.withBotMap = { toFun := WithBot.map ⇑f, map_one' := ⋯ }
-- Mathlib.Analysis.Convolution
/-- The convolution of two real-valued functions with respect to volume.  -/
Convolution.«term_⋆_» : Lean.TrailingParserDescr
-- Init.Data.BitVec.Lemmas
BitVec.setWidth_append_eq_right : ∀ {w w' : ℕ} {a : BitVec w} {b : BitVec w'}, BitVec.setWidth w' (a ++ b) = b
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
StarAlgEquiv.ofInjective'_apply : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A]
  [inst_2 : Module R A] [inst_3 : Star A] [inst_4 : NonUnitalSemiring B] [inst_5 : Module R B] [inst_6 : Star B]
  [inst_7 : FunLike F A B] [inst_8 : NonUnitalAlgHomClass F R A B] [inst_9 : StarHomClass F A B] (f : F)
  (hf : Function.Injective ⇑f) (x : A), ↑((StarAlgEquiv.ofInjective' f hf) x) = f x
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
/-- `PUnit` is a right identity for product of measurable spaces up to a measurable equivalence.  -/
MeasurableEquiv.prodPUnit : {α : Type u_1} → [inst : MeasurableSpace α] → α × PUnit.{u_6 + 1} ≃ᵐ α
-- Mathlib.Order.Interval.Set.InitialSeg
/-- **Alias** of `Set.principalSegIioIicOfLE_apply`. -/
Set.principalSegIioIicOfLE_toRelEmbedding : ∀ {α : Type u_1} [inst : Preorder α] {i j : α} (h : i ≤ j) (k : ↑(Set.Iio i)),
  (Set.principalSegIioIicOfLE h).toRelEmbedding k = ⟨↑k, ⋯⟩
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Basic
Matrix.charpoly_of_isUpperTriangular : ∀ {R : Type u_1} [inst : CommRing R] {n : Type u_4} [inst_1 : DecidableEq n] [inst_2 : Fintype n]
  [inst_3 : LinearOrder n] (M : Matrix n n R),
  M.IsUpperTriangular → M.charpoly = ∏ i, (Polynomial.X - Polynomial.C (M i i))
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.eqToHom_fst : ∀ {C : Type u₁} [inst : CategoryTheory.CategoryStruct.{v₁, u₁} C] {D : Type u₂}
  [inst_1 : CategoryTheory.CategoryStruct.{v₂, u₂} D] {X Y : C × D} (h : X = Y),
  (CategoryTheory.eqToHom h).1 = CategoryTheory.eqToHom ⋯
-- Mathlib.Data.Matrix.ColumnRowPartitioned
Matrix.fromCols_map : ∀ {R : Type u_1} {m : Type u_2} {n₁ : Type u_6} {n₂ : Type u_7} (A₁ : Matrix m n₁ R) (A₂ : Matrix m n₂ R)
  {R' : Type u_8} (f : R → R'), (A₁.fromCols A₂).map f = (A₁.map f).fromCols (A₂.map f)
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.equiv_apply_basis : ∀ {ι : Type u_1} {ι' : Type u_2} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] {E' : Type u_7} [inst_4 : Fintype ι']
  [inst_5 : NormedAddCommGroup E'] [inst_6 : InnerProductSpace 𝕜 E'] (b : OrthonormalBasis ι 𝕜 E)
  (b' : OrthonormalBasis ι' 𝕜 E') (e : ι ≃ ι') (i : ι), (b.equiv b' e) (b i) = b' (e i)
-- Mathlib.Data.Finsupp.Basic
Finsupp.sum_comapDomain : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : Zero M] [inst_1 : AddCommMonoid N] (f : α → β)
  (l : β →₀ M) (g : β → M → N) (hf : Set.BijOn f (f ⁻¹' ↑l.support) ↑l.support),
  (Finsupp.comapDomain f l ⋯).sum (g ∘ f) = l.sum g
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.prodFunctor_obj : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {C' : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C'] {D' : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} D'] (S : CategoryTheory.Functor C D) (S' : CategoryTheory.Functor C' D')
  (T : D) (T' : D') (f : CategoryTheory.CostructuredArrow (S.prod S') (T, T')),
  (CategoryTheory.CostructuredArrow.prodFunctor S S' T T').obj f =
    (CategoryTheory.CostructuredArrow.mk f.hom.1, CategoryTheory.CostructuredArrow.mk f.hom.2)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Poly.mulC_nc.go : Lean.Grind.CommRing.Poly → ℕ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly
-- Mathlib.CategoryTheory.SmallObject.Iteration.Basic
CategoryTheory.SmallObject.SuccStruct.Iteration.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} {Φ : CategoryTheory.SmallObject.SuccStruct C}
  [inst_1 : LinearOrder J] [inst_2 : SuccOrder J] [inst_3 : OrderBot J]
  [inst_4 : CategoryTheory.Limits.HasIterationOfShape J C] [inst_5 : WellFoundedLT J] {j : J} [inst_6 : SizeOf C]
  [inst_7 : SizeOf J] (F : CategoryTheory.Functor (↑(Set.Iic j)) C) (obj_bot : F.obj ⟨⊥, ⋯⟩ = Φ.X₀)
  (arrowSucc_eq :
    ∀ (i : J) (hi : i < j), CategoryTheory.SmallObject.SuccStruct.arrowSucc F i hi = Φ.toSuccArrow (F.obj ⟨i, ⋯⟩))
  (arrowMap_limit :
    ∀ (i : J) (hi : Order.IsSuccLimit i) (hij : i ≤ j) (k : J) (hk : k < i),
      CategoryTheory.SmallObject.SuccStruct.arrowMap F k i ⋯ hij =
        CategoryTheory.SmallObject.SuccStruct.arrowι (CategoryTheory.SmallObject.restrictionLT F hij) hi k hk),
  sizeOf { F := F, obj_bot := obj_bot, arrowSucc_eq := arrowSucc_eq, arrowMap_limit := arrowMap_limit } =
    1 + sizeOf F + sizeOf obj_bot
-- Mathlib.Analysis.Normed.Operator.Extend
LinearEquiv.norm_extend_le : ∀ {𝕜 : Type u_1} {𝕜₂ : Type u_2} {E : Type u_3} {Eₗ : Type u_4} {F : Type u_5} {Fₗ : Type u_6}
  [inst : NormedDivisionRing 𝕜] [inst_1 : NormedDivisionRing 𝕜₂] [inst_2 : AddCommGroup E]
  [inst_3 : NormedAddCommGroup Eₗ] [inst_4 : AddCommGroup F] [inst_5 : NormedAddCommGroup Fₗ] [inst_6 : Module 𝕜 E]
  [inst_7 : Module 𝕜 Eₗ] [inst_8 : IsBoundedSMul 𝕜 Eₗ] [inst_9 : Module 𝕜₂ F] [inst_10 : Module 𝕜₂ Fₗ]
  [inst_11 : IsBoundedSMul 𝕜₂ Fₗ] [inst_12 : CompleteSpace Eₗ] [inst_13 : CompleteSpace Fₗ] {σ₁₂ : 𝕜 →+* 𝕜₂}
  {σ₂₁ : 𝕜₂ →+* 𝕜} [inst_14 : RingHomInvPair σ₁₂ σ₂₁] [inst_15 : RingHomInvPair σ₂₁ σ₁₂] (f : E ≃ₛₗ[σ₁₂] F)
  (e₁ : E →ₗ[𝕜] Eₗ) (e₂ : F →ₗ[𝕜₂] Fₗ) (C : ℝ) (h_dense₁ : DenseRange ⇑e₁)
  (h_norm₁ : ∀ (x : E), ‖e₂ (f x)‖ ≤ C * ‖e₁ x‖) (h_dense₂ : DenseRange ⇑e₂)
  (h_norm₂ : ∃ C, ∀ (x : F), ‖e₁ (f.symm x)‖ ≤ C * ‖e₂ x‖) (x : Eₗ),
  ‖(f.extend e₁ e₂ h_dense₁ ⋯ h_dense₂ h_norm₂) x‖ ≤ C * ‖x‖
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
MeasureTheory.lintegral_indicator_const : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s → ∀ (c : ENNReal), ∫⁻ (a : α), s.indicator (fun x => c) a ∂μ = c * μ s
-- Lean.Meta.Tactic.Grind.Theorems
Lean.Meta.Grind.Origin.local.inj : ∀ {id id_1 : Lean.Name}, Lean.Meta.Grind.Origin.local id = Lean.Meta.Grind.Origin.local id_1 → id = id_1
-- Init.Data.String.Lemmas.Basic
String.pos.eq_1 : ∀ (s : String) (off : String.Pos.Raw) (h : String.Pos.Raw.IsValid s off),
  s.pos off h = String.Pos.ofToSlice (s.toSlice.pos off ⋯)
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.matrix_monotone : ∀ {R : Type u_1} (n : Type u_2) [inst : NonUnitalNonAssocRing R] [inst_1 : Fintype n], Monotone (TwoSidedIdeal.matrix n)
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.modEq_refl : ∀ {M : Type u_1} [inst : AddCommMonoid M] {p : M} (a : M), a ≡ a [PMOD p]
-- Mathlib.CategoryTheory.Adjunction.AdjointFunctorTheorems
/-- The functor `G : D ⥤ C` satisfies the *solution set condition* if for every `A : C`, there is a
family of morphisms `{f_i : A ⟶ G (B_i) // i ∈ ι}` such that given any morphism `h : A ⟶ G X`,
there is some `i ∈ ι` such that `h` factors through `f_i`.

The key part of this definition is that the indexing set `ι` lives in `Type v`, where `v` is the
universe of morphisms of the category: this is the "smallness" condition which allows the general
adjoint functor theorem to go through.
 -/
CategoryTheory.SolutionSetCondition : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u₁} → [inst_1 : CategoryTheory.Category.{v₁, u₁} D] → CategoryTheory.Functor D C → Prop
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.mk'_one : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N]
  (f : S.LocalizationMap N) (x : M), f.mk' x 1 = f x
-- Std.Http.Data.Headers.Basic
Std.Http.Header.Host.mk : Std.Http.URI.Host → Std.Http.URI.Port → Std.Http.Header.Host
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.Small.pbind : ∀ {α : Type v} {β : Type w} (P : α → Prop) (Q : (a : α) → P a → β → Prop),
  Std.Internal.Small { a // P a } →
    (∀ (a : α) (h : P a), Std.Internal.Small { b // Q a h b }) → Std.Internal.Small { b // ∃ a, ∃ (h : P a), Q a h b }
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Every kernel fork `s` is isomorphic (actually, equal) to `fork.ofι (fork.ι s) _`.  -/
CategoryTheory.Limits.isoOfι : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} → {f : X ⟶ Y} → (s : CategoryTheory.Limits.Fork f 0) → s ≅ CategoryTheory.Limits.Fork.ofι s.ι ⋯
-- Mathlib.Topology.Algebra.Monoid
/-- **Alias** of `continuous_finsetProd`. -/
continuous_finset_prod : ∀ {ι : Type u_1} {M : Type u_3} {X : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace M]
  [inst_2 : CommMonoid M] [ContinuousMul M] {f : ι → X → M} (s : Finset ι),
  (∀ i ∈ s, Continuous (f i)) → Continuous fun a => ∏ i ∈ s, f i a
-- Mathlib.Topology.Metrizable.Uniformity
/-- A `PseudoMetricSpace` instance compatible with a given `UniformSpace` structure.  -/
UniformSpace.pseudoMetricSpace : (X : Type u_2) → [inst : UniformSpace X] → [(uniformity X).IsCountablyGenerated] → PseudoMetricSpace X
-- Mathlib.CategoryTheory.FiberedCategory.Cocartesian
/-- The canonical isomorphism between the codomains of two strongly co-Cartesian arrows lying over
isomorphic objects.  -/
CategoryTheory.Functor.IsStronglyCocartesian.codomainIsoOfBaseIso : {𝒮 : Type u₁} →
  {𝒳 : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳] →
        (p : CategoryTheory.Functor 𝒳 𝒮) →
          {R S S' : 𝒮} →
            {a b b' : 𝒳} →
              {f : R ⟶ S} →
                {f' : R ⟶ S'} →
                  {g : S ≅ S'} →
                    f' = CategoryTheory.CategoryStruct.comp f g.hom →
                      (φ : a ⟶ b) →
                        (φ' : a ⟶ b') → [p.IsStronglyCocartesian f φ] → [p.IsStronglyCocartesian f' φ'] → b ≅ b'
-- Mathlib.CategoryTheory.Filtered.Final
/-- The functor `StructuredArrow.proj : StructuredArrow Y T ⥤ C` is final if `T : C ⥤ D` is final
and `C` is filtered.  -/
CategoryTheory.StructuredArrow.final_proj_of_isFiltered : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.IsFilteredOrEmpty C] (T : CategoryTheory.Functor C D) [T.Final] (Y : D),
  (CategoryTheory.StructuredArrow.proj Y T).Final
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.proj_surjective : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X), Function.Surjective S.proj
-- Mathlib.Geometry.RingedSpace.LocallyRingedSpace
AlgebraicGeometry.LocallyRingedSpace.iso_hom_base_inv_base : ∀ {X Y : AlgebraicGeometry.LocallyRingedSpace} (e : X ≅ Y),
  CategoryTheory.CategoryStruct.comp e.hom.base e.inv.base = CategoryTheory.CategoryStruct.id ↑X.toPresheafedSpace
-- Std.Data.Iterators.Lemmas.Combinators.TakeWhile
_private.Std.Data.Iterators.Lemmas.Combinators.TakeWhile.0.Std.Iter.step_takeWhile.match_1.splitter : (motive : Bool → Sort u_1) → (x : Bool) → (x = true → motive true) → (x = false → motive false) → motive x
-- Mathlib.Topology.Semicontinuity.Basic
upperSemicontinuousOn_iff_preimage_Ici : ∀ {α : Type u_4} [inst : TopologicalSpace α] {β : Type u_5} {f : α → β} {s : Set α} [inst_1 : LinearOrder β],
  UpperSemicontinuousOn f s ↔ ∀ (b : β), ∃ v, IsClosed v ∧ s ∩ f ⁻¹' Set.Ici b = s ∩ v
-- Std.Data.DTreeMap.Internal.Balancing
Std.DTreeMap.Internal.Impl.balance!.match_3.congr_eq_4 : ∀ {α : Type u_1} {β : α → Type u_2}
  (motive : Std.DTreeMap.Internal.Impl α β → Std.DTreeMap.Internal.Impl α β → Sort u_3)
  (ll lr : Std.DTreeMap.Internal.Impl α β)
  (h_1 : Unit → motive Std.DTreeMap.Internal.Impl.leaf Std.DTreeMap.Internal.Impl.leaf)
  (h_2 :
    (size : ℕ) →
      (lrk : α) →
        (lrv : β lrk) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive Std.DTreeMap.Internal.Impl.leaf (Std.DTreeMap.Internal.Impl.inner size lrk lrv l r))
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l r) Std.DTreeMap.Internal.Impl.leaf)
  (h_4 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (lrs : ℕ) →
              (lrk : α) →
                (lrv : β lrk) →
                  (lrl lrr : Std.DTreeMap.Internal.Impl α β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v l r)
                      (Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr))
  (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β) (lrs : ℕ) (lrk : α) (lrv : β lrk)
  (lrl lrr : Std.DTreeMap.Internal.Impl α β),
  ll = Std.DTreeMap.Internal.Impl.inner size k v l r →
    lr = Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr →
      (match ll, lr with
        | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.leaf => h_1 ()
        | Std.DTreeMap.Internal.Impl.leaf, Std.DTreeMap.Internal.Impl.inner size lrk lrv l r => h_2 size lrk lrv l r
        | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.leaf => h_3 size k v l r
        | Std.DTreeMap.Internal.Impl.inner size k v l r, Std.DTreeMap.Internal.Impl.inner lrs lrk lrv lrl lrr =>
          h_4 size k v l r lrs lrk lrv lrl lrr) ≍
        h_4 size k v l r lrs lrk lrv lrl lrr
-- Init.Data.Nat.Fold
_private.Init.Data.Nat.Fold.0.Nat.fold.eq_def : ∀ {α : Type u} (x : ℕ) (x_1 : (i : ℕ) → i < x → α → α) (x_2 : α),
  x.fold x_1 x_2 =
    match x, x_1, x_2 with
    | 0, f, a => a
    | n.succ, f, a => f n ⋯ (n.fold (fun i h => f i ⋯) a)
-- Init.Data.Vector.Extract
Vector.extract_append : ∀ {α : Type u_1} {n m : ℕ} {xs : Vector α n} {ys : Vector α m} {i j : ℕ},
  (xs ++ ys).extract i j = Vector.cast ⋯ (xs.extract i j ++ ys.extract (i - n) (j - n))
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
CochainComplex.HomComplex.Cochain.v_comp_XIsoOfEq_hom_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} {n : ℤ} (γ : CochainComplex.HomComplex.Cochain F G n) (p q q' : ℤ) (hpq : p + n = q)
  (hq' : q = q') {Z : C} (h : G.X q' ⟶ Z),
  CategoryTheory.CategoryStruct.comp (γ.v p q hpq)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.XIsoOfEq G hq').hom h) =
    CategoryTheory.CategoryStruct.comp (γ.v p q' ⋯) h
-- Mathlib.CategoryTheory.Limits.Shapes.Diagonal
CategoryTheory.Limits.pullbackDiagonalMapIdIso.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y : C} [inst_1 : CategoryTheory.Limits.HasPullbacks C]
  {S T : C} (f : X ⟶ T) (g : Y ⟶ T) (i : T ⟶ S) [inst_2 : CategoryTheory.Limits.HasPullback i i]
  [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp f i) (CategoryTheory.CategoryStruct.comp g i)]
  [inst_5 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.Limits.pullback.diagonal i)
      (CategoryTheory.Limits.pullback.map (CategoryTheory.CategoryStruct.comp f i)
        (CategoryTheory.CategoryStruct.comp g i) i i f g (CategoryTheory.CategoryStruct.id S) ⋯ ⋯)],
  CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i = CategoryTheory.Limits.pullbackDiagonalMapIdIso f g i
-- LeanSearchClient.LoogleSyntax
LeanSearchClient.instReprLoogleMatch.repr : LeanSearchClient.LoogleMatch → ℕ → Std.Format
-- Mathlib.Data.DFinsupp.Defs
DFinsupp.instDecidableEq : {ι : Type u} →
  {β : ι → Type v} →
    [DecidableEq ι] → [inst : (i : ι) → Zero (β i)] → [(i : ι) → DecidableEq (β i)] → DecidableEq (Π₀ (i : ι), β i)
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
CategoryTheory.SimplicialObject.Augmented.ExtraDegeneracy.s'_σ₀Iter : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X : CategoryTheory.SimplicialObject.Augmented C}
  (ed : X.ExtraDegeneracy) (n : ℕ),
  CategoryTheory.CategoryStruct.comp ed.s' (X.left.σ₀Iter n ⋯) = ed.section_.app (Opposite.op { len := n })
-- Batteries.Recycling.RBTree.WF
/-- The `balLeft` function preserves the ordering invariants.  -/
RBTree.RBNode.Ordered.balLeft : ∀ {α : Type u_1} {cmp : α → α → Ordering} {l : RBTree.RBNode α} {v : α} {r : RBTree.RBNode α},
  RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp x v) l →
    RBTree.RBNode.All (fun x => RBTree.RBNode.cmpLT cmp v x) r →
      RBTree.RBNode.Ordered cmp l → RBTree.RBNode.Ordered cmp r → RBTree.RBNode.Ordered cmp (l.balLeft v r)
-- Mathlib.Algebra.Order.Monoid.Unbundled.ExistsOfLE
ExistsMulOfLE.mk : ∀ {α : Type u} [inst : Mul α] [inst_1 : LE α], (∀ {a b : α}, a ≤ b → ∃ c, b = a * c) → ExistsMulOfLE α
-- Mathlib.Algebra.Group.Action.Defs
SMulDistribClass.mk : ∀ {G : Type u_9} {R : Type u_10} {S : Type u_11} [inst : SMul G R] [inst_1 : SMul G S] [inst_2 : SMul R S],
  (∀ (g : G) (r : R) (s : S), g • r • s = (g • r) • g • s) → SMulDistribClass G R S
-- Mathlib.Algebra.Group.Hom.Defs
map_comp_zpow' : ∀ {ι : Type u_1} {G : Type u_7} {H : Type u_8} {F : Type u_9} [inst : FunLike F G H] [inst_1 : DivInvMonoid G]
  [inst_2 : DivInvMonoid H] [MonoidHomClass F G H] (f : F),
  (∀ (x : G), f x⁻¹ = (f x)⁻¹) → ∀ (g : ι → G) (n : ℤ), ⇑f ∘ (g ^ n) = ⇑f ∘ g ^ n
-- Mathlib.Topology.Sheaves.Presheaf
TopCat.Presheaf.presheafEquivOfIso_functor_map_app : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X Y : TopCat} (H : X ≅ Y)
  {X_1 Y_1 : CategoryTheory.Functor (TopologicalSpace.Opens ↑X)ᵒᵖ C} (α : X_1 ⟶ Y_1)
  (X_2 : (TopologicalSpace.Opens ↑Y)ᵒᵖ),
  ((TopCat.Presheaf.presheafEquivOfIso C H).functor.map α).app X_2 =
    α.app (Opposite.op ((TopologicalSpace.Opens.map H.hom).obj (Opposite.unop X_2)))
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The composition of morphisms in `Φ.RightResolution X₂`.  -/
CategoryTheory.LocalizerMorphism.RightResolution.Hom.comp : {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 R' R'' : Φ.RightResolution X₂} → R.Hom R' → R'.Hom R'' → R.Hom R''
-- Mathlib.LinearAlgebra.TensorProduct.Tower
/-- Just as `TensorProduct.ext` is marked `ext` instead of `TensorProduct.ext'`, this is
a better `ext` lemma than `TensorProduct.AlgebraTensorModule.ext` below.

See note [partially-applied ext lemmas].  -/
TensorProduct.AlgebraTensorModule.curry_injective : ∀ {R : Type uR} {A : Type uA} {M : Type uM} {N : Type uN} {P : Type uP} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module R M] [inst_5 : Module A M]
  [inst_6 : IsScalarTower R A M] [inst_7 : AddCommMonoid N] [inst_8 : Module R N] [inst_9 : AddCommMonoid P]
  [inst_10 : Module R P] [inst_11 : Module A P] [inst_12 : IsScalarTower R A P],
  Function.Injective TensorProduct.AlgebraTensorModule.curry
-- Mathlib.Algebra.Lie.Basic
/-- The identity map is a morphism of Lie modules.  -/
LieModuleHom.id : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → M →ₗ⁅R,L⁆ M
-- Mathlib.RepresentationTheory.FiniteIndex
Rep.resIndAdjunction.eq_1 : ∀ (k : Type u) {G : Type v} [inst : CommRing k] [inst_1 : Group G] (S : Subgroup G)
  [inst_2 : DecidableRel ⇑(QuotientGroup.rightRel S)] [inst_3 : S.FiniteIndex],
  Rep.resIndAdjunction k S = (Rep.resCoindAdjunction k S.subtype).ofNatIsoRight (Rep.indCoindNatIso k S).symm