mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.MorphismProperty.OverAdjunction
/-- `Under.map` commutes with composition.  -/
CategoryTheory.MorphismProperty.Under.mapComp : {T : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} T] →
    {P : CategoryTheory.MorphismProperty T} →
      (Q : CategoryTheory.MorphismProperty T) →
        [inst_1 : Q.IsMultiplicative] →
          {X Y Z : T} →
            [inst_2 : P.IsStableUnderComposition] →
              {f : X ⟶ Y} →
                (hf : P f) →
                  {g : Y ⟶ Z} →
                    (hg : P g) →
                      [Q.RespectsIso] →
                        (fg : optParam (X ⟶ Z) (CategoryTheory.CategoryStruct.comp f g)) →
                          (hfg :
                              autoParam (fg = CategoryTheory.CategoryStruct.comp f g)
                                CategoryTheory.MorphismProperty.Under.mapComp._auto_1) →
                            CategoryTheory.MorphismProperty.Under.map Q ⋯ ≅
                              (CategoryTheory.MorphismProperty.Under.map Q hg).comp
                                (CategoryTheory.MorphismProperty.Under.map Q hf)
-- Lean.Compiler.IR.Basic
Lean.IR.LocalContextEntry.joinPoint.inj : ∀ {a : Array Lean.IR.Param} {a_1 : Lean.IR.FnBody} {a_2 : Array Lean.IR.Param} {a_3 : Lean.IR.FnBody},
  Lean.IR.LocalContextEntry.joinPoint a a_1 = Lean.IR.LocalContextEntry.joinPoint a_2 a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.im_neg : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : AddGroup R], (-a).im = -a.im
-- Mathlib.Order.Filter.Basic
Filter.principal_le_iff : ∀ {α : Type u} {s : Set α} {f : Filter α}, Filter.principal s ≤ f ↔ ∀ V ∈ f, s ⊆ V
-- Mathlib.Algebra.Group.Hom.Defs
ZeroHom.id_comp : ∀ {M : Type u_4} {N : Type u_5} [inst : Zero M] [inst_1 : Zero N] (f : ZeroHom M N), (ZeroHom.id N).comp f = f
-- Mathlib.Topology.Compactness.Paracompact
instParacompactSpaceProdOfCompactSpace_1 : ∀ {X : Type v} {Y : Type w} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] [ParacompactSpace X]
  [CompactSpace Y], ParacompactSpace (X × Y)
-- Mathlib.Order.Filter.Pointwise
Filter.mulActionFilter.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Monoid α] [inst_1 : MulAction α β],
  Filter.mulActionFilter = { toSMul := Filter.instSMulFilter, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Data.ZMod.Basic
ZMod.inv_mul_eq_one_of_isUnit : ∀ {n : ℕ} {a : ZMod n}, IsUnit a → ∀ (b : ZMod n), a⁻¹ * b = 1 ↔ a = b
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.mul_inv_rev : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (G : C) [inst_3 : CategoryTheory.GrpObj G],
  CategoryTheory.CategoryStruct.comp CategoryTheory.MonObj.mul CategoryTheory.GrpObj.inv =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategoryStruct.tensorHom CategoryTheory.GrpObj.inv CategoryTheory.GrpObj.inv)
      (CategoryTheory.CategoryStruct.comp (β_ G G).hom CategoryTheory.MonObj.mul)
-- Mathlib.Topology.Algebra.ContinuousAffineEquiv
ContinuousAffineEquiv.coe_symm_toAffineEquiv : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {V₁ : Type u_6} {V₂ : Type u_7} [inst : Ring k]
  [inst_1 : AddCommGroup V₁] [inst_2 : Module k V₁] [inst_3 : AddTorsor V₁ P₁] [inst_4 : TopologicalSpace P₁]
  [inst_5 : AddCommGroup V₂] [inst_6 : Module k V₂] [inst_7 : AddTorsor V₂ P₂] [inst_8 : TopologicalSpace P₂]
  (e : P₁ ≃ᴬ[k] P₂), ⇑(↑e).symm = ⇑e.symm
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.forall_mem_iff_forall_contains_getKey_getValue : ∀ {α : Type u} [inst : BEq α] [EquivBEq α] {β : Type v} {l : List ((_ : α) × β)} {p : α → β → Prop},
  Std.Internal.List.DistinctKeys l →
    ((∀ x ∈ l, p x.fst x.snd) ↔
      ∀ (a : α) (h : Std.Internal.List.containsKey a l = true),
        p (Std.Internal.List.getKey a l h) (Std.Internal.List.getValue a l h))
