mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.EMetricSpace.Basic
EMetric.isUniformInducing_iff : ∀ {α : Type u} {β : Type v} [inst : PseudoEMetricSpace α] [inst_1 : PseudoEMetricSpace β] {f : α → β},
  IsUniformInducing f ↔ UniformContinuous f ∧ ∀ δ > 0, ∃ ε > 0, ∀ {a b : α}, edist (f a) (f b) < ε → edist a b < δ
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddGroup.eq_1 : ∀ {α : Type u_1} [inst : AddGroup α],
  AddOpposite.instAddGroup = { toSubNegMonoid := AddOpposite.instSubNegMonoid, neg_add_cancel := ⋯ }
-- Batteries.Data.String.Lemmas
String.extract_cons_addChar : ∀ (c : Char) (cs : List Char) (b e : String.Pos.Raw),
  String.Pos.Raw.extract (String.ofList (c :: cs)) (b + c) (e + c) = String.Pos.Raw.extract (String.ofList cs) b e
-- Mathlib.Topology.NhdsSet
Filter.Eventually.self_of_nhdsSet : ∀ {X : Type u_2} [inst : TopologicalSpace X] {s : Set X} {p : X → Prop}, (∀ᶠ (x : X) in nhdsSet s, p x) → ∀ x ∈ s, p x
-- Mathlib.Analysis.CStarAlgebra.Module.Synonym
WithCStarModule.instModule : (A : Type u_3) →
  (E : Type u_4) →
    {R : Type u_5} → [inst : Semiring R] → [inst_1 : AddCommGroup E] → [Module R E] → Module R (WithCStarModule A E)
-- Mathlib.Topology.Order.Rolle
/-- If a function `f` is continuous on an unordered open interval
and tends to the same value at its endpoints,
then it has an extremum on this unordered open interval.  -/
exists_isExtrOn_uIoo_of_tendsto : ∀ {X : Type u_1} {Y : Type u_2} [inst : ConditionallyCompleteLinearOrder X] [DenselyOrdered X]
  [inst_2 : TopologicalSpace X] [OrderTopology X] [inst_4 : LinearOrder Y] [inst_5 : TopologicalSpace Y]
  [OrderTopology Y] {f : X → Y} {a b : X} {l : Y},
  a ≠ b →
    ContinuousOn f (Set.uIoo a b) →
      Filter.Tendsto f (nhdsWithin a (Set.uIoo a b)) (nhds l) →
        Filter.Tendsto f (nhdsWithin b (Set.uIoo a b)) (nhds l) → ∃ c ∈ Set.uIoo a b, IsExtrOn f (Set.uIoo a b) c
-- Init.Data.String.Slice
String.Slice.instLE : LE String.Slice
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.exists_notMem_of_length_lt : ∀ {α : Type u_1} (l : List α), ↑l.length < Cardinal.mk α → ∃ z, z ∉ l
-- Mathlib.Algebra.Module.Submodule.Equiv
/-- The restriction of a bilinear map to a submodule in which it takes values.  -/
LinearMap.codRestrict₂ : {R : Type u_1} →
  {M : Type u_5} →
    {M₁ : Type u_6} →
      {M₂ : Type u_7} →
        {M₃ : Type u_8} →
          [inst : CommSemiring R] →
            [inst_1 : AddCommMonoid M] →
              [inst_2 : AddCommMonoid M₁] →
                [inst_3 : AddCommMonoid M₂] →
                  [inst_4 : AddCommMonoid M₃] →
                    [inst_5 : Module R M] →
                      [inst_6 : Module R M₁] →
                        [inst_7 : Module R M₂] →
                          [inst_8 : Module R M₃] →
                            (f : M₁ →ₗ[R] M₂ →ₗ[R] M) →
                              (i : M₃ →ₗ[R] M) →
                                Function.Injective ⇑i → (∀ (x : M₁) (y : M₂), (f x) y ∈ i.range) → M₁ →ₗ[R] M₂ →ₗ[R] M₃
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- The `v`-adic norm of an integer is at most 1.  -/
NumberField.FinitePlace.norm_le_one : ∀ (K : Type u_1) [inst : Field K] {R : Type u_2} [inst_1 : CommRing R] [inst_2 : Algebra R K]
  [inst_3 : IsDedekindDomain R] [inst_4 : IsFractionRing R K] (v : IsDedekindDomain.HeightOneSpectrum R)
  [inst_5 : Module.Finite ℤ R] [inst_6 : Module.Free ℤ R] (x : R),
  ‖(NumberField.FinitePlace.embedding v) ((algebraMap R K) x)‖ ≤ 1
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.mem_of_mem_union_of_not_mem_right : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m₁ m₂ : Std.ExtDHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α}, k ∈ m₁ ∪ m₂ → k ∉ m₂ → k ∈ m₁
-- Lean.CompactedRegion
_private.Lean.CompactedRegion.0.Lean.CompactedRegion.mk.inj : ∀ {filePath : System.FilePath} {size : USize} {isMemoryMapped : Bool} {baseAddr bufferOffset : USize} {root : NonScalar}
  {filePath_1 : System.FilePath} {size_1 : USize} {isMemoryMapped_1 : Bool} {baseAddr_1 bufferOffset_1 : USize}
  {root_1 : NonScalar},
  { filePath := filePath, size := size, isMemoryMapped := isMemoryMapped, baseAddr := baseAddr,
        bufferOffset := bufferOffset, root := root } =
      { filePath := filePath_1, size := size_1, isMemoryMapped := isMemoryMapped_1, baseAddr := baseAddr_1,
        bufferOffset := bufferOffset_1, root := root_1 } →
    filePath = filePath_1 ∧
      size = size_1 ∧
        isMemoryMapped = isMemoryMapped_1 ∧ baseAddr = baseAddr_1 ∧ bufferOffset = bufferOffset_1 ∧ root = root_1
