mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Sat.CNF.RelabelFin
_private.Std.Sat.CNF.RelabelFin.0.Std.Sat.CNF.numLiterals.match_1.eq_2 : ∀ (motive : Option ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive none) (h_2 : (n : ℕ) → motive (some n)),
  (match some n with
    | none => h_1 ()
    | some n => h_2 n) =
    h_2 n
-- Lean.Meta.Sym.SymM
Lean.Meta.Sym.Canon.State.mk : Std.HashMap Lean.Expr Lean.Expr → Std.HashMap Lean.Expr Lean.Expr → Lean.Meta.Sym.Canon.State
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubAddAction.ext : ∀ {R : Type u} {M : Type v} [inst : VAdd R M] {p q : SubAddAction R M}, (∀ (x : M), x ∈ p ↔ x ∈ q) → p = q
-- Mathlib.RingTheory.Nilpotent.Basic
IsRadical.of_dvd : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] [IsCancelMulZero R] {x y : R}, IsRadical y → y ≠ 0 → x ∣ y → IsRadical x
-- Mathlib.Tactic.NormNum.Prime
Mathlib.Meta.NormNum.isNat_prime_0 : ∀ {n : ℕ}, Mathlib.Meta.NormNum.IsNat n 0 → ¬Nat.Prime n
-- Init.Data.Array.Range
Array.erase_range : ∀ {n i : ℕ}, (Array.range n).erase i = Array.range (min n i) ++ Array.range' (i + 1) (n - (i + 1))
-- Mathlib.MeasureTheory.Measure.Stieltjes
/-- **Alias** of `StieltjesFunction.length_sdiff_botSet`. -/
StieltjesFunction.length_diff_botSet : ∀ {R : Type u_1} [inst : LinearOrder R] [inst_1 : TopologicalSpace R] (f : StieltjesFunction R) {s : Set R},
  f.length (s \ botSet) = f.length s
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- The denominator of the generator.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.g : {K : Type u_1} → [inst : Field K] → IntermediateField K (RatFunc K) → Polynomial K
-- Std.Data.HashMap.Basic
Std.HashMap.instInter : {α : Type u} → {β : Type v} → [inst : BEq α] → [inst_1 : Hashable α] → Inter (Std.HashMap α β)
-- Mathlib.Order.Category.BddLat
BddLat.mk.injEq : ∀ (toLat : Lat) [isBoundedOrder : BoundedOrder ↑toLat] (toLat_1 : Lat) (isBoundedOrder_1 : BoundedOrder ↑toLat_1),
  ({ toLat := toLat, isBoundedOrder := isBoundedOrder } = { toLat := toLat_1, isBoundedOrder := isBoundedOrder_1 }) =
    (toLat = toLat_1 ∧ isBoundedOrder ≍ isBoundedOrder_1)
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasureTheory.Measure.instDistribMulActionDomMulAct : {G : Type u_1} →
  {A : Type u_2} →
    [inst : Group G] →
      [inst_1 : MulAction G A] →
        [inst_2 : MeasurableSpace A] → [MeasurableConstSMul G A] → DistribMulAction Gᵈᵐᵃ (MeasureTheory.Measure A)
-- Mathlib.Data.PNat.Xgcd
/-- Final value of `z`  -/
PNat.gcdZ : ℕ+ → ℕ+ → ℕ+
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- **Alias** of the forward direction of `AddAction.isBlock_iff_vadd_eq_of_mem`. -/
AddAction.IsBlock.vadd_eq_of_mem : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X},
  AddAction.IsBlock G B → ∀ ⦃g : G⦄ ⦃a : X⦄, a ∈ B → g +ᵥ a ∈ B → g +ᵥ B = B
