mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.Matroid.Rank.ENat
/-- A version of submodularity applied to the complements of two sets.  -/
Matroid.eRk_compl_union_add_eRk_compl_inter_le : ∀ {α : Type u_1} (M : Matroid α) (X Y : Set α),
  M.eRk (M.E \ (X ∪ Y)) + M.eRk (M.E \ (X ∩ Y)) ≤ M.eRk (M.E \ X) + M.eRk (M.E \ Y)
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
NumberField.mixedEmbedding.fundamentalCone.compactSet.congr_simp : ∀ (K : Type u_1) [inst : Field K] [inst_1 : NumberField K] (a a_1 : NumberField.mixedEmbedding.realSpace K),
  a = a_1 →
    NumberField.mixedEmbedding.fundamentalCone.compactSet K a =
      NumberField.mixedEmbedding.fundamentalCone.compactSet K a_1
-- Std.Data.DTreeMap.Internal.Queries
/-- Implementation detail of the tree map  -/
Std.DTreeMap.Internal.Impl.Const.getEntryLT? : {α : Type u} → {β : Type v} → [Ord α] → α → (Std.DTreeMap.Internal.Impl α fun x => β) → Option (α × β)
-- Mathlib.Algebra.MvPolynomial.Eval
MvPolynomial.aevalTower_comp_algebraMap : ∀ {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),
  (↑(MvPolynomial.aevalTower g y)).comp (algebraMap R (MvPolynomial σ R)) = ↑g
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- An inequality constraint and its justification/proof.  -/
Lean.Meta.Grind.Arith.Cutsat.LeCnstr : Type
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.deriv_derivWeierstrassPExcept_self : ∀ (L : PeriodPair) (l : ℂ), deriv (L.derivWeierstrassPExcept l) l = 6 * L.sumInvPow l 4
-- Mathlib.Data.Multiset.FinsetOps
Multiset.mem_ndinsert_of_mem : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Multiset α}, a ∈ s → a ∈ Multiset.ndinsert b s
-- Mathlib.MeasureTheory.Measure.ResolventTransform
MeasureTheory.analyticOn_resolventTransform : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [HereditarilyLindelofSpace 𝕜] [CompleteSpace 𝕜]
  [inst_3 : MeasurableSpace 𝕜] [BorelSpace 𝕜] [inst_5 : NormedAlgebra 𝕜 ℂ] {μ : MeasureTheory.Measure 𝕜}
  [MeasureTheory.IsFiniteMeasure μ], AnalyticOn ℂ (MeasureTheory.resolventTransform μ) (⇑(algebraMap 𝕜 ℂ) '' μ.support)ᶜ
-- Mathlib.GroupTheory.Perm.Centralizer
Equiv.Perm.OnCycleFactors.kerParam_range_le_centralizer : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : Fintype α] {g : Equiv.Perm α},
  (Equiv.Perm.OnCycleFactors.kerParam g).range ≤ Subgroup.centralizer {g}
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Jordan
MeasureTheory.SignedMeasure.of_inter_eq_of_symmDiff_eq_zero_positive : ∀ {α : Type u_1} [inst : MeasurableSpace α] {s : MeasureTheory.SignedMeasure α} {u v w : Set α},
  MeasurableSet u →
    MeasurableSet v →
      MeasurableSet w →
        MeasureTheory.VectorMeasure.restrict 0 u ≤ MeasureTheory.VectorMeasure.restrict s u →
          MeasureTheory.VectorMeasure.restrict 0 v ≤ MeasureTheory.VectorMeasure.restrict s v →
            s (symmDiff u v) = 0 → s (w ∩ u) = s (w ∩ v)
-- Mathlib.CategoryTheory.EffectiveEpi.Comp
/-- An effective epi family precomposed by a family of split epis is effective epimorphic.
This version takes an explicit section to the split epis, and is mainly used to define
`effectiveEpiStructCompOfEffectiveEpiSplitEpi`,
which takes a `IsSplitEpi` instance instead.
 -/
