mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
isIntegral_natCast : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] (a : ℕ), IsIntegral R ↑a
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp_assoc_left_inv_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b c d : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) {Z : F.obj a ⟶ F.obj d}
  (h_1 : F.map (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp f g) h) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapComp f g).inv (F.map h))
      (CategoryTheory.CategoryStruct.comp (F.mapComp (CategoryTheory.CategoryStruct.comp f g) h).inv h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (F.map f) (F.map g) (F.map h)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapComp g h).inv)
        (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.comp g h)).inv
          (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.associator f g h).inv) h_1)))
-- Init.Omega.Constraint
/-- An optional upper bound on a integer.  -/
Lean.Omega.UpperBound : Type
-- Mathlib.CategoryTheory.ObjectProperty.FunctorCategory.PreservesLimits
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphismsFunctorPreservesFiniteColimits : ∀ {J : Type u_1} {C : Type u_3} [inst : CategoryTheory.Category.{v_3, u_1} J]
  [inst_1 : CategoryTheory.Category.{v_5, u_3} C],
  CategoryTheory.ObjectProperty.preservesFiniteColimits.IsClosedUnderIsomorphisms
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.measure_union_add_inter : ∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {t : Set α} (s : Set α),
  MeasurableSet t → μ (s ∪ t) + μ (s ∩ t) = μ s + μ t
-- Mathlib.Data.Ordmap.Invariants
Ordnode.rotateR_nil : ∀ {α : Type u_1} (y : α) (r : Ordnode α), Ordnode.nil.rotateR y r = Ordnode.nil.node' y r
-- Mathlib.Analysis.Convex.Combination
/-- The convex hull of `s` is equal to the set of centers of masses of finite families of points in
`s`.

For universe reasons, you shouldn't use this lemma to prove that a given center of mass belongs
to the convex hull. Use `mem_convexHull_of_exists_fintype` of the convex hull instead.  -/
mem_convexHull_iff_exists_fintype : ∀ {R : Type u_1} {E : Type u_3} [inst : Field R] [inst_1 : AddCommGroup E] [inst_2 : Module R E]
  [inst_3 : LinearOrder R] [IsStrictOrderedRing R] {s : Set E} {x : E},
  x ∈ (convexHull R) s ↔ ∃ ι x_1 w z, (∀ (i : ι), 0 ≤ w i) ∧ ∑ i, w i = 1 ∧ (∀ (i : ι), z i ∈ s) ∧ ∑ i, w i • z i = x
-- Init.Data.Vector.Lemmas
Vector.findSomeRevM?_mk : ∀ {m : Type u_1 → Type u_2} {α : Type u_3} {n : ℕ} {β : Type u_1} [inst : Monad m] {xs : Array α} (h : xs.size = n)
  (f : α → m (Option β)), Vector.findSomeRevM? f (Vector.mk xs h) = Array.findSomeRevM? f xs
-- Mathlib.Algebra.Group.Commute.Defs
/-- Two elements additively commute if `a + b = b + a`  -/
AddCommute : {S : Type u_3} → [Add S] → S → S → Prop
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_mul_cos_add_sin_mul_I : ∀ {r : ℝ},
  0 < r → ∀ {θ : ℝ}, θ ∈ Set.Ioc (-Real.pi) Real.pi → (↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)).arg = θ
