mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
/-- Constructor for morphisms to `mappingCocone`.  -/
CochainComplex.mappingCocone.lift : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      {K L : CochainComplex C ℤ} →
        (φ : K ⟶ L) →
          [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] →
            {M : CochainComplex C ℤ} →
              (α : M ⟶ K) →
                (β : CochainComplex.HomComplex.Cochain M L (-1)) →
                  CochainComplex.HomComplex.δ (-1) 0 β +
                        CochainComplex.HomComplex.Cochain.ofHom (CategoryTheory.CategoryStruct.comp α φ) =
                      0 →
                    (M ⟶ CochainComplex.mappingCocone φ)
-- Mathlib.Algebra.Group.Pointwise.Finset.Scalar
Finset.Nonempty.smul : ∀ {α : Type u_2} {β : Type u_3} [inst : DecidableEq β] [inst_1 : SMul α β] {s : Finset α} {t : Finset β},
  s.Nonempty → t.Nonempty → (s • t).Nonempty
-- Mathlib.Topology.Homotopy.Path
Path.Homotopy.cast_apply : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} {p₀ p₁ q₀ q₁ : Path x₀ x₁} (F : p₀.Homotopy p₁) (h₀ : p₀ = q₀)
  (h₁ : p₁ = q₁) (a : ↑unitInterval × ↑unitInterval), (F.cast h₀ h₁) a = F a
-- Mathlib.Order.SuccPred.Basic
WithBot.pred_coe_of_not_isMin : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [inst_2 : (a : α) → Decidable (Order.pred a = a)]
  {a : α}, ¬IsMin a → Order.pred ↑a = ↑(Order.pred a)
-- Mathlib.AlgebraicTopology.SimplicialSet.HornColimits
/-- Let `i : Fin (n + 2)`. This is the condition that a family of morphisms
`Δ[n] ⟶ X` for `j ≠ i` are the "faces" of a morphism  `Λ[n + 1, i] ⟶ X`.  -/
SSet.horn.IsCompatible : {n : ℕ} → {X : SSet} → {i : Fin (n + 2)} → ((j : Fin (n + 2)) → j ≠ i → (SSet.stdSimplex.obj { len := n } ⟶ X)) → Prop
-- Mathlib.Data.Fin.Tuple.Basic
/-- Repeat `a` `m` times. For example `Fin.repeat 2 ![0, 3, 7] = ![0, 3, 7, 0, 3, 7]`.  -/
Fin.repeat : {n : ℕ} → {α : Sort u_1} → (m : ℕ) → (Fin n → α) → Fin (m * n) → α
-- Mathlib.CategoryTheory.Filtered.Grothendieck
CategoryTheory.instIsFilteredGrothendieckOfαCategoryObjCat : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (F : CategoryTheory.Functor C CategoryTheory.Cat)
  [CategoryTheory.IsFiltered C] [∀ (c : C), CategoryTheory.IsFiltered ↑(F.obj c)],
  CategoryTheory.IsFiltered (CategoryTheory.Grothendieck F)
-- Mathlib.MeasureTheory.Integral.TorusIntegral
/-- The integral over a generalized torus with center `c ∈ ℂⁿ` and radius `R ∈ ℝⁿ`, defined
as the `•`-product of the derivative of `torusMap` and `f (torusMap c R θ)`  -/
torusIntegral : {n : ℕ} →
  {E : Type u_1} → [inst : NormedAddCommGroup E] → [NormedSpace ℂ E] → ((Fin n → ℂ) → E) → (Fin n → ℂ) → (Fin n → ℝ) → E
-- Std.Time.DateTime
/-- Returns the aligned week of the month for a `DateTime`. Weeks are fixed 7-day slots
starting from day 1: days 1–7 are week 1, days 8–14 are week 2, etc.
 -/
