mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.Order.Compact
/-- The **extreme value theorem**: if a continuous function `f` is larger than a value in its range
away from compact sets, then it has a global minimum.  -/
Continuous.exists_forall_le' : ∀ {α : Type u_2} {β : Type u_3} [inst : LinearOrder α] [inst_1 : TopologicalSpace α] [inst_2 : TopologicalSpace β]
  [ClosedIicTopology α] {f : β → α},
  Continuous f → ∀ (x₀ : β), (∀ᶠ (x : β) in Filter.cocompact β, f x₀ ≤ f x) → ∃ x, ∀ (y : β), f x ≤ f y
-- Lean.Elab.PreDefinition.Structural.Basic
/-- Return true iff `e` contains an application `recFnName .. t ..` where the term `t` is
the argument we are trying to recurse on, and it contains loose bound variables.

We use this test to decide whether we should process a matcher-application as a regular
application or not. That is, whether we should push the `below` argument should be affected by the matcher or not.
If `e` does not contain an application of the form `recFnName .. t ..`, then we know
the recursion doesn't depend on any pattern variable in this matcher.
 -/
Lean.Elab.Structural.recArgHasLooseBVarsAt : Lean.Name → ℕ → Lean.Expr → Bool
-- Mathlib.Analysis.Calculus.VectorField
VectorField.fderiv_pullback : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_3} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] (f : E → F)
  (V : F → F) (x : E), (fderiv 𝕜 f x).IsInvertible → (fderiv 𝕜 f x) (VectorField.pullback 𝕜 f V x) = V (f x)
-- Init.Data.List.Lemmas
List.flatten_ne_nil_iff : ∀ {α : Type u_1} {xss : List (List α)}, xss.flatten ≠ [] ↔ ∃ xs ∈ xss, xs ≠ []
-- Mathlib.GroupTheory.Perm.Sign
Equiv.Perm.sign_trans : ∀ {α : Type u} [inst : DecidableEq α] [inst_1 : Fintype α] (f g : Equiv.Perm α),
  Equiv.Perm.sign (Equiv.trans f g) = Equiv.Perm.sign g * Equiv.Perm.sign f
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.objIsoOfEq_trans : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (X : CategoryTheory.Limits.FormalCoproduct C) {i j k : X.I}
  (hij : i = j) (hjk : j = k), X.objIsoOfEq hij ≪≫ X.objIsoOfEq hjk = X.objIsoOfEq ⋯
-- Mathlib.Algebra.Order.Kleene
Prod.instIdemCommSemiring : {α : Type u_1} → {β : Type u_2} → [IdemCommSemiring α] → [IdemCommSemiring β] → IdemCommSemiring (α × β)
-- Mathlib.MeasureTheory.Measure.AddContent
MeasureTheory.addContent_sdiff_of_ne_top : ∀ {α : Type u_1} {C : Set (Set α)} (m : MeasureTheory.AddContent ENNReal C),
  MeasureTheory.IsSetRing C → (∀ s ∈ C, m s ≠ ⊤) → ∀ {s t : Set α}, s ∈ C → t ∈ C → t ⊆ s → m (s \ t) = m s - m t
-- Mathlib.Algebra.Order.Hom.TypeTags
/-- Reinterpret `Multiplicative G ≃*o H` as `G ≃+o Additive H` as.  -/
OrderMonoidIso.toAdditiveRight : {G : Type u_1} →
  {H : Type u_2} →
    [inst : AddCommMonoid G] →
      [inst_1 : PartialOrder G] →
        [inst_2 : CommMonoid H] → [inst_3 : PartialOrder H] → (Multiplicative G ≃*o H) ≃ (G ≃+o Additive H)
