mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Group.Pi.Lemmas
/-- A family of monoid homomorphisms `f i : M i →* N i` defines a monoid homomorphism
`MonoidHom.piMap f : (Π i, M i) →* (Π i, N i)`
given by `MonoidHom.piMap f x i = f i x`. This is `Pi.map` for `MonoidHom`s.  -/
MonoidHom.piMap : {ι : Type u_1} →
  {M : ι → Type u_3} →
    {N : ι → Type u_4} →
      [inst : (i : ι) → MulOneClass (M i)] →
        [inst_1 : (i : ι) → MulOneClass (N i)] → ((i : ι) → M i →* N i) → ((i : ι) → M i) →* (i : ι) → N i
-- Mathlib.Algebra.Homology.Embedding.Connect
CochainComplex.ConnectData.cochainComplex_X : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {K : ChainComplex C ℕ} {L : CochainComplex C ℕ} (h : CochainComplex.ConnectData K L) (a : ℤ),
  h.cochainComplex.X a = CochainComplex.ConnectData.X K L a
-- Mathlib.Topology.Instances.EReal.Lemmas
EReal.limsup_const_mul_of_nonpos_of_ne_bot : ∀ {α : Type u_3} {f : Filter α} {u : α → EReal} [f.NeBot] {c : EReal},
  c ≤ 0 → c ≠ ⊥ → Filter.limsup (fun x => c * u x) f = c * Filter.liminf u f
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃'_obj_obj_obj : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (k j X₃ : C),
  (((CategoryTheory.BraidedCategory.Hexagon.functor₂₁₃' C).obj k).obj j).obj X₃ =
    CategoryTheory.MonoidalCategoryStruct.tensorObj j (CategoryTheory.MonoidalCategoryStruct.tensorObj k X₃)
-- Mathlib.Algebra.Polynomial.EraseLead
Polynomial.eraseLead_X_pow : ∀ {R : Type u_1} [inst : Semiring R] (n : ℕ), (Polynomial.X ^ n).eraseLead = 0
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.norm.injEq : ∀ (c c_1 : Lean.Meta.Grind.Arith.Cutsat.DvdCnstr),
  (Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.norm c = Lean.Meta.Grind.Arith.Cutsat.DvdCnstrProof.norm c_1) = (c = c_1)
-- Mathlib.Order.Interval.Set.Fin
Fin.preimage_val_Ici_val : ∀ {n : ℕ} (i : Fin n), Fin.val ⁻¹' Set.Ici ↑i = Set.Ici i
-- Init.Data.Dyadic.Basic
Dyadic.le_trans : ∀ {x y z : Dyadic}, x ≤ y → y ≤ z → x ≤ z
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.find?_toList_eq_none_iff_not_mem : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, List.find? (fun x => cmp x.1 k == Ordering.eq) (Std.DTreeMap.Raw.Const.toList t) = none ↔ k ∉ t
-- Mathlib.GroupTheory.GroupExtension.Basic
AddGroupExtension.Section.equivComp.eq_1 : ∀ {N : Type u_1} {G : Type u_2} [inst : AddGroup N] [inst_1 : AddGroup G] {E : Type u_3} [inst_2 : AddGroup E]
  {S : AddGroupExtension N E G} {E' : Type u_4} [inst_3 : AddGroup E'] {S' : AddGroupExtension N E' G} (σ : S.Section)
  (equiv : S.Equiv S'), σ.equivComp equiv = { toFun := ⇑equiv ∘ ⇑σ, rightInverse_rightHom := ⋯ }
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.cons.injEq : ∀ (a a_1 a_2 a_3 : Turing.ToPartrec.Code), (a.cons a_1 = a_2.cons a_3) = (a = a_2 ∧ a_1 = a_3)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.toArray_succ_succ_eq_map : ∀ {α : Type u} [inst : LE α] [DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [Std.PRange.LinearlyUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst : Std.PRange.InfinitelyUpwardEnumerable α] [inst_4 : Std.Rxi.IsAlwaysFinite α]
  [inst_5 : Std.PRange.LawfulUpwardEnumerable α] {lo : α},
  (Std.PRange.succ lo)...*.toArray = Array.map Std.PRange.succ lo...*.toArray
-- Mathlib.RingTheory.Polynomial.DegreeLT
Polynomial.degreeLT.addLinearEquiv_symm_apply_inl : ∀ {R : Type u_1} [inst : Semiring R] {m n : ℕ} (P : ↥(Polynomial.degreeLT R m)),
  ↑((Polynomial.degreeLT.addLinearEquiv R m n).symm
        ((LinearMap.inl R ↥(Polynomial.degreeLT R m) ↥(Polynomial.degreeLT R n)) P)) =
    ↑P
-- Mathlib.Algebra.Homology.HomotopyCategory.Plus
/-- The class of quasi-isomorphisms in the homotopy category of bounded below cochain
complexes.  -/
HomotopyCategory.Plus.quasiIso : (A : Type u_3) →
  [inst : CategoryTheory.Category.{v_3, u_3} A] →
    [inst_1 : CategoryTheory.Abelian A] → CategoryTheory.MorphismProperty (HomotopyCategory.Plus A)
-- Init.Data.SInt.IntToBitVec
ISize.toBitVec64_not : ∀ {a : ISize} (h : System.Platform.numBits = 64), (~~~a).toBitVec64 h = ~~~a.toBitVec64 h
-- Init.Data.Iterators.Basic
/-- This theorem is used by a `decreasing_trivial` extension. It powers automatic termination proofs
with `IterM.finitelyManySteps`.
 -/
Std.IterM.TerminationMeasures.Finite.rel_of_yield : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] {it it' : Std.IterM m β} {out : β},
  it.IsPlausibleStep (Std.IterStep.yield it' out) → { it := it' }.Rel { it := it }
-- Mathlib.Data.Nat.Choose.Bounds
Nat.choose_succ_le_two_pow : ∀ (n k : ℕ), (n + 1).choose k ≤ 2 ^ n
-- Mathlib.Topology.Algebra.InfiniteSum.Constructions
Summable.prod_factor : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : AddCommGroup α] [inst_1 : UniformSpace α] [IsUniformAddGroup α]
  [CompleteSpace α] {f : β × γ → α}, Summable f → ∀ (b : β), Summable fun c => f (b, c)
-- Mathlib.Analysis.Convex.Between
Function.Injective.wbtw_map_iff : ∀ {R : Type u_1} {V : Type u_2} {V' : Type u_3} {P : Type u_4} {P' : Type u_5} [inst : Ring R] [inst_1 : PartialOrder R]
  [inst_2 : AddCommGroup V] [inst_3 : Module R V] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup V']
  [inst_6 : Module R V'] [inst_7 : AddTorsor V' P'] {x y z : P} {f : P →ᵃ[R] P'},
  Function.Injective ⇑f → (Wbtw R (f x) (f y) (f z) ↔ Wbtw R x y z)
-- Init.Data.UInt.Bitwise
UInt32.left_le_or : ∀ {a b : UInt32}, a ≤ a ||| b
-- Init.Data.List.ToArray
List.popWhile_toArray : ∀ {α : Type u_1} (p : α → Bool) (l : List α), Array.popWhile p l.toArray = (List.dropWhile p l.reverse).reverse.toArray
-- Mathlib.Order.Interval.Basic
Interval.disjoint_coe : ∀ {α : Type u_1} [inst : Lattice α] (s t : Interval α), Disjoint ↑s ↑t ↔ Disjoint s t
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsLoop.closure : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsLoop e → M.closure {e} = M.loops
-- Mathlib.CategoryTheory.Monoidal.Bimod
Bimod.actRight_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {A B : CategoryTheory.Mon C} (self : Bimod A B),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft self.X CategoryTheory.MonObj.one) self.actRight =
    (CategoryTheory.MonoidalCategoryStruct.rightUnitor self.X).hom
-- Mathlib.ModelTheory.Arithmetic.Presburger.Semilinear.Defs
IsLinearSet.singleton : ∀ {M : Type u_1} [inst : AddCommMonoid M] (a : M), IsLinearSet {a}
-- Mathlib.SetTheory.Cardinal.Finite
Nat.card_congr : ∀ {α : Type u_1} {β : Type u_2} (f : α ≃ β), Nat.card α = Nat.card β
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.instAlgebra : {K : Type u_1} →
  [inst : Field K] →
    (v : NumberField.InfinitePlace K) →
      (R : Type u_2) →
        [inst_1 : CommSemiring R] →
          [inst_2 : Algebra R (WithAbs ↑v)] → [UniformContinuousConstSMul R (WithAbs ↑v)] → Algebra R v.Completion
-- Init.Data.List.Erase
List.erase_filter : ∀ {α : Type u_1} [inst : BEq α] {a : α} [LawfulBEq α] {f : α → Bool} {l : List α},
  (List.filter f l).erase a = List.filter f (l.erase a)
-- Mathlib.Analysis.Normed.Operator.BoundedLinearMaps
ContinuousOn.continuousLinearMapCoprod : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  {G : Type u_4} [inst_5 : SeminormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {X : Type u_5}
  [inst_7 : TopologicalSpace X] {f : X → E →L[𝕜] G} {g : X → F →L[𝕜] G} {s : Set X},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun x => (f x).coprod (g x)) s
-- Init.Data.Nat.Lemmas
Nat.add_lt_add_iff_right : ∀ {k n m : ℕ}, n + k < m + k ↔ n < m
-- Mathlib.NumberTheory.ArithmeticFunction.VonMangoldt
ArithmeticFunction.log_mul_moebius_eq_vonMangoldt : ArithmeticFunction.log * ↑ArithmeticFunction.moebius = ArithmeticFunction.vonMangoldt
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
AddEquiv.toAddEquiv_toContinuousAddEquiv : ∀ {G : Type u} [inst : TopologicalSpace G] {H : Type v} [inst_1 : TopologicalSpace H] [inst_2 : Add G] [inst_3 : Add H]
  {e : G ≃+ H} (he : ∀ (s : Set H), IsOpen (⇑e ⁻¹' s) ↔ IsOpen s), ↑(e.toContinuousAddEquiv he) = e
-- Mathlib.Topology.Order.OrderClosed
continuousWithinAt_Ico_iff_Ici : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [ClosedIciTopology α]
  [inst_3 : TopologicalSpace β] {a b : α} {f : α → β},
  b < a → (ContinuousWithinAt f (Set.Ico b a) b ↔ ContinuousWithinAt f (Set.Ici b) b)
-- Std.Data.Internal.List.Associative
Std.Internal.List.getKey?_insertListIfNewUnit_of_contains_eq_false_of_mem : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k k' : α},
  (k == k') = true →
    Std.Internal.List.containsKey k l = false →
      List.Pairwise (fun a b => (a == b) = false) toInsert →
        k ∈ toInsert → Std.Internal.List.getKey? k' (Std.Internal.List.insertListIfNewUnit l toInsert) = some k
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.get?_terminates_le : ∀ {α : Type u} {s : Stream'.WSeq α} {m n : ℕ}, m ≤ n → (s.get? n).Terminates → (s.get? m).Terminates
-- Mathlib.Data.Rel
SetRel.symm : ∀ {α : Type u_1} (R : SetRel α α) {a b : α} [R.IsSymm], (a, b) ∈ R → (b, a) ∈ R
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.canonicalEquiv_trans_canonicalEquiv : ∀ {R : Type u_1} [inst : CommRing R] (S : Submonoid R) (P : Type u_2) [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (P' : Type u_3) [inst_3 : CommRing P'] [inst_4 : Algebra R P'] [inst_5 : IsLocalization S P]
  [inst_6 : IsLocalization S P'] (P'' : Type u_5) [inst_7 : CommRing P''] [inst_8 : Algebra R P'']
  [inst_9 : IsLocalization S P''],
  (FractionalIdeal.canonicalEquiv S P P').trans (FractionalIdeal.canonicalEquiv S P' P'') =
    FractionalIdeal.canonicalEquiv S P P''
-- Mathlib.CategoryTheory.Presentable.StrongGenerator
CategoryTheory.IsCardinalFilteredGenerator.of_isDense : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.LocallySmall.{w, v, u} C] {J : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} J] [CategoryTheory.EssentiallySmall.{w, v', u'} J]
  (F : CategoryTheory.Functor J C) [F.IsDense] (κ : Cardinal.{w}) [inst_5 : Fact κ.IsRegular]
  [∀ (j : J), CategoryTheory.IsCardinalPresentable (F.obj j) κ]
  [∀ (X : C), CategoryTheory.IsCardinalFiltered (CategoryTheory.CostructuredArrow F X) κ],
  (⊤.map F).IsCardinalFilteredGenerator κ
-- Mathlib.RingTheory.Etale.StandardEtale
StandardEtalePair.equivMvPolynomialQuotient.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (P : StandardEtalePair R),
  P.equivMvPolynomialQuotient =
    (Ideal.span {Polynomial.C P.f, Polynomial.X * Polynomial.C P.g - 1}).quotientEquivAlg
      (Ideal.span
        {(Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.C P.f),
          (Polynomial.Bivariate.equivMvPolynomial R) (Polynomial.X * Polynomial.C P.g - 1)})
      (Polynomial.Bivariate.equivMvPolynomial R) ⋯
-- Lean.Elab.Match
_private.Lean.Elab.Match.0.Lean.Elab.Term.elabMatchTypeAndDiscrs.expandDiscrIdent : Lean.Syntax → Lean.MetaM Lean.Syntax
-- Mathlib.Data.Finsupp.Basic
Finsupp.prod_mapDomain_index_inj : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_5} {N : Type u_6} [inst : AddCommMonoid M] [inst_1 : CommMonoid N]
  {f : α → β} {s : α →₀ M} {h : β → M → N},
  Function.Injective f → (Finsupp.mapDomain f s).prod h = s.prod fun a b => h (f a) b
-- Mathlib.Algebra.Lie.Weights.Basic
/-- A Lie module `M` of a Lie algebra `L` is triangularizable if the endomorphism of `M` defined by
any `x : L` is triangularizable.  -/
LieModule.IsTriangularizable : (R : Type u_2) →
  (L : Type u_3) →
    (M : Type u_4) →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : LieAlgebra R L] →
            [inst_3 : AddCommGroup M] → [inst_4 : Module R M] → [inst_5 : LieRingModule L M] → [LieModule R L M] → Prop
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.instToJsonLeanServerCapabilities : Lean.ToJson Lean.Lsp.LeanServerCapabilities
-- Mathlib.Order.Filter.Lift
Filter.lift_iInf : ∀ {α : Type u_1} {β : Type u_2} {ι : Sort u_4} [Nonempty ι] {f : ι → Filter α} {g : Set α → Filter β},
  (∀ (s t : Set α), g (s ∩ t) = g s ⊓ g t) → (iInf f).lift g = ⨅ i, (f i).lift g
-- Mathlib.Algebra.Homology.SpectralObject.SpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyIso'.eq_1 : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  (r r' : ℤ) (hrr' : r + 1 = r') (hr : r₀ ≤ r) (pq pq' pq'' : κ) (hpq : (c r).prev pq' = pq)
  (hpq' : (c r).next pq' = pq'') (i₀' i₀ i₁ i₂ i₃ i₃' : ι) (hi₀' : i₀' = data.i₀ r' pq' ⋯) (hi₀ : i₀ = data.i₀ r pq' ⋯)
  (hi₁ : i₁ = data.i₁ pq') (hi₂ : i₂ = data.i₂ pq') (hi₃ : i₃ = data.i₃ r pq' ⋯) (hi₃' : i₃' = data.i₃ r' pq' ⋯)
  (n₀ n₁ n₂ : ℤ) (hn₁' : n₁ = data.deg pq') [inst_3 : X.HasSpectralSequence data] (hn₁ : n₀ + 1 = n₁)
  (hn₂ : n₁ + 1 = n₂),
  CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyIso' X data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀ i₁
      i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' hn₁ hn₂ =
    (CategoryTheory.Abelian.SpectralObject.SpectralSequence.homologyData X data r r' hrr' hr pq pq' pq'' hpq hpq' i₀' i₀
            i₁ i₂ i₃ i₃' hi₀' hi₀ hi₁ hi₂ hi₃ hi₃' n₀ n₁ n₂ hn₁' ⋯ ⋯).left.homologyIso ≪≫
      (CategoryTheory.Abelian.SpectralObject.SpectralSequence.pageXIso X data r' ⋯ pq' i₀' i₁ i₂ i₃' hi₀' hi₁ hi₂ hi₃'
          n₀ n₁ n₂ hn₁' ⋯ ⋯).symm
-- Lean.Environment
Lean.PersistentEnvExtensionState.mk.inj : ∀ {α σ : Type} {importedEntries : Array (Array α)} {state : σ} {importedEntries_1 : Array (Array α)} {state_1 : σ},
  { importedEntries := importedEntries, state := state } = { importedEntries := importedEntries_1, state := state_1 } →
    importedEntries = importedEntries_1 ∧ state = state_1
-- Mathlib.Order.Disjoint
codisjoint_self : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, Codisjoint a a ↔ a = ⊤
-- Mathlib.Order.BoundedOrder.Monotone
Monotone.ball : ∀ {α : Type u} {β : Type v} [inst : Preorder α] {P : β → α → Prop} {s : Set β},
  (∀ x ∈ s, Monotone (P x)) → Monotone fun y => ∀ x ∈ s, P x y
-- Mathlib.RingTheory.FreeCommRing
FreeRing.FreeCommRing.instCoe : (α : Type u) → Coe (FreeRing α) (FreeCommRing α)
-- Batteries.Tactic.GeneralizeProofs
Batteries.Tactic.GeneralizeProofs.AContext.mk : Array Lean.Expr →
  Lean.ExprMap Lean.Expr →
    ℕ → Lean.LocalContext → Batteries.Tactic.GeneralizeProofs.Config → Batteries.Tactic.GeneralizeProofs.AContext
-- Std.Async.Signal
/-- Continue after stop.
 -/
Std.Async.Signal.sigcont : Std.Async.Signal
-- Mathlib.Topology.Algebra.Valued.LocallyCompact
Valued.maximalIdeal.eq_1 : ∀ (K : Type u_1) [inst : Field K] {Γ₀ : Type u_2} [inst_1 : LinearOrderedCommGroupWithZero Γ₀] [vK : Valued K Γ₀],
  Valued.maximalIdeal K = IsLocalRing.maximalIdeal ↥(Valued.integer K)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
/-- Sometimes rewriting with `comp_c_app` doesn't work because of dependent type issues.
In that case, `erw comp_c_app_assoc` might make progress.
The lemma `comp_c_app_assoc` is also better suited for rewrites in the opposite direction.  -/
AlgebraicGeometry.PresheafedSpace.comp_c_app_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {X Y Z : AlgebraicGeometry.PresheafedSpace C} (α : X ⟶ Y)
  (β : Y ⟶ Z) (U : (TopologicalSpace.Opens ↑↑Z)ᵒᵖ) {Z_1 : C}
  (h : ((TopCat.Presheaf.pushforward C (CategoryTheory.CategoryStruct.comp α β).base).obj X.presheaf).obj U ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.CategoryStruct.comp α β).c.app U) h =
    CategoryTheory.CategoryStruct.comp (β.c.app U)
      (CategoryTheory.CategoryStruct.comp
        (α.c.app (Opposite.op ((TopologicalSpace.Opens.map β.base).obj (Opposite.unop U)))) h)
-- Mathlib.Topology.Algebra.Monoid
continuousOn_pow : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : Monoid M] [ContinuousMul M] {s : Set M} (n : ℕ),
  ContinuousOn (fun x => x ^ n) s
-- Std.Sat.CNF.Basic
Std.Sat.CNF.not_VarMem_empty : ∀ {α : Type u_1} {v : α}, ¬Std.Sat.CNF.VarMem v Std.Sat.CNF.empty
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.minKeyD.match_1.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : Std.DTreeMap.Internal.Impl α β → α → Sort u_3)
  (x : Std.DTreeMap.Internal.Impl α β) (x_1 : α)
  (h_1 : (fallback : α) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β k) →
          (r : Std.DTreeMap.Internal.Impl α β) →
            (x : α) → motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x)
  (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 α β) →
                        (fallback : α) →
                          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)
                            fallback)
  (size : ℕ) (k : α) (v : β k) (r : Std.DTreeMap.Internal.Impl α β) (x_2 : α),
  x = Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r →
    x_1 = x_2 →
      (match x, x_1 with
        | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
        | Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r, x => h_2 size k v r x
        | 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,
          fallback => h_3 size k v l size_1 k_1 v_1 l_1 r h r_1 fallback) ≍
        h_2 size k v r x_2
-- Init.Data.SInt.Lemmas
ISize.toInt_ofNat' : ∀ {n : ℕ}, (ISize.ofNat n).toInt = (↑n).bmod ISize.size
-- Mathlib.Analysis.Convex.Hull
segment_subset_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : Module 𝕜 E] {s : Set E} {x y : E}, x ∈ s → y ∈ s → segment 𝕜 x y ⊆ (convexHull 𝕜) s
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.hasEqualizers : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive],
  CategoryTheory.Limits.HasEqualizers D
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupNorm.coe_sup : ∀ {E : Type u_3} [inst : AddGroup E] (p q : AddGroupNorm E), ⇑(p ⊔ q) = ⇑p ⊔ ⇑q
-- Mathlib.Probability.Kernel.Defs
/-- **Alias** of `smul_apply`. -/
ProbabilityTheory.Kernel.nsmul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Mathlib.Data.Finset.NAry
Finset.image₂.eq_1 : ∀ {α : Type u_1} {β : Type u_3} {γ : Type u_5} [inst : DecidableEq γ] (f : α → β → γ) (s : Finset α) (t : Finset β),
  Finset.image₂ f s t = Finset.image (Function.uncurry f) (s ×ˢ t)
