mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Control.Traversable.Basic
/-- An `ApplicativeTransformation` intertwines `seq`.  -/
ApplicativeTransformation.preserves_seq' : ∀ {F : Type u → Type v} [inst : Applicative F] {G : Type u → Type w} [inst_1 : Applicative G]
  (self : ApplicativeTransformation F G) {α β : Type u} (x : F (α → β)) (y : F α),
  self.app β (x <*> y) = self.app (α → β) x <*> self.app α y
-- Mathlib.Topology.Category.TopCat.Limits.Products
/-- The projection from the product as a bundled continuous map.  -/
TopCat.piπ : {ι : Type v} → (α : ι → TopCat) → (i : ι) → TopCat.of ((i : ι) → ↑(α i)) ⟶ α i
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- A binary bicone for a pair of objects `P Q : C` consists of the cone point `X`,
maps from `X` to both `P` and `Q`, and maps from both `P` and `Q` to `X`,
so that `inl ≫ fst = 𝟙 P`, `inl ≫ snd = 0`, `inr ≫ fst = 0`, and `inr ≫ snd = 𝟙 Q`  -/
CategoryTheory.Limits.BinaryBicone.inr_snd : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} (self : CategoryTheory.Limits.BinaryBicone P Q),
  CategoryTheory.CategoryStruct.comp self.inr self.snd = CategoryTheory.CategoryStruct.id Q
-- Mathlib.Order.CompleteLattice.Basic
iInf_unique : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] [inst_1 : Unique ι] (f : ι → α), ⨅ i, f i = f default
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getKey?_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k k' : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).getKey? k' =
        if cmp k k' = Ordering.eq then if (f (Std.DTreeMap.Raw.Const.get? t k)).isSome = true then some k else none
        else t.getKey? k'
-- Mathlib.Combinatorics.Additive.Convolution
Finset.addConvolution.eq_1 : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] (A B : Finset G) (x : G),
  A.addConvolution B x = {ab ∈ A ×ˢ B | ab.1 + ab.2 = x}.card
-- Std.Do.WP.Monad
_private.Std.Do.WP.Monad.0.EStateM.run_bind.match_1.eq_1 : ∀ {ε σ α : Type u_1} (motive : EStateM.Result ε σ α → Sort u_2) (x : α) (s : σ)
  (h_1 : (x : α) → (s : σ) → motive (EStateM.Result.ok x s))
  (h_2 : (e : ε) → (s : σ) → motive (EStateM.Result.error e s)),
  (match EStateM.Result.ok x s with
    | EStateM.Result.ok x s => h_1 x s
    | EStateM.Result.error e s => h_2 e s) =
    h_1 x s
-- Mathlib.AlgebraicTopology.Quasicategory.TwoTruncated
/-- If we have a factorization `homMk f ≫ homMk g = homMk h`, this is the choice
of a structure `CompStruct f g h`.
 -/
SSet.Truncated.Edge.CompStruct.ofHomotopyCategory₂Fac : {A : SSet.Truncated 2} →
  [inst : A.Quasicategory₂] →
    {x y z : A.obj (Opposite.op { obj := { len := 0 }, property := SSet.Truncated.Quasicategory₂._proof_1 })} →
      {f : SSet.Truncated.Edge x y} →
        {g : SSet.Truncated.Edge y z} →
          {h : SSet.Truncated.Edge x z} →
            CategoryTheory.CategoryStruct.comp (SSet.Truncated.HomotopyCategory₂.homMk f)
                  (SSet.Truncated.HomotopyCategory₂.homMk g) =
                SSet.Truncated.HomotopyCategory₂.homMk h →
              f.CompStruct g h