-- Mathlib.Data.Set.Sigma
Set.union_sigma : ∀ {ι : Type u_1} {α : ι → Type u_3} {s₁ s₂ : Set ι} {t : (i : ι) → Set (α i)},
  (s₁ ∪ s₂).sigma t = s₁.sigma t ∪ s₂.sigma t
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.ApproximatesLinearOn
ApproximatesLinearOn.antilipschitz : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {f' : E ≃L[𝕜] F} {s : Set E} {c : NNReal},
  ApproximatesLinearOn f (↑f') s c →
    Subsingleton E ∨ c < ‖↑f'.symm‖₊⁻¹ → AntilipschitzWith (‖↑f'.symm‖₊⁻¹ - c)⁻¹ (s.domRestrict f)
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
/-- Reorder a product.

The difference with `Finset.prod_nbij` is that the bijection is specified with an inverse, rather
than as a surjective injection.

The difference with `Finset.prod_bij'` is that the bijection and its inverse are non-dependent
functions, rather than being allowed to use membership of the domains of the products.

The difference with `Finset.prod_equiv` is that bijectivity is only required to hold on the domains
of the products, rather than on the entire types.
 -/
Finset.prod_nbij' : ∀ {ι : Type u_1} {κ : Type u_2} {M : Type u_3} [inst : CommMonoid M] {s : Finset ι} {t : Finset κ} {f : ι → M}
  {g : κ → M} (i : ι → κ) (j : κ → ι),
  (∀ a ∈ s, i a ∈ t) →
    (∀ a ∈ t, j a ∈ s) →
      (∀ a ∈ s, j (i a) = a) → (∀ a ∈ t, i (j a) = a) → (∀ a ∈ s, f a = g (i a)) → ∏ x ∈ s, f x = ∏ x ∈ t, g x
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Periodic
AddCircle.measurable_mk' : ∀ {a : ℝ}, Measurable QuotientAddGroup.mk
-- Mathlib.Topology.Category.TopCat.Monoidal
TopCat.ι₀_comp : ∀ {X Y : TopCat} (f : X ⟶ Y),
  CategoryTheory.CategoryStruct.comp TopCat.ι₀ (CategoryTheory.MonoidalCategoryStruct.whiskerRight f TopCat.I) =
    CategoryTheory.CategoryStruct.comp f TopCat.ι₀
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
PseudoMetricSpace.replaceBornology_eq : ∀ {α : Type u_3} [m : PseudoMetricSpace α] [B : Bornology α]
  (H : ∀ (s : Set α), Bornology.IsBounded s ↔ Bornology.IsBounded s), m.replaceBornology H = m
-- Mathlib.CategoryTheory.Monoidal.Braided.Basic
CategoryTheory.op_inv_braiding : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] (X Y : C), (β_ X Y).inv.op = (β_ (Opposite.op Y) (Opposite.op X)).inv
-- Mathlib.CategoryTheory.Functor.KanExtension.DenseAt
/-- If `F : C ⥤ D` is dense at `Y : D`, then so is `G ⋙ F` if
the canonical functor `CostructuredArrow (G ≫ F) Y ⥤ CostructuredArrow F Y` is final.
This holds in particular if `G` is an equivalence.  -/
CategoryTheory.Functor.DenseAt.precompOfFinal : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {Y : D} →
            F.DenseAt Y →
              {C' : Type u_1} →
                [inst_2 : CategoryTheory.Category.{v_1, u_1} C'] →
                  (G : CategoryTheory.Functor C' C) →
                    [(CategoryTheory.CostructuredArrow.pre G F Y).Final] → (G.comp F).DenseAt Y
-- Init.Data.UInt.BasicAux
BitVec.ofNat.eq_1 : ∀ (n i : ℕ), BitVec.ofNat n i = { toFin := Fin.Internal.ofNat (2 ^ n) ⋯ i }
-- Mathlib.RingTheory.AdjoinRoot
AdjoinRoot.lift_root : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] {f : Polynomial R} [inst_1 : CommRing S] {i : R →+* S} {a : S}
  (h : Polynomial.eval₂ i a f = 0), (AdjoinRoot.lift i a h) (AdjoinRoot.root f) = a
-- Std.Tactic.BVDecide.Normalize.BitVec
Std.Tactic.BVDecide.Normalize.Int64.toBitVec_cond : ∀ {c : Bool} {t e : Int64}, (bif c then t else e).toBitVec = bif c then t.toBitVec else e.toBitVec
-- Std.Sat.AIG.RelabelNat
_private.Std.Sat.AIG.RelabelNat.0.Std.Sat.AIG.relabelNat'.match_1.splitter : (motive : Option ℕ → Sort u_1) → (x : Option ℕ) → ((var : ℕ) → motive (some var)) → (Unit → motive none) → motive x
-- Mathlib.MeasureTheory.Measure.AEMeasurable
/-- A characterization of the a.e.-measurability of the indicator function which takes a constant
value `b` on a set `A` and `0` elsewhere.  -/
aemeasurable_indicator_const_iff : ∀ {α : Type u_2} {β : Type u_3} {m0 : MeasurableSpace α} [inst : MeasurableSpace β] {μ : MeasureTheory.Measure α}
  [inst_1 : Zero β] {s : Set α} [MeasurableSingletonClass β] (b : β) [NeZero b],
  AEMeasurable (s.indicator fun x => b) μ ↔ MeasureTheory.NullMeasurableSet s μ
-- Init.Data.BitVec.Lemmas
BitVec.toInt_append : ∀ {n m : ℕ} {x : BitVec n} {y : BitVec m},
  (x ++ y).toInt = if (n == 0) = true then y.toInt else 2 ^ m * x.toInt + ↑y.toNat
-- Init.System.IO
IO.instMaxTaskState : Max IO.TaskState
-- Std.Sync.Mutex
/-- Unlocks a `BaseMutex`.

The current thread must have already locked the mutex.
Unlocking an unlocked mutex is undefined behavior (inherited from the C++ implementation).
If this is unavoidable in your code, consider using `BaseRecursiveMutex`.
 -/
Std.BaseMutex.unlock : Std.BaseMutex → BaseIO Unit
-- Mathlib.Data.List.Enum
List.exists_mem_zipIdx : ∀ {α : Type u_1} {l : List α} {n : ℕ} {p : α × ℕ → Prop},
  (∃ x ∈ l.zipIdx n, p x) ↔ ∃ i, ∃ (x : i < l.length), p (l[i], n + i)
-- Mathlib.Data.Nat.Digits.Defs
Nat.digitsAux.eq_2 : ∀ (b : ℕ) (h : 2 ≤ b) (n : ℕ), b.digitsAux h n.succ = (n + 1) % b :: b.digitsAux h ((n + 1) / b)
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.mk.inj : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} {carrier : TopCat} {presheaf : TopCat.Presheaf C carrier}
  {carrier_1 : TopCat} {presheaf_1 : TopCat.Presheaf C carrier_1},
  { carrier := carrier, presheaf := presheaf } = { carrier := carrier_1, presheaf := presheaf_1 } →
    carrier = carrier_1 ∧ presheaf ≍ presheaf_1
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.LeftExtension.postcomp₁_obj_right_map : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} {D' : Type u_5} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  [inst_3 : CategoryTheory.Category.{v_5, u_5} D'] {L : CategoryTheory.Functor C D} {L' : CategoryTheory.Functor C D'}
  (G : CategoryTheory.Functor D D') (f : L' ⟶ L.comp G) (F : CategoryTheory.Functor C H)
  (X :
    CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit F) ((CategoryTheory.Functor.whiskeringLeft C D' H).obj L'))
  {X_1 Y : D} (f_1 : X_1 ⟶ Y),
  ((CategoryTheory.Functor.LeftExtension.postcomp₁ G f F).obj X).right.map f_1 = X.right.map (G.map f_1)
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey_eq_iff_getKey?_eq_self_and_forall : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  {he : t.isEmpty = false} {km : α}, t.minKey he = km ↔ t.getKey? km = some km ∧ ∀ k ∈ t, (cmp km k).isLE = true
-- Mathlib.Computability.Reduce
_private.Mathlib.Computability.Reduce.0.«term_⊕'__1» : Lean.TrailingParserDescr
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.AddMon.Hom.hom_add : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {M N : CategoryTheory.AddMon C}
  [inst_3 : CategoryTheory.IsCommAddMonObj N.X] (f g : M ⟶ N), (f + g).hom = f.hom + g.hom
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.instAddGroup : {R : Type u_1} → {a b : R} → [AddGroup R] → AddGroup (QuadraticAlgebra R a b)
-- Mathlib.Analysis.Complex.ReImTopology
/-- `Complex.re` turns `ℂ` into a trivial topological fiber bundle over `ℝ`.  -/
Complex.isHomeomorphicTrivialFiberBundle_re : IsHomeomorphicTrivialFiberBundle ℝ Complex.re
-- Mathlib.Algebra.CharP.Defs
ringExpChar.eq_1 : ∀ (R : Type u_1) [inst : NonAssocSemiring R], ringExpChar R = max (ringChar R) 1
-- Mathlib.Algebra.Group.Subgroup.Lattice
AddSubgroup.notMem_of_notMem_closure : ∀ {G : Type u_1} [inst : AddGroup G] {k : Set G} {P : G}, P ∉ AddSubgroup.closure k → P ∉ k
-- Mathlib.CategoryTheory.Limits.Elements
/-- (implementation) The constructed limit cone is a limit cone.  -/
CategoryTheory.CategoryOfElements.CreatesLimitsAux.isLimit : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor C (Type w)} →
      {I : Type u₁} →
        [inst_1 : CategoryTheory.Category.{v₁, u₁} I] →
          [inst_2 : Small.{w, u₁} I] →
            (F : CategoryTheory.Functor I A.Elements) →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape I C] →
                [inst_4 : CategoryTheory.Limits.PreservesLimitsOfShape I A] →
                  CategoryTheory.Limits.IsLimit (CategoryTheory.CategoryOfElements.CreatesLimitsAux.liftedCone F)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.card_add_singleton : ∀ {α : Type u_2} [inst : Add α] [IsRightCancelAdd α] [inst_2 : DecidableEq α] (s : Finset α) (a : α),
  (s + {a}).card = s.card
