mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.TensorProduct.Free
Algebra.TensorProduct.equivPiOfFiniteBasis_apply : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommSemiring A] [inst_1 : CommSemiring R] [inst_2 : Algebra R A]
  [inst_3 : AddCommGroup V] [inst_4 : Module R V] {ι : Type u_4} (b : Module.Basis ι R V) [inst_5 : Finite ι]
  (x : TensorProduct R A V) (a : ι),
  (Algebra.TensorProduct.equivPiOfFiniteBasis A b) x a =
    (TensorProduct.piScalarRightHom R A A ι) ((LinearMap.baseChange A ↑b.equivFun) x) a
-- Mathlib.Algebra.Homology.ShortComplex.Linear
CategoryTheory.ShortComplex.homologyFunctor_linear : ∀ {R : Type u_1} {C : Type u_2} [inst : Semiring R] [inst_1 : CategoryTheory.Category.{v_1, u_2} C]
  [inst_2 : CategoryTheory.Preadditive C] [inst_3 : CategoryTheory.Linear R C]
  [inst_4 : CategoryTheory.CategoryWithHomology C],
  CategoryTheory.Functor.Linear R (CategoryTheory.ShortComplex.homologyFunctor C)
-- Mathlib.Algebra.Star.Basic
/-- `star` as a `MulAut` for commutative `R`.  -/
starMulAut : {R : Type u} → [inst : CommSemigroup R] → [StarMul R] → MulAut R
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
SimpleGraph.pathGraph_le_cycleGraph : ∀ {n : ℕ}, SimpleGraph.pathGraph n ≤ SimpleGraph.cycleGraph n
-- Mathlib.MeasureTheory.Group.Prod
/-- Any two nonzero left-invariant measures are absolutely continuous w.r.t. each other.  -/
MeasureTheory.absolutelyContinuous_of_isMulLeftInvariant : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : Group G] [MeasurableMul₂ G] (μ ν : MeasureTheory.Measure G)
  [MeasureTheory.SFinite ν] [MeasureTheory.SFinite μ] [MeasurableInv G] [μ.IsMulLeftInvariant] [ν.IsMulLeftInvariant],
  ν ≠ 0 → μ.AbsolutelyContinuous ν
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.getElem?_inter_of_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap α β cmp} [Std.TransCmp cmp] {k : α},
  k ∈ t₂ → (t₁ ∩ t₂)[k]? = t₁[k]?
-- Mathlib.Probability.Kernel.Composition.CompMap
ProbabilityTheory.Kernel.fst_comp : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {γ : Type u_4} {δ : Type u_5}
  {mγ : MeasurableSpace γ} {mδ : MeasurableSpace δ} (κ : ProbabilityTheory.Kernel α β)
  (η : ProbabilityTheory.Kernel β (γ × δ)), (η.comp κ).fst = η.fst.comp κ
-- Mathlib.Algebra.GroupWithZero.Units.Lemmas
/-- Inversion on a commutative group with zero, considered as a monoid with zero homomorphism.  -/
invMonoidWithZeroHom : {G₀ : Type u_8} → [inst : CommGroupWithZero G₀] → G₀ →*₀ G₀
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.stronglyMeasurable_limit_process' : ∀ {Ω : Type u_1} {ι : Type u_2} {m : MeasurableSpace Ω} [inst : Preorder ι] {E : Type u_4} [inst_1 : Zero E]
  [inst_2 : TopologicalSpace E] {ℱ : MeasureTheory.Filtration ι m} {f : ι → Ω → E} {μ : MeasureTheory.Measure Ω},
  MeasureTheory.StronglyMeasurable (MeasureTheory.Filtration.limitProcess f ℱ μ)
-- Mathlib.RingTheory.Polynomial.Hermite.Basic
Polynomial.coeff_hermite_of_even_add : ∀ {n k : ℕ},
  Even (n + k) → (Polynomial.hermite n).coeff k = (-1) ^ ((n - k) / 2) * ↑(n - k - 1).doubleFactorial * ↑(n.choose k)
-- Mathlib.RingTheory.Adjoin.FG
Subalgebra.fg_def : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] {S : Subalgebra R A},
  S.FG ↔ ∃ t, t.Finite ∧ Algebra.adjoin R t = S