-- Mathlib.CategoryTheory.Limits.Types.Coproducts
/-- The categorical binary coproduct in `Type u` is the sum `X ⊕ Y`.  -/
CategoryTheory.Limits.Types.binaryCoproductIso : (X Y : Type u) → X ⨿ Y ≅ X ⊕ Y
-- Mathlib.AlgebraicTopology.SingularSet
/-- The geometric realization of the representable simplicial sets agree
with the usual topological simplices.  -/
SSet.toTopSimplex : CategoryTheory.Functor.comp SSet.stdSimplex SSet.toTop ≅ SimplexCategory.toTop.{u}
-- Lean.Message
Lean.instToMessageDataLevel : Lean.ToMessageData Lean.Level
-- Mathlib.Algebra.MonoidAlgebra.Defs
/-- Remove a term from an element of the additive monoid algebra.  -/
AddMonoidAlgebra.erase : {R : Type u_1} → {M : Type u_4} → [inst : Semiring R] → M → AddMonoidAlgebra R M → AddMonoidAlgebra R M
-- Mathlib.Analysis.Complex.Circle
Circle.toUnits_apply : ∀ (z : Circle), Circle.toUnits z = Units.mk0 ↑z ⋯
-- Init.System.IOError
IO.Error.inappropriateType.sizeOf_spec : ∀ (filename : Option String) (osCode : UInt32) (details : String),
  sizeOf (IO.Error.inappropriateType filename osCode details) = 1 + sizeOf filename + sizeOf osCode + sizeOf details
-- Init.Data.SInt.Lemmas
UInt16.toInt16_add : ∀ (a b : UInt16), (a + b).toInt16 = a.toInt16 + b.toInt16
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKey!_filterMap : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} {γ : α → Type w}
  [inst : LawfulBEq α] [inst_1 : Inhabited α] {f : (a : α) → β a → Option (γ a)} {k : α},
  (Std.DHashMap.filterMap f m).getKey! k = ((m.getKey? k).pfilter fun x_2 h' => (f x_2 (m.get x_2 ⋯)).isSome).get!
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Equalizers
CategoryTheory.Limits.Cofork.unop_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : Cᵒᵖ} {f g : X ⟶ Y}
  (c : CategoryTheory.Limits.Cofork f g), c.unop.ι = c.π.unop
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_disjSum : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : OrderTop α] (s : Finset β)
  (t : Finset γ) (f : β ⊕ γ → α), (s.disjSum t).inf f = (s.inf fun x => f (Sum.inl x)) ⊓ t.inf fun x => f (Sum.inr x)
-- Mathlib.Algebra.Homology.ShortComplex.HomologicalComplex
HomologicalComplex.iCycles_d_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} (K : HomologicalComplex C c) (i j : ι) [inst_2 : K.HasHomology i] {Z : C}
  (h : K.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (K.iCycles i) (CategoryTheory.CategoryStruct.comp (K.d i j) h) =
    CategoryTheory.CategoryStruct.comp 0 h
-- Mathlib.GroupTheory.Perm.Cycle.Factors
Equiv.Perm.cycleOf_apply_of_not_sameCycle : ∀ {α : Type u_2} {f : Equiv.Perm α} {x y : α} [inst : DecidableRel f.SameCycle], ¬f.SameCycle x y → (f.cycleOf x) y = y
-- Lean.Data.Lsp.Diagnostics
Lean.Lsp.instBEqDiagnosticSeverity : BEq Lean.Lsp.DiagnosticSeverity
-- Mathlib.Order.Filter.AtTopBot.CompleteLattice
/-- If `f` is an antitone function with bounded range
and `g` tends to `atTop` along a nontrivial filter,
then the indexed infimum of `f ∘ g` is equal to the indexed infimum of `f`.

The assumption `BddBelow (range f)` can be omitted,
if the codomain of `f` is a conditionally complete linear order or a complete lattice, see below.
 -/
Antitone.ciInf_comp_tendsto_atTop : ∀ {α : Type u_3} {β : Type u_4} {γ : Type u_5} [inst : Preorder β] [inst_1 : ConditionallyCompleteLattice γ]
  {l : Filter α} [l.NeBot] {f : β → γ},
  Antitone f → BddBelow (Set.range f) → ∀ {g : α → β}, Filter.Tendsto g l Filter.atTop → ⨅ a, f (g a) = ⨅ b, f b
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instDivisionCommMonoidOfMulOpposite : {M : Type u_1} → [DivisionCommMonoid Mᵐᵒᵖ] → DivisionCommMonoid Mᵈᵐᵃ
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_mul_closure_one : ∀ {G : Type u_1} [inst : MulOneClass G] [inst_1 : TopologicalSpace G] (s : Set G), s ⊆ s * closure {1}
-- Mathlib.GroupTheory.Perm.Option
/-- The set of all permutations of `Option α` can be constructed by augmenting the set of
permutations of `α` by each element of `Option α` in turn.  -/
Finset.univ_perm_option : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α],
  Finset.univ = Finset.map Equiv.Perm.decomposeOption.symm.toEmbedding Finset.univ