CategoryTheory.effectiveEpiFamilyStructCompOfEffectiveEpiSplitEpi' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {α : Type u_2} →
      {B : C} →
        {X Y : α → C} →
          (f : (a : α) → X a ⟶ B) →
            (g : (a : α) → Y a ⟶ X a) →
              (i : (a : α) → X a ⟶ Y a) →
                (∀ (a : α), CategoryTheory.CategoryStruct.comp (i a) (g a) = CategoryTheory.CategoryStruct.id (X a)) →
                  [CategoryTheory.EffectiveEpiFamily X f] →
                    CategoryTheory.EffectiveEpiFamilyStruct Y fun a => CategoryTheory.CategoryStruct.comp (g a) (f a)
-- Std.Sync.Semaphore
/-- Releases one permit and resolves one waiting acquirer, if any.
 -/
Std.Semaphore.release : Std.Semaphore → BaseIO Unit
-- Mathlib.Algebra.Group.Support
Function.mulSupport_pow : ∀ {α : Type u_1} {M : Type u_2} [inst : Monoid M] (f : α → M) (n : ℕ),
  (Function.mulSupport fun x => f x ^ n) ⊆ Function.mulSupport f
-- Init.Data.Vector.InsertIdx
Vector.getElem_insertIdx : ∀ {α : Type u} {n : ℕ} {xs : Vector α n} {x : α} {i k : ℕ} (w : i ≤ n) (h : k < n + 1),
  (xs.insertIdx i x w)[k] = if h₁ : k < i then xs[k] else if h₂ : k = i then x else xs[k - 1]
-- Mathlib.Analysis.InnerProductSpace.Orthogonal
Submodule.IsOrtho.comap : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : NormedAddCommGroup F] [inst_4 : InnerProductSpace 𝕜 F] (f : E →ₗᵢ[𝕜] F)
  {U V : Submodule 𝕜 F}, U ⟂ V → Submodule.comap (↑f) U ⟂ Submodule.comap (↑f) V
-- Mathlib.MeasureTheory.VectorMeasure.Basic
MeasureTheory.VectorMeasure.instSMul : {α : Type u_1} →
  {m : MeasurableSpace α} →
    {M : Type u_3} →
      [inst : AddCommMonoid M] →
        [inst_1 : TopologicalSpace M] →
          {R : Type u_4} →
            [inst_2 : Semiring R] →
              [inst_3 : DistribMulAction R M] → [ContinuousConstSMul R M] → SMul R (MeasureTheory.VectorMeasure α M)
-- Mathlib.Topology.Algebra.Ring.Basic
NonUnitalSubring.isClosed_topologicalClosure : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalRing R] [inst_2 : IsSemitopologicalRing R]
  (s : NonUnitalSubring R), IsClosed ↑s.topologicalClosure
-- Mathlib.Analysis.Convex.Gauge
exists_lt_of_gauge_lt : ∀ {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℝ E] {s : Set E} {x : E} {a : ℝ},
  Absorbent ℝ s → gauge s x < a → ∃ b, 0 < b ∧ b < a ∧ x ∈ b • s
-- Mathlib.FieldTheory.Galois.Abelian
IsAbelianGalois.tower_bot : ∀ (K : Type u_1) (L : Type u_2) (M : Type u_3) [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L]
  [inst_3 : Field M] [inst_4 : Algebra K M] [inst_5 : Algebra L M] [IsScalarTower K L M] [IsAbelianGalois K M],
  IsAbelianGalois K L
