mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine_apply : ∀ {X : AlgebraicGeometry.Scheme} [inst : AlgebraicGeometry.IsAffine X] (I : X.IdealSheafData),
  AlgebraicGeometry.Scheme.IdealSheafData.equivOfIsAffine I = I.ideal ⟨⊤, ⋯⟩
-- Mathlib.Topology.DiscreteQuotient
DiscreteQuotient.fiber_eq : ∀ {X : Type u_2} [inst : TopologicalSpace X] (S : DiscreteQuotient X) (x : X),
  S.proj ⁻¹' {S.proj x} = Set.ofPred (S.toSetoid x)
-- Mathlib.Algebra.Group.End
MulAut.coe_one : ∀ (M : Type u_2) [inst : Mul M], ⇑1 = id
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instAddRightCancelSemigroup : {α : Type u_1} → [AddRightCancelSemigroup α] → AddRightCancelSemigroup (Colex α)
-- Mathlib.Order.RelSeries
SetRel.IsWellFounded.inv_of_finiteDimensional : ∀ {α : Type u_1} (r : SetRel α α) [r.FiniteDimensional], r.inv.IsWellFounded
-- Mathlib.MeasureTheory.Constructions.HaarToSphere
/-- A ball of radius `ε` on the unit sphere in a real normed space
has measure at least `toSphereBallBound n ε * μ (ball 0 1)`,
where `n` is the dimension of the space,
`toSphereBallBound n ε` is a lower estimate that depends only on the dimension and `ε`,
which is positive for positive `n` and `ε`.

This is a version stated in terms `MeasureTheory.Measure.real`.  -/
MeasureTheory.Measure.toSphereBallBound_mul_measureReal_unitBall_le_toSphere_ball : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E]
  (μ : MeasureTheory.Measure E) [BorelSpace E] [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure] {ε : ℝ},
  0 < ε →
    ∀ (x : ↑(Metric.sphere 0 1)),
      ↑(MeasureTheory.Measure.toSphereBallBound (Module.finrank ℝ E) ε) * μ.real (Metric.ball 0 1) ≤
        μ.toSphere.real (Metric.ball x ε)
-- Mathlib.Topology.Semicontinuity.Defs
/-- A function `f : α → Set β` is upper hemicontinuous on a set `s` if, whenever `x ∈ s` and `t` is
a neighborhood of `f x`, then `t` is a neighborhood of `f x'` for all `x'` sufficiently close to
`x` within `s`.  -/
UpperHemicontinuousOn : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [TopologicalSpace β] → (α → Set β) → Set α → Prop
-- Mathlib.Data.Set.Lattice.Image
Set.iUnion_image_left : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (f : α → β → γ) {s : Set α} {t : Set β},
  ⋃ a ∈ s, f a '' t = Set.image2 f s t
-- Mathlib.Condensed.Discrete.Basic
/-- A version of `LightCondensed.discrete_underlying_adj` in the `LightCondSet` namespace  -/
LightCondSet.discreteUnderlyingAdj : LightCondSet.discrete ⊣ LightCondSet.underlying
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
CategoryTheory.kernelCokernelCompSequence.δ_fac : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {X Y Z : C} (f : X ⟶ Y)
  (g : Y ⟶ Z),
  CategoryTheory.kernelCokernelCompSequence.δ f g =
    -CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι g) (CategoryTheory.Limits.cokernel.π f)
-- Mathlib.RingTheory.Extension.Cotangent.Basis
/-- The backwards direction of the isomorphism `S ⊗[T] J/J² ≃ₗ[S] I/I²`.  -/
_private.Mathlib.RingTheory.Extension.Cotangent.Basis.0.Algebra.Generators.PresentationOfFreeCotangent.Aux.tensorCotangentInv : {R : Type u_1} →
  {S : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : Algebra R S] →
          {ι : Type u_4} →
            {P : Algebra.Generators R S ι} →
              {σ : Type u_5} →
                {b : Module.Basis σ S P.toExtension.Cotangent} →
                  (D : Algebra.Generators.PresentationOfFreeCotangent.Aux✝ P b) →
                    P.toExtension.Cotangent →ₗ[S]
                      TensorProduct (Algebra.Generators.PresentationOfFreeCotangent.Aux.T✝ D) S
                        (Algebra.Generators.PresentationOfFreeCotangent.Aux.presLeft✝ D).toExtension.Cotangent
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.size_add_size_eq_size_union_add_size_inter : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet α cmp} [Std.TransCmp cmp],
  t₁.size + t₂.size = (t₁ ∪ t₂).size + (t₁ ∩ t₂).size
