mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Triangulated.Subcategory
CategoryTheory.ObjectProperty.monotone_extensionProduct_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.HasShift C ℤ] [inst_3 : CategoryTheory.Preadditive C]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (P : CategoryTheory.ObjectProperty C) {Q Q' : CategoryTheory.ObjectProperty C},
  Q ≤ Q' → P.extensionProduct Q ≤ P.extensionProduct Q'
-- Mathlib.Topology.Algebra.Nonarchimedean.Basic
NonarchimedeanAddGroup.nonarchimedean_of_emb : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [NonarchimedeanAddGroup G] {H : Type u_2}
  [inst_3 : AddGroup H] [inst_4 : TopologicalSpace H] [IsTopologicalAddGroup H] (f : G →+ H),
  Topology.IsOpenEmbedding ⇑f → NonarchimedeanAddGroup H
-- Aesop.Util.Tactic.Ext
Aesop.ExtResult.mk : ℕ → Array Lean.FVarId → Array (Lean.MVarId × Array Lean.FVarId) → Aesop.ExtResult
-- Init.Data.Nat.Basic
Nat.eq_zero_or_pos : ∀ (n : ℕ), n = 0 ∨ n > 0
-- Lean.Data.Lsp.CodeActions
/-- Code actions were requested automatically.

This typically happens when current selection in a file changes, but can
also be triggered when file content changes.  -/
Lean.Lsp.CodeActionTriggerKind.automatic : Lean.Lsp.CodeActionTriggerKind
-- Mathlib.Algebra.Group.Units.Defs
Units.instCoeHead.eq_1 : ∀ {α : Type u} [inst : Monoid α], Units.instCoeHead = { coe := Units.val }
-- Mathlib.NumberTheory.NumberField.Completion.FinitePlace
/-- **Alias** of `NumberField.FinitePlace.hasFiniteMulSupport`. -/
NumberField.FinitePlace.mulSupport_finite : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] {x : K}, x ≠ 0 → Function.HasFiniteMulSupport fun w => w x
-- Init.Data.String.Termination
String.Pos.map_toSlice_prev? : ∀ {s : String} {p : s.Pos}, Option.map String.Pos.toSlice p.prev? = p.toSlice.prev?
-- Mathlib.Geometry.Convex.Cone.TensorProduct
PointedCone.maxTensorProduct.eq_1 : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : LinearOrder R] [inst_2 : IsStrictOrderedRing R] {G : Type u_2}
  [inst_3 : AddCommGroup G] [inst_4 : Module R G] {H : Type u_3} [inst_5 : AddCommGroup H] [inst_6 : Module R H]
  (C₁ : PointedCone R G) (C₂ : PointedCone R H),
  C₁.maxTensorProduct C₂ =
    PointedCone.dual (TensorProduct.dualDistrib R G H)
      ↑((PointedCone.dual (Module.Dual.eval R G) ↑C₁).minTensorProduct (PointedCone.dual (Module.Dual.eval R H) ↑C₂))
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
ZMod.rootsOfUnityAddChar.eq_1 : ∀ (n : ℕ) [inst : NeZero n],
  ZMod.rootsOfUnityAddChar n =
    { toFun := fun x => ⟨toUnits (ZMod.toCircle x), ⋯⟩, map_zero_eq_one' := ⋯, map_add_eq_mul' := ⋯ }
