mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Compiler.LCNF.Basic
_private.Lean.Compiler.LCNF.Basic.0.Lean.Compiler.LCNF.attachCodeDecls.go.match_1.eq_3 : ∀ {pu : Lean.Compiler.LCNF.Purity} (motive : Lean.Compiler.LCNF.CodeDecl pu → Sort u_1)
  (decl : Lean.Compiler.LCNF.FunDecl pu)
  (h_1 : (decl : Lean.Compiler.LCNF.LetDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.let decl))
  (h_2 :
    (decl : Lean.Compiler.LCNF.FunDecl pu) →
      (h : pu = Lean.Compiler.LCNF.Purity.pure) → motive (Lean.Compiler.LCNF.CodeDecl.fun decl h))
  (h_3 : (decl : Lean.Compiler.LCNF.FunDecl pu) → motive (Lean.Compiler.LCNF.CodeDecl.jp decl))
  (h_4 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.Compiler.LCNF.Arg pu) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h))
  (h_5 :
    (fvarId : Lean.FVarId) →
      (idx : ℕ) →
        (y : Lean.FVarId) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h))
  (h_6 :
    (fvarId : Lean.FVarId) →
      (idx offset : ℕ) →
        (y : Lean.FVarId) →
          (ty : Lean.Expr) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h))
  (h_7 :
    (fvarId : Lean.FVarId) →
      (cidx : ℕ) →
        (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h))
  (h_8 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (h : pu = Lean.Compiler.LCNF.Purity.impure) →
            motive (Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h))
  (h_9 :
    (fvarId : Lean.FVarId) →
      (n : ℕ) →
        (check persistent : Bool) →
          (objs? : Option ℕ) →
            (h : pu = Lean.Compiler.LCNF.Purity.impure) →
              motive (Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h))
  (h_10 :
    (fvarId : Lean.FVarId) →
      (h : pu = Lean.Compiler.LCNF.Purity.impure) → motive (Lean.Compiler.LCNF.CodeDecl.del fvarId h)),
  (match Lean.Compiler.LCNF.CodeDecl.jp decl with
    | Lean.Compiler.LCNF.CodeDecl.let decl => h_1 decl
    | Lean.Compiler.LCNF.CodeDecl.fun decl h => h_2 decl h
    | Lean.Compiler.LCNF.CodeDecl.jp decl => h_3 decl
    | Lean.Compiler.LCNF.CodeDecl.oset fvarId idx y h => h_4 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.uset fvarId idx y h => h_5 fvarId idx y h
    | Lean.Compiler.LCNF.CodeDecl.sset fvarId idx offset y ty h => h_6 fvarId idx offset y ty h
    | Lean.Compiler.LCNF.CodeDecl.setTag fvarId cidx h => h_7 fvarId cidx h
    | Lean.Compiler.LCNF.CodeDecl.inc fvarId n check persistent h => h_8 fvarId n check persistent h
    | Lean.Compiler.LCNF.CodeDecl.dec fvarId n check persistent objs? h => h_9 fvarId n check persistent objs? h
    | Lean.Compiler.LCNF.CodeDecl.del fvarId h => h_10 fvarId h) =
    h_3 decl
-- Mathlib.CategoryTheory.Localization.LocalizerMorphism
CategoryTheory.LocalizerMorphism.IsInduced.inverseImage_eq : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C₁}
  {inst_1 : CategoryTheory.Category.{v₂, u₂} C₂} {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) [self : Φ.IsInduced],
  W₂.inverseImage Φ.functor = W₁
-- Mathlib.MeasureTheory.MeasurableSpace.Embedding
MeasurableEquiv.symm_apply_apply : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β] (e : α ≃ᵐ β) (x : α),
  e.symm (e x) = x
