mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.Adjoin.Polynomial.Basic
Polynomial.adjoin_X : ∀ {R : Type u} [inst : CommSemiring R], R[Polynomial.X] = ⊤
-- Mathlib.MeasureTheory.Measure.Prod
MeasureTheory.Measure.snd_add : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : MeasurableSpace β]
  {μ ν : MeasureTheory.Measure (α × β)}, (μ + ν).snd = μ.snd + ν.snd
-- Mathlib.CategoryTheory.NatIso
CategoryTheory.Iso.hom_inv_id_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F G : CategoryTheory.Functor C D} (α : F ≅ G) (X : C) {Z : D} (h : F.obj X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (α.hom.app X) (CategoryTheory.CategoryStruct.comp (α.inv.app X) h) = h
-- Mathlib.CategoryTheory.Sites.Sieves
/-- If a sieve S is contained in a sieve T, then we have a morphism of presheaves on their induced
presheaves.
 -/
CategoryTheory.Sieve.natTransOfLe : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X : C} → {S T : CategoryTheory.Sieve X} → S ≤ T → (S.functor ⟶ T.functor)
-- Mathlib.Topology.OpenPartialHomeomorph.Basic
OpenPartialHomeomorph.target_inter_inv_preimage_preimage : ∀ {X : Type u_1} {Y : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  (e : OpenPartialHomeomorph X Y) (s : Set Y), e.target ∩ ↑e.symm ⁻¹' ↑e ⁻¹' s = e.target ∩ s
-- Init.Ext
PProd.ext : ∀ {α : Sort u} {β : Sort v} {x y : α ×' β}, x.fst = y.fst → x.snd = y.snd → x = y
-- Mathlib.Topology.Algebra.InfiniteSum.SummationFilter
SummationFilter.map_filter : ∀ {β : Type u_2} {γ : Type u_3} (L : SummationFilter β) (f : β ↪ γ),
  (L.map f).filter = Filter.map (Finset.map f) L.filter
-- Mathlib.CategoryTheory.Monoidal.Multifunctor
CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapᵣ_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {D : Type u_2} [inst_2 : CategoryTheory.Category.{v_2, u_2} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F : CategoryTheory.Functor C D}
  (η : F.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ⟶ CategoryTheory.MonoidalCategoryStruct.tensorUnit D)
  (X : C),
  (CategoryTheory.Functor.OplaxMonoidal.ofBifunctor.bottomMapᵣ η).app X =
    CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj X) η
-- Lean.Linter.MissingDocs
Lean.Linter.MissingDocs.lintStructField : Lean.Syntax → Lean.Syntax → String → Lean.Elab.Command.CommandElabM Unit
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
Std.Iterators.Types.TakeWhile.mk : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
        Std.IterM m β → Std.Iterators.Types.TakeWhile α m β P
-- Mathlib.Combinatorics.SimpleGraph.Walk.Operations
SimpleGraph.Walk.edges_tail : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} {p : G.Walk u v}, p.tail.edges = p.edges.tail
-- Mathlib.Topology.MetricSpace.Polish
PolishSpace.toSecondCountableTopology : ∀ {α : Type u_3} {h : TopologicalSpace α} [self : PolishSpace α], SecondCountableTopology α
-- Mathlib.Topology.Homeomorph.Lemmas
Fin.continuous_append : ∀ {X : Type u_1} [inst : TopologicalSpace X] (m n : ℕ), Continuous fun p => Fin.append p.1 p.2
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- The elliptic relator `ER(p, q, r, s)` that defines an elliptic net.  -/
IsEllipticNet.rel : {R : Type u_1} → [CommRing R] → (ℤ → R) → ℤ → ℤ → ℤ → ℤ → R
-- Mathlib.Topology.Constructions
Sigma.nhds_eq : ∀ {ι : Type u_5} {σ : ι → Type u_7} [inst : (i : ι) → TopologicalSpace (σ i)] (x : Sigma σ),
  nhds x = Filter.map (Sigma.mk x.fst) (nhds x.snd)
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'₁₂_eq_pullHom_of_chosenPullback₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  (sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃))
  {obj obj' : (i : ι) → ↑(F.obj { as := Opposite.op (X i) })}
  (hom :
    (i j : ι) →
      (F.map (sq i j).p₁.op.toLoc).toFunctor.obj (obj i) ⟶ (F.map (sq i j).p₂.op.toLoc).toFunctor.obj (obj' j))
  (i₁ i₂ i₃ : ι),
  CategoryTheory.Pseudofunctor.DescentData'.pullHom' hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯ =
    CategoryTheory.Pseudofunctor.LocallyDiscreteOpToCat.pullHom (hom i₁ i₂) (sq₃ i₁ i₂ i₃).p₁₂ (sq₃ i₁ i₂ i₃).p₁
      (sq₃ i₁ i₂ i₃).p₂ ⋯ ⋯
-- Mathlib.Analysis.InnerProductSpace.Reproducing
/-- Point evaluation `f ↦ f x` is the adjoint of the kernel function `kerFun H x`.  -/
RKHS.adjoint_kerFun : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {X : Type u_2} {V : Type u_3} [inst_1 : NormedAddCommGroup V]
  [inst_2 : InnerProductSpace 𝕜 V] {H : Type u_4} [inst_3 : NormedAddCommGroup H] [inst_4 : InnerProductSpace 𝕜 H]
  [inst_5 : RKHS 𝕜 H X V] [inst_6 : CompleteSpace H] [inst_7 : CompleteSpace V] (x : X) (f : H),
  (ContinuousLinearMap.adjoint (RKHS.kerFun H x)) f = f x
-- Mathlib.Analysis.InnerProductSpace.Spectrum
_private.Mathlib.Analysis.InnerProductSpace.Spectrum.0.«term⟪_,_⟫» : Lean.ParserDescr
-- Mathlib.Probability.Kernel.Disintegration.Density
ProbabilityTheory.Kernel.measurable_densityProcess : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : MeasurableSpace.CountablyGenerated γ] (κ : ProbabilityTheory.Kernel α (γ × β))
  (ν : ProbabilityTheory.Kernel α γ) (n : ℕ) {s : Set β},
  MeasurableSet s → Measurable fun p => κ.densityProcess ν n p.1 p.2 s
-- Mathlib.Order.Compare
/-- Generate a linear order structure from a preorder and `cmp` function.  -/
linearOrderOfCompares : {α : Type u_1} → [inst : Preorder α] → (cmp : α → α → Ordering) → (∀ (a b : α), (cmp a b).Compares a b) → LinearOrder α
-- Mathlib.Order.CompleteBooleanAlgebra
sSup_inf_eq : ∀ {α : Type u} [inst : Order.Frame α] {s : Set α} {b : α}, sSup s ⊓ b = ⨆ a ∈ s, a ⊓ b
-- Mathlib.Tactic.Ring.Common
/-- Stores all of the normalization procedures on the coefficient type.

`ring` implements these using `norm_num`
`algebra` will implement these using `ring`  -/
Mathlib.Tactic.Ring.Common.RingCompute : {u : Lean.Level} → {α : Q(Type u)} → (Q(«$α») → Type) → Q(CommSemiring «$α») → Type
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.mem_modify : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp], t.WF → ∀ {k k' : α} {f : β k → β k}, k' ∈ t.modify k f ↔ k' ∈ t
-- Init.Data.BitVec.Lemmas
BitVec.toInt.eq_1 : ∀ {n : ℕ} (x : BitVec n), x.toInt = if 2 * x.toNat < 2 ^ n then ↑x.toNat else ↑x.toNat - ↑(2 ^ n)
-- Lean.Data.LOption
Lean.LOption.some.injEq : ∀ {α : Type u} (a a_1 : α), (Lean.LOption.some a = Lean.LOption.some a_1) = (a = a_1)
-- Mathlib.MeasureTheory.Measure.OpenPos
/-- A *closed* measure zero subset is nowhere dense. (Closedness is required: for instance, the
rational numbers are countable (thus have measure zero), but are dense (hence not nowhere dense).)
 -/
IsNowhereDense.of_isClosed_null : ∀ {X : Type u_1} [inst : TopologicalSpace X] [inst_1 : MeasurableSpace X] {s : Set X} {μ : MeasureTheory.Measure X}
  [μ.IsOpenPosMeasure], IsClosed s → μ s = 0 → IsNowhereDense s
-- Mathlib.LinearAlgebra.Contraction
rTensorHomEquivHomRTensor.congr_simp : ∀ (R : Type u_2) (M : Type u_3) (P : Type u_5) (Q : Type u_6) [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid P] [inst_3 : AddCommMonoid Q] [inst_4 : Module R M] [inst_5 : Module R P]
  [inst_6 : Module R Q] [inst_7 : Module.Projective R M] [inst_8 : Module.Finite R M],
  rTensorHomEquivHomRTensor R M P Q = rTensorHomEquivHomRTensor R M P Q
-- Lean.Level
/-- Similar to `mkLevelIMax`, but applies cheap simplifications  -/
Lean.mkLevelIMax' : Lean.Level → Lean.Level → Lean.Level
-- Mathlib.Topology.Homeomorph.Defs
/-- Identity map as a homeomorphism.  -/
Homeomorph.refl : (X : Type u_7) → [inst : TopologicalSpace X] → X ≃ₜ X
-- Mathlib.RingTheory.WittVector.Defs
WittVector.mk'.injEq : ∀ {p : ℕ} {R : Type u_1} (coeff coeff_1 : ℕ → R), ({ coeff := coeff } = { coeff := coeff_1 }) = (coeff = coeff_1)
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.of_smul : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤} {c : ℝ},
  BoxIntegral.Integrable I l (c • f) vol → c ≠ 0 → BoxIntegral.Integrable I l f vol
-- Mathlib.MeasureTheory.Measure.CharacteristicFunction.TaylorExpansion
MeasureTheory.taylorWithinEval_charFun_two_zero : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} [MeasureTheory.IsProbabilityMeasure P]
  {X : Ω → ℝ},
  AEMeasurable X P →
    MeasureTheory.MemLp id 2 (MeasureTheory.Measure.map X P) →
      ∀ (t : ℝ),
        taylorWithinEval (MeasureTheory.charFun (MeasureTheory.Measure.map X P)) 2 Set.univ 0 t =
          1 + ↑(∫ (x : Ω), X x ∂P) * ↑t * Complex.I - ↑(∫ (x : Ω), (X ^ 2) x ∂P) * ↑t ^ 2 / 2