-- Mathlib.Algebra.Group.Subgroup.Lattice
/-- **Alias** of `Subgroup.closure_sdiff_one`. -/
Subgroup.closure_diff_one : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Subgroup.closure (s \ {1}) = Subgroup.closure s
-- Mathlib.Data.Seq.Computation
/-- `run c` is an unsound meta function that runs `c` to completion, possibly
resulting in an infinite loop in the VM.  -/
Computation.run : {α : Type u} → Computation α → α
-- Mathlib.Order.Hom.Basic
OrderIso.symm_apply_le : ∀ {α : Type u_2} {β : Type u_3} [inst : LE α] [inst_1 : LE β] (e : α ≃o β) {x : α} {y : β}, e.symm y ≤ x ↔ y ≤ e x
-- Mathlib.Topology.UniformSpace.Equicontinuity
/-- If a set of functions is equicontinuous, its closure for the product topology is also
equicontinuous.  -/
Set.Equicontinuous.closure : ∀ {X : Type u_3} {α : Type u_6} [tX : TopologicalSpace X] [uα : UniformSpace α] {A : Set (X → α)},
  A.Equicontinuous → (closure A).Equicontinuous
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.iso.congr_simp : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f f_1 : M →ₗ[R] M') (e_f : f = f_1)
  [inst_5 : IsLocalizedModule S f], IsLocalizedModule.iso S f = IsLocalizedModule.iso S f_1
-- Mathlib.AlgebraicTopology.FundamentalGroupoid.Basic
Path.Homotopy.transReflReparamAux.eq_1 : ∀ (t : ↑unitInterval), Path.Homotopy.transReflReparamAux t = if ↑t ≤ 1 / 2 then 2 * ↑t else 1
-- Lean.Data.Lsp.Ipc
Lean.Lsp.Ipc.CallHierarchy.brecOn_1.eq : ∀ {motive_1 : Lean.Lsp.Ipc.CallHierarchy → Sort u} {motive_2 : Array Lean.Lsp.Ipc.CallHierarchy → Sort u}
  {motive_3 : List Lean.Lsp.Ipc.CallHierarchy → Sort u} (t : Array Lean.Lsp.Ipc.CallHierarchy)
  (F_1 : (t : Lean.Lsp.Ipc.CallHierarchy) → t.below → motive_1 t)
  (F_2 : (t : Array Lean.Lsp.Ipc.CallHierarchy) → Lean.Lsp.Ipc.CallHierarchy.below_1 t → motive_2 t)
  (F_3 : (t : List Lean.Lsp.Ipc.CallHierarchy) → Lean.Lsp.Ipc.CallHierarchy.below_2 t → motive_3 t),
  Lean.Lsp.Ipc.CallHierarchy.brecOn_1 t F_1 F_2 F_3 = F_2 t (Lean.Lsp.Ipc.CallHierarchy.brecOn_1.go t F_1 F_2 F_3).2
-- Mathlib.FieldTheory.PurelyInseparable.PerfectClosure
/-- If `E / F` is a field extension of exponential characteristic `q`, if `{ u_i }` is a
family of separable elements of `E` which is `F`-linearly independent, then `{ u_i ^ (q ^ n) }`
is also `F`-linearly independent for any natural number `n`.  -/
LinearIndependent.map_pow_expChar_pow_of_isSeparable' : ∀ {F : Type u} {E : Type v} [inst : Field F] [inst_1 : Field E] [inst_2 : Algebra F E] (q n : ℕ) [hF : ExpChar F q]
  {ι : Type u_1} {v : ι → E},
  (∀ (i : ι), IsSeparable F (v i)) → LinearIndependent F v → LinearIndependent F fun x => v x ^ q ^ n
-- Mathlib.RingTheory.Trace.Basic
Algebra.trace_eq_of_equiv_equiv : ∀ {A₁ : Type u_7} {B₁ : Type u_8} {A₂ : Type u_9} {B₂ : Type u_10} [inst : CommRing A₁] [inst_1 : CommRing B₁]
  [inst_2 : CommRing A₂] [inst_3 : CommRing B₂] [inst_4 : Algebra A₁ B₁] [inst_5 : Algebra A₂ B₂] (e₁ : A₁ ≃+* A₂)
  (e₂ : B₁ ≃+* B₂),
  (algebraMap A₂ B₂).comp ↑e₁ = (↑e₂).comp (algebraMap A₁ B₁) →
    ∀ (x : B₁), (Algebra.trace A₁ B₁) x = e₁.symm ((Algebra.trace A₂ B₂) (e₂ x))