-- Mathlib.Order.CompleteLattice.Chain
ChainClosure.succ_fixpoint_iff : ∀ {α : Type u_1} {r : α → α → Prop} {c : Set α}, ChainClosure r c → (SuccChain r c = c ↔ c = maxChain r)
-- Init.Data.SInt.Lemmas
ISize.lt_iff_toBitVec_slt : ∀ {a b : ISize}, a < b ↔ a.toBitVec.slt b.toBitVec = true
-- Mathlib.Control.LawfulFix
Part.ωScottContinuous_toUnitMono : ∀ {α : Type u_1} (f : Part α → Part α) (hc : OmegaCompletePartialOrder.ωScottContinuous f),
  OmegaCompletePartialOrder.ωScottContinuous ⇑(Part.toUnitMono { toFun := f, monotone' := ⋯ })
-- Lean.Meta.Tactic.Cases
Lean.Meta.GeneralizeIndicesSubgoal : Type
-- Mathlib.CategoryTheory.Sites.Hypercover.One
_private.Mathlib.CategoryTheory.Sites.Hypercover.One.0.CategoryTheory.PreOneHypercover.Hom.mapMulticospan.match_3.eq_3 : ∀ {C : Type u_3} [inst : CategoryTheory.Category.{u_2, u_3} C] {S : C} {E : CategoryTheory.PreOneHypercover S}
  (motive : (X Y : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape) → (X ⟶ Y) → Sort u_4)
  (i : E.multicospanShape.R)
  (h_1 :
    (x : CategoryTheory.Limits.WalkingMulticospan E.multicospanShape) →
      motive x x (CategoryTheory.Limits.WalkingMulticospan.Hom.id x))
  (h_2 :
    (i : E.multicospanShape.R) →
      motive (CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.fst i))
        (CategoryTheory.Limits.WalkingMulticospan.right i) (CategoryTheory.Limits.WalkingMulticospan.Hom.fst i))
  (h_3 :
    (i : E.multicospanShape.R) →
      motive (CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.snd i))
        (CategoryTheory.Limits.WalkingMulticospan.right i) (CategoryTheory.Limits.WalkingMulticospan.Hom.snd i)),
  (match CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.snd i),
      CategoryTheory.Limits.WalkingMulticospan.right i, CategoryTheory.Limits.WalkingMulticospan.Hom.snd i with
    | x, .(x), CategoryTheory.Limits.WalkingMulticospan.Hom.id .(x) => h_1 x
    | .(CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.fst i)),
      .(CategoryTheory.Limits.WalkingMulticospan.right i), CategoryTheory.Limits.WalkingMulticospan.Hom.fst i => h_2 i
    | .(CategoryTheory.Limits.WalkingMulticospan.left (E.multicospanShape.snd i)),
      .(CategoryTheory.Limits.WalkingMulticospan.right i), CategoryTheory.Limits.WalkingMulticospan.Hom.snd i =>
      h_3 i) =
    h_3 i
-- Mathlib.Analysis.Convex.Intrinsic
isClosed_intrinsicClosure : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P},
  IsClosed ↑(affineSpan 𝕜 s) → IsClosed (intrinsicClosure 𝕜 s)
-- Mathlib.Algebra.GroupWithZero.Basic
isReduced_of_subsingleton : ∀ {R : Type u_3} [inst : Zero R] [inst_1 : Pow R ℕ] [Subsingleton R], IsReduced R
-- Lean.Compiler.ExternAttr
Lean.instInhabitedExternAttrData.default : Lean.ExternAttrData
-- Mathlib.NumberTheory.EllipticDivisibilitySequence
/-- Strong recursion principle for the complement sequence for a normalised EDS: if we have
* `P 0`, `P 1`,
* for all `m : ℕ` we can prove `P (2 * (m + 3))` from `P k` for all `k < 2 * (m + 3)`, and
* for all `m : ℕ` we can prove `P (2 * (m + 2) + 1)` from `P k` for all `k < 2 * (m + 2) + 1`,