-- Init.Data.Dyadic.Basic
Rat.toDyadic_mkRat : ∀ (a : ℤ) (b : ℕ) (prec : ℤ),
  (mkRat a b).toDyadic prec = Dyadic.ofIntWithPrec (a <<< prec.toNat / ↑(b <<< (-prec).toNat)) prec
-- Mathlib.Algebra.Group.Submonoid.MulOpposite
Submonoid.mem_unop : ∀ {M : Type u_2} [inst : MulOneClass M] {x : M} {S : Submonoid Mᵐᵒᵖ}, x ∈ S.unop ↔ MulOpposite.op x ∈ S
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
HurwitzZeta.completedSinZeta_neg : ∀ (a : UnitAddCircle) (s : ℂ), HurwitzZeta.completedSinZeta (-a) s = -HurwitzZeta.completedSinZeta a s
-- Mathlib.Data.Set.Insert
LE.le.ssubset_of_mem_notMem : ∀ {α : Type u_1} {s t : Set α} {a : α}, s ⊆ t → a ∈ t → a ∉ s → s ⊂ t
-- Mathlib.RingTheory.WittVector.Domain
WittVector.verschiebung_shift : ∀ {p : ℕ} {R : Type u_1} [hp : Fact (Nat.Prime p)] [inst : CommRing R] (x : WittVector p R) (k : ℕ),
  (∀ i < k + 1, x.coeff i = 0) → WittVector.verschiebung (x.shift k.succ) = x.shift k
-- Mathlib.Topology.Algebra.Ring.Basic
instIsTopologicalRingAddOpposite : ∀ {R : Type u_1} [inst : NonUnitalNonAssocRing R] [inst_1 : TopologicalSpace R] [IsTopologicalRing R],
  IsTopologicalRing Rᵃᵒᵖ
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.iteration_map_succ_injectivity : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {W : CategoryTheory.MorphismProperty C} {Z : C}
  [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_4 :
    ∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
  {κ : Cardinal.{w}} [inst_5 : OrderBot κ.ord.ToType]
  [inst_6 : CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C] [Fact κ.IsRegular] {X Y : C} (f : X ⟶ Y),
  W f →
    ∀ {j : κ.ord.ToType} (g₁ g₂ : Y ⟶ (CategoryTheory.OrthogonalReflection.iteration W Z κ).obj j),
      CategoryTheory.CategoryStruct.comp f g₁ = CategoryTheory.CategoryStruct.comp f g₂ →
        CategoryTheory.CategoryStruct.comp g₁
            ((CategoryTheory.OrthogonalReflection.iteration W Z κ).map (CategoryTheory.homOfLE ⋯)) =
          CategoryTheory.CategoryStruct.comp g₂
            ((CategoryTheory.OrthogonalReflection.iteration W Z κ).map (CategoryTheory.homOfLE ⋯))
-- Batteries.Data.String.Lemmas
/-- The canonical constructor for `ValidFor`.  -/
String.Legacy.Iterator.ValidFor.mk : ∀ {l r : List Char},
  String.Legacy.Iterator.ValidFor l r { s := String.ofList (l.reverseAux r), i := { byteIdx := String.utf8Len l } }
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.get?_eq_some_getD : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α} {fallback : β},
  a ∈ m → Std.DHashMap.Const.get? m a = some (Std.DHashMap.Const.getD m a fallback)
