mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Analytic.CPolynomialDef
HasFiniteFPowerSeriesAt.eventually : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {p : FormalMultilinearSeries 𝕜 E F} {x : E} {n : ℕ},
  HasFiniteFPowerSeriesAt f p x n → ∀ᶠ (r : ENNReal) in nhdsWithin 0 (Set.Ioi 0), HasFiniteFPowerSeriesOnBall f p x n r
-- Std.Sync.CancellationToken
/-- Checks if the token is cancelled.
 -/
Std.CancellationToken.isCancelled : Std.CancellationToken → BaseIO Bool
-- Mathlib.RingTheory.Norm.Transitivity
Algebra.norm_eq_prod_automorphisms : ∀ {L : Type u_6} (K : Type u_7) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : FiniteDimensional K L] [IsGalois K L] (x : L), (algebraMap K L) ((Algebra.norm K) x) = ∏ σ, σ x
-- Std.Time.Date.Unit.Month
Std.Time.Month.Ordinal.difference_eq : ∀ {leap : Bool} {month : Std.Time.Month.Ordinal} (p : ↑month ≤ 11),
  have next :=
    (Std.Time.Internal.Bounded.LE.truncateTop month p).addTop 1 Std.Time.Month.Ordinal.difference_eq._proof_1;
  (Std.Time.Month.Ordinal.cumulativeDays leap next).val =
    (Std.Time.Month.Ordinal.cumulativeDays leap month).val + ↑(Std.Time.Month.Ordinal.days leap month)
-- Mathlib.Analysis.InnerProductSpace.LinearMap
/-- The inner product as a continuous sesquilinear map. Note that `toDualMap` (resp. `toDual`)
in `InnerProductSpace.Dual` is a version of this given as a linear isometry (resp. linear
isometric equivalence).  -/
innerSL : (𝕜 : Type u_1) →
  {E : Type u_2} →
    [inst : RCLike 𝕜] → [inst_1 : SeminormedAddCommGroup E] → [inst_2 : InnerProductSpace 𝕜 E] → E →L⋆[𝕜] E →L[𝕜] 𝕜
-- Mathlib.Algebra.Order.Monoid.Unbundled.Pow
instIsMulTorsionFreeOfMulLeftStrictMonoOfMulRightStrictMono : ∀ {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftStrictMono M] [MulRightStrictMono M],
  IsMulTorsionFree M
-- Mathlib.Topology.Algebra.RestrictedProduct.TopologicalSpace
RestrictedProduct.instContinuousMulCoePrincipal : ∀ {ι : Type u_1} (R : ι → Type u_2) {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)] {B : (i : ι) → S i}
  {T : Set ι} [inst_1 : (i : ι) → TopologicalSpace (R i)] [inst_2 : (i : ι) → Mul (R i)]
  [inst_3 : ∀ (i : ι), MulMemClass (S i) (R i)] [∀ (i : ι), ContinuousMul (R i)],
  ContinuousMul (RestrictedProduct (fun i => R i) (fun i => ↑(B i)) (Filter.principal T))
-- Mathlib.Topology.Algebra.InfiniteSum.ConditionalInt
SummationFilter.hasProd_symmetricIcc_iff : ∀ {α : Type u_2} [inst : CommMonoid α] [inst_1 : TopologicalSpace α] {f : ℤ → α} {a : α},
  HasProd f a (SummationFilter.symmetricIcc ℤ) ↔
    Filter.Tendsto (fun N => ∏ n ∈ Finset.Icc (-↑N) ↑N, f n) Filter.atTop (nhds a)
