mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Order.Interval.Set.OrdConnectedComponent
Set.disjoint_ordT5Nhd : ∀ {α : Type u_1} [inst : LinearOrder α] {s t : Set α}, Disjoint (s.ordT5Nhd t) (t.ordT5Nhd s)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Loop
Std.IterM.length_eq_fold : ∀ {α β : Type w} {m : Type w → Type w'} [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α m m] {it : Std.IterM m β},
  it.length = Std.IterM.fold (fun acc x => { down := acc.down + 1 }) { down := 0 } it
-- Mathlib.Data.Setoid.Basic
Quotient.subsingleton_iff : ∀ {α : Type u_1} {s : Setoid α}, Subsingleton (Quotient s) ↔ s = ⊤
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurable_to_prop : ∀ {α : Type u_1} {mα : MeasurableSpace α} {f : α → Prop}, MeasurableSet (f ⁻¹' {True}) → Measurable f
-- Mathlib.Tactic.CategoryTheory.Coherence.Normalize
/-- Evaluate `f ◁ (α ≫ η ≫ ηs)`.  -/
Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft.mkEvalWhiskerLeftOfCons : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MkEvalWhiskerLeft m] →
    Mathlib.Tactic.BicategoryLike.Atom₁ →
      Mathlib.Tactic.BicategoryLike.Structural →
        Mathlib.Tactic.BicategoryLike.WhiskerLeft →
          Mathlib.Tactic.BicategoryLike.NormalExpr → Mathlib.Tactic.BicategoryLike.NormalExpr → Lean.Expr → m Lean.Expr
-- Mathlib.Topology.Germ
eq_of_germ_isConstant_on : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] {f : X → Y} {x : X} {s : Set X},
  (∀ x ∈ s, (↑f).IsConstant) → IsPreconnected s → ∀ {x' : X}, x ∈ s → x' ∈ s → f x = f x'
-- Mathlib.Order.Filter.AtTopBot.Interval
Finset.tendsto_Icc_atBot_prod_atTop : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrder α],
  Filter.Tendsto (fun p => Finset.Icc p.1 p.2) (Filter.atBot ×ˢ Filter.atTop) Filter.atTop
-- Mathlib.Algebra.Homology.HomologicalComplex
/-- If `c.Rel i j`, then `C.xPrev j` is isomorphic to `C.X i`.  -/
HomologicalComplex.xPrevIso : {ι : Type u_1} →
  {V : Type u} →
    [inst : CategoryTheory.Category.{v, u} V] →
      [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] →
        {c : ComplexShape ι} → (C : HomologicalComplex V c) → {i j : ι} → c.Rel i j → (C.xPrev j ≅ C.X i)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.self_le_maxKey?_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  (h : t.WF) {k : α} {v : β k} {kmi : α}, (t.insertIfNew k v).maxKey?.get ⋯ = kmi → (cmp k kmi).isLE = true
-- Mathlib.LinearAlgebra.ExteriorPower.Basic
exteriorPower.presentation.Rels.add.inj : ∀ {R : Type u} {ι : Type u_4} {M : Type u_5} {m : ι → M} {i : ι} {x y : M} {m_1 : ι → M} {i_1 : ι} {x_1 y_1 : M},
  exteriorPower.presentation.Rels.add m i x y = exteriorPower.presentation.Rels.add m_1 i_1 x_1 y_1 →
    m = m_1 ∧ i = i_1 ∧ x = x_1 ∧ y = y_1
-- Mathlib.Data.Int.Bitwise
Int.xor.eq_2 : ∀ (m n : ℕ), (Int.ofNat m).xor (Int.negSucc n) = Int.negSucc (m ^^^ n)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mathlib.Tactic.MonTauto.rightUnitor_neg_tensor_zero_add_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M X₁ : C}
  [inst_2 : CategoryTheory.AddMonObj M] (f : X₁ ⟶ M) {Z : C} (h : M ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor X₁).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.tensorHom f CategoryTheory.AddMonObj.zero)
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add h)) =
    CategoryTheory.CategoryStruct.comp f h