then we have `P n` for all `n : ℕ`.  -/
complEDSRec' : {P : ℕ → Sort u_4} →
  P 0 →
    P 1 →
      ((m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) → P k) → P (2 * (m + 1))) →
        ((m : ℕ) → ((k : ℕ) → k < 2 * (m + 1) + 1 → P k) → P (2 * (m + 1) + 1)) → (n : ℕ) → P n
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.mk'_apply_adj : ∀ {V : Type u} (x : { adj // (∀ (x y : V), adj x y = adj y x) ∧ ∀ (x : V), ¬adj x x = true }) (v w : V),
  (SimpleGraph.mk' x).Adj v w = (↑x v w = true)
-- Mathlib.CategoryTheory.Equivalence
/-- The forwards direction of an equivalence.  -/
CategoryTheory.Equivalence.functor : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → (C ≌ D) → CategoryTheory.Functor C D
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.X : ∀ {R : Type u_1} [inst : Semiring R], Polynomial.X.Splits
-- Init.Data.Range.Polymorphic.PRange
Std.Rxi.IsAlwaysFinite.mk : ∀ {α : Type u} [inst : Std.PRange.UpwardEnumerable α],
  (∀ (init : α), ∃ n, Std.PRange.succMany? n init = none) → Std.Rxi.IsAlwaysFinite α
-- Mathlib.Topology.Algebra.Group.Basic
continuousInv_of_discreteTopology : ∀ {H : Type x} [inst : TopologicalSpace H] [inst_1 : Inv H] [DiscreteTopology H], ContinuousInv H
-- Mathlib.Algebra.Quandle
Rack.PreEnvelGroup.brecOn.eq : ∀ {R : Type u} {motive : Rack.PreEnvelGroup R → Sort u_1} (t : Rack.PreEnvelGroup R)
  (F_1 : (t : Rack.PreEnvelGroup R) → Rack.PreEnvelGroup.below t → motive t),
  Rack.PreEnvelGroup.brecOn t F_1 = F_1 t (Rack.PreEnvelGroup.brecOn.go t F_1).2
-- Mathlib.Data.ENat.Basic
ENat.toNat_eq_iff_eq_natCast : ∀ (n : ℕ∞) (m : ℕ) [NeZero m], n.toNat = m ↔ n = ↑m
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The inverse of a bijective `MulSemiringActionHom` is a `MulSemiringActionHom`.  -/
MulSemiringActionHom.inverse : {M : Type u_1} →
  [inst : Monoid M] →
    {R : Type u_10} →
      [inst_1 : Semiring R] →
        [inst_2 : MulSemiringAction M R] →
          {S₁ : Type u_15} →
            [inst_3 : Semiring S₁] →
              [inst_4 : MulSemiringAction M S₁] →
                (f : R →+*[M] S₁) → (g : S₁ → R) → Function.LeftInverse g ⇑f → Function.RightInverse g ⇑f → S₁ →+*[M] R
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instMulZeroClassOfMulHomClassOfZeroHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → MulZeroClass (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), MulHomClass (T h) (G i) (G j)] →
                      [∀ (i j : ι) (h : i ≤ j), ZeroHomClass (T h) (G i) (G j)] → MulZeroClass (DirectLimit G f)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.polynomial_eq : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R},
  W.polynomial =
    { a := 0, b := 1, c := { a := 0, b := 0, c := W.a₁, d := W.a₃ }.toPoly,
        d := { a := -1, b := -W.a₂, c := -W.a₄, d := -W.a₆ }.toPoly }.toPoly
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.instCategoryCostructuredArrow : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor C D} →
          {T : D} → CategoryTheory.Category.{v₁, max u₁ v₂} (CategoryTheory.CostructuredArrow S T)
-- Mathlib.CategoryTheory.Retract
/-- a retract determines a split monomorphism.  -/
CategoryTheory.Retract.splitMono : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : C} → (h : CategoryTheory.Retract X Y) → CategoryTheory.SplitMono h.i
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleIntegral.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℂ E] (f : ℂ → E) (c : ℂ) (R : ℝ),
  circleIntegral f c R = ∫ (θ : ℝ) in 0..2 * Real.pi, deriv (circleMap c R) θ • f (circleMap c R θ)