-- Lean.Data.Lsp.Basic
Lean.Lsp.instToJsonWorkDoneProgressBegin.toJson : Lean.Lsp.WorkDoneProgressBegin → Lean.Json
-- Std.Data.DTreeMap.Internal.Model
_private.Std.Data.DTreeMap.Internal.Model.0.Std.DTreeMap.Internal.Impl.Const.maxEntry?.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (Unit → motive Std.DTreeMap.Internal.Impl.leaf) →
          ((size : ℕ) →
              (k : α) →
                (v : β) →
                  (l : Std.DTreeMap.Internal.Impl α fun x => β) →
                    motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf)) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (l : Std.DTreeMap.Internal.Impl α fun x => β) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β) →
                            (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) →
                              motive
                                (Std.DTreeMap.Internal.Impl.inner size k v l
                                  (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r))) →
              motive x
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.derivative_X_add_C_sq : ∀ {R : Type u} [inst : CommSemiring R] (c : R),
  Polynomial.derivative ((Polynomial.X + Polynomial.C c) ^ 2) = Polynomial.C 2 * (Polynomial.X + Polynomial.C c)
-- Mathlib.Algebra.Homology.QuasiIso
quasiIso_iff : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  [inst_2 : ∀ (i : ι), K.HasHomology i] [inst_3 : ∀ (i : ι), L.HasHomology i], QuasiIso f ↔ ∀ (i : ι), QuasiIsoAt f i
-- Mathlib.Topology.UniformSpace.Compact
/-- If `K` is a compact set in a uniform space and `{V i | p i}` is a basis of entourages,
then `{⋃ x ∈ K, UniformSpace.ball x (V i) | p i}` is a basis of `𝓝ˢ K`.

Here "`{s i | p i}` is a basis of a filter `l`" means `Filter.HasBasis l p s`.  -/
IsCompact.nhdsSet_basis_uniformity : ∀ {α : Type ua} {ι : Sort u_1} [inst : UniformSpace α] {K : Set α} {p : ι → Prop} {V : ι → Set (α × α)},
  (uniformity α).HasBasis p V → IsCompact K → (nhdsSet K).HasBasis p fun i => ⋃ x ∈ K, UniformSpace.ball x (V i)
-- Mathlib.GroupTheory.Perm.MaximalSubgroups
MulAction.IsBlock.subsingleton_of_ssubset_of_stabilizer_le : ∀ {M : Type u_1} {α : Type u_2} [inst : Group M] [inst_1 : MulAction M α] {s B : Set α},
  B ⊂ s → MulAction.IsBlock M B → Function.Surjective MulAction.toPerm → B.Subsingleton
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.getKeyD_ofList_of_contains_eq_false : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [Std.TransCmp cmp] [inst : BEq α] [Std.LawfulBEqCmp cmp]
  {l : List ((a : α) × β a)} {k fallback : α},
  (List.map Sigma.fst l).contains k = false → (Std.DTreeMap.ofList l cmp).getKeyD k fallback = fallback
-- Mathlib.Analysis.CStarAlgebra.Multiplier
/-- The type of *double centralizers*, also known as the *multiplier algebra* and denoted by
`𝓜(𝕜, A)`, of a non-unital normed algebra.

If `x : 𝓜(𝕜, A)`, then `x.fst` and `x.snd` are what is usually referred to as $L$ and $R$.  -/
DoubleCentralizer : (𝕜 : Type u) →
  (A : Type v) →
    [inst : NontriviallyNormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] → [SMulCommClass 𝕜 A A] → [IsScalarTower 𝕜 A A] → Type v
-- Mathlib.Topology.ContinuousOn
Topology.IsEmbedding.map_nhdsWithin_eq : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  Topology.IsEmbedding f → ∀ (s : Set α) (x : α), Filter.map f (nhdsWithin x s) = nhdsWithin (f x) (f '' s)
-- Mathlib.Topology.FiberBundle.Trivialization
Bundle.Pretrivialization.symm_apply_mk_proj : ∀ {B : Type u_1} {F : Type u_2} {Z : Type u_4} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F] {proj : Z → B}
  (e : Bundle.Pretrivialization F proj) {x : Z}, x ∈ e.source → ↑e.symm (proj x, (↑e x).2) = x
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.eq_one_or_neg_one_of_mem_support_of_smul_mem : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} (b : P.Base)
  [CharZero R] [Finite ι] [IsAddTorsionFree M] [IsAddTorsionFree N],
  ∀ i ∈ b.support, ∀ (t : R), t • P.root i ∈ Set.range ⇑P.root → t = 1 ∨ t = -1
