mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Combinatorics.SimpleGraph.CompleteMultipartite
SimpleGraph.not_isCompleteMultipartite_of_pathGraph3ComplEmbedding : ∀ {α : Type u} {G : SimpleGraph α} (e : (SimpleGraph.pathGraph 3)ᶜ ↪g G), ¬G.IsCompleteMultipartite
-- Mathlib.LinearAlgebra.Matrix.Reindex
Matrix.reindexAlgEquiv_apply : ∀ {m : Type u_2} {n : Type u_3} (R : Type u_11) (A : Type u_12) [inst : CommSemiring R] [inst_1 : Fintype n]
  [inst_2 : Fintype m] [inst_3 : DecidableEq m] [inst_4 : DecidableEq n] [inst_5 : Semiring A] [inst_6 : Algebra R A]
  (e : m ≃ n) (M : Matrix m m A), (Matrix.reindexAlgEquiv R A e) M = (Matrix.reindex e e) M
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput.mk : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {aig : Std.Sat.AIG α} →
        {len : ℕ} → aig.RefVec len → aig.Ref → Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.ShiftConcatInput aig len
-- Mathlib.Tactic.ITauto
Mathlib.Tactic.ITauto.Proof.orInL.inj : ∀ {p p_1 : Mathlib.Tactic.ITauto.Proof}, p.orInL = p_1.orInL → p = p_1
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.preEquivalence_functor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  {G : CategoryTheory.Functor D E} {e : E} (f : CategoryTheory.StructuredArrow e G),
  (CategoryTheory.StructuredArrow.preEquivalence F f).functor = CategoryTheory.StructuredArrow.preEquivalenceFunctor F f
-- Mathlib.Data.Set.Restrict
/-- **Alias** of `Set.restrictPreimage_injective`. -/
Function.Injective.restrictPreimage : ∀ {α : Type u_1} {β : Type u_2} (t : Set β) {f : α → β},
  Function.Injective f → Function.Injective (t.restrictPreimage f)
-- Mathlib.Topology.MetricSpace.HolderNorm
HolderWith.nnholderNorm_le : ∀ {X : Type u_1} {Y : Type u_2} [inst : MetricSpace X] [inst_1 : EMetricSpace Y] {C r : NNReal} {f : X → Y},
  HolderWith C r f → nnHolderNorm r f ≤ C
-- Mathlib.Analysis.Complex.BorelCaratheodory
/-- **Borel-Carathéodory theorem** for functions vanishing at the origin.

If `f` is analytic on the open ball `‖z‖ < R`, satisfies `(f z).re ≤ M` for all such `z`,
and `f 0 = 0`, then `‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)` for all `‖z‖ < R`.  -/
Complex.borelCaratheodory_zero : ∀ {f : ℂ → ℂ} {M R : ℝ} {z : ℂ},
  0 < M →
    DifferentiableOn ℂ f (Metric.ball 0 R) →
      Set.MapsTo f (Metric.ball 0 R) {z | z.re ≤ M} →
        0 < R → z ∈ Metric.ball 0 R → f 0 = 0 → ‖f z‖ ≤ 2 * M * ‖z‖ / (R - ‖z‖)
-- Mathlib.Order.Minimal
minimal_lt_iff : ∀ {α : Type u_2} {x y : α} [inst : Preorder α], Minimal (fun x => x < y) x ↔ x < y ∧ IsMin x
-- Mathlib.RingTheory.WittVector.Defs
WittVector.constantCoeff_wittAdd : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (n : ℕ), MvPolynomial.constantCoeff (WittVector.wittAdd p n) = 0
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
_private.Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv.0.Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.match_1.splitter : {α : Type} →
  [inst : Hashable α] →
    [inst_1 : DecidableEq α] →
      {w : ℕ} →
        (aig : Std.Sat.AIG α) →
          (motive : aig.BinaryRefVec w → Sort u_1) →
            (input : aig.BinaryRefVec w) → ((lhs rhs : aig.RefVec w) → motive { lhs := lhs, rhs := rhs }) → motive input