-- Mathlib.RingTheory.TwoSidedIdeal.Basic
TwoSidedIdeal.le_iff : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] {I J : TwoSidedIdeal R}, I ≤ J ↔ ↑I ⊆ ↑J
-- Lean.Parser.Command
Lean.Parser.Command.recommended_spelling.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Topology.ContinuousMap.Algebra
ContinuousMap.instSemigroupOfContinuousMul.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [inst_2 : Semigroup β]
  [inst_3 : ContinuousMul β],
  ContinuousMap.instSemigroupOfContinuousMul = { toMul := ContinuousMap.instMul, mul_assoc := ⋯ }
-- Mathlib.Algebra.Polynomial.Div
Polynomial.divModByMonicAux.eq_1 : ∀ {R : Type u} [inst : Ring R] (x x_1 : Polynomial R) (x_2 : x_1.Monic),
  x.divModByMonicAux x_2 =
    if h : x_1.degree ≤ x.degree ∧ x ≠ 0 then
      have z := Polynomial.C x.leadingCoeff * Polynomial.X ^ (x.natDegree - x_1.natDegree);
      have _wf := ⋯;
      have dm := (x - x_1 * z).divModByMonicAux x_2;
      (z + dm.1, dm.2)
    else (0, x)
-- Mathlib.Combinatorics.Graph.Lattice
Graph.inf_isLink : ∀ {α : Type u_1} {β : Type u_2} {x y : α} {e : β} {G H : Graph α β},
  (G ⊓ H).IsLink e x y ↔ G.IsLink e x y ∧ H.IsLink e x y
-- Mathlib.RingTheory.Adjoin.Basic
Algebra.adjoin_top : ∀ (R : Type uR) {S : Type uS} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] {A : Type u_1}
  [inst_3 : Semiring A] [inst_4 : Algebra S A] (t : Set A),
  Algebra.adjoin (↥⊤) t = Subalgebra.restrictScalars (↥⊤) (Algebra.adjoin S t)
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.arg.withParens : ℕ → Lean.Parser.ParserFn
-- Init.Data.Int.DivMod.Lemmas
Int.lt_mul_of_ediv_lt : ∀ {a b c : ℤ}, 0 < c → a / c < b → a < b * c
-- Mathlib.Topology.Compactness.LocallyCompact
IsClosed.weaklyLocallyCompactSpace : ∀ {X : Type u_1} [inst : TopologicalSpace X] [WeaklyLocallyCompactSpace X] {s : Set X},
  IsClosed s → WeaklyLocallyCompactSpace ↑s
