mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Analysis.Calculus.ContDiff.FiniteDimension
/-- This is a useful lemma to prove that a certain operation preserves functions being `C^n`.
When you do induction on `n`, this gives a useful characterization of a function being `C^(n+1)`,
assuming you have already computed the derivative. The advantage of this version over
`contDiff_succ_iff_fderiv` is that both occurrences of `ContDiff` are for functions with the same
domain and codomain (`D` and `E`). This is not the case for `contDiff_succ_iff_fderiv`, which
often requires an inconvenient need to generalize `F`, which results in universe issues
(see the discussion in the section of `ContDiff.comp`).

This lemma avoids these universe issues, but only applies for finite-dimensional `D`.  -/
contDiff_succ_iff_fderiv_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {D : Type uD} [inst_1 : NormedAddCommGroup D]
  [inst_2 : NormedSpace 𝕜 D] {E : Type uE} [inst_3 : NormedAddCommGroup E] [inst_4 : NormedSpace 𝕜 E] {n : WithTop ℕ∞}
  {f : D → E} [CompleteSpace 𝕜] [FiniteDimensional 𝕜 D],
  ContDiff 𝕜 (n + 1) f ↔
    Differentiable 𝕜 f ∧ (n = ⊤ → AnalyticOnNhd 𝕜 f Set.univ) ∧ ∀ (y : D), ContDiff 𝕜 n fun x => (fderiv 𝕜 f x) y
-- Init.Data.Array.Basic
/-- Returns `true` if `as` and `bs` have the same length and they are pairwise related by `eqv`.

Short-circuits at the first non-related pair of elements.

Examples:
* `#[1, 2, 3].isEqv #[2, 3, 4] (· < ·) = true`
* `#[1, 2, 3].isEqv #[2, 2, 4] (· < ·) = false`
* `#[1, 2, 3].isEqv #[2, 3] (· < ·) = false`
 -/
Array.isEqv : {α : Type u} → Array α → Array α → (α → α → Bool) → Bool
-- Mathlib.RingTheory.Finiteness.Quotient
/-- `B ⧸ P` is a Noetherian `A ⧸ p`-module if `B` is a Noetherian `A`-module.  -/
isNoetherian_of_liesOver : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] (P : Ideal B)
  (p : Ideal A) [inst_3 : P.LiesOver p] [IsNoetherian A B], IsNoetherian (A ⧸ p) (B ⧸ P)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassFactorizationAt.map_ne_zero_of_ne_top : ∀ {A : Type u_1} [inst : CommRing A] {g : PowerSeries A} {f : Polynomial A} {h : PowerSeries A} {I : Ideal A},
  g.IsWeierstrassFactorizationAt f h I → I ≠ ⊤ → (PowerSeries.map (Ideal.Quotient.mk I)) g ≠ 0
-- Mathlib.Algebra.Ring.Equiv
/-- See Note [custom simps projection]  -/
RingEquiv.Simps.symm_apply : {R : Type u_4} →
  {S : Type u_5} → [inst : Mul R] → [inst_1 : Mul S] → [inst_2 : Add R] → [inst_3 : Add S] → R ≃+* S → S → R
-- Mathlib.Tactic.CrossRefAttribute
Mathlib.CrossRef.instHashableDatabase.hash : Mathlib.CrossRef.Database → UInt64
-- Mathlib.Probability.BrownianMotion.GaussianProjectiveFamily
ProbabilityTheory.BrownianReal.covariance_projectiveFamily : ∀ (I : Finset NNReal) (f g : (↥I → ℝ) → ℝ),
  ProbabilityTheory.covariance f g (ProbabilityTheory.BrownianReal.projectiveFamily I) =
    ProbabilityTheory.covariance (f ∘ WithLp.ofLp) (g ∘ WithLp.ofLp)
      (ProbabilityTheory.multivariateGaussian 0 (ProbabilityTheory.BrownianReal.covMatrix I))
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.contains_ofList : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α]
  {l : List ((a : α) × β a)} {k : α}, (Std.DHashMap.Raw.ofList l).contains k = (List.map Sigma.fst l).contains k
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.yonedaAddMonObjRepresentableBy.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.AddMonObj M],
  CategoryTheory.yonedaAddMonObjRepresentableBy M =
    CategoryTheory.Functor.representableByEquiv.symm (CategoryTheory.Iso.refl (CategoryTheory.yoneda.obj M))