-- Init.Grind.Ordered.Linarith
/-- Converts the given expression into a polynomial.  -/
Lean.Grind.Linarith.Expr.toPoly' : Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Poly
-- Mathlib.Data.Multiset.Defs
Multiset.Nodup.ext : ∀ {α : Type u_1} {s t : Multiset α}, s.Nodup → t.Nodup → (s = t ↔ ∀ (a : α), a ∈ s ↔ a ∈ t)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Types
Lean.Meta.Grind.Arith.Linear.RingIneqCnstrProof : Type
-- Init.Data.Array.Lemmas
Array.toList_extract : ∀ {α : Type u_1} {xs : Array α} {start stop : ℕ}, (xs.extract start stop).toList = xs.toList.extract start stop
-- Mathlib.RingTheory.MatrixAlgebra
MatrixEquivTensor.invFun_algebraMap : ∀ (n : Type u_3) (R : Type u_5) (A : Type u_7) [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A]
  [inst_3 : DecidableEq n] [inst_4 : Fintype n] (M : Matrix n n R),
  MatrixEquivTensor.invFun n R A (M.map ⇑(algebraMap R A)) = 1 ⊗ₜ[R] M
-- Init.Data.Order.MinMaxOn
minOn_eq_min : ∀ {α : Type u_1} {β : Type u_2} [inst : Min α] [inst_1 : LE α] [DecidableLE α] [Std.LawfulOrderLeftLeaningMin α]
  [inst_4 : LE β] [inst_5 : DecidableLE β] {f : α → β} {a b : α}, (f a ≤ f b ↔ a ≤ b) → minOn f a b = a ⊓ b
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- A `MvPolynomial φ` is symmetric if it is invariant under
permutations of its variables by the `rename` operation  -/
MvPolynomial.IsSymmetric : {σ : Type u_1} → {R : Type u_3} → [inst : CommSemiring R] → MvPolynomial σ R → Prop
-- Init.Data.Range.Polymorphic.UInt
UInt8.instLawfulUpwardEnumerable : Std.PRange.LawfulUpwardEnumerable UInt8
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.foldM_eq_foldlM_keysArray : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) {δ : Type w} {m' : Type w → Type w'}
  [inst : Monad m'] [LawfulMonad m'] {f : δ → α → m' δ} {init : δ},
  Std.DHashMap.Raw.foldM (fun d a x => f d a) init ↑m = Array.foldlM f init (↑m).keysArray
-- Mathlib.CategoryTheory.Sites.Over
/-- For `f : X ⟶ Y`, this is the morphism from `F.over Y` to the pushforward of `F.over X`
along `Over.pullback f` induced by `Limits.pullback.fst`.  -/
CategoryTheory.Sheaf.toPushforwardOverPullback : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {A : Type u'} →
        [inst_1 : CategoryTheory.Category.{v', u'} A] →
          [inst_2 : CategoryTheory.Limits.HasPullbacks C] →
            (F : CategoryTheory.Sheaf J A) →
              {X Y : C} →
                (f : X ⟶ Y) →
                  F.over Y ⟶
                    ((CategoryTheory.Over.pullback f).sheafPushforwardContinuous A (J.over Y) (J.over X)).obj (F.over X)
-- Init.Notation
/-- * The `by_elab doSeq` expression runs the `doSeq` as a `TermElabM Expr` to
  synthesize the expression.
* `by_elab fun expectedType? => do doSeq` receives the expected type (an `Option Expr`)
  as well.
 -/
Lean.byElab : Lean.ParserDescr
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.natCast_lt_omega0 : ∀ (n : ℕ), ↑n < Ordinal.omega0
-- Batteries.Data.UnionFind.Basic
Batteries.UnionFind.find_root_1 : ∀ (self : Batteries.UnionFind) (x : Fin self.size) (i : ℕ), (self.find x).fst.rootD i = self.rootD i
-- Mathlib.Algebra.GradedMonoid
List.dProd_cons : ∀ {ι : Type u_1} {α : Type u_2} {A : ι → Type u_3} [inst : AddMonoid ι] [inst_1 : GradedMonoid.GMonoid A] (fι : α → ι)
  (fA : (a : α) → A (fι a)) (a : α) (l : List α), (a :: l).dProd fι fA = GradedMonoid.GMul.mul (fA a) (l.dProd fι fA)
-- Mathlib.Data.Set.Lattice
Set.iInter_union_of_antitone : ∀ {ι : Type u_12} {α : Type u_13} [inst : Preorder ι] [IsDirectedOrder ι] {s t : ι → Set α},
  Antitone s → Antitone t → ⋂ i, s i ∪ t i = (⋂ i, s i) ∪ ⋂ i, t i
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.sheafYonedaHom.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] {K : CategoryTheory.GrothendieckTopology D} {A : Type u_4}
  [inst_2 : CategoryTheory.Category.{v_4, u_4} A] {G : CategoryTheory.Functor C D} [inst_3 : G.IsCoverDense K]
  [inst_4 : G.IsLocallyFull K] {ℱ : CategoryTheory.Functor Dᵒᵖ A} {ℱ' : CategoryTheory.Sheaf K A}
  (α α_1 : G.op.comp ℱ ⟶ G.op.comp ℱ'.obj),
  α = α_1 →
    CategoryTheory.Functor.IsCoverDense.sheafYonedaHom α = CategoryTheory.Functor.IsCoverDense.sheafYonedaHom α_1
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rci.toList_toArray : ∀ {α : Type u} {r : Std.Rci α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.PRange.LawfulUpwardEnumerable α]
  [inst_2 : Std.Rxi.IsAlwaysFinite α], r.toArray.toList = r.toList
-- Mathlib.Algebra.Group.Equiv.Defs
/-- Transitivity of addition-preserving isomorphisms  -/
AddEquiv.trans : {M : Type u_4} →
  {N : Type u_5} → {P : Type u_6} → [inst : Add M] → [inst_1 : Add N] → [inst_2 : Add P] → M ≃+ N → N ≃+ P → M ≃+ P
-- Mathlib.Data.Nat.Fib.Basic
/-- **Alias** of `Nat.fastFibAux_eq`. -/
Nat.fast_fib_aux_eq : ∀ (n : ℕ), n.fastFibAux = (Nat.fib n, Nat.fib (n + 1))
-- Mathlib.Order.Category.BddDistLat
/-- Turn a morphism in `BddDistLat` back into a `BoundedLatticeHom`.  -/
BddDistLat.Hom.hom : {X Y : BddDistLat} → X.Hom Y → BoundedLatticeHom ↑X.toDistLat ↑Y.toDistLat
-- Mathlib.CategoryTheory.Products.Associator
CategoryTheory.prod.prodμ_functor_map : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] (D : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (E : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (A : Type u₄)
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A] {X Y : (A × C) × D × E} (f : X ⟶ Y),
  (CategoryTheory.prod.prodμ C D E A).functor.map f =
    CategoryTheory.Prod.mkHom (CategoryTheory.Prod.mkHom f.1.1 f.2.1) (CategoryTheory.Prod.mkHom f.1.2 f.2.2)
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Basic
WeierstrassCurve.preΨ_ofNat : ∀ {R : Type r} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℕ), W.preΨ ↑n = W.preΨ' n
-- Mathlib.MeasureTheory.Constructions.SimpleGraph
SimpleGraph.measurable_adj : ∀ {V : Type u_1}, Measurable SimpleGraph.Adj
-- Std.Data.TreeMap.Raw.Basic
/-- Checks whether a key is present in a map, returning the associated value, and inserts a value for
the key if it was not found.

If the returned value is `some v`, then the returned map is unaltered. If it is `none`, then the
returned map has a new value inserted.

Equivalent to (but potentially faster than) calling `get?` followed by `insertIfNew`.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.TreeMap.Raw.getThenInsertIfNew? : {α : Type u} →
  {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → β → Option β × Std.TreeMap.Raw α β cmp
-- Std.Internal.Do.WP.Lemmas
Std.Internal.Do.WPMonad.le_wp_set_StateT_apply : ∀ {Pred : Type u_1} {EPred : Type u_2} {m : Type u → Type v} [inst : Monad m] [inst_1 : Std.Internal.Do.Assertion Pred]
  [inst_2 : Std.Internal.Do.Assertion EPred] [inst_3 : Std.Internal.Do.WPMonad m Pred EPred] {σ : Type u} (x : σ)
  (post : PUnit.{u + 1} → σ → Pred) (epost : EPred),
  Lean.Order.PartialOrder.rel (fun x_1 => post PUnit.unit x) (Std.Internal.Do.wp (set x) post epost)
-- Mathlib.Algebra.Ring.IsFormallyReal
IsFormallyReal.of_eq_zero_of_eq_zero_of_mul_self_add : ∀ {R : Type u_1} [inst : NonUnitalNonAssocSemiring R],
  (∀ {s a : R}, IsSumSq s → a * a + s = 0 → a = 0) → IsFormallyReal R
-- Mathlib.Data.Bool.Basic
Bool.decide_false : ∀ {p : Prop} [inst : Decidable p], ¬p → decide p = false
-- Lean.Meta.ArgsPacker
/-- Given expression `e` of type `(x : a ⊗' b ⊕' c ⊗' d) → e[x]`, wraps that expression
to produce an expression of the isomorphic type
```
((x: a) → (y : b) → e[.inl (x,y)]) ∧ ((x : c) → (y : d) → e[.inr (x,y)])
```
 -/
Lean.Meta.ArgsPacker.curry : Lean.Meta.ArgsPacker → Lean.Expr → Lean.MetaM Lean.Expr
-- Mathlib.NumberTheory.Divisors
Nat.divisors_subset_of_dvd : ∀ {n m : ℕ}, n ≠ 0 → m ∣ n → m.divisors ⊆ n.divisors
-- Init.Data.Array.Lemmas
Array.toList_eraseIdxIfInBounds : ∀ {α : Type u_1} {xs : Array α} {i : ℕ}, (xs.eraseIdxIfInBounds i).toList = xs.toList.eraseIdx i
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.add : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [Add α] → Add (Matrix m n α)
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
mfderiv_comp : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {E'' : Type u_8}
  [inst_11 : NormedAddCommGroup E''] [inst_12 : NormedSpace 𝕜 E''] {H'' : Type u_9} [inst_13 : TopologicalSpace H'']
  {I'' : ModelWithCorners 𝕜 E'' H''} {M'' : Type u_10} [inst_14 : TopologicalSpace M''] [inst_15 : ChartedSpace H'' M'']
  {f : M → M'} (x : M) {g : M' → M''},
  MDiffAt g (f x) → MDiffAt f x → mfderiv% (g ∘ f) x = mfderiv% g (f x) ∘SL mfderiv% f x
-- Mathlib.CategoryTheory.Bicategory.Functor.LocallyDiscrete
CategoryTheory.Functor.toPseudofunctor'_mapId : ∀ {I : Type u_1} {B : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} I] [inst_1 : CategoryTheory.Bicategory B]
  [inst_2 : CategoryTheory.Bicategory.Strict B] (F : CategoryTheory.Functor I B) (x : CategoryTheory.LocallyDiscrete I),
  F.toPseudofunctor'.mapId x = CategoryTheory.eqToIso ⋯
-- Lean.Meta.Tactic.Injection
Lean.Meta.injectionCore : Lean.MVarId → Lean.FVarId → Lean.MetaM Lean.Meta.InjectionResultCore
-- Mathlib.Analysis.Complex.UpperHalfPlane.Measure
UpperHalfPlane.instIsLocallyFiniteMeasureComapComplexCoeVolume : MeasureTheory.IsLocallyFiniteMeasure (MeasureTheory.Measure.comap UpperHalfPlane.coe MeasureTheory.volume)
-- Mathlib.FieldTheory.Galois.GaloisClosure
FiniteGaloisIntermediateField.le_iff : ∀ {k : Type u_1} {K : Type u_2} [inst : Field k] [inst_1 : Field K] [inst_2 : Algebra k K]
  (L₁ L₂ : FiniteGaloisIntermediateField k K), L₁ ≤ L₂ ↔ L₁.toIntermediateField ≤ L₂.toIntermediateField
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.isSuccPrelimit_mul_left : ∀ {a b : Ordinal.{u_4}}, Order.IsSuccLimit a → Order.IsSuccPrelimit (a * b)
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.condIndep_limsup_atBot_self : ∀ {Ω : Type u_2} {ι : Type u_3} {s : ι → MeasurableSpace Ω} {m m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω}
  [inst : SemilatticeInf ι] [NoMinOrder ι] [Nonempty ι] [inst_3 : StandardBorelSpace Ω] (hm : m ≤ m0)
  [inst_4 : MeasureTheory.IsFiniteMeasure μ],
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.iCondIndep m hm s μ →
      ProbabilityTheory.CondIndep m (Filter.limsup s Filter.atBot) (Filter.limsup s Filter.atBot) hm μ
-- Mathlib.CategoryTheory.ObjectProperty.ColimitsOfShape
CategoryTheory.ObjectProperty.prop_colimit : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.ObjectProperty C) {J : Type u'}
  [inst_1 : CategoryTheory.Category.{v', u'} J] [P.IsClosedUnderColimitsOfShape J] (F : CategoryTheory.Functor J C)
  [inst_3 : CategoryTheory.Limits.HasColimit F], (∀ (j : J), P (F.obj j)) → P (CategoryTheory.Limits.colimit F)
-- Std.Sat.AIG.CachedLemmas
/-- `mkAtomCached` pushes to the input AIG upon a cache miss.
 -/
Std.Sat.AIG.mkAtomCached_miss_aig : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {var : α} (aig : Std.Sat.AIG α),
  aig.cache.get? (Std.Sat.AIG.Decl.atom var) = none →
    (aig.mkAtomCached var).aig.decls = aig.decls.push (Std.Sat.AIG.Decl.atom var)
-- Mathlib.Computability.AkraBazzi.AkraBazzi
/-- The main proof of the upper-bound part of the Akra-Bazzi theorem. The factor `1 - ε n` does not
change the asymptotic order, but it is needed for the induction step to go through.  -/
AkraBazziRecurrence.T_isBigO_smoothingFn_mul_asympBound : ∀ {α : Type u_1} [inst : Fintype α] {T : ℕ → ℝ} {g : ℝ → ℝ} {a b : α → ℝ} {r : α → ℕ → ℕ} [inst_1 : Nonempty α]
  (R : AkraBazziRecurrence T g a b r),
  T =O[Filter.atTop] fun n => (1 - AkraBazziRecurrence.smoothingFn ↑n) * AkraBazziRecurrence.asympBound g a b n
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- The `q`-expansion of a function on the upper half plane, bundled as a `FormalMultilinearSeries`.

TODO: Maybe get rid of this and instead define a general API for converting `PowerSeries` to
`FormalMultilinearSeries`.
 -/
UpperHalfPlane.qExpansionFormalMultilinearSeries : {F : Type u_1} → [FunLike F UpperHalfPlane ℂ] → ℝ → F → FormalMultilinearSeries ℂ ℂ ℂ
-- Mathlib.Analysis.SpecificLimits.Basic
/-- If when `x` tends to `∞`, `f x / g x` tends to a positive constant, then `f` tends to `∞` if
and only if `g` tends to `∞`.  -/
Filter.Tendsto.num_atTop_iff_den_atTop : ∀ {α : Type u_4} {K : Type u_5} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : TopologicalSpace K] [OrderTopology K] [ContinuousInv K] {f g : α → K} {l : Filter α} {a : K},
  0 < a →
    Filter.Tendsto (fun x => f x / g x) l (nhds a) → (Filter.Tendsto f l Filter.atTop ↔ Filter.Tendsto g l Filter.atTop)
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.PendingSolverPropagationsData.diseqs.injEq : ∀ (solverId : ℕ) (ps : Lean.Meta.Grind.ParentSet) (rest : Lean.Meta.Grind.PendingSolverPropagationsData✝)
  (solverId_1 : ℕ) (ps_1 : Lean.Meta.Grind.ParentSet) (rest_1 : Lean.Meta.Grind.PendingSolverPropagationsData✝),
  (Lean.Meta.Grind.PendingSolverPropagationsData.diseqs✝ solverId ps rest =
      Lean.Meta.Grind.PendingSolverPropagationsData.diseqs✝ solverId_1 ps_1 rest_1) =
    (solverId = solverId_1 ∧ ps = ps_1 ∧ rest = rest_1)
-- Mathlib.Algebra.SkewMonoidAlgebra.Basic
SkewMonoidAlgebra.smul_of : ∀ (k : Type u_1) (G : Type u_2) [inst : Semiring k] [inst_1 : Monoid G] [inst_2 : MulSemiringAction G k] (g : G)
  (r : k), r • (SkewMonoidAlgebra.of k G) g = SkewMonoidAlgebra.single g r
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.smulZeroClass.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {A : Type u_8} [inst_1 : SMulZeroClass A R],
  MonoidAlgebra.smulZeroClass =
    { smul := fun a a_1 => MonoidAlgebra.coeffEquiv.2 (a • MonoidAlgebra.coeffEquiv.toFun a_1), smul_zero := ⋯ }
-- Mathlib.Algebra.Homology.HomotopyCategory.ShiftSequence
CochainComplex.liftCycles_shift_homologyπ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.CategoryWithHomology C] (K : CochainComplex C ℤ) {A : C} {n i : ℤ}
  (f : A ⟶ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).X i) (j : ℤ)
  (hj : (ComplexShape.up ℤ).next i = j)
  (hf : CategoryTheory.CategoryStruct.comp f (((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K).d i j) = 0)
  (i' : ℤ) (hi' : n + i = i') (j' : ℤ) (hj' : (ComplexShape.up ℤ).next i' = j'),
  CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.liftCycles ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) f j hj hf)
      (HomologicalComplex.homologyπ ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) n).obj K) i) =
    CategoryTheory.CategoryStruct.comp
      (HomologicalComplex.liftCycles K (CategoryTheory.CategoryStruct.comp f (K.shiftFunctorObjXIso n i i' ⋯).hom) j'
        hj' ⋯)
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyπ K i')
        (((HomologicalComplex.homologyFunctor C (ComplexShape.up ℤ) 0).shiftIso n i i' hi').inv.app K))
-- Mathlib.Probability.Independence.ZeroOne
ProbabilityTheory.Kernel.measure_zero_or_one_of_measurableSet_limsup : ∀ {α : Type u_1} {Ω : Type u_2} {ι : Type u_3} {_mα : MeasurableSpace α} {s : ι → MeasurableSpace Ω}
  {m0 : MeasurableSpace Ω} {κ : ProbabilityTheory.Kernel α Ω} {μα : MeasureTheory.Measure α} {β : Type u_4}
  {p : Set ι → Prop} {f : Filter ι} {ns : β → Set ι},
  (∀ (n : ι), s n ≤ m0) →
    ProbabilityTheory.Kernel.iIndep s κ μα →
      (∀ (t : Set ι), p t → tᶜ ∈ f) →
        Directed (fun x1 x2 => x1 ⊆ x2) ns →
          (∀ (a : β), p (ns a)) →
            (∀ (n : ι), ∃ a, n ∈ ns a) → ∀ {t : Set Ω}, MeasurableSet t → ∀ᵐ (a : α) ∂μα, (κ a) t = 0 ∨ (κ a) t = 1
-- Mathlib.Algebra.Group.Prod
Prod.instCancelMonoid : {M : Type u_3} → {N : Type u_4} → [CancelMonoid M] → [CancelMonoid N] → CancelMonoid (M × N)
-- Batteries.Recycling.RBTree.WF
/-- The red-red invariant is a weakening of the red-black balance invariant which allows
the root to be red with red children, but does not allow any other violations.
It occurs as a temporary condition in the `insert` and `erase` functions.

The `p` parameter allows the `.redred` case to be dependent on an additional condition.
If it is false, then this is equivalent to the usual red-black invariant.
 -/
RBTree.RBNode.RedRed : Prop → {α : Type u_1} → RBTree.RBNode α → ℕ → Prop
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr : ∀ (n w : ℕ) (x x' : BitVec w), x = x' → x'.rotateLeft n = x.rotateLeft n
-- Init.Grind.Ordered.Module
Lean.Grind.OrderedAdd.add_le_right_iff : ∀ {M : Type u} [inst : LE M] [inst_1 : Std.IsPreorder M] [inst_2 : Lean.Grind.AddCommMonoid M] [Lean.Grind.OrderedAdd M]
  {a b : M} (c : M), a ≤ b ↔ c + a ≤ c + b
-- Mathlib.Algebra.Group.Translate
translate_zero_right : ∀ {α : Type u_2} {G : Type u_5} [inst : AddCommGroup G] [inst_1 : Zero α] (a : G), translate a 0 = 0
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.foldrM_eq_foldrM_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : α → δ → m δ} {init : δ},
  Std.ExtTreeSet.foldrM f init t = List.foldrM f init t.toList
-- Init.Control.Lawful.MonadAttach.Lemmas
_private.Init.Control.Lawful.MonadAttach.Lemmas.0.MonadAttach.pbind.eq_1 : ∀ {m : Type u_1 → Type u_2} {α β : Type u_1} [inst : Monad m] [inst_1 : MonadAttach m] (x : m α)
  (f : (a : α) → MonadAttach.CanReturn x a → m β),
  MonadAttach.pbind x f = do
    let x_1 ← MonadAttach.attach x
    match x_1 with
      | ⟨a, ha⟩ => f a ha
-- Mathlib.Order.SuccPred.Basic
Order.Ioo_eq_empty_iff_pred_le : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : PredOrder α] {a b : α} [NoMinOrder α],
  Set.Ioo b a = ∅ ↔ Order.pred a ≤ b
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
/-- The affine subspace `as` is tangent to the sphere `s` at some point.  -/
EuclideanGeometry.Sphere.IsTangent : {V : Type u_1} →
  {P : Type u_2} →
    [inst : NormedAddCommGroup V] →
      [inst_1 : InnerProductSpace ℝ V] →
        [inst_2 : MetricSpace P] →
          [inst_3 : NormedAddTorsor V P] → EuclideanGeometry.Sphere P → AffineSubspace ℝ P → Prop
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Sigma.ι_map_assoc : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {f g : β → C}
  [inst_1 : CategoryTheory.Limits.HasCoproduct f] [inst_2 : CategoryTheory.Limits.HasCoproduct g]
  (p : (b : β) → f b ⟶ g b) (b : β) {Z : C} (h : ∐ g ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι f b)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.map p) h) =
    CategoryTheory.CategoryStruct.comp (p b) (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι g b) h)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
