mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop.0.Std.Tactic.BVDecide.BVExpr.bitblast.denote_blastCpopTree.go : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} {assign : α → Bool} (aig : Std.Sat.AIG α) (len : ℕ)
  (l : aig.RefVec (len * w)) (h : 0 < len) (bv : BitVec (len * w)),
  (∀ (idx : ℕ) (hidx : idx < len * w), ⟦assign, { aig := aig, ref := l.get idx hidx }⟧ = bv.getLsbD idx) →
    ∀ (idx : ℕ) (hidx : idx < w),
      ⟦assign,
          { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go l h).aig,
            ref := (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopTree.go l h).vec.get idx hidx }⟧ =
        bv.cpopTree.getLsbD idx
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.const_smul : ∀ {α : Type u_1} {l : Filter α} {M : Type u_5} {G : Type u_6} [inst : SMul M G] (n : M) (a : G), ↑(n • a) = n • ↑a
-- Mathlib.Analysis.Calculus.AddTorsor.AffineMap
ContDiffAt.lineMap : ∀ {𝕜 : Type u_1} {V : Type u_2} {E : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup V]
  [inst_2 : NormedSpace 𝕜 V] [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {f₁ f₂ : E → V} {g : E → 𝕜}
  {x : E} {n : WithTop ℕ∞},
  ContDiffAt 𝕜 n f₁ x →
    ContDiffAt 𝕜 n f₂ x → ContDiffAt 𝕜 n g x → ContDiffAt 𝕜 n (fun x => (AffineMap.lineMap (f₁ x) (f₂ x)) (g x)) x
-- Mathlib.Algebra.Free
FreeAddSemigroup.instDecidableEq : {α : Type u} → [DecidableEq α] → DecidableEq (FreeAddSemigroup α)
-- Lean.Parser.Do
Lean.Parser.Term.termFor : Lean.Parser.Parser
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.mkPatternFromTypeWithKey.go : {α : Type} →
  List Lean.Name →
    Lean.Expr →
      (Lean.Expr → Lean.MetaM (Lean.Expr × α)) → Lean.Expr → Array Lean.Expr → Lean.MetaM (Lean.Meta.Sym.Pattern × α)
-- Mathlib.Topology.Homeomorph.Lemmas
_private.Mathlib.Topology.Homeomorph.Lemmas.0.Fin.appendEquiv_eq_homeomorph : ∀ {X : Type u_1} [inst : TopologicalSpace X] (m n : ℕ),
  Fin.appendEquiv m n =
    (Homeomorph.sumArrowHomeomorphProdArrow.symm.trans (Homeomorph.piCongrLeft finSumFinEquiv)).toEquiv
-- Mathlib.LinearAlgebra.BilinearForm.TensorProduct
/-- The tensor product of two bilinear forms, a shorthand for dot notation.  -/
LinearMap.BilinForm.tmul : {R : Type uR} →
  {A : Type uA} →
    {M₁ : Type uM₁} →
      {M₂ : Type uM₂} →
        [inst : CommSemiring R] →
          [inst_1 : CommSemiring A] →
            [inst_2 : AddCommMonoid M₁] →
              [inst_3 : AddCommMonoid M₂] →
                [inst_4 : Algebra R A] →
                  [inst_5 : Module R M₁] →
                    [inst_6 : Module A M₁] →
                      [inst_7 : SMulCommClass R A M₁] →
                        [IsScalarTower R A M₁] →
                          [inst_9 : Module R M₂] →
                            LinearMap.BilinForm A M₁ →
                              LinearMap.BilinMap R M₂ R → LinearMap.BilinMap A (TensorProduct R M₁ M₂) A
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKey_eq_getKeyD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a fallback : α} {h : a ∈ m}, m.getKey a h = m.getKeyD a fallback
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.coe_injective : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁}
  [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂] {M₁ : Type u_4} [inst_4 : TopologicalSpace M₁]
  [inst_5 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_6 : TopologicalSpace M₂] [inst_7 : AddCommMonoid M₂]
  [inst_8 : Module R₁ M₁] [inst_9 : Module R₂ M₂], Function.Injective ContinuousLinearEquiv.toContinuousLinearMap
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- `erase p n` is the polynomial `p` in which the `X ^ n` term has been erased.  -/
SkewPolynomial.erase : {R : Type u_1} → [inst : Semiring R] → ℕ → SkewPolynomial R → SkewPolynomial R
-- Mathlib.Algebra.Lie.Cochain
LieModule.Cohomology.add_apply_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] (a b : ↥(LieModule.Cohomology.twoCochain R L M)) (x y : L),
  ((a + b) x) y = (a x) y + (b x) y