-- Mathlib.Topology.Sheaves.CommRingCat
/-- An upgraded version of the Yoneda embedding, observing that the continuous maps
from `X : TopCat` to `R : TopCommRingCat` form a commutative ring, functorial in both `X` and
`R`.  -/
TopCat.commRingYoneda : CategoryTheory.Functor TopCommRingCat (CategoryTheory.Functor TopCatᵒᵖ CommRingCat)
-- Mathlib.Data.Fintype.WithTopBot
instFiniteWithBot : ∀ {α : Type u_1} [Finite α], Finite (WithBot α)
-- Mathlib.Analysis.Normed.Operator.Mul
ContinuousLinearMap.flip_mul : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {R : Type u_3} [inst_1 : NonUnitalSeminormedCommRing R]
  [inst_2 : NormedSpace 𝕜 R] [inst_3 : IsScalarTower 𝕜 R R] [inst_4 : SMulCommClass 𝕜 R R],
  (ContinuousLinearMap.mul 𝕜 R).flip = ContinuousLinearMap.mul 𝕜 R
-- Mathlib.Algebra.Lie.Free
FreeLieAlgebra.liftAux_map_smul : ∀ (R : Type u) {X : Type v} [inst : CommRing R] {L : Type w} [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (f : X → L)
  (t : R) (a : FreeNonUnitalNonAssocAlgebra R X),
  (FreeLieAlgebra.liftAux R f) (t • a) = t • (FreeLieAlgebra.liftAux R f) a
-- Mathlib.CategoryTheory.Action.Basic
/-- The forgetful functor is intertwined by `functorCategoryEquivalence` with
evaluation at `PUnit.star`.  -/
Action.functorCategoryEquivalenceCompEvaluation : (V : Type u_1) →
  [inst : CategoryTheory.Category.{v_1, u_1} V] →
    (G : Type u_2) →
      [inst_1 : Monoid G] →
        (Action.functorCategoryEquivalence V G).functor.comp
            ((CategoryTheory.evaluation (CategoryTheory.SingleObj G) V).obj PUnit.unit) ≅
          Action.forget V G
-- Mathlib.FieldTheory.Galois.Basic
IsGalois.normalAutEquivQuotient_apply : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : FiniteDimensional K L] [inst_4 : IsGalois K L] (H : Subgroup Gal(L/K)) [inst_5 : H.Normal] (σ : Gal(L/K)),
  (IsGalois.normalAutEquivQuotient H) ↑σ = (AlgEquiv.restrictNormalHom ↥(IntermediateField.fixedField H)) σ
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a b : α}, (a == b) = true → Std.DHashMap.Const.get? m a = Std.DHashMap.Const.get? m b
-- Mathlib.CategoryTheory.Sites.Grothendieck
CategoryTheory.GrothendieckTopology.Cover.index_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X : C} {J : CategoryTheory.GrothendieckTopology C}
  {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D] (S : J.Cover X) (P : CategoryTheory.Functor Cᵒᵖ D)
  (I : S.shape.L), (S.index P).left I = P.obj (Opposite.op I.Y)