Std.Time.DateTime.alignedWeekOfMonth : Std.Time.DateTime → Std.Time.Week.Aligned.Ordinal
-- Mathlib.RingTheory.Localization.AtPrime.Basic
IsLocalization.AtPrime.under_maximalIdeal_pow : ∀ {R : Type u_1} [inst : CommSemiring R] (p : Ideal R) [inst_1 : p.IsPrime] (Rₚ : Type u_4) [inst_2 : CommSemiring Rₚ]
  [inst_3 : Algebra R Rₚ] [IsLocalization.AtPrime Rₚ p] [inst_5 : IsLocalRing Rₚ] [p.IsMaximal] (n : ℕ),
  Ideal.under R (IsLocalRing.maximalIdeal Rₚ ^ n) = p ^ n
-- Mathlib.Order.LiminfLimsup
/-- See also `Filter.bliminf_or_eq_inf`.  -/
Filter.bliminf_or_le_inf : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : Filter β} {p q : β → Prop} {u : β → α},
  (Filter.bliminf u f fun x => p x ∨ q x) ≤ Filter.bliminf u f p ⊓ Filter.bliminf u f q
-- Mathlib.Algebra.Algebra.Operations
/-- Multiplication of sub-R-modules of an R-module A that is also a semiring. The submodule `M * N`
consists of finite sums of elements `m * n` for `m ∈ M` and `n ∈ N`.  -/
Submodule.mul : {R : Type u} →
  [inst : Semiring R] →
    {A : Type v} → [inst_1 : Semiring A] → [inst_2 : Module R A] → [IsScalarTower R A A] → Mul (Submodule R A)
-- Mathlib.Data.List.Sort
/-- **Alias** of the reverse direction of `List.sortedGT_iff_isChain`. -/
List.IsChain.sortedGT : ∀ {α : Type u_1} {l : List α} [inst : Preorder α], List.IsChain (fun x1 x2 => x1 > x2) l → l.SortedGT
-- Mathlib.Analysis.SpecialFunctions.Log.ENNRealLog
ENNReal.log_of_nnreal : ∀ {x : NNReal}, x ≠ 0 → (↑x).log = ↑(Real.log ↑x)
-- Mathlib.Algebra.Order.Module.PositiveLinearMap
/-- Notation for a `PositiveLinearMap`.  -/
«term_→ₚ[_]_» : Lean.TrailingParserDescr
-- Mathlib.LinearAlgebra.AffineSpace.Simplex.Basic
/-- A face of a simplex is a simplex with the given subset of
points.  -/
Affine.Simplex.face : {k : Type u_1} →
  {V : Type u_2} →
    {P : Type u_5} →
      [inst : Ring k] →
        [inst_1 : AddCommGroup V] →
          [inst_2 : Module k V] →
            [inst_3 : AddTorsor V P] →
              {n : ℕ} →
                Affine.Simplex k P n → {fs : Finset (Fin (n + 1))} → {m : ℕ} → fs.card = m + 1 → Affine.Simplex k P m
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Two maps to the domain of `f`  -/
CategoryTheory.RegularEpi.left : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {X Y : C} → {f : X ⟶ Y} → (self : CategoryTheory.RegularEpi f) → self.W ⟶ X
-- Init.Data.List.Scan.Lemmas
List.scanl_cons : ∀ {β : Type u_1} {α : Type u_2} {b : β} {a : α} {l : List α} {f : β → α → β},
  List.scanl f b (a :: l) = b :: List.scanl f (f b a) l
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.constantsOn_constants : ∀ {α : Type u'}, (FirstOrder.Language.constantsOn α).Constants = α
-- Mathlib.Analysis.Normed.Module.Convex
/-- Emetric diameter of the convex hull of a set `s` equals the emetric diameter of `s`.  -/
convexHull_ediam : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (s : Set E),
  Metric.ediam ((convexHull ℝ) s) = Metric.ediam s
-- Mathlib.Algebra.MvPolynomial.Expand
MvPolynomial.of_irreducible_expand : ∀ {R : Type u_1} (σ : Type u_2) [inst : CommRing R] {p : ℕ},
  p ≠ 0 → ∀ {f : MvPolynomial σ R}, Irreducible ((MvPolynomial.expand p) f) → Irreducible f
-- Mathlib.Geometry.RingedSpace.OpenImmersion
/-- An open immersion `f : X ⟶ Y` induces an isomorphism `X ≅ Y|_{f(X)}`.  -/
AlgebraicGeometry.SheafedSpace.IsOpenImmersion.isoRestrict : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X Y : AlgebraicGeometry.SheafedSpace C} →
      (f : X ⟶ Y) → [H : AlgebraicGeometry.SheafedSpace.IsOpenImmersion f] → X ≅ Y.restrict ⋯
