mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.DiscreteValuationRing.Basic
/-- Every nonzero ideal in a DVR is a power of the maximal ideal.
See `idealOrderIsoENat` for a precise classification of ideals in a DVR.  -/
IsDiscreteValuationRing.ideal_eq_span_pow_irreducible : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [IsDiscreteValuationRing R] {s : Ideal R},
  s ≠ ⊥ → ∀ {ϖ : R}, Irreducible ϖ → ∃ n, s = Ideal.span {ϖ ^ n}
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
/-- If `s` is a compact set and `μ` is finite at `𝓝 x` for every `x ∈ s`, then `s` admits an open
superset of finite measure.  -/
IsCompact.exists_open_superset_measure_lt_top' : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MeasurableSpace α] {μ : MeasureTheory.Measure α} {s : Set α},
  IsCompact s → (∀ x ∈ s, μ.FiniteAtFilter (nhds x)) → ∃ U ⊇ s, IsOpen U ∧ μ U < ⊤
-- Mathlib.CategoryTheory.Monoidal.Functor
CategoryTheory.Functor.instLaxMonoidalProdProd : {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] →
            {E : Type u₃} →
              [inst_4 : CategoryTheory.Category.{v₃, u₃} E] →
                [inst_5 : CategoryTheory.MonoidalCategory E] →
                  {C' : Type u₁'} →
                    [inst_6 : CategoryTheory.Category.{v₁', u₁'} C'] →
                      (F : CategoryTheory.Functor C D) →
                        (G : CategoryTheory.Functor E C') →
                          [inst_7 : CategoryTheory.MonoidalCategory C'] →
                            [F.LaxMonoidal] → [G.LaxMonoidal] → (F.prod G).LaxMonoidal
-- Init.Coe
/-- The resulting value of type `β`. The input `x : α` is a parameter to
the type class, so the value of type `β` may possibly depend on additional
typeclasses on `x`.  -/
CoeDep.coe : {α : Sort u} → (x : α) → {β : Sort v} → [self : CoeDep α x β] → β
-- Mathlib.Algebra.Group.Hom.Defs
/-- `1` is the monoid homomorphism sending all elements to `1`.  -/
instOneMonoidHom : {M : Type u_4} → {N : Type u_5} → [inst : MulOne M] → [inst_1 : MulOneClass N] → One (M →* N)
-- Init.Control.MonadAttach
/-- A predicate that can be assumed to be true for all return values `a` of actions `x`
  in `m`, in all situations.
   -/
MonadAttach.CanReturn : {m : Type u → Type v} → [self : MonadAttach m] → {α : Type u} → m α → α → Prop
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.dist_map : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x y : E), dist (e x) (e y) = dist x y
-- Mathlib.CategoryTheory.CodiscreteCategory
/-- Left triangle equality of the adjunction `Cat.objects ⊣ Codiscrete.functorToCat`,
as a universe polymorphic statement.  -/
CategoryTheory.Codiscrete.left_triangle_components : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  CategoryTheory.Codiscrete.counitApp C ∘ (CategoryTheory.Codiscrete.unitApp C).obj = id
-- Mathlib.RingTheory.Flat.Rank
Module.algebraMap_surjective_of_rankAtStalk_le_one : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] [Module.Flat R S]
  [Module.Finite R S], (∀ (p : PrimeSpectrum R), Module.rankAtStalk S p ≤ 1) → Function.Surjective ⇑(algebraMap R S)
-- Mathlib.Topology.Algebra.InfiniteSum.Group
Multipliable.multipliable_of_eq_one_or_self : ∀ {α : Type u_1} {β : Type u_2} [inst : UniformSpace α] [inst_1 : CommGroup α] [IsUniformGroup α] {f g : β → α}
  [CompleteSpace α], Multipliable f → (∀ (b : β), g b = 1 ∨ g b = f b) → Multipliable g
-- Mathlib.CategoryTheory.Sites.DenseSubsite.OneHypercoverDense
CategoryTheory.Functor.PreOneHypercoverDenseData.w : ∀ {C₀ : Type u₀} {C : Type u} [inst : CategoryTheory.Category.{v₀, u₀} C₀] [inst_1 : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor C₀ C} {S : C} (self : F.PreOneHypercoverDenseData S) ⦃i₁ i₂ : self.I₀⦄
  (j : self.I₁ i₁ i₂),
  CategoryTheory.CategoryStruct.comp (F.map (self.p₁ j)) (self.f i₁) =
    CategoryTheory.CategoryStruct.comp (F.map (self.p₂ j)) (self.f i₂)
-- Mathlib.Data.Finset.Density
Finset.dens_union_add_dens_inter : ∀ {α : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq α] (s t : Finset α),
  (s ∪ t).dens + (s ∩ t).dens = s.dens + t.dens
-- Mathlib.Data.Nat.Size
Nat.shiftLeft_eq_mul_pow : ∀ (m n : ℕ), m <<< n = m * 2 ^ n
-- Mathlib.Topology.Algebra.Module.Equiv
ContinuousLinearEquiv.eq_toContinuousLinearMap_symm_comp : ∀ {R₁ : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} [inst : Semiring R₁] [inst_1 : Semiring R₂] [inst_2 : Semiring R₃]
  {σ₁₂ : R₁ →+* R₂} {σ₂₁ : R₂ →+* R₁} [inst_3 : RingHomInvPair σ₁₂ σ₂₁] [inst_4 : RingHomInvPair σ₂₁ σ₁₂]
  {σ₃₂ : R₃ →+* R₂} {σ₃₁ : R₃ →+* R₁} [inst_5 : RingHomCompTriple σ₃₂ σ₂₁ σ₃₁] {M₁ : Type u_4}
  [inst_6 : TopologicalSpace M₁] [inst_7 : AddCommMonoid M₁] {M₂ : Type u_5} [inst_8 : TopologicalSpace M₂]
  [inst_9 : AddCommMonoid M₂] {M₃ : Type u_6} [inst_10 : TopologicalSpace M₃] [inst_11 : AddCommMonoid M₃]
  [inst_12 : Module R₁ M₁] [inst_13 : Module R₂ M₂] [inst_14 : Module R₃ M₃] {e₁₂ : M₁ ≃SL[σ₁₂] M₂}
  [inst_15 : RingHomCompTriple σ₃₁ σ₁₂ σ₃₂] (f : M₃ →SL[σ₃₁] M₁) (g : M₃ →SL[σ₃₂] M₂),
  f = ↑e₁₂.symm ∘SL g ↔ ↑e₁₂ ∘SL f = g
-- Mathlib.Analysis.Analytic.Constructions
/-- ZPowers of analytic functions (into a normed division algebra over `𝕜`) are analytic if the
exponent is nonnegative.  -/
AnalyticAt.zpow_nonneg : ∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {𝕝 : Type u_8} [inst_3 : NormedDivisionRing 𝕝] [inst_4 : NormedAlgebra 𝕜 𝕝] {f : E → 𝕝}
  {z : E} {n : ℤ}, AnalyticAt 𝕜 f z → 0 ≤ n → AnalyticAt 𝕜 (f ^ n) z
-- Mathlib.NumberTheory.ModularForms.CuspFormSubmodule
ModularForm.mem_cuspFormSubmodule_iff : ∀ {Γ : Subgroup (GL (Fin 2) ℝ)} {k : ℤ} [inst : Γ.HasDetOne] {f : ModularForm Γ k},
  f ∈ ModularForm.cuspFormSubmodule Γ k ↔ f.IsCuspForm
-- Mathlib.Topology.Algebra.Constructions
MulOpposite.comap_unop_nhds : ∀ {M : Type u_1} [inst : TopologicalSpace M] (x : M), Filter.comap MulOpposite.unop (nhds x) = nhds (MulOpposite.op x)
-- Mathlib.Data.ENNReal.Inv
ENNReal.mul_inv_le_iff : ∀ {x y z : ENNReal}, y ≠ 0 → y ≠ ⊤ → (x * y⁻¹ ≤ z ↔ x ≤ z * y)
-- Mathlib.Algebra.Lie.Solvable
Function.instIsSolvableSubtypeMemLieIdeal : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (A : LieIdeal R L)
  [LieAlgebra.IsSolvable L], LieAlgebra.IsSolvable ↥A
-- Mathlib.Logic.Equiv.Defs
Equiv.bijective_comp : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β → γ), Function.Bijective (f ∘ ⇑e) ↔ Function.Bijective f
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.pullbackAssoc_inv_fst_snd : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄]
  [inst_4 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
        (CategoryTheory.Limits.pullback.snd f₁ f₂)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.snd f₁
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
      (CategoryTheory.Limits.pullback.fst f₃ f₄)
-- Mathlib.Algebra.Category.ModuleCat.Presheaf
PresheafOfModules.add_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {R : CategoryTheory.Functor Cᵒᵖ RingCat}
  {M₁ M₂ : PresheafOfModules R} (f g : M₁ ⟶ M₂) (X : Cᵒᵖ), (f + g).app X = f.app X + g.app X
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- Assumes left covariance.
The lemma assuming right covariance is `Right.one_lt_mul_of_lt_of_le`.  -/
Left.one_lt_mul_of_lt_of_le : ∀ {α : Type u_1} [inst : MulOneClass α] [inst_1 : Preorder α] [MulLeftMono α] {a b : α}, 1 < a → 1 ≤ b → 1 < a * b
-- Lean.Declaration
/-- Returns the value of a definition. With `allowOpaque := true`, values
of theorems and opaque declarations are also returned.
 -/
Lean.ConstantInfo.value! : Lean.ConstantInfo → optParam Bool false → Lean.Expr
-- Mathlib.Data.ENNReal.Operations
ENNReal.toNNReal_iInf : ∀ {ι : Sort u_1} {f : ι → ENNReal}, (∀ (i : ι), f i ≠ ⊤) → (iInf f).toNNReal = ⨅ i, (f i).toNNReal
-- Mathlib.Order.Northcott
northcott_iff_tendsto : ∀ {α : Type u_1} {β : Type u_2} (h : α → β) [inst : LinearOrder β] [NoMaxOrder β],
  Northcott h ↔ Filter.Tendsto h Filter.cofinite Filter.atTop
-- Lean.Elab.ParseImportsFast
Lean.PrintImportResult.result? : Lean.PrintImportResult → Option Lean.ModuleHeader
-- Mathlib.Analysis.Normed.Lp.PiLp
PiLp.dist_single_same : ∀ (p : ENNReal) {ι : Type u_2} (β : ι → Type u_4) [hp : Fact (1 ≤ p)] [inst : Fintype ι]
  [inst_1 : (i : ι) → SeminormedAddCommGroup (β i)] [inst_2 : DecidableEq ι] (i : ι) (b₁ b₂ : β i),
  dist (PiLp.single p i b₁) (PiLp.single p i b₂) = dist b₁ b₂
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.π₁_obj : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} [inst : CategoryTheory.Category.{v₁, u₁} A]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} B] [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  (F : CategoryTheory.Functor A B) (G : CategoryTheory.Functor C B) (x : CategoryTheory.Limits.CategoricalPullback F G),
  (CategoryTheory.Limits.CategoricalPullback.π₁ F G).obj x = x.fst
-- Mathlib.Algebra.GroupWithZero.Basic
left_ne_zero_of_mul_eq_one : ∀ {M₀ : Type u_1} [inst : MulZeroOneClass M₀] [Nontrivial M₀] {a b : M₀}, a * b = 1 → a ≠ 0
-- Init.Data.Subtype.Order
Subtype.instIsLinearPreorder : ∀ {α : Type u} [inst : LE α] [Std.IsLinearPreorder α] {P : α → Prop}, Std.IsLinearPreorder (Subtype P)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Lemmas.Expr.0.Std.Tactic.BVDecide.BVExpr.Cache.insert.match_1.splitter : {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} →
  (motive : Std.Tactic.BVDecide.BVExpr.Cache aig → Sort u_1) →
    (cache : Std.Tactic.BVDecide.BVExpr.Cache aig) →
      ((map : Std.DHashMap Std.Tactic.BVDecide.BVExpr.Cache.Key fun k => Vector Std.Sat.AIG.Fanin k.w) →
          (hbound :
              ∀ {i : ℕ} (k : Std.Tactic.BVDecide.BVExpr.Cache.Key) (h1 : k ∈ map) (h2 : i < k.w),
                (map.get k h1)[i].gate < aig.decls.size) →
            motive { map := map, hbound := hbound }) →
        motive cache
-- Mathlib.RingTheory.Coalgebra.Basic
Finsupp.lcoeFun.eq_1 : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  Finsupp.lcoeFun = { toFun := DFunLike.coe, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.NumberTheory.LSeries.HurwitzZetaOdd
/-- The sine zeta function is differentiable everywhere.  -/
HurwitzZeta.differentiableAt_sinZeta : ∀ (a : UnitAddCircle), Differentiable ℂ (HurwitzZeta.sinZeta a)
-- Mathlib.Algebra.ContinuedFractions.Basic
/-- Lift a scf to a gcf using the inclusion map.  -/
SimpContFract.instCoeGenContFract : {α : Type u_1} → [inst : One α] → Coe (SimpContFract α) (GenContFract α)
-- Mathlib.Geometry.Euclidean.Altitude
/-- The inner product of two altitudes has value strictly greater than the negated product of
their lengths.
 -/
Affine.Simplex.neg_mul_lt_inner_vsub_altitudeFoot : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) [inst_4 : n.AtLeastTwo] (i j : Fin (n + 1)),
  -(s.height i * s.height j) < inner ℝ (s.points i -ᵥ s.altitudeFoot i) (s.points j -ᵥ s.altitudeFoot j)
-- Lean.Elab.Deriving.Util
/-- Return the inductive declaration's type applied to the arguments in `argNames`.  -/
Lean.Elab.Deriving.mkInductiveApp : Lean.InductiveVal → Array Lean.Name → Lean.Elab.TermElabM Lean.Term
-- Init.Internal.Order.Lemmas
_private.Init.Internal.Order.Lemmas.0.Array.mapFinIdxM.map.match_1.eq_2 : ∀ {α : Type u_1} (as : Array α) (j : ℕ) (motive : (i : ℕ) → i + j = as.size → Sort u_2) (i : ℕ)
  (inv : i + 1 + j = as.size) (h_1 : (x : 0 + j = as.size) → motive 0 x)
  (h_2 : (i : ℕ) → (inv : i + 1 + j = as.size) → motive i.succ inv),
  (match i.succ, inv with
    | 0, x => h_1 x
    | i.succ, inv => h_2 i inv) =
    h_2 i inv
-- Mathlib.Algebra.Algebra.NonUnitalSubalgebra
NonUnitalAlgHom.coe_codRestrict : ∀ {F : Type v'} {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : NonUnitalNonAssocSemiring A]
  [inst_2 : Module R A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [inst_6 : NonUnitalAlgHomClass F R A B] (f : F) (S : NonUnitalSubalgebra R B) (hf : ∀ (x : A), f x ∈ S) (x : A),
  ↑((NonUnitalAlgHom.codRestrict f S hf) x) = f x
-- Mathlib.CategoryTheory.Monoidal.Mod
CategoryTheory.AddMod.Hom.mk'_hom : ∀ {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.MonoidalLeftAction C D]
  {A : C} [inst_4 : CategoryTheory.AddMonObj A] {M N : CategoryTheory.AddMod D A} (f : M.X ⟶ N.X)
  (vadd_hom :
    autoParam
      (CategoryTheory.CategoryStruct.comp CategoryTheory.AddModObj.vadd f =
        CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight A f)
          CategoryTheory.AddModObj.vadd)
      CategoryTheory.AddMod.Hom.mk'._auto_1),
  (CategoryTheory.AddMod.Hom.mk' f vadd_hom).hom = f
-- Mathlib.SetTheory.Lists
Lists'.toList.eq_def : ∀ {α : Type u_1} (x : Bool) (x_1 : Lists' α x),
  x_1.toList =
    match x, x_1 with
    | .(false), Lists'.atom a => []
    | .(true), Lists'.nil => []
    | .(true), a.cons' l => ⟨b, a⟩ :: l.toList
-- Mathlib.Combinatorics.SimpleGraph.Partition
/-- A proof that `parts` is a proper partition of `V`.  -/
SimpleGraph.Partition.isPartition : ∀ {V : Type u} {G : SimpleGraph V} (self : G.Partition), Setoid.IsPartition self.parts
-- Mathlib.Combinatorics.Additive.FreimanHom
IsMulFreimanHom.subtypeVal : ∀ {α : Type u_2} [inst : CommMonoid α] {n : ℕ} {S : Type u_5} [inst_1 : SetLike S α] [inst_2 : SubmonoidClass S α]
  {s : S}, IsMulFreimanHom n Set.univ Set.univ Subtype.val
-- Mathlib.CategoryTheory.Localization.FiniteProducts
CategoryTheory.Localization.instPreservesFiniteProductsLocalization'Q' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (W : CategoryTheory.MorphismProperty C)
  [W.ContainsIdentities] [CategoryTheory.Limits.HasFiniteProducts C] [W.IsStableUnderFiniteProducts]
  [inst_4 : W.HasLocalization], CategoryTheory.Limits.PreservesFiniteProducts W.Q'
-- Mathlib.CategoryTheory.Functor.TwoSquare
CategoryTheory.TwoSquare.ext : ∀ {C₁ : Type u₁} {C₂ : Type u₂} {C₃ : Type u₃} {C₄ : Type u₄} [inst : CategoryTheory.Category.{v₁, u₁} C₁]
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃]
  [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] {T : CategoryTheory.Functor C₁ C₂} {L : CategoryTheory.Functor C₁ C₃}
  {R : CategoryTheory.Functor C₂ C₄} {B : CategoryTheory.Functor C₃ C₄} (w w' : CategoryTheory.TwoSquare T L R B),
  (∀ (X : C₁), w.natTrans.app X = w'.natTrans.app X) → w = w'
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.singleton_one : ∀ {α : Type u_2} [inst : One α], {1} = 1
-- Mathlib.LinearAlgebra.RootSystem.Defs
/-- Two roots are orthogonal when they are fixed by each others' reflections.  -/
RootPairing.IsOrthogonal : {ι : Type u_1} →
  {R : Type u_2} →
    {M : Type u_3} →
      {N : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : Module R M] →
              [inst_3 : AddCommGroup N] → [inst_4 : Module R N] → RootPairing ι R M N → ι → ι → Prop
-- Mathlib.Tactic.Sat.FromLRAT
/-- The reification of a negative literal `¬⟦¬a⟧_v ≡ a`.  -/
Sat.Literal.reify_neg : ∀ {v : Sat.Valuation} {a : Prop} {n : ℕ}, (v n ↔ a) → Sat.Literal.reify v (Sat.Literal.neg n) a
-- Mathlib.Algebra.Category.MonCat.Limits
AddCommMonCat.limitAddCommMonoid : {J : Type v} →
  [inst : CategoryTheory.Category.{w, v} J] →
    (F : CategoryTheory.Functor J AddCommMonCat) →
      [inst_1 : Small.{u, max u v} ↑(F.comp (CategoryTheory.forget AddCommMonCat)).sections] →
        AddCommMonoid (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget AddCommMonCat))).pt
-- Mathlib.Algebra.Order.Sub.Unbundled.Basic
AddLECancellable.tsub_inj_right : ∀ {α : Type u_1} [inst : AddCommSemigroup α] [inst_1 : PartialOrder α] [ExistsAddOfLE α] [AddLeftMono α]
  [inst_4 : Sub α] [OrderedSub α] {a b c : α}, AddLECancellable (a - b) → b ≤ a → c ≤ a → a - b = a - c → b = c
-- Init.Grind.Lemmas
Lean.Grind.eq_false_of_imp_eq_true : ∀ {a b : Prop}, (a → b) = True → b = False → a = False
-- Mathlib.CategoryTheory.Types.Basic
/-- **Alias** of `CategoryTheory.NatTrans.naturality_apply`. -/
CategoryTheory.FunctorToTypes.naturality : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {FD : outParam (D → D → Type u_2)} {CD : outParam (D → Type w)}
  [inst_2 : outParam ((X Y : D) → FunLike (FD X Y) (CD X) (CD Y))] [inst_3 : CategoryTheory.ConcreteCategory D FD]
  {F G : CategoryTheory.Functor C D} (φ : F ⟶ G) {X Y : C} (f : X ⟶ Y) (x : CategoryTheory.ToType (F.obj X)),
  (CategoryTheory.ConcreteCategory.hom (φ.app Y)) ((CategoryTheory.ConcreteCategory.hom (F.map f)) x) =
    (CategoryTheory.ConcreteCategory.hom (G.map f)) ((CategoryTheory.ConcreteCategory.hom (φ.app X)) x)
-- Mathlib.LinearAlgebra.Alternating.Basic
AlternatingMap.map_add_univ : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {N : Type u_3}
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N] {ι : Type u_7} (f : M [⋀^ι]→ₗ[R] N) [inst_5 : DecidableEq ι]
  [inst_6 : Fintype ι] (m m' : ι → M), f (m + m') = ∑ s, f (s.piecewise m m')
-- Mathlib.Data.Nat.Bits
Nat.bodd_two : Nat.bodd 2 = false
-- Mathlib.Topology.UniformSpace.CompactConvergence
/-- If `K` is a compact exhaustion of `α`
and `V i` bounded by `p i` is a basis of entourages of `β`,
then `fun (n, i) ↦ {(f, g) | ∀ x ∈ K n, (f x, g x) ∈ V i}` bounded by `p i`
is a basis of entourages of `C(α, β)`.  -/
CompactExhaustion.hasBasis_compactConvergenceUniformity : ∀ {α : Type u₁} {β : Type u₂} [inst : TopologicalSpace α] [inst_1 : UniformSpace β] {ι : Type u_1} {p : ι → Prop}
  {V : ι → Set (β × β)} (K : CompactExhaustion α),
  (uniformity β).HasBasis p V →
    (uniformity C(α, β)).HasBasis (fun i => p i.2) fun i => {fg | ∀ x ∈ K i.1, (fg.1 x, fg.2 x) ∈ V i.2}
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.toList_insert_perm : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} (m : Std.DHashMap.Internal.Raw₀ α fun x => β)
  [EquivBEq α] [LawfulHashable α],
  (↑m).WF →
    ∀ {k : α} {v : β},
      (Std.DHashMap.Raw.Const.toList ↑(m.insert k v)).Perm
        ((k, v) :: List.filter (fun x => decide ¬(k == x.1) = true) (Std.DHashMap.Raw.Const.toList ↑m))
-- Mathlib.CategoryTheory.MorphismProperty.Comma
CategoryTheory.MorphismProperty.CostructuredArrow.homMk_left : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{u_3, u_1} C]
  [inst_1 : CategoryTheory.Category.{u_4, u_2} D] {P : CategoryTheory.MorphismProperty D}
  {Q : CategoryTheory.MorphismProperty C} [inst_2 : Q.IsMultiplicative] {F : CategoryTheory.Functor C D} {X : D}
  {A B : P.CostructuredArrow Q F X} (f : A.left ⟶ B.left) (hf : Q f)
  (w :
    autoParam (CategoryTheory.CategoryStruct.comp (F.map f) B.hom = A.hom)
      CategoryTheory.MorphismProperty.CostructuredArrow.homMk._auto_1),
  (CategoryTheory.MorphismProperty.CostructuredArrow.homMk f hf w).left = f
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_of_isNoetherianRing_of_finite : ∀ (R : Type u_1) (M : Type u_2) [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [IsNoetherianRing R]
  [Module.Finite R M], IsNoetherian R M
-- Mathlib.Algebra.Algebra.RestrictScalars
/-- This instance is only relevant when `RestrictScalars.moduleOrig` is available as an instance.
 -/
RestrictScalars.isScalarTower : ∀ (R : Type u_1) (S : Type u_2) (M : Type u_3) [inst : Semiring S] [inst_1 : AddCommMonoid M] [inst_2 : CommSemiring R]
  [inst_3 : Algebra R S] [inst_4 : Module S M], IsScalarTower R S (RestrictScalars R S M)
-- Mathlib.Data.Matrix.Basic
LinearMap.mapMatrix_comp : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {T : Type u_9} {α : Type u_11} {β : Type u_12}
  {γ : Type u_13} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : Semiring T] {σᵣₛ : R →+* S} {σₛₜ : S →+* T}
  {σᵣₜ : R →+* T} [inst_3 : RingHomCompTriple σᵣₛ σₛₜ σᵣₜ] [inst_4 : AddCommMonoid α] [inst_5 : AddCommMonoid β]
  [inst_6 : AddCommMonoid γ] [inst_7 : Module R α] [inst_8 : Module S β] [inst_9 : Module T γ] (f : β →ₛₗ[σₛₜ] γ)
  (g : α →ₛₗ[σᵣₛ] β), f.mapMatrix ∘ₛₗ g.mapMatrix = (f ∘ₛₗ g).mapMatrix
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_insertIfNew : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF → ∀ {k : α} {v : β k}, (↑(m.insertIfNew k v)).size = if m.contains k = true then (↑m).size else (↑m).size + 1
-- Mathlib.Logic.ExistsUnique
ExistsUnique.exists : ∀ {α : Sort u_1} {p : α → Prop}, (∃! x, p x) → ∃ x, p x
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The comparison morphism for the equalizer of `f,g`.
This is an isomorphism iff `G` preserves the equalizer of `f,g`; see
`Mathlib/CategoryTheory/Limits/Preserves/Shapes/Equalizers.lean`
 -/
