mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Tactic.NormNum.BigOperators
Mathlib.Meta.Multiset.ProveZeroOrConsResult.cons.injEq : ∀ {u : Lean.Level} {α : Q(Type u)} {s : Q(Multiset «$α»)} (a : Q(«$α»)) (s' : Q(Multiset «$α»))
  (pf : Q(«$s» = «$a» ::ₘ «$s'»)) (a_1 : Q(«$α»)) (s'_1 : Q(Multiset «$α»)) (pf_1 : Q(«$s» = «$a_1» ::ₘ «$s'_1»)),
  (Mathlib.Meta.Multiset.ProveZeroOrConsResult.cons a s' pf =
      Mathlib.Meta.Multiset.ProveZeroOrConsResult.cons a_1 s'_1 pf_1) =
    (a = a_1 ∧ s' = s'_1 ∧ pf = pf_1)
-- Mathlib.Topology.Algebra.Valued.WithVal
WithVal.equivWithVal_symm : ∀ {R : Type u_1} {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] [inst_1 : Ring R] {Γ'₀ : Type u_3}
  [inst_2 : LinearOrderedCommGroupWithZero Γ'₀] (v : Valuation R Γ₀) (w : Valuation R Γ'₀),
  (WithVal.congr v w (RingEquiv.refl R)).symm = WithVal.congr w v (RingEquiv.refl R)
-- Mathlib.Tactic.GCongr.Core
/-- The number of arguments that `head` is applied to.
For example, `a + b ≤ a + c` has `arity := 6`, because `HAdd.hAdd` has 6 arguments.  -/
Mathlib.Tactic.GCongr.GCongrKey.arity : Mathlib.Tactic.GCongr.GCongrKey → ℕ
-- Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Unital
cfc_le_iff : ∀ {R : Type u_1} {A : Type u_2} {p : A → Prop} [inst : CommRing R] [inst_1 : PartialOrder R] [inst_2 : StarRing R]
  [inst_3 : MetricSpace R] [inst_4 : IsTopologicalRing R] [inst_5 : ContinuousStar R] [ContinuousSqrt R]
  [StarOrderedRing R] [inst_8 : TopologicalSpace A] [inst_9 : Ring A] [inst_10 : StarRing A] [inst_11 : PartialOrder A]
  [StarOrderedRing A] [inst_13 : Algebra R A] [instCFC : ContinuousFunctionalCalculus R A p] [NonnegSpectrumClass R A]
  (f g : R → R) (a : A),
  autoParam (ContinuousOn f (spectrum R a)) cfc_le_iff._auto_1 →
    autoParam (ContinuousOn g (spectrum R a)) cfc_le_iff._auto_3 →
      autoParam (p a) cfc_le_iff._auto_5 → (cfc f a ≤ cfc g a ↔ ∀ x ∈ spectrum R a, f x ≤ g x)
-- Mathlib.NumberTheory.Fermat
/-- Prime `a ^ n - 1` implies `a = 2` and prime `n`.  -/
Nat.prime_of_pow_sub_one_prime : ∀ {a n : ℕ}, n ≠ 1 → Nat.Prime (a ^ n - 1) → a = 2 ∧ Nat.Prime n
-- Mathlib.Algebra.Category.Ring.Under.Basic
/-- Make an isomorphism in `Under R` from an algebra isomorphism.  -/
AlgEquiv.toUnder : {R : CommRingCat} →
  {A B : Type u} →
    [inst : CommRing A] →
      [inst_1 : CommRing B] →
        [inst_2 : Algebra (↑R) A] → [inst_3 : Algebra (↑R) B] → (A ≃ₐ[↑R] B) → (R.mkUnder A ≅ R.mkUnder B)
-- Mathlib.Data.Vector.MapLemmas
List.Vector.map_map : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} (xs : List.Vector α n) (f₁ : β → γ) (f₂ : α → β),
  List.Vector.map f₁ (List.Vector.map f₂ xs) = List.Vector.map (fun x => f₁ (f₂ x)) xs
-- Init.Data.SInt.Lemmas
Int8.right_eq_add : ∀ {a b : Int8}, b = a + b ↔ a = 0
-- Lean.Data.Lsp.BasicAux
Lean.Lsp.instLTRange : LT Lean.Lsp.Range
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.isEmpty_dropWhile : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String.Slice},
  (s.dropWhile pat).isEmpty = s.all pat
-- Mathlib.RingTheory.Extension.Presentation.Submersive
Algebra.PreSubmersivePresentation.naive_toPresentation : ∀ {R : Type u} {ι : Type w} {σ : Type t} [inst : CommRing R] {v : ι → MvPolynomial σ R} (a : ι → σ)
  (ha : Function.Injective a)
  (s : optParam (MvPolynomial σ R ⧸ Ideal.span (Set.range v) → MvPolynomial σ R) (Function.surjInv ⋯))
  (hs :
    autoParam
      (∀ (x : MvPolynomial σ R ⧸ Ideal.span (Set.range v)), (Ideal.Quotient.mk (Ideal.span (Set.range v))) (s x) = x)
      Algebra.PreSubmersivePresentation.naive._auto_1),
  (Algebra.PreSubmersivePresentation.naive a ha s hs).toPresentation = Algebra.Presentation.naive s hs
-- Mathlib.Topology.Algebra.Algebra.Equiv
ContinuousAlgEquivClass.toHomeomorphClass : ∀ {F : Type u_1} {R : outParam (Type u_2)} {A : outParam (Type u_3)} {B : outParam (Type u_4)} {inst : CommSemiring R}
  {inst_1 : Semiring A} {inst_2 : TopologicalSpace A} {inst_3 : Semiring B} {inst_4 : TopologicalSpace B}
  {inst_5 : Algebra R A} {inst_6 : Algebra R B} {inst_7 : EquivLike F A B} [self : ContinuousAlgEquivClass F R A B],
  HomeomorphClass F A B
-- Mathlib.Data.Set.Insert
Set.mem_of_mem_insert_of_ne : ∀ {α : Type u_1} {s : Set α} {a b : α}, b ∈ insert a s → b ≠ a → b ∈ s
-- Mathlib.Data.Nat.Factorization.Root
Nat.ceilRoot_zero_right : ∀ (n : ℕ), n.ceilRoot 0 = 0
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_smul : ∀ {K : Type u_9} {V : Type u_10} {V₂ : Type u_11} [inst : Semifield K] [inst_1 : AddCommMonoid V] [inst_2 : Module K V]
  [inst_3 : AddCommMonoid V₂] [inst_4 : Module K V₂] (f : V →ₗ[K] V₂) (p : Submodule K V₂) (a : K),
  a ≠ 0 → Submodule.comap (a • f) p = Submodule.comap f p
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.getElem?_eq : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k : α}, m₁.Equiv m₂ → m₁[k]? = m₂[k]?
-- Init.Data.List.Basic
/-- Separates a list of pairs into two lists that contain the respective first and second components.

`O(|l|)`.

Examples:
* `[("Monday", 1), ("Tuesday", 2)].unzip = (["Monday", "Tuesday"], [1, 2])`
* `[(x₁, y₁), (x₂, y₂), (x₃, y₃)].unzip = ([x₁, x₂, x₃], [y₁, y₂, y₃])`
* `([] : List (Nat × String)).unzip = (([], []) : List Nat × List String)`
 -/
List.unzip : {α : Type u} → {β : Type v} → List (α × β) → List α × List β
-- Mathlib.NumberTheory.LSeries.Linearity
LSeries.term_add_apply : ∀ (f g : ℕ → ℂ) (s : ℂ) (n : ℕ), LSeries.term (f + g) s n = LSeries.term f s n + LSeries.term g s n
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.d_normEq0_cert : ℕ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.CategoryTheory.Presentable.CardinalDirectedPoset
/-- **Alias** of `CategoryTheory.CardinalDirectedPoset.coconeWithTop`.

---

If `J : CardinalFilteredPoset κ` and `κ'` is any regular cardinal,
this is a colimit cocone which exhibits `J.withTop` as the `κ'`-filtered
colimit of its subsets that are of cardinality `< κ'` and contain `⊤`.  -/
CategoryTheory.CardinalFilteredPoset.coconeWithTop : {κ : Cardinal.{u}} →
  [inst : Fact κ.IsRegular] →
    (J : CategoryTheory.CardinalDirectedPoset κ) →
      (κ' : Cardinal.{u}) →
        [inst_1 : Fact κ'.IsRegular] →
          CategoryTheory.Limits.Cocone
            (CategoryTheory.CardinalDirectedPoset.functorOfPredicateSet (J.PropSetWithTop κ'))
-- Std.Http.Protocol.H1
/-- Returns `true` if both reader and writer are closed and no output remains.
 -/
Std.Http.Protocol.H1.Machine.halted : {dir : Std.Http.Protocol.H1.Direction} → Std.Http.Protocol.H1.Machine dir → Bool
-- Mathlib.Data.PFunctor.Multivariate.M
/-- Implementation of destructor for M-type of `P`  -/
MvPFunctor.M.pathDestLeft : {n : ℕ} →
  (P : MvPFunctor.{u} (n + 1)) →
    {α : TypeVec.{u_1} n} →
      {x : P.last.M} →
        {a : P.A} →
          {f : P.last.B a → P.last.M} → x.dest = ⟨a, f⟩ → TypeVec.Arrow (MvPFunctor.M.Path P x) α → (P.drop.B a).Arrow α
-- Mathlib.Order.Filter.Extr
IsMinFilter.max : ∀ {α : Type u} {β : Type v} [inst : LinearOrder β] {f g : α → β} {a : α} {l : Filter α},
  IsMinFilter f l a → IsMinFilter g l a → IsMinFilter (fun x => max (f x) (g x)) l a
-- Mathlib.Probability.Decision.Risk.Basic
/-- The maximal Bayes risk is less than or equal to the minimax risk.  -/
ProbabilityTheory.iSup_bayesRisk_le_minimaxRisk : ∀ {Θ : Type u_1} {𝓧 : Type u_2} {𝓨 : Type u_4} {mΘ : MeasurableSpace Θ} {m𝓧 : MeasurableSpace 𝓧}
  {m𝓨 : MeasurableSpace 𝓨} (ℓ : Θ → 𝓨 → ENNReal) (P : ProbabilityTheory.Kernel Θ 𝓧),
  ⨆ π, ⨆ (_ : MeasureTheory.IsProbabilityMeasure π), ProbabilityTheory.bayesRisk ℓ P π ≤
    ProbabilityTheory.minimaxRisk ℓ P
-- Std.Data.Internal.List.Associative
Std.Internal.List.Const.getValueD_map : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : BEq α] [EquivBEq α] {fallback : γ} {f : α → β → γ}
  {l : List ((_ : α) × β)},
  Std.Internal.List.DistinctKeys l →
    ∀ {k : α},
      Std.Internal.List.getValueD k (List.map (fun p => ⟨p.fst, f p.fst p.snd⟩) l) fallback =
        (Option.pmap (fun v h => f (Std.Internal.List.getKey k l h) v) (Std.Internal.List.getValue? k l) ⋯).getD
          fallback
-- Mathlib.Combinatorics.Quiver.Covering
Prefunctor.star_fst : ∀ {U : Type u_1} [inst : Quiver U] {V : Type u_2} [inst_1 : Quiver V] (φ : U ⥤q V) (u : U) (a : Quiver.Star u),
  (φ.star u a).fst = φ.obj a.fst
-- Mathlib.Data.Finset.Prod
Finset.Nonempty.snd : ∀ {α : Type u_1} {β : Type u_2} {s : Finset α} {t : Finset β}, (s ×ˢ t).Nonempty → t.Nonempty
-- Mathlib.Topology.Algebra.Field
/-- If `f, g` are functions `α → 𝕜`, both continuous on a preconnected set `S`, with
`f ^ 2 = g ^ 2` on `S`, and `g z ≠ 0` all `z ∈ S`, then as soon as `f = g` holds at
one point of `S` it holds for all points.  -/
IsPreconnected.eq_of_sq_eq : ∀ {α : Type u_2} {𝕜 : Type u_3} {f g : α → 𝕜} {S : Set α} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace 𝕜]
  [T1Space 𝕜] [inst_3 : Field 𝕜] [ContinuousInv₀ 𝕜] [ContinuousMul 𝕜],
  IsPreconnected S →
    ContinuousOn f S →
      ContinuousOn g S →
        Set.EqOn (f ^ 2) (g ^ 2) S → (∀ {x : α}, x ∈ S → g x ≠ 0) → ∀ {y : α}, y ∈ S → f y = g y → Set.EqOn f g S
-- Lean.DocString.Markdown
/-- Splits a string into an array of lines on `'\n'`, retaining empty trailing/leading lines (so
`"a\nb\n"` yields `#["a", "b", ""]`). Used to convert code blocks into the line-array representation
used by the rest of the renderer.
 -/
_private.Lean.DocString.Markdown.0.Lean.Doc.splitNewlines : String → Array String
-- Mathlib.LinearAlgebra.Dual.Basis
Module.Basis.eval_ker : ∀ {R : Type uR} {M : Type uM} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_1}
  (b : Module.Basis ι R M), (Module.Dual.eval R M).ker = ⊥
-- Mathlib.Order.Interval.Set.Basic
Set.Ioc_eq_Icc_same_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ioc a b = Set.Icc a b ↔ ¬a ≤ b
-- Init.Data.List.Lemmas
List.mem_of_mem_tail : ∀ {α : Type u_1} {a : α} {l : List α}, a ∈ l.tail → a ∈ l
-- Aesop.Search.Queue
Aesop.LIFOQueue.popGoal : Aesop.LIFOQueue → Option Aesop.GoalRef × Aesop.LIFOQueue
-- Mathlib.Algebra.Order.Ring.StandardPart
ArchimedeanClass.stdPart_ofNat : ∀ {K : Type u_1} [inst : LinearOrder K] [inst_1 : Field K] [inst_2 : IsOrderedRing K] (n : ℕ) [inst_3 : n.AtLeastTwo],
  ArchimedeanClass.stdPart (OfNat.ofNat n) = ↑n
-- Mathlib.Topology.Order.IntermediateValue
ContinuousOn.image_Iio_of_strictAntiOn : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : ConditionallyCompleteLinearOrder α] [OrderTopology α]
  [DenselyOrdered α] {δ : Type u_1} [inst_4 : LinearOrder δ] [inst_5 : TopologicalSpace δ] [OrderClosedTopology δ]
  {a : α} {f : α → δ},
  ContinuousOn f (Set.Iic a) →
    StrictAntiOn f (Set.Iic a) → Filter.Tendsto f Filter.atBot Filter.atTop → f '' Set.Iio a = Set.Ioi (f a)
-- Mathlib.CategoryTheory.Sites.Continuous
CategoryTheory.Functor.sheafPushforwardContinuousIso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F F' : CategoryTheory.Functor C D} (e : F ≅ F') (A : Type u) [inst_2 : CategoryTheory.Category.{t, u} A]
  (J : CategoryTheory.GrothendieckTopology C) (K : CategoryTheory.GrothendieckTopology D) [inst_3 : F.IsContinuous J K]
  [inst_4 : F'.IsContinuous J K],
  (CategoryTheory.Functor.sheafPushforwardContinuousIso e A J K).inv =
    CategoryTheory.Functor.sheafPushforwardContinuousNatTrans e.hom A J K
-- Mathlib.Topology.UniformSpace.Equiv
/-- Uniform isomorphism between `α² = Fin 2 → α` and `α × α`.  -/
UniformEquiv.finTwoArrow : (α : Type u_4) → [inst : UniformSpace α] → (Fin 2 → α) ≃ᵤ α × α
-- Mathlib.CategoryTheory.Presentable.OrthogonalReflection
CategoryTheory.OrthogonalReflection.isLocal_isLocal_reflection : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C) (Z : C)
  [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₁]
  [inst_3 : ∀ (Z : C), CategoryTheory.Limits.HasCoproduct CategoryTheory.OrthogonalReflection.D₁.obj₂]
  [inst_4 :
    ∀ (Z : C), CategoryTheory.Limits.HasMulticoequalizer (CategoryTheory.OrthogonalReflection.D₂.multispanIndex W Z)]
  (κ : Cardinal.{w}) [inst_5 : OrderBot κ.ord.ToType]
  [inst_6 : CategoryTheory.Limits.HasIterationOfShape κ.ord.ToType C],
  W.isLocal.isLocal (CategoryTheory.OrthogonalReflection.reflection W Z κ)
-- Init.Control.Basic
ForInStep.value_yield : ∀ {β : Type u_1} (b : β), (ForInStep.yield b).value = b
-- Mathlib.Topology.Order.OrderClosed
/-- **Alias** of `nhds_inf_atBot`. -/
inf_nhds_atBot : ∀ {α : Type u} [inst : Preorder α] [NoBotOrder α] [inst_2 : TopologicalSpace α] [ClosedIicTopology α] (a : α),
  nhds a ⊓ Filter.atBot = ⊥
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_of_contains_filter : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {f : α → β → Bool} {k : α},
  (Std.ExtHashMap.filter f m).contains k = true → m.contains k = true
-- Mathlib.LinearAlgebra.Projection
/-- **Alias** of `LinearMap.surjective_comp_projectionOnto`. -/
LinearMap.surjective_comp_linearProjOfIsCompl : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {p q : Submodule R E}
  {M : Type u_6} [inst_3 : AddCommMonoid M] (h : IsCompl p q) [inst_4 : Module R M],
  Function.Surjective (p.projectionOnto q h).comp
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat_i₀ : ∀ (r : ℤ) (pq : ℕ × ℕ) (hr : 2 ≤ r),
  CategoryTheory.Abelian.SpectralObject.coreE₂CohomologicalNat.i₀ r pq hr = WithBotTop.coe (↑pq.2 - r + 2)
-- Mathlib.Order.RelIso.Basic
/-- Surjective relation embeddings are equivalent to relation isomorphisms.  -/
RelIso.embeddingSurjectiveEquivIso : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → { f // Function.Surjective ⇑f } ≃ (r ≃r s)
-- Mathlib.AlgebraicGeometry.AffineScheme
AlgebraicGeometry.Scheme.zeroLocus_iInf : ∀ {X : AlgebraicGeometry.Scheme} {U : X.Opens} {ι : Type u_1} (I : ι → Ideal ↑(X.presheaf.obj (Opposite.op U)))
  [Finite ι], X.zeroLocus ↑(⨅ i, I i) = (⋃ i, X.zeroLocus ↑(I i)) ∪ (↑U)ᶜ
-- Mathlib.Analysis.Normed.Module.TransferInstance
/-- Transfer a `SeminormedCommGroup` across an `Equiv`  -/
Equiv.seminormedCommGroup : {α : Type u_1} → {β : Type u_2} → [SeminormedCommGroup β] → α ≃ β → SeminormedCommGroup α
-- Mathlib.Order.Interval.Set.Basic
Set.nonempty_Ioi : ∀ {α : Type u_1} [inst : Preorder α] {a : α} [NoMaxOrder α], (Set.Ioi a).Nonempty
-- Mathlib.RingTheory.Bialgebra.MonoidAlgebra
MonoidAlgebra.mapDomainBialgHomMulEquiv_symm_apply : ∀ {R : Type u_1} {G : Type u_5} {H : Type u_6} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : CommGroup G]
  [inst_3 : CommGroup H] (a : WithConv (MonoidAlgebra R G →ₐc[R] MonoidAlgebra R H)),
  MonoidAlgebra.mapDomainBialgHomMulEquiv.symm a = MonoidAlgebra.mapDomainOfBialgHom a.ofConv
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.eq_normEq0_cert : ℕ → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Lean.Grind.CommRing.Poly → Bool
-- Mathlib.GroupTheory.OreLocalization.Basic
/-- A characterization lemma for the vector addition on the Ore localization,
allowing for a choice of Ore minuend and Ore subtrahend.  -/
AddOreLocalization.oreSub_vadd_char : ∀ {R : Type u_1} [inst : AddMonoid R] {S : AddSubmonoid R} [inst_1 : AddOreLocalization.AddOreSet S] {X : Type u_2}
  [inst_2 : AddAction R X] (r₁ : R) (r₂ : X) (s₁ s₂ : ↥S) (r' : R) (s' : ↥S),
  ↑s' + r₁ = r' + ↑s₂ → (r₁ -ₒ s₁) +ᵥ r₂ -ₒ s₂ = (r' +ᵥ r₂) -ₒ (s' + s₁)
-- Mathlib.Order.UpperLower.Closure
upperClosure_eq : ∀ {α : Type u_1} [inst : Preorder α] {s : Set α}, ↑(upperClosure s) = s ↔ IsUpperSet s
-- Init.Grind.Ring.CommSolver
cond.eq_2 : ∀ {α : Sort u} (x y : α), (bif false then x else y) = y
-- Mathlib.Topology.Order.Basic
IsUpperSet.isOpen : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [WellFoundedGT α] {s : Set α},
  IsUpperSet s → IsOpen s
-- Mathlib.Analysis.Calculus.Deriv.Mul
hasDerivAt_mul_const : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {x : 𝕜} (c : 𝕜), HasDerivAt (fun x => x * c) c x
-- Mathlib.Topology.Compactness.Lindelof
/-- A compact space `X` is Lindelöf.  -/
instLindelofSpaceOfCompactSpace : ∀ {X : Type u} [inst : TopologicalSpace X] [CompactSpace X], LindelofSpace X
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.zpowers_eq : ∀ {R : Type u_4} [inst : CommRing R] [IsDomain R] {k : ℕ} [NeZero k] {ζ : Rˣ},
  IsPrimitiveRoot ζ k → Subgroup.zpowers ζ = rootsOfUnity k R
-- Mathlib.SetTheory.Cardinal.Aleph
Cardinal.countable_iff_lt_aleph_one : ∀ {α : Type u_1} (s : Set α), s.Countable ↔ Cardinal.mk ↑s < Cardinal.aleph 1
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToIntInfo
Lean.Meta.Grind.Arith.Cutsat.ToIntThms.mk.inj : ∀ {c? c_ww? c_wl? c_wr? c?_1 c_ww?_1 c_wl?_1 c_wr?_1 : Option Lean.Expr},
  { c? := c?, c_ww? := c_ww?, c_wl? := c_wl?, c_wr? := c_wr? } =
      { c? := c?_1, c_ww? := c_ww?_1, c_wl? := c_wl?_1, c_wr? := c_wr?_1 } →
    c? = c?_1 ∧ c_ww? = c_ww?_1 ∧ c_wl? = c_wl?_1 ∧ c_wr? = c_wr?_1
-- Mathlib.LinearAlgebra.CliffordAlgebra.Basic
/-- See note [partially-applied ext lemmas].  -/
CliffordAlgebra.hom_ext : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  {Q : QuadraticForm R M} {A : Type u_4} [inst_3 : Semiring A] [inst_4 : Algebra R A] {f g : CliffordAlgebra Q →ₐ[R] A},
  f.toLinearMap ∘ₗ CliffordAlgebra.ι Q = g.toLinearMap ∘ₗ CliffordAlgebra.ι Q → f = g
-- Mathlib.CategoryTheory.Category.Cat.CartesianClosed
CategoryTheory.curryingIso_inv_toFunctor_obj_obj_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] (F : CategoryTheory.Functor (C × D) E) (X : C) {X_1 Y : D}
  (g : X_1 ⟶ Y),
  ((CategoryTheory.curryingIso.inv.toFunctor.obj F).obj X).map g =
    F.map (CategoryTheory.Prod.mkHom (CategoryTheory.CategoryStruct.id X) g)
-- Mathlib.Algebra.Polynomial.Laurent
LaurentPolynomial.algebraMap_eq_toLaurent : ∀ {R : Type u_1} [inst : CommSemiring R] (f : Polynomial R),
  (algebraMap (Polynomial R) (LaurentPolynomial R)) f = Polynomial.toLaurent f
-- Mathlib.ModelTheory.Algebra.Field.Basic
FirstOrder.Field.FieldAxiom.toProp.eq_9 : ∀ (K : Type u_2) [inst : Add K] [inst_1 : Mul K] [inst_2 : Neg K] [inst_3 : Zero K] [inst_4 : One K],
  FirstOrder.Field.FieldAxiom.toProp K FirstOrder.Field.FieldAxiom.existsPairNE = ∃ x y, x ≠ y
-- Mathlib.Data.Set.Basic
Set.inter_union_distrib_right : ∀ {α : Type u} (s t u : Set α), s ∩ t ∪ u = (s ∪ u) ∩ (t ∪ u)
-- Mathlib.Topology.Constructions
nhds_subtype : ∀ {X : Type u} [inst : TopologicalSpace X] (s : Set X) (x : { x // x ∈ s }), nhds x = Filter.comap Subtype.val (nhds ↑x)
-- Mathlib.Data.Nat.Choose.Basic
Nat.choose_mono : ∀ (b : ℕ), Monotone fun a => a.choose b
-- Mathlib.Order.CompleteLattice.Lemmas
iSup_inf_le_iSup_inf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : CompleteLattice α] (f : ι → α) (a : α), ⨆ i, f i ⊓ a ≤ (⨆ i, f i) ⊓ a
-- Mathlib.Order.Category.Preord
Preord.ext : ∀ {X Y : Preord} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Algebra.RingQuot
RingQuot.Rel.sub_right : ∀ {R : Type uR} [inst : Ring R] {r : R → R → Prop} ⦃a b c : R⦄, RingQuot.Rel r b c → RingQuot.Rel r (a - b) (a - c)
-- Mathlib.Topology.Sheaves.Flasque
CategoryTheory.Category.toCategoryStruct.hcongr_2 : ∀ (obj obj' : Type u),
  obj = obj' →
    ∀ (self : CategoryTheory.Category.{v, u} obj) (self' : CategoryTheory.Category.{v, u} obj'),
      self ≍ self' → self.toCategoryStruct ≍ self'.toCategoryStruct
-- Lean.Expr
/-- Does the expression contain level (aka universe) or expression metavariables?
This is a constant time operation.
 -/
Lean.Expr.hasMVar : Lean.Expr → Bool
-- Mathlib.Geometry.Manifold.MFDeriv.FDeriv
/-- **Alias** of the forward direction of `mdifferentiableOn_iff_differentiableOn`.

---

For maps between vector spaces, `MDifferentiableOn` and `DifferentiableOn` coincide  -/
MDifferentiableOn.differentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {E' : Type u_3} [inst_3 : NormedAddCommGroup E'] [inst_4 : NormedSpace 𝕜 E'] {f : E → E'}
  {s : Set E}, MDiff[s] f → DifferentiableOn 𝕜 f s
-- Mathlib.Analysis.SpecialFunctions.Pow.NNReal
NNReal.rpow_le_rpow_of_exponent_ge : ∀ {x : NNReal} {y z : ℝ}, 0 < x → x ≤ 1 → z ≤ y → x ^ y ≤ x ^ z
-- Mathlib.Analysis.Complex.Hadamard
Complex.HadamardThreeLines.sSupNormIm.eq_1 : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] (f : ℂ → E) (x : ℝ),
  Complex.HadamardThreeLines.sSupNormIm f x = sSup (norm ∘ f '' Complex.re ⁻¹' {x})
-- Mathlib.Analysis.Convex.Between
wbtw_self_iff : ∀ (R : Type u_1) {V : Type u_2} {P : Type u_4} [inst : Ring R] [inst_1 : PartialOrder R] [inst_2 : AddCommGroup V]
  [inst_3 : Module R V] [inst_4 : AddTorsor V P] [IsOrderedRing R] {x y : P}, Wbtw R x y x ↔ y = x
-- Init.Data.UInt.Bitwise
UInt64.xor_not : ∀ {a b : UInt64}, a ^^^ ~~~b = ~~~(a ^^^ b)
-- Init.Data.String.Lemmas.Pattern.Find.Pred
String.Slice.contains_prop_eq : ∀ {p : Char → Prop} [inst : DecidablePred p] {s : String.Slice}, s.contains p = s.copy.toList.any fun b => decide (p b)
-- Mathlib.Data.Part
Part.getOrElse_of_dom : ∀ {α : Type u_1} (a : Part α) (h : a.Dom) [inst : Decidable a.Dom] (d : α), a.getOrElse d = a.get h
-- Mathlib.CategoryTheory.Adjunction.Quadruple
/-- For an adjoint quadruple `L ⊣ F ⊣ G ⊣ R` where `F` (and hence also `R`) is fully faithful, all
components of the natural transformation `G ⟶ L` are epimorphisms iff all components of the natural
transformation `F ⟶ R` are monomorphisms.  -/
CategoryTheory.Adjunction.Quadruple.epi_leftTriple_rightToLeft_app_iff_mono_rightTriple_leftToRight_app : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {L : CategoryTheory.Functor C D} {F : CategoryTheory.Functor D C} {G : CategoryTheory.Functor C D}
  {R : CategoryTheory.Functor D C} (q : CategoryTheory.Adjunction.Quadruple L F G R) [inst_2 : F.Full]
  [inst_3 : F.Faithful],
  (∀ (X : C), CategoryTheory.Epi (q.leftTriple.rightToLeft.app X)) ↔
    ∀ (X : D), CategoryTheory.Mono (q.rightTriple.leftToRight.app X)
-- Init.Data.List.Attach
List.tail_attachWith : ∀ {α : Type u_1} {P : α → Prop} {xs : List α} {H : ∀ a ∈ xs, P a}, (xs.attachWith P H).tail = xs.tail.attachWith P ⋯
-- Lean.Data.Lsp.Extra
Lean.Lsp.instFromJsonLeanModule.fromJson : Lean.Json → Except String Lean.Lsp.LeanModule
-- Lean.Meta.Tactic.Grind.Types
/-- Inactive global theorems. As we internalize terms, we activate theorems as we find their symbols.
Local theorem provided by users are added directly into `newThms`.
 -/
Lean.Meta.Grind.EMatch.State.thmMap : Lean.Meta.Grind.EMatch.State → Lean.Meta.Grind.EMatchTheoremsArray
-- Mathlib.Topology.Inseparable
SeparationQuotient.continuousWithinAt_lift : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {x : X} {f : X → Y}
  {hf : ∀ (x y : X), Inseparable x y → f x = f y} {s : Set (SeparationQuotient X)},
  ContinuousWithinAt (SeparationQuotient.lift f hf) s (SeparationQuotient.mk x) ↔
    ContinuousWithinAt f (SeparationQuotient.mk ⁻¹' s) x
-- Std.Time.Date.Basic
Std.Time.instHAddOffsetOffset_3 : HAdd Std.Time.Nanosecond.Offset Std.Time.Hour.Offset Std.Time.Nanosecond.Offset
-- Mathlib.RepresentationTheory.Homological.GroupHomology.LowDegree
groupHomology.cyclesIso₀_inv_comp_iCycles_apply : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] (A : Rep.{u, u, u} k G) (x : ↑A),
  (CategoryTheory.ConcreteCategory.hom (groupHomology.iCycles A 0))
      ((CategoryTheory.ConcreteCategory.hom (groupHomology.cyclesIso₀ A).inv) x) =
    (CategoryTheory.ConcreteCategory.hom (groupHomology.chainsIso₀ A).inv) x