-- Batteries.Data.PairingHeap
/-- `O(n log n)`. Convert the heap to a list in increasing order.  -/
Batteries.PairingHeapImp.Heap.toList : {α : Type u_1} → (α → α → Bool) → Batteries.PairingHeapImp.Heap α → List α
-- Init.Data.Vector.Basic
Vector.mk.congr_simp : ∀ {α : Type u} {n : ℕ} (toArray toArray_1 : Array α) (e_toArray : toArray = toArray_1)
  (size_toArray : toArray.size = n), Vector.mk toArray size_toArray = Vector.mk toArray_1 ⋯
-- Mathlib.Analysis.Asymptotics.TVS
/-- **Alias** of the forward direction of `Asymptotics.isLittleOTVS_iff_tendsto_div`. -/
Asymptotics.IsLittleOTVS.tendsto_div : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f : α → E} {g : α → F} {l : Filter α},
  f =o[𝕜; l] g → ∀ U ∈ nhds 0, ∃ V ∈ nhds 0, Filter.Tendsto (fun x => egauge 𝕜 U (f x) / egauge 𝕜 V (g x)) l (nhds 0)
-- Lean.Message
Lean.MessageData.ofFormatWithInfos.sizeOf_spec : ∀ (a : Lean.FormatWithInfos), sizeOf (Lean.MessageData.ofFormatWithInfos a) = 1 + sizeOf a
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
nullMeasurableSet_lt : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [OpensMeasurableSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : LinearOrder α] [SecondCountableTopology α] [OrderClosedTopology α]
  {μ : MeasureTheory.Measure δ} {f g : δ → α},
  AEMeasurable f μ → AEMeasurable g μ → MeasureTheory.NullMeasurableSet {a | f a < g a} μ
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.containsThenInsert_snd : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {v : β k}, (t.containsThenInsert k v).2 = t.insert k v
-- Mathlib.RingTheory.WittVector.Isocrystal
/-- A one-dimensional isocrystal over an algebraically closed field
admits an isomorphism to one of the standard (indexed by `m : ℤ`) one-dimensional isocrystals.  -/
WittVector.isocrystal_classification : ∀ (p : ℕ) [inst : Fact (Nat.Prime p)] (k : Type u_2) [inst_1 : Field k] [inst_2 : IsAlgClosed k] [inst_3 : CharP k p]
  (V : Type u_3) [inst_4 : AddCommGroup V] [inst_5 : WittVector.Isocrystal p k V],
  Module.finrank (FractionRing (WittVector p k)) V = 1 →
    ∃ m, Nonempty (WittVector.IsocrystalEquiv p k (WittVector.StandardOneDimIsocrystal p k m) V)
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.comulAlgHom_comp_mapRingHom : ∀ {R : Type u_1} {S : Type u_2} {M : Type u_8} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : CommMonoid M]
  (f : R →+* S),
  (Bialgebra.comulAlgHom S (MonoidAlgebra S M)).comp (MonoidAlgebra.mapRingHom M f) =
    (Algebra.TensorProduct.mapRingHom f (MonoidAlgebra.mapRingHom M f) (MonoidAlgebra.mapRingHom M f) ⋯ ⋯).comp
      (Bialgebra.comulAlgHom R (MonoidAlgebra R M)).toRingHom
-- Mathlib.RingTheory.Bialgebra.Hom
BialgHom.bialgHomClass : ∀ {R : Type u_1} {A : Type u_2} {B : Type u_3} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B],
  BialgHomClass (A →ₐc[R] B) R A B
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.min.congr_simp : ∀ {α : Type u} {cmp : α → α → Ordering} (t t_1 : Std.TreeSet α cmp) (e_t : t = t_1) (h : t.isEmpty = false),
  t.min h = t_1.min ⋯
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
/-- A `E₂`-cohomological spectral sequence lying on finitely many rows
has differentials given by the vector `(r, 1 - r)` on the `r`th page for `2 ≤ r`.  -/
CategoryTheory.E₂CohomologicalSpectralSequenceFin : (C : Type u_1) → [inst : CategoryTheory.Category.{u_3, u_1} C] → [CategoryTheory.Abelian C] → ℕ → Type (max u_1 u_3)
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Inverse
Filter.Tendsto.arcsin_nhdsGE : ∀ {α : Type u_1} {l : Filter α} {x : ℝ} {f : α → ℝ},
  Filter.Tendsto f l (nhdsWithin x (Set.Ici x)) →
    Filter.Tendsto (fun x => Real.arcsin (f x)) l (nhdsWithin (Real.arcsin x) (Set.Ici (Real.arcsin x)))
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Functor.toProfunctorRev_obj_obj : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D) (X : D) (X_1 : Cᵒᵖ),
  (F.toProfunctorRev.obj X).obj X_1 = (F.obj (Opposite.unop X_1) ⟶ X)