-- Mathlib.Topology.Separation.Basic
isOpen_compl_singleton : ∀ {X : Type u_1} [inst : TopologicalSpace X] [T1Space X] {x : X}, IsOpen {x}ᶜ
-- Mathlib.Analysis.InnerProductSpace.TensorProduct
TensorProduct.ridIsometry_apply : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  (x : TensorProduct 𝕜 E 𝕜), (TensorProduct.ridIsometry 𝕜 E) x = (TensorProduct.rid 𝕜 E) x
-- Lean.Meta.Match.MatcherInfo
Lean.Meta.Match.addMatcherInfo : {m : Type → Type} → [Monad m] → [Lean.MonadEnv m] → Lean.Name → Lean.Meta.MatcherInfo → m Unit
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_filterMap_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited γ] {f : α → β → Option γ} {k k' : α},
  m.WF →
    m.getKey? k = some k' →
      Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.filterMap f m) k =
        ((Std.DHashMap.Raw.Const.get? m k).bind fun x => f k' x).get!
-- Mathlib.Algebra.Order.UpperLower
UpperSet.instAdd.eq_1 : ∀ {α : Type u_1} [inst : AddCommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedAddMonoid α],
  UpperSet.instAdd = { add := fun s t => { carrier := Set.image2 (fun x1 x2 => x1 + x2) ↑s ↑t, upper' := ⋯ } }
-- Init.Data.String.Defs
String.instLEPos : {s : String} → LE s.Pos
-- Mathlib.Order.Filter.Basic
Filter.Eventually.exists_mem : ∀ {α : Type u} {p : α → Prop} {f : Filter α}, (∀ᶠ (x : α) in f, p x) → ∃ v ∈ f, ∀ y ∈ v, p y
-- Mathlib.FieldTheory.Perfect
/-- For a reduced ring, surjectivity of the Frobenius map is a sufficient condition for perfection.
 -/
PerfectRing.ofSurjective : ∀ (R : Type u_2) (p : ℕ) [inst : CommRing R] [inst_1 : ExpChar R p] [IsReduced R],
  Function.Surjective ⇑(frobenius R p) → PerfectRing R p
-- Mathlib.Algebra.Homology.Additive
/-- A natural isomorphism between functors induces a natural isomorphism
between those functors applied to homological complexes.
 -/
CategoryTheory.NatIso.mapHomologicalComplex : {ι : Type u_1} →
  {W₁ : Type u_3} →
    {W₂ : Type u_4} →
      [inst : CategoryTheory.Category.{v_2, u_3} W₁] →
        [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] →
          [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁] →
            [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] →
              {F G : CategoryTheory.Functor W₁ W₂} →
                [inst_4 : F.PreservesZeroMorphisms] →
                  [inst_5 : G.PreservesZeroMorphisms] →
                    (F ≅ G) → (c : ComplexShape ι) → F.mapHomologicalComplex c ≅ G.mapHomologicalComplex c
-- Mathlib.Topology.Order.LocalExtr
Filter.EventuallyEq.isLocalMaxOn_iff : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder β] {s : Set α} {f g : α → β} {a : α},
  f =ᶠ[nhdsWithin a s] g → a ∈ s → (IsLocalMaxOn f s a ↔ IsLocalMaxOn g s a)
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.instIsLocalizationCarrierObjOppositeOpensCarrierCommRingCatObjLocalizationPresheaf : ∀ {X : TopCat} {F : TopCat.Presheaf CommRingCat X} (G : F.SubmonoidPresheaf) (U : (TopologicalSpace.Opens ↑X)ᵒᵖ),
  IsLocalization (G.obj U) ↑(G.localizationPresheaf.obj U)
-- Mathlib.Algebra.Module.Presentation.Basic
Module.Relations.Solution.π_single : ∀ {A : Type u} [inst : Ring A] {relations : Module.Relations A} {M : Type v} [inst_1 : AddCommGroup M]
  [inst_2 : Module A M] (solution : relations.Solution M) (g : relations.G), (solution.π fun₀ | g => 1) = solution.var g
-- Std.Time.Zoned.Database.Basic
/-- Retrieves the local zone rules information (`ZoneRules`) at a given timestamp.
 -/
Std.Time.Database.getLocalZoneRules : {α : Type} → [self : Std.Time.Database α] → α → IO Std.Time.TimeZone.ZoneRules
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getKey_modify : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} [inst : Std.TransCmp cmp] [Inhabited α]
  {k k' : α} {f : β → β} {hc : k' ∈ t.modify k f},
  (t.modify k f).getKey k' hc = if cmp k k' = Ordering.eq then k else t.getKey k' ⋯
-- Mathlib.Algebra.EuclideanDomain.Basic
EuclideanDomain.gcd_one_left : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a : R), EuclideanDomain.gcd 1 a = 1
-- Init.Data.Nat.Basic
Nat.add_right_cancel : ∀ {n m k : ℕ}, n + m = k + m → n = k
-- Init.System.Platform
System.Platform.System.Platform.sixteen_dvd_numBits : 16 ∣ System.Platform.numBits
-- Mathlib.Data.Finset.Defs
Finset.PiFinsetCoe.canLift : ∀ (ι : Type u_4) (α : ι → Type u_5) [_ne : ∀ (i : ι), Nonempty (α i)] (s : Finset ι),
  CanLift ((i : ↥s) → α ↑i) ((i : ι) → α i) (fun f i => f ↑i) fun x => True
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
CliffordAlgebra.equivBaseChange_symm_apply : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V)
  (a : TensorProduct R A (CliffordAlgebra Q)),
  (CliffordAlgebra.equivBaseChange A Q).symm a = (CliffordAlgebra.ofBaseChange A Q) a