-- Mathlib.CategoryTheory.Presentable.Basic
CategoryTheory.Functor.instIsCardinalAccessibleOfPreservesColimitsOfSize : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (κ : Cardinal.{w}) [inst_2 : Fact κ.IsRegular]
  [CategoryTheory.Limits.PreservesColimitsOfSize.{w, w, v₁, v₂, u₁, u₂} F], F.IsCardinalAccessible κ
-- Std.Data.DTreeMap.Raw.Basic
Std.DTreeMap.Raw.mk.injEq : ∀ {α : Type u} {β : α → Type v} {_cmp : autoParam (α → α → Ordering) Std.DTreeMap.Raw._auto_1}
  (inner inner_1 : Std.DTreeMap.Internal.Impl α β), ({ inner := inner } = { inner := inner_1 }) = (inner = inner_1)
-- Mathlib.Data.Fintype.OfMap
/-- Any subsingleton type with a witness is a fintype (with one term).  -/
Fintype.ofSubsingleton : {α : Type u_1} → α → [Subsingleton α] → Fintype α
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getElem!_empty : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : Inhabited β] {a : α}, ∅[a]! = default
-- Mathlib.Algebra.FreeMonoid.Basic
/-- Equivalence between maps `α → A` and additive monoid homomorphisms
`FreeAddMonoid α →+ A`.  -/
FreeAddMonoid.lift : {α : Type u_1} → {M : Type u_4} → [inst : AddMonoid M] → (α → M) ≃ (FreeAddMonoid α →+ M)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.post_forget_eq_forget_comp : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor T D) (X : T),
  (CategoryTheory.Under.post F).comp (CategoryTheory.Under.forget (F.obj X)) = (CategoryTheory.Under.forget X).comp F
-- Mathlib.Data.Finset.Defs
Finset.val_strictMono : ∀ {α : Type u_1}, StrictMono Finset.val
-- Mathlib.Analysis.Analytic.ConvergenceRadius
FormalMultilinearSeries.div_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 →L[𝕜] F),
  p.radius / ‖u‖ₑ ≤ (p.compContinuousLinearMap u).radius
-- Batteries.Recycling.RBTree.WF
RBTree.RBNode.reverse_balLeft : ∀ {α : Type u_1} (l : RBTree.RBNode α) (v : α) (r : RBTree.RBNode α),
  (l.balLeft v r).reverse = r.reverse.balRight v l.reverse
-- Mathlib.RingTheory.RingInvo
/-- Construct a ring involution from a ring homomorphism.  -/
RingInvo.mk' : {R : Type u_2} →
  [inst : Semiring R] → (f : R →+* Rᵐᵒᵖ) → (∀ (r : R), MulOpposite.unop (f (MulOpposite.unop (f r))) = r) → RingInvo R
-- Mathlib.Algebra.Order.SuccPred.TypeTags
instIsSuccArchimedeanMultiplicative : ∀ {X : Type u_1} [inst : Preorder X] [inst_1 : SuccOrder X] [h : IsSuccArchimedean X],
  IsSuccArchimedean (Multiplicative X)
-- Mathlib.Topology.Path
Path.map_map : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x y : X} (γ : Path x y)
  {Z : Type u_4} [inst_2 : TopologicalSpace Z] {f : X → Y} (hf : Continuous f) {g : Y → Z} (hg : Continuous g),
  (γ.map hf).map hg = γ.map ⋯