-- Mathlib.RingTheory.Polynomial.Cyclotomic.Basic
Polynomial.int_cyclotomic_rw : ∀ {n : ℕ} (h : n ≠ 0), Polynomial.cyclotomic n ℤ = ⋯.choose
-- Mathlib.Algebra.Module.LinearMap.Polynomial
Matrix.toMvPolynomial.eq_1 : ∀ {m : Type u_1} {n : Type u_2} {R : Type u_4} [inst : Fintype n] [inst_1 : CommSemiring R] (M : Matrix m n R) (i : m),
  M.toMvPolynomial i = ∑ j, (MvPolynomial.monomial fun₀ | j => 1) (M i j)
-- Init.Data.List.MinMaxOn
_private.Init.Data.List.MinMaxOn.0.List.minOn.match_1.eq_1 : ∀ {α : Type u_1} (motive : (l : List α) → l ≠ [] → Sort u_2) (x : α) (xs : List α) (h : x :: xs ≠ [])
  (h_1 : (x : α) → (xs : List α) → (h : x :: xs ≠ []) → motive (x :: xs) h),
  (match x :: xs, h with
    | x :: xs, h => h_1 x xs h) =
    h_1 x xs h
-- Init.SizeOf
Lean.ParserDescr.unary.sizeOf_spec : ∀ (name : Lean.Name) (p : Lean.ParserDescr), sizeOf (Lean.ParserDescr.unary name p) = 1 + sizeOf name + sizeOf p
-- Mathlib.Topology.Category.LightProfinite.AsLimit
LightProfinite.proj_comp_transitionMap' : ∀ (S : LightProfinite) (n : ℕ),
  ⇑(CategoryTheory.ConcreteCategory.hom (S.transitionMap n)) ∘ ⇑(CategoryTheory.ConcreteCategory.hom (S.proj (n + 1))) =
    ⇑(CategoryTheory.ConcreteCategory.hom (S.proj n))