-- Mathlib.RingTheory.UniqueFactorizationDomain.Multiplicity
UniqueFactorizationMonoid.pow_dvd_pow_iff_dvd : ∀ {R : Type u_2} [inst : CommMonoidWithZero R] [UniqueFactorizationMonoid R] {a b : R} {n : ℕ},
  n ≠ 0 → (a ^ n ∣ b ^ n ↔ a ∣ b)
-- Mathlib.RingTheory.IsAdjoinRoot
IsAdjoinRoot.lift_self : ∀ {R : Type u} {S : Type v} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {f : Polynomial R}
  (h : IsAdjoinRoot S f), h.lift (algebraMap R S) h.root ⋯ = RingHom.id S
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.Pairwise.Hom.id_pair.sizeOf_spec : ∀ {ι : Type v} [inst : SizeOf ι] (i j : ι), sizeOf (CategoryTheory.Pairwise.Hom.id_pair i j) = 1 + sizeOf i + sizeOf j
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.size_alter : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  (t.alter k f).size =
    if k ∈ t ∧ (f (t.get? k)).isNone = true then t.size - 1
    else if k ∉ t ∧ (f (t.get? k)).isSome = true then t.size + 1 else t.size
-- Std.Sat.AIG.RefVecOperator.Fold
Std.Sat.AIG.RefVec.fold_decl_eq : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len : ℕ} {aig : Std.Sat.AIG α} (vec : aig.RefVec len)
  (func : (aig : Std.Sat.AIG α) → aig.BinaryInput → Std.Sat.AIG.Entrypoint α)
  [inst_2 : Std.Sat.AIG.LawfulOperator α Std.Sat.AIG.BinaryInput func] (idx : ℕ) (h1 : idx < aig.decls.size)
  (h2 : idx < (Std.Sat.AIG.RefVec.fold aig vec func).aig.decls.size),
  (Std.Sat.AIG.RefVec.fold aig vec func).aig.decls[idx] = aig.decls[idx]
-- Mathlib.Algebra.Ring.Ext
AddCommMonoidWithOne.ext_iff : ∀ {R : Type u} {inst₁ inst₂ : AddCommMonoidWithOne R}, inst₁ = inst₂ ↔ HAdd.hAdd = HAdd.hAdd ∧ One.one = One.one
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.of_apply : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} (f : m → n → α) (i : m) (j : n), Matrix.of f i j = f i j
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.get?_eq_getValueCast? : ∀ {α : Type u} {β : α → Type v} [instBEq : BEq α] [inst : Ord α] [i : Std.LawfulBEqOrd α] [Std.TransOrd α]
  [inst_2 : Std.LawfulEqOrd α] {k : α} {t : Std.DTreeMap.Internal.Impl α β},
  t.Ordered → t.get? k = Std.Internal.List.getValueCast? k t.toListModel
-- Mathlib.LinearAlgebra.Matrix.Cartan
CartanMatrix.E₇.eq_1 : CartanMatrix.E₇ =
  !![2, 0, -1, 0, 0, 0, 0;
    0, 2, 0, -1, 0, 0, 0;
    -1, 0, 2, -1, 0, 0, 0;
    0, -1, -1, 2, -1, 0, 0;
    0, 0, 0, -1, 2, -1, 0;
    0, 0, 0, 0, -1, 2, -1;
    0, 0, 0, 0, 0, -1, 2]
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.writes.eq_5 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} [inst : Fintype Γ] (l : Γ → σ → Λ),
  Turing.TM1to1.writes (Turing.TM1.Stmt.goto l) = ∅
-- Mathlib.Order.Atoms
isAtomic_iff_forall_isAtomic_Iic : ∀ {α : Type u_2} [inst : PartialOrder α] [inst_1 : OrderBot α], IsAtomic α ↔ ∀ (x : α), IsAtomic ↑(Set.Iic x)
-- Mathlib.Algebra.Algebra.Tower
AlgHom.toLinearMap_restrictScalars : ∀ (R : Type u) {S : Type v} {A : Type w} {B : Type u₁} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : Semiring A] [inst_3 : Semiring B] [inst_4 : Algebra R S] [inst_5 : Algebra S A] [inst_6 : Algebra S B]
  [inst_7 : Algebra R A] [inst_8 : Algebra R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B]
  (f : A →ₐ[S] B), (AlgHom.restrictScalars R f).toLinearMap = ↑R f.toLinearMap