-- Lean.Meta.AppBuilder
Lean.Meta.mkSome : Lean.Expr → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.RingTheory.AdicCompletion.Basic
/-- The canonical linear map from Cauchy sequences to the completion.  -/
AdicCompletion.mk : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_4) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] → AdicCompletion.AdicCauchySequence I M →ₗ[R] AdicCompletion I M
-- Mathlib.Algebra.Category.AlgCat.Basic
AlgCat.instAlgebraCarrierObjRingCatForget₂AlgHomCarrierRingHom : (R : Type u) → [inst : CommRing R] → (A : AlgCat R) → Algebra R ↑((CategoryTheory.forget₂ (AlgCat R) RingCat).obj A)
-- Mathlib.NumberTheory.LegendreSymbol.AddCharacter
/-- The first projection from `PrimitiveAddChar`, giving the cyclotomic field.  -/
AddChar.PrimitiveAddChar.n : {R : Type u} → [inst : CommRing R] → {R' : Type v} → [inst_1 : Field R'] → AddChar.PrimitiveAddChar R R' → ℕ+
-- Mathlib.Order.UpperLower.Closure
/-- **Alias** of the forward direction of `bddAbove_lowerClosure`. -/
BddAbove.of_lowerClosure : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, BddAbove ↑(lowerClosure s) → BddAbove s
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.EMatchTheoremConstraint.depthLt.injEq : ∀ (lhs n lhs_1 n_1 : ℕ),
  (Lean.Meta.Grind.EMatchTheoremConstraint.depthLt lhs n = Lean.Meta.Grind.EMatchTheoremConstraint.depthLt lhs_1 n_1) =
    (lhs = lhs_1 ∧ n = n_1)
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousAddMonoidHom.compLeft.eq_1 : ∀ {A : Type u_2} {B : Type u_3} (E : Type u_6) [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : AddCommGroup E]
  [inst_3 : TopologicalSpace A] [inst_4 : TopologicalSpace B] [inst_5 : TopologicalSpace E]
  [inst_6 : IsTopologicalAddGroup E] (f : A →ₜ+ B),
  ContinuousAddMonoidHom.compLeft E f =
    { toFun := fun g => g.comp f, map_zero' := ⋯, map_add' := ⋯, continuous_toFun := ⋯ }
-- Mathlib.AlgebraicGeometry.OpenImmersion
/-- The universal property of open immersions:
For an open immersion `f : X ⟶ Z`, given any morphism of schemes `g : Y ⟶ Z` whose topological
image is contained in the image of `f`, we can lift this morphism to a unique `Y ⟶ X` that
commutes with these maps.
 -/
AlgebraicGeometry.IsOpenImmersion.lift : {X Y Z : AlgebraicGeometry.Scheme} →
  (f : X ⟶ Z) → (g : Y ⟶ Z) → [H : AlgebraicGeometry.IsOpenImmersion f] → Set.range ⇑g ⊆ Set.range ⇑f → (Y ⟶ X)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
/-- Mapping from variables to their "lower" bounds. We say a relational constraint `c` is a lower bound for a variable `x`
if `x` is the maximal variable in `c`, and `x` coefficient in `c` is negative.
 -/
Lean.Meta.Grind.Arith.Cutsat.State.lowers : Lean.Meta.Grind.Arith.Cutsat.State → Lean.PArray (Lean.PArray Lean.Meta.Grind.Arith.Cutsat.LeCnstr)
-- Mathlib.Algebra.Order.Monoid.Unbundled.Defs
/-- Typeclass for monotonicity of multiplication on the left,
namely `b₁ < b₂ → a * b₁ < a * b₂`.