-- Mathlib.Topology.UniformSpace.ProdApproximation
/-- A continuous function on `X × Y`, taking values in a ring `R` equipped with a uniformity
compatible with addition, can be uniformly approximated by sums of functions of the form
`(x, y) ↦ f x * g y`.

Note that no assumption is needed relating the multiplication on `R` to the uniformity.  -/
ContinuousMap.exists_finite_sum_mul_approximation_of_mem_uniformity : ∀ {X : Type u_1} {Y : Type u_2} {R : Type u_3} [inst : TopologicalSpace X] [TotallyDisconnectedSpace X] [T2Space X]
  [CompactSpace X] [inst_4 : TopologicalSpace Y] [CompactSpace Y] [inst_6 : Ring R] [inst_7 : UniformSpace R]
  [IsUniformAddGroup R] (f : C(X × Y, R)) {S : Set (R × R)},
  S ∈ uniformity R → ∃ n g h, ∀ (x : X) (y : Y), (f (x, y), ∑ i, (g i) x * (h i) y) ∈ S
-- Mathlib.Order.Filter.AtTopBot.Basic
Filter.HasAntitoneBasis.tendsto : ∀ {ι : Type u_1} {α : Type u_3} [inst : Preorder ι] {l : Filter α} {s : ι → Set α},
  l.HasAntitoneBasis s → ∀ {φ : ι → α}, (∀ (i : ι), φ i ∈ s i) → Filter.Tendsto φ Filter.atTop l
-- Mathlib.Computability.AkraBazzi.SumTransform
AkraBazziRecurrence.eventually_one_add_smoothingFn_r_pos : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r),
  ∀ᶠ (n : ℕ) in Filter.atTop, ∀ (i : α), 0 < 1 + AkraBazziRecurrence.smoothingFn ↑(r i n)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.deriv_cos' : deriv Real.cos = fun x => -Real.sin x
-- Mathlib.MeasureTheory.Integral.IntegrableOn
MeasureTheory.IntegrableAtFilter.inf_ae_iff : ∀ {α : Type u_1} {ε : Type u_3} {mα : MeasurableSpace α} {f : α → ε} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace ε] [inst_1 : ContinuousENorm ε] {l : Filter α},
  MeasureTheory.IntegrableAtFilter f (l ⊓ MeasureTheory.ae μ) μ ↔ MeasureTheory.IntegrableAtFilter f l μ
-- Init.Data.SInt.Lemmas
Int32.lt_or_eq_of_le : ∀ {a b : Int32}, a ≤ b → a < b ∨ a = b
-- Lean.Elab.App
/-- Return `true` if the next argument to be processed is the outparam of a local instance, and it the result type
of the function.

For example, suppose we have the class
```lean
class Get (Cont : Type u) (Idx : Type v) (Elem : outParam (Type w)) where
  get (xs : Cont) (i : Idx) : Elem
```
And the current value of `fType` is
```
{Cont : Type u_1} → {Idx : Type u_2} → {Elem : Type u_3} → [self : Get Cont Idx Elem] → Cont → Idx → Elem
```
then the result returned by this method is `false` since `Cont` is not the output param of any local instance.
Now assume `fType` is
```
{Elem : Type u_3} → [self : Get Cont Idx Elem] → Cont → Idx → Elem
```
then, the method returns `true` because `Elem` is an output parameter for the local instance `[self : Get Cont Idx Elem]`.

Remark: if `resultIsOutParamSupport` is `false`, this method returns `false`.
 -/
_private.Lean.Elab.App.0.Lean.Elab.Term.ElabAppArgs.isNextOutParamOfLocalInstanceAndResult : Lean.Elab.Term.ElabAppArgs.M Bool
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.ι_evalHom : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)) (U : (TopologicalSpace.OpenNhds x)ᵒᵖ),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.colimit.ι
        ((TopologicalSpace.OpenNhds.inclusion x).op.comp (smoothSheafCommRing IM I M R).presheaf) U)
      (smoothSheafCommRing.evalHom IM I M R x) =
    smoothSheafCommRing.evalAt IM I M R x (Opposite.unop U)