-- Mathlib.Algebra.Group.Subsemigroup.Membership
AddSubsemigroup.mem_sSup_of_mem : ∀ {M : Type u_2} [inst : Add M] {S : Set (AddSubsemigroup M)} {s : AddSubsemigroup M},
  s ∈ S → ∀ {x : M}, x ∈ s → x ∈ sSup S
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateRow_submatrix_equiv : ∀ {l : Type u_1} {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type v} [inst : DecidableEq l]
  [inst_1 : DecidableEq m] (A : Matrix m n α) (i : l) (r : o → α) (e : l ≃ m) (f : o ≃ n),
  (A.submatrix ⇑e ⇑f).updateRow i r = (A.updateRow (e i) fun j => r (f.symm j)).submatrix ⇑e ⇑f
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
/-- If `L` is a localization functor for `W` and `e : F ≅ L ⋙ G` is an isomorphism,
then `e.inv` makes `G` a pointwise right Kan extension of `F` along `L`.  -/
CategoryTheory.Functor.isPointwiseRightKanExtensionOfIsoOfIsLocalization : {C : Type u₁} →
  {D : Type u₂} →
    {H : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} H] →
            {F : CategoryTheory.Functor C H} →
              {L : CategoryTheory.Functor C D} →
                (W : CategoryTheory.MorphismProperty C) →
                  {G : CategoryTheory.Functor D H} →
                    (e : F ≅ L.comp G) →
                      [L.IsLocalization W] →
                        (CategoryTheory.Functor.RightExtension.mk G e.inv).IsPointwiseRightKanExtension
