mathlib-initiative/mathlib-types huggingface dataset:
-- Lean.Meta.Sym.DSimp.DSimpM
/-- Simplifier configuration options.  -/
Lean.Meta.Sym.DSimp.Context.config : Lean.Meta.Sym.DSimp.Context → Lean.Meta.Sym.DSimp.Config
-- Mathlib.NumberTheory.LSeries.PrimesInAP
/-- **Dirichlet's Theorem** on primes in arithmetic progression: if `q` is a positive
integer and `a : ZMod q` is a unit, then there are infinitely many prime numbers `p`
such that `(p : ZMod q) = a`.  -/
Nat.forall_exists_prime_gt_and_eq_mod : ∀ {q : ℕ} [NeZero q] {a : ZMod q}, IsUnit a → ∀ (n : ℕ), ∃ p > n, Nat.Prime p ∧ ↑p = a
-- Mathlib.Data.Vector.Mem
List.Vector.mem_cons_iff : ∀ {α : Type u_1} {n : ℕ} (a a' : α) (v : List.Vector α n), a' ∈ (a ::ᵥ v).toList ↔ a' = a ∨ a' ∈ v.toList
-- Init.Data.Array.Sort.Lemmas
Subarray.mergeSort_toArray : ∀ {α : Type u_1} {xs : Subarray α} {le : α → α → Bool}, (Std.Slice.toArray xs).mergeSort le = xs.mergeSort le
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.mk : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat} →
      (base : 𝒮) → ↑(F.obj { as := base }) → F.Grothendieck
-- Mathlib.MeasureTheory.Measure.OpenPos
Metric.measure_ball_pos : ∀ {X : Type u_1} [inst : PseudoMetricSpace X] {m : MeasurableSpace X} (μ : MeasureTheory.Measure X) [μ.IsOpenPosMeasure]
  (x : X) {r : ℝ}, 0 < r → 0 < μ (Metric.ball x r)
-- Init.Data.BitVec.Lemmas
BitVec.getMsbD_of_ge : ∀ {w : ℕ} (x : BitVec w) (i : ℕ), w ≤ i → x.getMsbD i = false
-- Mathlib.LinearAlgebra.RootSystem.WeylGroup
/-- The natural representation of the Weyl group on the root space.  -/
RootPairing.weylGroupRootRep : {ι : 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] → (P : RootPairing ι R M N) → Representation R (↥P.weylGroup) M
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.X_pow_mul_monomial : ∀ {R : Type u} [inst : Semiring R] (k n : ℕ) (r : R),
  Polynomial.X ^ k * (Polynomial.monomial n) r = (Polynomial.monomial (n + k)) r
-- Mathlib.RingTheory.Localization.FractionRing
IsFractionRing.idem : ∀ (R : Type u_1) [inst : CommRing R] (K : Type u_5) [inst_1 : CommRing K] [inst_2 : Algebra R K] [IsFractionRing R K],
  IsFractionRing K K