-- Mathlib.Probability.Decision.BayesEstimator
ProbabilityTheory.IsArgminEstimator.mk : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧} [inst : StandardBorelSpace Θ]
  [inst_1 : Nonempty Θ] {𝓨 : Type u_4} [inst_2 : MeasurableSpace 𝓨] {ℓ : Θ → 𝓨 → ENNReal}
  {P : ProbabilityTheory.Kernel Θ 𝓧} [inst_3 : ProbabilityTheory.IsFiniteKernel P] {π : MeasureTheory.Measure Θ}
  [inst_4 : MeasureTheory.IsFiniteMeasure π] {f : 𝓧 → 𝓨},
  Measurable f →
    (∀ᵐ (x : 𝓧) ∂π.bind ⇑P,
        ∫⁻ (θ : Θ), ℓ θ (f x) ∂(ProbabilityTheory.posterior P π) x =
          ⨅ y, ∫⁻ (θ : Θ), ℓ θ y ∂(ProbabilityTheory.posterior P π) x) →
      ProbabilityTheory.IsArgminEstimator ℓ P π f
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum.eq_1 : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] (s : Finset α) (f : α → β)
  (comm : (↑s).Pairwise (Function.onFun AddCommute f)), s.noncommSum f comm = (Multiset.map f s.val).noncommSum ⋯
-- Mathlib.LinearAlgebra.SpecialLinearGroup
SpecialLinearGroup.det_coe : ∀ {R : Type u_1} {V : Type u_2} [inst : CommRing R] [inst_1 : AddCommGroup V] [inst_2 : Module R V]
  (A : SpecialLinearGroup R V), LinearEquiv.det ↑A = 1
-- Mathlib.Lean.Meta.RefinedDiscrTree.Basic
/-- Return values, at a leaf  -/
Lean.Meta.RefinedDiscrTree.Trie.values : {α : Type} → Lean.Meta.RefinedDiscrTree.Trie α → Array α
-- Mathlib.Topology.Order.Filter
Filter.tendsto_nhds_atBot : ∀ {X : Type u_2} [inst : TopologicalSpace X] [inst_1 : PartialOrder X] [OrderTopology X] [NoMinOrder X],
  Filter.Tendsto nhds Filter.atBot (nhds Filter.atBot)