-- Init.Data.List.Lemmas
_private.Init.Data.List.Lemmas.0.List.partition.loop.match_1.eq_1 : ∀ {α : Type u_1} (motive : List α → List α × List α → Sort u_2) (bs cs : List α)
  (h_1 : (bs cs : List α) → motive [] (bs, cs)) (h_2 : (a : α) → (as bs cs : List α) → motive (a :: as) (bs, cs)),
  (match [], (bs, cs) with
    | [], (bs, cs) => h_1 bs cs
    | a :: as, (bs, cs) => h_2 a as bs cs) =
    h_1 bs cs
-- Mathlib.Algebra.DirectSum.Internal
finsetProd_apply_eq_zero : ∀ {ι : Type u_1} {σ : Type u_2} {R : Type u_4} [inst : AddCommMonoid ι] [inst_1 : LinearOrder ι] [IsOrderedAddMonoid ι]
  [inst_3 : DecidableEq ι] [CanonicallyOrderedAdd ι] [inst_5 : CommSemiring R] [inst_6 : SetLike σ R]
  [inst_7 : AddSubmonoidClass σ R] {A : ι → σ} [inst_8 : SetLike.GradedMonoid A]
  {s : Finset (DirectSum ι fun i => ↥(A i))} {m : ι},
  (∀ x ∈ s, ∀ k < m, x k = 0) → ∀ ⦃n : ι⦄, n < s.card • m → (∏ x ∈ s, x) n = 0
-- Mathlib.RingTheory.Polynomial.UniversalFactorizationRing
Polynomial.map_map_freeMonic : ∀ (R : Type u_1) (S : Type u_2) [inst : CommRing R] [inst_1 : CommRing S] (n : ℕ) (f : R →+* S),
  Polynomial.map (MvPolynomial.map f) (Polynomial.freeMonic R n) = Polynomial.freeMonic S n
-- Lean.Compiler.LCNF.Basic
Lean.Compiler.LCNF.LetValue.const.inj : ∀ {pu : Lean.Compiler.LCNF.Purity} {declName : Lean.Name} {us : List Lean.Level}
  {args : Array (Lean.Compiler.LCNF.Arg pu)}
  {h : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.LetValue._auto_3} {declName_1 : Lean.Name}
  {us_1 : List Lean.Level} {args_1 : Array (Lean.Compiler.LCNF.Arg pu)}
  {h_1 : autoParam (pu = Lean.Compiler.LCNF.Purity.pure) Lean.Compiler.LCNF.LetValue._auto_3},
  Lean.Compiler.LCNF.LetValue.const declName us args h = Lean.Compiler.LCNF.LetValue.const declName_1 us_1 args_1 h_1 →
    declName = declName_1 ∧ us = us_1 ∧ args = args_1
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzOnWith_iff_norm_div_le : ∀ {E : Type u_2} {F : Type u_3} [inst : SeminormedCommGroup E] [inst_1 : SeminormedCommGroup F] {f : E → F} {C : NNReal}
  {s : Set E}, LipschitzOnWith C f s ↔ ∀ ⦃x : E⦄, x ∈ s → ∀ ⦃y : E⦄, y ∈ s → ‖f x / f y‖ ≤ ↑C * ‖x / y‖
