mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Tactic.Grind.AC.Types
Lean.Meta.Grind.AC.DiseqCnstrProof.simp_exact.sizeOf_spec : ∀ (lhs : Bool) (c₁ : Lean.Meta.Grind.AC.EqCnstr) (c₂ : Lean.Meta.Grind.AC.DiseqCnstr),
  sizeOf (Lean.Meta.Grind.AC.DiseqCnstrProof.simp_exact lhs c₁ c₂) = 1 + sizeOf lhs + sizeOf c₁ + sizeOf c₂
-- Mathlib.Analysis.Analytic.Order
analyticOrderAt_smul_eq_top_of_right : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {g : 𝕜 → E} {z₀ : 𝕜} {f : 𝕜 → 𝕜}, analyticOrderAt g z₀ = ⊤ → analyticOrderAt (f • g) z₀ = ⊤
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.sdiff_subset_comm`. -/
Set.diff_subset_comm : ∀ {α : Type u_1} {s t u : Set α}, s \ t ⊆ u ↔ s \ u ⊆ t
-- Mathlib.Algebra.Star.StarAlgHom
/-- Reinterpret a unital star algebra homomorphism as a unital algebra homomorphism
by forgetting the interaction with the star operation.  -/
StarAlgHom.toAlgHom : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : Semiring A] →
          [inst_2 : Algebra R A] →
            [inst_3 : Star A] →
              [inst_4 : Semiring B] → [inst_5 : Algebra R B] → [inst_6 : Star B] → (A →⋆ₐ[R] B) → A →ₐ[R] B
-- Mathlib.Combinatorics.Enumerative.DyckWord
/-- Named in analogy to `Bool.dichotomy`.  -/
DyckStep.dichotomy : ∀ (s : DyckStep), s = DyckStep.U ∨ s = DyckStep.D
-- Std.Data.DTreeMap.Raw.Basic
/-- Folds the given monadic function over the mappings in the map in ascending order.  -/
Std.DTreeMap.Raw.foldlM : {α : Type u} →
  {β : α → Type v} →
    {cmp : α → α → Ordering} →
      {δ : Type w} → {m : Type w → Type w₂} → [Monad m] → (δ → (a : α) → β a → m δ) → δ → Std.DTreeMap.Raw α β cmp → m δ
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.ofCoeff_injective : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R], Function.Injective AddMonoidAlgebra.ofCoeff
-- Mathlib.CategoryTheory.WithTerminal.Basic
_private.Mathlib.CategoryTheory.WithTerminal.Basic.0.CategoryTheory.WithInitial.id.match_1.eq_1 : ∀ {C : Type u_1} (motive : CategoryTheory.WithInitial C → Sort u_2) (a : C)
  (h_1 : (a : C) → motive (CategoryTheory.WithInitial.of a)) (h_2 : Unit → motive CategoryTheory.WithInitial.star),
  (match CategoryTheory.WithInitial.of a with
    | CategoryTheory.WithInitial.of a => h_1 a
    | CategoryTheory.WithInitial.star => h_2 ()) =
    h_1 a
-- Init.Grind.Ring.Basic
Lean.Grind.Ring.toSemiring : {α : Type u} → [self : Lean.Grind.Ring α] → Lean.Grind.Semiring α
-- Init.Data.UInt.Lemmas
USize.toUInt64_neg : ∀ (a : USize), (-a).toUInt64 = -a.toUInt64 % UInt64.ofNat USize.size
-- Aesop.Builder.Forward
Aesop.RuleBuilder.forward : Bool → Aesop.RuleBuilder
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight_cons_zero : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {n : ℕ} (x : Fin n → K),
  Height.logHeight (Matrix.vecCons 0 x) = Height.logHeight x
-- Mathlib.Algebra.Order.ToIntervalMod
toIocMod_zero_sub_comm : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : LinearOrder α] [inst_2 : IsOrderedAddMonoid α] [hα : Archimedean α]
  {p : α} (hp : 0 < p) (a b : α), toIocMod hp 0 (a - b) = p - toIcoMod hp 0 (b - a)
-- Lean.Declaration
Lean.Declaration.thmDecl.injEq : ∀ (val val_1 : Lean.TheoremVal), (Lean.Declaration.thmDecl val = Lean.Declaration.thmDecl val_1) = (val = val_1)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVExpr.shiftLeft.injEq : ∀ {m n : ℕ} (lhs : Std.Tactic.BVDecide.BVExpr m) (rhs : Std.Tactic.BVDecide.BVExpr n) (n_1 : ℕ)
  (lhs_1 : Std.Tactic.BVDecide.BVExpr m) (rhs_1 : Std.Tactic.BVDecide.BVExpr n_1),
  (lhs.shiftLeft rhs = lhs_1.shiftLeft rhs_1) = (n = n_1 ∧ lhs = lhs_1 ∧ rhs ≍ rhs_1)
-- Mathlib.Algebra.Category.Grp.FiniteGrp
/-- The morphism in `FiniteGrp`, induced from a morphism of the category `GrpCat`.  -/
FiniteGrp.ofHom : {X Y : Type u} →
  [inst : Group X] →
    [inst_1 : Finite X] → [inst_2 : Group Y] → [inst_3 : Finite Y] → (X →* Y) → (FiniteGrp.of X ⟶ FiniteGrp.of Y)
-- Mathlib.NumberTheory.LucasLehmer
LucasLehmer.X.right_distrib : ∀ {q : ℕ} (x y z : LucasLehmer.X q), (x + y) * z = x * z + y * z
-- Mathlib.Analysis.Complex.CanonicalDecomposition
/-- Given a canonical decomposition `CanonicalDecomp f g R`, the function associated with the divisor of
`g` equals the function associated with the divisor of `f`, seen as a meromorphic function on the
sphere.
 -/
Complex.CanonicalDecomp.divisor_eq_divisor : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {R : ℝ} {f g : ℂ → E} {x : ℂ},
  Complex.CanonicalDecomp f g R →
    0 < R → (MeromorphicOn.divisor g (Metric.closedBall 0 R)) x = (MeromorphicOn.divisor f (Metric.sphere 0 R)) x
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.exists_lift : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A] {B : Type u_1}
  [inst_3 : CommRing B] [inst_4 : Algebra R B] [Algebra.FormallySmooth R A] (I : Ideal B),
  IsNilpotent I → ∀ (g : A →ₐ[R] B ⧸ I), ∃ f, (Ideal.Quotient.mkₐ R I).comp f = g
-- Mathlib.Analysis.Normed.Ring.WithAbs
/-- The canonical `R`-linear isomorphism between `WithAbs v` and `T`, when
`v : AbsoluteValue T S`.  -/
WithAbs.linearEquiv : {S : Type u_2} →
  [inst : Semiring S] →
    [inst_1 : PartialOrder S] →
      (R : Type u_3) →
        {T : Type u_4} →
          [inst_2 : Semiring R] →
            [inst_3 : Semiring T] → [inst_4 : Module R T] → (v : AbsoluteValue T S) → WithAbs v ≃ₗ[R] T
-- Mathlib.Algebra.Lie.Nilpotent
Function.Injective.lieModuleIsNilpotent : ∀ {R : Type u} {L : Type v} {M : Type w} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [LieModule R L M] {L₂ : Type u_1}
  {M₂ : Type u_2} [inst_7 : LieRing L₂] [inst_8 : LieAlgebra R L₂] [inst_9 : AddCommGroup M₂] [inst_10 : Module R M₂]
  [inst_11 : LieRingModule L₂ M₂] {f : L →ₗ⁅R⁆ L₂} {g : M →ₗ[R] M₂},
  (∀ (x : L) (m : M), ⁅f x, g m⁆ = g ⁅x, m⁆) →
    ∀ [LieModule R L₂ M₂], Function.Injective ⇑g → ∀ [LieModule.IsNilpotent L₂ M₂], LieModule.IsNilpotent L M
-- Mathlib.Algebra.Algebra.Hom
/-- **Alias** of `IsScalarTower.toAlgHom_apply`. -/
Algebra.algHom_apply : ∀ (R : Type u_1) (S : Type u_2) (A : Type u_3) [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Algebra R S] [inst_4 : Algebra S A] [inst_5 : Algebra R A] [inst_6 : IsScalarTower R S A] (y : S),
  (IsScalarTower.toAlgHom R S A) y = (algebraMap S A) y
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.instIsLieAbelianSubtypeLMemLieIdealKerProj : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [IsLieAbelian M] (E : LieAlgebra.Extension R M L),
  IsLieAbelian ↥E.proj.ker
-- Lean.Meta.Tactic.Grind.Extension
/-- Number of abstracted metavariable in the `rhs`  -/
Lean.Meta.Grind.CnstrRHS.numMVars : Lean.Meta.Grind.CnstrRHS → ℕ
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.tensorHom.eq_6 : ∀ {y₁ y₂ : AugmentedSimplexCategory} (f₁ : CategoryTheory.WithInitial.star ⟶ y₁)
  (f₂ : CategoryTheory.WithInitial.star ⟶ y₂),
  AugmentedSimplexCategory.tensorHom f₁ f₂ =
    match CategoryTheory.WithInitial.star, y₁, CategoryTheory.WithInitial.star, y₂, f₁, f₂ with
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, CategoryTheory.WithInitial.of a_2,
      CategoryTheory.WithInitial.of a_3, f₁, f₂ => AugmentedSimplexCategory.tensorHomOf f₁ f₂
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of y₁, CategoryTheory.WithInitial.star,
      CategoryTheory.WithInitial.of y₂, f₁, x =>
      CategoryTheory.CategoryStruct.comp f₁
        (CategoryTheory.CategoryStruct.comp (SimplexCategory.mkHom (Fin.castAddOrderEmb (y₂.len + 1)).toOrderHom)
          (CategoryTheory.eqToHom ⋯))
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of y₁, CategoryTheory.WithInitial.of a,
      CategoryTheory.WithInitial.of y₂, x, f₂ =>
      CategoryTheory.CategoryStruct.comp f₂
        (CategoryTheory.CategoryStruct.comp (SimplexCategory.mkHom (Fin.natAddOrderEmb (y₁.len + 1)).toOrderHom)
          (CategoryTheory.eqToHom ⋯))
    | CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.star, CategoryTheory.WithInitial.of a,
      CategoryTheory.WithInitial.of a_1, x, f₂ => f₂
    | CategoryTheory.WithInitial.of a, CategoryTheory.WithInitial.of a_1, CategoryTheory.WithInitial.star,
      CategoryTheory.WithInitial.star, f₁, x => f₁
    | CategoryTheory.WithInitial.star, x, CategoryTheory.WithInitial.star, x_1, x_2, x_3 =>
      CategoryTheory.WithInitial.starInitial.to (x.tensorObj x_1)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.mem_filter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Bool} {k : α},
  k ∈ Std.ExtDTreeMap.filter f t ↔ ∃ (h : k ∈ t), f k (t.get k h) = true
-- Mathlib.Data.Bundle
/-- `Bundle.TotalSpace.proj` is the canonical projection `Bundle.TotalSpace F E → B` from the
total space to the base space.  -/
Bundle.termπ__ : Lean.ParserDescr
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.minKeyD_insert_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, t.isEmpty = true → ∀ {fallback : α}, (t.insert k v).minKeyD fallback = k
-- Mathlib.Algebra.Category.Grp.Basic
GrpCat.hom_inv_apply : ∀ {X Y : GrpCat} (e : X ≅ Y) (s : ↑Y),
  (CategoryTheory.ConcreteCategory.hom e.hom) ((CategoryTheory.ConcreteCategory.hom e.inv) s) = s
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.Mor₂Iso.inv.sizeOf_spec : ∀ (e : Lean.Expr) (f g : Mathlib.Tactic.BicategoryLike.Mor₁) (η : Mathlib.Tactic.BicategoryLike.Mor₂Iso),
  sizeOf (Mathlib.Tactic.BicategoryLike.Mor₂Iso.inv e f g η) = 1 + sizeOf e + sizeOf f + sizeOf g + sizeOf η
-- Mathlib.CategoryTheory.Discrete.SumsProducts
CategoryTheory.Discrete.sumEquiv_counitIso_hom_app : ∀ {J : Type u_1} {K : Type u_2} (X : CategoryTheory.Discrete J ⊕ CategoryTheory.Discrete K),
  CategoryTheory.Discrete.sumEquiv.counitIso.hom.app X =
    (match X with
      | Sum.inl x => CategoryTheory.Iso.refl (Sum.inl x)
      | Sum.inr x => CategoryTheory.Iso.refl (Sum.inr x)).hom
-- Mathlib.CategoryTheory.SmallObject.TransfiniteCompositionLifting
CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : Type w} [inst_1 : LinearOrder J] [inst_2 : OrderBot J]
  {F : CategoryTheory.Functor J C} {c : CategoryTheory.Limits.Cocone F} {X Y : C} {p : X ⟶ Y} {f : F.obj ⊥ ⟶ X}
  {g : c.pt ⟶ Y} {j : J} [inst_3 : SizeOf C] [inst_4 : SizeOf J] (f' : F.obj j ⟶ X)
  (w₁ :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.homOfLE ⋯)) f' = f)
      CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₁._autoParam)
  (w₂ :
    autoParam (CategoryTheory.CategoryStruct.comp f' p = CategoryTheory.CategoryStruct.comp (c.ι.app j) g)
      CategoryTheory.HasLiftingProperty.transfiniteComposition.SqStruct.w₂._autoParam),
  sizeOf { f' := f', w₁ := w₁, w₂ := w₂ } = 1 + sizeOf f' + sizeOf w₁ + sizeOf w₂
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.card_rootsOfUnity : ∀ {R : Type u_4} [inst : CommRing R] [IsDomain R] {ζ : R} {n : ℕ} [NeZero n],
  IsPrimitiveRoot ζ n → Nat.card ↥(rootsOfUnity n R) = n
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.adjoin_singleton_algebraMap : ∀ {R : Type uR} (A : Type uA) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (x : R),
  R[(algebraMap R A) x] = ⊥
-- Lean.Elab.Tactic.RCases
_private.Lean.Elab.Tactic.RCases.0.Lean.Elab.Tactic.RCases.evalRCases : Lean.Elab.Tactic.Tactic
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instInvOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : Inv Mᵐᵒᵖ], DomMulAct.instInvOfMulOpposite = inst
-- Mathlib.Analysis.InnerProductSpace.PiL2
EuclideanSpace.dist_sq_eq : ∀ {𝕜 : Type u_7} [inst : RCLike 𝕜] {n : Type u_8} [inst_1 : Fintype n] (x y : EuclideanSpace 𝕜 n),
  dist x y ^ 2 = ∑ i, dist (x.ofLp i) (y.ofLp i) ^ 2
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.orderTop.eq_1 : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] (x : HahnSeries Γ R),
  x.orderTop = if h : x = 0 then ⊤ else ↑(⋯.min ⋯)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get_diff : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] (h₁ : t₁.WF) (h₂ : t₂.WF) {k : α} {h_mem : k ∈ t₁ \ t₂},
  (t₁ \ t₂).get k h_mem = t₁.get k ⋯
-- Mathlib.NumberTheory.GaussSum
/-- We have `gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = Fintype.card R`
when `χ` is nontrivial and `ψ` is primitive (and `R` is a field).  -/
gaussSum_mul_gaussSum_eq_card : ∀ {R : Type u} [inst : Field R] [inst_1 : Fintype R] {R' : Type v} [inst_2 : CommRing R'] [IsDomain R']
  {χ : MulChar R R'}, χ ≠ 1 → ∀ {ψ : AddChar R R'}, ψ.IsPrimitive → gaussSum χ ψ * gaussSum χ⁻¹ ψ⁻¹ = ↑(Fintype.card R)
-- Mathlib.Algebra.Lie.Basic
LieEquiv.hasCoeToLieHom : {R : Type u} →
  {L₁ : Type v} →
    {L₂ : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L₁] →
          [inst_2 : LieRing L₂] →
            [inst_3 : LieAlgebra R L₁] → [inst_4 : LieAlgebra R L₂] → Coe (L₁ ≃ₗ⁅R⁆ L₂) (L₁ →ₗ⁅R⁆ L₂)
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Implementation
Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula.clauses : {numVarsSucc : ℕ} →
  Std.Tactic.BVDecide.LRAT.Internal.DefaultFormula numVarsSucc →
    Array (Option (Std.Tactic.BVDecide.LRAT.Internal.DefaultClause numVarsSucc))
-- Mathlib.Algebra.Ring.InjSurj
/-- A type endowed with `0`, `1` and `+` is an additive monoid with one,
if it admits an injective map that preserves `0`, `1` and `+` to an additive monoid with one.
See note [reducible non-instances].  -/
Function.Injective.addMonoidWithOne : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Add S] →
      [inst_1 : Zero S] →
        [inst_2 : One S] →
          [inst_3 : SMul ℕ S] →
            [inst_4 : NatCast S] →
              [inst_5 : AddMonoidWithOne R] →
                (f : S → R) →
                  Function.Injective f →
                    f 0 = 0 →
                      f 1 = 1 →
                        (∀ (x y : S), f (x + y) = f x + f y) →
                          (∀ (n : ℕ) (x : S), f (n • x) = n • f x) → (∀ (n : ℕ), f ↑n = ↑n) → AddMonoidWithOne S
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- Composition of a square between left adjoints with a conjugate square.  -/
CategoryTheory.Bicategory.leftAdjointSquareConjugate.vcomp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d : B} →
      {g : a ⟶ c} →
        {h : b ⟶ d} →
          {l₁ : a ⟶ b} →
            {l₂ l₃ : c ⟶ d} →
              (CategoryTheory.CategoryStruct.comp g l₂ ⟶ CategoryTheory.CategoryStruct.comp l₁ h) →
                (l₃ ⟶ l₂) → (CategoryTheory.CategoryStruct.comp g l₃ ⟶ CategoryTheory.CategoryStruct.comp l₁ h)
-- Mathlib.CategoryTheory.Category.Factorisation
CategoryTheory.Factorisation.terminal_mid : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y},
  CategoryTheory.Factorisation.terminal.mid = Y
-- Mathlib.Data.Finsupp.Single
Finsupp.update_idem : ∀ {α : Type u_1} {M : Type u_5} [inst : Zero M] (f : α →₀ M) (a : α) (b c : M), (f.update a b).update a c = f.update a c
-- Init.Internal.Order.Basic
Lean.Order.fun_sup : {α : Sort u} →
  {β : α → Sort v} → [(x : α) → Lean.Order.CompleteLattice (β x)] → (((x : α) → β x) → Prop) → (x : α) → β x
-- Mathlib.Algebra.Group.Subgroup.Finite
/-- **Alias** of `AddSubgroup.val_finsetSum`. -/
AddSubgroup.val_finset_sum : ∀ {ι : Type u_3} {G : Type u_4} [inst : AddCommGroup G] (H : AddSubgroup G) (f : ι → ↥H) (s : Finset ι),
  ↑(∑ i ∈ s, f i) = ∑ i ∈ s, ↑(f i)
-- Mathlib.Combinatorics.Matroid.IndepAxioms
Matroid.ofExistsFiniteIsBase.congr_simp : ∀ {α : Type u_1} (E E_1 : Set α) (e_E : E = E_1) (IsBase IsBase_1 : Set α → Prop) (e_IsBase : IsBase = IsBase_1)
  (exists_finite_base : ∃ B, IsBase B ∧ B.Finite) (isBase_exchange : Matroid.ExchangeProperty IsBase)
  (subset_ground : ∀ (B : Set α), IsBase B → B ⊆ E),
  Matroid.ofExistsFiniteIsBase E IsBase exists_finite_base isBase_exchange subset_ground =
    Matroid.ofExistsFiniteIsBase E_1 IsBase_1 ⋯ ⋯ ⋯
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.ShiftRight
Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (distance : ℕ)
  (input : aig.RefVec w) (curr : ℕ) (hcurr : curr ≤ w) (s : aig.RefVec curr) (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 :
    idx < (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance curr hcurr s).aig.decls.size),
  (Std.Tactic.BVDecide.BVExpr.bitblast.blastShiftRightConst.go aig input distance curr hcurr s).aig.decls[idx] =
    aig.decls[idx]
-- Mathlib.Topology.MetricSpace.IsometricSMul
/-- **Alias** of `Metric.preimage_smul_eball`. -/
EMetric.preimage_smul_ball : ∀ {G : Type v} {X : Type w} [inst : PseudoEMetricSpace X] [inst_1 : Group G] [inst_2 : MulAction G X]
  [IsIsometricSMul G X] (c : G) (x : X) (r : ENNReal), (fun x => c • x) ⁻¹' Metric.eball x r = Metric.eball (c⁻¹ • x) r
-- Mathlib.Topology.Compactness.Compact
Filter.mem_cocompact : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X}, s ∈ Filter.cocompact X ↔ ∃ t, IsCompact t ∧ tᶜ ⊆ s
-- Lean.Elab.MutualInductive
/-- Elaborated header for an inductive type before fvars for each inductive are added to the local context.  -/
Lean.Elab.Command.PreElabHeaderResult : Type
-- Lean.Declaration
Lean.mkInductiveValEx : Lean.Name →
  List Lean.Name → Lean.Expr → ℕ → ℕ → List Lean.Name → List Lean.Name → ℕ → Bool → Bool → Bool → Lean.InductiveVal
-- Mathlib.Algebra.Lie.Weights.Linear
LieModule.Weight.apply_lie : ∀ {R : Type u_2} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [LieModule.LinearWeights R L M] {χ : LieModule.Weight R L M} (x y : L), χ ⁅x, y⁆ = 0
-- Init.Core
of_toBoolUsing_eq_false : ∀ {p : Prop} {d : Decidable p}, toBoolUsing d = false → ¬p
-- Mathlib.Geometry.Euclidean.MongePoint
/-- The Monge point of an (n+2)-simplex, minus the centroid of an
n-dimensional face, in terms of `pointsWithCircumcenter`.  -/
Affine.Simplex.mongePoint_vsub_face_centroid_eq_weightedVSub_of_pointsWithCircumcenter : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P (n + 2)) {i₁ i₂ : Fin (n + 3)},
  i₁ ≠ i₂ →
    s.mongePoint -ᵥ Finset.centroid ℝ {i₁, i₂}ᶜ s.points =
      (Finset.univ.weightedVSub s.pointsWithCircumcenter)
        (Affine.Simplex.mongePointVSubFaceCentroidWeightsWithCircumcenter i₁ i₂)
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
Subalgebra.isIntegral_iff : ∀ {R : Type u_1} {B : Type u_3} [inst : CommRing R] [inst_1 : Ring B] [inst_2 : Algebra R B] (S : Subalgebra R B),
  Algebra.IsIntegral R ↥S ↔ ∀ x ∈ S, IsIntegral R x
-- Mathlib.CategoryTheory.Filtered.Final
/-- If `C` is cofiltered, then we can give an explicit condition for a functor `F : C ⥤ D` to
be initial.  -/
CategoryTheory.Functor.initial_iff_of_isCofiltered : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsCofilteredOrEmpty C],
  F.Initial ↔
    (∀ (d : D), ∃ c, Nonempty (F.obj c ⟶ d)) ∧
      ∀ {d : D} {c : C} (s s' : F.obj c ⟶ d),
        ∃ c' t, CategoryTheory.CategoryStruct.comp (F.map t) s = CategoryTheory.CategoryStruct.comp (F.map t) s'
-- Mathlib.Algebra.Module.Submodule.Basic
Submodule.neg_coe : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] {module_M : Module R M} (p : Submodule R M),
  -↑p = ↑p
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
measurableSet_mem_finset : ∀ {α : Type u_1} (a : α), MeasurableSet {s | a ∈ s}
-- Mathlib.Data.Prod.Basic
Prod.fst_eq_iff : ∀ {α : Type u_1} {β : Type u_2} {p : α × β} {x : α}, p.1 = x ↔ p = (x, p.2)
-- Mathlib.Data.Seq.Basic
/-- The statement of `length_le_iff'` does not assume that the sequence terminates. For a
simpler statement of the theorem where the sequence is known to terminate see `length_le_iff`.  -/
Stream'.Seq.length_le_iff' : ∀ {α : Type u} {s : Stream'.Seq α} {n : ℕ}, (∃ (h : s.Terminates), s.length h ≤ n) ↔ s.TerminatedAt n
-- Mathlib.GroupTheory.GroupAction.SubMulAction.OfFixingSubgroup
/-- The identity between the `SubAddAction`s of `fixingAddSubgroup`s
of equal sets, as an equivariant map.  -/
SubAddAction.ofFixingAddSubgroup_of_eq : (M : Type u_1) →
  {α : Type u_2} →
    [inst : AddGroup M] →
      [inst_1 : AddAction M α] →
        {s t : Set α} →
          (hst : s = t) →
            have φ := AddEquiv.addSubgroupCongr ⋯;
            ↥(SubAddAction.ofFixingAddSubgroup M s) →ₑ[⇑φ] ↥(SubAddAction.ofFixingAddSubgroup M t)
-- Mathlib.RingTheory.FractionalIdeal.Operations
FractionalIdeal.le_self_mul_one_div : ∀ {R₁ : Type u_3} [inst : CommRing R₁] {K : Type u_4} [inst_1 : Field K] [inst_2 : Algebra R₁ K]
  [inst_3 : IsFractionRing R₁ K] [inst_4 : IsDomain R₁] {I : FractionalIdeal (nonZeroDivisors R₁) K},
  I ≤ 1 → I ≤ I * (1 / I)
-- Mathlib.MeasureTheory.Measure.Stieltjes
StieltjesFunction.eq_of_measure_of_eq : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R)
  [inst_2 : OrderTopology R] [inst_3 : CompactIccSpace R] [inst_4 : MeasurableSpace R] [inst_5 : BorelSpace R]
  [inst_6 : SecondCountableTopology R] [inst_7 : DenselyOrdered R] (g : StieltjesFunction R) {y : R},
  f.measure = g.measure → ↑f y = ↑g y → f = g
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Mapping from variables to their disequalities. We say a disequality constraint `c` is a disequality for a variable `x`
if `x` is the maximal variable in `c`.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.diseqs : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.DiseqCnstr)
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.SimplyConnected
isSimplyConnected_smul_set₀_iff : ∀ {X : Type u_1} [inst : TopologicalSpace X] {G : Type u_3} [inst_1 : GroupWithZero G] [inst_2 : MulAction G X]
  [ContinuousConstSMul G X] {c : G} {s : Set X}, c ≠ 0 → (IsSimplyConnected (c • s) ↔ IsSimplyConnected s)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.mem_supportSet_iff_mem_support : ∀ {X : AlgebraicGeometry.Scheme} {I : X.IdealSheafData} {x : ↥X}, x ∈ I.supportSet ↔ x ∈ I.support