-- Std.Data.DHashMap.Internal.Model
Std.DHashMap.Internal.Raw₀.insertIfNewₘ.eq_1 : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] (m : Std.DHashMap.Internal.Raw₀ α β) (a : α)
  (b : β a), m.insertIfNewₘ a b = if m.containsₘ a = true then m else (m.consₘ a b).expandIfNecessary
-- Mathlib.CategoryTheory.Sites.Sieves
CategoryTheory.Presieve.le_pullback_pushforward : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : Y ⟶ X) (R : CategoryTheory.Presieve Y),
  R ≤ CategoryTheory.Presieve.pullback f (CategoryTheory.Presieve.pushforward f R)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.check.inj : ∀ {e e_1 : Lean.Expr},
  Lean.Meta.Grind.EMatchTheoremConstraint.check e = Lean.Meta.Grind.EMatchTheoremConstraint.check e_1 → e = e_1
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp.Hom.add : {M N : SemiNormedGrp} → Add (M ⟶ N)
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegrable_zero_radius : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] {f : ℂ → E} {c : ℂ}, CircleIntegrable f c 0
-- Lean.Meta.Basic
Lean.Meta.ExprParamInfo.mk.sizeOf_spec : ∀ (name : Lean.Name) (type : Lean.Expr) (binderInfo : Lean.BinderInfo),
  sizeOf { name := name, type := type, binderInfo := binderInfo } = 1 + sizeOf name + sizeOf type + sizeOf binderInfo
-- Mathlib.CategoryTheory.Abelian.GrothendieckAxioms.Basic
CategoryTheory.instCountableAB4StarOfAB4StarOfSize : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C]
  [CategoryTheory.AB4StarOfSize.{0, v, u} C], CategoryTheory.CountableAB4Star C
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four
_private.Mathlib.CategoryTheory.Abelian.DiagramLemmas.Four.0.CategoryTheory.ComposableArrows.Precomp.map.match_1.eq_4 : ∀ {n : ℕ} (motive : (x x_1 : Fin (n + 1 + 1)) → x ≤ x_1 → Sort u_1) (i : ℕ) (hi : i + 1 < n + 1 + 1) (j : ℕ)
  (hj : j + 1 < n + 1 + 1) (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩)
  (h_1 : (isLt isLt_1 : 0 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨0, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨0, isLt_1⟩ x)
  (h_2 :
    (isLt : 0 < n + 1 + 1) → (isLt_1 : 1 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨1, isLt_1⟩) → motive ⟨0, isLt⟩ ⟨1, isLt_1⟩ x)
  (h_3 :
    (isLt : 0 < n + 1 + 1) →
      (j : ℕ) → (hj : j + 2 < n + 1 + 1) → (x : ⟨0, isLt⟩ ≤ ⟨j + 2, hj⟩) → motive ⟨0, isLt⟩ ⟨j.succ.succ, hj⟩ x)
  (h_4 :
    (i : ℕ) →
      (hi : i + 1 < n + 1 + 1) →
        (j : ℕ) → (hj : j + 1 < n + 1 + 1) → (hij : ⟨i + 1, hi⟩ ≤ ⟨j + 1, hj⟩) → motive ⟨i.succ, hi⟩ ⟨j.succ, hj⟩ hij),
  (match ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij with
    | ⟨0, isLt⟩, ⟨0, isLt_1⟩, x => h_1 isLt isLt_1 x
    | ⟨0, isLt⟩, ⟨1, isLt_1⟩, x => h_2 isLt isLt_1 x
    | ⟨0, isLt⟩, ⟨j.succ.succ, hj⟩, x => h_3 isLt j hj x
    | ⟨i.succ, hi⟩, ⟨j.succ, hj⟩, hij => h_4 i hi j hj hij) =
    h_4 i hi j hj hij
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.mk_out : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided] (x : R ⧸ I),
  (Ideal.Quotient.mk I) (Quotient.out x) = x