CategoryTheory.Limits.equalizerComparison : {C : Type u} →
  {X Y : C} →
    [inst : CategoryTheory.Category.{v, u} C] →
      (f g : X ⟶ Y) →
        {D : Type u₂} →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
            (G : CategoryTheory.Functor C D) →
              [inst_2 : CategoryTheory.Limits.HasEqualizer f g] →
                [inst_3 : CategoryTheory.Limits.HasEqualizer (G.map f) (G.map g)] →
                  G.obj (CategoryTheory.Limits.equalizer f g) ⟶ CategoryTheory.Limits.equalizer (G.map f) (G.map g)
-- Init.System.IOError
IO.Error.noFileOrDirectory.injEq : ∀ (filename : String) (osCode : UInt32) (details filename_1 : String) (osCode_1 : UInt32) (details_1 : String),
  (IO.Error.noFileOrDirectory filename osCode details = IO.Error.noFileOrDirectory filename_1 osCode_1 details_1) =
    (filename = filename_1 ∧ osCode = osCode_1 ∧ details = details_1)
-- Init.Data.UInt.Lemmas
UInt64.toUInt16_ofNatClamp_of_lt : ∀ {n : ℕ}, n < UInt64.size → (UInt64.ofNatClamp n).toUInt16 = UInt16.ofNat n
-- Mathlib.RingTheory.Extension.Generators
Algebra.Generators.Hom.id_comp : ∀ {R : Type u} {S : Type v} {ι : Type w} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (P : Algebra.Generators R S ι) {R' : Type u_1} {S' : Type u_2} {ι' : Type u_3} [inst_3 : CommRing R']
  [inst_4 : CommRing S'] [inst_5 : Algebra R' S'] (P' : Algebra.Generators R' S' ι') [inst_6 : Algebra S S']
  (f : P.Hom P'), (Algebra.Generators.Hom.id P').comp f = f
-- Mathlib.Order.KrullDimension
/-- The height of an element is infinite iff there exist series of arbitrary length ending in that
element.
 -/
Order.height_eq_top_iff : ∀ {α : Type u_1} [inst : Preorder α] {x : α}, Order.height x = ⊤ ↔ ∀ (n : ℕ), ∃ p, RelSeries.last p = x ∧ p.length = n