-- Mathlib.Data.Finset.Slice
Set.sized_union : ∀ {α : Type u_1} {A B : Set (Finset α)} {r : ℕ}, Set.Sized r (A ∪ B) ↔ Set.Sized r A ∧ Set.Sized r B
-- Mathlib.Algebra.Category.Grp.Basic
CommGrpCat.ext : ∀ {X Y : CommGrpCat} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.NumberTheory.Bernoulli
bernoulli'_def' : ∀ (n : ℕ), bernoulli' n = 1 - ∑ k, ↑(n.choose ↑k) / (↑n - ↑↑k + 1) * bernoulli' ↑k
-- Mathlib.Algebra.Category.ModuleCat.Semi
/-- Convenience shortcut for `SemimoduleCat.hom_bijective.surjective`.  -/
SemimoduleCat.hom_surjective : ∀ {R : Type u} [inst : Semiring R] {M N : SemimoduleCat R}, Function.Surjective SemimoduleCat.Hom.hom
-- Mathlib.GroupTheory.Coset.Basic
orbit_addSubgroup_zero_eq_self : ∀ {α : Type u_1} [inst : AddGroup α] (s : AddSubgroup α), AddAction.orbit (↥s) 0 = ↑s
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
CategoryTheory.Functor.PreservesPointwiseRightKanExtensionAt.mk : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] {G : CategoryTheory.Functor B D} {F : CategoryTheory.Functor A B}
  {L : CategoryTheory.Functor A C} {c : C},
  (∀ (E : L.RightExtension F) (a : E.IsPointwiseRightKanExtensionAt c),
      Nonempty (((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj E).IsPointwiseRightKanExtensionAt c)) →
    G.PreservesPointwiseRightKanExtensionAt F L c
-- Mathlib.MeasureTheory.Measure.Lebesgue.Basic
Real.volume_univ : MeasureTheory.volume Set.univ = ⊤
-- Mathlib.MeasureTheory.Function.ConditionalExpectation.CondJensen
/-- **Conditional Jensen's inequality**: in a finite dimensional Banach space `E` with a measure
`μ` that is σ-finite on a sub-σ-algebra `m`, if `φ : E → ℝ` is convex, then for any `f : α → E` such
that `f` and `φ ∘ f` are integrable, we have `φ (𝔼[f | m]) ≤ᵐ[μ] 𝔼[φ ∘ f | m]`.  -/
ConvexOn.map_condExp_le_of_finiteDimensional : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [CompleteSpace E] {α : Type u_2} {f : α → E}
  {φ : E → ℝ} {m mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} [FiniteDimensional ℝ E] (hm : m ≤ mα)
  [MeasureTheory.SigmaFinite (μ.trim hm)],
  ConvexOn ℝ Set.univ φ →
    MeasureTheory.Integrable f μ → MeasureTheory.Integrable (φ ∘ f) μ → φ ∘ μ[f | m] ≤ᵐ[μ] μ[φ ∘ f | m]
-- Init.Core
/-- Lifts a binary function from the underlying types to a binary function on quotients. The function
must respect both quotients' equivalence relations.

`Quotient.liftOn` is a version of this operation for unary functions. `Quotient.lift₂` is a version
that take the quotient parameters last.
 -/
Quotient.liftOn₂ : {α : Sort uA} →
  {β : Sort uB} →
    {φ : Sort uC} →
      {s₁ : Setoid α} →
        {s₂ : Setoid β} →
          Quotient s₁ →
            Quotient s₂ →
              (f : α → β → φ) → (∀ (a₁ : α) (b₁ : β) (a₂ : α) (b₂ : β), a₁ ≈ a₂ → b₁ ≈ b₂ → f a₁ b₁ = f a₂ b₂) → φ
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift_le_size : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (n d : aig.RefVec w) (wn wr : ℕ)
  (q r : aig.RefVec w),
  aig.decls.size ≤
    (Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.blastDivSubtractShift aig n d wn wr q r).aig.decls.size
-- Mathlib.CategoryTheory.EquivalenceRelation
/-- `t` is the morphism witnessing transitivity  -/
CategoryTheory.EquivalenceRelation.t : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {R X : C} → {p₁ p₂ : R ⟶ X} → (self : CategoryTheory.EquivalenceRelation p₁ p₂) → self.c.pt ⟶ R
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenNormalAddSubgroup.instPartialOrderOpenNormalAddSubgroup : {G : Type u} → [inst : AddGroup G] → [inst_1 : TopologicalSpace G] → PartialOrder (OpenNormalAddSubgroup G)
-- Mathlib.CategoryTheory.FiberedCategory.Cartesian
/-- Given a diagram
```
a'        a --φ--> b
|         |        |
v         v        v
R' --g--> R --f--> S
```
such that `φ` is strongly Cartesian, and a morphism `φ' : a' ⟶ b`. Then `map` is the map `a' ⟶ a`
lying over `g` obtained from the universal property of `φ`.  -/
CategoryTheory.Functor.IsStronglyCartesian.map : {𝒮 : 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.IsStronglyCartesian f φ] →
                    {R' : 𝒮} →
                      {a' : 𝒳} →
                        {g : R' ⟶ R} →
                          {f' : R' ⟶ S} →
                            f' = CategoryTheory.CategoryStruct.comp g f → (φ' : a' ⟶ b) → [p.IsHomLift f' φ'] → a' ⟶ a
-- Mathlib.Tactic.NormNum.Core
Mathlib.Meta.NormNum.NormNums.mk.inj : ∀ {tree : Lean.Meta.DiscrTree Mathlib.Meta.NormNum.NormNumExt} {erased : Lean.PHashSet Lean.Name}
  {tree_1 : Lean.Meta.DiscrTree Mathlib.Meta.NormNum.NormNumExt} {erased_1 : Lean.PHashSet Lean.Name},
  { tree := tree, erased := erased } = { tree := tree_1, erased := erased_1 } → tree = tree_1 ∧ erased = erased_1
-- Lean.Elab.Tactic.ElabTerm
/-- Execute `k`, and collect any fresh metavariables created during the execution of `k`.
 -/
Lean.Elab.Tactic.collectFreshMVars : {m : Type → Type u_1} → [Monad m] → [MonadLiftT Lean.MetaM m] → m Lean.Expr → m (Lean.Expr × Array Lean.MVarId)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.getKey!_alter_self : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β}
  [inst_2 : EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited α] {k : α} {f : Option β → Option β},
  m.WF →
    (Std.DHashMap.Raw.Const.alter m k f).getKey! k =
      if (f (Std.DHashMap.Raw.Const.get? m k)).isSome = true then k else default
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.List.mapA.match_1.splitter : {α : Type u_1} →
  (motive : List α → Sort u_2) →
    (x : List α) → (Unit → motive []) → ((a : α) → (as : List α) → motive (a :: as)) → motive x
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.sInf_toSubmonoid : ∀ {R : Type u} [inst : NonAssocRing R] (s : Set (Subring R)), (sInf s).toSubmonoid = ⨅ t ∈ s, t.toSubmonoid
-- Mathlib.LinearAlgebra.RootSystem.Defs
RootPairing.mk.injEq : ∀ {ι : 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] (toLinearMap : M →ₗ[R] N →ₗ[R] R)
  [isPerfPair_toLinearMap : toLinearMap.IsPerfPair] (root : ι ↪ M) (coroot : ι ↪ N)
  (root_coroot_two : ∀ (i : ι), (toLinearMap (root i)) (coroot i) = 2) (reflectionPerm : ι → ι ≃ ι)
  (reflectionPerm_root : ∀ (i j : ι), root j - (toLinearMap (root j)) (coroot i) • root i = root ((reflectionPerm i) j))
  (reflectionPerm_coroot :
    ∀ (i j : ι), coroot j - (toLinearMap (root i)) (coroot j) • coroot i = coroot ((reflectionPerm i) j))
  (toLinearMap_1 : M →ₗ[R] N →ₗ[R] R) (isPerfPair_toLinearMap_1 : toLinearMap_1.IsPerfPair) (root_1 : ι ↪ M)
  (coroot_1 : ι ↪ N) (root_coroot_two_1 : ∀ (i : ι), (toLinearMap_1 (root_1 i)) (coroot_1 i) = 2)
  (reflectionPerm_1 : ι → ι ≃ ι)
  (reflectionPerm_root_1 :
    ∀ (i j : ι), root_1 j - (toLinearMap_1 (root_1 j)) (coroot_1 i) • root_1 i = root_1 ((reflectionPerm_1 i) j))
  (reflectionPerm_coroot_1 :
    ∀ (i j : ι), coroot_1 j - (toLinearMap_1 (root_1 i)) (coroot_1 j) • coroot_1 i = coroot_1 ((reflectionPerm_1 i) j)),
  ({ toLinearMap := toLinearMap, isPerfPair_toLinearMap := isPerfPair_toLinearMap, root := root, coroot := coroot,
        root_coroot_two := root_coroot_two, reflectionPerm := reflectionPerm,
        reflectionPerm_root := reflectionPerm_root, reflectionPerm_coroot := reflectionPerm_coroot } =
      { toLinearMap := toLinearMap_1, isPerfPair_toLinearMap := isPerfPair_toLinearMap_1, root := root_1,
        coroot := coroot_1, root_coroot_two := root_coroot_two_1, reflectionPerm := reflectionPerm_1,
        reflectionPerm_root := reflectionPerm_root_1, reflectionPerm_coroot := reflectionPerm_coroot_1 }) =
    (toLinearMap = toLinearMap_1 ∧ root = root_1 ∧ coroot = coroot_1 ∧ reflectionPerm = reflectionPerm_1)
-- Mathlib.Probability.Kernel.Proper
/-- **Alias** of the reverse direction of `ProbabilityTheory.Kernel.isProper_iff_restrict_eq_indicator_smul`. -/
ProbabilityTheory.Kernel.IsProper.of_restrict_eq_indicator_smul : ∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X} (h𝓑𝓧 : 𝓑 ≤ 𝓧),
  (∀ ⦃B : Set X⦄ (hB : MeasurableSet B) (x : X), (π.restrict ⋯) x = B.indicator (fun x => 1) x • π x) → π.IsProper
-- Mathlib.Algebra.Lie.Extension
LieAlgebra.Extension.d₁₂_oneCochainOfTwoSplitting : ∀ {R : Type u_1} {L : Type u_3} {M : Type u_4} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : LieRing M] [inst_4 : LieAlgebra R M] [inst_5 : IsLieAbelian M] (E : LieAlgebra.Extension R M L)
  {s₁ s₂ : L →ₗ[R] E.L} (hs₁ : Function.LeftInverse ⇑E.proj ⇑s₁) (hs₂ : Function.LeftInverse ⇑E.proj ⇑s₂),
  (LieModule.Cohomology.d₁₂ R L M) (E.oneCochainOfTwoSplitting hs₁ hs₂) = ↑(E.twoCocycleOf hs₁) - ↑(E.twoCocycleOf hs₂)
-- Mathlib.Algebra.Order.Quantale
AddQuantale.iSup_add_distrib : ∀ {α : Type u_1} {ι : Type u_2} {x : α} {f : ι → α} [inst : AddSemigroup α] [inst_1 : CompleteLattice α]
  [IsAddQuantale α], (⨆ i, f i) + x = ⨆ i, f i + x
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- See also `Ideal.IsMaximal.mul_mem_pow` for maximal ideal.  -/
Ideal.IsPrime.mul_mem_pow : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] (I : Ideal R) [hI : I.IsPrime] {a b : R} {n : ℕ},
  a * b ∈ I ^ n → a ∈ I ∨ b ∈ I ^ n