-- Mathlib.Algebra.BigOperators.Finprod
/-- A more general version of `finsum_mem_add_diff` that requires `t ∩ support f` rather
than `t` to be finite.  -/
finsum_mem_add_sdiff' : ∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] {f : α → M} {s t : Set α},
  s ⊆ t →
    (t ∩ Function.support f).Finite →
      ∑ᶠ (i : α) (_ : i ∈ s), f i + ∑ᶠ (i : α) (_ : i ∈ t \ s), f i = ∑ᶠ (i : α) (_ : i ∈ t), f i
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.Alt.patterns : {σ : Type} → Lean.Elab.Term.Do.Alt σ → Lean.Syntax
-- Init.Data.List.Lex
/-- `l₁` is lexicographically less than `l₂` if either
- `l₁` is pairwise equivalent under `· == ·` to `l₂.take l₁.length`,
  and `l₁` is shorter than `l₂` or
- there exists an index `i` such that
  - for all `j < i`, `l₁[j] == l₂[j]` and
  - `l₁[i] < l₂[i]`
 -/
List.lex_eq_true_iff_exists : ∀ {α : Type u_1} {l₁ l₂ : List α} [inst : BEq α] (lt : α → α → Bool),
  l₁.lex l₂ lt = true ↔
    (l₁.isEqv (List.take l₁.length l₂) fun x1 x2 => x1 == x2) = true ∧ l₁.length < l₂.length ∨
      ∃ i,
        ∃ (h₁ : i < l₁.length) (h₂ : i < l₂.length),
          (∀ (j : ℕ) (hj : j < i), (l₁[j] == l₂[j]) = true) ∧ lt l₁[i] l₂[i] = true
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.minKeyD_insertIfNew : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k : α}
  {v : β} {fallback : α},
  (t.insertIfNew k v).minKeyD fallback = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.addRight_apply : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LE α] [inst_2 : AddRightMono α] (a x : α), (OrderIso.addRight a) x = x + a
-- Mathlib.Order.Basic
eq_of_le_of_forall_gt_imp_ge_of_dense : ∀ {α : Type u_2} [inst : LinearOrder α] [DenselyOrdered α] {a₁ a₂ : α}, a₁ ≤ a₂ → (∀ a < a₂, a ≤ a₁) → a₁ = a₂
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1to1.trNormal.eq_2 : ∀ {Γ : Type u_1} {Λ : Type u_2} {σ : Type u_3} {n : ℕ} (dec : List.Vector Bool n → Γ) (a : Γ → σ → Γ)
  (q : Turing.TM1.Stmt Γ Λ σ),
  Turing.TM1to1.trNormal dec (Turing.TM1.Stmt.write a q) =
    Turing.TM1to1.read dec fun a_1 => Turing.TM1.Stmt.goto fun x s => Turing.TM1to1.Λ'.write (a a_1 s) q
-- Batteries.Control.Nondet.Basic
/-- The `Id` monad is trivially backtrackable, with state `Unit`.  -/
instMonadBacktrackUnitId_batteries : Lean.MonadBacktrack Unit Id
-- Init.Data.Array.BasicAux
/-- Applies a monadic function to each element of an array, returning the array of results. The function is
monomorphic: it is required to return a value of the same type. The internal implementation uses
pointer equality, and does not allocate a new array if the result of each function call is
pointer-equal to its argument.
 -/
Array.mapMonoM : {m : Type u_1 → Type u_2} → {α : Type u_1} → [Monad m] → Array α → (α → m α) → m (Array α)
-- Init.Data.String.TakeDrop
/-- Returns a `String.Slice` that contains the last `n` characters \(Unicode code points\) of
`s`.

If `n` is greater than `s.toList.length`, returns `s.toSlice`.

This is a cheap operation because it does not allocate a new string to hold the result.
To convert the result into a string, use `String.Slice.copy`.

Examples:

* `"red green blue".takeEnd 4 == "blue".toSlice`

* `"red green blue".takeEnd 1 == "e".toSlice`

* `"red green blue".takeEnd 0 == "".toSlice`

* `"red green blue".takeEnd 100 == "red green blue".toSlice`

* `"مرحبا بالعالم".takeEnd 5 == "لعالم".toSlice`
 -/
String.takeEnd : String → ℕ → String.Slice
-- Mathlib.Logic.Relation
/-- `EqvGen r`: equivalence closure of `r`.  -/
Relation.EqvGen : {α : Type u_1} → (α → α → Prop) → α → α → Prop
-- Mathlib.Topology.Convenient.Localization
TopCat.instIsLocalizationGeneratedByTopCatToGeneratedByTopCatMorphismPropertyWithGeneratedByTopologyEquiv : ∀ {ι : Type t} (X : ι → Type u) [inst : (i : ι) → TopologicalSpace (X i)],
  TopCat.toGeneratedByTopCat.IsLocalization (TopCat.morphismPropertyWithGeneratedByTopologyEquiv X)