-- Mathlib.Analysis.InnerProductSpace.Basic
Real.inner_apply : ∀ (x y : ℝ), inner ℝ x y = x * y
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.interface : Lean.Lsp.SymbolKind
-- Mathlib.Data.Set.Basic
Set.sep_eq_inter_sep : ∀ {α : Type u_1} {s t : Set α} {p : α → Prop}, s ⊆ t → {x | x ∈ s ∧ p x} = s ∩ {x | x ∈ t ∧ p x}
-- Std.Time.Date.Unit.Year
Std.Time.Year.instReprOffset : Repr Std.Time.Year.Offset
-- Lean.Meta.SynthInstance
/-- Target type has metavariables, and class has output parameters.  -/
_private.Lean.Meta.SynthInstance.0.Lean.Meta.PreprocessKind.mvarsOutputParams : Lean.Meta.PreprocessKind✝
-- Mathlib.NumberTheory.NumberField.Units.DirichletTheorem
NumberField.Units.instFreeIntAdditiveQuotientUnitsRingOfIntegersSubgroupTorsion : ∀ (K : Type u_1) [inst : Field K] [NumberField K],
  Module.Free ℤ (Additive ((NumberField.RingOfIntegers K)ˣ ⧸ NumberField.Units.torsion K))
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.core.inj : ∀ {a b : Lean.Expr} {ra rb : Lean.Grind.CommRing.Expr} {a_1 b_1 : Lean.Expr} {ra_1 rb_1 : Lean.Grind.CommRing.Expr},
  Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.core a b ra rb =
      Lean.Meta.Grind.Arith.Linear.RingEqCnstrProof.core a_1 b_1 ra_1 rb_1 →
    a = a_1 ∧ b = b_1 ∧ ra = ra_1 ∧ rb = rb_1
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.equiv_iff_keysArray_perm : ∀ {α : Type u} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => Unit}, t₁.Equiv t₂ ↔ t₁.keysArray.Perm t₂.keysArray
-- Mathlib.MeasureTheory.Measure.Typeclasses.SFinite
/-- If the union of disjoint measurable sets has finite measure, then there are only
countably many members of the union whose measure is positive.  -/
MeasureTheory.Measure.countable_meas_pos_of_disjoint_of_meas_iUnion_ne_top : ∀ {α : Type u_1} {ι : Type u_4} {x : MeasurableSpace α} (μ : MeasureTheory.Measure α) {As : ι → Set α},
  (∀ (i : ι), MeasurableSet (As i)) →
    Pairwise (Function.onFun Disjoint As) → μ (⋃ i, As i) ≠ ⊤ → {i | 0 < μ (As i)}.Countable
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.hasLimitsOfShape_iff_isLeftAdjoint_const : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C],
  CategoryTheory.Limits.HasLimitsOfShape J C ↔ (CategoryTheory.Functor.const J).IsLeftAdjoint
-- Mathlib.CategoryTheory.LiftingProperties.Basic
CategoryTheory.HasLiftingProperty.of_comp_left : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {A B B' X Y : C} (i : A ⟶ B) (i' : B ⟶ B') (p : X ⟶ Y)
  [CategoryTheory.HasLiftingProperty i p] [CategoryTheory.HasLiftingProperty i' p],
  CategoryTheory.HasLiftingProperty (CategoryTheory.CategoryStruct.comp i i') p
-- Init.Data.Rat.Lemmas
Rat.divInt_eq_div : ∀ (a b : ℤ), Rat.divInt a b = ↑a / ↑b
-- Mathlib.Data.Analysis.Filter
CFilter.f : {α : Type u_1} → {σ : Type u_2} → [inst : PartialOrder α] → CFilter α σ → σ → α
-- Mathlib.Algebra.GroupWithZero.Defs
mul_inv_cancel₀ : ∀ {G₀ : Type u} [inst : GroupWithZero G₀] {a : G₀}, a ≠ 0 → a * a⁻¹ = 1
-- Mathlib.Topology.Inseparable
SeparationQuotient.continuous_lift₂ : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y → Z}
  {hf : ∀ (a : X) (b : Y) (c : X) (d : Y), Inseparable a c → Inseparable b d → f a b = f c d},
  Continuous (Function.uncurry (SeparationQuotient.lift₂ f hf)) ↔ Continuous (Function.uncurry f)
-- Mathlib.Algebra.Order.Module.Defs
smul_neg_iff_of_neg_left : ∀ {α : Type u_1} {β : Type u_2} {a : α} {b : β} [inst : Ring α] [inst_1 : PartialOrder α] [IsOrderedRing α]
  [inst_3 : AddCommGroup β] [inst_4 : PartialOrder β] [IsOrderedAddMonoid β] [inst_6 : Module α β]
  [PosSMulStrictMono α β] [PosSMulReflectLT α β], a < 0 → (a • b < 0 ↔ 0 < b)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE_ι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.natTransTruncLTOfLE a b h).app X) ((t.truncLTι b).app X) = (t.truncLTι a).app X
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getElem?_insert_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β}, (t.insert k v)[k]? = some v
-- Mathlib.RingTheory.Congruence.Basic
/-- The smallest congruence relation containing a binary relation `r` is contained in any
congruence relation containing `r`.  -/
RingCon.ringConGen_le : ∀ {R : Type u_3} [inst : Add R] [inst_1 : Mul R] {r : R → R → Prop} {c : RingCon R}, ringConGen r ≤ c ↔ r ≤ ⇑c
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
Submodule.toNonUnitalSubalgebra_toSubmodule : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A] [inst_2 : Module R A]
  (p : Submodule R A) (h_mul : ∀ (x y : A), x ∈ p → y ∈ p → x * y ∈ p), (p.toNonUnitalSubalgebra h_mul).toSubmodule = p