-- Mathlib.Data.Set.Lattice
Set.biInter_and' : ∀ {α : Type u_1} {ι : Sort u_5} {ι' : Sort u_6} (p : ι' → Prop) (q : ι → ι' → Prop)
  (s : (x : ι) → (y : ι') → p y ∧ q x y → Set α),
  ⋂ x, ⋂ y, ⋂ (h : p y ∧ q x y), s x y h = ⋂ y, ⋂ (hy : p y), ⋂ x, ⋂ (hx : q x y), s x y ⋯
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.mulR.injEq : ∀ (a : Nat.Internal.Linear.Expr) (k : ℕ) (a_1 : Nat.Internal.Linear.Expr) (k_1 : ℕ),
  (a.mulR k = a_1.mulR k_1) = (a = a_1 ∧ k = k_1)
-- Mathlib.CategoryTheory.Abelian.DiagramLemmas.KernelCokernelComp
/-- If `f : X ⟶ Y` and `g : Y ⟶ Z` are composable morphisms,
this is the morphism `X ⊞ Y ⟶ Y ⊞ Z` given by the matrix
```
(f  -𝟙 Y)
(0     g)
```
 -/
CategoryTheory.kernelCokernelCompSequence.φ : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] → {X Y Z : C} → (X ⟶ Y) → (Y ⟶ Z) → (X ⊞ Y ⟶ Y ⊞ Z)
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.prodIsoProd_inv_snd : ∀ (X Y : TopCat),
  CategoryTheory.CategoryStruct.comp (X.prodIsoProd Y).inv CategoryTheory.Limits.prod.snd = TopCat.prodSnd
-- Mathlib.Lean.Meta.RefinedDiscrTree.Initialize
/-- The reference to the `RefinedDiscrTree`.  -/
Lean.Meta.RefinedDiscrTree.ModuleDiscrTreeRef.ref : {α : Type} → Lean.Meta.RefinedDiscrTree.ModuleDiscrTreeRef α → IO.Ref (Lean.Meta.RefinedDiscrTree α)
-- Mathlib.LinearAlgebra.Dimension.StrongRankCondition
strongRankCondition_iff_forall_zero_lt_finrank : ∀ {R : Type u} [inst : Semiring R] [Nontrivial R], StrongRankCondition R ↔ ∀ n > 0, 0 < Module.finrank R (Fin n → R)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.CoordinateRing.instIsScalarTowerPolynomial : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R}, IsScalarTower R (Polynomial R) W'.CoordinateRing
-- Mathlib.RingTheory.Congruence.Hom
RingCon.liftₐEquiv_symm_apply_coe : ∀ {M : Type u_1} {P : Type u_3} {R : Type u_4} [inst : CommSemiring R] [inst_1 : Semiring M] [inst_2 : Algebra R M]
  [inst_3 : Semiring P] [inst_4 : Algebra R P] (c : RingCon M) (F : c.Quotient →ₐ[R] P),
  ↑(c.liftₐEquiv.symm F) = F.comp (RingCon.mkₐ R c)
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonProd : {α : Type u_1} → {β : Type u_2} → [Lean.ToJson α] → [Lean.ToJson β] → Lean.ToJson (α × β)
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.comp_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N O : CategoryTheory.Mon C} (f : M.Hom N) (g : N.Hom O),
  (CategoryTheory.Mon.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
AddSubgroup.op.eq_1 : ∀ {G : Type u_2} [inst : AddGroup G] (H : AddSubgroup G),
  H.op = { carrier := AddOpposite.unop ⁻¹' ↑H, add_mem' := ⋯, zero_mem' := ⋯, neg_mem' := ⋯ }
-- Mathlib.Analysis.MeanInequalities
Real.geom_mean_le_arith_mean2_weighted : ∀ {w₁ w₂ p₁ p₂ : ℝ}, 0 ≤ w₁ → 0 ≤ w₂ → 0 ≤ p₁ → 0 ≤ p₂ → w₁ + w₂ = 1 → p₁ ^ w₁ * p₂ ^ w₂ ≤ w₁ * p₁ + w₂ * p₂
-- Mathlib.Tactic.CrossRefAttribute
/-- The `#lmfdb_tags` command retrieves all declarations that have the `lmfdb` attribute.

For each found declaration, it prints a line
```
'declaration_name' corresponds to tag 'declaration_tag'.
```
The variant `#lmfdb_tags!` also adds the theorem statement (for theorems)
or declaration type (for definitions, structures, instances, etc.) after each summary line.
 -/
Mathlib.CrossRef.lmfdbTags : Lean.ParserDescr
-- Lean.PrettyPrinter.Formatter
Lean.PrettyPrinter.Formatter.throwBacktrack : {α : Type} → Lean.PrettyPrinter.FormatterM α
-- Mathlib.Data.Nat.Squarefree
Nat.instDecidablePredSquarefree : DecidablePred Squarefree
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Deriv
Real.hasStrictDerivAt_cos : ∀ (x : ℝ), HasStrictDerivAt Real.cos (-Real.sin x) x
-- Std.Http.Data.Status
/-- 403 Forbidden
 -/
Std.Http.Status.forbidden : Std.Http.Status
-- Mathlib.CategoryTheory.Filtered.FinallySmall
/-- If `C` is a locally small filtered finally small category,
this is a final functor from a small filtered category.  -/
CategoryTheory.FinallySmall.fromFilteredFinalModel : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.IsFiltered C] →
      [inst_2 : CategoryTheory.LocallySmall.{w, v, u} C] →
        [inst_3 : CategoryTheory.FinallySmall C] →
          CategoryTheory.Functor (CategoryTheory.FinallySmall.FilteredFinalModel C) C
-- Mathlib.Algebra.Group.Equiv.Defs
/-- The identity map is a multiplicative isomorphism.  -/
MulEquiv.refl : (M : Type u_9) → [inst : Mul M] → M ≃* M
-- Mathlib.AlgebraicGeometry.Limits
AlgebraicGeometry.Scheme.eq_emptyTo : ∀ {X : AlgebraicGeometry.Scheme} (f : ∅ ⟶ X), f = X.emptyTo
-- Mathlib.Analysis.Meromorphic.Basic
/-- The singular set of a meromorphic function is countable.
 -/
MeromorphicOn.countable_compl_analyticAt_inter : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {f : 𝕜 → E} {U : Set 𝕜} [SecondCountableTopology 𝕜] [CompleteSpace E],
  MeromorphicOn f U → ({z | AnalyticAt 𝕜 f z}ᶜ ∩ U).Countable