-- Init.Omega.Int
Lean.Omega.Int.le_add_iff_sub_le : ∀ {a b c : ℤ}, a ≤ b + c ↔ a - c ≤ b
-- Mathlib.Algebra.Star.NonUnitalSubalgebra
NonUnitalStarSubalgebra.toNonUnitalCommSemiring : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : NonUnitalCommSemiring A] →
        [inst_2 : Module R A] → [inst_3 : Star A] → (S : NonUnitalStarSubalgebra R A) → NonUnitalCommSemiring ↥S
-- Lean.Meta.Tactic.Cases
/-- Auxiliary structure for storing `byCases` tactic result.  -/
Lean.Meta.ByCasesSubgoal : Type
-- Mathlib.Topology.Sion
Sion.exists_lt_iInf_of_lt_iInf_of_finite : ∀ {E : Type u_1} {F : Type u_2} {β : Type u_3} [inst : LinearOrder β] {X : Set E} {Y : Set F} {f : E → F → β}
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup E] [inst_3 : Module ℝ E] [IsTopologicalAddGroup E]
  [ContinuousSMul ℝ E],
  X.Nonempty →
    IsCompact X →
      (∀ y ∈ Y, LowerSemicontinuousOn (fun x => f x y) X) →
        (∀ y ∈ Y, QuasiconvexOn ℝ X fun x => f x y) →
          ∀ [inst_6 : TopologicalSpace F] [inst_7 : AddCommGroup F] [inst_8 : Module ℝ F],
            Convex ℝ Y →
              (∀ x ∈ X, UpperSemicontinuousOn (fun y => f x y) Y) →
                (∀ x ∈ X, QuasiconcaveOn ℝ Y fun y => f x y) →
                  ∀ [DenselyOrdered β] [IsTopologicalAddGroup F] [ContinuousSMul ℝ F],
                    Convex ℝ X →
                      ∀ {s : Set F},
                        s.Finite → s ⊆ Y → ∀ {t : β}, (∀ x ∈ X, ∃ y ∈ s, t < f x y) → ∃ y0 ∈ Y, ∀ x ∈ X, t < f x y0
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.Decomposition.right_inv : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} {inst : DecidableEq ι} {inst_1 : AddCommMonoid M} {inst_2 : SetLike σ M}
  {inst_3 : AddSubmonoidClass σ M} {ℳ : ι → σ} [self : DirectSum.Decomposition ℳ],
  Function.RightInverse (⇑(DirectSum.coeAddMonoidHom ℳ)) DirectSum.Decomposition.decompose'
-- Mathlib.Combinatorics.SimpleGraph.LineGraph
SimpleGraph.Copy.toLineGraphEmbedding.eq_1 : ∀ {V : Type u_1} {V' : Type u_2} {G : SimpleGraph V} {G' : SimpleGraph V'} (f : G.Copy G'),
  f.toLineGraphEmbedding = { toFun := fun e => ⟨Sym2.map ⇑f ↑e, ⋯⟩, inj' := ⋯, map_rel_iff' := ⋯ }
-- Init.Data.Int.LemmasAux
Int.max_min_distrib_left : ∀ (a b c : ℤ), max a (min b c) = min (max a b) (max a c)
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.smul_C : ∀ {R : Type u_1} {a b : R} [inst : CommSemiring R] (r1 r2 : R),
  r1 • QuadraticAlgebra.C r2 = QuadraticAlgebra.C (r1 * r2)
-- Mathlib.FieldTheory.Fixed
FixedPoints.minpoly.of_eval₂ : ∀ (G : Type u) [inst : Group G] (F : Type v) [inst_1 : Field F] [inst_2 : MulSemiringAction G F] [inst_3 : Fintype G]
  (x : F) (f : Polynomial ↥(FixedPoints.subfield G F)),
  Polynomial.eval₂ (FixedPoints.subfield G F).subtype x f = 0 → FixedPoints.minpoly G F x ∣ f