-- Mathlib.Algebra.Homology.Embedding.Extend
HomologicalComplex.extendMap_f_eq_zero : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {K L : HomologicalComplex C c} (φ : K ⟶ L) (e : c.Embedding c')
  (i' : ι'), (∀ (i : ι), e.f i ≠ i') → (HomologicalComplex.extendMap φ e).f i' = 0
-- Mathlib.AlgebraicTopology.SimplicialSet.Monoidal
SSet.Subcomplex.top_prod_le_unionProd : ∀ {X Y : SSet} (S : X.Subcomplex) (T : Y.Subcomplex), ⊤.prod T ≤ S.unionProd T
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.U.eq_def : ∀ (R : Type u_1) [inst : CommRing R] (x : ℤ),
  Polynomial.Chebyshev.U R x =
    match x with
    | 0 => 1
    | 1 => 2 * Polynomial.X
    | Int.ofNat n.succ.succ => 2 * Polynomial.X * Polynomial.Chebyshev.U R (↑n + 1) - Polynomial.Chebyshev.U R ↑n
    | Int.negSucc n => 2 * Polynomial.X * Polynomial.Chebyshev.U R (-↑n) - Polynomial.Chebyshev.U R (-↑n + 1)
-- Std.Time.Format.Modifier
/-- Four-digit year format (e.g., "2023")
 -/
Std.Time.Year.fourDigit : Std.Time.Year
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.coeSubmodule : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] →
            [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → CoeOut (LieSubmodule R L M) (Submodule R M)
-- Init.Data.Iterators.Internal.LawfulMonadLiftFunction
Std.Internal.instLawfulMonadLiftFunctionMonadLiftOfLawfulMonadLiftT : ∀ {m : Type u → Type v} [inst : Monad m] {n : Type u → Type w} [inst_1 : Monad n] [inst_2 : MonadLiftT m n]
  [LawfulMonadLiftT m n], Std.Internal.LawfulMonadLiftFunction fun ⦃α⦄ => monadLift
-- Mathlib.Probability.ConditionalExpectation
/-- If `m₁, m₂` are independent σ-algebras and `f` is `m₁`-measurable, then `𝔼[f | m₂] = 𝔼[f]`
almost everywhere.  -/
MeasureTheory.condExp_indep_eq : ∀ {Ω : Type u_1} {E : Type u_2} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E]
  {m₁ m₂ m : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} {f : Ω → E},
  m₁ ≤ m →
    ∀ (hle₂ : m₂ ≤ m) [MeasureTheory.SigmaFinite (μ.trim hle₂)],
      MeasureTheory.StronglyMeasurable f → ProbabilityTheory.Indep m₁ m₂ μ → μ[f | m₂] =ᵐ[μ] fun x => ∫ (x : Ω), f x ∂μ
-- Mathlib.CategoryTheory.ComposableArrows.Basic
/-- The `ComposableArrows C n` obtained by forgetting the first arrow.  -/
CategoryTheory.ComposableArrows.δlast : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {n : ℕ} → CategoryTheory.ComposableArrows C (n + 1) → CategoryTheory.ComposableArrows C n
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.instIsZLatticeRealComplexLattice : ∀ (L : PeriodPair), IsZLattice ℝ L.lattice
-- Mathlib.CategoryTheory.Groupoid
CategoryTheory.Groupoid.invEquivalence_functor_obj : ∀ (C : Type u) [inst : CategoryTheory.Groupoid C] (unop : C),
  (CategoryTheory.Groupoid.invEquivalence C).functor.obj unop = Opposite.op unop
-- Std.Data.DHashMap.Internal.AssocList.Basic
/-- Internal implementation detail of the hash map  -/
Std.DHashMap.Internal.AssocList.getKey : {α : Type u} →
  {β : α → Type v} →
    [inst : BEq α] →
      (a : α) → (l : Std.DHashMap.Internal.AssocList α β) → Std.DHashMap.Internal.AssocList.contains a l = true → α
-- Mathlib.Algebra.Group.Conj
conjugatesOf.eq_1 : ∀ {α : Type u} [inst : Monoid α] (a : α), conjugatesOf a = {b | IsConj a b}
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.Rpow.IntegralRepresentation
Real.aestronglyMeasurable_rpowIntegrand₀₁ : ∀ {p x : ℝ},
  p ∈ Set.Ioo 0 1 →
    0 ≤ x →
      MeasureTheory.AEStronglyMeasurable (fun x_1 => p.rpowIntegrand₀₁ x_1 x)
        (MeasureTheory.volume.restrict (Set.Ioi 0))
-- Mathlib.CategoryTheory.Limits.FintypeCat
CategoryTheory.Limits.FintypeCat.nonempty_pi_of_nonempty : ∀ {ι : Type u_1} [inst : Finite ι] (X : ι → FintypeCat) [∀ (i : ι), Nonempty (X i).obj], Nonempty (∏ᶜ X).obj
-- Batteries.Data.UInt
UInt32.ext : ∀ {x y : UInt32}, x.toNat = y.toNat → x = y
-- Mathlib.Combinatorics.Derangements.Basic
/-- A permutation is a derangement if it has no fixed points.  -/
derangements : (α : Type u_1) → Set (Equiv.Perm α)
-- Mathlib.GroupTheory.OrderOfElement
finEquivMultiples_apply : ∀ {G : Type u_1} [inst : AddMonoid G] {x : G} (hx : IsOfFinAddOrder x) {n : Fin (addOrderOf x)},
  (finEquivMultiples hx) n = ⟨↑n • x, ⋯⟩
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.instToJsonInlayHintClientCapabilities.toJson : Lean.Lsp.InlayHintClientCapabilities → Lean.Json
-- Lean.Widget.TaggedText
Lean.Widget.instBEqTaggedText.beq : {α : Type u_1} → [BEq α] → Lean.Widget.TaggedText α → Lean.Widget.TaggedText α → Bool
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
TangentBundle.trivializationAt_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_6}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] [inst_6 : IsManifold I 1 M] (x : M) (z : TangentBundle I M),
  ↑(trivializationAt E (TangentSpace I) x) z =
    (z.proj,
      (fderivWithin 𝕜 (↑((chartAt H x).extend I) ∘ ↑((chartAt H z.proj).extend I).symm) (Set.range ↑I)
          (↑((chartAt H z.proj).extend I) z.proj))
        z.snd)
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.get?_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp} [inst : Std.TransCmp cmp]
  {k a : α},
  Std.ExtDTreeMap.Const.get? (t.erase k) a = if cmp k a = Ordering.eq then none else Std.ExtDTreeMap.Const.get? t a
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Operations.Cpop.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer_denote_mem_prefix.go : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {len w : ℕ} {assign : α → Bool} {start : ℕ} {inv : Bool}
  (aig : Std.Sat.AIG α) (iterNum : ℕ) (hstart : start < aig.decls.size) (hold' : 2 * (iterNum - 1) < len)
  (oldLayer : aig.RefVec (len * w)) (newLayer : aig.RefVec (iterNum * w)),
  ⟦assign,
      { aig := (Std.Tactic.BVDecide.BVExpr.bitblast.blastCpopLayer.go iterNum oldLayer newLayer hold' ⋯).aig,
        ref := { gate := start, invert := inv, hgate := ⋯ } }⟧ =
    ⟦assign, { aig := aig, ref := { gate := start, invert := inv, hgate := hstart } }⟧
-- Mathlib.NumberTheory.PythagoreanTriples
circleEquivGen_apply : ∀ {K : Type u_1} [inst : Field K] (hk : ∀ (x : K), 1 + x ^ 2 ≠ 0) (x : K),
  ↑((circleEquivGen hk) x) = (2 * x / (1 + x ^ 2), (1 - x ^ 2) / (1 + x ^ 2))
-- Mathlib.CategoryTheory.Bicategory.Functor.Prelax
/-- Prelax functors preserve compositions of 2-morphisms.  -/
CategoryTheory.PrelaxFunctor.map₂_comp_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.PrelaxFunctor B C) {a b : B} {f g h : a ⟶ b} (η : f ⟶ g) (θ : g ⟶ h)
  {Z : self.obj a ⟶ self.obj b} (h_1 : self.map h ⟶ Z),
  CategoryTheory.CategoryStruct.comp (self.map₂ (CategoryTheory.CategoryStruct.comp η θ)) h_1 =
    CategoryTheory.CategoryStruct.comp (self.map₂ η) (CategoryTheory.CategoryStruct.comp (self.map₂ θ) h_1)
-- Init.Grind.Interactive
/-- Proves `<term>` using the current `grind` state and default search strategy.
 -/
Lean.Parser.Tactic.Grind.haveSilent : Lean.ParserDescr
-- Mathlib.Analysis.Normed.Module.Basic
NormedField.toNormedSpace : {𝕜 : Type u_1} → [inst : NormedField 𝕜] → NormedSpace 𝕜 𝕜
-- Mathlib.Algebra.Polynomial.Monic
Polynomial.Monic.as_sum : ∀ {R : Type u} [inst : Semiring R] {p : Polynomial R},
  p.Monic → p = Polynomial.X ^ p.natDegree + ∑ i ∈ Finset.range p.natDegree, Polynomial.C (p.coeff i) * Polynomial.X ^ i
-- Mathlib.RingTheory.UniqueFactorizationDomain.Basic
_private.Mathlib.RingTheory.UniqueFactorizationDomain.Basic.0.«term_~ᵤ_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.Matrix.Circulant
Matrix.Fin.circulant_isSymm_iff : ∀ {α : Type u_1} {n : ℕ} {v : Fin n → α}, (Matrix.circulant v).IsSymm ↔ ∀ (i : Fin n), v (-i) = v i
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.nsmul_right_monotone : ∀ {α : Type u_2} [inst : AddMonoid α] {s : Set α}, 0 ∈ s → Monotone fun x => x • s
-- Mathlib.Geometry.Manifold.Notation
/-- Delaborator for `Bundle.TotalSpace.mk` using anonymous constructor notation.  -/
Manifold.delabTotalSpaceMk : Lean.PrettyPrinter.Delaborator.Delab
-- Mathlib.CategoryTheory.Abelian.Images
/-- The cokernel of the kernel of `f` is called the (abelian) coimage of `f`.  -/
CategoryTheory.Abelian.coimage : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {P Q : C} →
        (f : P ⟶ Q) →
          [inst_2 : CategoryTheory.Limits.HasKernel f] →
            [CategoryTheory.Limits.HasCokernel (CategoryTheory.Limits.kernel.ι f)] → C
-- Mathlib.ModelTheory.Complexity
/-- A universal formula is a formula defined by applying only universal quantifiers to a
quantifier-free formula.  -/
FirstOrder.Language.BoundedFormula.IsUniversal : {L : FirstOrder.Language} → {α : Type u'} → {n : ℕ} → L.BoundedFormula α n → Prop
-- Std.Data.ExtDHashMap.Lemmas
/-- Simpler variant of `get_filterMap` when `LawfulBEq` is available.  -/
Std.ExtDHashMap.Const.get_filterMap' : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {γ : Type w} {m : Std.ExtDHashMap α fun x => β}
  [inst : LawfulBEq α] {f : α → β → Option γ} {k : α} {h : k ∈ Std.ExtDHashMap.filterMap f m},
  Std.ExtDHashMap.Const.get (Std.ExtDHashMap.filterMap f m) k h = (f k (Std.ExtDHashMap.Const.get m k ⋯)).get ⋯
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Same as `Monotone.covariant_of_const`, but with the constant on the other side of
the operator.  E.g., `∀ (m : ℕ), Monotone f → Monotone (fun n ↦ f (n + m))`.  -/
Monotone.covariant_of_const' : ∀ {N : Type u_2} {α : Type u_3} [inst : Preorder α] [inst_1 : Preorder N] {f : N → α} {μ : N → N → N}
  [CovariantClass N N (Function.swap μ) fun x1 x2 => x1 ≤ x2], Monotone f → ∀ (m : N), Monotone fun x => f (μ x m)
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.SInt
Int16.reduceDiv : Lean.Meta.Simp.DSimproc
-- Mathlib.Combinatorics.Matroid.Minor.Order
/-- The minor order is a `PartialOrder` on `Matroid α`.
We prefer the spelling `N ≤m M` over `N ≤ M` for the dot notation.  -/
Matroid.instPartialOrder : (α : Type u_2) → PartialOrder (Matroid α)
-- Std.Sat.AIG.CNF
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.mk.injEq : ∀ {aig : Std.Sat.AIG ℕ} (cnf : Std.Sat.CNF ℕ) (cache : Std.Sat.AIG.toCNF.Cache✝ aig cnf)
  (inv : Std.Sat.AIG.toCNF.State.Inv✝ aig cnf) (cnf_1 : Std.Sat.CNF ℕ) (cache_1 : Std.Sat.AIG.toCNF.Cache✝ aig cnf_1)
  (inv_1 : Std.Sat.AIG.toCNF.State.Inv✝ aig cnf_1),
  ({ cnf := cnf, cache := cache, inv := inv } = { cnf := cnf_1, cache := cache_1, inv := inv_1 }) =
    (cnf = cnf_1 ∧ cache ≍ cache_1)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.right_neg : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.CartesianMonoidalCategory C}
  (X : C) [self : CategoryTheory.AddGrpObj X],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.id X) CategoryTheory.AddGrpObj.neg)
      CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit X)
      CategoryTheory.AddMonObj.zero
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.Kernels
CategoryTheory.Limits.isIso_kernel_map_of_isPullback : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X₁ X₂ X₃ X₄ : C} {t : X₁ ⟶ X₂} {l : X₁ ⟶ X₃} {r : X₂ ⟶ X₄} {b : X₃ ⟶ X₄} [inst_2 : CategoryTheory.Limits.HasKernel t]
  [inst_3 : CategoryTheory.Limits.HasKernel b] (sq : CategoryTheory.IsPullback t l r b),
  CategoryTheory.IsIso (CategoryTheory.Limits.kernel.map t b l r ⋯)