-- Mathlib.AlgebraicGeometry.Morphisms.Basic
AlgebraicGeometry.IsZariskiLocalAtSource.of_isOpenImmersion : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [AlgebraicGeometry.IsZariskiLocalAtSource P]
  {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [P.ContainsIdentities] [AlgebraicGeometry.IsOpenImmersion f], P f
-- Batteries.Data.Array.Scan
Array.scanlM.eq_1 : ∀ {m : Type u_1 → Type u_2} {β : Type u_1} {α : Type u_3} [inst : Monad m] (f : β → α → m β) (init : β) (as : Array α)
  (start stop : ℕ),
  Array.scanlM f init as start stop = Array.scanlM.loop f init as (min start as.size) (min stop as.size) ⋯ #[]
-- Mathlib.Order.CountableSupClosed
countableSupClosed_countableSupClosure : ∀ {α : Type u_2} {s : Set α} [inst : Preorder α], CountableSupClosed (countableSupClosure s)
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Basic
/-- In a `p ^ (k + 1)`-th cyclotomic extension of `ℚ `, we have that `ζ` is not congruent to an
integer modulo `p` if `p ≠ 2`.  -/
IsPrimitiveRoot.not_exists_int_prime_dvd_sub_of_prime_ne_two : ∀ {p k : ℕ} {K : Type u} [inst : Field K] {ζ : K} [hp : Fact (Nat.Prime p)] [inst_1 : CharZero K]
  [hcycl : IsCyclotomicExtension {p ^ (k + 1)} ℚ K] (hζ : IsPrimitiveRoot ζ (p ^ (k + 1))),
  p ≠ 2 → ¬∃ n, ↑p ∣ hζ.toInteger - ↑n
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Square
CategoryTheory.Square.IsPullback.unop : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {sq : CategoryTheory.Square Cᵒᵖ},
  sq.IsPullback → sq.unop.IsPushout
-- Mathlib.Algebra.Homology.ShortComplex.Limits
CategoryTheory.ShortComplex.hasFiniteLimits : ∀ {C : Type u_2} [inst : CategoryTheory.Category.{v_2, u_2} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [CategoryTheory.Limits.HasFiniteLimits C], CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.ShortComplex C)
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.IsReal.comp : ∀ {K : Type u_1} [inst : Field K] {k : Type u_2} [inst_1 : Field k] (f : k →+* K) {φ : K →+* ℂ},
  NumberField.ComplexEmbedding.IsReal φ → NumberField.ComplexEmbedding.IsReal (φ.comp f)
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_insertMany_emptyWithCapacity_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} [EquivBEq α] [LawfulHashable α] {l : List (α × β)}
  {k k' : α},
  (k == k') = true →
    ∀ {v : β} [inst_4 : Inhabited β],
      List.Pairwise (fun a b => (a.1 == b.1) = false) l →
        (k, v) ∈ l →
          Std.DHashMap.Internal.Raw₀.Const.get!
              (↑(Std.DHashMap.Internal.Raw₀.Const.insertMany Std.DHashMap.Internal.Raw₀.emptyWithCapacity l)) k' =
            v
-- 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 α] [inst_4 : Inhabited α],
  (↑m).WF →
    ∀ {l : List α} {k : α},
      m.contains k = true → (↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)).getKey! k = m.getKey! k
-- Init.Data.List.Nat.TakeDrop
/-- The `i + j`-th element of a list coincides with the `j`-th element of the list obtained by
dropping the first `i` elements. Version designed to rewrite from the big list to the small list.  -/
List.getElem_drop' : ∀ {α : Type u_1} {xs : List α} {i j : ℕ} (h : i + j < xs.length), xs[i + j] = (List.drop i xs)[j]
-- Mathlib.Algebra.Group.Pointwise.Set.Scalar
Set.vadd_set_range : ∀ {α : Type u_2} {β : Type u_3} [inst : VAdd α β] {ι : Sort u_5} (a : α) (f : ι → β),
  a +ᵥ Set.range f = Set.range fun i => a +ᵥ f i
-- Mathlib.Analysis.Analytic.Constructions
alternatingGeometricSeries_radius : ∀ (𝕜 : Type u_2) [inst : NontriviallyNormedField 𝕜] (A : Type u_7) [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
  [NormOneClass A], (alternatingGeometricSeries 𝕜 A).radius = 1
-- Lean.Meta.Sym.ReplaceS
_private.Lean.Meta.Sym.ReplaceS.0.Lean.Meta.Sym.visit : Lean.Expr →
  ℕ → (Lean.Expr → ℕ → Lean.Meta.Sym.Internal.AlphaShareBuilderM (Option Lean.Expr)) → Lean.Meta.Sym.M✝ Lean.Expr
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValue_of_mem : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] {l : List ((_ : α) × β)} {x : (_ : α) × β},
  x ∈ l →
    ∀ {h' : Std.Internal.List.containsKey x.fst l = true},
      Std.Internal.List.DistinctKeys l → Std.Internal.List.getValue x.fst l h' = x.snd
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalSubalgebra.toNonUnitalStarSubalgebra_toNonUnitalSubalgebra : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : NonUnitalSemiring A] [inst_2 : Module R A]
  [inst_3 : Star A] (s : NonUnitalSubalgebra R A) (h_star : ∀ x ∈ s, star x ∈ s),
  (s.toNonUnitalStarSubalgebra h_star).toNonUnitalSubalgebra = s