-- Mathlib.CategoryTheory.ObjectProperty.ContainsZero
CategoryTheory.ObjectProperty.instHasZeroObjectFullSubcategoryOfContainsZero : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C) [P.ContainsZero],
  CategoryTheory.Limits.HasZeroObject P.FullSubcategory
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
IntermediateField.AdjoinSimple.gen.eq_1 : ∀ (F : Type u_1) [inst : Field F] {E : Type u_2} [inst_1 : Field E] [inst_2 : Algebra F E] (α : E),
  IntermediateField.AdjoinSimple.gen F α = ⟨α, ⋯⟩
-- Mathlib.Algebra.Group.Subsemigroup.MulOpposite
/-- A subsemigroup `H` of `M` determines a subsemigroup `H.op` of the opposite semigroup `Mᵐᵒᵖ`.  -/
Subsemigroup.opEquiv : {M : Type u_2} → [inst : Mul M] → Subsemigroup M ≃o Subsemigroup Mᵐᵒᵖ
-- Mathlib.Geometry.Manifold.PartitionOfUnity
SmoothBumpCovering.mk : {ι : Type uι} →
  {E : Type uE} →
    [inst : NormedAddCommGroup E] →
      [inst_1 : NormedSpace ℝ E] →
        {H : Type uH} →
          [inst_2 : TopologicalSpace H] →
            {I : ModelWithCorners ℝ E H} →
              {M : Type uM} →
                [inst_3 : TopologicalSpace M] →
                  [inst_4 : ChartedSpace H M] →
                    [inst_5 : FiniteDimensional ℝ E] →
                      {s : optParam (Set M) Set.univ} →
                        (c : ι → M) →
                          (toFun : (i : ι) → SmoothBumpFunction I (c i)) →
                            (∀ (i : ι), c i ∈ s) →
                              (LocallyFinite fun i => Function.support ↑(toFun i)) →
                                (∀ x ∈ s, ∃ i, ↑(toFun i) =ᶠ[nhds x] 1) → SmoothBumpCovering ι I M s
-- Mathlib.Logic.Embedding.Basic
/-- Fixing an element `b : β` gives an embedding `α ↪ α × β`.  -/
Function.Embedding.sectL : (α : Type u_1) → {β : Type u_2} → β → α ↪ α × β
-- Batteries.Data.MLList.Basic
/-- Compute, inside the monad, whether a `MLList` is empty.  -/
MLList.isEmpty : {m : Type u_1 → Type u_1} → {α : Type u_1} → [Monad m] → MLList m α → m (ULift.{u_1, 0} Bool)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.dExt_iff : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] {f g : E →ₛₗ.[σ] F},
  f = g ↔ ∃ (_ : f.domain = g.domain), ∀ ⦃x : ↥f.domain⦄ ⦃y : ↥g.domain⦄, ↑x = ↑y → ↑f x = ↑g y
-- Std.Data.TreeSet.Basic
Std.TreeSet.instUnion : {α : Type u} → {cmp : α → α → Ordering} → Union (Std.TreeSet α cmp)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
Std.Tactic.BVDecide.BVExpr.bitblast.go_denote_eq : ∀ {w : ℕ} (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (expr : Std.Tactic.BVDecide.BVExpr w)
  (assign : Std.Tactic.BVDecide.BVExpr.Assignment) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig),
  Std.Tactic.BVDecide.BVExpr.Cache.Inv assign aig cache →
    ∀ (idx : ℕ) (hidx : idx < w),
      ⟦assign.toAIGAssignment,
          { aig := (↑(Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr cache).result).aig,
            ref := (↑(Std.Tactic.BVDecide.BVExpr.bitblast.go aig expr cache).result).vec.get idx hidx }⟧ =
        (Std.Tactic.BVDecide.BVExpr.eval assign expr).getLsbD idx