-- Mathlib.NumberTheory.Dioph
Dioph.proj_dioph : ∀ {α : Type u} (i : α), Dioph.DiophFn fun v => v i
-- Mathlib.Topology.Sets.Compacts
TopologicalSpace.NonemptyCompacts.mem_toCompacts : ∀ {α : Type u_1} [inst : TopologicalSpace α] {x : α} {s : TopologicalSpace.NonemptyCompacts α}, x ∈ s.toCompacts ↔ x ∈ s
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.Nonempty.zero_mem_sub : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddGroup α] {s : Finset α}, s.Nonempty → 0 ∈ s - s
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.ne_zero_of_mem_rootSet : ∀ {S : Type v} {T : Type w} [inst : CommRing T] {p : Polynomial T} [inst_1 : CommRing S] [inst_2 : IsDomain S]
  [inst_3 : Algebra T S] {a : S}, a ∈ p.rootSet S → p ≠ 0
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Continuity
/-- `cfc` is continuous in the variable `a : A` when `s : Set ℝ≥0` is compact and `a` varies over
nonnegative elements whose spectrum is contained in `s`, and the function `f` is
continuous on `s`.  -/
Continuous.cfc_nnreal' : ∀ {X : Type u_1} {A : Type u_2} [inst : NormedRing A] [inst_1 : StarRing A] [inst_2 : NormedAlgebra ℝ A]
  [inst_3 : IsometricContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [ContinuousStar A] [inst_5 : PartialOrder A]
  [inst_6 : StarOrderedRing A] [inst_7 : NonnegSpectrumClass ℝ A] [T2Space A] [IsSemitopologicalRing A]
  [inst_10 : TopologicalSpace X] {s : Set NNReal},
  IsCompact s →
    ∀ (f : NNReal → NNReal) {a : X → A},
      Continuous a →
        (∀ (x : X), spectrum NNReal (a x) ⊆ s) →
          autoParam (ContinuousOn f s) Continuous.cfc_nnreal'._auto_1 →
            autoParam (∀ (x : X), 0 ≤ a x) Continuous.cfc_nnreal'._auto_3 → Continuous fun x => cfc f (a x)
-- Mathlib.LinearAlgebra.Transvection.Generation
/-- If an element `e : V ≃ₗ[K] V` is not exceptional,
then it is the product of at most `finrank K (V ⧸ e.fixedSubmodule)` dilatransvections.

This is the non-exceptional case in Dieudonné's theorem.  -/
LinearEquiv.mem_transvections_pow_mul_dilatransvections_of_not_isExceptional : ∀ {K : Type u_1} [inst : DivisionRing K] {V : Type u_2} [inst_1 : AddCommGroup V] [inst_2 : Module K V]
  [Module.Finite K V] {e : V ≃ₗ[K] V},
  ¬e.IsExceptional →
    e ∈
      LinearEquiv.transvections K V ^ (Module.finrank K (V ⧸ (↑e).fixedSubmodule) - 1) *
        LinearEquiv.dilatransvections K V
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.maxKey?_eq_minKey?_reverse : ∀ {α : Type u} {β : α → Type v} {l : Std.DTreeMap.Internal.Impl α β}, l.maxKey? = l.reverse.minKey?
-- Mathlib.RingTheory.Noetherian.Defs
/-- **Alias** of the forward direction of `isNoetherian_iff`. -/
IsNoetherian.wf : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M],
  IsNoetherian R M → WellFounded fun x1 x2 => x1 > x2
-- Mathlib.Data.Fin.Tuple.Embedding
Fin.Embedding.snoc_last : ∀ {α : Type u_1} {n : ℕ} {x : Fin n ↪ α} {a : α} {ha : a ∉ Set.range ⇑x}, (Fin.Embedding.snoc x ha) (Fin.last n) = a
-- Mathlib.Algebra.Group.Equiv.Basic
Equiv.neg_symm : ∀ {G : Type u_14} [inst : InvolutiveNeg G], Equiv.symm (Equiv.neg G) = Equiv.neg G
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.newton_seq_dist_tendsto : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]}
  (hnorm : ‖(Polynomial.aeval a) F‖ < ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2),
  (Polynomial.aeval a) F ≠ 0 →
    Filter.Tendsto (fun n => ‖↑(newton_cau_seq✝ hnorm) n - a‖) Filter.atTop
      (nhds (‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖))
-- Mathlib.Data.Part
Part.instMonad : Monad Part
-- Mathlib.Combinatorics.SimpleGraph.Walk.Chord
SimpleGraph.Walk.isChordless_iff_forall_mem_edges : ∀ {V : Type u_1} {G : SimpleGraph V} {u v : V} {p : G.Walk u v},
  p.IsChordless ↔ ∀ ⦃u' v' : V⦄, u' ∈ p.support → v' ∈ p.support → G.Adj u' v' → s(u', v') ∈ p.edges
-- Mathlib.CategoryTheory.Limits.Preserves.Opposites
/-- If `F.leftOp : Cᵒᵖ ⥤ D` reflects limits, then `F : C ⥤ Dᵒᵖ` reflects colimits.  -/
CategoryTheory.Limits.reflectsColimits_of_leftOp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C Dᵒᵖ) [CategoryTheory.Limits.ReflectsLimits F.leftOp],
  CategoryTheory.Limits.ReflectsColimits F