-- Mathlib.LinearAlgebra.AffineSpace.Combination
Finset.sum_affineCombinationSingleWeights : ∀ (k : Type u_1) [inst : Ring k] {ι : Type u_4} (s : Finset ι) [inst_1 : DecidableEq ι] {i : ι},
  i ∈ s → ∑ j ∈ s, Finset.affineCombinationSingleWeights k i j = 1
-- Init.Data.List.Lemmas
List.head_append : ∀ {α : Type u_1} {l₁ l₂ : List α} (w : l₁ ++ l₂ ≠ []),
  (l₁ ++ l₂).head w = if h : l₁.isEmpty = true then l₂.head ⋯ else l₁.head ⋯
-- Init.Data.Order.Ord
Std.TransCmp.gt_trans : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {a b c : α},
  cmp a b = Ordering.gt → cmp b c = Ordering.gt → cmp a c = Ordering.gt
-- Mathlib.Algebra.Category.Ring.EqualizerPushout
/-- A regular monomorphism structure on a map `f : R ⟶ S` in `CommRingCat` with
faithfully flat `f.hom : R ⟶ S`.  -/
CommRingCat.regularMonoOfFaithfullyFlat : {R S : CommRingCat} → (f : R ⟶ S) → (CommRingCat.Hom.hom f).FaithfullyFlat → CategoryTheory.RegularMono f
-- Mathlib.Analysis.Normed.Group.Basic
coe_normGroupNorm : ∀ (E : Type u_5) [inst : NormedGroup E], ⇑(normGroupNorm E) = norm
-- Mathlib.Algebra.Group.Subgroup.Pointwise
Subgroup.mul_inf_assoc : ∀ {G : Type u_2} [inst : Group G] (A B C : Subgroup G), A ≤ C → ↑A * ↑(B ⊓ C) = ↑A * ↑B ∩ ↑C
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.Functor.mapCommGrp_map_hom_hom_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.CartesianMonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  (F : CategoryTheory.Functor C D) [inst_6 : F.Braided] {X Y : CategoryTheory.CommGrp C} (f : X ⟶ Y),
  (F.mapCommGrp.map f).hom.hom.hom = F.map f.hom.hom.hom