-- Mathlib.Analysis.InnerProductSpace.Adjoint
ContinuousLinearMap.norm_map_iff_adjoint_comp_self : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {H : Type u_5} [inst_1 : NormedAddCommGroup H] [inst_2 : InnerProductSpace 𝕜 H]
  [inst_3 : CompleteSpace H] {K : Type u_6} [inst_4 : NormedAddCommGroup K] [inst_5 : InnerProductSpace 𝕜 K]
  [inst_6 : CompleteSpace K] (u : H →L[𝕜] K), (∀ (x : H), ‖u x‖ = ‖x‖) ↔ ContinuousLinearMap.adjoint u ∘SL u = 1
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Mat_.id_apply_of_ne : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (M : CategoryTheory.Mat_ C) (i j : M.ι), i ≠ j → CategoryTheory.CategoryStruct.id M i j = 0
-- Mathlib.Data.Seq.Defs
Stream'.Seq.not_terminates_iff : ∀ {α : Type u} {s : Stream'.Seq α}, ¬s.Terminates ↔ ∀ (n : ℕ), (s.get? n).isSome = true
-- Init.Data.BitVec.Lemmas
BitVec.getLsbD_of_zero_length : ∀ {w i : ℕ}, w = 0 → ∀ (x : BitVec w), x.getLsbD i = false
-- Mathlib.Topology.Algebra.Field
/-- In an ordered field, the units of the nonnegative elements are the positive elements.  -/
Nonneg.unitsHomeomorphPos : (R : Type u_2) →
  [inst : DivisionSemiring R] →
    [inst_1 : PartialOrder R] →
      [inst_2 : IsStrictOrderedRing R] →
        [PosMulReflectLT R] → [inst_4 : TopologicalSpace R] → [ContinuousInv₀ R] → { r // 0 ≤ r }ˣ ≃ₜ { r // 0 < r }
-- Mathlib.Topology.ContinuousMap.T0Sierpinski
TopologicalSpace.productOfMemOpens_isInducing : ∀ (X : Type u_1) [inst : TopologicalSpace X], Topology.IsInducing ⇑(TopologicalSpace.productOfMemOpens X)
-- Mathlib.Order.Filter.Bases.Basic
Filter.IsBasis.filterBasis.congr_simp : ∀ {α : Type u_1} {ι : Sort u_4} {p p_1 : ι → Prop} (e_p : p = p_1) {s s_1 : ι → Set α} (e_s : s = s_1)
  (h : Filter.IsBasis p s), h.filterBasis = ⋯.filterBasis
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- **Alias** of `Multiset.disjoint_finsetSum_right`. -/
Multiset.disjoint_finset_sum_right : ∀ {ι : Type u_1} {α : Type u_6} {i : Finset ι} {f : ι → Multiset α} {a : Multiset α},
  Disjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b)
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.mem_adjoin_pair_right : ∀ (K : Type u_1) {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (x y : L), y ∈ K⟮x, y⟯
-- Mathlib.Data.Set.Prod
image_toPullbackDiag : ∀ {X : Type u_1} {Y : Sort u_2} (f : X → Y) (s : Set X),
  toPullbackDiag f '' s = Function.pullbackDiagonal f ∩ Subtype.val ⁻¹' s ×ˢ s
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
nsmul_lt_nsmul_right : ∀ {M : Type u_3} [inst : AddMonoid M] [inst_1 : Preorder M] [AddLeftStrictMono M] [AddRightStrictMono M] {n : ℕ},
  n ≠ 0 → ∀ {a b : M}, a < b → n • a < n • b
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.norm_intCast_lt_one_iff : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {k : ℤ}, ‖↑k‖ < 1 ↔ ↑p ∣ k
-- Std.Sat.CNF.Relabel
Std.Sat.CNF.relabel_append : ∀ {α : Type u_1} {α_1 : Type u_2} {r : α → α_1} {f1 f2 : Std.Sat.CNF α},
  Std.Sat.CNF.relabel r (f1 ++ f2) = Std.Sat.CNF.relabel r f1 ++ Std.Sat.CNF.relabel r f2
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.contains_maxKeyD : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.contains (t.maxKeyD fallback) = true
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.InternalState.mk.sizeOf_spec : ∀ (footnotes : Std.HashMap String (Lean.Doc.Ref✝ (Lean.Doc.Inline Lean.ElabInline)))
  (urls : Std.HashMap String (Lean.Doc.Ref✝ String)) (deferred : Array Lean.Doc.DeferredCheck),
  sizeOf { footnotes := footnotes, urls := urls, deferred := deferred } =
    1 + sizeOf footnotes + sizeOf urls + sizeOf deferred
-- Mathlib.Data.Fin.SuccPred
Fin.succAbove_zero_apply : ∀ {n : ℕ} (i : Fin n), Fin.succAbove 0 i = i.succ
-- Mathlib.RingTheory.AdicCompletion.Algebra
AdicCompletion.evalOneₐ.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R),
  AdicCompletion.evalOneₐ I = (Ideal.Quotient.factorₐ R ⋯).comp (AdicCompletion.evalₐ I 1)