-- Mathlib.MeasureTheory.Order.UpperLower
Set.OrdConnected.nullMeasurableSet : ∀ {ι : Type u_1} [inst : Fintype ι] {s : Set (ι → ℝ)},
  s.OrdConnected → MeasureTheory.NullMeasurableSet s MeasureTheory.volume
-- Mathlib.Data.Fintype.Order
/-- A finite bounded lattice is complete.  -/
Fintype.toCompleteLattice : (α : Type u_2) → [Fintype α] → [inst : Lattice α] → [BoundedOrder α] → CompleteLattice α
-- Mathlib.Algebra.Homology.HomologicalComplex
HomologicalComplex.dFrom_comp_xNextIso_assoc : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V] {c : ComplexShape ι} (C : HomologicalComplex V c) {i j : ι}
  (r : c.Rel i j) {Z : V} (h : C.X j ⟶ Z),
  CategoryTheory.CategoryStruct.comp (C.dFrom i) (CategoryTheory.CategoryStruct.comp (C.xNextIso r).hom h) =
    CategoryTheory.CategoryStruct.comp (C.d i j) h
-- Init.Data.UInt.Lemmas
UInt8.ofFin_toFin : ∀ (n : UInt8), UInt8.ofFin n.toFin = n
-- Mathlib.NumberTheory.Padics.PadicNumbers
Padic.valuation_one : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], Padic.valuation 1 = 0
-- Std.Http.Protocol.H1.Error
/-- Request entity too large.
 -/