-- Lean.Syntax
/-- Split an `ident` into its dot-separated components while preserving source info.
Macro scopes are first erased.  For example, `` `foo.bla.boo._@._hyg.4 `` ↦ `` [`foo, `bla, `boo] ``.
If `nFields` is set, we take that many fields from the end and keep the remaining components
as one name. For example, `` `foo.bla.boo `` with `(nFields := 1)` ↦ `` [`foo.bla, `boo] ``.  -/
Lean.Syntax.identComponents : Lean.Syntax → optParam (Option ℕ) none → List Lean.Syntax
-- Mathlib.NumberTheory.Harmonic.EulerMascheroni
Real.tendsto_eulerMascheroniSeq : Filter.Tendsto Real.eulerMascheroniSeq Filter.atTop (nhds Real.eulerMascheroniConstant)
-- Mathlib.CategoryTheory.Bicategory.Yoneda
/-- Right unitor as a 2-isomorphism in `Cat`.  -/
CategoryTheory.Bicategory.rightUnitorNatIsoCat : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    (a b : B) →
      (CategoryTheory.Bicategory.postcomposingCat a b b).obj (CategoryTheory.CategoryStruct.id b) ≅
        CategoryTheory.CategoryStruct.id (CategoryTheory.Cat.of (a ⟶ b))
-- Mathlib.CategoryTheory.Functor.Basic
CategoryTheory.Functor.comp_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (F : CategoryTheory.Functor C D), F.comp (CategoryTheory.Functor.id D) = F
-- Mathlib.AlgebraicTopology.ModelCategory.Cylinder
HomotopicalAlgebra.Cylinder.symm_π : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : C}
  [inst_1 : HomotopicalAlgebra.CategoryWithWeakEquivalences C] (P : HomotopicalAlgebra.Cylinder A), P.symm.π = P.π
-- Mathlib.Tactic.Widget.Calc
instSelectInsertParamsClassCalcParams : SelectInsertParamsClass CalcParams
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousAddMonoidHom.mk.injEq : ∀ {A : Type u_7} {B : Type u_8} [inst : AddMonoid A] [inst_1 : AddMonoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] (toAddMonoidHom : A →+ B)
  (continuous_toFun : autoParam (Continuous (↑toAddMonoidHom).toFun) ContinuousMap.continuous_toFun._autoParam)
  (toAddMonoidHom_1 : A →+ B)
  (continuous_toFun_1 : autoParam (Continuous (↑toAddMonoidHom_1).toFun) ContinuousMap.continuous_toFun._autoParam),
  ({ toAddMonoidHom := toAddMonoidHom, continuous_toFun := continuous_toFun } =
      { toAddMonoidHom := toAddMonoidHom_1, continuous_toFun := continuous_toFun_1 }) =
    (toAddMonoidHom = toAddMonoidHom_1)
-- Mathlib.ModelTheory.DirectLimit
FirstOrder.Language.DirectLimit.rangeLiftInclusion : ∀ {L : FirstOrder.Language} {ι : Type v} [inst : Preorder ι] [inst_1 : Nonempty ι] [inst_2 : IsDirectedOrder ι]
  {M : Type u_1} [inst_3 : L.Structure M] (S : ι →o L.Substructure M),
  (FirstOrder.Language.DirectLimit.liftInclusion S).toHom.range = ⨆ i, S i
-- Mathlib.Algebra.DirectSum.Ring
/-- The piecewise multiplication from the `Mul` instance, as a bundled homomorphism.  -/
DirectSum.gMulHom : {ι : Type u_1} →
  (A : ι → Type u_2) →
    [inst : Add ι] →
      [inst_1 : (i : ι) → AddCommMonoid (A i)] →
        [DirectSum.GNonUnitalNonAssocSemiring A] → {i j : ι} → A i →+ A j →+ A (i + j)
-- Mathlib.SetTheory.Ordinal.Arithmetic
Cardinal.isSuccLimit_ord : ∀ {c : Cardinal.{u_1}}, Cardinal.aleph0 ≤ c → Order.IsSuccLimit c.ord
-- Lean.Meta.Tactic.Grind.Intro
/-- Returns `true` if `type` is an inductive type with at most one constructor.  -/
_private.Lean.Meta.Tactic.Grind.Intro.0.Lean.Meta.Grind.isCheapInductive : Lean.Expr → Lean.CoreM Bool
-- Std.Data.TreeMap.Basic
/-- Checks whether a key is present in a map and unconditionally inserts a value for the key.

Equivalent to (but potentially faster than) calling `contains` followed by `insert`.
 -/
Std.TreeMap.containsThenInsert : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap α β cmp → α → β → Bool × Std.TreeMap α β cmp
-- Mathlib.Tactic.FieldSimp
/-- The main algorithm behind the `field_simp` tactic: partially-normalizing an
expression in a field `M` into the form x1 ^ c1 * x2 ^ c2 * ... x_k ^ c_k,
where x1, x2, ... are distinct atoms in `M`, and c1, c2, ... are integers.  -/
Mathlib.Tactic.FieldSimp.normalize : {v : Lean.Level} →
  {M : Q(Type v)} →
    ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) →
      (iM : Q(CommGroupWithZero «$M»)) →
        (x : Q(«$M»)) →
          Mathlib.Tactic.AtomM
            ((y : Q(«$M»)) ×
              ((g : Mathlib.Tactic.FieldSimp.Sign M) ×
                  have a := g.expr y;
                  Q(«$x» = «$a»)) ×
                (l : Mathlib.Tactic.FieldSimp.qNF M) ×
                  have a := l.toNF;
                  Q(«$y» = «$a».eval))
-- Mathlib.Algebra.MvPolynomial.Variables
MvPolynomial.aeval_ite_mem_eq_self : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] (q : MvPolynomial σ R) {s : Set σ},
  ↑q.vars ⊆ s →
    ∀ [inst_1 : (i : σ) → Decidable (i ∈ s)], (MvPolynomial.aeval fun i => if i ∈ s then MvPolynomial.X i else 0) q = q
-- Lean.Meta.Tactic.Grind.Types
_private.Lean.Meta.Tactic.Grind.Types.0.Lean.Meta.Grind.Solvers.propagateDiseqs.go.match_1.eq_2 : ∀ (motive : Lean.Meta.Grind.SolverTerms → Lean.Meta.Grind.SolverTerms → Sort u_1) (x : Lean.Meta.Grind.SolverTerms)
  (h_1 : (x : Lean.Meta.Grind.SolverTerms) → motive Lean.Meta.Grind.SolverTerms.nil x)
  (h_2 : (x : Lean.Meta.Grind.SolverTerms) → motive x Lean.Meta.Grind.SolverTerms.nil)
  (h_3 :
    (id₁ : ℕ) →
      (lhs : Lean.Expr) →
        (lhsTerms : Lean.Meta.Grind.SolverTerms) →
          (id₂ : ℕ) →
            (rhs : Lean.Expr) →
              (rhsTerms : Lean.Meta.Grind.SolverTerms) →
                motive (Lean.Meta.Grind.SolverTerms.next id₁ lhs lhsTerms)
                  (Lean.Meta.Grind.SolverTerms.next id₂ rhs rhsTerms)),
  (x = Lean.Meta.Grind.SolverTerms.nil → False) →
    (match x, Lean.Meta.Grind.SolverTerms.nil with
      | Lean.Meta.Grind.SolverTerms.nil, x => h_1 x
      | x, Lean.Meta.Grind.SolverTerms.nil => h_2 x
      | Lean.Meta.Grind.SolverTerms.next id₁ lhs lhsTerms, Lean.Meta.Grind.SolverTerms.next id₂ rhs rhsTerms =>
        h_3 id₁ lhs lhsTerms id₂ rhs rhsTerms) =
      h_2 x
-- Init.Data.Nat.Gcd
Nat.gcd_dvd_right : ∀ (m n : ℕ), m.gcd n ∣ n
-- Mathlib.LinearAlgebra.TensorProduct.Basic
TensorProduct.neg_tmul : ∀ {R : Type u_1} [inst : CommSemiring R] {M : Type u_2} {N : Type u_3} [inst_1 : AddCommGroup M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] (m : M) (n : N), (-m) ⊗ₜ[R] n = -m ⊗ₜ[R] n
-- Init.SimpLemmas
not_and_self : ∀ {a : Prop}, ¬(¬a ∧ a)
-- Mathlib.CategoryTheory.ObjectProperty.Basic
/-- The property of objects in a category that is satisfied by a single object `X : C`.  -/
CategoryTheory.ObjectProperty.singleton : {C : Type u} → [inst : CategoryTheory.CategoryStruct.{v, u} C] → C → CategoryTheory.ObjectProperty C
-- Mathlib.Algebra.Group.Action.Opposite
AddOpposite.unop_vadd_eq_unop_vadd_unop : ∀ {M : Type u_1} {α : Type u_3} [inst : VAdd M α] [inst_1 : VAdd Mᵃᵒᵖ α] [IsCentralVAdd M α] (r : Mᵃᵒᵖ) (a : αᵃᵒᵖ),
  AddOpposite.unop (r +ᵥ a) = AddOpposite.unop r +ᵥ AddOpposite.unop a
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iUnion_sub_right_image : ∀ {α : Type u_2} [inst : Sub α] {s t : Set α}, ⋃ a ∈ t, (fun x => x - a) '' s = s - t
-- Init.Data.Nat.Internal.Linear
Nat.Internal.Linear.Expr.brecOn.go : {motive : Nat.Internal.Linear.Expr → Sort u} →
  (t : Nat.Internal.Linear.Expr) →
    ((t : Nat.Internal.Linear.Expr) → Nat.Internal.Linear.Expr.below t → motive t) →
      motive t ×' Nat.Internal.Linear.Expr.below t
-- Mathlib.GroupTheory.GroupAction.Blocks
AddAction.IsBlock.translate : ∀ {G : Type u_1} [inst : AddGroup G] {X : Type u_2} [inst_1 : AddAction G X] {B : Set X} (g : G),
  AddAction.IsBlock G B → AddAction.IsBlock G (g +ᵥ B)
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientGroup.mulEquivPiModRangePowMonoidHom.eq_1 : ∀ {ι : Type u_1} (A : ι → Type u_2) [inst : (i : ι) → CommGroup (A i)] (n : ℕ),
  QuotientGroup.mulEquivPiModRangePowMonoidHom A n = QuotientGroup.liftEquiv (powMonoidHom n).range ⋯ ⋯
-- Init.Data.Slice.Array.Lemmas
Array.mkSlice_rcc_eq_mkSlice_rco_min : ∀ {α : Type u_1} {xs : Array α} {lo hi : ℕ},
  (Std.Rcc.Sliceable.mkSlice xs lo...=hi) =
    Std.Rco.Sliceable.mkSlice xs (min lo (min (hi + 1) xs.size))...min (hi + 1) xs.size
-- Init.Data.UInt.Bitwise
UInt8.or_self : ∀ {a : UInt8}, a ||| a = a
-- Mathlib.RingTheory.MvPowerSeries.Order
/-- The `weightedOrder` of the monomial `a*X^d` is infinite if `a = 0` and `weight w d` otherwise.
 -/
MvPowerSeries.weightedOrder_monomial : ∀ {σ : Type u_1} {R : Type u_2} [inst : Semiring R] (w : σ → ℕ) {d : σ →₀ ℕ} {a : R} [inst_1 : Decidable (a = 0)],
  MvPowerSeries.weightedOrder w ((MvPowerSeries.monomial d) a) = if a = 0 then ⊤ else ↑((Finsupp.weight w) d)
-- Mathlib.MeasureTheory.Measure.MeasureSpace
/-- If two sets `s` and `t` are included in a set `u`, and `μ s + μ t > μ u`,
then `s` intersects `t`. Version assuming that `t` is measurable.  -/
MeasureTheory.nonempty_inter_of_measure_lt_add : ∀ {α : Type u_1} {m : MeasurableSpace α} (μ : MeasureTheory.Measure α) {s t u : Set α},
  MeasurableSet t → s ⊆ u → t ⊆ u → μ u < μ s + μ t → (s ∩ t).Nonempty
-- Mathlib.Analysis.CStarAlgebra.Basic
CStarRing.norm_coe_unitary_mul : ∀ {E : Type u_2} [inst : NormedRing E] [inst_1 : StarRing E] [CStarRing E] (U : ↥(unitary E)) (A : E), ‖↑U * A‖ = ‖A‖
-- Mathlib.ModelTheory.Complexity
_private.Mathlib.ModelTheory.Complexity.0.FirstOrder.Language.BoundedFormula.toPrenexImpRight.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : (x : ℕ) → L.BoundedFormula α x → L.BoundedFormula α x → Sort u_4)
  (n : ℕ) (φ : L.BoundedFormula α n) (ψ : L.BoundedFormula α (n + 1))
  (h_1 :
    (n : ℕ) →
      (φ : L.BoundedFormula α n) →
        (ψ : L.BoundedFormula α (n + 1)) →
          motive n φ
            ((ψ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum))
  (h_2 : (n : ℕ) → (φ : L.BoundedFormula α n) → (ψ : L.BoundedFormula α (n + 1)) → motive n φ ψ.all)
  (h_3 : (_n : ℕ) → (φ ψ : L.BoundedFormula α _n) → motive _n φ ψ),
  (match n, φ, ψ.all with
    | n, φ, (ψ.imp FirstOrder.Language.BoundedFormula.falsum).all.imp FirstOrder.Language.BoundedFormula.falsum =>
      h_1 n φ ψ
    | n, φ, ψ.all => h_2 n φ ψ
    | _n, φ, ψ => h_3 _n φ ψ) =
    h_2 n φ ψ
-- Mathlib.Order.LiminfLimsup
Filter.bliminf_or_le_inf_aux_left : ∀ {α : 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
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.maxEntryD.match_1.eq_3 : ∀ {α : Type u_1} {β : Type u_2} (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3) (size : ℕ)
  (k : α) (v : β) (l : Std.DTreeMap.Internal.Impl α fun x => β) (size_1 : ℕ) (k_1 : α) (v_1 : β)
  (l_1 r : Std.DTreeMap.Internal.Impl α fun x => β) (fallback : α × β)
  (h_1 : (fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback)
  (h_2 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l : Std.DTreeMap.Internal.Impl α fun x => β) →
            (x : α × β) → motive (Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf) x)
  (h_3 :
    (size : ℕ) →
      (k : α) →
        (v : β) →
          (l r : Std.DTreeMap.Internal.Impl α fun x => β) →
            (size_2 : ℕ) →
              (k_2 : α) →
                (v_2 : β) →
                  (l_2 r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                    r = Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1 →
                      (fallback : α × β) →
                        motive
                          (Std.DTreeMap.Internal.Impl.inner size k v l
                            (Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1))
                          fallback),
  (match Std.DTreeMap.Internal.Impl.inner size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r),
      fallback with
    | Std.DTreeMap.Internal.Impl.leaf, fallback => h_1 fallback
    | Std.DTreeMap.Internal.Impl.inner size k v l Std.DTreeMap.Internal.Impl.leaf, x => h_2 size k v l x
    | Std.DTreeMap.Internal.Impl.inner size k v l r@h:(Std.DTreeMap.Internal.Impl.inner size_2 k_2 v_2 l_2 r_1),
      fallback => h_3 size k v l r size_2 k_2 v_2 l_2 r_1 h fallback) =
    h_3 size k v l (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l_1 r) size_1 k_1 v_1 l_1 r ⋯ fallback
-- Mathlib.Algebra.Order.Monoid.Unbundled.WithTop
WithBot.coe_eq_zero : ∀ {α : Type u} [inst : Zero α] {a : α}, ↑a = 0 ↔ a = 0
-- Init.Data.SInt.Lemmas
Int64.le_iff_toBitVec_sle : ∀ {a b : Int64}, a ≤ b ↔ a.toBitVec.sle b.toBitVec = true
-- Init.Data.Nat.Basic
Nat.succ_lt_succ_iff : ∀ {a b : ℕ}, a.succ < b.succ ↔ a < b
-- Mathlib.Topology.Category.TopPair
/-- Given `Homotopy f₀ f₁` and `Homotopy f₁ f₂`, we can define a `Homotopy f₀ f₂` by
`TopCat.Homotopy.trans` on the first and second components.
 -/
TopPair.Homotopy.trans : {X Y : TopPair} → {f₀ f₁ f₂ : X ⟶ Y} → TopPair.Homotopy f₀ f₁ → TopPair.Homotopy f₁ f₂ → TopPair.Homotopy f₀ f₂
-- Std.Time.Date.PlainDate
/-- Subtracts `Month.Offset` from a `PlainDate`, it clips the day to the last valid day of that month.
 -/
Std.Time.PlainDate.subMonthsClip : Std.Time.PlainDate → Std.Time.Month.Offset → Std.Time.PlainDate
-- Lean.Data.LBool
Lean.LBool : Type
-- Init.Data.UInt.Lemmas
UInt32.ne_iff_toBitVec_ne : ∀ {a b : UInt32}, a ≠ b ↔ a.toBitVec ≠ b.toBitVec
-- Mathlib.Analysis.Normed.Ring.Units
Units.nhds : ∀ {R : Type u_1} [inst : NormedRing R] [HasSummableGeomSeries R] (x : Rˣ), {x | IsUnit x} ∈ nhds ↑x
-- Mathlib.Analysis.Normed.Module.Multilinear.Basic
/-- Continuous multilinear maps themselves form a seminormed space with respect to
the operator norm.  -/
ContinuousMultilinearMap.seminormedAddCommGroup : {𝕜 : Type u} →
  {ι : Type v} →
    {E : ι → Type wE} →
      {G : Type wG} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : (i : ι) → SeminormedAddCommGroup (E i)] →
            [inst_2 : (i : ι) → NormedSpace 𝕜 (E i)] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 G] → [Fintype ι] → SeminormedAddCommGroup (ContinuousMultilinearMap 𝕜 E G)
-- Mathlib.Data.Set.Operations
/-- **Alias** of `Set.ofPred_mem_eq`. -/
Set.setOf_mem_eq : ∀ {α : Type u} {s : Set α}, {x | x ∈ s} = s
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.codeBlockExpandersFor : Lean.Ident →
  Lean.Elab.TermElabM
    (Array
      (Lean.Name ×
        (Lean.StrLit →
          StateT (Array (Lean.TSyntax `doc_arg)) Lean.Doc.DocM (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))))