-- Mathlib.Analysis.Convex.Star
StarConvex.neg : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {x : E} {s : Set E}, StarConvex 𝕜 x s → StarConvex 𝕜 (-x) (-s)
-- Init.Data.Nat.Lemmas
Nat.eq_zero_of_le_div : ∀ {n m : ℕ}, 2 ≤ n → m ≤ m / n → m = 0
-- Init.Data.Int.DivMod.Bootstrap
Int.dvd_zero : ∀ (n : ℤ), n ∣ 0
-- Mathlib.Topology.UniformSpace.Defs
/-- Symmetric entourages form a basis of `𝓤 α`  -/
UniformSpace.hasBasis_symmetric : ∀ {α : Type ua} [inst : UniformSpace α], (uniformity α).HasBasis (fun s => s ∈ uniformity α ∧ s.IsSymm) id
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Clz
Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} → (aig : Std.Sat.AIG α) → aig.RefVec w → ℕ → aig.RefVec w → Std.Sat.AIG.RefVecEntry α w
-- Mathlib.Data.DFinsupp.Defs
/-- `DFinsupp.single` as an `AddMonoidHom`.  -/
DFinsupp.singleAddHom : {ι : Type u} →
  (β : ι → Type v) → [DecidableEq ι] → [inst : (i : ι) → AddZeroClass (β i)] → (i : ι) → β i →+ Π₀ (i : ι), β i
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δ.eq_1 : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  {σ : Type w₂} (Q : Algebra.Generators S T ι) (P : Algebra.Generators R S σ),
  Algebra.Generators.H1Cotangent.δ Q P =
    SnakeLemma.δ' (LinearMap.baseChange T P.toExtension.cotangentComplex) (Q.comp P).toExtension.cotangentComplex
      Q.toExtension.cotangentComplex
      (LinearMap.liftBaseChange T (Algebra.Extension.Cotangent.map (Q.toComp P).toExtensionHom))
      (Algebra.Extension.Cotangent.map (Q.ofComp P).toExtensionHom) ⋯
      (LinearMap.liftBaseChange T (Algebra.Extension.CotangentSpace.map (Q.toComp P).toExtensionHom))
      (Algebra.Extension.CotangentSpace.map (Q.ofComp P).toExtensionHom) ⋯ ⋯ ⋯ Algebra.Extension.h1Cotangentι ⋯
      (LinearMap.baseChange T P.toExtension.toKaehler) ⋯ ⋯ ⋯
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instAddCancelCommMonoid : {α : Type u_1} → [AddCancelCommMonoid α] → AddCancelCommMonoid αᵃᵒᵖ
-- Std.Tactic.Do.Syntax
/-- `mrename_i` is like `rename_i`, but names inaccessible stateful hypotheses in a `Std.Do.SPred` goal.
 -/