-- Mathlib.Computability.StateTransition
StateTransition.Reaches₀.refl : ∀ {σ : Type u_1} {f : σ → Option σ} (a : σ), StateTransition.Reaches₀ f a a
-- Mathlib.CategoryTheory.Idempotents.Karoubi
/-- The formal direct factor of `P.X` given by the idempotent `P.p` in the category `C`
is actually a direct factor in the category `Karoubi C`.  -/
CategoryTheory.Idempotents.Karoubi.decompId_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Idempotents.Karoubi C)
  {Z : CategoryTheory.Idempotents.Karoubi C} (h : P ⟶ Z),
  h = CategoryTheory.CategoryStruct.comp P.decompId_i (CategoryTheory.CategoryStruct.comp P.decompId_p h)
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- The content of the matrix.  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.DenseMatrix.data : {n m : ℕ} → Mathlib.Tactic.Linarith.SimplexAlgorithm.DenseMatrix n m → Array (Array ℚ)
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.one_apply : ∀ {R : Type u_1} {G : Type u_2} {V : Type u_3} [inst : Monoid G] [inst_1 : Ring R] [inst_2 : AddCommGroup V]
  [inst_3 : TopologicalSpace V] [inst_4 : IsTopologicalAddGroup V] [inst_5 : Module R V] {π₁ : ContRepresentation R G V}
  (v : V), 1 v = v
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.lift_swap : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P) (x : Monoid.Coprod N M),
  (Monoid.Coprod.lift f g) ((Monoid.Coprod.swap N M) x) = (Monoid.Coprod.lift g f) x
-- Mathlib.Analysis.Normed.Operator.NormedSpace
LinearIsometry.inl_apply : ∀ (𝕜 : Type u_9) [inst : NontriviallyNormedField 𝕜] (E : Type u_10) (F : Type u_11) [inst_1 : SeminormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (x : E),
  (LinearIsometry.inl 𝕜 E F) x = (x, 0)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getD_filterMap_of_getKey?_eq_some : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ} {k k' : α} {fallback : γ},
  m.WF →
    m.getKey? k = some k' → (Std.HashMap.Raw.filterMap f m).getD k fallback = (m[k]?.bind fun x => f k' x).getD fallback
-- Mathlib.Algebra.GCDMonoid.Basic
normalize_dvd_iff : ∀ {α : Type u_1} [inst : MonoidWithZero α] [inst_1 : NormalizationMonoid α] {a b : α}, normalize a ∣ b ↔ a ∣ b
-- Mathlib.ModelTheory.Syntax
_private.Mathlib.ModelTheory.Syntax.0.FirstOrder.Language.Term.constantsToVars.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_4} {γ : Type u_2} (motive : (L.withConstants γ).Term α → Sort u_5) (a : α)
  (h_1 : (a : α) → motive (FirstOrder.Language.var a))
  (h_2 :
    (f : (L.withConstants γ).Functions 0) →
      (ts : Fin 0 → (L.withConstants γ).Term α) → motive (FirstOrder.Language.func f ts))
  (h_3 :
    (_n : ℕ) →
      (f : (L.withConstants γ).Functions (_n + 1)) →
        (ts : Fin (_n + 1) → (L.withConstants γ).Term α) → motive (FirstOrder.Language.func f ts)),
  (match FirstOrder.Language.var a with
    | FirstOrder.Language.var a => h_1 a
    | FirstOrder.Language.func f ts => h_2 f ts
    | FirstOrder.Language.func f ts => h_3 _n f ts) =
    h_1 a
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddCancelCommMonoid.eq_1 : ∀ {α : Type u_1} [inst : AddCancelCommMonoid α],
  AddOpposite.instAddCancelCommMonoid = { toAddCommMonoid := AddOpposite.instAddCommMonoid, toIsLeftCancelAdd := ⋯ }
-- Lean.Meta.Tactic.Grind.Main
/-- Returns the extensions used by the `lia` tactic.