-- Mathlib.Data.Finset.Range
Finset.self_mem_range_succ : ∀ (n : ℕ), n ∈ Finset.range (n + 1)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
/-- An isomorphism `T ≅ T'` induces an equivalence
`CostructuredArrow S T ≌ CostructuredArrow S T'`.  -/
CategoryTheory.CostructuredArrow.mapIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {T T' : D} →
          {S : CategoryTheory.Functor C D} →
            (T ≅ T') → (CategoryTheory.CostructuredArrow S T ≌ CategoryTheory.CostructuredArrow S T')
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.contains_minKey? : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [Std.TransCmp cmp] {km : α},
  t.minKey? = some km → t.contains km = true
-- Mathlib.Analysis.Seminorm
Seminorm.instAddCommMonoid : {𝕜 : Type u_3} →
  {E : Type u_7} →
    [inst : SeminormedRing 𝕜] → [inst_1 : AddGroup E] → [inst_2 : SMul 𝕜 E] → AddCommMonoid (Seminorm 𝕜 E)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.atIdx_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {i : ℕ} {h' : i < t₁.size}
  (h : t₁.Equiv t₂), t₁.atIdx i h' = t₂.atIdx i ⋯
-- Mathlib.Algebra.Order.Group.PosPart
abs_sub_eq_two_nsmul_negPart : ∀ {α : Type u_1} [inst : Lattice α] [inst_1 : AddCommGroup α] [AddLeftMono α] (a : α), |a| - a = 2 • a⁻
-- Mathlib.Algebra.Homology.SpectralObject.Cycles
/-- The short complex expressing `Z^n(f, g)` as a cokernel of
the map `H^n(f) ⟶ H^n(f ≫ g)`.  -/
CategoryTheory.Abelian.SpectralObject.cokernelSequenceCycles : {C : Type u_1} →
  {ι : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} ι] →
        [inst_2 : CategoryTheory.Abelian C] →
          CategoryTheory.Abelian.SpectralObject C ι →
            {i j k : ι} →
              (f : i ⟶ j) →
                (g : j ⟶ k) →
                  (fg : i ⟶ k) → CategoryTheory.CategoryStruct.comp f g = fg → ℤ → CategoryTheory.ShortComplex C
-- Mathlib.MeasureTheory.Integral.Lebesgue.Basic
/-- The measurability assumption is necessary, otherwise there are counterexamples: for instance,
the conclusion fails if `s = univ` and `f` is the characteristic function of a Vitali set.  -/
MeasureTheory.setLIntegral_eq_zero_iff' : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {s : Set α},
  MeasurableSet s →
    ∀ {f : α → ENNReal}, AEMeasurable f (μ.restrict s) → (∫⁻ (a : α) in s, f a ∂μ = 0 ↔ ∀ᵐ (x : α) ∂μ, x ∈ s → f x = 0)
-- Mathlib.FieldTheory.Finite.Extension
FiniteField.finrank_extension : ∀ (k : Type u_1) [inst : Field k] [inst_1 : Finite k] (p : ℕ) [inst_2 : Fact (Nat.Prime p)] [inst_3 : CharP k p] (n : ℕ)
  [inst_4 : NeZero n], Module.finrank k (FiniteField.Extension k p n) = n
-- Mathlib.RingTheory.Localization.Module
LocalizedModule.restrictScalars_map_eq : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] {N : Type u_5} [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {M' : Type u_3} {N' : Type u_4}
  [inst_5 : AddCommMonoid M'] [inst_6 : AddCommMonoid N'] [inst_7 : Module R M'] [inst_8 : Module R N']
  (g₁ : M →ₗ[R] M') (g₂ : N →ₗ[R] N') [inst_9 : IsLocalizedModule S g₁] [inst_10 : IsLocalizedModule S g₂]
  (l : M →ₗ[R] N),
  ↑R ((LocalizedModule.map S) l) =
    ↑(IsLocalizedModule.iso S g₂).symm ∘ₗ (IsLocalizedModule.map S g₁ g₂) l ∘ₗ ↑(IsLocalizedModule.iso S g₁)
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
/-- (Implementation). The maps given in `appIso` is inverse to each other and gives a `ℱ(X) ≅ ℱ'(X)`.
 -/
CategoryTheory.Functor.IsCoverDense.Types.appIso : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {D : Type u_2} →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
        {K : CategoryTheory.GrothendieckTopology D} →
          {G : CategoryTheory.Functor C D} →
            [G.IsCoverDense K] →
              [G.IsLocallyFull K] →
                {ℱ ℱ' : CategoryTheory.Sheaf K (Type v)} →
                  (G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj) →
                    (X : D) → ℱ.obj.obj (Opposite.op X) ≅ ℱ'.obj.obj (Opposite.op X)
-- Mathlib.Data.Finset.Sym
Finset.sym_nonempty : ∀ {α : Type u_1} {s : Finset α} [inst : DecidableEq α] {n : ℕ}, (s.sym n).Nonempty ↔ n = 0 ∨ s.Nonempty
-- Init.Data.Int.DivMod.Lemmas
Int.neg_tmod : ∀ (a b : ℤ), (-a).tmod b = -a.tmod b
-- Init.Data.UInt.Lemmas
USize.sub_def : ∀ (a b : USize), a - b = { toBitVec := a.toBitVec - b.toBitVec }
-- Lean.Meta.HaveTelescope
/-- The set of `have`s that the body depends on, as indices into `haveInfo`.
Used in `computeFixedUsed` to compute used `have`s.  -/
Lean.Meta.HaveTelescopeInfo.bodyDeps : Lean.Meta.HaveTelescopeInfo → Std.HashSet ℕ
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.isoMk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {f g : CategoryTheory.MonoOver X}
  (h h_1 : f.obj.left ≅ g.obj.left) (e_h : h = h_1) (w : CategoryTheory.CategoryStruct.comp h.hom g.arrow = f.arrow),
  CategoryTheory.MonoOver.isoMk h w = CategoryTheory.MonoOver.isoMk h_1 ⋯
-- Mathlib.Data.Finset.Basic
Finset.insert_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {s : Finset α} {a : α}, a ∈ s → insert a (s.erase a) = s
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instModule : {S : Type u_2} →
  {R : Type u_3} →
    {A : Type u_4} →
      [inst : Semiring S] →
        [inst_1 : AddCommMonoid R] →
          [inst_2 : AddCommMonoid A] → [Module S R] → [Module S A] → Module S (Unitization R A)
-- Mathlib.CategoryTheory.Subfunctor.Image
CategoryTheory.Subfunctor.preimage_eq_top_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F F' : CategoryTheory.Functor C (Type w)}
  (G : CategoryTheory.Subfunctor F) (p : F' ⟶ F), G.preimage p = ⊤ ↔ CategoryTheory.Subfunctor.range p ≤ G
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orInR.inj : ∀ {p p_1 : Mathlib.Tactic.ITauto.Proof}, p.orInR = p_1.orInR → p = p_1
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.find?_toList_eq_none_iff_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α}, List.find? (fun x => cmp x.fst k == Ordering.eq) t.toList = none ↔ t.contains k = false
-- Mathlib.Algebra.Lie.TensorProduct
TensorProduct.LieModule.liftLie_apply : ∀ (R : Type u) [inst : CommRing R] (L : Type v) (M : Type w) (N : Type w₁) (P : Type w₂) [inst_1 : LieRing L]
  [inst_2 : LieAlgebra R L] [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M]
  [inst_6 : LieModule R L M] [inst_7 : AddCommGroup N] [inst_8 : Module R N] [inst_9 : LieRingModule L N]
  [inst_10 : LieModule R L N] [inst_11 : AddCommGroup P] [inst_12 : Module R P] [inst_13 : LieRingModule L P]
  [inst_14 : LieModule R L P] (f : M →ₗ⁅R,L⁆ N →ₗ[R] P) (m : M) (n : N),
  ((TensorProduct.LieModule.liftLie R L M N P) f) (m ⊗ₜ[R] n) = (f m) n
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexCohomology
CochainComplex.HomComplex.leftHomologyData_i_hom_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  (K L : CochainComplex C ℤ) (n : ℤ) (x : CochainComplex.HomComplex.Cocycle K L n),
  (AddCommGrpCat.Hom.hom (CochainComplex.HomComplex.leftHomologyData K L n).i) x = ↑x
-- Mathlib.Algebra.Group.Submonoid.Pointwise
AddSubmonoid.neg_bot : ∀ {G : Type u_2} [inst : AddGroup G], -⊥ = ⊥
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.fromIncl_comp_coproductIsoSelf_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) (i : X.I),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.FormalCoproduct.Hom.fromIncl i (CategoryTheory.CategoryStruct.id (X.obj i)))
      X.coproductIsoSelf.inv =
    CategoryTheory.Limits.Sigma.ι X.toFun i