-- Mathlib.RingTheory.FiniteLength
exists_compositionSeries_of_isNoetherian_isArtinian : ∀ (R : Type u_1) [inst : Ring R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherian R M]
  [IsArtinian R M], ∃ s, RelSeries.head s = ⊥ ∧ RelSeries.last s = ⊤
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.LEComap.comp : ∀ {X : Type u_2} {Y : Type u_3} {Z : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : C(X, Y)} {A : DiscreteQuotient X} {B : DiscreteQuotient Y} {g : C(Y, Z)}
  {C : DiscreteQuotient Z},
  DiscreteQuotient.LEComap g B C → DiscreteQuotient.LEComap f A B → DiscreteQuotient.LEComap (g.comp f) A C
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aevalTower_ofNat : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {S : Type u_2} {A : Type u_3} [inst_1 : CommSemiring S]
  [inst_2 : CommSemiring A] [inst_3 : Algebra S R] [inst_4 : Algebra S A] (g : R →ₐ[S] A) (y : σ → A) (n : ℕ)
  [inst_5 : n.AtLeastTwo], (MvPolynomial.aevalTower g y) (OfNat.ofNat n) = OfNat.ofNat n
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ico_inr_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (a : α) (b : β),
  Finset.Ico (Sum.inrₗ b) (Sum.inlₗ a) = ∅
-- Lean.DocString.Parser
Lean.Doc.Parser.instInhabitedBlockCtxt : Inhabited Lean.Doc.Parser.BlockCtxt
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.coe_nsmul : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P]
  (n : ℕ) (I : FractionalIdeal S P), ↑(n • I) = n • ↑I
-- Mathlib.Order.SuccPred.Basic
Order.lt_succ_of_le_of_not_isMax : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : SuccOrder α] {a b : α}, b ≤ a → ¬IsMax a → b < Order.succ a
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
NormedRing.toRingNorm_apply : ∀ (R : Type u_2) [inst : NormedRing R] (x : R), (NormedRing.toRingNorm R) x = ‖x‖
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Basic
Real.sqrtTwoAddSeries_zero_nonneg : ∀ (n : ℕ), 0 ≤ Real.sqrtTwoAddSeries 0 n
-- Std.Sat.AIG.RelabelNat
Std.Sat.AIG.RelabelNat.State.Inv2.gate : ∀ {α : Type} [inst : DecidableEq α] [inst_1 : Hashable α] {decls : Array (Std.Sat.AIG.Decl α)} {idx : ℕ}
  {map : Std.HashMap α ℕ} {l r : Std.Sat.AIG.Fanin},
  Std.Sat.AIG.RelabelNat.State.Inv2 decls idx map →
    ∀ (hlt : idx < decls.size),
      decls[idx] = Std.Sat.AIG.Decl.gate l r → Std.Sat.AIG.RelabelNat.State.Inv2 decls (idx + 1) map
-- Mathlib.Algebra.BigOperators.Group.Finset.Defs
Finset.prod_coe_sort_eq_attach : ∀ {ι : Type u_1} {M : Type u_3} (s : Finset ι) [inst : CommMonoid M] (f : ↥s → M), ∏ i, f i = ∏ i ∈ s.attach, f i
-- Mathlib.GroupTheory.Congruence.Defs
/-- The inductive principle used to prove propositions about
the elements of a quotient by an additive congruence relation.  -/
AddCon.induction_on : ∀ {M : Type u_1} [inst : Add M] {c : AddCon M} {C : c.Quotient → Prop} (q : c.Quotient), (∀ (x : M), C ↑x) → C q
-- Mathlib.CategoryTheory.Shift.Twist
CategoryTheory.TwistShiftData.commShift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type w} [inst_1 : AddMonoid A]
  [inst_2 : CategoryTheory.HasShift C A] (self : CategoryTheory.TwistShiftData C A) (a b : A),
  CategoryTheory.NatTrans.CommShift (↑(self.z a b)) A