-- Init.Data.Vector.Zip
Vector.reverse_zipWith : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} {f : α → β → γ} {as : Vector α n} {bs : Vector β n},
  (Vector.zipWith f as bs).reverse = Vector.zipWith f as.reverse bs.reverse
-- Mathlib.Algebra.Homology.SpectralObject.FirstPage
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.HasFirstPageComputation.mk : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  {data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀},
  (∀ (pq : κ), data.i₀ r₀ pq ⋯ = data.i₁ pq) → (∀ (pq : κ), data.i₂ pq = data.i₃ r₀ pq ⋯) → data.HasFirstPageComputation
-- Mathlib.RingTheory.LocalRing.ResidueField.Basic
IsLocalRing.ResidueField.instIsScalarTower : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : IsLocalRing R] [inst_2 : CommRing S]
  [inst_3 : IsLocalRing S] [inst_4 : Algebra R S] [inst_5 : IsLocalHom (algebraMap R S)] {R₀ : Type u_4}
  [inst_6 : CommRing R₀] [inst_7 : Algebra R₀ R] [inst_8 : Algebra R₀ S] [IsScalarTower R₀ R S],
  IsScalarTower R₀ (IsLocalRing.ResidueField R) (IsLocalRing.ResidueField S)
-- Mathlib.Order.Monotone.Basic
List.foldr_strictMono : ∀ {α : Type u} {β : Type v} [inst : Preorder β] {f : α → β → β},
  (∀ (a : α), StrictMono (f a)) → ∀ (l : List α), StrictMono fun b => List.foldr f b l