Lean.Parser.Tactic.mrenameIError : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
/-- If a `BinaryFan` is a limit, then its opposite is a colimit.  -/
CategoryTheory.Limits.BinaryFan.IsLimit.op : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} →
      {c : CategoryTheory.Limits.BinaryFan X Y} → CategoryTheory.Limits.IsLimit c → CategoryTheory.Limits.IsColimit c.op
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Embedding.sumInl_apply : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} (u : V),
  SimpleGraph.Embedding.sumInl u = Sum.inl u
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.insertMin.match_3.congr_eq_2 : ∀ {α : Type u_1} {β : α → Type u_2} (motive : (t : Std.DTreeMap.Internal.Impl α β) → t.Balanced → Sort u_3)
  (t : Std.DTreeMap.Internal.Impl α β) (hr : t.Balanced)
  (h_1 : (hr : Std.DTreeMap.Internal.Impl.leaf.Balanced) → motive Std.DTreeMap.Internal.Impl.leaf hr)
  (h_2 :
    (sz : ℕ) →
      (k' : α) →
        (v' : β k') →
          (l' r' : Std.DTreeMap.Internal.Impl α β) →
            (hr : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced) →
              motive (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r') hr)
  (sz : ℕ) (k' : α) (v' : β k') (l' r' : Std.DTreeMap.Internal.Impl α β)
  (hr_1 : (Std.DTreeMap.Internal.Impl.inner sz k' v' l' r').Balanced),
  t = Std.DTreeMap.Internal.Impl.inner sz k' v' l' r' →
    hr ≍ hr_1 →
      (match t, hr with
        | Std.DTreeMap.Internal.Impl.leaf, hr => h_1 hr
        | Std.DTreeMap.Internal.Impl.inner sz k' v' l' r', hr => h_2 sz k' v' l' r' hr) ≍
        h_2 sz k' v' l' r' hr_1
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
LinearMap.rTensor_range : ∀ {R : Type u_1} [inst : CommSemiring R] {N : Type u_3} {P : Type u_4} (Q : Type u_5) [inst_1 : AddCommMonoid N]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R N] [inst_5 : Module R P]
  [inst_6 : Module R Q] {g : N →ₗ[R] P}, (LinearMap.rTensor Q g).range = (LinearMap.rTensor Q g.range.subtype).range
-- Qq.MatchImpl
Qq.Impl.PatVarDecl.ty : Qq.Impl.PatVarDecl → Option Q(Lean.Expr)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.get_eq_get! : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : Inhabited β] {a : α} {h : a ∈ t}, Std.DTreeMap.Const.get t a h = Std.DTreeMap.Const.get! t a
-- Mathlib.Geometry.Manifold.StructureGroupoid
/-- If `f = g` on `u` and `property f u`, then `property g u`  -/
Pregroupoid.congr : ∀ {H : Type u_2} [inst : TopologicalSpace H] (self : Pregroupoid H) {f g : H → H} {u : Set H},
  IsOpen u → (∀ x ∈ u, g x = f x) → self.property f u → self.property g u
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.ServerCapabilities.textDocumentSync? : Lean.Lsp.ServerCapabilities → Option Lean.Lsp.TextDocumentSyncOptions
-- Mathlib.Algebra.Order.Ring.Units
Units.index_posSubgroup : ∀ (R : Type u_1) [inst : Ring R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R],
  (Units.posSubgroup R).index = 2
-- Mathlib.Algebra.Category.ModuleCat.Simple
simple_iff_isSimpleModule' : ∀ {R : Type u_1} [inst : Ring R] (M : ModuleCat R), CategoryTheory.Simple M ↔ IsSimpleModule R ↑M
-- Mathlib.Analysis.Meromorphic.Basic
/-- If `f` is meromorphic at a point, then so is its logarithmic derivative.  -/
MeromorphicAt.logDeriv : ∀ {𝕜 : Type u_1} {𝕜' : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NontriviallyNormedField 𝕜']
  [inst_2 : NormedAlgebra 𝕜 𝕜'] {x : 𝕜} [CompleteSpace 𝕜'] {f : 𝕜 → 𝕜'},
  MeromorphicAt f x → MeromorphicAt (logDeriv f) x
-- Mathlib.GroupTheory.Commutator.Basic
/-- **The Hall-Witt identity**  -/
addCommutatorElement_addConj_addCommutatorElement_add : ∀ {G : Type u_1} [inst : AddGroup G] (a b c : G), ⁅a + b + -a, ⁅c, a⁆⁆ + ⁅c + a + -c, ⁅b, c⁆⁆ + ⁅b + c + -b, ⁅a, b⁆⁆ = 0
-- Batteries.Lean.LawfulMonadLift
_private.Batteries.Lean.LawfulMonadLift.0.EST.bind.match_1.splitter : {ε σ α : Type} →
  (motive : EST.Out ε σ α → Sort u_1) →
    (x : EST.Out ε σ α) →
      ((a : α) → (s : Void σ) → motive (EST.Out.ok a s)) →
        ((e : ε) → (s : Void σ) → motive (EST.Out.error e s)) → motive x
-- Mathlib.GroupTheory.Index
MonoidHom.surjective_of_card_ker_le_div : ∀ {G : Type u_1} {M : Type u_2} [inst : Group G] [inst_1 : Group M] [Finite G] [Finite M] (f : G →* M),
  Nat.card ↥f.ker ≤ Nat.card G / Nat.card M → Function.Surjective ⇑f
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- Conversion to normal form at `x` changes the value only at x.  -/
MeromorphicAt.eq_nhdsNE_toMeromorphicNFAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {x : 𝕜}, MeromorphicAt f x → f =ᶠ[nhdsWithin x {x}ᶜ] toMeromorphicNFAt f x
-- Mathlib.Algebra.Lie.Classical
LieAlgebra.Orthogonal.so'.eq_1 : ∀ (p : Type u_2) (q : Type u_3) (R : Type u₂) [inst : DecidableEq p] [inst_1 : DecidableEq q] [inst_2 : CommRing R]
  [inst_3 : Fintype p] [inst_4 : Fintype q],
  LieAlgebra.Orthogonal.so' p q R = skewAdjointMatricesLieSubalgebra (LieAlgebra.Orthogonal.indefiniteDiagonal p q R)
-- Mathlib.Algebra.GCDMonoid.Basic
gcd_eq_of_dvd_sub_left : ∀ {α : Type u_1} [inst : CommRing α] [inst_1 : NormalizedGCDMonoid α] {a b c : α}, a ∣ b - c → gcd b a = gcd c a
-- Init.Data.Nat.Basic
Nat.add_mul : ∀ (n m k : ℕ), (n + m) * k = n * k + m * k
-- Mathlib.CategoryTheory.Abelian.Projective.Dimension
CategoryTheory.instHasProjectiveDimensionLTSucc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] (X : C) (n : ℕ)
  [CategoryTheory.HasProjectiveDimensionLT X n], CategoryTheory.HasProjectiveDimensionLT X n.succ
-- Std.Data.HashSet.Lemmas
Std.HashSet.get.congr_simp : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] (m m_1 : Std.HashSet α) (e_m : m = m_1) (a a_1 : α) (e_a : a = a_1)
  (h : a ∈ m), m.get a h = m_1.get a_1 ⋯
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.comap_inclusion_addSubgroupOf : ∀ {G : Type u_1} [inst : AddGroup G] {K₁ K₂ : AddSubgroup G} (h : K₁ ≤ K₂) (H : AddSubgroup G),
  AddSubgroup.comap (AddSubgroup.inclusion h) (H.addSubgroupOf K₂) = H.addSubgroupOf K₁
-- Std.Data.Iterators.Producers.Monadic.Vector
/-- Returns a finite monadic iterator for the given vector starting at the given index.
The iterator yields the elements of the vector in order and then terminates.

The pure version of this iterator is
`Vector.iterFromIdx`.

**Termination properties:**

* `Finite` instance: always

* `Productive` instance: always
 -/
Vector.iterFromIdxM : {α : Type w} → {n : ℕ} → Vector α n → (m : Type w → Type w') → ℕ → [Pure m] → Std.IterM m α
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aevalTower_X : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S : Type u_2} {A : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring A] [inst_3 : Algebra S R] [inst_4 : Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (i : σ),
  (MvPolynomial.aevalTower g y) (MvPolynomial.X i) = y i
-- Mathlib.AlgebraicGeometry.Sites.BigZariski
AlgebraicGeometry.Scheme.zariskiTopology.eq_1 : AlgebraicGeometry.Scheme.zariskiTopology =
  AlgebraicGeometry.Scheme.grothendieckTopology AlgebraicGeometry.IsOpenImmersion
-- Mathlib.LinearAlgebra.Matrix.Transvection
Matrix.transvection.eq_1 : ∀ {n : Type u_1} {R : Type u₂} [inst : DecidableEq n] [inst_1 : CommRing R] (i j : n) (c : R),
  Matrix.transvection i j c = 1 + Matrix.single i j c
-- Init.Data.Ord.Basic
instOrdOption : {α : Type u_1} → [Ord α] → Ord (Option α)
-- Mathlib.SetTheory.Cardinal.Arithmetic
Cardinal.mk_add_one_eq : ∀ {α : Type u_1} [Infinite α], Cardinal.mk α + 1 = Cardinal.mk α
-- Init.System.IOError
IO.Error.mkInvalidArgument : UInt32 → String → IO.Error
-- Plausible.Sampleable
Plausible.Prod.sampleableExt : {α : Type u} →
  {β : Type v} → [Plausible.SampleableExt α] → [Plausible.SampleableExt β] → Plausible.SampleableExt (α × β)
-- Init.Data.BitVec.Bitblast
/-- Remember that negating a bitvector is equal to incrementing the complement
by one, i.e., `-x = ~~~x + 1`. See also `neg_eq_not_add`.

This computation has two crucial properties:
- The least significant bit of `-x` is the same as the least significant bit of `x`, and
- The `i+1`-th least significant bit of `-x` is the complement of the `i+1`-th bit of `x`, unless
  all of the preceding bits are `false`, in which case the bit is equal to the `i+1`-th bit of `x`
 -/
BitVec.getLsbD_neg : ∀ {w i : ℕ} {x : BitVec w}, (-x).getLsbD i = (x.getLsbD i ^^ decide (i < w) && decide (∃ j < i, x.getLsbD j = true))
-- Mathlib.Tactic.CasesM
/-- `cases_type I` searches for a hypothesis `h : type` where `I` has the form `(I ...)`, and splits the
main goal by cases on `h`. `cases_type p` fails if no hypothesis type has the identifier `I` as its
head symbol.

* `cases_type I_1 ... I_n` searches for a hypothesis `h : type` where `type` has one or more of
  `I_1`, ..., `I_n` as its head symbol, and splits the main goal by cases on `h`.
* `cases_type* I` repeatedly performs case splits until no more hypothesis type has `I` as its head
  symbol. This shorthand for `· repeat cases_type I`.
* `cases_type! p` and `cases_type!* p` skip a hypothesis if the main goal would be replaced with two
  or more subgoals.

Example:
```
example (h : a ∧ b ∨ c ∧ d) (h2 : e ∧ f) : True := by
  -- The following tactic destructs all conjunctions and disjunctions in the current context.
  cases_type* Or And
  · clear ‹a› ‹b› ‹e› ‹f›; (fail_if_success clear ‹c›); trivial
  · clear ‹c› ‹d› ‹e› ‹f›; trivial
```
 -/
Mathlib.Tactic.casesType : Lean.ParserDescr
-- Std.Time.Zoned.Database.TzIf
/-- An optional footer for additional metadata in version 2.
 -/
Std.Time.TimeZone.TZif.TZifV2.footer : Std.Time.TimeZone.TZif.TZifV2 → Option String
-- Aesop.Index.Forward
Aesop.ForwardIndex.instEmptyCollection : EmptyCollection Aesop.ForwardIndex
-- Mathlib.Combinatorics.Tiling.Tile
DiscreteTiling.Prototile.mk.sizeOf_spec : ∀ {G : Type u_1} {X : Type u_2} [inst : Group G] [inst_1 : MulAction G X] [inst_2 : SizeOf G] [inst_3 : SizeOf X]
  (carrier : Set X) (symmetries : Subgroup ↥(MulAction.stabilizer G carrier)),
  sizeOf { carrier := carrier, symmetries := symmetries } = 1 + sizeOf symmetries
-- Mathlib.RingTheory.DividedPowerAlgebra.Init
DividedPowerAlgebra.map_id : ∀ {R : Type u_2} {M : Type u_3} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  DividedPowerAlgebra.map R LinearMap.id = AlgHom.id R (DividedPowerAlgebra R M)
-- Mathlib.Analysis.Convex.Side
AffineSubspace.WSameSide.trans_sOppSide : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : Field R] [inst_1 : LinearOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y z : P}, s.WSameSide x y → s.SOppSide y z → s.WOppSide x z
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.lcm_dvd : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] {x y z : R},
  x ∣ z → y ∣ z → EuclideanDomain.lcm x y ∣ z