-- Mathlib.LinearAlgebra.QuadraticForm.Basic
LinearMap.BilinMap.toQuadraticMap_neg : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] (B : LinearMap.BilinMap R M N), (-B).toQuadraticMap = -B.toQuadraticMap
-- Aesop.Forward.State
/-- Structure representing the state of a slot cluster. Updates are performed
lazily: the `enqueueRawHyp` method enqueues a hyp or patten subst to be added to
the state, and the `update` method must be used to actually make the
corresponding changes and potentially generate new complete matches.  -/
Aesop.ClusterState : Type
-- Mathlib.Analysis.Distribution.TestFunction
TestFunction.mk.inj : ∀ {E : Type u_3} {inst : NormedAddCommGroup E} {inst_1 : NormedSpace ℝ E} {Ω : TopologicalSpace.Opens E} {F : Type u_4}
  {inst_2 : NormedAddCommGroup F} {inst_3 : NormedSpace ℝ F} {n : ℕ∞} {toFun : E → F}
  {contDiff' : ContDiff ℝ (↑n) toFun} {hasCompactSupport' : HasCompactSupport toFun}
  {tsupport_subset' : tsupport toFun ⊆ ↑Ω} {toFun_1 : E → F} {contDiff'_1 : ContDiff ℝ (↑n) toFun_1}
  {hasCompactSupport'_1 : HasCompactSupport toFun_1} {tsupport_subset'_1 : tsupport toFun_1 ⊆ ↑Ω},
  { toFun := toFun, contDiff' := contDiff', hasCompactSupport' := hasCompactSupport',
        tsupport_subset' := tsupport_subset' } =
      { toFun := toFun_1, contDiff' := contDiff'_1, hasCompactSupport' := hasCompactSupport'_1,
        tsupport_subset' := tsupport_subset'_1 } →
    toFun = toFun_1
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.coe_eq_zero : ∀ {z : Complex.UnitClosedDisc}, ↑z = 0 ↔ z = 0
-- Mathlib.Data.Sum.Interval
Sum.Lex.Ioo_inr_inl : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : LocallyFiniteOrder α]
  [inst_3 : LocallyFiniteOrder β] [inst_4 : LocallyFiniteOrderTop α] [inst_5 : LocallyFiniteOrderBot β] (a : α) (b : β),
  Finset.Ioo (Sum.inrₗ b) (Sum.inlₗ a) = ∅
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_injective_right : ∀ {α : Type u_2} [inst : DistribLattice α] [inst_1 : LocallyFiniteOrder α] (a : α),
  Function.Injective fun b => Finset.uIcc b a
-- Init.Data.Option.Attach
Option.isNone_attach : ∀ {α : Type u_1} (o : Option α), o.attach.isNone = o.isNone
-- Mathlib.Algebra.Group.Submonoid.Membership
Submonoid.decidableMemPowers : {M : Type u_1} → [inst : Monoid M] → {a : M} → DecidablePred fun x => x ∈ Submonoid.powers a
-- Mathlib.Analysis.Calculus.Deriv.Mul
HasDerivAt.congr_simp : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {F : Type v} [inst_1 : AddCommGroup F] [inst_2 : Module 𝕜 F]
  [inst_3 : TopologicalSpace F] [inst_4 : ContinuousSMul 𝕜 F] (f f_1 : 𝕜 → F),
  f = f_1 → ∀ (f' f'_1 : F), f' = f'_1 → ∀ (x x_1 : 𝕜), x = x_1 → HasDerivAt f f' x = HasDerivAt f_1 f'_1 x_1
-- Lean.DocString.Markdown
/-- Length of the longest unbroken run of `` ` `` characters in `str`.
 -/
_private.Lean.DocString.Markdown.0.Lean.Doc.longestBacktickRun : String → ℕ
-- Aesop.Util.Basic
Aesop.runTacticSeqCapturingPostState : Lean.TSyntax `Lean.Parser.Tactic.tacticSeq →
  Lean.Meta.SavedState → List Lean.MVarId → Lean.MetaM (Lean.Meta.SavedState × List Lean.MVarId)