-- Lean.Language.Lean.Types
Lean.Language.Lean.CommandElaboratingSnapshot.mk.injEq : ∀ (toSnapshot : Lean.Language.Snapshot) (elabSnap : Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot)
  (resultSnap : Lean.Language.SnapshotTask Lean.Language.Lean.CommandResultSnapshot)
  (infoTreeSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf)
  (reportSnap : Lean.Language.SnapshotTask Lean.Language.SnapshotTree) (toSnapshot_1 : Lean.Language.Snapshot)
  (elabSnap_1 : Lean.Language.SnapshotTask Lean.Language.DynamicSnapshot)
  (resultSnap_1 : Lean.Language.SnapshotTask Lean.Language.Lean.CommandResultSnapshot)
  (infoTreeSnap_1 : Lean.Language.SnapshotTask Lean.Language.SnapshotLeaf)
  (reportSnap_1 : Lean.Language.SnapshotTask Lean.Language.SnapshotTree),
  ({ toSnapshot := toSnapshot, elabSnap := elabSnap, resultSnap := resultSnap, infoTreeSnap := infoTreeSnap,
        reportSnap := reportSnap } =
      { toSnapshot := toSnapshot_1, elabSnap := elabSnap_1, resultSnap := resultSnap_1, infoTreeSnap := infoTreeSnap_1,
        reportSnap := reportSnap_1 }) =
    (toSnapshot = toSnapshot_1 ∧
      elabSnap = elabSnap_1 ∧ resultSnap = resultSnap_1 ∧ infoTreeSnap = infoTreeSnap_1 ∧ reportSnap = reportSnap_1)