-- Mathlib.CategoryTheory.Comma.Over.OverClass
CategoryTheory.OverClass.instHomIsOverHomOfInv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} (S : C) [inst_1 : CategoryTheory.OverClass X S]
  [inst_2 : CategoryTheory.OverClass Y S] {e : X ≅ Y} [CategoryTheory.HomIsOver e.inv S],
  CategoryTheory.HomIsOver e.hom S
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.mem_union_of_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∈ t₂ → k ∈ t₁ ∪ t₂
-- Mathlib.Data.Int.Init
Int.div_le_iff_of_dvd_of_pos : ∀ {a b c : ℤ}, 0 < b → b ∣ a → (a / b ≤ c ↔ a ≤ b * c)
-- Mathlib.GroupTheory.SemidirectProduct
/-- Define an isomorphism from `N₁ ⋊[φ₁] G₁` to `N₂ ⋊[φ₂] G₂` without specifying `φ₂`.  -/
SemidirectProduct.congr' : {N₁ : Type u_4} →
  {G₁ : Type u_5} →
    {N₂ : Type u_6} →
      {G₂ : Type u_7} →
        [inst : Group N₁] →
          [inst_1 : Group G₁] →
            [inst_2 : Group N₂] →
              [inst_3 : Group G₂] →
                {φ₁ : G₁ →* MulAut N₁} →
                  (fn : N₁ ≃* N₂) →
                    (fg : G₁ ≃* G₂) → N₁ ⋊[φ₁] G₁ ≃* N₂ ⋊[(↑(MulAut.congr fn)).comp (φ₁.comp ↑fg.symm)] G₂
-- Mathlib.Analysis.InnerProductSpace.PiL2
OrthonormalBasis.enorm_eq_one : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] (b : OrthonormalBasis ι 𝕜 E) (i : ι), ‖b i‖ₑ = 1
-- Mathlib.Order.Concept
/-- See `Concept.ext'` for a version using the intent.  -/
Concept.ext : ∀ {α : Type u_2} {β : Type u_3} {r : α → β → Prop} {c d : Concept α β r}, c.extent = d.extent → c = d
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.IsZero.eq_zero_of_src : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C},
  CategoryTheory.Limits.IsZero X → ∀ (f : X ⟶ Y), f = 0
-- Mathlib.LinearAlgebra.Span.Defs
Submodule.span_attach_biUnion : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : DecidableEq M] {α : Type u_9} (s : Finset α) (f : ↥s → Finset M),
  Submodule.span R ↑(s.attach.biUnion f) = ⨆ x, Submodule.span R ↑(f x)
-- Init.Data.String.Lemmas.Pattern.Char
_private.Init.Data.String.Lemmas.Pattern.Char.0.String.Slice.Pos.revSkipWhile.eq_1 : ∀ {ρ : Type} {s : String.Slice} (pos : s.Pos) (pat : ρ) [inst : String.Slice.Pattern.BackwardPattern pat],
  pos.revSkipWhile pat =
    match pos.revSkip? pat with
    | some nextCurr => if nextCurr < pos then nextCurr.revSkipWhile pat else pos
    | none => pos
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- If `G` preserves any pointwise left Kan extension of `F` along `L` at `c`, then it preserves
all of them.  -/
CategoryTheory.Functor.PreservesPointwiseLeftKanExtensionAt.mk' : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) (c : C) {E : L.LeftExtension F} (hE : E.IsPointwiseLeftKanExtensionAt c)
  (hGE : ((CategoryTheory.Functor.LeftExtension.postcompose₂ L F G).obj E).IsPointwiseLeftKanExtensionAt c),
  G.PreservesPointwiseLeftKanExtensionAt F L c