-- Init.Core
/-- The result of casting a term with `cast` is heterogeneously equal to the original term.
 -/
cast_heq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≍ a
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Affine
/-- If three points are not collinear, the sine of the angle between them is nonzero.  -/
EuclideanGeometry.sin_ne_zero_of_not_collinear : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {p₁ p₂ p₃ : P},
  ¬Collinear ℝ {p₁, p₂, p₃} → Real.sin (EuclideanGeometry.angle p₁ p₂ p₃) ≠ 0
-- Mathlib.Algebra.Order.AbsoluteValue.Basic
/-- Bound `abv (a + b)` from below  -/
AbsoluteValue.le_add : ∀ {R : Type u_3} {S : Type u_4} [inst : CommRing S] [inst_1 : PartialOrder S] [IsOrderedRing S] [inst_3 : Ring R]
  (abv : AbsoluteValue R S) [NoZeroDivisors S] (a b : R), abv a - abv b ≤ abv (a + b)
-- Mathlib.Topology.Algebra.Group.Basic
Filter.Tendsto.sub_const : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : Sub G] [ContinuousSub G] {c : G} {f : α → G}
  {l : Filter α}, Filter.Tendsto f l (nhds c) → ∀ (b : G), Filter.Tendsto (fun x => f x - b) l (nhds (c - b))
-- Init.Data.UInt.IntToBitVec
USize.toBitVec32_sub : ∀ {a b : USize} (h : System.Platform.numBits = 32), (a - b).toBitVec32 h = a.toBitVec32 h - b.toBitVec32 h
-- Init.Data.BitVec.Folds
BitVec.iunfoldr.fst_eq : ∀ {w : ℕ} {α : Type u_1} {f : Fin w → α → α × Bool} (state : ℕ → α) (s : α),
  s = state 0 → (∀ (i : Fin w), (f i (state ↑i)).1 = state (↑i + 1)) → (BitVec.iunfoldr f s).1 = state w
-- Mathlib.GroupTheory.OrderOfElement
/-- The image of an element of finite order has finite order.  -/
MonoidHom.isOfFinOrder : ∀ {G : Type u_1} {H : Type u_2} [inst : Monoid G] [inst_1 : Monoid H] (f : G →* H) {x : G},
  IsOfFinOrder x → IsOfFinOrder (f x)