-- Mathlib.Algebra.Homology.BifunctorAssociator
HomologicalComplex.mapBifunctor₂₃.ι.congr_simp : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₂₃ : Type u_4} {C₃ : Type u_5} {C₄ : Type u_6}
  [inst : CategoryTheory.Category.{v_1, u_1} C₁] [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂]
  [inst_2 : CategoryTheory.Category.{v_3, u_5} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_6} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_4} C₂₃] [inst_5 : CategoryTheory.Limits.HasZeroMorphisms C₁]
  [inst_6 : CategoryTheory.Limits.HasZeroMorphisms C₂] [inst_7 : CategoryTheory.Limits.HasZeroMorphisms C₃]
  [inst_8 : CategoryTheory.Preadditive C₂₃] [inst_9 : CategoryTheory.Preadditive C₄]
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄))
  (G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)) [inst_10 : G₂₃.PreservesZeroMorphisms]
  [inst_11 : ∀ (X₂ : C₂), (G₂₃.obj X₂).PreservesZeroMorphisms] [inst_12 : F.PreservesZeroMorphisms]
  [inst_13 : ∀ (X₁ : C₁), (F.obj X₁).Additive] {ι₁ : Type u_7} {ι₂ : Type u_8} {ι₃ : Type u_9} {ι₁₂ : Type u_10}
  {ι₂₃ : Type u_11} {ι₄ : Type u_12} [inst_14 : DecidableEq ι₄] {c₁ : ComplexShape ι₁} {c₂ : ComplexShape ι₂}
  {c₃ : ComplexShape ι₃} (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂) (K₃ : HomologicalComplex C₃ c₃)
  (c₁₂ : ComplexShape ι₁₂) (c₂₃ : ComplexShape ι₂₃) (c₄ : ComplexShape ι₄) [inst_15 : TotalComplexShape c₁ c₂ c₁₂]
  [inst_16 : TotalComplexShape c₁₂ c₃ c₄] [inst_17 : TotalComplexShape c₂ c₃ c₂₃]
  [inst_18 : TotalComplexShape c₁ c₂₃ c₄] [inst_19 : K₂.HasMapBifunctor K₃ G₂₃ c₂₃]
  [inst_20 : c₁.Associative c₂ c₃ c₁₂ c₂₃ c₄] [inst_21 : DecidableEq ι₂₃]
  [inst_22 : K₁.HasMapBifunctor (K₂.mapBifunctor K₃ G₂₃ c₂₃) F c₄] (i₁ : ι₁) (i₂ : ι₂) (i₃ : ι₃) (j : ι₄) (h : ⋯ = j),
  ⋯ = ⋯