-- Mathlib.Tactic.FunProp.Mor
Mathlib.Meta.FunProp.Mor.Arg.mk.injEq : ∀ (expr : Lean.Expr) (coe : Option Lean.Expr) (expr_1 : Lean.Expr) (coe_1 : Option Lean.Expr),
  ({ expr := expr, coe := coe } = { expr := expr_1, coe := coe_1 }) = (expr = expr_1 ∧ coe = coe_1)
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.isIntegralHom_over_iff_isEmpty : ∀ {n : Type u} (S : AlgebraicGeometry.Scheme),
  AlgebraicGeometry.IsIntegralHom (AlgebraicGeometry.AffineSpace n S ↘ S) ↔ IsEmpty ↥S ∨ IsEmpty n
-- Lean.Parser.Do
Lean.Parser.Term.termFor.parenthesizer : Lean.PrettyPrinter.Parenthesizer
-- Mathlib.Order.ConditionallyCompleteLattice.Basic
instCompleteLatticeWithTop.eq_1 : ∀ {α : Type u_1} [inst : CompleteLattice α],
  instCompleteLatticeWithTop =
    { toLattice := WithTop.lattice, toSupSet := WithTop.instSupSet, isLUB_sSup := ⋯, toInfSet := WithTop.instInfSet,
      isGLB_sInf := ⋯, toBoundedOrder := WithTop.instBoundedOrder }
-- Mathlib.Control.Bitraversable.Basic
LawfulBitraversable.toLawfulBifunctor : ∀ {t : Type u → Type u → Type u} {inst : Bitraversable t} [self : LawfulBitraversable t], LawfulBifunctor t
-- Lean.Util.CollectAxioms
_private.Lean.Util.CollectAxioms.0.Lean.ExportedAxiomsState.mk.inj : ∀ {importedModuleEntries importedModuleEntries_1 : Array (Array (Lean.Name × Array Lean.Name))},
  { importedModuleEntries := importedModuleEntries } = { importedModuleEntries := importedModuleEntries_1 } →
    importedModuleEntries = importedModuleEntries_1
-- Mathlib.Algebra.Homology.ShortComplex.Exact
/-- If a short complex `S` in a balanced category is exact and such that `S.g` is an epi,
then a morphism `k : S.X₂ ⟶ A` such that `S.f ≫ k = 0` descends to a morphism `S.X₃ ⟶ A`.  -/
CategoryTheory.ShortComplex.Exact.desc : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {S : CategoryTheory.ShortComplex C} →
        [CategoryTheory.Balanced C] →
          S.Exact →
            {A : C} →
              (k : S.X₂ ⟶ A) → CategoryTheory.CategoryStruct.comp S.f k = 0 → [CategoryTheory.Epi S.g] → S.X₃ ⟶ A
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.rpowIntegrand₀₁_eq_pow_div : ∀ {p t x : ℝ}, p ∈ Set.Ioo 0 1 → 0 ≤ t → 0 ≤ x → p.rpowIntegrand₀₁ t x = t ^ (p - 1) * x / (t + x)
-- Mathlib.Algebra.Exact.Basic
/-- When we have a commutative diagram from a sequence of two linear maps to another,
such that the left vertical map is surjective, the middle vertical map is bijective and the right
vertical map is injective, then the upper row is exact iff the lower row is.
See `ShortComplex.exact_iff_of_epi_of_isIso_of_mono` in the file
`Mathlib/Algebra/Homology/ShortComplex/Exact.lean` for the categorical version of this result.  -/
LinearMap.exact_iff_of_surjective_of_bijective_of_injective : ∀ {R : Type u_1} [inst : Ring R] {M₁ : Type u_8} {M₂ : Type u_9} {M₃ : Type u_10} {N₁ : Type u_11} {N₂ : Type u_12}
  {N₃ : Type u_13} [inst_1 : AddCommMonoid M₁] [inst_2 : AddCommMonoid M₂] [inst_3 : AddCommMonoid M₃]
  [inst_4 : AddCommMonoid N₁] [inst_5 : AddCommMonoid N₂] [inst_6 : AddCommMonoid N₃] [inst_7 : Module R M₁]
  [inst_8 : Module R M₂] [inst_9 : Module R M₃] [inst_10 : Module R N₁] [inst_11 : Module R N₂] [inst_12 : Module R N₃]
  (f : M₁ →ₗ[R] M₂) (g : M₂ →ₗ[R] M₃) (f' : N₁ →ₗ[R] N₂) (g' : N₂ →ₗ[R] N₃) (τ₁ : M₁ →ₗ[R] N₁) (τ₂ : M₂ →ₗ[R] N₂)
  (τ₃ : M₃ →ₗ[R] N₃),
  f' ∘ₗ τ₁ = τ₂ ∘ₗ f →
    g' ∘ₗ τ₂ = τ₃ ∘ₗ g →
      Function.Surjective ⇑τ₁ →
        Function.Bijective ⇑τ₂ → Function.Injective ⇑τ₃ → (Function.Exact ⇑f ⇑g ↔ Function.Exact ⇑f' ⇑g')