-- Mathlib.GroupTheory.Submonoid.Center
/-- The center of isomorphic monoids are isomorphic.  -/
Submonoid.centerCongr : {M : Type u_2} →
  {N : Type u_1} →
    [inst : MulOneClass M] → [inst_1 : MulOneClass N] → M ≃* N → ↥(Submonoid.center M) ≃* ↥(Submonoid.center N)
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_eq_zero : ∀ {x y : ℝ}, 0 ≤ x → y ≠ 0 → (x ^ y = 0 ↔ x = 0)
-- Mathlib.Algebra.Lie.Weights.Killing
/-- For any `α` and `β`, the corresponding root spaces are orthogonal with respect to the Killing
form, provided `α + β ≠ 0`.  -/
LieAlgebra.killingForm_apply_eq_zero_of_mem_rootSpace_of_add_ne_zero : ∀ (K : Type u_2) (L : Type u_3) [inst : LieRing L] [inst_1 : Field K] [inst_2 : LieAlgebra K L] [FiniteDimensional K L]
  (H : LieSubalgebra K L) [inst_4 : H.IsCartanSubalgebra] [LieModule.IsTriangularizable K (↥H) L] {α β : ↥H → K}
  {x y : L}, x ∈ LieAlgebra.rootSpace H α → y ∈ LieAlgebra.rootSpace H β → α + β ≠ 0 → ((killingForm K L) x) y = 0
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrp.tensorHom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {X₁ Y₁ X₂ Y₂ : CategoryTheory.AddGrp C} (f : X₁ ⟶ Y₁) (g : X₂ ⟶ Y₂),
  (CategoryTheory.MonoidalCategoryStruct.tensorHom f g).hom =
    CategoryTheory.MonoidalCategoryStruct.tensorHom f.hom g.hom