-- Mathlib.MeasureTheory.Measure.LevyProkhorovMetric
/-- The identity map `LevyProkhorov (ProbabilityMeasure Ω) → ProbabilityMeasure Ω` is continuous.  -/
MeasureTheory.LevyProkhorov.continuous_toMeasure_probabilityMeasure : ∀ {Ω : Type u_1} [inst : MeasurableSpace Ω] [inst_1 : PseudoMetricSpace Ω] [inst_2 : OpensMeasurableSpace Ω],
  Continuous MeasureTheory.LevyProkhorov.toMeasure
-- Mathlib.Geometry.Euclidean.Angle.Unoriented.Basic
/-- The angle between a normalized vector and another vector is equal to the angle
between the original vectors.  -/
InnerProductGeometry.angle_normalize_left : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] (x y : V),
  InnerProductGeometry.angle (NormedSpace.normalize x) y = InnerProductGeometry.angle x y
-- Mathlib.Data.Part
Part.mk.inj : ∀ {α : Type u} {Dom : Prop} {get : Dom → α} {Dom_1 : Prop} {get_1 : Dom_1 → α},
  { Dom := Dom, get := get } = { Dom := Dom_1, get := get_1 } → Dom = Dom_1 ∧ get ≍ get_1
-- Std.Sat.AIG.CNF
/-- The CNF clauses so far.
 -/
_private.Std.Sat.AIG.CNF.0.Std.Sat.AIG.toCNF.State.cnf : {aig : Std.Sat.AIG ℕ} → Std.Sat.AIG.toCNF.State✝ aig → Std.Sat.CNF ℕ
-- Mathlib.MeasureTheory.VectorMeasure.Integral
MeasureTheory.VectorMeasure.integral_neg_cbm : ∀ {X : Type u_2} {E : Type u_4} {F : Type u_5} {G : Type u_6} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] [inst_4 : NormedAddCommGroup G]
  [inst_5 : NormedSpace ℝ G] {f : X → E} {μ : MeasureTheory.VectorMeasure X F} {B : E →L[ℝ] F →L[ℝ] G},
  ∫ᵛ (x : X), f x ∂[-B; μ] = -∫ᵛ (x : X), f x ∂[B; μ]