-- Mathlib.Algebra.Group.NatPowAssoc
npow_mul : ∀ {M : Type u_1} [inst : MulOneClass M] [inst_1 : Pow M ℕ] [NatPowAssoc M] (x : M) (m n : ℕ), x ^ (m * n) = (x ^ m) ^ n
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_of_le_mul_of_le_one_left : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b c : α}, a ≤ b * c → c ≤ 1 → a ≤ b
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
/-- Given `f : G ≃ H`, we can map `l : SkewMonoidAlgebra k G` to
`equivMapDomain f l : SkewMonoidAlgebra k H` (computably) by mapping the support forwards
and the function backwards.  -/
SkewMonoidAlgebra.equivMapDomain : {k : Type u_1} →
  {G : Type u_2} → {H : Type u_3} → [inst : AddCommMonoid k] → G ≃ H → SkewMonoidAlgebra k G → SkewMonoidAlgebra k H
-- Init.Data.String.Substring
/-- Checks whether a substring is empty.

A substring is empty if its start and end positions are the same.
 -/
Substring.Raw.isEmpty : Substring.Raw → Bool
-- Mathlib.Computability.Primrec.Basic
Primcodable.empty : Primcodable Empty
-- Lean.Meta.Tactic.Try.Collect
Lean.Meta.Try.Collector.saveLibSearchCandidates : Lean.Expr → Lean.Meta.Try.Collector.M Unit
-- Init.Grind.Config
/-- Maximum number of steps performed by the `lia` solver while searching for an assignment
satisfying the linear integer arithmetic constraints.
A step is counted for each variable processed during the search. This threshold prevents
case-split explosion in examples that require enumerating a huge number of cases
(e.g., Cooper conflict resolution with large coefficients).
When the threshold is reached, the search is interrupted, and the solver becomes incomplete.
 -/
Lean.Grind.Config.liaSteps : Lean.Grind.Config → ℕ
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.emptyWithCapacity_equiv_iff_isEmpty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {c : ℕ}, m.WF → ((Std.HashMap.Raw.emptyWithCapacity c).Equiv m ↔ m.isEmpty = true)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.mop_whiskerRight : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {X Y : C}
  (f : X ⟶ Y) (Z : C),
  (CategoryTheory.MonoidalCategoryStruct.whiskerRight f Z).mop =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft { unmop := Z } f.mop
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
MonoidAlgebra.map_sum : ∀ {ι : Type u_1} {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S)
  (s : Finset ι) (x : ι → MonoidAlgebra R M), MonoidAlgebra.map f (∑ i ∈ s, x i) = ∑ i ∈ s, MonoidAlgebra.map f (x i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey?_mem : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → ∀ {km : α}, t.minKey? = some km → km ∈ t
-- Mathlib.Algebra.Homology.BifunctorHomotopy
fromNext.eq_1 : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (i : ι), fromNext i = AddMonoidHom.mk' (fun f => f (c.next i) i) ⋯
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_toNNReal : ∀ {a : ENNReal}, a ≠ ⊤ → ↑a.toNNReal = a
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb_mul : ∀ {b x y : ℝ}, x ≠ 0 → y ≠ 0 → Real.logb b (x * y) = Real.logb b x + Real.logb b y
-- Mathlib.Data.Vector.Defs
/-- The list obtained from a vector.  -/
List.Vector.toList : {α : Type u_1} → {n : ℕ} → List.Vector α n → List α
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- Two maps from a coequalizer are equal if they are equal when composed with the coequalizer
map  -/
CategoryTheory.Limits.coequalizer.hom_ext : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasCoequalizer f g] {W : C} {k l : CategoryTheory.Limits.coequalizer f g ⟶ W},
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) k =
      CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.coequalizer.π f g) l →
    k = l