-- Mathlib.CategoryTheory.Pi.Basic
CategoryTheory.Functor.pi'CompEval_inv_app : ∀ {I : Type w₀} {C : I → Type u₁} [inst : (i : I) → CategoryTheory.Category.{v₁, u₁} (C i)] {A : Type u_1}
  [inst_1 : CategoryTheory.Category.{v_1, u_1} A] (F : (i : I) → CategoryTheory.Functor A (C i)) (i : I) (X : A),
  (CategoryTheory.Functor.pi'CompEval F i).inv.app X = CategoryTheory.CategoryStruct.id ((F i).obj X)
-- Mathlib.Data.Set.Pairwise.Basic
Set.PairwiseDisjoint.mono_on : ∀ {α : Type u_1} {ι : Type u_4} [inst : PartialOrder α] [inst_1 : OrderBot α] {s : Set ι} {f g : ι → α},
  s.PairwiseDisjoint f → (∀ ⦃i : ι⦄, i ∈ s → g i ≤ f i) → s.PairwiseDisjoint g
-- Mathlib.Topology.IndicatorConstPointwise
tendsto_indicator_const_iff_forall_eventually' : ∀ {α : Type u_1} {A : Set α} {β : Type u_2} [inst : Zero β] [inst_1 : TopologicalSpace β] {ι : Type u_3} (L : Filter ι)
  {As : ι → Set α} (b : β),
  {0}ᶜ ∈ nhds b →
    {b}ᶜ ∈ nhds 0 →
      (Filter.Tendsto (fun i => (As i).indicator fun x => b) L (nhds (A.indicator fun x => b)) ↔
        ∀ (x : α), ∀ᶠ (i : ι) in L, x ∈ As i ↔ x ∈ A)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
/-- The sine of `π / 6` is `1 / 2`.  -/
Real.sin_pi_div_six : Real.sin (Real.pi / 6) = 1 / 2
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKeyD_unitOfList_of_contains_eq_false : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α] {l : List α} {k fallback : α},
  l.contains k = false → (Std.HashMap.Raw.unitOfList l).getKeyD k fallback = fallback