Std.Http.Protocol.H1.Error.entityTooLarge : Std.Http.Protocol.H1.Error
-- Mathlib.Topology.Order.Lattice
ContinuousOn.finset_sup' : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeSup L] [ContinuousSup L] {s : Finset ι} {f : ι → X → L} {t : Set X} (hne : s.Nonempty),
  (∀ i ∈ s, ContinuousOn (f i) t) → ContinuousOn (s.sup' hne f) t
-- Mathlib.Topology.Algebra.Module.Spaces.PointwiseConvergenceCLM
PointwiseConvergenceCLM.coeLMₛₗ_apply : ∀ {𝕜₁ : Type u_4} {𝕜₂ : Type u_5} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] (σ : 𝕜₁ →+* 𝕜₂) (E : Type u_7)
  (F : Type u_8) [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : IsTopologicalAddGroup F] [inst_7 : Module 𝕜₁ E] [inst_8 : Module 𝕜₂ F]
  [inst_9 : ContinuousConstSMul 𝕜₂ F] (self : E →SL[σ] F), (PointwiseConvergenceCLM.coeLMₛₗ σ E F) self = ↑self
-- Mathlib.Util.Notation3
Mathlib.Notation3.MatchState.mk : Std.HashMap Lean.Name (Lean.SubExpr × Lean.LocalContext × Lean.LocalInstances) →
  Option (Array (Lean.TSyntax `Batteries.ExtendedBinder.extBinderParenthesized)) →
    Std.HashMap Lean.Name (Array Lean.Term) → Mathlib.Notation3.MatchState
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
le_of_mul_le_mul_left' : ∀ {α : Type u_1} [inst : Mul α] [inst_1 : LE α] [MulLeftReflectLE α] {a b c : α}, a * b ≤ a * c → b ≤ c
-- Mathlib.LinearAlgebra.Prod
LinearMap.range_inl : ∀ (R : Type u) (M : Type v) (M₂ : Type w) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (LinearMap.inl R M M₂).range = (LinearMap.snd R M M₂).ker
-- Mathlib.Analysis.SpecialFunctions.Pow.Real
Real.rpow_sub_intCast' : ∀ {x y : ℝ}, 0 ≤ x → ∀ {n : ℤ}, y - ↑n ≠ 0 → x ^ (y - ↑n) = x ^ y / x ^ n
-- Std.Data.HashMap.Lemmas
Std.HashMap.values_empty : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v}, ∅.values = []
-- Mathlib.CategoryTheory.Bicategory.Kan.IsKan
/-- Two 2-morphisms out of a left Kan lift are equal if their compositions with
each triangle 2-morphism are equal.  -/
CategoryTheory.Bicategory.LeftLift.IsKan.hom_ext : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c : B} {f : b ⟶ a} {g : c ⟶ a}
  {t : CategoryTheory.Bicategory.LeftLift f g} (H : t.IsKan) {k : c ⟶ b} {τ τ' : t.lift ⟶ k},
  CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerRight τ f) =
      CategoryTheory.CategoryStruct.comp t.unit (CategoryTheory.Bicategory.whiskerRight τ' f) →
    τ = τ'
-- Mathlib.Probability.Kernel.Disintegration.Integral
MeasureTheory.Integrable.condKernel_ae : ∀ {α : Type u_1} {Ω : Type u_2} {F : Type u_4} {mα : MeasurableSpace α} [inst : MeasurableSpace Ω]
  [inst_1 : StandardBorelSpace Ω] [inst_2 : Nonempty Ω] [inst_3 : NormedAddCommGroup F]
  {ρ : MeasureTheory.Measure (α × Ω)} [inst_4 : MeasureTheory.IsFiniteMeasure ρ] {f : α × Ω → F},
  MeasureTheory.Integrable f ρ → ∀ᵐ (a : α) ∂ρ.fst, MeasureTheory.Integrable (fun ω => f (a, ω)) (ρ.condKernel a)
-- Lean.Meta.Sym.Arith.MonadCanon
/-- Canonicalize an expression (types, instances, support arguments).
In `SymM`, this is `Sym.canon`. In `PP.M` (diagnostics), this is the identity.
 -/
Lean.Meta.Sym.Arith.MonadCanon.canonExpr : {m : Type → Type} → [self : Lean.Meta.Sym.Arith.MonadCanon m] → Lean.Expr → m Lean.Expr
-- Mathlib.Logic.Embedding.Set
Function.Embedding.coe_sumSet : ∀ {α : Type u_1} {s t : Set α} (h : Disjoint s t), ⇑(Function.Embedding.sumSet h) = Sum.elim Subtype.val Subtype.val
-- Mathlib.Algebra.Star.Subalgebra
StarAlgEquiv.restrictScalars_symm_apply : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : CommSemiring R] [inst_1 : CommSemiring S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : MulAction R S]
  [inst_5 : Module S A] [inst_6 : Module S B] [inst_7 : Module R A] [inst_8 : Module R B] [inst_9 : IsScalarTower R S A]
  [inst_10 : IsScalarTower R S B] [inst_11 : Star A] [inst_12 : Star B] (f : A ≃⋆ₐ[S] B) (a : B),
  (StarAlgEquiv.restrictScalars R f).symm a = f.invFun a
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit_ind : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {ρ : Type w} [inst_2 : ForIn Id ρ α]
  {motive : (Std.DHashMap.Internal.Raw₀ α fun x => Unit) → Prop} (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit)
  (l : ρ),
  motive m →
    (∀ (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) (a : α), motive m → motive (m.insertIfNew a ())) →
      motive ↑(Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Add
Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput.cin : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] → {aig : Std.Sat.AIG α} → Std.Tactic.BVDecide.BVExpr.bitblast.FullAdderInput aig → aig.Ref
-- Init.Data.Fin.Basic
Fin.val_le_of_le : ∀ {n : ℕ} {a b : Fin n}, a ≤ b → ↑a ≤ ↑b
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.IsCommMonObj.mul_comm : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.MonoidalCategory C}
  {inst_2 : CategoryTheory.BraidedCategory C} (X : C) {inst_3 : CategoryTheory.MonObj X}
  [self : CategoryTheory.IsCommMonObj X],
  CategoryTheory.CategoryStruct.comp (β_ X X).hom CategoryTheory.MonObj.mul = CategoryTheory.MonObj.mul
-- Mathlib.CategoryTheory.DinatTrans
CategoryTheory.DinatTrans.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F G : CategoryTheory.Functor Cᵒᵖ (CategoryTheory.Functor C D)} →
          (app : (X : C) → (F.obj (Opposite.op X)).obj X ⟶ (G.obj (Opposite.op X)).obj X) →
            autoParam
                (∀ {X Y : C} (f : X ⟶ Y),
                  CategoryTheory.CategoryStruct.comp ((F.map f.op).app X)
                      (CategoryTheory.CategoryStruct.comp (app X) ((G.obj (Opposite.op X)).map f)) =
                    CategoryTheory.CategoryStruct.comp ((F.obj (Opposite.op Y)).map f)
                      (CategoryTheory.CategoryStruct.comp (app Y) ((G.map f.op).app Y)))
                CategoryTheory.DinatTrans.dinaturality._autoParam →
              CategoryTheory.DinatTrans F G
-- Mathlib.Algebra.DirectSum.Internal
DirectSum.coe_mul_apply_eq_sum_antidiagonal : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : DecidableEq ι] [inst_1 : Semiring R] [inst_2 : SetLike σ R]
  [inst_3 : AddSubmonoidClass σ R] (A : ι → σ) [inst_4 : AddMonoid ι] [inst_5 : Finset.HasAntidiagonal ι]
  [inst_6 : SetLike.GradedMonoid A] (r r' : DirectSum ι fun i => ↥(A i)) (n : ι),
  ↑((r * r') n) = ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, ↑(r ij.1) * ↑(r' ij.2)
-- Mathlib.CategoryTheory.Preadditive.Injective.Preserves
CategoryTheory.Functor.preservesInjectiveObjects_comp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) [F.PreservesInjectiveObjects] [G.PreservesInjectiveObjects],
  (F.comp G).PreservesInjectiveObjects
-- Mathlib.Combinatorics.Matroid.IndepAxioms
/-- Construct an `Matroid` from an independence predicate that agrees with that of some matroid `M`.
This is computable even if `M` is only known existentially, or when `M` exists for different
reasons in different cases. This can also be used to change the independence predicate to a
more useful definitional form.  -/
Matroid.ofExistsMatroid : {α : Type u_1} → (E : Set α) → (Indep : Set α → Prop) → (∃ M, E = M.E ∧ ∀ (I : Set α), M.Indep I ↔ Indep I) → Matroid α
-- Mathlib.FieldTheory.IntermediateField.Adjoin.Basic
/-- algebra isomorphism between `AdjoinRoot` and `F⟮α⟯`  -/
IntermediateField.adjoinRootEquivAdjoin : (F : Type u_1) →
  [inst : Field F] →
    {E : Type u_2} →
      [inst_1 : Field E] → [inst_2 : Algebra F E] → {α : E} → IsIntegral F α → AdjoinRoot (minpoly F α) ≃ₐ[F] ↥F⟮α⟯
-- Mathlib.FieldTheory.IntermediateField.Basic
IntermediateField.extendScalars.orderIso_symm_apply_coe : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (F : IntermediateField K L)
  (E : IntermediateField (↥F) L),
  ↑((RelIso.symm (IntermediateField.extendScalars.orderIso F)) E) = IntermediateField.restrictScalars K E
-- Mathlib.CategoryTheory.Monoidal.Comon_
CategoryTheory.Functor.obj.Δ_def : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] (X : C) [inst_5 : CategoryTheory.ComonObj X],
  CategoryTheory.ComonObj.comul =
    CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.ComonObj.comul)
      (CategoryTheory.Functor.OplaxMonoidal.δ F X X)
-- Mathlib.RingTheory.DividedPowers.Basic
/-- Transfer divided powers under an equivalence (Equiv version)  -/
DividedPowers.equiv : {A : Type u_1} →
  {B : Type u_2} →
    [inst : CommSemiring A] →
      {I : Ideal A} →
        [inst_1 : CommSemiring B] →
          {J : Ideal B} → {e : A ≃+* B} → Ideal.map e I = J → DividedPowers I ≃ DividedPowers J
-- Lean.Meta.LitValues
/-- Check if an expression is an array literal
(i.e. `List.toArray` applied to a nested chain of `List.cons`, ending at a `List.nil`),
where each element is "recognised" by a given function `f : Expr → MetaM (Option α)`,
and return the array of recognised values.
 -/
Lean.Meta.getArrayLitOf? : {α : Type} → Lean.Expr → (Lean.Expr → Lean.MetaM (Option α)) → Lean.MetaM (Option (Array α))
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.instZero.eq_1 : ∀ (A : Type u_2) (B : Type u_3) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B],
  ContinuousAddMonoidHom.instZero A B = { zero := { toAddMonoidHom := 0, continuous_toFun := ⋯ } }
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
/-- The nonsingular condition underlying a nonsingular projective point on `W`.  -/
WeierstrassCurve.Projective.Point.nonsingular : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Projective R} (self : W'.Point), W'.NonsingularLift self.point
-- Mathlib.LinearAlgebra.BilinearForm.Orthogonal
/-- A set of orthogonal vectors `v` with respect to some bilinear form `B` is linearly independent
if for all `i`, `B (v i) (v i) ≠ 0`.  -/
LinearMap.BilinForm.linearIndependent_of_iIsOrtho : ∀ {V : Type u_5} {K : Type u_6} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] {n : Type w}
  {B : LinearMap.BilinForm K V} {v : n → V}, B.iIsOrtho v → (∀ (i : n), (B (v i)) (v i) ≠ 0) → LinearIndependent K v
-- Mathlib.ModelTheory.Basic
Equiv.toEquiv_inducedStructureEquiv : ∀ {L : FirstOrder.Language} {M : Type u_1} {N : Type u_2} [inst : L.Structure M] (e : M ≃ N),
  e.inducedStructureEquiv.toEquiv = e
-- Mathlib.CategoryTheory.EffectiveEpi.Comp
CategoryTheory.effectiveEpi_of_effectiveEpi_epi_comp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {B X Y : C} (f : X ⟶ B) (g : Y ⟶ X)
  [CategoryTheory.Epi g] [CategoryTheory.EffectiveEpi (CategoryTheory.CategoryStruct.comp g f)],
  CategoryTheory.EffectiveEpi f
-- Mathlib.Data.Finset.Powerset
/-- **Formula for the Number of Combinations**  -/
Finset.card_powersetCard : ∀ {α : Type u_1} (n : ℕ) (s : Finset α), (Finset.powersetCard n s).card = s.card.choose n
-- Mathlib.Analysis.Complex.Exponential
Real.exp_sum : ∀ {α : Type u_1} (s : Finset α) (f : α → ℝ), Real.exp (∑ x ∈ s, f x) = ∏ x ∈ s, Real.exp (f x)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.getKey_eq_getKey? : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] (k : α) (l : Std.DTreeMap.Internal.Impl α β)
  {h : Std.DTreeMap.Internal.Impl.contains k l = true}, some (l.getKey k h) = l.getKey? k
-- Mathlib.Analysis.Asymptotics.Lemmas
Asymptotics.isBigO_iff_div_isBoundedUnder : ∀ {𝕜 : Type u_15} [inst : NormedDivisionRing 𝕜] {α : Type u_17} {l : Filter α} {f g : α → 𝕜},
  (∀ᶠ (x : α) in l, g x = 0 → f x = 0) →
    (f =O[l] g ↔ Filter.IsBoundedUnder (fun x1 x2 => x1 ≤ x2) l fun x => ‖f x / g x‖)
-- Init.Data.UInt.Bitwise
UInt8.toNat_shiftRight : ∀ (a b : UInt8), (a >>> b).toNat = a.toNat >>> (b.toNat % 8)