-- Init.Data.Int.Basic
/-- Non-strict inequality of integers, usually accessed via the `≤` operator.

`a ≤ b` is defined as `b - a ≥ 0`, using `Int.NonNeg`.
 -/
Int.le : ℤ → ℤ → Prop
-- Mathlib.Combinatorics.SimpleGraph.Subgraph
SimpleGraph.nonempty_subgraphOfAdj_verts : ∀ {V : Type u} {G : SimpleGraph V} {v w : V} (hvw : G.Adj v w), Nonempty ↑(G.subgraphOfAdj hvw).verts
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.SelectM.State.mk.injEq : ∀ (suggestions : Array Lean.Meta.Tactic.TryThis.Suggestion) (thms : Array Lean.Meta.Grind.EMatchTheorem)
  (suggestions_1 : Array Lean.Meta.Tactic.TryThis.Suggestion) (thms_1 : Array Lean.Meta.Grind.EMatchTheorem),
  ({ suggestions := suggestions, thms := thms } = { suggestions := suggestions_1, thms := thms_1 }) =
    (suggestions = suggestions_1 ∧ thms = thms_1)
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.totalDegree_eq : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (p : MvPolynomial σ R),
  p.totalDegree = p.support.sup fun m => (Finsupp.toMultiset m).card
-- Mathlib.Order.Circular
SBtw.sbtw.trans_left : ∀ {α : Type u_1} [inst : CircularPreorder α] {a b c d : α}, sbtw a b c → sbtw b d c → sbtw a d c
-- Mathlib.Algebra.BrauerGroup.Defs
/-- `CSA` is the set of all finite-dimensional central simple algebras over a field `K`. For the
generalization to a `CommRing`, see `IsAzumaya` in `Mathlib/Algebra/Azumaya/Defs.lean`.  -/
CSA : (K : Type u) → [Field K] → Type (max u (v + 1))
-- Mathlib.Data.Prod.TProd
/-- The product of a family of types over a list.  -/
List.TProd : {ι : Type u} → (ι → Type v) → List ι → Type v
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit!_cons : ∀ {α : Type u} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α fun x => Unit} {l : List α} {k : α},
  ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! t (k :: l)) =
    ↑(Std.DTreeMap.Internal.Impl.Const.insertManyIfNewUnit! (Std.DTreeMap.Internal.Impl.insertIfNew! k () t) l)
-- Std.Sync.Channel
_private.Std.Sync.Channel.0.Std.CloseableChannel.Consumer.select : {α : Type} → Std.Async.Waiter (Option α) → Std.CloseableChannel.Consumer✝ α
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.SimpKind.simp.sizeOf_spec : sizeOf Lean.Elab.Tactic.SimpKind.simp = 1
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.mergeWith : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ t₃ t₄ : Std.TreeMap α β cmp} [Std.TransCmp cmp]
  [Std.LawfulEqCmp cmp] (f : α → β → β → β),
  t₁.Equiv t₂ → t₃.Equiv t₄ → (Std.TreeMap.mergeWith f t₁ t₃).Equiv (Std.TreeMap.mergeWith f t₂ t₄)