-- Init.Data.UInt.Lemmas
UInt8.instLawfulOrderLT : Std.LawfulOrderLT UInt8
-- Mathlib.Data.Set.MemPartition
memPartitionSet_eq_iff : ∀ {α : Type u_1} {f : ℕ → Set α} {n : ℕ} (a : α) {s : Set α}, s ∈ memPartition f n → (memPartitionSet f n a = s ↔ a ∈ s)
-- Lean.Data.Lsp.Internal
Lean.Lsp.RefInfo.mk.sizeOf_spec : ∀ (definition? : Option Lean.Lsp.RefInfo.Location) (usages : Array Lean.Lsp.RefInfo.Location),
  sizeOf { definition? := definition?, usages := usages } = 1 + sizeOf definition? + sizeOf usages
-- Mathlib.CategoryTheory.Limits.Preserves.Limits
CategoryTheory.ι_preservesColimitIso_inv_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) {J : Type w} [inst_2 : CategoryTheory.Category.{w', w} J]
  (F : CategoryTheory.Functor J C) [inst_3 : CategoryTheory.Limits.PreservesColimit F G]
  [inst_4 : CategoryTheory.Limits.HasColimit F] (j : J) {Z : D} (h : G.obj (CategoryTheory.Limits.colimit F) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.colimit.ι (F.comp G) j)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.preservesColimitIso G F).inv h) =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.colimit.ι F j)) h
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
CategoryTheory.Limits.kernel.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C}
  (f f_1 : X ⟶ Y) (e_f : f = f_1) [inst_2 : CategoryTheory.Limits.HasKernel f],
  CategoryTheory.Limits.kernel f = CategoryTheory.Limits.kernel f_1
-- Mathlib.RingTheory.SimpleModule.Basic
/-- A module generated by semisimple submodules is itself semisimple.  -/
isSemisimpleModule_of_isSemisimpleModule_submodule : ∀ {ι : Type u_1} {R : Type u_2} [inst : Ring R] {M : Type u_4} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {s : Set ι} {p : ι → Submodule R M},
  (∀ i ∈ s, IsSemisimpleModule R ↥(p i)) → ⨆ i ∈ s, p i = ⊤ → IsSemisimpleModule R M
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Carry
Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go.eq_def : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {w : ℕ} (aig : Std.Sat.AIG α) (lhs rhs : aig.RefVec w)
  (curr : ℕ) (cin : aig.Ref),
  Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go aig lhs rhs curr cin =
    if hidx : curr < w then
      let lin := lhs.get curr hidx;
      let rin := rhs.get curr hidx;
      let res := Std.Tactic.BVDecide.BVExpr.bitblast.mkFullAdderCarry aig { lhs := lin, rhs := rin, cin := cin };
      have this := ⋯;
      let aig_1 := res.aig;
      have carryRef := res.ref;
      have lhs := lhs.cast this;
      have rhs := rhs.cast this;
      Std.Tactic.BVDecide.BVExpr.bitblast.mkOverflowBit.go aig_1 lhs rhs (curr + 1) carryRef
    else { aig := aig, ref := cin }