You should usually not use this very granular typeclass directly, but rather a typeclass like
`IsOrderedMonoid`.  -/
MulLeftStrictMono : (M : Type u_1) → [Mul M] → [LT M] → Prop
-- Mathlib.NumberTheory.ZetaValues
hasSum_one_div_pow_mul_fourier_mul_bernoulliFun : ∀ {k : ℕ},
  2 ≤ k →
    ∀ {x : ℝ},
      x ∈ Set.Icc 0 1 →
        HasSum (fun n => 1 / ↑n ^ k * (fourier n) ↑x)
          (-(2 * ↑Real.pi * Complex.I) ^ k / ↑k.factorial * ↑(bernoulliFun k x))
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.primeHeight_lt_top : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R) [I.FiniteHeight] [inst_2 : I.IsPrime], Ideal.primeHeight✝ I < ⊤
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.sup_factors_of_factors_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasImages C]
  [inst_2 : CategoryTheory.Limits.HasBinaryCoproducts C] {A B : C} {X Y : CategoryTheory.Subobject B} {f : A ⟶ B},
  Y.Factors f → (X ⊔ Y).Factors f
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.Spanning.mk : ∀ {α : Type u_2} {M : Matroid α} {S : Set α}, M.closure S = M.E → S ⊆ M.E → M.Spanning S
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.spectralSequencePageXIso.congr_simp : ∀ {C : Type u_1} {ι : Type u_2} {κ : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Abelian C] [inst_2 : Preorder ι] (X : CategoryTheory.Abelian.SpectralObject C ι)
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀)
  [inst_3 : X.HasSpectralSequence data] (r : ℤ) (hr : r₀ ≤ r) (pq : κ) (i₀ i₁ i₂ i₃ : ι) (h₀ : i₀ = data.i₀ r pq ⋯)
  (h₁ : i₁ = data.i₁ pq) (h₂ : i₂ = data.i₂ pq) (h₃ : i₃ = data.i₃ r pq ⋯) (n₀ n₁ n₂ : ℤ) (h : n₁ = data.deg pq)
  (hn₁ : n₀ + 1 = n₁) (hn₂ : n₁ + 1 = n₂),
  X.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁ hn₂ =
    X.spectralSequencePageXIso data r hr pq i₀ i₁ i₂ i₃ h₀ h₁ h₂ h₃ n₀ n₁ n₂ h hn₁ hn₂
-- Mathlib.AlgebraicGeometry.Cover.Directed
AlgebraicGeometry.Scheme.Cover.LocallyDirected.directed : ∀ {P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} {X : AlgebraicGeometry.Scheme}
  {𝒰 : AlgebraicGeometry.Scheme.Cover (AlgebraicGeometry.Scheme.precoverage P) X}
  {inst : CategoryTheory.Category.{v_1, u_1} 𝒰.I₀} [self : 𝒰.LocallyDirected] {i j : 𝒰.I₀}
  (x : ↥(CategoryTheory.Limits.pullback (𝒰.f i) (𝒰.f j))),
  ∃ k hki hkj y,
    (CategoryTheory.Limits.pullback.lift (AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans hki)
          (AlgebraicGeometry.Scheme.Cover.LocallyDirected.trans hkj) ⋯)
        y =
      x
-- Init.Data.String.Basic
String.Slice.Pos.cast_cast : ∀ {s t u : String.Slice} {hst : s.copy = t.copy} {htu : t.copy = u.copy} {pos : s.Pos},
  (pos.cast hst).cast htu = pos.cast ⋯
-- Mathlib.Analysis.Calculus.FDeriv.Add
HasStrictFDerivAt.add : ∀ {𝕜 : 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 g : E → F}
  {f' g' : E →L[𝕜] F} {x : E},
  HasStrictFDerivAt f f' x → HasStrictFDerivAt g g' x → HasStrictFDerivAt (f + g) (f' + g') x