-- Mathlib.CategoryTheory.Limits.Sifted
CategoryTheory.IsSifted.nonempty_of_colim_preservesLimitsOfShapeFinZero : ∀ (C : Type u) [inst : CategoryTheory.SmallCategory C]
  [CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete (Fin 0)) CategoryTheory.Limits.colim],
  Nonempty C
-- Mathlib.LinearAlgebra.Matrix.Charpoly.LinearMap
PiToModule.fromEnd_apply : ∀ {ι : Type u_1} [inst : Fintype ι] {M : Type u_2} [inst_1 : AddCommGroup M] (R : Type u_3) [inst_2 : CommRing R]
  [inst_3 : Module R M] (b : ι → M) (f : Module.End R M) (w : ι → R),
  ((PiToModule.fromEnd R b) f) w = f ((Fintype.linearCombination R b) w)
-- Mathlib.Algebra.GroupWithZero.Units.Basic
/-- Constructs a `GroupWithZero` structure on a `MonoidWithZero`
consisting only of units and 0.  -/
groupWithZeroOfIsUnitOrEqZero : {M : Type u_4} → [Nontrivial M] → [hM : MonoidWithZero M] → (∀ (a : M), IsUnit a ∨ a = 0) → GroupWithZero M
-- Mathlib.Topology.Category.LightProfinite.Basic
lightDiagramToProfinite_map : ∀ {X Y : CategoryTheory.InducedCategory Profinite LightDiagram.toProfinite} (f : X ⟶ Y),
  lightDiagramToProfinite.map f = f.hom