`lia` keeps the structural part of the default `grind` attribute (cases types, `funCC`,
and extensionality theorems), but instead of the full `@[grind]` E-matching lemma set it
only uses the dedicated `@[lia]` lemma set. This lets `cutsat` benefit from a small amount
of instantiation (e.g. `Nat.max_def`) without pulling in everything tagged `@[grind]`.
 -/
Lean.Meta.Grind.getLiaExtensions : Lean.MetaM Lean.Meta.Grind.ExtensionStateArray
-- Mathlib.Combinatorics.SimpleGraph.Metric
/-- The open ball of radius `r` centered at the vertex `c` in the graph extended metric.  -/
SimpleGraph.ball : {V : Type u_1} → SimpleGraph V → V → ℕ∞ → Set V
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.size_erase_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  (t.erase k).size ≤ t.size
-- Mathlib.AlgebraicGeometry.Morphisms.Finite
AlgebraicGeometry.IsFinite.of_comp : ∀ {X Y Z : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (g : Y ⟶ Z)
  [AlgebraicGeometry.IsFinite (CategoryTheory.CategoryStruct.comp f g)] [AlgebraicGeometry.IsSeparated g],
  AlgebraicGeometry.IsFinite f
-- Lean.Meta.PProdN
/-- `PProd.snd` or `And.right` (using `.proj`), inferring the type of `e`  -/
Lean.Meta.mkPProdSndM : Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.basicOpen_mul : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (f g : A),
  ProjectiveSpectrum.basicOpen 𝒜 (f * g) = ProjectiveSpectrum.basicOpen 𝒜 f ⊓ ProjectiveSpectrum.basicOpen 𝒜 g
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey?_eq_some_getKey : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α] {a : α}
  (h : a ∈ m), m.getKey? a = some (m.getKey a h)
-- Mathlib.Tactic.Abel
/-- Add the letter "g" to the end of the name, e.g. turning `term` into `termg`.

This is used to choose between declarations taking `AddCommMonoid` and those
taking `AddCommGroup` instances.
 -/
Mathlib.Tactic.Abel.addG : Lean.Name → Lean.Name
-- Mathlib.Data.Finset.Sort
Finset.map_orderEmbOfFin_univ : ∀ {α : Type u_1} [inst : LinearOrder α] (s : Finset α) {k : ℕ} (h : s.card = k),
  Finset.map (s.orderEmbOfFin h).toEmbedding Finset.univ = s
-- Mathlib.CategoryTheory.Limits.Elements
/-- (implementation) The constructed limit cone is a lift of the limit cone in `C`.  -/
CategoryTheory.CategoryOfElements.CreatesLimitsAux.isValidLift : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor C (Type w)} →
      {I : Type u₁} →
        [inst_1 : CategoryTheory.Category.{v₁, u₁} I] →
          [inst_2 : Small.{w, u₁} I] →
            (F : CategoryTheory.Functor I A.Elements) →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I C] →
                [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape I A] →
                  (CategoryTheory.CategoryOfElements.π A).mapCone
                      (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F) ≅
                    CategoryTheory.Limits.limit.cone (F.comp (CategoryTheory.CategoryOfElements.π A))
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.aroots_smul_nonzero : ∀ {S : Type v} {T : Type w} [inst : CommRing T] [IsDomain T] [inst_2 : CommRing S] [inst_3 : IsDomain S]
  [inst_4 : Algebra T S] [Module.IsTorsionFree T S] {a : T} (p : Polynomial T), a ≠ 0 → (a • p).aroots S = p.aroots S
-- Mathlib.Topology.Sheaves.Stalks
TopCat.Presheaf.germ.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C] {X : TopCat}
  (F : TopCat.Presheaf C X) (U : TopologicalSpace.Opens ↑X) (x : ↑X) (hx : x ∈ U), F.germ U x hx = F.germ U x hx