-- Mathlib.CategoryTheory.Adjunction.Basic
/-- Construct a left adjoint functor to `G`, given the functor's value on objects `F_obj` and
a bijection `e` between `F_obj X ⟶ Y` and `X ⟶ G.obj Y` satisfying a naturality law
`he : ∀ X Y Y' g h, e X Y' (h ≫ g) = e X Y h ≫ G.map g`.
Dual to `rightAdjointOfEquiv`.  -/
CategoryTheory.Adjunction.leftAdjointOfEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {G : CategoryTheory.Functor D C} →
          {F_obj : C → D} →
            (e : (X : C) → (Y : D) → (F_obj X ⟶ Y) ≃ (X ⟶ G.obj Y)) →
              (∀ (X : C) (Y Y' : D) (g : Y ⟶ Y') (h : F_obj X ⟶ Y),
                  (e X Y') (CategoryTheory.CategoryStruct.comp h g) =
                    CategoryTheory.CategoryStruct.comp ((e X Y) h) (G.map g)) →
                CategoryTheory.Functor C D
-- Mathlib.Order.SuccPred.Basic
Order.le_pred_iff_isMin : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] {a : α}, a ≤ Order.pred a ↔ IsMin a
-- Mathlib.Algebra.Ring.Subring.Order
/-- A subring of an ordered ring is an ordered ring.  -/
Subring.toIsOrderedRing : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : SetLike S R]
  [inst_3 : SubringClass S R] [IsOrderedRing R] (s : S), IsOrderedRing ↥s