CategoryTheory.Limits.cospanExt_inv_app_left : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y Z X' Y' Z' : C} (iX : X ≅ X') (iY : Y ≅ Y') (iZ : Z ≅ Z')
  {f : X ⟶ Z} {g : Y ⟶ Z} {f' : X' ⟶ Z'} {g' : Y' ⟶ Z'}
  (wf : CategoryTheory.CategoryStruct.comp iX.hom f' = CategoryTheory.CategoryStruct.comp f iZ.hom)
  (wg : CategoryTheory.CategoryStruct.comp iY.hom g' = CategoryTheory.CategoryStruct.comp g iZ.hom),
  (CategoryTheory.Limits.cospanExt iX iY iZ wf wg).inv.app CategoryTheory.Limits.WalkingCospan.left = iX.inv
-- Mathlib.Data.Int.Lemmas
Int.natAbs_inj_of_nonneg_of_nonneg : ∀ {a b : ℤ}, 0 ≤ a → 0 ≤ b → (a.natAbs = b.natAbs ↔ a = b)
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
cbiInf_eq_ciInf_subtype : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α},
  BddBelow (Set.range fun i => f ↑i ⋯) → ⨅ i, f ↑i ⋯ ≤ sInf ∅ → ⨅ i, ⨅ (h : p i), f i h = ⨅ x, f ↑x ⋯
-- Init.Data.List.Attach
List.getLast?_pmap : ∀ {α : Type u_1} {β : Type u_2} {P : α → Prop} {f : (a : α) → P a → β} {xs : List α} (H : ∀ a ∈ xs, P a),
  (List.pmap f xs H).getLast? =
    Option.map
      (fun x =>
        match x with
        | ⟨a, m⟩ => f a ⋯)
      xs.attach.getLast?