-- Mathlib.CategoryTheory.Monoidal.Ring
/-- A ring object in a cartesian monoidal category is an object that is equipped
with an additive group structure and a (multiplicative) monoid structure that
is left and right distributive over the additive structure.  -/
CategoryTheory.RingObj : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.CartesianMonoidalCategory C] → [CategoryTheory.BraidedCategory C] → C → Type v
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_of_getKey?_eq_some : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k k' : α}, t.getKey? k = some k' → k' ∈ t
-- Std.Data.DHashMap.IteratorLemmas
_private.Std.Data.DHashMap.IteratorLemmas.0.Std.DHashMap.toList_inner : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap α β}, m.inner.toList = m.toList
-- Mathlib.Data.Int.Bitwise
/-- `bodd n` returns `true` if `n` is odd  -/
Int.bodd : ℤ → Bool
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ExponentiableMorphism
/-- The pushforward functor  -/
CategoryTheory.ExponentiableMorphism.pushforward : {C : Type u} →
  {inst : CategoryTheory.Category.{v, u} C} →
    {I J : C} →
      (f : I ⟶ J) →
        {inst_1 : CategoryTheory.ChosenPullbacksAlong f} →
          [self : CategoryTheory.ExponentiableMorphism f] →
            CategoryTheory.Functor (CategoryTheory.Over I) (CategoryTheory.Over J)
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.linearIsometryBoundedOfCompact_toAddEquiv : ∀ {α : Type u_1} {E : Type u_3} [inst : TopologicalSpace α] [inst_1 : CompactSpace α]
  [inst_2 : SeminormedAddCommGroup E] {𝕜 : Type u_4} [inst_3 : NormedRing 𝕜] [inst_4 : Module 𝕜 E]
  [inst_5 : IsBoundedSMul 𝕜 E],
  ↑(ContinuousMap.linearIsometryBoundedOfCompact α E 𝕜).toLinearEquiv = ContinuousMap.addEquivBoundedOfCompact α E
-- Mathlib.Data.Nat.Multiplicity
/-- For a prime number `p`, taking `(p - 1)` times the multiplicity of `p` in `n!` equals `n` minus
the sum of base `p` digits of `n`.  -/
Nat.Prime.sub_one_mul_multiplicity_factorial : ∀ {n p : ℕ}, Nat.Prime p → (p - 1) * multiplicity p n.factorial = n - (p.digits n).sum
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The canonical functor from the structured arrow category on the diagonal functor
`T ⥤ T × T` to the structured arrow category on `Under.forget`.  -/
CategoryTheory.StructuredArrow.ofDiagEquivalence.functor : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    (X : T × T) →
      CategoryTheory.Functor (CategoryTheory.StructuredArrow X (CategoryTheory.Functor.diag T))
        (CategoryTheory.StructuredArrow X.2 (CategoryTheory.Under.forget X.1))
-- Mathlib.Probability.Independence.Basic
ProbabilityTheory.Indep.indepSets : ∀ {Ω : Type u_1} {_mΩ : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {s1 s2 : Set (Set Ω)},
  ProbabilityTheory.Indep (MeasurableSpace.generateFrom s1) (MeasurableSpace.generateFrom s2) μ →
    ProbabilityTheory.IndepSets s1 s2 μ
-- Mathlib.Analysis.InnerProductSpace.l2Space
/-- A Hilbert basis on `ι` for an inner product space `E` is an identification of `E` with the `lp`
space `ℓ²(ι, 𝕜)`.  -/
HilbertBasis : Type u_1 →
  (𝕜 : Type u_2) →
    [inst : RCLike 𝕜] →
      (E : Type u_3) → [inst_1 : NormedAddCommGroup E] → [InnerProductSpace 𝕜 E] → Type (max (max u_1 u_2) u_3)
-- Mathlib.AlgebraicGeometry.Morphisms.QuasiCompact
AlgebraicGeometry.Scheme.Hom.isCompact_preimage : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.QuasiCompact f] {U : Y.Opens},
  IsCompact ↑U → IsCompact ↑((TopologicalSpace.Opens.map f.base).obj U)
-- Mathlib.LinearAlgebra.Dual.Lemmas
/-- `f.dualMap` is bijective if and only if `f` is  -/
LinearMap.dualMap_bijective_iff : ∀ {K : Type u_1} {V₁ : Type u_2} {V₂ : Type u_3} [inst : Field K] [inst_1 : AddCommGroup V₁] [inst_2 : Module K V₁]
  [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] {f : V₁ →ₗ[K] V₂},
  Function.Bijective ⇑f.dualMap ↔ Function.Bijective ⇑f