-- Mathlib.LinearAlgebra.BilinearForm.Hom
/-- Apply a linear equivalence on the arguments of a bilinear form.  -/
LinearMap.BilinForm.congr : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {M' : Type u_7} →
            [inst_3 : AddCommMonoid M'] →
              [inst_4 : Module R M'] → (M ≃ₗ[R] M') → LinearMap.BilinForm R M ≃ₗ[R] LinearMap.BilinForm R M'
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.foldM_map : ∀ {α β γ δ : Type w} {n : Type w → Type w''} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad n]
  [LawfulMonad n] [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {f : β → γ} {g : δ → γ → n δ}
  {init : δ} {it : Std.Iter β},
  Std.Iter.foldM g init (Std.Iter.map f it) = Std.Iter.foldM (fun d b => g d (f b)) init it
-- Aesop.Frontend.Saturate
Aesop.Frontend.isImplication : Lean.Expr → Lean.MetaM Bool
-- Mathlib.GroupTheory.Congruence.Hom
Con.mapGen.eq_1 : ∀ {M : Type u_1} {N : Type u_2} [inst : Mul M] [inst_1 : Mul N] {c : Con M} (f : M → N),
  Con.mapGen f = conGen (Relation.Map (⇑c) f f)
-- Mathlib.AlgebraicGeometry.AffineTransitionLimit
/-- (Implementation) A family of open covers refining `𝒰S`. See the section docstring.  -/
AlgebraicGeometry.ExistsHomHomCompEqCompAux.𝒰X : {I : Type u} →
  [inst : CategoryTheory.Category.{u, u} I] →
    {S X : AlgebraicGeometry.Scheme} →
      {D : CategoryTheory.Functor I AlgebraicGeometry.Scheme} →
        {t : D ⟶ (CategoryTheory.Functor.const I).obj S} →
          {f : X ⟶ S} →
            (self : AlgebraicGeometry.ExistsHomHomCompEqCompAux D t f) →
              (i : (CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f self.𝒰S).I₀) →
                ((CategoryTheory.Precoverage.ZeroHypercover.pullback₁ f self.𝒰S).X i).OpenCover
-- Mathlib.Probability.Process.PartitionFiltration
ProbabilityTheory.iSup_partitionFiltration_eq_generateFrom_range : ∀ {α : Type u_1} [m : MeasurableSpace α] {t : ℕ → Set α} (ht : ∀ (n : ℕ), MeasurableSet (t n)),
  ⨆ n, ↑(ProbabilityTheory.partitionFiltration ht) n = MeasurableSpace.generateFrom (Set.range t)
-- Mathlib.Order.Filter.Map
Filter.map_eq_map_iff_of_injOn : ∀ {α : Type u_1} {β : Type u_2} {f g : Filter α} {m : α → β} {s : Set α},
  s ∈ f → s ∈ g → Set.InjOn m s → (Filter.map m f = Filter.map m g ↔ f = g)
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsTrail.of_append_left : ∀ {V : Type u} {G : SimpleGraph V} {u v w : V} {p : G.Walk u v} {q : G.Walk v w}, (p.append q).IsTrail → p.IsTrail
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.RealizeConstResult.dyn : Lean.Environment.RealizeConstResult✝ → Dynamic
-- Mathlib.ModelTheory.Basic
/-- A bijection as a first-order isomorphism with the induced structure on the codomain.  -/
Equiv.inducedStructureEquiv : {L : FirstOrder.Language} → {M : Type u_1} → {N : Type u_2} → [inst : L.Structure M] → (e : M ≃ N) → L.Equiv M N
-- Lean.Elab.Tactic.Omega.Core
Lean.Elab.Tactic.Omega.Justification.bmod.injEq : ∀ (m : ℕ) (r : ℤ) (i : ℕ) {x : Lean.Omega.Coeffs}
  (j j_1 : Lean.Elab.Tactic.Omega.Justification (Lean.Omega.Constraint.exact r) x),
  (Lean.Elab.Tactic.Omega.Justification.bmod m r i j = Lean.Elab.Tactic.Omega.Justification.bmod m r i j_1) = (j = j_1)
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.norm_cert : Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Expr → Lean.Grind.Linarith.Poly → Bool
-- Aesop.Tree.Data
Aesop.Goal.isForcedUnprovable : Aesop.Goal → Bool
-- Mathlib.Algebra.FreeMonoid.Basic
/-- Recursor for `FreeAddMonoid` using `0` and
`FreeAddMonoid.of x + xs` instead of `[]` and `x :: xs`.  -/
FreeAddMonoid.recOn : {α : Type u_1} →
  {motive : FreeAddMonoid α → Sort u_6} →
    (xs : FreeAddMonoid α) →
      motive 0 → ((x : α) → (xs : FreeAddMonoid α) → motive xs → motive (FreeAddMonoid.of x + xs)) → motive xs
-- Mathlib.Algebra.BigOperators.Group.List.Basic
List.add_sum_eraseIdx : ∀ {M : Type u_4} [inst : AddMonoid M] {l : List M} {i : ℕ} (hlen : i < l.length),
  (∀ a' ∈ List.take i l, AddCommute l[i] a') → l[i] + (l.eraseIdx i).sum = l.sum
-- Mathlib.Algebra.Ring.Parity
Nat.ne_of_odd_add : ∀ {m n : ℕ}, Odd (m + n) → m ≠ n
-- Mathlib.GroupTheory.PushoutI
Monoid.PushoutI.NormalWord.base_smul_def : ∀ {ι : Type u_1} {G : ι → Type u_2} {H : Type u_3} [inst : (i : ι) → Group (G i)] [inst_1 : Group H]
  {φ : (i : ι) → H →* G i} {d : Monoid.PushoutI.NormalWord.Transversal φ} [inst_2 : DecidableEq ι]
  [inst_3 : (i : ι) → DecidableEq (G i)] (h : H) (w : Monoid.PushoutI.NormalWord d),
  (Monoid.PushoutI.base φ) h • w = { toWord := w.toWord, head := h * w.head, normalized := ⋯ }
-- Mathlib.GroupTheory.Perm.Cycle.Basic
/-- Restrict a permutation to its support  -/
Equiv.Perm.subtypePermOfSupport : {α : Type u_2} → [inst : Fintype α] → [inst_1 : DecidableEq α] → (c : Equiv.Perm α) → Equiv.Perm ↥c.support
-- Mathlib.CategoryTheory.Shift.Induced
CategoryTheory.HasShift.Induced.add_hom_app_obj : ∀ {C : Type u_3} {D : Type u_1} [inst : CategoryTheory.Category.{v_1, u_3} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} D] (F : CategoryTheory.Functor C D) {A : Type u_2} [inst_2 : AddMonoid A]
  [inst_3 : CategoryTheory.HasShift C A] (s : A → CategoryTheory.Functor D D)
  (i : (a : A) → F.comp (s a) ≅ (CategoryTheory.shiftFunctor C a).comp F)
  [inst_4 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Full]
  [inst_5 : ((CategoryTheory.Functor.whiskeringLeft C D D).obj F).Faithful] (a b : A) (X : C),
  (CategoryTheory.HasShift.Induced.add F s i a b).hom.app (F.obj X) =
    CategoryTheory.CategoryStruct.comp ((i (a + b)).hom.app X)
      (CategoryTheory.CategoryStruct.comp (F.map ((CategoryTheory.shiftFunctorAdd C a b).hom.app X))
        (CategoryTheory.CategoryStruct.comp ((i b).inv.app ((CategoryTheory.shiftFunctor C a).obj X))
          ((s b).map ((i a).inv.app X))))
-- Mathlib.Data.EReal.Basic
EReal.exists : ∀ {p : EReal → Prop}, (∃ r, p r) ↔ p ⊥ ∨ p ⊤ ∨ ∃ r, p ↑r
-- Init.Data.Dyadic.Basic
Dyadic.ofOdd.sizeOf_spec : ∀ (n k : ℤ) (hn : n % 2 = 1), sizeOf (Dyadic.ofOdd n k hn) = 1 + sizeOf n + sizeOf k + sizeOf hn
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplexShift
CochainComplex.HomComplex.Cochain.leftUnshift_add : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} {n' a : ℤ}
  (γ₁ γ₂ : CochainComplex.HomComplex.Cochain ((CategoryTheory.shiftFunctor (CochainComplex C ℤ) a).obj K) L n') (n : ℤ)
  (hn : n + a = n'), (γ₁ + γ₂).leftUnshift n hn = γ₁.leftUnshift n hn + γ₂.leftUnshift n hn
-- Init.Data.Ord.Basic
Ordering.isGT_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isGT = (o₁.isGT || o₁.isEq && o₂.isGT)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.get!_diff_of_mem_right : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.DTreeMap.Raw α β cmp} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α} [inst_1 : Inhabited (β k)], k ∈ t₂ → (t₁ \ t₂).get! k = default
-- Mathlib.Order.TypeTags
/-- The canonical map from `α` into `WithBot α`  -/
WithBot.some : {α : Type u_1} → α → WithBot α
-- Mathlib.LinearAlgebra.Matrix.Determinant.Basic
Matrix.det_fin_two_of : ∀ {R : Type v} [inst : CommRing R] (a b c d : R), !![a, b; c, d].det = a * d - b * c
-- Mathlib.NumberTheory.LSeries.HurwitzZetaEven
HurwitzZeta.evenKernel_neg : ∀ (a : UnitAddCircle) (x : ℝ), HurwitzZeta.evenKernel (-a) x = HurwitzZeta.evenKernel a x
-- Mathlib.Topology.Algebra.OpenSubgroup
AddSubgroup.instFiniteQuotientOfSeparatelyContinuousAddOfCompactSpace : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [SeparatelyContinuousAdd G] [CompactSpace G]
  (U : OpenAddSubgroup G), Finite (G ⧸ ↑U)
-- Mathlib.Algebra.Order.Monoid.NatCast
/-- **Alias** of `zero_lt_four`.

---

See `zero_lt_four'` for a version with the type explicit.  -/
four_pos : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftMono α],
  0 < 4