-- Std.Data.DTreeMap.Internal.Operations
_private.Std.Data.DTreeMap.Internal.Operations.0.Std.DTreeMap.Internal.Impl.minView!.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') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k' v' l' r')),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k' v' l' r' => h_2 size k' v' l' r') =
    h_1 ()
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.Std.DTreeMap.Internal.Impl.toListModel.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) → (l r : Std.DTreeMap.Internal.Impl α β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l r)),
  (match Std.DTreeMap.Internal.Impl.leaf with
    | Std.DTreeMap.Internal.Impl.leaf => h_1 ()
    | Std.DTreeMap.Internal.Impl.inner size k v l r => h_2 size k v l r) =
    h_1 ()
-- Init.Tactics
/-- `impossible by t` uses the tactic `t` to prove that the current goal is impossible
to prove.

If the goal is `xs ⊢ P`, the tactic `t` sees the goal `¬(∀ xs, P)`. Any expression metavariables in
the original goal turn into variables in the context.

Universe parameters of the surrounding declaration are kept fixed (not abstracted); the `+levels`
option turns them into fresh level metavariables instead. Universe metavariables in the goal are
rejected.

The original goal is closed as if `sorry` was used.
 -/
Lean.Parser.Tactic.impossible : Lean.ParserDescr
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwInfo.mk.injEq : ∀ (rootExpr subExpr : Lean.Expr) (rflTarget? : Option Lean.Expr) (gpos : Array Mathlib.Tactic.ClickSuggestions.GrwPos)
  (rwKind : Mathlib.Tactic.ClickSuggestions.RwKind) (rootExpr_1 subExpr_1 : Lean.Expr) (rflTarget?_1 : Option Lean.Expr)
  (gpos_1 : Array Mathlib.Tactic.ClickSuggestions.GrwPos) (rwKind_1 : Mathlib.Tactic.ClickSuggestions.RwKind),
  ({ rootExpr := rootExpr, subExpr := subExpr, rflTarget? := rflTarget?, gpos := gpos, rwKind := rwKind } =
      { rootExpr := rootExpr_1, subExpr := subExpr_1, rflTarget? := rflTarget?_1, gpos := gpos_1,
        rwKind := rwKind_1 }) =
    (rootExpr = rootExpr_1 ∧ subExpr = subExpr_1 ∧ rflTarget? = rflTarget?_1 ∧ gpos = gpos_1 ∧ rwKind = rwKind_1)
-- Mathlib.Order.Filter.Defs
Filter.mem_sSup : ∀ {α : Type u_1} {s : Set α} {S : Set (Filter α)}, s ∈ sSup S ↔ ∀ f ∈ S, s ∈ f
-- Mathlib.Probability.Independence.Kernel.IndepFun
/-- **Alias** of `ProbabilityTheory.Kernel.iIndepFun.indepFun_finsetProd_of_notMem`. -/
ProbabilityTheory.Kernel.iIndepFun.indepFun_finset_prod_of_notMem : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {mα : MeasurableSpace α} {mΩ : MeasurableSpace Ω}
  {κ : ProbabilityTheory.Kernel α Ω} {μ : MeasureTheory.Measure α} {β : Type u_8} {m : MeasurableSpace β}
  [inst : CommMonoid β] [MeasurableMul₂ β] {f : ι → Ω → β},
  ProbabilityTheory.Kernel.iIndepFun f κ μ →
    (∀ (i : ι), Measurable (f i)) →
      ∀ {s : Finset ι} {i : ι}, i ∉ s → ProbabilityTheory.Kernel.IndepFun (∏ j ∈ s, f j) (f i) κ μ
-- Init.Data.SInt.Lemmas
Int32.toBitVec_ofBitVec : ∀ (b : BitVec 32), (Int32.ofBitVec b).toBitVec = b
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.single_eq_same : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → Zero (G i)] [inst_3 : ∀ (i : ι), ZeroMemClass (S i) (G i)] (i : ι)
  (r : G i), (RestrictedProduct.single A i r) i = r
-- Mathlib.Data.List.Sort
List.orderedInsert_length : ∀ {α : Type u_1} (r : α → α → Prop) [inst : DecidableRel r] (L : List α) (a : α),
  (List.orderedInsert r a L).length = L.length + 1