-- Mathlib.Data.Sum.Order
Sum.inr_mono : ∀ {α : Type u_1} {β : Type u_2} [inst : Preorder α] [inst_1 : Preorder β], Monotone Sum.inr
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_ite_mem : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] [inst_2 : DecidableEq ι]
  (s t : Finset ι) (f : ι → M),
  (s.expect fun i => if i ∈ t then f i else 0) = (↑(s ∩ t).card / ↑s.card) • (s ∩ t).expect fun i => f i
-- Mathlib.Topology.Category.Profinite.Nobeling.Successor
/-- The first way to map `C'` into `C`.  -/
Profinite.NobelingProof.CC'₀ : {I : Type u} →
  (C : Set (I → Bool)) →
    [inst : LinearOrder I] →
      [inst_1 : WellFoundedLT I] →
        {o : Ordinal.{u}} → (ho : o < Ordinal.type fun x1 x2 => x1 < x2) → ↑(Profinite.NobelingProof.C' C ho) → ↑C
-- Lean.Meta.Tactic.Grind.Proof
_private.Lean.Meta.Tactic.Grind.Proof.0.Lean.Meta.Grind.mkTrans : Lean.Expr → Lean.Expr → Bool → Lean.MetaM Lean.Expr
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.Attach
Std.IterM.count_attachWith : ∀ {α : Type u_1} {m : Type u_1 → Type u_2} {β : Type u_1} {P : β → Prop} {n : Type u_3 → Type u_4}
  [inst : Std.Iterator α m β] [inst_1 : Monad m] [Monad n] {it : Std.IterM m β}
  {hP : ∀ (out : β), it.IsPlausibleIndirectOutput out → P out} [Std.Iterators.Finite α m]
  [inst_4 : Std.IteratorLoop α m m] [LawfulMonad m] [Std.LawfulIteratorLoop α m m],
  (it.attachWith P hP).length = it.length
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.exists_min_root : ∀ {R : Type u} [inst : CommRing R] [IsDomain R] [inst_2 : LinearOrder R] (p : Polynomial R),
  p ≠ 0 → ∃ x₀, ∀ (x : R), p.IsRoot x → x₀ ≤ x
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- The product of two elements of a subsemigroup belongs to the subsemigroup.  -/
Subsemigroup.mul_mem' : ∀ {M : Type u_3} [inst : Mul M] (self : Subsemigroup M) {a b : M},
  a ∈ self.carrier → b ∈ self.carrier → a * b ∈ self.carrier
-- Mathlib.Algebra.Star.Basic
/-- A \*-magma is a magma `R` with an involutive operation `star`
such that `star (r * s) = star s * star r`.
 -/
StarMul : (R : Type u) → [Mul R] → Type u
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instIsTopologicalSemiring : ∀ {R : Type u_1} [inst : TopologicalSpace R] [inst_1 : NonUnitalNonAssocSemiring R] [inst_2 : IsTopologicalSemiring R],
  IsTopologicalSemiring (SeparationQuotient R)
-- Init.System.FilePath
/-- Replaces the current extension in a path `p` with `ext`, adding it if there is no extension. If the
path has multiple file extensions, only the last one is replaced. If the path has no filename, or if
`ext` is the empty string, then the filename is returned unmodified.

`ext` should not have a leading `.`, as this function adds one.

Examples:
* `("files/picture.jpeg" : System.FilePath).withExtension "jpg" = ⟨"files/picture.jpg"⟩`
* `("files/" : System.FilePath).withExtension "zip" = ⟨"files/"⟩`
* `("files" : System.FilePath).withExtension "zip" = ⟨"files.zip"⟩`
* `("files/archive.tar.gz" : System.FilePath).withExtension "xz" = ⟨"files.tar.xz"⟩`
 -/
System.FilePath.withExtension : System.FilePath → String → System.FilePath
-- Mathlib.CategoryTheory.Filtered.Final
/-- In this situation, `F` is also final, see
`Functor.final_of_exists_of_isFiltered_of_fullyFaithful`.  -/
CategoryTheory.IsFilteredOrEmpty.of_exists_of_isFiltered_of_fullyFaithful : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) [CategoryTheory.IsFilteredOrEmpty D] [F.Full] [F.Faithful],
  (∀ (d : D), ∃ c, Nonempty (d ⟶ F.obj c)) → CategoryTheory.IsFilteredOrEmpty C
-- Lean.Class
/-- An entry for the persistent environment extension for declared type classes  -/
Lean.ClassEntry : Type
-- Mathlib.ModelTheory.Semantics
FirstOrder.Language.BoundedFormula.realize_iSup : ∀ {L : FirstOrder.Language} {M : Type w} [inst : L.Structure M] {α : Type u'} {β : Type v'} {n : ℕ} [inst_1 : Finite β]
  {f : β → L.BoundedFormula α n} {v : α → M} {v' : Fin n → M},
  (FirstOrder.Language.BoundedFormula.iSup f).Realize v v' ↔ ∃ b, (f b).Realize v v'