-- Mathlib.Topology.Algebra.Valued.NormedValued
/-- The valuation of a normed field has rank at most one  -/
NormedField.instRankLeOneNNRealValuation : {K : Type u_1} → [hK : NormedField K] → [inst : IsUltrametricDist K] → NormedField.valuation.RankLeOne
-- Lean.Data.Lsp.TextSync
Lean.Lsp.TextDocumentSyncKind.none.sizeOf_spec : sizeOf Lean.Lsp.TextDocumentSyncKind.none = 1
-- Mathlib.Topology.Algebra.UniformConvergence
UniformFun.toFun_one : ∀ {α : Type u_1} {β : Type u_2} [inst : One β], UniformFun.toFun 1 = 1
-- Mathlib.Data.Sym.Basic
Sym.map.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} (f : α → β) (x : Sym α n), Sym.map f x = ⟨Multiset.map f ↑x, ⋯⟩
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.PullbackCone
CategoryTheory.Limits.PullbackCone.isoMk_hom_hom : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Functor CategoryTheory.Limits.WalkingCospan C} (t : CategoryTheory.Limits.Cone F),
  (CategoryTheory.Limits.PullbackCone.isoMk t).hom.hom = CategoryTheory.CategoryStruct.id t.pt
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.forM_eq_forM_keysArray : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m : Std.DHashMap.Raw α β} {m' : Type w → Type w'}
  [inst_2 : Monad m'] [LawfulMonad m'] {f : α → m' PUnit.{w + 1}},
  m.WF → Std.DHashMap.Raw.forM (fun a x => f a) m = Array.forM f m.keysArray
-- Mathlib.Topology.ContinuousMap.Compact
ContinuousMap.dist_le_iff_of_nonempty : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : CompactSpace α] [inst_2 : PseudoMetricSpace β]
  {f g : C(α, β)} {C : ℝ} [Nonempty α], dist f g ≤ C ↔ ∀ (x : α), dist (f x) (g x) ≤ C