-- Mathlib.CategoryTheory.Monoidal.Discrete
/-- The monoidal natural isomorphism corresponding to composing two multiplicative morphisms.
 -/
CategoryTheory.Discrete.monoidalFunctorComp : {M : Type u} →
  [inst : Monoid M] →
    {N : Type u'} →
      [inst_1 : Monoid N] →
        {K : Type u} →
          [inst_2 : Monoid K] →
            (F : M →* N) →
              (G : N →* K) →
                (CategoryTheory.Discrete.monoidalFunctor F).comp (CategoryTheory.Discrete.monoidalFunctor G) ≅
                  CategoryTheory.Discrete.monoidalFunctor (G.comp F)
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.keyAtIdxD.eq_2 : ∀ {α : Type u} {β : α → Type v} (x : ℕ) (x_1 : α) (size : ℕ) (k : α) (v : β k) (l r : Std.DTreeMap.Internal.Impl α β),
  (Std.DTreeMap.Internal.Impl.inner size k v l r).keyAtIdxD x x_1 =
    match compare x l.size with
    | Ordering.lt => l.keyAtIdxD x x_1
    | Ordering.eq => k
    | Ordering.gt => r.keyAtIdxD (x - l.size - 1) x_1
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
Set.sub_subset_iff : ∀ {α : Type u_2} [inst : Sub α] {s t u : Set α}, s - t ⊆ u ↔ ∀ x ∈ s, ∀ y ∈ t, x - y ∈ u
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.getKeyD_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.DHashMap α β} [EquivBEq α]
  [LawfulHashable α] {k fallback : α}, k ∉ m₂ → (m₁ ∩ m₂).getKeyD k fallback = fallback
-- Mathlib.Topology.Compactness.LocallyCompact
/-- In a locally compact space, for every containment `K ⊆ U` of a compact set `K` in an open
set `U`, there is a compact neighborhood `L` such that `K ⊆ L ⊆ U`: equivalently, there is a
compact `L` such that `K ⊆ interior L` and `L ⊆ U`.
See also `exists_compact_closed_between`, in which one guarantees additionally that `L` is closed
if the space is regular.  -/
exists_compact_between : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] {K U : Set X},
  IsCompact K → IsOpen U → K ⊆ U → ∃ L, IsCompact L ∧ K ⊆ interior L ∧ L ⊆ U
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.ext_iff : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] {f g : A ≃⋆+* B}, f = g ↔ ∀ (a : A), f a = g a
-- Mathlib.LinearAlgebra.RootSystem.Hom
RootPairing.Hom.comp_assoc : ∀ {ι : 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] {ι₁ : Type u_5} {M₁ : Type u_6} {N₁ : Type u_7}
  {ι₂ : Type u_8} {M₂ : Type u_9} {N₂ : Type u_10} {ι₃ : Type u_11} {M₃ : Type u_12} {N₃ : Type u_13}
  [inst_5 : AddCommGroup M₁] [inst_6 : Module R M₁] [inst_7 : AddCommGroup N₁] [inst_8 : Module R N₁]
  [inst_9 : AddCommGroup M₂] [inst_10 : Module R M₂] [inst_11 : AddCommGroup N₂] [inst_12 : Module R N₂]
  [inst_13 : AddCommGroup M₃] [inst_14 : Module R M₃] [inst_15 : AddCommGroup N₃] [inst_16 : Module R N₃]
  {P : RootPairing ι R M N} {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} {P₃ : RootPairing ι₃ R M₃ N₃}
  (h : P₂.Hom P₃) (g : P₁.Hom P₂) (f : P.Hom P₁), (h.comp g).comp f = h.comp (g.comp f)
-- Mathlib.MeasureTheory.SetAlgebra
/-- If a family of sets `𝒜` is contained in an algebra of sets `ℬ`, then so is the algebra of sets
generated by `𝒜`.  -/
MeasureTheory.IsSetAlgebra.generateSetAlgebra_subset : ∀ {α : Type u_1} {𝒜 ℬ : Set (Set α)}, 𝒜 ⊆ ℬ → MeasureTheory.IsSetAlgebra ℬ → MeasureTheory.generateSetAlgebra 𝒜 ⊆ ℬ
-- Mathlib.RingTheory.Kaehler.JacobiZariski
Algebra.Generators.H1Cotangent.δAux_mul : ∀ {R : Type u₁} {S : Type u₂} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S] {T : Type u₃}
  [inst_3 : CommRing T] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] {ι : Type w₁}
  (Q : Algebra.Generators S T ι) (x y : Q.Ring),
  (Algebra.Generators.H1Cotangent.δAux R Q) (x * y) =
    x • (Algebra.Generators.H1Cotangent.δAux R Q) y + y • (Algebra.Generators.H1Cotangent.δAux R Q) x