-- Mathlib.CategoryTheory.Monoidal.Bimon_
/-- A bimonoid object in a braided category `C` is a comonoid object in the (monoidal)
category of monoid objects in `C`.
 -/
CategoryTheory.Bimon : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] → [CategoryTheory.BraidedCategory C] → Type (max (max u₁ v₁) v₁)
-- Mathlib.Tactic.Sat.FromLRAT
/-- A clause is a list of literals, thought of as a disjunction like `a ∨ b ∨ ¬c`.  -/
Sat.Clause : Type
-- Std.Time.Internal.Bounded
/-- Convert a `Nat` to a `Bounded.LE` using the lower boundary too.
 -/
Std.Time.Internal.Bounded.LE.ofNat' : {lo hi : ℕ} → (val : ℕ) → lo ≤ val ∧ val ≤ hi → Std.Time.Internal.Bounded.LE ↑lo ↑hi
-- Mathlib.Analysis.Calculus.InverseFunctionTheorem.FDeriv
/-- If a function has an invertible strict derivative at all points, then it is an open map.  -/
isOpenMap_of_hasStrictFDerivAt_equiv : ∀ {𝕜 : 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] [CompleteSpace E]
  {f : E → F} {f' : E → E ≃L[𝕜] F}, (∀ (x : E), HasStrictFDerivAt f (↑(f' x)) x) → IsOpenMap f
-- Mathlib.Algebra.Order.Field.Basic
inv_pow_le_inv_pow_of_le : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a : α} [IsStrictOrderedRing α],
  1 ≤ a → ∀ {m n : ℕ}, m ≤ n → (a ^ n)⁻¹ ≤ (a ^ m)⁻¹
-- Init.Data.Int.Linear
Int.Internal.Linear.norm_eq_coeff' : ∀ (ctx : Int.Internal.Linear.Context) (p p' : Int.Internal.Linear.Poly) (k : ℤ),
  p = p'.mul k → k > 0 → (Int.Internal.Linear.Poly.denote ctx p = 0 ↔ Int.Internal.Linear.Poly.denote ctx p' = 0)
-- Mathlib.Data.WSeq.Relation
Stream'.WSeq.join_append : ∀ {α : Type u} (S T : Stream'.WSeq (Stream'.WSeq α)), (S.append T).join ~ʷ S.join.append T.join
-- Mathlib.Data.ENat.BigOperators
/-- A sum is finite iff all summands are finite.  -/
ENat.sum_lt_top : ∀ {α : Type u_1} {s : Finset α} {f : α → ℕ∞}, ∑ a ∈ s, f a < ⊤ ↔ ∀ a ∈ s, f a < ⊤
-- Mathlib.Analysis.SpecialFunctions.Log.Monotone
Real.log_div_self_antitoneOn : AntitoneOn (fun x => Real.log x / x) (Set.Ici (Real.exp 1))
-- Std.Sat.AIG.RefVec
Std.Sat.AIG.BinaryRefVec.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α} {len : ℕ}
  {lhs rhs lhs_1 rhs_1 : aig.RefVec len},
  { lhs := lhs, rhs := rhs } = { lhs := lhs_1, rhs := rhs_1 } → lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.Order.WellFoundedSet
Set.Finite.partiallyWellOrderedOn : ∀ {α : Type u_2} {r : α → α → Prop} {s : Set α} [Std.Refl r], s.Finite → s.PartiallyWellOrderedOn r
-- Mathlib.Analysis.Normed.Field.Approximation
/-- **Continuity of Roots.** A variation of
`Polynomial.exists_roots_norm_sub_lt_of_norm_coeff_sub_lt` allowing roots of `g` lives in a
field extension.  -/
Polynomial.exists_aroots_norm_sub_lt_of_norm_coeff_sub_lt : ∀ {K : Type u_1} {L : Type u_2} [inst : NormedField K] [inst_1 : NormedField L] [inst_2 : NormedAlgebra K L]
  {f g : Polynomial K} {ε : ℝ},
  0 < ε →
    ∀ {a : L},
      (Polynomial.aeval a) f = 0 →
        f.Monic →
          g.Monic →
            g.natDegree = f.natDegree →
              (∀ (i : ℕ), ‖g.coeff i - f.coeff i‖ < ε) →
                (Polynomial.map (algebraMap K L) g).Splits →
                  ∃ b ∈ g.aroots L, ‖a - b‖ < ((↑f.natDegree + 1) * ε) ^ (↑f.natDegree)⁻¹ * max ‖a‖ 1