-- Mathlib.GroupTheory.GroupAction.SubMulAction
SubMulAction.instInfSet.eq_1 : ∀ {R : Type u} {M : Type v} [inst : SMul R M],
  SubMulAction.instInfSet = { sInf := fun S => { carrier := ⋂ s ∈ S, ↑s, smul_mem' := ⋯ } }
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
Std.Tactic.BVDecide.BVBinOp.instToString : ToString Std.Tactic.BVDecide.BVBinOp
-- Batteries.Recycling.RBTree.Basic
/-- `O(n)`. Map a function on every value in the tree.
This requires `IsMonotone` on the function in order to preserve the order invariant.
 -/
RBTree.RBNode.map : {α : Type u_1} → {β : Type u_2} → (α → β) → RBTree.RBNode α → RBTree.RBNode β
-- Mathlib.Topology.LocallyFinite
LocallyFinite.isClosed_iUnion : ∀ {ι : Type u_1} {X : Type u_4} [inst : TopologicalSpace X] {f : ι → Set X},
  LocallyFinite f → (∀ (i : ι), IsClosed (f i)) → IsClosed (⋃ i, f i)
-- Init.Data.SInt.Lemmas
Int32.toInt_ofIntTruncate : ∀ {x : ℤ}, Int32.minValue.toInt ≤ x → x ≤ Int32.maxValue.toInt → (Int32.ofIntClamp x).toInt = x
-- Mathlib.NumberTheory.RamificationInertia.Basic
Ideal.Factors.piQuotientEquiv_mk : ∀ {R : Type u} [inst : CommRing R] {S : Type v} [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [inst_3 : IsDedekindDomain S] (p : Ideal R) (hp : Ideal.map (algebraMap R S) p ≠ ⊥) (x : S),
  (Ideal.Factors.piQuotientEquiv p hp) ((Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) x) = fun x_1 =>
    (Ideal.Quotient.mk (↑x_1 ^ p.ramificationIdx' ↑x_1)) x
-- Mathlib.Algebra.Order.Monoid.Canonical.Basic
lt_add_iff_lt_left_or_exists_lt : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c : α} [inst_1 : Add α] [CanonicallyOrderedAdd α] [AddLeftReflectLT α]
  [IsLeftCancelAdd α], a < b + c ↔ a < b ∨ ∃ d < c, a = b + d
-- Batteries.Data.List.Lemmas
List.min!.eq_1 : ∀ {α : Type u_1} [inst : Inhabited α] [inst_1 : Min α] (xs : List α),
  xs.min! =
    match xs.min? with
    | none => panicWithPosWithDecl "Batteries.Data.List.Basic" "List.min!" 27 12 "List.min! called on empty list"
    | some x => x
-- Mathlib.Algebra.MvPolynomial.Degrees
/-- `degreeOf n p` gives the highest power of $X_n$ that appears in `p`  -/
MvPolynomial.degreeOf : {R : Type u} → {σ : Type u_1} → [inst : CommSemiring R] → σ → MvPolynomial σ R → ℕ
-- Mathlib.Control.Fold
Traversable.foldrm.eq_1 : ∀ {α β : Type u} {t : Type u → Type u} [inst : Traversable t] {m : Type u → Type u} [inst_1 : Monad m] (f : α → β → m β)
  (x : β) (xs : t α), Traversable.foldrm f x xs = (Traversable.foldMap (Monoid.foldrM.mk ∘ f) xs).get x
-- Mathlib.Analysis.Normed.Ring.Basic
NormedCommRing.toNormedRing : {α : Type u_5} → [self : NormedCommRing α] → NormedRing α
-- Init.Data.Iterators.Consumers.Monadic.Loop
/-- Internal implementation detail of the iterator library.  -/
Std.IteratorLoop.WithWF : (α : Type w) →
  (m : Type w → Type w') →
    {β : Type w} →
      [inst : Std.Iterator α m β] →
        {γ : Type x} →
          (PlausibleForInStep : β → γ → ForInStep γ → Prop) →
            Std.IteratorLoop.WellFounded α m PlausibleForInStep → Type (max w x)
-- Aesop.Util.UnionFind
Aesop.UnionFind : (α : Type u_1) → [BEq α] → [Hashable α] → Type u_1
-- Lean.Elab.Tactic.ElabTerm
Lean.Elab.Tactic.evalApplyLikeTactic : (Lean.MVarId → Lean.Expr → Lean.MetaM (List Lean.MVarId)) → Lean.Syntax → Lean.Elab.Tactic.TacticM Unit