-- Init.Data.Array.Extract
Array.takeWhile_eq_extract_findIdx_not : ∀ {α : Type u_1} {xs : Array α} {p : α → Bool}, Array.takeWhile p xs = xs.extract 0 (Array.findIdx (fun a => !p a) xs)
-- Mathlib.LinearAlgebra.Matrix.SpecialLinearGroup
Matrix.SpecialLinearGroup.map_apply_coe : ∀ {n : Type u} [inst : DecidableEq n] [inst_1 : Fintype n] {R : Type v} [inst_2 : CommRing R] {S : Type u_1}
  [inst_3 : CommRing S] (f : R →+* S) (g : Matrix.SpecialLinearGroup n R),
  ↑((Matrix.SpecialLinearGroup.map f) g) = f.mapMatrix ↑g
-- Mathlib.Logic.Godel.GodelBetaFunction
_private.Mathlib.Logic.Godel.GodelBetaFunction.0.Nat.pairwise_coprime_coprimes : ∀ {m : ℕ} (a : Fin m → ℕ), Pairwise (Function.onFun Nat.Coprime (Nat.coprimes✝ a))
-- Mathlib.CategoryTheory.Category.Cat
CategoryTheory.Cat.Hom.toNatIso_rightUnitor : ∀ {B C : CategoryTheory.Cat} (F : B ⟶ C),
  CategoryTheory.Cat.Hom.toNatIso (CategoryTheory.Bicategory.rightUnitor F) =
    CategoryTheory.eqToIso ⋯ ≪≫ F.toFunctor.rightUnitor ≪≫ CategoryTheory.eqToIso ⋯
-- Init.Data.Bool
Bool.and_left_comm : ∀ (x y z : Bool), (x && (y && z)) = (y && (x && z))
-- Mathlib.CategoryTheory.Presentable.Directed
CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal.ext : ∀ (J : Type w) [inst : CategoryTheory.SmallCategory J] (κ : Cardinal.{w})
  {D₁ D₂ : CategoryTheory.IsCardinalFiltered.exists_cardinal_directed.DiagramWithUniqueTerminal J κ},
  D₁.W = D₂.W → D₁.P = D₂.P → D₁ = D₂
-- Lean.Compiler.Specialize
Lean.Compiler.instInhabitedSpecializeAttributeKind.default : Lean.Compiler.SpecializeAttributeKind
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
/-- Let `B` be a charted space modelled on `HB`.  Then a fiber bundle `E` over a base `B` with model
fiber `F` is naturally a charted space modelled on `HB.prod F`.  -/
FiberBundle.chartedSpace : {B : Type u_2} →
  {F : Type u_4} →
    {E : B → Type u_6} →
      [inst : TopologicalSpace F] →
        [inst_1 : TopologicalSpace (Bundle.TotalSpace F E)] →
          [inst_2 : (x : B) → TopologicalSpace (E x)] →
            {HB : Type u_7} →
              [inst_3 : TopologicalSpace HB] →
                [inst_4 : TopologicalSpace B] →
                  [ChartedSpace HB B] → [FiberBundle F E] → ChartedSpace (ModelProd HB F) (Bundle.TotalSpace F E)
-- Lean.Widget.InteractiveDiagnostic
_private.Lean.Widget.InteractiveDiagnostic.0.Lean.Widget.EmbedFmt.widget.inj : ∀ {wi : Lean.Widget.WidgetInstance} {alt : Std.Format} {wi_1 : Lean.Widget.WidgetInstance} {alt_1 : Std.Format},
  Lean.Widget.EmbedFmt.widget✝ wi alt = Lean.Widget.EmbedFmt.widget✝ wi_1 alt_1 → wi = wi_1 ∧ alt = alt_1