-- Mathlib.Analysis.Normed.Ring.Basic
nnnorm_intCast_abs : ∀ {α : Type u_2} [inst : SeminormedRing α] (z : ℤ), ‖↑|z|‖₊ = ‖↑z‖₊
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle_inv_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ] (X₁ X₂ : C)
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X₁ X₂],
  (CategoryTheory.Pretriangulated.binaryProductTriangleIsoBinaryBiproductTriangle X₁ X₂).inv.hom₃ =
    CategoryTheory.CategoryStruct.id X₂
-- Mathlib.Algebra.SkewPolynomial.Basic
/-- `X` is the SkewPolynomial variable (aka indeterminate).  -/
SkewPolynomial.X : {R : Type u_1} → [inst : Semiring R] → SkewPolynomial R
-- Mathlib.GroupTheory.FreeGroup.CyclicallyReduced
FreeGroup.reduceCyclically.nil : ∀ {α : Type u} [inst : DecidableEq α], FreeGroup.reduceCyclically [] = []
-- Lean.Util.Diff
Lean.Diff.instToStringAction : ToString Lean.Diff.Action
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.isEmpty_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k : α},
  (t.erase k).isEmpty = (t.isEmpty || t.size == 1 && t.contains k)
-- Mathlib.CategoryTheory.Sites.Hypercover.Zero
CategoryTheory.Precoverage.Small.mk : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Precoverage C},
  (∀ {S : C} (E : J.ZeroHypercover S), E.Small) → J.Small