-- Mathlib.CategoryTheory.EffectiveEpi.Basic
/-- ...and as such, unique.  -/
CategoryTheory.EffectiveEpiFamilyStruct.uniq : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B : C} {α : Type u_2} {X : α → C}
  {π : (a : α) → X a ⟶ B} (self : CategoryTheory.EffectiveEpiFamilyStruct X π) {W : C} (e : (a : α) → X a ⟶ W)
  (h :
    ∀ {Z : C} (a₁ a₂ : α) (g₁ : Z ⟶ X a₁) (g₂ : Z ⟶ X a₂),
      CategoryTheory.CategoryStruct.comp g₁ (π a₁) = CategoryTheory.CategoryStruct.comp g₂ (π a₂) →
        CategoryTheory.CategoryStruct.comp g₁ (e a₁) = CategoryTheory.CategoryStruct.comp g₂ (e a₂))
  (m : B ⟶ W), (∀ (a : α), CategoryTheory.CategoryStruct.comp (π a) m = e a) → m = self.desc e ⋯
-- Mathlib.Geometry.Manifold.ChartedSpace
ChartedSpace.secondCountable_of_sigmaCompact : ∀ (H : Type u) (M : Type u_2) [inst : TopologicalSpace H] [inst_1 : TopologicalSpace M] [ChartedSpace H M]
  [SecondCountableTopology H] [SigmaCompactSpace M], SecondCountableTopology M