-- Mathlib.Topology.Algebra.Module.FiniteDimension
/-- The continuous linear map induced by a linear map on a finite-dimensional space  -/
LinearMap.toContinuousLinearMap : {𝕜 : Type u} →
  [hnorm : NontriviallyNormedField 𝕜] →
    {E : Type v} →
      [inst : AddCommGroup E] →
        [inst_1 : Module 𝕜 E] →
          [inst_2 : TopologicalSpace E] →
            [IsTopologicalAddGroup E] →
              [ContinuousSMul 𝕜 E] →
                {F' : Type x} →
                  [inst_5 : AddCommGroup F'] →
                    [inst_6 : Module 𝕜 F'] →
                      [inst_7 : TopologicalSpace F'] →
                        [inst_8 : IsTopologicalAddGroup F'] →
                          [inst_9 : ContinuousSMul 𝕜 F'] →
                            [CompleteSpace 𝕜] → [T2Space E] → [FiniteDimensional 𝕜 E] → (E →ₗ[𝕜] F') ≃ₗ[𝕜] E →L[𝕜] F'
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.FixPoint.M : Type → Type
-- Mathlib.Analysis.Analytic.Constructions
hasFPowerSeriesWithinOnBall_pi_iff : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {ι : Type u_9} [inst_3 : Fintype ι] {e : E} {Fm : ι → Type u_10}
  [inst_4 : (i : ι) → NormedAddCommGroup (Fm i)] [inst_5 : (i : ι) → NormedSpace 𝕜 (Fm i)] {f : (i : ι) → E → Fm i}
  {s : Set E} {r : ENNReal} {p : (i : ι) → FormalMultilinearSeries 𝕜 E (Fm i)},
  0 < r →
    (HasFPowerSeriesWithinOnBall (fun x x_1 => f x_1 x) (FormalMultilinearSeries.pi p) s e r ↔
      ∀ (i : ι), HasFPowerSeriesWithinOnBall (f i) (p i) s e r)
-- Mathlib.Data.Set.Card
Set.ncard_le_ncard_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} (f : α → β),
  (∀ a ∈ s, f a ∈ t) → Set.InjOn f s → autoParam t.Finite Set.ncard_le_ncard_of_injOn._auto_1 → s.ncard ≤ t.ncard
-- Mathlib.Algebra.Order.Module.Defs
OrderDual.instPosSMulStrictMono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : SMul α β] [inst_3 : Zero α]
  [PosSMulStrictMono α β], PosSMulStrictMono α βᵒᵈ
-- Mathlib.Tactic.NormNum.GCD
Mathlib.Meta.NormNum.isInt_gcd : ∀ {x y nx ny : ℤ} {z : ℕ},
  Mathlib.Meta.NormNum.IsInt x nx →
    Mathlib.Meta.NormNum.IsInt y ny → nx.gcd ny = z → Mathlib.Meta.NormNum.IsNat (x.gcd y) z
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Formula
/-- The `Y`-coordinate of a representative of `P + Q` for two distinct projective point
representatives `P` and `Q` on a Weierstrass curve.

If the representatives of `P` and `Q` are equal, then this returns the value `0`.  -/
WeierstrassCurve.Projective.addY : {R : Type r} → [CommRing R] → WeierstrassCurve.Projective R → (Fin 3 → R) → (Fin 3 → R) → R
-- Mathlib.Algebra.Category.Semigrp.Basic
AddEquiv.toAddMagmaCatIso.eq_1 : ∀ {X Y : Type u} [inst : Add X] [inst_1 : Add Y] (e : X ≃+ Y),
  e.toAddMagmaCatIso =
    { hom := AddMagmaCat.ofHom e.toAddHom, inv := AddMagmaCat.ofHom e.symm.toAddHom, hom_inv_id := ⋯, inv_hom_id := ⋯ }
-- Mathlib.MeasureTheory.Category.MeasCat
/-- The Giry monad, i.e. the monadic structure associated with `Measure`.  -/
MeasCat.Giry : CategoryTheory.Monad MeasCat
-- Mathlib.Analysis.Normed.Group.Uniform
/-- A homomorphism `f` of seminormed groups is Lipschitz, if there exists a constant
`C` such that for all `x`, one has `‖f x‖ ≤ C * ‖x‖`. The analogous condition for a linear map of
(semi)normed spaces is in `Mathlib/Analysis/Normed/Operator/Basic.lean`.  -/
AddMonoidHomClass.lipschitz_of_bound : ∀ {𝓕 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F]
  [inst_2 : FunLike 𝓕 E F] [AddMonoidHomClass 𝓕 E F] (f : 𝓕) (C : ℝ),
  (∀ (x : E), ‖f x‖ ≤ C * ‖x‖) → LipschitzWith C.toNNReal ⇑f
-- Init.Data.Fin.Lemmas
Fin.cases_succ' : ∀ {n : ℕ} {motive : Fin (n + 1) → Sort u_1} {zero : motive 0} {succ : (i : Fin n) → motive i.succ} {i : ℕ}
  (h : i + 1 < n + 1), Fin.cases zero succ ⟨i.succ, h⟩ = succ ⟨i, ⋯⟩
-- Mathlib.CategoryTheory.Monoidal.Internal.Limits
CategoryTheory.Mon.instCreatesLimitForget : {J : Type w} →
  [inst : CategoryTheory.Category.{v_1, w} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        [inst_2 : CategoryTheory.MonoidalCategory C] →
          (F : CategoryTheory.Functor J (CategoryTheory.Mon C)) →
            CategoryTheory.CreatesLimit F (CategoryTheory.Mon.forget C)
-- Mathlib.MeasureTheory.Function.Jacobian
MeasureTheory.aemeasurable_toNNReal_abs_det_fderivWithin : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [FiniteDimensional ℝ E] {s : Set E}
  {f : E → E} {f' : E → E →L[ℝ] E} [inst_3 : MeasurableSpace E] [BorelSpace E] (μ : MeasureTheory.Measure E)
  [μ.IsAddHaarMeasure],
  MeasurableSet s →
    (∀ x ∈ s, HasFDerivWithinAt f (f' x) s x) → AEMeasurable (fun x => |(f' x).det|.toNNReal) (μ.restrict s)
-- Mathlib.Logic.Function.Iterate
Function.Commute.iterate_iterate : ∀ {α : Type u} {f g : α → α}, Function.Commute f g → ∀ (m n : ℕ), Function.Commute f^[m] g^[n]
-- Mathlib.LinearAlgebra.PiTensorProduct.DirectSum
PiTensorProduct.ofDirectSumEquiv_symm_lof_tprod : ∀ {R : Type u_1} {ι : Type u_2} {κ : ι → Type u_3} {M : (i : ι) → κ i → Type u_4} [inst : CommSemiring R]
  [inst_1 : (i : ι) → (j : κ i) → AddCommMonoid (M i j)] [inst_2 : (i : ι) → (j : κ i) → Module R (M i j)]
  [inst_3 : Fintype ι] [inst_4 : (i : ι) → DecidableEq (κ i)] (p : (i : ι) → κ i) (x : (i : ι) → M i (p i)),
  PiTensorProduct.ofDirectSumEquiv.symm
      ((DirectSum.lof R ((i : ι) → κ i) (fun p => PiTensorProduct R fun i => M i (p i)) p)
        ((PiTensorProduct.tprod R) x)) =
    (PiTensorProduct.tprod R) fun i => (DirectSum.lof R (κ i) (M i) (p i)) (x i)
-- Mathlib.Algebra.Group.Subgroup.Defs
AddSubgroup.mk_eq_zero : ∀ {G : Type u_1} [inst : AddGroup G] (H : AddSubgroup G) {g : G} {h : g ∈ H}, ⟨g, h⟩ = 0 ↔ g = 0
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.insertMany_cons : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α],
  m.WF → ∀ {l : List α} {k : α}, m.insertMany (k :: l) = (m.insert k).insertMany l
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.isBridge_iff_forall_cycle_notMem : ∀ {V : Type u} {G : SimpleGraph V} {e : Sym2 V},
  e ∈ G.edgeSet → (G.IsBridge e ↔ ∀ ⦃u : V⦄ (p : G.Walk u u), p.IsCycle → e ∉ p.edges)
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.div_eq_zero_iff : ∀ {R : Type u} [inst : Field R] {p q : Polynomial R}, q ≠ 0 → (p / q = 0 ↔ p.degree < q.degree)
-- Mathlib.Algebra.Ring.Hom.InjSurj
/-- Pullback `IsDomain` instance along an injective function.  -/
Function.Injective.isDomain : ∀ {α : Type u_1} {β : Type u_2} [inst : Semiring α] [IsDomain α] [inst_2 : Semiring β] {F : Type u_3}
  [inst_3 : FunLike F β α] [MonoidWithZeroHomClass F β α] (f : F), Function.Injective ⇑f → IsDomain β
-- Mathlib.Order.Filter.Tendsto
Filter.Tendsto.if' : ∀ {α : Type u_5} {β : Type u_6} {l₁ : Filter α} {l₂ : Filter β} {f g : α → β} {p : α → Prop} [inst : DecidablePred p],
  Filter.Tendsto f l₁ l₂ → Filter.Tendsto g l₁ l₂ → Filter.Tendsto (fun a => if p a then f a else g a) l₁ l₂
-- Mathlib.Topology.Instances.Int
Int.isClosedEmbedding_coe_real : Topology.IsClosedEmbedding Int.cast
-- Mathlib.FieldTheory.SeparableDegree
Polynomial.natSepDegree_X_pow_char_pow_sub_C : ∀ {F : Type u} [inst : Field F] (q : ℕ) [ExpChar F q] (n : ℕ) (y : F),
  (Polynomial.X ^ q ^ n - Polynomial.C y).natSepDegree = 1
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.instInhabitedEMatchDiagSource.default : Lean.Meta.Grind.EMatchDiagSource
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.getKey_insertManyIfNewUnit_list_of_contains : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF →
    ∀ {l : List α} {k : α} {h' : (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).contains k = true}
      (contains : m.contains k = true),
      (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKey k h' = m.getKey k contains
-- Lean.Data.JsonRpc
Lean.JsonRpc.Message.responseError.inj : ∀ {id : Lean.JsonRpc.RequestID} {code : Lean.JsonRpc.ErrorCode} {message : String} {data? : Option Lean.Json}
  {id_1 : Lean.JsonRpc.RequestID} {code_1 : Lean.JsonRpc.ErrorCode} {message_1 : String} {data?_1 : Option Lean.Json},
  Lean.JsonRpc.Message.responseError id code message data? =
      Lean.JsonRpc.Message.responseError id_1 code_1 message_1 data?_1 →
    id = id_1 ∧ code = code_1 ∧ message = message_1 ∧ data? = data?_1
-- Mathlib.Algebra.RingQuot
RingQuot.mkAlgHom_coe : ∀ (S : Type uS) [inst : CommSemiring S] {A : Type uA} [inst_1 : Semiring A] [inst_2 : Algebra S A] (s : A → A → Prop),
  ↑(RingQuot.mkAlgHom S s) = RingQuot.mkRingHom s
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat_i₀ : ∀ (r : ℤ) (pq : ℕ × ℕ) (hr : 2 ≤ r),
  CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat.i₀ r pq hr = WithBotTop.coe (-↑pq.2 - r + 2)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
CategoryTheory.BicartesianSq.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {W X Y Z : C} {f : W ⟶ X} {g : W ⟶ Y} {h : X ⟶ Z}
  {i : Y ⟶ Z} (toIsPullback : CategoryTheory.IsPullback f g h i),
  Nonempty (CategoryTheory.Limits.IsColimit (CategoryTheory.Limits.PushoutCocone.mk h i ⋯)) →
    CategoryTheory.BicartesianSq f g h i
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
Lean.Meta.Grind.Arith.Cutsat.ToIntM.run : Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM Unit → Lean.Meta.Grind.GoalM Unit
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.d₂₃_apply : ∀ (R : Type u_1) [inst : CommRing R] (L : Type u_2) [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (M : Type u_3)
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  (a : ↥(LieModule.Cohomology.twoCochain R L M)) (x y z : L),
  ((((LieModule.Cohomology.d₂₃ R L M) a) x) y) z =
    ⁅x, (a y) z⁆ - ⁅y, (a x) z⁆ + ⁅z, (a x) y⁆ - (a ⁅x, y⁆) z + (a ⁅x, z⁆) y - (a ⁅y, z⁆) x
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKey.induct_unfolding : ∀ {α : Type u} {β : α → Type v} (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.isEmpty = false → α → Prop),
  (∀ (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β)
      (x : (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false),
      (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf).isEmpty = false →
        motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x k) →
    (∀ (size : ℕ) (k : α) (v : β k) (l : Std.DTreeMap.Internal.Impl α β) (size_1 : ℕ) (k_1 : α) (v_1 : β k_1)
        (l_1 r : Std.DTreeMap.Internal.Impl α β)
        (h :
          (Std.DTreeMap.Internal.Impl.inner size k v l
                (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
            false),
        (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r)).isEmpty =
            false →
          motive (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) ⋯
              ((Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxKey ⋯) →
            motive (Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))
              h ((Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r).maxKey ⋯)) →
      ∀ (t : Std.DTreeMap.Internal.Impl α β) (h : t.isEmpty = false), motive t h (t.maxKey h)
-- Init.Data.String.Substring
/-- Retains only the specified number of characters (Unicode code points) at the beginning of a
substring, by moving its end position towards its start position.

If the substring's start position is reached, the end position is not retracted past it.
 -/
Substring.Raw.take : Substring.Raw → ℕ → Substring.Raw
-- Lean.Meta.Tactic.Injection
/-- Applies `injection` to local declarations in `mvarId`. It uses `newNames` to name the new local declarations.
`maxDepth` is the maximum recursion depth. Only local declarations that are not in `forbidden` are considered.
Recall that some of local declarations may not have been eliminated from the local context due to forward dependencies, and
we use `forbidden` to avoid non-termination when using `injections` in a loop.
 -/
Lean.Meta.injections : Lean.MVarId →
  optParam (List Lean.Name) [] → optParam ℕ 5 → optParam Lean.FVarIdSet ∅ → Lean.MetaM Lean.Meta.InjectionsResult
-- Mathlib.Tactic.ClickSuggestions.Apply
Mathlib.Tactic.ClickSuggestions.ApplyKey.mk.injEq : ∀ (numGoals nameLength replacementSize : ℕ) (name : String) (newGoals : Array Lean.Meta.AbstractMVarsResult)
  (numGoals_1 nameLength_1 replacementSize_1 : ℕ) (name_1 : String) (newGoals_1 : Array Lean.Meta.AbstractMVarsResult),
  ({ numGoals := numGoals, nameLength := nameLength, replacementSize := replacementSize, name := name,
        newGoals := newGoals } =
      { numGoals := numGoals_1, nameLength := nameLength_1, replacementSize := replacementSize_1, name := name_1,
        newGoals := newGoals_1 }) =
    (numGoals = numGoals_1 ∧
      nameLength = nameLength_1 ∧ replacementSize = replacementSize_1 ∧ name = name_1 ∧ newGoals = newGoals_1)
-- Init.Data.String.TakeDrop
/-- If `pat` matches a suffix of `s`, returns the position at the beginning of the suffix.
Returns `none` otherwise.

This function is generic over all currently supported patterns.
 -/
String.skipSuffix? : {ρ : Type} → (s : String) → (pat : ρ) → [String.Slice.Pattern.BackwardPattern pat] → Option s.Pos
-- Mathlib.Topology.LocallyFinsupp.Pushforward
Function.locallyFinsupp.map.congr_simp : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (f f_1 : X → Y)
  (e_f : f = f_1) (w w_1 : X → R),
  w = w_1 →
    ∀ [inst_2 : Semiring R] [inst_3 : PrespectralSpace Y] (hf : IsSpectralMap f) (c c_1 : Function.locallyFinsupp X R),
      c = c_1 → Function.locallyFinsupp.map f w hf c = Function.locallyFinsupp.map f_1 w_1 ⋯ c_1
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.d_snd_v : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] (i j : ℤ) (hij : i + 1 = j),
  CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone φ).d i j)
      ((CochainComplex.mappingCone.snd φ).v j j ⋯) =
    CategoryTheory.CategoryStruct.comp ((↑(CochainComplex.mappingCone.fst φ)).v i j hij) (φ.f j) +
      CategoryTheory.CategoryStruct.comp ((CochainComplex.mappingCone.snd φ).v i i ⋯) (G.d i j)
-- Std.Data.DTreeMap.Basic
Std.DTreeMap.mk : {α : Type u} →
  {β : α → Type v} →
    {cmp : autoParam (α → α → Ordering) Std.DTreeMap._auto_1} →
      (inner : Std.DTreeMap.Internal.Impl α β) → inner.WF → Std.DTreeMap α β cmp
-- Mathlib.Dynamics.OmegaLimit
omegaLimit_eq_biInter_inter : ∀ {τ : Type u_1} {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace β] (f : Filter τ) (ϕ : τ → α → β) (s : Set α)
  {v : Set τ}, v ∈ f → omegaLimit f ϕ s = ⋂ u ∈ f, closure (Set.image2 ϕ (u ∩ v) s)
-- Mathlib.GroupTheory.Coxeter.Matrix
/-- The Coxeter matrix of type H₄.

The corresponding Coxeter-Dynkin diagram is:
```
       5
    o --- o --- o --- o
```
 -/
CoxeterMatrix.H₄ : CoxeterMatrix (Fin 4)
-- Mathlib.Data.List.Dedup
List.mem_dedup : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {l : List α}, a ∈ l.dedup ↔ a ∈ l
-- Mathlib.Algebra.Order.IsBotOne
one_notMem_iff : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : One α] [IsBotOneClass α] {s : Set α}, 1 ∉ s ↔ ∀ x ∈ s, 1 < x
-- Mathlib.Tactic.Linter.MinImports
/-- `minImportsRef` keeps track of cumulative imports across multiple commands, using `ImportState`.
 -/
_private.Mathlib.Tactic.Linter.MinImports.0.Mathlib.Linter.minImportsRef : IO.Ref Mathlib.Linter.ImportState✝
-- Mathlib.Analysis.InnerProductSpace.TwoDim
Orientation.rightAngleRotation_symm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E] [inst_2 : Fact (Module.finrank ℝ E = 2)]
  (o : Orientation ℝ E (Fin 2)), o.rightAngleRotation.symm = o.rightAngleRotation.trans (LinearIsometryEquiv.neg ℝ)
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.smul_const : ∀ {lc : Lean.Omega.LinearCombo} {i : ℤ}, (i * lc).const = i * lc.const
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Trivialization.apply_mk_symm : ∀ {B : Type u_1} {F : Type u_2} {E : B → Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_3 : ∀ (x : B), Nonempty (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) {b : B}, b ∈ e.baseSet → ∀ (y : F), ↑e ⟨b, e.symm b y⟩ = (b, y)
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.preimage_mul_right_closedEBall`. -/
EMetric.preimage_mul_right_closedBall : ∀ {G : Type v} [inst : Group G] [inst_1 : PseudoEMetricSpace G] [IsIsometricSMul Gᵐᵒᵖ G] (a b : G) (r : ENNReal),
  (fun x => x * a) ⁻¹' Metric.closedEBall b r = Metric.closedEBall (b / a) r
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey?_inter_of_not_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∩ m₂).getKey? k = none
-- Mathlib.Topology.IndicatorConstPointwise
tendsto_indicator_const_iff_tendsto_pi_pure' : ∀ {α : 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)) ↔
        Filter.Tendsto (fun i x => x ∈ As i) L (Filter.pi fun x => pure (x ∈ A)))
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RankNat
SSet.Subcomplex.Pairing.isRegular_iff_nonempty_rankFunction : ∀ {X : SSet} {A : X.Subcomplex} (P : A.Pairing) [P.IsProper], P.IsRegular ↔ Nonempty (P.RankFunction ℕ)
-- Lean.Elab.PreDefinition.WF.Eqns
Lean.Elab.WF.instInhabitedEqnInfo.default : Lean.Elab.WF.EqnInfo
-- Lean.Declaration
Lean.DefinitionVal.toConstantVal : Lean.DefinitionVal → Lean.ConstantVal