-- Init.Data.Float.Float32
Float32.ofModel.sizeOf_spec : ∀ (toModel : Float32.Model), sizeOf { toModel := toModel } = 1 + sizeOf toModel
-- Init.Data.Fin.Fold
_private.Init.Data.Fin.Fold.0.Fin.foldl_loop : ∀ {α : Sort u_1} {n i : ℕ} (f : α → Fin (n + 1) → α) (x : α) (h : i < n + 1),
  Fin.foldl.loop (n + 1) f x i = Fin.foldl.loop n (fun x j => f x j.succ) (f x ⟨i, h⟩) i
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- The mates equivalence commutes with this composition, essentially by `mateEquiv_vcomp`.  -/
CategoryTheory.Bicategory.conjugateEquiv_mateEquiv_vcomp : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d : B} {g : a ⟶ c} {h : b ⟶ d} {l₁ : a ⟶ b} {r₁ : b ⟶ a}
  {l₂ : a ⟶ b} {r₂ : b ⟶ a} {l₃ : c ⟶ d} {r₃ : d ⟶ c} (adj₁ : CategoryTheory.Bicategory.Adjunction l₁ r₁)
  (adj₂ : CategoryTheory.Bicategory.Adjunction l₂ r₂) (adj₃ : CategoryTheory.Bicategory.Adjunction l₃ r₃) (α : l₂ ⟶ l₁)
  (β : CategoryTheory.CategoryStruct.comp g l₃ ⟶ CategoryTheory.CategoryStruct.comp l₂ h),
  (CategoryTheory.Bicategory.mateEquiv adj₁ adj₃) (CategoryTheory.Bicategory.leftAdjointConjugateSquare.vcomp α β) =
    CategoryTheory.Bicategory.rightAdjointConjugateSquare.vcomp ((CategoryTheory.Bicategory.conjugateEquiv adj₁ adj₂) α)
      ((CategoryTheory.Bicategory.mateEquiv adj₂ adj₃) β)
-- Mathlib.RingTheory.Nilpotent.Lemmas
nilpotent_iff_mem_prime : ∀ {R : Type u_1} [inst : CommSemiring R] {x : R}, IsNilpotent x ↔ ∀ (J : Ideal R), J.IsPrime → x ∈ J
-- Mathlib.CategoryTheory.FiberedCategory.HomLift
CategoryTheory.IsHomLift.domain_eq : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₂} 𝒳] [inst_1 : CategoryTheory.Category.{v₂, u₁} 𝒮]
  (p : CategoryTheory.Functor 𝒳 𝒮) {R S : 𝒮} {a b : 𝒳} (f : R ⟶ S) (φ : a ⟶ b) [p.IsHomLift f φ], p.obj a = R
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.fromCostructuredArrow_obj_π : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor J C) (c : CategoryTheory.CostructuredArrow (CategoryTheory.Functor.const J) F),
  ((CategoryTheory.Limits.Cone.fromCostructuredArrow F).obj c).π = c.hom
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictlyUnitary
/-- A helper structure that bundles the necessary data to
construct a `StrictlyUnitaryPseudofunctor` without specifying the redundant
field `mapId`  -/
CategoryTheory.StrictlyUnitaryPseudofunctorCore : (B : Type u₁) →
  [CategoryTheory.Bicategory B] →
    (C : Type u₂) → [CategoryTheory.Bicategory C] → Type (max (max (max (max (max u₁ u₂) v₁) v₂) w₁) w₂)