-- Init.Data.String.Basic
String.Slice.Pos.str_lt_endExclusive : ∀ {s : String.Slice} (p : s.Pos), p ≠ s.endPos → p.str < s.endExclusive
-- Lean.Meta.Tactic.Grind.EMatchTheorem
_private.Lean.Meta.Tactic.Grind.EMatchTheorem.0.Lean.Meta.Grind.collectGroundPattern?.visit? : Lean.Expr → Lean.Meta.Grind.CollectorM✝ (Option Lean.Expr)
-- Mathlib.Logic.Embedding.Set
Function.Embedding.optionElim_apply : ∀ {α : Type u_1} {β : Type u_2} (f : α ↪ β) (x : β) (h : x ∉ Set.range ⇑f) (a : Option α),
  (f.optionElim x h) a = Option.elim' x (⇑f) a
-- Mathlib.Topology.PartitionOfUnity
/-- the functions are non-negative  -/
BumpCovering.nonneg' : ∀ {ι : Type u_1} {X : Type u_2} [inst : TopologicalSpace X] {s : optParam (Set X) Set.univ} (self : BumpCovering ι X s),
  0 ≤ self.toFun
-- Lean.Meta.Tactic.Simp.SimpCongrTheorems
Lean.Meta.congrExtension : Lean.SimpleScopedEnvExtension Lean.Meta.SimpCongrTheorem Lean.Meta.SimpCongrTheorems
-- Init.Omega.Coeffs
Lean.Omega.Coeffs.gcd_dvd_dot_left : ∀ (xs ys : Lean.Omega.Coeffs), ↑xs.gcd ∣ xs.dot ys
-- Std.Internal.Do.Triple.SpecLemmas
Std.Internal.Do.Spec.monadMap_trans : ∀ {m : Type u → Type v} {Pred EPred : Type u} [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}
  {post : α → Pred} {epost : EPred} {n₁ n₂ : Type u → Type v} [inst_4 : MonadFunctor n₁ m]
  [inst_5 : MonadFunctorT n₂ n₁] {f : {β : Type u} → n₂ β → n₂ β} (x : m α),
  ⦃ Std.Internal.Do.wp (MonadFunctor.monadMap (fun {β} => monadMap fun {β} => f) x) post epost ⦄
    monadMap (fun {β} => f) x ⦃ post; epost ⦄
-- Mathlib.Data.Nat.Cast.Prod
Prod.snd_natCast : ∀ {α : Type u_1} {β : Type u_2} [inst : AddMonoidWithOne α] [inst_1 : AddMonoidWithOne β] (n : ℕ), (↑n).2 = ↑n
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} [inst_3 : Inhabited (β a)], m.isEmpty = true → m.get! a = default
-- Lean.Compiler.IR.Basic
Lean.IR.IRType.isPossibleRef : Lean.IR.IRType → Bool
-- Mathlib.Data.Seq.Computation
Computation.liftRel_bind : ∀ {α : Type u} {β : Type v} {γ : Type w} {δ : Type u_1} (R : α → β → Prop) (S : γ → δ → Prop) {s1 : Computation α}
  {s2 : Computation β} {f1 : α → Computation γ} {f2 : β → Computation δ},
  Computation.LiftRel R s1 s2 →
    (∀ {a : α} {b : β}, R a b → Computation.LiftRel S (f1 a) (f2 b)) → Computation.LiftRel S (s1.bind f1) (s2.bind f2)
-- Mathlib.Order.Filter.Extr
IsMinFilter.filter_inf : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β} {l : Filter α} {a : α},
  IsMinFilter f l a → ∀ (l' : Filter α), IsMinFilter f (l ⊓ l') a
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientAddSubgroupOfMapOfLE_apply_mk : ∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (H : AddSubgroup α) (h : s ≤ t) (g : ↥H),
  AddSubgroup.quotientAddSubgroupOfMapOfLE H h ↑g = ↑g