-- Mathlib.GroupTheory.Perm.Cycle.Type
Equiv.Perm.cycleType_one : ∀ {α : Type u_1} [inst : Fintype α] [inst_1 : DecidableEq α], Equiv.Perm.cycleType 1 = 0
-- Mathlib.MeasureTheory.MeasurableSpace.CountablyGenerated
/-- If a measurable space is countably generated and separates points, it is measure equivalent
to some subset of the Cantor space `ℕ → Bool` (equipped with the product sigma algebra).
Note: `s` need not be measurable, so this map need not be a `MeasurableEmbedding` to
the Cantor Space.  -/
MeasurableSpace.measurableEquiv_nat_bool_of_countablyGenerated : ∀ (α : Type u_1) [inst : MeasurableSpace α] [MeasurableSpace.CountablyGenerated α] [MeasurableSpace.SeparatesPoints α],
  ∃ s, Nonempty (α ≃ᵐ ↑s)
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- The monad used by the certificate-chaining evaluator  -/
Mathlib.Tactic.Determinant.CertM : {u : Lean.Level} → {α : Q(Type u)} → Q(CommRing «$α») → Type → Type
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.get?_empty : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {a : α}, ∅.get? a = none
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.of_forall_getKey_eq_of_forall_constGet?_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  (∀ (k : α) (hk : k ∈ m₁) (hk' : k ∈ m₂), m₁.getKey k hk = m₂.getKey k hk') →
    (∀ (k : α), Std.DHashMap.Const.get? m₁ k = Std.DHashMap.Const.get? m₂ k) → m₁.Equiv m₂
-- Mathlib.Analysis.SpecialFunctions.Pow.NthRootLemmas
Nat.nthRoot.go.eq_1 : ∀ (n a x : ℕ), Nat.nthRoot.go n a 0 x = x
-- Mathlib.Analysis.SpecialFunctions.Pow.Deriv
DifferentiableOn.const_cpow : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] {f : E → ℂ} {s : Set E} {c : ℂ},
  DifferentiableOn ℂ f s → (c ≠ 0 ∨ ∀ x ∈ s, f x ≠ 0) → DifferentiableOn ℂ (fun x => c ^ f x) s