-- Mathlib.Algebra.GroupWithZero.Hom
NeZero.of_map : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Zero α] [inst_1 : Zero β] [inst_2 : FunLike F α β]
  [ZeroHomClass F α β] {a : α} (f : F) [neZero : NeZero (f a)], NeZero a
-- Init.Data.BitVec.Lemmas
BitVec.msb_setWidth'' : ∀ {w k : ℕ} (x : BitVec w), (BitVec.setWidth (k + 1) x).msb = x.getLsbD k
-- Init.Data.UInt.Basic
instMulUInt32 : Mul UInt32
-- Mathlib.RingTheory.Length
Module.length.eq_1 : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Module.length R M = (Order.krullDim (Submodule R M)).unbot ⋯
-- Mathlib.Algebra.Category.Grp.FilteredColimits
AddGrpCat.FilteredColimits.colimit_add_mk_eq : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] [inst_1 : CategoryTheory.IsFiltered J]
  (F : CategoryTheory.Functor J AddGrpCat) (x y : (j : J) × ↑(F.obj j)) (k : J) (f : x.fst ⟶ k) (g : y.fst ⟶ k),
  AddGrpCat.FilteredColimits.G.mk F x + AddGrpCat.FilteredColimits.G.mk F y =
    AddGrpCat.FilteredColimits.G.mk F
      ⟨k, (CategoryTheory.ConcreteCategory.hom (F.map f)) x.snd + (CategoryTheory.ConcreteCategory.hom (F.map g)) y.snd⟩
-- Mathlib.Algebra.Ring.Basic
one_div_neg_one_eq_neg_one : ∀ {R : Type u_1} [inst : DivisionMonoid R] [inst_1 : HasDistribNeg R], 1 / -1 = -1
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_mul_expect : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_4} [inst : Semiring M] [inst_1 : Module ℚ≥0 M] [IsScalarTower ℚ≥0 M M]
  [SMulCommClass ℚ≥0 M M] (s : Finset ι) (t : Finset κ) (f : ι → M) (g : κ → M),
  ((s.expect fun i => f i) * t.expect fun j => g j) = s.expect fun i => t.expect fun j => f i * g j
-- Mathlib.Algebra.Module.DedekindDomain
/-- A finitely generated torsion module over a Dedekind domain is an internal direct sum of its
`p i ^ e i`-torsion submodules for some prime ideals `p i` and numbers `e i`.  -/
Submodule.exists_isInternal_prime_power_torsion : ∀ {R : Type u} [inst : CommRing R] [IsDedekindDomain R] {M : Type v} [inst_2 : AddCommGroup M] [inst_3 : Module R M]
  [Module.Finite R M],
  Module.IsTorsion R M →
    ∃ P x, ∃ (_ : ∀ p ∈ P, Prime p), ∃ e, DirectSum.IsInternal fun p => Submodule.torsionBySet R M ↑(↑p ^ e p)
-- ProofWidgets.Component.Panel.Basic
ProofWidgets.PanelWidgetProps.mk.injEq : ∀ (pos : Lean.Lsp.Position) (goals : Array Lean.Widget.InteractiveGoal)
  (termGoal? : Option Lean.Widget.InteractiveTermGoal) (selectedLocations : Array Lean.SubExpr.GoalsLocation)
  (pos_1 : Lean.Lsp.Position) (goals_1 : Array Lean.Widget.InteractiveGoal)
  (termGoal?_1 : Option Lean.Widget.InteractiveTermGoal) (selectedLocations_1 : Array Lean.SubExpr.GoalsLocation),
  ({ pos := pos, goals := goals, termGoal? := termGoal?, selectedLocations := selectedLocations } =
      { pos := pos_1, goals := goals_1, termGoal? := termGoal?_1, selectedLocations := selectedLocations_1 }) =
    (pos = pos_1 ∧ goals = goals_1 ∧ termGoal? = termGoal?_1 ∧ selectedLocations = selectedLocations_1)