-- Mathlib.CategoryTheory.Sites.Point.Basic
/-- If `Φ` is a point of a site and `F : A ⥤ B` is a functor which preserves
filtered colimits, then taking fibers of presheaves at `Φ` commutes with `F`.  -/
CategoryTheory.GrothendieckTopology.Point.presheafFiberCompIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      (Φ : J.Point) →
        {A : Type u'} →
          [inst_1 : CategoryTheory.Category.{v', u'} A] →
            {B : Type u''} →
              [inst_2 : CategoryTheory.Category.{v'', u''} B] →
                [inst_3 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v', u'} A] →
                  [inst_4 : CategoryTheory.Limits.HasColimitsOfSize.{w, w, v'', u''} B] →
                    (F : CategoryTheory.Functor A B) →
                      [CategoryTheory.LocallySmall.{w, v, u} C] →
                        [CategoryTheory.Limits.PreservesFilteredColimitsOfSize.{w, w, v', v'', u', u''} F] →
                          ((CategoryTheory.Functor.whiskeringRight Cᵒᵖ A B).obj F).comp Φ.presheafFiber ≅
                            Φ.presheafFiber.comp F
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Basic
WeierstrassCurve.Projective.not_equiv_of_Y_ne : ∀ {R : Type r} [inst : CommRing R] {P Q : Fin 3 → R}, P 1 * Q 2 ≠ Q 1 * P 2 → ¬P ≈ Q
-- Mathlib.RingTheory.Smooth.Basic
Algebra.FormallySmooth.of_isLocalization : ∀ {R : Type u_4} {Rₘ : Type u_6} [inst : CommRing R] [inst_1 : CommRing Rₘ] (M : Submonoid R) [inst_2 : Algebra R Rₘ]
  [IsLocalization M Rₘ], Algebra.FormallySmooth R Rₘ
-- Init.Data.Int.Order
Int.le_add_iff_sub_le : ∀ {a b c : ℤ}, a ≤ b + c ↔ a - c ≤ b
-- Mathlib.Order.FixedPoints
OrderHom.map_inf_fixedPoints_le : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) (x y : ↑(Function.fixedPoints ⇑f)), f (↑x ⊓ ↑y) ≤ ↑x ⊓ ↑y
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.LocalTimeType.mk.injEq : ∀ (gmtOffset : Std.Time.TimeZone.Offset) (isDst : Bool) (abbreviation : String) (wall : Std.Time.TimeZone.StdWall)
  (utLocal : Std.Time.TimeZone.UTLocal) (identifier : String) (gmtOffset_1 : Std.Time.TimeZone.Offset) (isDst_1 : Bool)
  (abbreviation_1 : String) (wall_1 : Std.Time.TimeZone.StdWall) (utLocal_1 : Std.Time.TimeZone.UTLocal)
  (identifier_1 : String),
  ({ gmtOffset := gmtOffset, isDst := isDst, abbreviation := abbreviation, wall := wall, utLocal := utLocal,
        identifier := identifier } =
      { gmtOffset := gmtOffset_1, isDst := isDst_1, abbreviation := abbreviation_1, wall := wall_1,
        utLocal := utLocal_1, identifier := identifier_1 }) =
    (gmtOffset = gmtOffset_1 ∧
      isDst = isDst_1 ∧ abbreviation = abbreviation_1 ∧ wall = wall_1 ∧ utLocal = utLocal_1 ∧ identifier = identifier_1)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Equiv.rfl : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β}, m.Equiv m
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.flipFunctor_map_τ₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : CategoryTheory.Square C} (φ : X ⟶ Y),
  (CategoryTheory.Square.flipFunctor.map φ).τ₁ = φ.τ₁
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Const.insertMany_append : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap α (fun x => β) cmp} {l₁ l₂ : List (α × β)},
  Std.DTreeMap.Const.insertMany t (l₁ ++ l₂) = Std.DTreeMap.Const.insertMany (Std.DTreeMap.Const.insertMany t l₁) l₂