-- Mathlib.GroupTheory.Perm.Cycle.Factors
/-- The auxiliary of `cycleFactorsAux`. This functions separates cycles from `f` instead of `g`
to prevent the process of a cycle gets complex.  -/
Equiv.Perm.cycleFactorsAux.go : {α : Type u_2} →
  [inst : DecidableEq α] →
    [inst_1 : Fintype α] →
      (f : Equiv.Perm α) →
        (l : List α) →
          (g : Equiv.Perm α) →
            (∀ {x : α}, g x ≠ x → x ∈ l) →
              (∀ {x : α}, g x ≠ x → f.cycleOf x = g.cycleOf x) →
                { pl // pl.prod = g ∧ (∀ g' ∈ pl, g'.IsCycle) ∧ List.Pairwise Equiv.Perm.Disjoint pl }
-- Mathlib.Algebra.Ring.Shrink
Shrink.instNonUnitalRing : {α : Type u_1} → [inst : Small.{v, u_1} α] → [NonUnitalRing α] → NonUnitalRing (Shrink.{v, u_1} α)
-- Mathlib.Topology.UniformSpace.Completion
CauchyFilter.basis_uniformity : ∀ {α : Type u} [inst : UniformSpace α] {ι : Sort u_1} {p : ι → Prop} {s : ι → SetRel α α},
  (uniformity α).HasBasis p s → (uniformity (CauchyFilter α)).HasBasis p (CauchyFilter.gen ∘ s)
-- Mathlib.Algebra.ContinuedFractions.Computation.Translations
_private.Mathlib.Algebra.ContinuedFractions.Computation.Translations.0.Stream'.Seq.map.match_1.splitter : {α : Type u_1} →
  (motive : Stream'.Seq α → Sort u_2) →
    (x : Stream'.Seq α) → ((s : Stream' (Option α)) → (al : s.IsSeq) → motive ⟨s, al⟩) → motive x
-- Std.Tactic.BVDecide.Syntax
/-- Close fixed-width `BitVec` and `Bool` goals by obtaining a proof from an external SAT solver and
verifying it inside Lean. The solvable goals are currently limited to
- the Lean equivalent of [`QF_BV`](https://smt-lib.org/logics-all.shtml#QF_BV)
- automatically splitting up `structure`s that contain information about `BitVec` or `Bool`
```lean
example : ∀ (a b : BitVec 64), (a &&& b) + (a ^^^ b) = a ||| b := by
  intros
  bv_decide
```

If `bv_decide` encounters an unknown definition it will be treated like an unconstrained `BitVec`
variable. Sometimes this enables solving goals despite not understanding the definition because
the precise properties of the definition do not matter in the specific proof.

If `bv_decide` fails to close a goal it provides a counter-example, containing assignments for all
terms that were considered as variables.

In order to avoid calling a SAT solver every time, the proof can be cached with `bv_decide?`.

If solving your problem relies inherently on using associativity or commutativity, consider enabling
the `bv.ac_nf` option.

Note: `bv_decide` trusts the correctness of the code generator and adds a axioms asserting its result.

Note: include `import Std.Tactic.BVDecide`
 -/
Lean.Parser.Tactic.bvDecide : Lean.ParserDescr
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- If `prodComparison F A B` is an isomorphism, then `F` preserves the limit of `pair A B`.  -/
CategoryTheory.CartesianMonoidalCategory.preservesLimit_pair_of_isIso_prodComparison : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) (A B : C)
  [CategoryTheory.IsIso (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.pair A B) F
-- Mathlib.LinearAlgebra.StdBasis
/-- Let `k` be an integral domain and `G` an arbitrary finite set.
Then any algebra morphism `φ : (G → k) →ₐ[k] k` is an evaluation map.  -/
AlgHom.eq_piEvalAlgHom : ∀ {k : Type u_1} {G : Type u_2} [inst : CommSemiring k] [NoZeroDivisors k] [Nontrivial k] [Finite G]
  (φ : (G → k) →ₐ[k] k), ∃ s, φ = Pi.evalAlgHom k (fun i => k) s
-- Mathlib.CategoryTheory.Adjunction.Mates
CategoryTheory.conjugateEquiv_symm_apply_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L₁ L₂ : CategoryTheory.Functor C D} {R₁ R₂ : CategoryTheory.Functor D C} (adj₁ : L₁ ⊣ R₁) (adj₂ : L₂ ⊣ R₂)
  (a : R₁ ⟶ R₂) (X : C),
  ((CategoryTheory.conjugateEquiv adj₁ adj₂).symm a).app X =
    CategoryTheory.CategoryStruct.comp (L₂.map (adj₁.unit.app X))
      (CategoryTheory.CategoryStruct.comp (L₂.map (a.app (L₁.obj X))) (adj₂.counit.app (L₁.obj X)))
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
ContinuousLinearMap.coe_restrict_apply : ∀ {R₁ : Type u_1} {R₂ : Type u_2} [inst : Semiring R₁] [inst_1 : Semiring R₂] {σ₁₂ : R₁ →+* R₂} {M₁ : Type u_4}
  {M₂ : Type u_5} [inst_2 : TopologicalSpace M₁] [inst_3 : AddCommMonoid M₁] [inst_4 : Module R₁ M₁]
  [inst_5 : TopologicalSpace M₂] [inst_6 : AddCommMonoid M₂] [inst_7 : Module R₂ M₂] {f : M₁ →SL[σ₁₂] M₂}
  {p : Submodule R₁ M₁} {q : Submodule R₂ M₂} (hf : ∀ x ∈ p, f x ∈ q) (x : ↥p), ↑((f.restrict hf) x) = f ↑x
-- Std.Data.DHashMap.Basic
/-- Creates a hash map from an array of mappings. If the same key appears multiple times, the last
occurrence takes precedence.  -/
Std.DHashMap.ofArray : {α : Type u} → {β : α → Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Array ((a : α) × β a) → Std.DHashMap α β
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.face_upper : ∀ {n : ℕ} (I : BoxIntegral.Box (Fin (n + 1))) (i : Fin (n + 1)) (a : Fin n),
  (I.face i).upper a = I.upper (i.succAbove a)
-- Mathlib.RingTheory.WittVector.Verschiebung
WittVector.verschiebungPoly_zero : WittVector.verschiebungPoly 0 = 0
-- Mathlib.Probability.Martingale.Upcrossing
MeasureTheory.le_sub_of_le_upcrossingsBefore : ∀ {Ω : Type u_1} {a b : ℝ} {f : ℕ → Ω → ℝ} {N n : ℕ} {ω : Ω},
  0 < N →
    a < b →
      n < MeasureTheory.upcrossingsBefore a b f N ω →
        b - a ≤
          MeasureTheory.stoppedValue f (fun ω => ↑(MeasureTheory.upperCrossingTime a b f N (n + 1) ω)) ω -
            MeasureTheory.stoppedValue f (fun ω => ↑(MeasureTheory.lowerCrossingTime a b f N n ω)) ω
-- Lean.Data.Trie
Lean.Data.Trie.node1.injEq : ∀ {α : Type} (a : Option α) (a_1 : UInt8) (a_2 : Lean.Data.Trie α) (a_3 : Option α) (a_4 : UInt8)
  (a_5 : Lean.Data.Trie α),
  (Lean.Data.Trie.node1 a a_1 a_2 = Lean.Data.Trie.node1 a_3 a_4 a_5) = (a = a_3 ∧ a_1 = a_4 ∧ a_2 = a_5)
-- Mathlib.Analysis.LocallyConvex.Polar
StrongDual.polar_empty : ∀ (𝕜 : Type u_4) [inst : NontriviallyNormedField 𝕜] {E : Type u_5} [inst_1 : AddCommMonoid E]
  [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E], StrongDual.polar 𝕜 ∅ = Set.univ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getD_alter_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {fallback : β k} {f : Option (β k) → Option (β k)}, (m.alter k f).getD k fallback = (f (m.get? k)).getD fallback
-- Mathlib.NumberTheory.RamificationInertia.Unramified
/-- In characteristic zero, the zero ideal is unramified in an integral domain extension.  -/
Algebra.isUnramifiedIn_bot : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [IsDomain R]
  [IsDomain S] [FaithfulSMul R S] [CharZero R] [Algebra.IsIntegral R S], Algebra.IsUnramifiedIn S ⊥
-- Mathlib.Data.List.Cycle
Cycle.nontrivial_coe_nodup_iff : ∀ {α : Type u_1} {l : List α}, l.Nodup → ((↑l).Nontrivial ↔ 2 ≤ l.length)
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
CategoryTheory.StrictlyUnitaryPseudofunctor.mapId_eq_eqToIso : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictlyUnitaryPseudofunctor B C) (X : B), self.mapId X = CategoryTheory.eqToIso ⋯
-- Mathlib.Order.Hom.Set
/-- Sets on sum types are order-equivalent to pairs of sets on each summand.  -/
Set.sumEquiv : {α : Type u_1} → {β : Type u_2} → Set (α ⊕ β) ≃o Set α × Set β
-- Mathlib.LinearAlgebra.Projection
/-- An idempotent linear operator is equal to the linear projection onto
its range along its kernel.  -/
LinearMap.IsIdempotentElem.eq_projection : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {T : E →ₗ[R] E}
  (hT : IsIdempotentElem T), T = T.range.projection T.ker ⋯
-- Init.Data.Ord.Basic
Ordering.isLE_eq_not_beq_gt : ∀ {o : Ordering}, o.isLE = !o == Ordering.gt
-- Mathlib.Analysis.Normed.Group.Uniform
AntilipschitzWith.le_mul_norm : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedAddGroup E] [inst_1 : SeminormedAddGroup F] {f : E → F} {K : NNReal},
  AntilipschitzWith K f → f 0 = 0 → ∀ (x : E), ‖x‖ ≤ ↑K * ‖f x‖
-- Lean.Elab.Quotation
Lean.Elab.Term.Quotation.ArrayStxBuilder.empty : Lean.Elab.Term.Quotation.ArrayStxBuilder