-- Std.Http.Data.Headers.Name
Std.Http.Header.instReprName : Repr Std.Http.Header.Name
-- Init.Data.Int.Order
Int.toNat_one : Int.toNat 1 = 1
-- Mathlib.RingTheory.Coalgebra.Basic
Coalgebra.sum_map_tmul_counit_eq : ∀ {R : Type u} {A : Type v} {ι : Type u_1} [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : Coalgebra R A] {B : Type u_4} [inst_4 : AddCommMonoid B] [inst_5 : Module R B] {F : Type u_5}
  [inst_6 : FunLike F A B] [LinearMapClass F R A B] (f : F) (a : A) {repr : Coalgebra.Repr R a ι},
  ∑ i ∈ repr.index, f (repr.left i) ⊗ₜ[R] CoalgebraStruct.counit (repr.right i) = f a ⊗ₜ[R] 1
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.coe_one : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V], ↑1 = 1
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_map : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {γ : α → Type w}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {f : (a : α) → β a → γ a} {k : α},
  m.WF → (Std.DHashMap.Raw.map f m).getKey! k = m.getKey! k
-- Mathlib.MeasureTheory.Integral.Bochner.L1
MeasureTheory.weightedSMul_zero_measure : ∀ {α : Type u_1} {F : Type u_3} [inst : NormedAddCommGroup F] [inst_1 : NormedSpace ℝ F] {m : MeasurableSpace α},
  MeasureTheory.weightedSMul 0 = 0