-- Mathlib.CategoryTheory.GradedObject.Trifunctor
CategoryTheory.GradedObject.mapBifunctorBifunctor₂₃MapObj_ext : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {C₃ : Type u_3} {C₄ : Type u_4} {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_3} C₃] [inst_3 : CategoryTheory.Category.{v_4, u_4} C₄]
  [inst_4 : CategoryTheory.Category.{v_6, u_6} C₂₃] {F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂₃ C₄)}
  {G₂₃ : CategoryTheory.Functor C₂ (CategoryTheory.Functor C₃ C₂₃)} {I₁ : Type u_7} {I₂ : Type u_8} {I₃ : Type u_9}
  {J : Type u_10} {r : I₁ × I₂ × I₃ → J} {ρ₂₃ : CategoryTheory.GradedObject.BifunctorComp₂₃IndexData r}
  {X₁ : CategoryTheory.GradedObject I₁ C₁} {X₂ : CategoryTheory.GradedObject I₂ C₂}
  {X₃ : CategoryTheory.GradedObject I₃ C₃}
  [inst_5 : (((CategoryTheory.GradedObject.mapBifunctor G₂₃ I₂ I₃).obj X₂).obj X₃).HasMap ρ₂₃.p]
  [inst_6 :
    (((CategoryTheory.GradedObject.mapBifunctor F I₁ ρ₂₃.I₂₃).obj X₁).obj
          (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃)).HasMap
      ρ₂₃.q]
  [H : CategoryTheory.GradedObject.HasGoodTrifunctor₂₃Obj F G₂₃ ρ₂₃ X₁ X₂ X₃] {j : J} {A : C₄}
  {f g :
    CategoryTheory.GradedObject.mapBifunctorMapObj F ρ₂₃.q X₁
        (CategoryTheory.GradedObject.mapBifunctorMapObj G₂₃ ρ₂₃.p X₂ X₃) j ⟶
      A},
  (∀ (i₁ : I₁) (i₂ : I₂) (i₃ : I₃) (h : r (i₁, i₂, i₃) = j),
      CategoryTheory.CategoryStruct.comp
          (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) f =
        CategoryTheory.CategoryStruct.comp
          (CategoryTheory.GradedObject.ιMapBifunctorBifunctor₂₃MapObj F G₂₃ ρ₂₃ X₁ X₂ X₃ i₁ i₂ i₃ j h) g) →
    f = g
-- Mathlib.Data.Finset.Sups
Finset.compls_nonempty : ∀ {α : Type u_2} [inst : BooleanAlgebra α] {s : Finset α}, s.compls.Nonempty ↔ s.Nonempty
-- Mathlib.Topology.UniformSpace.Basic
Uniform.continuous_iff'_left : ∀ {α : Type ua} {β : Type ub} [inst : UniformSpace α] [inst_1 : TopologicalSpace β] {f : β → α},
  Continuous f ↔ ∀ (b : β), Filter.Tendsto (fun x => (f x, f b)) (nhds b) (uniformity α)
-- Mathlib.Topology.CWComplex.Classical.Basic
/-- **Alias** of `Topology.RelCWComplex.cellFrontier_zero_eq_empty`. -/
Topology.CWComplex.cellFrontier_zero_eq_empty : ∀ {X : Type u_1} [t : TopologicalSpace X] {C D : Set X} [inst : Topology.RelCWComplex C D]
  {j : Topology.RelCWComplex.cell C 0}, Topology.RelCWComplex.cellFrontier 0 j = ∅
-- Lean.Meta.CongrTheorems
Lean.Meta.instReprCongrArgKind.repr : Lean.Meta.CongrArgKind → ℕ → Std.Format
-- Mathlib.Order.Interval.Finset.Defs
Fintype.card_Iio : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : LocallyFiniteOrderBot α] (a : α) [inst_2 : Fintype ↑(Set.Iio a)],
  Fintype.card ↑(Set.Iio a) = (Finset.Iio a).card