-- Mathlib.CategoryTheory.Preadditive.CommGrp_
CategoryTheory.Preadditive.instGrpObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.CartesianMonoidalCategory C] → (X : C) → CategoryTheory.GrpObj X
-- Mathlib.Data.Finset.Card
/-- A two-element finset `{a, b}` has cardinality `2` iff `a ≠ b`. The reverse direction is
`Finset.card_pair`.  -/
Finset.card_pair_eq_two_iff : ∀ {α : Type u_1} {a b : α} [inst : DecidableEq α], {a, b}.card = 2 ↔ a ≠ b
-- Mathlib.Topology.Defs.Induced
Topology.IsQuotientMap.isCoinducing : ∀ {X : Type u_3} {Y : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  Topology.IsQuotientMap f → Topology.IsCoinducing f
-- Mathlib.Topology.Algebra.Module.Alternating.Topology
ContinuousAlternatingMap.completeSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} {ι : Type u_4} [inst : NormedField 𝕜] [inst_1 : AddCommGroup E]
  [inst_2 : Module 𝕜 E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : UniformSpace F] [inst_7 : IsUniformAddGroup F] [ContinuousSMul 𝕜 E] [ContinuousConstSMul 𝕜 F]
  [CompleteSpace F], Topology.IsCoherentWith {s | Bornology.IsVonNBounded 𝕜 s} → CompleteSpace (E [⋀^ι]→L[𝕜] F)