-- Mathlib.Algebra.ContinuedFractions.Translations
_private.Mathlib.Algebra.ContinuedFractions.Translations.0.GenContFract.contsAux.match_1.eq_1 : ∀ {K : Type u_1} (motive : Option (GenContFract.Pair K) → Sort u_2) (h_1 : Unit → motive none)
  (h_2 : (gp : GenContFract.Pair K) → motive (some gp)),
  (match none with
    | none => h_1 ()
    | some gp => h_2 gp) =
    h_1 ()
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_id : ∀ {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.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (c : C) (d : D),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight c (CategoryTheory.CategoryStruct.id d) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj c d)
-- Init.System.CancelToken
/-- Checks whether the cancellation token has been activated.  -/
IO.CancelToken.isSet : IO.CancelToken → BaseIO Bool
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.le_radius_compContinuousLinearMap : ∀ {𝕜 : Type u_1} {E : Type u_3} {F : Type u_4} {G : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (p : FormalMultilinearSeries 𝕜 F G) (u : E →ₗᵢ[𝕜] F),
  p.radius ≤ (p.compContinuousLinearMap u.toContinuousLinearMap).radius
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.SplitMonoCategory.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C],
  (∀ {X Y : C} (f : X ⟶ Y) [CategoryTheory.Mono f], CategoryTheory.IsSplitMono f) → CategoryTheory.SplitMonoCategory C
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- The kernel of a linear map into a noetherian module is CoFG.  -/
Submodule.CoFG.ker : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [IsNoetherian R N] (f : M →ₗ[R] N), f.ker.CoFG
-- Mathlib.Analysis.Analytic.Constructions
HasFPowerSeriesOnBall.prod : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} {F : Type u_4} {G : Type u_5}
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] {e : E} {f : E → F} {g : E → G} {r s : ENNReal}
  {p : FormalMultilinearSeries 𝕜 E F} {q : FormalMultilinearSeries 𝕜 E G},
  HasFPowerSeriesOnBall f p e r →
    HasFPowerSeriesOnBall g q e s → HasFPowerSeriesOnBall (fun x => (f x, g x)) (p.prod q) e (min r s)
-- Init.Omega.Int
Lean.Omega.Prod.snd_mk : ∀ {α : Type u_1} {x : α} {α_1 : Type u_2} {y : α_1}, (x, y).2 = y
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.NonUnital
/-- The non-unital continuous functional calculus obtained by restricting a unital calculus
to functions that map zero to zero. This is an auxiliary definition and is not
intended for use outside this file. The equality between the non-unital and unital
calculi in this case is encoded in the lemma `cfcₙ_eq_cfc`.  -/
cfcₙHom_of_cfcHom : (R : Type u_1) →
  {A : Type u_2} →
    {p : A → Prop} →
      [inst : Semifield R] →
        [inst_1 : StarRing R] →
          [inst_2 : MetricSpace R] →
            [inst_3 : IsTopologicalSemiring R] →
              [inst_4 : ContinuousStar R] →
                [inst_5 : Ring A] →
                  [inst_6 : StarRing A] →
                    [inst_7 : TopologicalSpace A] →
                      [inst_8 : Algebra R A] →
                        [ContinuousFunctionalCalculus R A p] →
                          {a : A} → p a → ContinuousMapZero (↑(quasispectrum R a)) R →⋆ₙₐ[R] A
-- Mathlib.Analysis.SpecialFunctions.Complex.Arg
Complex.arg_mul_cos_add_sin_mul_I_eq_toIocMod : ∀ {r : ℝ},
  0 < r → ∀ (θ : ℝ), (↑r * (Complex.cos ↑θ + Complex.sin ↑θ * Complex.I)).arg = toIocMod Real.two_pi_pos (-Real.pi) θ
-- Mathlib.CategoryTheory.Limits.Shapes.Opposites.Pullbacks
CategoryTheory.Limits.PullbackCone.op_inr : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y Z : C} {f : X ⟶ Z} {g : Y ⟶ Z}
  (c : CategoryTheory.Limits.PullbackCone f g), c.op.inr = c.snd.op