-- Mathlib.Analysis.Calculus.Rademacher
/-- In a real finite-dimensional normed vector space,
the norm is almost everywhere differentiable.  -/
ae_differentiableAt_norm : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : MeasurableSpace E] [BorelSpace E]
  {μ : MeasureTheory.Measure E} [FiniteDimensional ℝ E] [μ.IsAddHaarMeasure],
  ∀ᵐ (x : E) ∂μ, DifferentiableAt ℝ (fun x => ‖x‖) x
-- Mathlib.Order.Filter.Pointwise
Filter.inv_le_iff_le_inv : ∀ {α : Type u_2} [inst : InvolutiveInv α] {f g : Filter α}, f⁻¹ ≤ g ↔ f ≤ g⁻¹
-- Init.Data.String.Basic
String.utf8ByteSize_sliceTo : ∀ {s : String} {p : s.Pos}, (s.sliceTo p).utf8ByteSize = p.offset.byteIdx
-- Mathlib.AlgebraicTopology.SimplicialSet.Simplices
SSet.S.mk : {X : SSet} → {dim : ℕ} → X.obj (Opposite.op { len := dim }) → X.S
-- Mathlib.Algebra.Order.Module.Defs
/-- An ordered module is a module with a partial order such that scalar multiplication by a
nonnegative scalar and of a nonnegative vector are both monotone.  -/
IsOrderedModule : (α : Type u_1) → (β : Type u_2) → [SMul α β] → [Preorder α] → [Preorder β] → [Zero α] → [Zero β] → Prop
-- Mathlib.Analysis.BoxIntegral.Partition.Split
/-- Let `s : Finset (ι × ℝ)` be a set of hyperplanes `{x : ι → ℝ | x i = r}` in `ι → ℝ` encoded as
pairs `(i, r)`. Suppose that this set contains all faces of a box `J`. The hyperplanes of `s` split
a box `I` into subboxes. Let `Js` be one of them. If `J` and `Js` have nonempty intersection, then
`Js` is a subbox of `J`.  -/
BoxIntegral.Prepartition.not_disjoint_imp_le_of_subset_of_mem_splitMany : ∀ {ι : Type u_1} {I J Js : BoxIntegral.Box ι} {s : Finset (ι × ℝ)},
  (∀ (i : ι), {(i, J.lower i), (i, J.upper i)} ⊆ s) →
    Js ∈ BoxIntegral.Prepartition.splitMany I s → ¬Disjoint ↑J ↑Js → Js ≤ J
-- Mathlib.Algebra.Quaternion
QuaternionAlgebra.imK_star : ∀ {R : Type u_3} {c₁ c₂ c₃ : R} (a : QuaternionAlgebra R c₁ c₂ c₃) [inst : CommRing R], (star a).imK = -a.imK
-- Mathlib.RingTheory.AdicCompletion.LocalRing
AdicCompletion.isAdicComplete_self : ∀ {R : Type u_1} [inst : CommRing R] (I : Ideal R),
  I.FG → IsAdicComplete (Ideal.map (algebraMap R (AdicCompletion I R)) I) (AdicCompletion I R)
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.mahlerMeasure_eq_zero_iff : ∀ (p : Polynomial ℂ), p.mahlerMeasure = 0 ↔ p = 0
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get?_erase_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {k : α}, (t.erase k).get? k = none
-- Mathlib.Algebra.Order.GroupWithZero.Action.Synonym
Lex.instSMulWithZero : {G₀ : Type u_1} →
  {M₀ : Type u_2} → [inst : Zero G₀] → [inst_1 : Zero M₀] → [SMulWithZero G₀ M₀] → SMulWithZero (Lex G₀) M₀
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Substructure
Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go.eq_4 : ∀ (aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit) (cache : Std.Tactic.BVDecide.BVExpr.Cache aig)
  (discr lhs rhs : Std.Tactic.BVDecide.BoolExpr Std.Tactic.BVDecide.BVPred),
  Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig (discr.ite lhs rhs) cache =
    match Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig discr cache with
    | { result := ⟨{ aig := aig_1, ref := discrRef }, dextend⟩, cache := cache } =>
      match Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig_1 lhs cache with
      | { result := ⟨{ aig := aig_2, ref := lhsRef }, lextend⟩, cache := cache } =>
        match Std.Tactic.BVDecide.BVLogicalExpr.bitblast.go aig_2 rhs cache with
        | { result := ⟨{ aig := aig_3, ref := rhsRef }, rextend⟩, cache := cache } =>
          let discrRef_1 := discrRef.cast ⋯;
          let lhsRef_1 := lhsRef.cast rextend;
          let input := { discr := discrRef_1, lhs := lhsRef_1, rhs := rhsRef };
          let ret := aig_3.mkIfCached input;
          have this := ⋯;
          have cache := cache.cast this;
          have this := ⋯;
          { result := ⟨ret, this⟩, cache := cache }