-- Mathlib.Data.WSeq.Basic
Stream'.WSeq.destruct_flatten : ∀ {α : Type u} (c : Computation (Stream'.WSeq α)), (Stream'.WSeq.flatten c).destruct = c >>= Stream'.WSeq.destruct
-- Init.Data.String.PosRaw
String.getUtf8Byte : (s : String) → (p : String.Pos.Raw) → p < s.rawEndPos → UInt8
-- Mathlib.NumberTheory.LSeries.Nonvanishing
_private.Mathlib.NumberTheory.LSeries.Nonvanishing.0.DirichletCharacter.BadChar.χ_sq : ∀ {N : ℕ} [inst : NeZero N] (self : DirichletCharacter.BadChar✝ N), DirichletCharacter.BadChar.χ✝ self ^ 2 = 1
-- Mathlib.Logic.Equiv.Sum
Equiv.sigmaFiberEquiv_symm_apply_fst : ∀ {α : Type u_9} {β : Type u_10} (f : α → β) (x : α), ((Equiv.sigmaFiberEquiv f).symm x).fst = f x
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the key-value pair with the largest key that is less than or equal to the
given key, returning `fallback` if no such pair exists.
 -/
Std.ExtDTreeMap.Const.getEntryLED : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α → α × β → α × β
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- `NonUnitalSubsemiringClass S R` states that `S` is a type of subsets `s ⊆ R` that
are both an additive submonoid and also a multiplicative subsemigroup.  -/
NonUnitalSubsemiringClass : (S : Type u_1) → (R : outParam (Type u)) → [NonUnitalNonAssocSemiring R] → [SetLike S R] → Prop
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
CategoryTheory.Subobject.Classifier.isTerminalFrom_eq_χ₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (c : CategoryTheory.Subobject.Classifier C),
  CategoryTheory.Subobject.Classifier.isTerminalΩ₀.from = c.χ₀
-- Mathlib.Data.Erased
/-- `Erased α` is the same as `α`, except that the elements
of `Erased α` are erased in the VM in the same way as types
and proofs. This can be used to track data without storing it
literally.  -/
Erased : Sort u → Sort (max 1 u)
-- Mathlib.CategoryTheory.Triangulated.Opposite.Subcategory
CategoryTheory.ObjectProperty.instIsTriangulatedOppositeOp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) [P.IsTriangulated], P.op.IsTriangulated
-- Mathlib.Analysis.Meromorphic.Divisor
/-- The divisor of the function `z ↦ z - z₀` at `x` is `0` if `x ≠ z₀`.  -/
MeromorphicOn.divisor_sub_const_of_ne : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {U : Set 𝕜} {z₀ x : 𝕜},
  x ≠ z₀ → (MeromorphicOn.divisor (fun x => x - z₀) U) x = 0
-- Mathlib.Data.Countable.Defs
Bool.countable : Countable Bool
-- Mathlib.Data.EReal.Operations
EReal.bot_mul_coe_of_neg : ∀ {x : ℝ}, x < 0 → ⊥ * ↑x = ⊤
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.size_filter!_eq_size_iff : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α] {f : (a : α) → β a → Bool},
  t.WF →
    ((Std.DTreeMap.Internal.Impl.filter! f t).size = t.size ↔
      ∀ (a : α) (h : Std.DTreeMap.Internal.Impl.contains a t = true), f a (t.get a h) = true)
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.uproj.sizeOf_spec : ∀ (i : ℕ) (x : Lean.IR.VarId), sizeOf (Lean.IR.Expr.uproj i x) = 1 + sizeOf i + sizeOf x
-- Mathlib.Analysis.Complex.Exponential
_private.Mathlib.Analysis.Complex.Exponential.0.Nat.factorial.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Combinatorics.Hall.Basic
/-- When the Hall condition is satisfied, the set of matchings on a finite set is nonempty.
This is where `Finset.all_card_le_biUnion_card_iff_existsInjective'` comes into the argument.  -/
hallMatchingsOn.nonempty : ∀ {ι : Type u} {α : Type v} [inst : DecidableEq α] (t : ι → Finset α),
  (∀ (s : Finset ι), s.card ≤ (s.biUnion t).card) → ∀ (ι' : Finset ι), Nonempty ↑(hallMatchingsOn t ι')
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaAddMon.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C],
  CategoryTheory.yonedaAddMon =
    { obj := fun M => CategoryTheory.yonedaAddMonObj M.X,
      map := fun {X Y} ψ =>
        { app := fun x => AddMonCat.ofHom (CategoryTheory.IsAddMonHom.addMonoidHom ψ.hom (Opposite.unop x)),
          naturality := ⋯ },
      map_id := ⋯, map_comp := ⋯ }