-- Mathlib.GroupTheory.DoubleCoset
DoubleCoset.eq'' : ∀ {G : Type u_1} [inst : Group G] {a b : G} (H K : Subgroup G),
  DoubleCoset.mk H K a = DoubleCoset.mk H K b ↔ (DoubleCoset.setoid ↑H ↑K) a b
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_sum_comm : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] (s : Finset ι)
  (t : Finset κ) (f : ι → κ → M), (s.expect fun i => ∑ j ∈ t, f i j) = ∑ j ∈ t, s.expect fun i => f i j
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.spanSingleton_zero : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  [inst_3 : IsLocalization S P], FractionalIdeal.spanSingleton S 0 = 0
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- Conjugating preserves self-adjointness.  -/
IsSelfAdjoint.adjoint_conj : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : CompleteSpace E] [inst_6 : CompleteSpace F] {T : E →L[𝕜] E},
  IsSelfAdjoint T → ∀ (S : F →L[𝕜] E), IsSelfAdjoint (ContinuousLinearMap.adjoint S ∘SL T ∘SL S)
-- Mathlib.Analysis.SpecificLimits.Basic
NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one : ∀ {r : NNReal}, r < 1 → Filter.Tendsto (fun n => r ^ n) Filter.atTop (nhds 0)
-- Init.Data.String.TakeDrop
String.Slice.takeRight : String.Slice → ℕ → String.Slice
-- Mathlib.CategoryTheory.ObjectProperty.FiniteProducts
/-- The typeclass saying that `P : ObjectProperty C` is stable under finite coproducts.  -/
CategoryTheory.ObjectProperty.IsClosedUnderFiniteCoproducts : {C : Type u_1} → [inst : CategoryTheory.Category.{v_1, u_1} C] → CategoryTheory.ObjectProperty C → Prop
-- Mathlib.CategoryTheory.EpiMono
/-- A split mono category is a category in which every monomorphism is split.  -/
CategoryTheory.SplitMonoCategory : (C : Type u₁) → [CategoryTheory.Category.{v₁, u₁} C] → Prop
-- Mathlib.Algebra.Order.CauSeq.Basic
CauSeq.instOne : {α : Type u_1} →
  {β : Type u_2} →
    [inst : Field α] →
      [inst_1 : LinearOrder α] →
        [inst_2 : IsStrictOrderedRing α] →
          [inst_3 : Ring β] → {abv : β → α} → [IsAbsoluteValue abv] → One (CauSeq β abv)
-- Mathlib.MeasureTheory.Measure.NullMeasurable
MeasureTheory.NullMeasurableSet.compl_toMeasurable_compl_ae_eq : ∀ {α : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasureTheory.NullMeasurableSet s μ → (MeasureTheory.toMeasurable μ sᶜ)ᶜ =ᵐ[μ] s
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get?_modify : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : β → β},
  Std.ExtDHashMap.Const.get? (Std.ExtDHashMap.Const.modify m k f) k' =
    if (k == k') = true then Option.map f (Std.ExtDHashMap.Const.get? m k) else Std.ExtDHashMap.Const.get? m k'
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.hasFiniteFPowerSeriesOnBall : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E →L[𝕜] F)
  (x : E), HasFiniteFPowerSeriesOnBall (⇑f) (f.fpowerSeries x) x 2 ⊤
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
Associates.factors_mk : ∀ {α : Type u_1} [inst : CommMonoidWithZero α] [inst_1 : UniqueFactorizationMonoid α] (a : α),
  a ≠ 0 → (Associates.mk a).factors = ↑(Associates.factors' a)
-- Mathlib.Topology.Sequences
IsSeqCompact.subseq_of_frequently_in : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X},
  IsSeqCompact s →
    ∀ {x : ℕ → X},
      (∃ᶠ (n : ℕ) in Filter.atTop, x n ∈ s) → ∃ a ∈ s, ∃ φ, StrictMono φ ∧ Filter.Tendsto (x ∘ φ) Filter.atTop (nhds a)
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.trNormal.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {Λ : Type u_3} {σ : Type u_4} (k : K) (a : σ → Option (Γ k) → σ)
  (q : Turing.TM2.Stmt Γ Λ σ),
  Turing.TM2to1.trNormal (Turing.TM2.Stmt.peek k a q) =
    Turing.TM1.Stmt.goto fun x x_1 => Turing.TM2to1.Λ'.go k (Turing.TM2to1.StAct.peek a) q