-- Mathlib.Analysis.Convex.EGauge
egauge_eq_zero_iff : ∀ {𝕜 : Type u_1} [inst : NormedDivisionRing 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {s : Set E} {x : E}, egauge 𝕜 s x = 0 ↔ ∃ᶠ (c : 𝕜) in nhds 0, x ∈ c • s
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey!_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : BEq α] [Std.LawfulBEqCmp cmp] [inst_3 : Inhabited α] {l : List (α × β)} {k : α},
  (List.map Prod.fst l).contains k = false → (t.insertMany l).getKey! k = t.getKey! k
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.coe_eq_univ : ∀ {α : Type u_1} [inst : LE α] {s : UpperSet α}, ↑s = Set.univ ↔ s = ⊥
-- Lean.Elab.Tactic.Omega.Core
/-- The justification of a derived fact.  -/
Lean.Elab.Tactic.Omega.Fact.justification : (self : Lean.Elab.Tactic.Omega.Fact) → Lean.Elab.Tactic.Omega.Justification self.constraint self.coeffs
-- Mathlib.MeasureTheory.Integral.TorusIntegral
/-- The n-dimensional exponential map $θ_i ↦ c + R e^{θ_i*I}, θ ∈ ℝⁿ$ representing
a torus in `ℂⁿ` with center `c ∈ ℂⁿ` and generalized radius `R ∈ ℝⁿ`, so we can adjust
it to every n axis.  -/
torusMap : {n : ℕ} → (Fin n → ℂ) → (Fin n → ℝ) → (Fin n → ℝ) → Fin n → ℂ
-- Mathlib.Data.Finsupp.SMulWithZero
Finsupp.isScalarTower : ∀ (α : Type u_1) (M : Type u_5) {R : Type u_11} {S : Type u_12} [inst : Zero M] [inst_1 : SMulZeroClass R M]
  [inst_2 : SMulZeroClass S M] [inst_3 : SMul R S] [IsScalarTower R S M], IsScalarTower R S (α →₀ M)
-- Mathlib.RingTheory.FreeCommRing
FreeCommRing.of_ne_zero : ∀ {α : Type u} (x : α), FreeCommRing.of x ≠ 0
-- Mathlib.Topology.VectorBundle.Hom
/-- The continuous `σ`-semilinear maps between two vector bundles form a vector bundle.  -/
Bundle.ContinuousLinearMap.vectorBundle : ∀ {𝕜₁ : Type u_1} [inst : NontriviallyNormedField 𝕜₁] {𝕜₂ : Type u_2} [inst_1 : NontriviallyNormedField 𝕜₂]
  (σ : 𝕜₁ →+* 𝕜₂) {B : Type u_3} (F₁ : Type u_4) [inst_2 : NormedAddCommGroup F₁] [inst_3 : NormedSpace 𝕜₁ F₁]
  (E₁ : B → Type u_5) [inst_4 : (x : B) → AddCommGroup (E₁ x)] [inst_5 : (x : B) → Module 𝕜₁ (E₁ x)]
  [inst_6 : TopologicalSpace (Bundle.TotalSpace F₁ E₁)] (F₂ : Type u_6) [inst_7 : NormedAddCommGroup F₂]
  [inst_8 : NormedSpace 𝕜₂ F₂] (E₂ : B → Type u_7) [inst_9 : (x : B) → AddCommGroup (E₂ x)]
  [inst_10 : (x : B) → Module 𝕜₂ (E₂ x)] [inst_11 : TopologicalSpace (Bundle.TotalSpace F₂ E₂)]
  [inst_12 : TopologicalSpace B] [inst_13 : (x : B) → TopologicalSpace (E₁ x)] [inst_14 : FiberBundle F₁ E₁]
  [inst_15 : VectorBundle 𝕜₁ F₁ E₁] [inst_16 : (x : B) → TopologicalSpace (E₂ x)] [inst_17 : FiberBundle F₂ E₂]
  [inst_18 : VectorBundle 𝕜₂ F₂ E₂] [inst_19 : ∀ (x : B), IsTopologicalAddGroup (E₂ x)]
  [inst_20 : ∀ (x : B), ContinuousSMul 𝕜₂ (E₂ x)] [inst_21 : RingHomIsometric σ],
  VectorBundle 𝕜₂ (F₁ →SL[σ] F₂) fun x => E₁ x →SL[σ] E₂ x
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalSubalgebraClass.coe_subtype : ∀ {S : Type u_1} {R : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : SetLike S A] [inst_4 : NonUnitalSubsemiringClass S A] [hSR : SMulMemClass S R A]
  (s : S), ⇑(NonUnitalSubalgebraClass.subtype s) = Subtype.val
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.coeffs_nonempty_iff : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R}, p.coeffs.Nonempty ↔ p ≠ 0
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
pos_of_lt_add_right : ∀ {α : Type u_1} [inst : AddZeroClass α] [inst_1 : LT α] [AddLeftReflectLT α] {a b : α}, a < a + b → 0 < b