-- Init.Data.Nat.Lemmas
Nat.mul_dvd_mul_iff_right : ∀ {a b c : ℕ}, 0 < c → (a * c ∣ b * c ↔ a ∣ b)
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
CategoryTheory.CardinalDirectedPoset.instIsCardinalFilteredElemCarrierObjPartOrdEmbIsCardinalFilteredValSetPropSet : ∀ {κ : Cardinal.{u}} [inst : Fact κ.IsRegular] (J : CategoryTheory.CardinalDirectedPoset κ) (S : Subtype J.PropSet),
  CategoryTheory.IsCardinalFiltered (↑↑S) κ
-- Mathlib.Algebra.Ring.Action.Rat
Rat.instIsScalarTowerRight : ∀ {R : Type u_1} [inst : DivisionRing R], IsScalarTower ℚ R R
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Clz
Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (x : aig.RefVec w) (curr : ℕ)
  (acc : aig.RefVec w),
  Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go aig x curr acc =
    if hc : curr < w then
      let lhs := Std.Tactic.BVDecide.BVExpr.bitblast.blastConst aig (↑w - 1 - ↑curr);
      let res := Std.Sat.AIG.RefVec.ite aig { discr := x.get curr hc, lhs := lhs, rhs := acc };
      let aig_1 := res.aig;
      have acc_1 := res.vec;
      have this := ⋯;
      have x := x.cast this;
      Std.Tactic.BVDecide.BVExpr.bitblast.blastClz.go aig_1 x (curr + 1) acc_1
    else { aig := aig, vec := acc }
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.singleZeroRingHom.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] [inst_1 : AddZeroClass M],
  AddMonoidAlgebra.singleZeroRingHom =
    { toFun := (↑(AddMonoidAlgebra.singleAddHom 0)).toFun, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Roots
_private.Mathlib.RingTheory.Polynomial.Cyclotomic.Roots.0.Polynomial.isRoot_cyclotomic_iff' : ∀ {n : ℕ} {K : Type u_2} [inst : Field K] {μ : K} [NeZero ↑n],
  (Polynomial.cyclotomic n K).IsRoot μ ↔ IsPrimitiveRoot μ n
-- Init.Data.Int.Linear
Int.Internal.Linear.OrOver.eq_def : ∀ (n : ℕ) (p : ℕ → Prop),
  Int.Internal.Linear.OrOver n p =
    match n with
    | 0 => False
    | n.succ => p n ∨ Int.Internal.Linear.OrOver n p
-- Mathlib.Algebra.Ring.Periodic
Function.Periodic.const_inv_smul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {f : α → β} {c : α} [inst : AddMonoid α] [inst_1 : Group γ]
  [inst_2 : DistribMulAction γ α], Function.Periodic f c → ∀ (a : γ), Function.Periodic (fun x => f (a⁻¹ • x)) (a • c)
-- Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect
_private.Init.Data.Iterators.Lemmas.Consumers.Monadic.Collect.0.Std.IterM.toListRev.match_1.eq_2 : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Std.Iterator α m β] (it : Std.IterM m β)
  (motive : it.Step → Sort u_3) (it' : Std.IterM m β) (h : it.IsPlausibleStep (Std.IterStep.skip it'))
  (h_1 :
    (it' : Std.IterM m β) →
      (out : β) → (h : it.IsPlausibleStep (Std.IterStep.yield it' out)) → motive ⟨Std.IterStep.yield it' out, h⟩)
  (h_2 : (it' : Std.IterM m β) → (h : it.IsPlausibleStep (Std.IterStep.skip it')) → motive ⟨Std.IterStep.skip it', h⟩)
  (h_3 : (property : it.IsPlausibleStep Std.IterStep.done) → motive ⟨Std.IterStep.done, property⟩),
  (match ⟨Std.IterStep.skip it', h⟩ with
    | ⟨Std.IterStep.yield it' out, h⟩ => h_1 it' out h
    | ⟨Std.IterStep.skip it', h⟩ => h_2 it' h
    | ⟨Std.IterStep.done, property⟩ => h_3 property) =
    h_2 it' h
-- Mathlib.Analysis.RCLike.Basic
RCLike.conj_ofReal : ∀ {K : Type u_1} [inst : RCLike K] (r : ℝ), (starRingEnd K) ↑r = ↑r
-- Mathlib.Analysis.Normed.Ring.Basic
/-- An injective non-unital ring homomorphism from a `CommRing` to a `NormedRing` induces a
`NormedCommRing` structure on the domain.

See note [reducible non-instances]  -/
NormedCommRing.induced : {F : Type u_5} →
  (R : Type u_6) →
    (S : Type u_7) →
      [inst : FunLike F R S] →
        [inst_1 : CommRing R] →
          [inst_2 : NormedRing S] → [NonUnitalRingHomClass F R S] → (f : F) → Function.Injective ⇑f → NormedCommRing R
-- Mathlib.Algebra.Group.ULift
ULift.mul.eq_1 : ∀ {α : Type u} [inst : Mul α], ULift.mul = { mul := fun f g => { down := f.down * g.down } }
-- Mathlib.SetTheory.Ordinal.Notation
_private.Mathlib.SetTheory.Ordinal.Notation.0.ONote.fastGrowing.match_1.eq_2 : ∀ (o : ONote) (motive : (x : Option ONote ⊕ (ℕ → ONote)) → o.FundamentalSequenceProp x → Sort u_1) (a : ONote)
  (h : o.FundamentalSequenceProp (Sum.inl (some a)))
  (h_1 : (x : o.FundamentalSequenceProp (Sum.inl none)) → motive (Sum.inl none) x)
  (h_2 : (a : ONote) → (h : o.FundamentalSequenceProp (Sum.inl (some a))) → motive (Sum.inl (some a)) h)
  (h_3 : (f : ℕ → ONote) → (h : o.FundamentalSequenceProp (Sum.inr f)) → motive (Sum.inr f) h),
  (match Sum.inl (some a), h with
    | Sum.inl none, x => h_1 x
    | Sum.inl (some a), h => h_2 a h
    | Sum.inr f, h => h_3 f h) =
    h_2 a h
-- Mathlib.Algebra.Group.Units.Basic
isUnit_of_subsingleton : ∀ {M : Type u_1} [inst : Monoid M] [Subsingleton M] (a : M), IsUnit a
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.domLCongr_trans : ∀ (R : Type u_1) [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (N : Type u_3)
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] (ι : Type u_7) {M₂ : Type u_10} [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂] {M₃ : Type u_11} [inst_7 : AddCommMonoid M₃] [inst_8 : Module R M₃] (S : Type u_12)
  [inst_9 : Semiring S] [inst_10 : Module S N] [inst_11 : SMulCommClass R S N] (e : M ≃ₗ[R] M₂) (f : M₂ ≃ₗ[R] M₃),
  AlternatingMap.domLCongr R N ι S e ≪≫ₗ AlternatingMap.domLCongr R N ι S f = AlternatingMap.domLCongr R N ι S (e ≪≫ₗ f)
-- Mathlib.RingTheory.Ideal.Operations
Ideal.IsPrime.multiset_prod_mem_iff_exists_mem : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R}, I.IsPrime → ∀ (s : Multiset R), s.prod ∈ I ↔ ∃ p ∈ s, p ∈ I
-- Mathlib.Algebra.Category.Ring.Colimits
RingCat.Colimits.Relation.below.one_mul : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J RingCat}
  {motive : (a a_1 : RingCat.Colimits.Prequotient F) → RingCat.Colimits.Relation F a a_1 → Prop}
  (x : RingCat.Colimits.Prequotient F), RingCat.Colimits.Relation.below ⋯
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
_private.Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap.0.List.filterMap.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Init.Data.List.Lemmas
List.append_eq_filter_iff : ∀ {α : Type u_1} {L₁ L₂ l : List α} {p : α → Bool},
  L₁ ++ L₂ = List.filter p l ↔ ∃ l₁ l₂, l = l₁ ++ l₂ ∧ List.filter p l₁ = L₁ ∧ List.filter p l₂ = L₂