-- Mathlib.Data.WSeq.Basic
/-- Recursion principle for weak sequences, compare with `List.recOn`.  -/
Stream'.WSeq.recOn : {α : Type u} →
  {motive : Stream'.WSeq α → Sort v} →
    (s : Stream'.WSeq α) →
      motive Stream'.WSeq.nil →
        ((x : α) → (s : Stream'.WSeq α) → motive (Stream'.WSeq.cons x s)) →
          ((s : Stream'.WSeq α) → motive s.think) → motive s
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.hurwitzOddFEPair_f : ∀ (a : UnitAddCircle) (a_1 : ℝ), (HurwitzZeta.hurwitzOddFEPair a).f a_1 = (Complex.ofReal ∘ HurwitzZeta.oddKernel a) a_1
-- Mathlib.Data.Finset.Basic
List.toFinset_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (l l' : List α), (l ∩ l').toFinset = l.toFinset ∩ l'.toFinset
-- Mathlib.CategoryTheory.Triangulated.Opposite.Functor
CategoryTheory.Functor.mapTriangleOpCompTriangleOpEquivalenceFunctorApp_hom_hom₂ : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.HasShift C ℤ]
  [inst_3 : CategoryTheory.HasShift D ℤ] (F : CategoryTheory.Functor C D) [inst_4 : F.CommShift ℤ]
  (T : CategoryTheory.Pretriangulated.Triangle C),
  (F.mapTriangleOpCompTriangleOpEquivalenceFunctorApp T).hom.hom₂ =
    CategoryTheory.CategoryStruct.id (Opposite.op (F.obj T.obj₂))
-- Mathlib.Tactic.Simproc.FinsetInterval
_private.Mathlib.Tactic.Simproc.FinsetInterval.0.Mathlib.Tactic.Simp.Int.Iio_zero : Finset.Iio 0 = ∅
-- Init.SimpLemmas
and_congr_left : ∀ {c a b : Prop}, (c → (a ↔ b)) → (a ∧ c ↔ b ∧ c)
-- Mathlib.AlgebraicTopology.ModelCategory.BifibrantObjectHomotopy
HomotopicalAlgebra.BifibrantObject.toHoCat_map_eq_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : HomotopicalAlgebra.ModelCategory C]
  {X Y : HomotopicalAlgebra.BifibrantObject C} (f g : X ⟶ Y),
  HomotopicalAlgebra.BifibrantObject.toHoCat.map f = HomotopicalAlgebra.BifibrantObject.toHoCat.map g ↔
    HomotopicalAlgebra.BifibrantObject.homRel C f g
-- Mathlib.Testing.Plausible.Functions
/-- Shrink an injective function slicing a segment in the middle of the domain and removing
the corresponding elements in the codomain, hence maintaining the property that
one is a permutation of the other.
 -/
Plausible.InjectiveFunction.shrink : {α : Type} → [DecidableEq α] → Plausible.InjectiveFunction α → List (Plausible.InjectiveFunction α)
-- Init.Data.SInt.Lemmas
Int8.ofBitVec_le_iff_sle : ∀ (a b : BitVec 8), Int8.ofBitVec a ≤ Int8.ofBitVec b ↔ a.sle b = true
-- Mathlib.LinearAlgebra.Dimension.FreeAndStrongRankCondition
Submodule.finrank_le_one_iff_isPrincipal : ∀ {K : Type u} {V : Type v} [inst : Ring K] [StrongRankCondition K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  (W : Submodule K V) [Module.Free K ↥W] [Module.Finite K ↥W], Module.finrank K ↥W ≤ 1 ↔ W.IsPrincipal
-- Lean.DocString.Extension
/-- Finds a docstring without performing any alias resolution or enrichment with extra metadata.
For Markdown docstrings, the result is a string; for Verso docstrings, it's a `VersoDocString`.

Docstrings to be shown to a user should be looked up with `Lean.findDocString?` instead.
 -/
Lean.findInternalDocString? : Lean.Environment → Lean.Name → optParam Bool true → IO (Option (String ⊕ Lean.VersoDocString))
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.get!_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a b : α},
  (a == b) = true → Std.ExtDHashMap.Const.get! m a = Std.ExtDHashMap.Const.get! m b
-- Mathlib.LinearAlgebra.Eigenspace.Semisimple
Module.End.IsSemisimple.iSup_eigenspace_eq_top : ∀ {K : Type u_3} {V : Type u_4} [inst : Field K] [IsAlgClosed K] [inst_2 : AddCommGroup V] [inst_3 : Module K V]
  [FiniteDimensional K V] {f : Module.End K V}, f.IsSemisimple → ⨆ μ, f.eigenspace μ = ⊤
-- Std.Data.Internal.List.Associative
Std.Internal.List.getValueCastD_filter_not_contains_map_fst_of_containsKey_eq_false_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] {l₁ l₂ : List ((a : α) × β a)} {k : α}
  {fallback : β k},
  Std.Internal.List.DistinctKeys l₁ →
    Std.Internal.List.containsKey k l₂ = false →
      Std.Internal.List.getValueCastD k (List.filter (fun p => !(List.map Sigma.fst l₂).contains p.fst) l₁) fallback =
        Std.Internal.List.getValueCastD k l₁ fallback