-- Aesop.RuleTac.RuleTerm
Aesop.RuleTerm.term.sizeOf_spec : ∀ (term : Lean.Term), sizeOf (Aesop.RuleTerm.term term) = 1 + sizeOf term
-- Lean.Data.OpenDecl
Lean.instBEqOpenDecl.beq : Lean.OpenDecl → Lean.OpenDecl → Bool
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.le_prod_nonempty_of_submultiplicative_on_pred : ∀ {α : Type u_5} {β : Type u_6} [inst : Monoid α] [inst_1 : CommMonoid β] [inst_2 : Preorder β] [IsOrderedMonoid β]
  (f : α → β) (p : α → Prop),
  (∀ (a b : α), p a → p b → f (a * b) ≤ f a * f b) →
    (∀ (a b : α), p a → p b → p (a * b)) → ∀ (l : List α), l ≠ [] → (∀ a ∈ l, p a) → f l.prod ≤ (List.map f l).prod
-- Mathlib.Data.Analysis.Topology
/-- Every `Ctop` is a topological space.  -/
Ctop.toTopsp : {α : Type u_1} → {σ : Type u_3} → Ctop α σ → TopologicalSpace α
-- Mathlib.MeasureTheory.Integral.Gamma
integral_rpow_mul_exp_neg_rpow : ∀ {p q : ℝ}, 0 < p → -1 < q → ∫ (x : ℝ) in Set.Ioi 0, x ^ q * Real.exp (-x ^ p) = 1 / p * Real.Gamma ((q + 1) / p)
-- Mathlib.Data.ENNReal.Basic
ENNReal.coe_mul : ∀ (x y : NNReal), ↑(x * y) = ↑x * ↑y
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.getKey!_filter_key : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {f : α → Bool} {k : α},
  t.WF → (Std.DTreeMap.Raw.filter (fun k x => f k) t).getKey! k = (Option.filter f (t.getKey? k)).get!
-- Mathlib.RingTheory.FilteredAlgebra.Basic
IsFiltration.is_le : ∀ {ι : Type u_1} {σ : Type u_3} {inst : Preorder ι} {inst_1 : Preorder σ} {F : ι → σ} {F_lt : outParam (ι → σ)}
  [self : IsFiltration F F_lt] {i j : ι}, i < j → F i ≤ F_lt j
-- Mathlib.Data.Real.Basic
Real.cauchy_zero : Real.cauchy 0 = 0