-- Mathlib.Order.WithBot
WithBot.le_of_forall_lt_iff_le : ∀ {α : Type u_1} [inst : LinearOrder α] {x y : WithBot α} [DenselyOrdered α] [NoMinOrder α],
  (∀ (z : α), x < ↑z → y ≤ ↑z) ↔ y ≤ x
-- Init.Data.BitVec.Lemmas
BitVec.toFin_sshiftRight_of_msb_false : ∀ {w : ℕ} {x : BitVec w} {n : ℕ}, x.msb = false → (x.sshiftRight n).toFin = Fin.ofNat (2 ^ w) (x.toNat >>> n)
-- Mathlib.Tactic.NormNum.BigOperators
/-- If `s` unifies with `t`, convert a result for `s` to a result for `t`.

If `s` does not unify with `t`, this results in a type-incorrect proof.
 -/
Mathlib.Meta.Multiset.ProveZeroOrConsResult.uncheckedCast : {u v : Lean.Level} →
  {α : Q(Type u)} →
    {β : Q(Type v)} →
      (s : Q(Multiset «$α»)) →
        (t : Q(Multiset «$β»)) →
          Mathlib.Meta.Multiset.ProveZeroOrConsResult s → Mathlib.Meta.Multiset.ProveZeroOrConsResult t
-- Mathlib.NumberTheory.ModularForms.Discriminant
CuspForm.coe_discriminant : ⇑CuspForm.discriminant = ModularForm.discriminant
-- Mathlib.RingTheory.Polynomial.Vieta
/-- A sum version of **Vieta's formula** for `Multiset`: the product of the linear terms `X + λ`
where `λ` runs through a multiset `s` is equal to a linear combination of the symmetric functions
`esymm s` of the `λ`'s .  -/
Multiset.prod_X_add_C_eq_sum_esymm : ∀ {R : Type u_1} [inst : CommSemiring R] (s : Multiset R),
  (Multiset.map (fun r => Polynomial.X + Polynomial.C r) s).prod =
    ∑ j ∈ Finset.range (s.card + 1), Polynomial.C (s.esymm j) * Polynomial.X ^ (s.card - j)
-- Mathlib.AlgebraicGeometry.EllipticCurve.VariableChange
WeierstrassCurve.VariableChange.ext_iff : ∀ {R : Type u} {inst : CommRing R} {x y : WeierstrassCurve.VariableChange R},
  x = y ↔ x.u = y.u ∧ x.r = y.r ∧ x.s = y.s ∧ x.t = y.t
-- Mathlib.GroupTheory.Torsion
AddCommGroup.isAddTorsion_quotient_range_nsmulAddMonoidHom : ∀ (G : Type u_1) [inst : AddCommGroup G] {n : ℕ}, n ≠ 0 → IsAddTorsion (G ⧸ (nsmulAddMonoidHom n).range)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Restrict
Submodule.isEmbedding_subtypeL : ∀ {R : Type u_1} [inst : Semiring R] {M : Type u_2} [inst_1 : TopologicalSpace M] [inst_2 : AddCommMonoid M]
  [inst_3 : Module R M] (p : Submodule R M), Topology.IsEmbedding ⇑p.subtypeL
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.toEquiv_mulLeft : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableMul G] (g : G),
  (MeasurableEquiv.mulLeft g).toEquiv = Equiv.mulLeft g
-- Mathlib.Analysis.Calculus.FDeriv.Add
fderiv_const_smul : ∀ {𝕜 : 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] {f : E → F}
  {x : E} {R : Type u_4} [inst_5 : Monoid R] [inst_6 : DistribMulAction R F] [inst_7 : SMulCommClass 𝕜 R F]
  [inst_8 : ContinuousConstSMul R F], DifferentiableAt 𝕜 f x → ∀ (c : R), fderiv 𝕜 (c • f) x = c • fderiv 𝕜 f x