-- Init.SizeOf
Subtype.mk.sizeOf_spec : ∀ {α : Sort u} {p : α → Prop} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (p a)] (val : α) (property : p val),
  sizeOf ⟨val, property⟩ = 1 + sizeOf val + sizeOf property
-- Mathlib.GroupTheory.Focal
/-- The transfer homomorphism `V : G → H/H*` from `G` the abelian quotient `H/H*`.  -/
AddSubgroup.transferFocal : {G : Type u_1} → [inst : AddGroup G] → (H : AddSubgroup G) → [H.FiniteIndex] → G →+ ↥H ⧸ H.focalAddSubgroupOf
-- Mathlib.Algebra.Lie.SkewAdjoint
LinearMap.BilinForm.isSkewAdjoint_bracket : ∀ {R : Type u} {M : Type v} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  (B : LinearMap.BilinForm R M) {f g : Module.End R M},
  f ∈ LinearMap.skewAdjointSubmodule B →
    g ∈ LinearMap.skewAdjointSubmodule B → ⁅f, g⁆ ∈ LinearMap.skewAdjointSubmodule B
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SetLike.val_vadd_of_tower : ∀ {S : Type u'} {M : Type v} {N : Type u_1} {α : Type u_2} [inst : SetLike S α] [inst_1 : VAdd M N] [inst_2 : VAdd M α]
  [inst_3 : AddMonoid N] [inst_4 : AddAction N α] [inst_5 : VAddMemClass S N α] [inst_6 : VAddAssocClass M N α] (s : S)
  (r : M) (x : ↥s), ↑(r +ᵥ x) = r +ᵥ ↑x
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.domCongr_symm : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (e : M ≃* N),
  (MonoidAlgebra.domCongr R A e).symm = MonoidAlgebra.domCongr R A e.symm
-- Init.Data.SInt.Lemmas
Int64.toInt_sub_of_le : ∀ (a b : Int64), 0 ≤ b → b ≤ a → (a - b).toInt = a.toInt - b.toInt
-- Mathlib.CategoryTheory.Sites.Hypercover.One
CategoryTheory.GrothendieckTopology.OneHypercover.comp_h₀ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {S : C}
  {X Y Z : J.OneHypercover S} (f : X.Hom Y) (g : Y.Hom Z) (i : X.I₀),
  (CategoryTheory.CategoryStruct.comp f g).h₀ i = CategoryTheory.CategoryStruct.comp (f.h₀ i) (g.h₀ (f.s₀ i))
-- Mathlib.Algebra.Order.GroupWithZero.Basic
StrictMono.mul_const : ∀ {α : Type u_1} {M₀ : Type u_2} [inst : MonoidWithZero M₀] [inst_1 : PartialOrder M₀] {a : M₀} [inst_2 : Preorder α]
  {f : α → M₀} [MulPosStrictMono M₀], StrictMono f → 0 < a → StrictMono fun x => f x * a
-- Init.Data.Int.Bitwise.Lemmas
Int.shiftRight_eq_div_pow : ∀ (m : ℤ) (n : ℕ), m >>> n = m / ↑(2 ^ n)
-- Mathlib.Data.Finset.Card
/-- Analogue of `strongDownwardInduction` with order of arguments swapped.  -/
Finset.strongDownwardInductionOn : {α : Type u_1} →
  {n : ℕ} →
    {p : Finset α → Sort u_4} →
      (s : Finset α) →
        ((t₁ : Finset α) → ({t₂ : Finset α} → t₂.card ≤ n → t₁ ⊂ t₂ → p t₂) → t₁.card ≤ n → p t₁) → s.card ≤ n → p s
-- Init.Data.Range.Polymorphic.Iterators
Std.Rcc.Internal.isPlausibleIndirectOutput_iter_iff : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  [Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α] {r : Std.Rcc α} {a : α},
  (Std.Rcc.Internal.iter r).IsPlausibleIndirectOutput a ↔ a ∈ r
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.pullbackMap_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {Y' Z' X' Y'' Z'' X'' : C} {f' : Y' ⟶ X'} {g' : Z' ⟶ X'}
  {f'' : Y'' ⟶ X''} {g'' : Z'' ⟶ X''} [inst_2 : CategoryTheory.ChosenPullbacksAlong g']
  [inst_3 : CategoryTheory.ChosenPullbacksAlong g''] {γ₁ : Y' ⟶ Y} {γ₂ : Z' ⟶ Z} {γ₃ : X' ⟶ X} {δ₁ : Y'' ⟶ Y'}
  {δ₂ : Z'' ⟶ Z'} {δ₃ : X'' ⟶ X'}
  (comm₁ :
    autoParam (CategoryTheory.CategoryStruct.comp f' γ₃ = CategoryTheory.CategoryStruct.comp γ₁ f)
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_comp._auto_1)
  (comm₂ :
    autoParam (CategoryTheory.CategoryStruct.comp g' γ₃ = CategoryTheory.CategoryStruct.comp γ₂ g)
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_comp._auto_3)
  (comm₁' :
    autoParam (CategoryTheory.CategoryStruct.comp f'' δ₃ = CategoryTheory.CategoryStruct.comp δ₁ f')
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_comp._auto_5)
  (comm₂' :
    autoParam (CategoryTheory.CategoryStruct.comp g'' δ₃ = CategoryTheory.CategoryStruct.comp δ₂ g')
      CategoryTheory.ChosenPullbacksAlong.pullbackMap_comp._auto_7)
  {Z_1 : C} (h : CategoryTheory.ChosenPullbacksAlong.pullbackObj f g ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.pullbackMap f' g' f'' g'' δ₁ δ₂ δ₃ comm₁' comm₂')
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.ChosenPullbacksAlong.pullbackMap f g f' g' γ₁ γ₂ γ₃ comm₁ comm₂) h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.ChosenPullbacksAlong.pullbackMap f g f'' g'' (CategoryTheory.CategoryStruct.comp δ₁ γ₁)
        (CategoryTheory.CategoryStruct.comp δ₂ γ₂) (CategoryTheory.CategoryStruct.comp δ₃ γ₃) ⋯ ⋯)
      h
-- Mathlib.MeasureTheory.Covering.Besicovitch
Besicovitch.SatelliteConfig.hlast : ∀ {α : Type u_1} [inst : MetricSpace α] {N : ℕ} {τ : ℝ} (self : Besicovitch.SatelliteConfig α N τ),
  ∀ i < Fin.last N, self.r i ≤ dist (self.c i) (self.c (Fin.last N)) ∧ self.r (Fin.last N) ≤ τ * self.r i
-- Init.Data.List.Lemmas
List.flatten_append : ∀ {α : Type u_1} {L₁ L₂ : List (List α)}, (L₁ ++ L₂).flatten = L₁.flatten ++ L₂.flatten
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
ciSup_mono_of_forall_exists : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {ι' : Sort u_5} [Nonempty ι] {f : ι → α}
  {g : ι' → α}, BddAbove (Set.range g) → (∀ (i : ι), ∃ i', f i ≤ g i') → ⨆ i, f i ≤ ⨆ i', g i'
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Commute
/-- For `a` selfadjoint, an element commutes with `cfc f a` if it commutes with `a`.

If the base ring is `ℝ` or `ℝ≥0`, see `Commute.cfc_real` or `Commute.cfc_nnreal` which don't require
the `IsSelfAdjoint` hypothesis on `a` (due to the junk value `cfc f a = 0`).  -/
IsSelfAdjoint.commute_cfc : ∀ {𝕜 : Type u_1} {A : Type u_2} {p : A → Prop} [inst : RCLike 𝕜] [inst_1 : Ring A] [inst_2 : StarRing A]
  [inst_3 : Algebra 𝕜 A] [inst_4 : TopologicalSpace A] [inst_5 : ContinuousFunctionalCalculus 𝕜 A p]
  [IsSemitopologicalRing A] [T2Space A] {a b : A}, IsSelfAdjoint a → Commute a b → ∀ (f : 𝕜 → 𝕜), Commute (cfc f a) b
-- Init.Data.BitVec.Bitblast
/-- Shifts `x` to the left by the first `n` bits of `y`.

The theorem `BitVec.shiftLeft_eq_shiftLeftRec` proves the equivalence of `(x <<< y)` and
`BitVec.shiftLeftRec x y`.

Together with equations `BitVec.shiftLeftRec_zero` and `BitVec.shiftLeftRec_succ`, this allows
`BitVec.shiftLeft` to be unfolded into a circuit for bit blasting.
  -/
BitVec.shiftLeftRec : {w₁ w₂ : ℕ} → BitVec w₁ → BitVec w₂ → ℕ → BitVec w₁
-- Mathlib.Algebra.Homology.Embedding.CochainComplex
CochainComplex.isLE_shift : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  (K : CochainComplex C ℤ) [CategoryTheory.CategoryWithHomology C] (n : ℤ) [K.IsLE n] (a n' : ℤ),
  a + n' = n → ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K).IsLE n'
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
IsClosed.nullMeasurableSet : ∀ {α : Type u_1} {s : Set α} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] [OpensMeasurableSpace α]
  {μ : MeasureTheory.Measure α}, IsClosed s → MeasureTheory.NullMeasurableSet s μ
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.toPoly'.go.match_1.eq_7 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (a : Int.Internal.Linear.Expr)
  (h_1 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_2 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_3 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_4 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b))
  (h_5 : (k : ℤ) → (a : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k a))
  (h_6 : (a : Int.Internal.Linear.Expr) → (k : ℤ) → motive (a.mulR k))
  (h_7 : (a : Int.Internal.Linear.Expr) → motive a.neg),
  (match a.neg with
    | Int.Internal.Linear.Expr.num k => h_1 k
    | Int.Internal.Linear.Expr.var v => h_2 v
    | a.add b => h_3 a b
    | a.sub b => h_4 a b
    | Int.Internal.Linear.Expr.mulL k a => h_5 k a
    | a.mulR k => h_6 a k
    | a.neg => h_7 a) =
    h_7 a
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.num_denom_mul : ∀ {K : Type u} [inst : Field K] (x y : RatFunc K), (x * y).num * (x.denom * y.denom) = x.num * y.num * (x * y).denom
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomMulAct.instNonAssocSemiringOfMulOpposite.eq_1 : ∀ {M : Type u_1} [inst : NonAssocSemiring Mᵐᵒᵖ], DomMulAct.instNonAssocSemiringOfMulOpposite = inst
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.instInhabitedRuleSets : Inhabited Aesop.Frontend.RuleSets
-- Mathlib.Algebra.Order.Monoid.Prod
Prod.instIsOrderedMonoid : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α] [inst_3 : CommMonoid β]
  [inst_4 : Preorder β] [IsOrderedMonoid β], IsOrderedMonoid (α × β)
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.getKey!_alter_self : ∀ {α : Type u} {β : Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.HashMap.Raw α β} [inst_2 : EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α] {k : α} {f : Option β → Option β},
  m.WF → (m.alter k f).getKey! k = if (f m[k]?).isSome = true then k else default
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.OverMorphism.ext_iff : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} {f g : U ⟶ V},
  f = g ↔ CategoryTheory.Over.Hom.left f = CategoryTheory.Over.Hom.left g
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.prod_min_le : ∀ {α : Type u_2} {M : Type u_3} [inst : Monoid M] [inst_1 : LinearOrder M] [MulLeftMono M] [MulRightMono M] (l : List α)
  (f g : α → M), (List.map (fun i => min (f i) (g i)) l).prod ≤ min (List.map f l).prod (List.map g l).prod
-- Batteries.Data.Fin.Lemmas
Fin.findSome?_succ_of_none : ∀ {n : ℕ} {α : Type u_1} {f : Fin (n + 1) → Option α}, f 0 = none → Fin.findSome? f = Fin.findSome? fun x => f x.succ
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Cfg.halt.inj : ∀ {a a_1 : List ℕ}, Turing.ToPartrec.Cfg.halt a = Turing.ToPartrec.Cfg.halt a_1 → a = a_1
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The identity map is a continuous multiplicative isomorphism.  -/
ContinuousMulEquiv.refl : (M : Type u_1) → [inst : TopologicalSpace M] → [inst_1 : Mul M] → M ≃ₜ* M
-- Mathlib.Analysis.Fourier.ZMod
ZMod.dft_const_smul : ∀ {N : ℕ} [inst : NeZero N] {E : Type u_1} [inst_1 : AddCommGroup E] [inst_2 : Module ℂ E] {R : Type u_2}
  [inst_3 : DistribSMul R E] [SMulCommClass R ℂ E] (r : R) (Φ : ZMod N → E), ZMod.dft (r • Φ) = r • ZMod.dft Φ
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.instCompleteLatticeOfT1Space : {R : Type u_2} →
  {N : Type u_4} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid N] →
        [inst_2 : TopologicalSpace N] →
          [inst_3 : Module R N] →
            [ContinuousAdd N] → [ContinuousConstSMul R N] → [T1Space N] → CompleteLattice (ClosedSubmodule R N)
-- Mathlib.Order.Bounds.Basic
bddBelow_Icc : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, BddBelow (Set.Icc b a)
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquiv.map_eq_zero_iff : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : TopologicalSpace A] [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A]
  [inst_6 : Algebra R B] (e : A ≃A[R] B) {a : A}, e a = 0 ↔ a = 0
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.bsup_lt_ord_lift_of_isRegular : ∀ {o : Ordinal.{u}} {f : (a : Ordinal.{u}) → a < o → Ordinal.{max u v}} {c : Cardinal.{max u v}},
  c.IsRegular → Cardinal.lift.{v, u} o.card < c → (∀ (i : Ordinal.{u}) (hi : i < o), f i hi < c.ord) → o.bsup f < c.ord
-- Mathlib.Topology.Irreducible
IsIrreducible.nonempty : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsIrreducible s → s.Nonempty
-- Std.Data.HashMap.Lemmas
Std.HashMap.contains_of_contains_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α] {f : α → β → Option γ} {k : α}, (Std.HashMap.filterMap f m).contains k = true → m.contains k = true
-- Mathlib.Algebra.Order.Group.DenselyOrdered
_private.Mathlib.Algebra.Order.Group.DenselyOrdered.0.exists_lt_add_left : ∀ {α : Type u_1} [inst : AddGroup α] [inst_1 : LT α] [DenselyOrdered α] [AddRightStrictMono α] {a b c : α},
  c < a + b → ∃ a' < a, c < a' + b
-- Mathlib.ModelTheory.Algebra.Ring.FreeCommRing
/-- Make a `Language.ring.Term α` from an element of `FreeCommRing α`  -/
FirstOrder.Ring.termOfFreeCommRing : {α : Type u_1} → FreeCommRing α → FirstOrder.Language.ring.Term α
-- Mathlib.RingTheory.Valuation.Basic
Valuation.comap_id : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀),
  Valuation.comap (RingHom.id R) v = v
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.mk.sizeOf_spec : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] [inst_4 : SizeOf 𝕜] [inst_5 : SizeOf E]
  (toPreAbstractSimplicialComplex : PreAbstractSimplicialComplex E)
  (indep : ∀ {s : Finset E}, s ∈ toPreAbstractSimplicialComplex.faces → AffineIndependent 𝕜 Subtype.val)
  (inter_subset_convexHull :
    ∀ {s t : Finset E},
      s ∈ toPreAbstractSimplicialComplex.faces →
        t ∈ toPreAbstractSimplicialComplex.faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t ⊆ (convexHull 𝕜) (↑s ∩ ↑t)),
  sizeOf
      { toPreAbstractSimplicialComplex := toPreAbstractSimplicialComplex, indep := indep,
        inter_subset_convexHull := inter_subset_convexHull } =
    1 + sizeOf toPreAbstractSimplicialComplex