-- Mathlib.Analysis.Meromorphic.Basic
MeromorphicOn.eventually_codiscreteWithin_analyticAt : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {U : Set 𝕜} [CompleteSpace E] (f : 𝕜 → E),
  MeromorphicOn f U → ∀ᶠ (y : 𝕜) in Filter.codiscreteWithin U, AnalyticAt 𝕜 f y
-- Mathlib.AlgebraicTopology.SimplexCategory.Augmented.Monoidal
AugmentedSimplexCategory.tensorHom.eq_5 : ∀ (a a_1 : SimplexCategory) (f₁_2 : CategoryTheory.WithInitial.of a ⟶ CategoryTheory.WithInitial.of a_1)
  (x : CategoryTheory.WithInitial.star ⟶ CategoryTheory.WithInitial.star),
  AugmentedSimplexCategory.tensorHom f₁_2 x = f₁_2
-- Mathlib.Analysis.Normed.Field.Lemmas
tendsto_zpow_nhdsNE_zero_cobounded : ∀ {α : Type u_1} [inst : NormedDivisionRing α] {m : ℤ},
  m < 0 → Filter.Tendsto (fun x => x ^ m) (nhdsWithin 0 {0}ᶜ) (Bornology.cobounded α)
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.CtorInfo.mk.sizeOf_spec : ∀ (name : Lean.Name) (cidx size usize ssize : ℕ),
  sizeOf { name := name, cidx := cidx, size := size, usize := usize, ssize := ssize } =
    1 + sizeOf name + sizeOf cidx + sizeOf size + sizeOf usize + sizeOf ssize
-- Mathlib.Order.Filter.TendstoCofinite
Filter.tendstoCofinite_of_finite : ∀ {α : Type u_1} {β : Type u_2} (f : α → β) [Finite α], Filter.TendstoCofinite f