-- Mathlib.Analysis.MellinInversion
_private.Mathlib.Analysis.MellinInversion.0.rexp_neg_image_aux : Real.exp ∘ Neg.neg '' Set.univ = Set.Ioi 0
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.selfLeftAction_actionUnitIso : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C] (x : C),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionUnitIso x =
    CategoryTheory.MonoidalCategoryStruct.leftUnitor x
-- Mathlib.RingTheory.Ideal.Operations
Ideal.span_singleton_mul_right_mono : ∀ {R : Type u} [inst : CommSemiring R] {I J : Ideal R} [IsDomain R] {x : R},
  x ≠ 0 → (Ideal.span {x} * I ≤ Ideal.span {x} * J ↔ I ≤ J)
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
/-- The third index  -/
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.i₃ : {ι : Type u_2} →
  {κ : Type u_3} →
    [inst : Preorder ι] →
      {c : ℤ → ComplexShape κ} →
        {r₀ : ℤ} →
          CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀ →
            (r : ℤ) → κ → autoParam (r₀ ≤ r) CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore._auto_3 → ι
-- Std.Tactic.BVDecide.LRAT.Internal.Clause
Std.Tactic.BVDecide.LRAT.Internal.Clause.delete : {α : outParam (Type u)} →
  {β : Type v} → [self : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] → β → Std.Sat.Literal α → β
-- Mathlib.Analysis.Normed.Affine.ContinuousAffineMap
ContinuousAffineMap.fst_decompLinearIsometryEquiv : ∀ (𝕜 : Type u_1) (R : Type u_2) (V : Type u_3) (W : Type u_4) [inst : SeminormedAddCommGroup V]
  [inst_1 : SeminormedAddCommGroup W] [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 V]
  [inst_4 : NormedSpace 𝕜 W] [inst_5 : Ring R] [inst_6 : Module R W] [inst_7 : ContinuousConstSMul R W]
  [inst_8 : SMulCommClass 𝕜 R W] (f : V →ᴬ[𝕜] W), ((ContinuousAffineMap.decompLinearIsometryEquiv 𝕜 R V W) f).1 = f 0
-- Mathlib.Analysis.SpecialFunctions.Arcosh
Real.arcosh_zero : Real.arcosh 1 = 0
-- Lean.Expr
Lean.Expr.looseBVarRangeEx : Lean.Expr → UInt32
-- Mathlib.Analysis.Distribution.Sobolev
TemperedDistribution.besselPotential_neg_one_lineDerivOp_eq : ∀ {E : Type u_1} {F : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedAddCommGroup F]
  [inst_2 : InnerProductSpace ℝ E] [inst_3 : FiniteDimensional ℝ E] [inst_4 : MeasurableSpace E] [inst_5 : BorelSpace E]
  [inst_6 : NormedSpace ℂ F] {m : E} (f : TemperedDistribution E F),
  (TemperedDistribution.besselPotential E F (-1)) (LineDeriv.lineDerivOp m f) =
    (2 * ↑Real.pi * Complex.I) •
      (TemperedDistribution.fourierMultiplierCLM F fun x => ↑(inner ℝ x m * (1 + ‖x‖ ^ 2) ^ (-1 / 2))) f