-- Mathlib.GroupTheory.GroupAction.DomAct.Basic
DomAddAct.instSemiringOfAddOpposite.eq_1 : ∀ {M : Type u_1} [inst : Semiring Mᵃᵒᵖ], DomAddAct.instSemiringOfAddOpposite = inst
-- Init.Data.Vector.Lemmas
Vector.singleton_eq_toVector_singleton : ∀ {α : Type u_1} {a : α}, #v[a] = #[a].toVector
-- Mathlib.Data.FunLike.Group
/-- A `FunLike` type that satisfies `(f * g) x = f x * g x` has right multiplication if
`β` has right multiplication.  -/
FunLike.isCancelMul : ∀ {F : Type u_1} {α : Type u_2} {β : Type u_3} [inst : FunLike F α β] [inst_1 : Mul F] [inst_2 : Mul β] [IsCancelMul β]
  [IsMulApply F α β], IsCancelMul F
-- Lean.Elab.Deriving.Util
Lean.Elab.Deriving.mkLet : Array (Lean.TSyntax `Lean.Parser.Term.letDecl) → Lean.Term → Lean.Elab.TermElabM Lean.Term
-- Mathlib.Order.SuccPred.Archimedean
lt_or_le_of_directed : ∀ {α : Type u_1} [inst : PartialOrder α] [inst_1 : PredOrder α] [IsPredArchimedean α] {r v₁ v₂ : α},
  v₂ ≤ r → v₁ ≤ r → v₂ < v₁ ∨ v₁ ≤ v₂
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.ΓSpecIso_inv_naturality_assoc : ∀ {R S : CommRingCat} (f : R ⟶ S) {Z : CommRingCat} (h : (AlgebraicGeometry.Spec S).presheaf.obj (Opposite.op ⊤) ⟶ Z),
  CategoryTheory.CategoryStruct.comp f
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso S).inv h) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.ΓSpecIso R).inv
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Hom.appTop (AlgebraicGeometry.Spec.map f)) h)
-- Init.Data.Vector.Lemmas
Vector.toList_range : ∀ {n : ℕ}, (Vector.range n).toList = List.range n
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.Hom.mk.injEq : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  {D₁ D₂ : F.DescentData' sq sq₃} (hom : (i : ι) → D₁.obj i ⟶ D₂.obj i)
  (comm :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (hom i₁)) (D₂.hom i₁ i₂) =
          CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (hom i₂)))
      CategoryTheory.Pseudofunctor.DescentData'.Hom.comm._autoParam)
  (hom_1 : (i : ι) → D₁.obj i ⟶ D₂.obj i)
  (comm_1 :
    autoParam
      (∀ (i₁ i₂ : ι),
        CategoryTheory.CategoryStruct.comp ((F.map (sq i₁ i₂).p₁.op.toLoc).toFunctor.map (hom_1 i₁)) (D₂.hom i₁ i₂) =
          CategoryTheory.CategoryStruct.comp (D₁.hom i₁ i₂) ((F.map (sq i₁ i₂).p₂.op.toLoc).toFunctor.map (hom_1 i₂)))
      CategoryTheory.Pseudofunctor.DescentData'.Hom.comm._autoParam),
  ({ hom := hom, comm := comm } = { hom := hom_1, comm := comm_1 }) = (hom = hom_1)
-- Mathlib.Data.Vector.Defs
/-- `map` is natural with respect to `cons`.  -/
List.Vector.map_cons : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (a : α) (v : List.Vector α n),
  List.Vector.map f (a ::ᵥ v) = f a ::ᵥ List.Vector.map f v