-- Mathlib.Topology.ApproximateUnit
/-- If `l` is an approximate unit and `⊥ < l' ≤ l`, then `l'` is also an approximate unit.  -/
Filter.IsApproximateUnit.mono : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : MulOneClass α] {l l' : Filter α},
  l.IsApproximateUnit → l' ≤ l → ∀ [hl' : l'.NeBot], l'.IsApproximateUnit
-- Mathlib.Algebra.Lie.Classical
/-- A matrix for transforming the indefinite diagonal bilinear form into the definite one, provided
the parameter `i` is a square root of -1.  -/
LieAlgebra.Orthogonal.Pso : (p : Type u_2) →
  (q : Type u_3) → (R : Type u₂) → [DecidableEq p] → [DecidableEq q] → [CommRing R] → R → Matrix (p ⊕ q) (p ⊕ q) R
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_mem_commutator : ∀ {G : Type u_1} [inst : Group G] {g₁ g₂ : G} {H₁ H₂ : Subgroup G}, g₁ ∈ H₁ → g₂ ∈ H₂ → ⁅g₁, g₂⁆ ∈ ⁅H₁, H₂⁆
-- Mathlib.Order.Heyting.Basic
le_compl_comm : ∀ {α : Type u_2} [inst : HeytingAlgebra α] {a b : α}, a ≤ bᶜ ↔ b ≤ aᶜ
-- Lean.Data.NameMap.Basic
Lean.NameMap.find? : {α : Type} → Lean.NameMap α → Lean.Name → Option α
-- Mathlib.Data.Rel
SetRel.isSymm_preimage : ∀ {α : Type u_1} {β : Type u_2} {R : SetRel α α} {f : β → α} [R.IsSymm], SetRel.IsSymm (Prod.map f f ⁻¹' R)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- A set `B` is a `G`-invariant block if `g +ᵥ B ⊆ B` for all `g : G`.

Note: It is not necessarily a block when the action is not by a group.  -/
AddAction.IsInvariantBlock : (G : Type u_1) → {X : Type u_2} → [VAdd G X] → Set X → Prop
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.skipSuffixWhile_eq_skipSuffixWhile_toSlice : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.BackwardPattern pat] {s : String},
  s.skipSuffixWhile pat = String.Pos.ofToSlice (s.toSlice.skipSuffixWhile pat)
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions
CategoryTheory.MorphismProperty.LeftFraction.map_eq_of_map_eq : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {W : CategoryTheory.MorphismProperty C} {X Y : C}
  (φ₁ φ₂ : W.LeftFraction X Y) {E : Type u_3} [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  (L₁ : CategoryTheory.Functor C D) (L₂ : CategoryTheory.Functor C E) [inst_3 : L₁.IsLocalization W]
  [inst_4 : L₂.IsLocalization W], φ₁.map L₁ ⋯ = φ₂.map L₁ ⋯ → φ₁.map L₂ ⋯ = φ₂.map L₂ ⋯
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.IsColoop.dual_isLoop : ∀ {α : Type u_1} {M : Matroid α} {e : α}, M.IsColoop e → M✶.IsLoop e
-- Mathlib.Analysis.InnerProductSpace.Symmetric
LinearMap.IsSymmetricProjection.sub_of_range_le_range : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {p q : E →ₗ[𝕜] E},
  p.IsSymmetricProjection → q.IsSymmetricProjection → p.range ≤ q.range → (q - p).IsSymmetricProjection
-- Mathlib.Analysis.Asymptotics.TVS
Asymptotics.IsBigOTVS.congr_left : ∀ {α : Type u_1} {𝕜 : Type u_3} {E : Type u_4} {F : Type u_5} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : AddCommGroup E] [inst_2 : TopologicalSpace E] [inst_3 : Module 𝕜 E] [inst_4 : AddCommGroup F]
  [inst_5 : TopologicalSpace F] [inst_6 : Module 𝕜 F] {f₁ f₂ : α → E} {g : α → F} {l : Filter α},
  f₁ =O[𝕜; l] g → (∀ (x : α), f₁ x = f₂ x) → f₂ =O[𝕜; l] g