mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.Strict.Pseudofunctor
CategoryTheory.Pseudofunctor.mapComp'_comp_id_hom_app : ∀ {B : Type u_1} [inst : CategoryTheory.Bicategory B] [inst_1 : CategoryTheory.Bicategory.Strict B]
  (F : CategoryTheory.Pseudofunctor B CategoryTheory.Cat) {b₀ b₁ : B} (f : b₀ ⟶ b₁) (X : ↑(F.obj b₀)),
  (F.mapComp' f (CategoryTheory.CategoryStruct.id b₁) f ⋯).hom.toNatTrans.app X =
    (F.mapId b₁).inv.toNatTrans.app ((F.map f).toFunctor.obj X)
-- Mathlib.Tactic.Explode.Datatypes
/-- Find a row where `Entry.expr` == `e`.  -/
Mathlib.Explode.Entries.find? : Mathlib.Explode.Entries → Lean.Expr → Option Mathlib.Explode.Entry
-- Batteries.Data.BitVec.Lemmas
BitVec.getElem_ofFnLE : ∀ {n : ℕ} (f : Fin n → Bool) (i : ℕ) (h : i < n), (BitVec.ofFnLE f)[i] = f ⟨i, h⟩
-- Mathlib.Computability.TuringMachine.Config
/-- `id` is the identity function: `id v = v`.  -/
Turing.ToPartrec.Code.id : Turing.ToPartrec.Code
-- Std.Tactic.BVDecide.LRAT.Internal.CNF
Std.Tactic.BVDecide.LRAT.Internal.Clause.eval.eq_1 : ∀ {α : Type u_1} {β : Type u_2} [inst : Std.Tactic.BVDecide.LRAT.Internal.Clause α β] (a : α → Bool) (c : β),
  Std.Tactic.BVDecide.LRAT.Internal.Clause.eval a c =
    List.any (Std.Tactic.BVDecide.LRAT.Internal.Clause.toList c) fun l =>
      decide (Std.Tactic.BVDecide.LRAT.Internal.Entails.eval a l)
-- Lean.Elab.PreDefinition.WF.Preprocess
Lean.Elab.WF.wfPreprocessSimpExtension : Lean.Meta.SimpExtension
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Over
CategoryTheory.Over.leftUnitor_inv_left_fst_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {X : C}
  (Y : CategoryTheory.Over X) {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Over.Hom.left (CategoryTheory.MonoidalCategoryStruct.leftUnitor Y).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.id X) Y.hom) h) =
    CategoryTheory.CategoryStruct.comp Y.hom h
-- Mathlib.Data.Quot
Quotient.eq : ∀ {α : Sort u_1} {r : Setoid α} {x y : α}, ⟦x⟧ = ⟦y⟧ ↔ r x y
-- Init.Data.List.Basic
List.appendTR.eq_1 : ∀ {α : Type u} (as bs : List α), as.appendTR bs = as.reverse.reverseAux bs
-- Lean.Elab.Command
Lean.Elab.Command.instMonadQuotationCommandElabM : Lean.MonadQuotation Lean.Elab.Command.CommandElabM
-- Mathlib.Analysis.Normed.Operator.Compact.Basic
IsCompactOperator.add : ∀ {M₁ : Type u_3} {M₂ : Type u_4} [inst : TopologicalSpace M₁] [inst_1 : AddCommMonoid M₁]
  [inst_2 : TopologicalSpace M₂] [inst_3 : AddCommMonoid M₂] [ContinuousAdd M₂] {f g : M₁ → M₂},
  IsCompactOperator f → IsCompactOperator g → IsCompactOperator (f + g)
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul
Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.instLawfulVecOperatorBinaryRefVecBlast : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α],
  Std.Sat.AIG.LawfulVecOperator α Std.Sat.AIG.BinaryRefVec fun {len} =>
    Std.Tactic.BVDecide.BVExpr.bitblast.blastMul.blast
-- Mathlib.Tactic.NormNum.Result
/-- Untyped version of `Result.isNegNat`.  -/
Mathlib.Meta.NormNum.Result'.isNegNat : Lean.Expr → Lean.Expr → Lean.Expr → Mathlib.Meta.NormNum.Result'
-- Mathlib.Algebra.Polynomial.Eval.Defs
Polynomial.eval_mul_C_of_commute : ∀ {R : Type u} {a : R} [inst : Semiring R] {p : Polynomial R} {x : R},
  Commute a x → Polynomial.eval x (p * Polynomial.C a) = Polynomial.eval x p * a
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.getLastD.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → α → Sort u_2) (a : α) (as : List α) (x : α) (h_1 : (a₀ : α) → motive [] a₀)
  (h_2 : (a : α) → (as : List α) → (x : α) → motive (a :: as) x),
  (match a :: as, x with
    | [], a₀ => h_1 a₀
    | a :: as, x => h_2 a as x) =
    h_2 a as x
-- Mathlib.Order.Category.Semilat
SemilatInfCat.Iso.mk_inv_toFun : ∀ {α β : SemilatInfCat} (e : α.X ≃o β.X) (a : β.X), (SemilatInfCat.Iso.mk e).inv a = e.symm a
-- Mathlib.Analysis.Meromorphic.NormalForm
/-- If `f` is meromorphic on `U`, convert `f` to normal form on `U` by changing its
values along a discrete subset within `U`. Otherwise, returns the 0 function.
 -/
toMeromorphicNFOn : {𝕜 : Type u_1} →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} → [inst_1 : NormedAddCommGroup E] → [NormedSpace 𝕜 E] → (𝕜 → E) → Set 𝕜 → 𝕜 → E
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.IsPeriodicPt.minimalPeriod_pos : ∀ {α : Type u_1} {f : α → α} {x : α} {n : ℕ}, 0 < n → Function.IsPeriodicPt f n x → 0 < Function.minimalPeriod f x
-- Mathlib.Topology.MetricSpace.Pseudo.Defs
/-- A constant size neighborhood of the diagonal is an entourage.  -/
Metric.dist_mem_uniformity : ∀ {α : Type u} [inst : PseudoMetricSpace α] {ε : ℝ}, 0 < ε → {p | dist p.1 p.2 < ε} ∈ uniformity α
-- Mathlib.Data.Set.Sups
Set.infs_empty : ∀ {α : Type u_2} [inst : SemilatticeInf α] {s : Set α}, s ⊼ ∅ = ∅
-- Mathlib.Order.Hom.Basic
OrderIso.map_inf : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeInf α] [inst_1 : SemilatticeInf β] (f : α ≃o β) (x y : α),
  f (x ⊓ y) = f x ⊓ f y
-- Mathlib.Algebra.FiveLemma
/-- A special case of the five lemma in terms of additive groups.
For a diagram explaining the variables, see the module docstring.  -/
AddMonoidHom.bijective_of_surjective_of_bijective_of_right_exact : ∀ {M₁ : Type u_1} {M₂ : Type u_2} {M₃ : Type u_3} {N₁ : Type u_6} {N₂ : Type u_7} {N₃ : Type u_8} [inst : AddGroup M₁]
  [inst_1 : AddGroup M₂] [inst_2 : AddGroup M₃] [inst_3 : AddGroup N₁] [inst_4 : AddGroup N₂] [inst_5 : AddGroup N₃]
  (f₁ : M₁ →+ M₂) (f₂ : M₂ →+ M₃) (g₁ : N₁ →+ N₂) (g₂ : N₂ →+ N₃) (i₁ : M₁ →+ N₁) (i₂ : M₂ →+ N₂) (i₃ : M₃ →+ N₃),
  g₁.comp i₁ = i₂.comp f₁ →
    g₂.comp i₂ = i₃.comp f₂ →
      Function.Exact ⇑f₁ ⇑f₂ →
        Function.Exact ⇑g₁ ⇑g₂ →
          Function.Surjective ⇑i₁ →
            Function.Bijective ⇑i₂ → Function.Surjective ⇑f₂ → Function.Surjective ⇑g₂ → Function.Bijective ⇑i₃
-- Mathlib.Analysis.Normed.Lp.WithLp
LinearEquiv.withLpCongr_trans : ∀ (p : ENNReal) {K : Type u_1} {K' : Type u_2} {K'' : Type u_3} {V : Type u_4} {V' : Type u_5} {V'' : Type u_6}
  [inst : Semiring K] [inst_1 : Semiring K'] [inst_2 : Semiring K''] {σ : K →+* K'} {σ' : K' →+* K}
  [inst_3 : RingHomInvPair σ σ'] [inst_4 : RingHomInvPair σ' σ] {τ : K' →+* K''} {τ' : K'' →+* K'}
  [inst_5 : RingHomInvPair τ τ'] [inst_6 : RingHomInvPair τ' τ] {ρ : K →+* K''} {ρ' : K'' →+* K}
  [inst_7 : RingHomInvPair ρ ρ'] [inst_8 : RingHomInvPair ρ' ρ] [inst_9 : RingHomCompTriple σ τ ρ]
  [inst_10 : RingHomCompTriple τ' σ' ρ'] [inst_11 : AddCommGroup V] [inst_12 : Module K V] [inst_13 : AddCommGroup V']
  [inst_14 : Module K' V'] [inst_15 : AddCommGroup V''] [inst_16 : Module K'' V''] (f : V ≃ₛₗ[σ] V')
  (g : V' ≃ₛₗ[τ] V''),
  LinearEquiv.withLpCongr p (f.trans g) = (LinearEquiv.withLpCongr p f).trans (LinearEquiv.withLpCongr p g)
-- Init.Data.Sum.Lemmas
Sum.isLeft_eq_false : ∀ {α : Type u_1} {β : Type u_2} {x : α ⊕ β}, x.isLeft = false ↔ x.isRight = true
-- Mathlib.Analysis.Normed.Module.Alternating.Basic
/-- If one controls the norm of every `f x`, then one controls the norm of `f`.  -/
ContinuousAlternatingMap.opNorm_le_bound : ∀ {𝕜 : Type u} {E : Type wE} {F : Type wF} {ι : Type v} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : SeminormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : SeminormedAddCommGroup F]
  [inst_4 : NormedSpace 𝕜 F] [inst_5 : Fintype ι] (f : E [⋀^ι]→L[𝕜] F) {M : ℝ},
  0 ≤ M → (∀ (m : ι → E), ‖f m‖ ≤ M * ∏ i, ‖m i‖) → ‖f‖ ≤ M
-- Mathlib.Topology.Category.Stonean.Basic
CompHaus.lift_lifts : ∀ {X Y : CompHaus} {Z : Stonean} (e : Z.compHaus ⟶ Y) (f : X ⟶ Y) [inst : CategoryTheory.Epi f],
  CategoryTheory.CategoryStruct.comp (CompHaus.lift e f) f = e
-- Mathlib.AlgebraicGeometry.ValuativeCriterion
AlgebraicGeometry.ValuativeCriterion.uniqueness : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y},
  AlgebraicGeometry.ValuativeCriterion f → AlgebraicGeometry.ValuativeCriterion.Uniqueness f
-- Mathlib.RingTheory.Radical.Basic
UniqueFactorizationMonoid.radical_eq_iff_primeFactors_eq : ∀ {M : Type u_1} [inst : CommMonoidWithZero M] [inst_1 : NormalizationMonoid M] [inst_2 : UniqueFactorizationMonoid M]
  {a b : M},
  UniqueFactorizationMonoid.radical a = UniqueFactorizationMonoid.radical b ↔
    UniqueFactorizationMonoid.primeFactors a = UniqueFactorizationMonoid.primeFactors b
-- Mathlib.GroupTheory.GroupAction.CardCommute
_private.Mathlib.GroupTheory.GroupAction.CardCommute.0.MulAction.termΩ : Lean.ParserDescr
-- Mathlib.Order.Interval.Set.Disjoint
iUnion_Iic_eq_Iio_iSup : ∀ {ι : Sort u} {R : Type u_1} [inst : CompleteLinearOrder R] {f : ι → R},
  ⨆ i, f i ∉ Set.range f → ⋃ i, Set.Iic (f i) = Set.Iio (⨆ i, f i)
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Mon.ofVar : Lean.Grind.CommRing.Var → Lean.Grind.CommRing.Mon
-- Mathlib.SetTheory.Ordinal.Notation
ONote.zero_add : ∀ (o : ONote), 0 + o = o
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.mem_diff_iff : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₁ \ m₂ ↔ k ∈ m₁ ∧ k ∉ m₂
-- Mathlib.Algebra.Module.Congruence.Defs
VAddCon.mk : {S : Type u_2} →
  {M : Type u_3} →
    [inst : VAdd S M] →
      (toSetoid : Setoid M) → (∀ (s : S) {x y : M}, toSetoid x y → toSetoid (s +ᵥ x) (s +ᵥ y)) → VAddCon S M
-- Mathlib.SetTheory.Ordinal.Exponential
Ordinal.div_two_opow_log : ∀ {o : Ordinal.{u_1}}, o ≠ 0 → o / 2 ^ Ordinal.log 2 o = 1
-- Mathlib.Data.Nat.Bitwise
Nat.testBit_land : ∀ (m n k : ℕ), (m &&& n).testBit k = (m.testBit k && n.testBit k)
-- Mathlib.Topology.Algebra.WithZeroTopology
/-- If `γ` is an invertible element of a linearly ordered group with zero element adjoined, then
`{γ}` is a neighbourhood of `γ`.  -/
WithZeroTopology.singleton_mem_nhds_of_units : ∀ {Γ₀ : Type u_2} [inst : LinearOrderedCommGroupWithZero Γ₀] (γ : Γ₀ˣ), {↑γ} ∈ nhds ↑γ
-- Mathlib.LinearAlgebra.Dimension.Constructions
/-- The dimension of a quotient is bounded by the dimension of the ambient space.  -/
Submodule.finrank_quotient_le : ∀ {R : Type u} {M : Type v} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] [StrongRankCondition R]
  [Module.Finite R M] (s : Submodule R M), Module.finrank R (M ⧸ s) ≤ Module.finrank R M
-- Mathlib.CategoryTheory.Limits.Shapes.SplitCoequalizer
CategoryTheory.IsSplitCoequalizer.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f g : X ⟶ Y} {Z : C} {π : Y ⟶ Z} [inst_1 : SizeOf C]
  (rightSection : Z ⟶ Y) (leftSection : Y ⟶ X)
  (condition :
    autoParam (CategoryTheory.CategoryStruct.comp f π = CategoryTheory.CategoryStruct.comp g π)
      CategoryTheory.IsSplitCoequalizer.condition._autoParam)
  (rightSection_π :
    autoParam (CategoryTheory.CategoryStruct.comp rightSection π = CategoryTheory.CategoryStruct.id Z)
      CategoryTheory.IsSplitCoequalizer.rightSection_π._autoParam)
  (leftSection_bottom :
    autoParam (CategoryTheory.CategoryStruct.comp leftSection g = CategoryTheory.CategoryStruct.id Y)
      CategoryTheory.IsSplitCoequalizer.leftSection_bottom._autoParam)
  (leftSection_top :
    autoParam (CategoryTheory.CategoryStruct.comp leftSection f = CategoryTheory.CategoryStruct.comp π rightSection)
      CategoryTheory.IsSplitCoequalizer.leftSection_top._autoParam),
  sizeOf
      { rightSection := rightSection, leftSection := leftSection, condition := condition,
        rightSection_π := rightSection_π, leftSection_bottom := leftSection_bottom,
        leftSection_top := leftSection_top } =
    1 + sizeOf rightSection + sizeOf leftSection + sizeOf condition + sizeOf rightSection_π +
        sizeOf leftSection_bottom +
      sizeOf leftSection_top
-- Std.Data.DTreeMap.Internal.Zipper
Std.DTreeMap.Internal.Const.toList_rco : ∀ {α : Type u} {β : Type v} [inst : Ord α] [Std.TransOrd α] (t : Std.DTreeMap.Internal.Impl α fun x => β),
  t.Ordered →
    ∀ (lowerBound upperBound : α),
      Std.Slice.toList (Std.Rco.Sliceable.mkSlice t lowerBound...upperBound) =
        List.filter (fun e => decide ((compare e.1 lowerBound).isGE = true ∧ (compare e.1 upperBound).isLT = true))
          (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.QExpansion
/-- This is a version of `summableLocallyUniformlyOn_iteratedDerivWithin_smul_cexp` for level one
and q-expansion coefficients all `1`.  -/
summableLocallyUniformlyOn_iteratedDerivWithin_cexp : ∀ (k : ℕ),
  SummableLocallyUniformlyOn
    (fun n =>
      iteratedDerivWithin k (fun z => Complex.exp (2 * ↑Real.pi * Complex.I * z) ^ n) UpperHalfPlane.upperHalfPlaneSet)
    UpperHalfPlane.upperHalfPlaneSet
-- Mathlib.Tactic.Module
Mathlib.Tactic.Module.NF.sub_eq_eval : ∀ {R : Type u_2} {M : Type u_3} {R₁ : Type u_4} {R₂ : Type u_5} {S₁ : Type u_6} {S₂ : Type u_7} [inst : AddCommGroup M]
  [inst_1 : Ring R] [inst_2 : Module R M] [inst_3 : Semiring R₁] [inst_4 : Module R₁ M] [inst_5 : Semiring R₂]
  [inst_6 : Module R₂ M] [inst_7 : Semiring S₁] [inst_8 : Module S₁ M] [inst_9 : Semiring S₂] [inst_10 : Module S₂ M]
  {l₁ l₂ l : Mathlib.Tactic.Module.NF R M} {l₁' : Mathlib.Tactic.Module.NF R₁ M} {l₂' : Mathlib.Tactic.Module.NF R₂ M}
  {l₁'' : Mathlib.Tactic.Module.NF S₁ M} {l₂'' : Mathlib.Tactic.Module.NF S₂ M} {x₁ x₂ : M},
  x₁ = l₁''.eval →
    x₂ = l₂''.eval →
      l₁'.eval = l₁''.eval →
        l₂'.eval = l₂''.eval → l₁.eval = l₁'.eval → l₂.eval = l₂'.eval → l₁.eval - l₂.eval = l.eval → x₁ - x₂ = l.eval
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- Given a continuous group homomorphism `φ : H →ₜ* G`, precomposition with `φ` defines a
continuous intertwining map `π.coind₁.restrict φ →ⁱL (π.restrict φ).coind₁`.  -/
ContRepresentation.coind₁Res : {R : Type u_1} →
  {V : Type u_3} →
    [inst : Ring R] →
      [inst_1 : AddCommGroup V] →
        [inst_2 : TopologicalSpace V] →
          [inst_3 : IsTopologicalAddGroup V] →
            [inst_4 : Module R V] →
              {G : Type u_7} →
                {H : Type u_8} →
                  [inst_5 : Group G] →
                    [inst_6 : TopologicalSpace G] →
                      [inst_7 : TopologicalSpace R] →
                        [inst_8 : ContinuousSMul R V] →
                          [inst_9 : Group H] →
                            [inst_10 : TopologicalSpace H] →
                              [inst_11 : IsTopologicalGroup G] →
                                [inst_12 : IsTopologicalGroup H] →
                                  (φ : H →ₜ* G) →
                                    (π : ContRepresentation R G V) →
                                      ContIntertwiningMap (π.coind₁.restrict ↑φ) (π.restrict ↑φ).coind₁
-- Mathlib.Topology.MetricSpace.GromovHausdorff
/-- Map any nonempty compact type to `GHSpace`  -/
GromovHausdorff.toGHSpace : (X : Type u) → [inst : MetricSpace X] → [CompactSpace X] → [Nonempty X] → GromovHausdorff.GHSpace
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.IsImage.restr_source : ∀ {α : Type u_1} {β : Type u_2} {e : PartialEquiv α β} {s : Set α} {t : Set β} (h : e.IsImage s t),
  h.restr.source = e.source ∩ s
-- Mathlib.Algebra.Group.Subgroup.Defs
Subgroup.inclusion_injective : ∀ {G : Type u_1} [inst : Group G] {H K : Subgroup G} (h : H ≤ K), Function.Injective ⇑(Subgroup.inclusion h)
-- Mathlib.Geometry.RingedSpace.Stalks
/-- For an open embedding `f : U ⟶ X` and a point `x : U`, we get an isomorphism between the stalk
of `X` at `f x` and the stalk of the restriction of `X` along `f` at `x`.
 -/
AlgebraicGeometry.PresheafedSpace.restrictStalkIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasColimits C] →
      {U : TopCat} →
        (X : AlgebraicGeometry.PresheafedSpace C) →
          {f : U ⟶ ↑X} →
            (h : Topology.IsOpenEmbedding ⇑(CategoryTheory.ConcreteCategory.hom f)) →
              (x : ↑U) → (X.restrict h).presheaf.stalk x ≅ X.presheaf.stalk ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.MeasureTheory.Function.LpSpace.ContinuousFunctions
/-- By definition, the elements of `Lp.boundedContinuousFunction E p μ` are the elements of
`Lp E p μ` which contain a bounded continuous representative.  -/
MeasureTheory.Lp.mem_boundedContinuousFunction_iff : ∀ {α : Type u_1} {E : Type u_2} {m0 : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : TopologicalSpace α] [inst_1 : BorelSpace α] [inst_2 : NormedAddCommGroup E]
  [inst_3 : SecondCountableTopologyEither α E] {f : ↥(MeasureTheory.Lp E p μ)},
  f ∈ MeasureTheory.Lp.boundedContinuousFunction E p μ ↔ ∃ f₀, ContinuousMap.toAEEqFun μ f₀.toContinuousMap = ↑f
-- Std.Data.TreeMap.Raw.Basic
/-- Checks if a mapping for the given key exists and returns the key if it does, otherwise `fallback`.
If a mapping exists the result is guaranteed to be pointer equal to the key in the map.
 -/
Std.TreeMap.Raw.getKeyD : {α : Type u} → {β : Type v} → {cmp : α → α → Ordering} → Std.TreeMap.Raw α β cmp → α → α → α
-- Mathlib.Data.Set.Lattice
Set.iUnion_false : ∀ {α : Type u_1} {s : False → Set α}, Set.iUnion s = ∅
-- Mathlib.Data.Set.Card
/-- Every set is either empty, infinite, or can have its `encard` reduced by a removal. Intended
for well-founded induction on the value of `encard`.  -/
Set.eq_empty_or_encard_eq_top_or_encard_sdiff_singleton_lt : ∀ {α : Type u_1} (s : Set α), s = ∅ ∨ s.encard = ⊤ ∨ ∃ a ∈ s, (s \ {a}).encard < s.encard
-- Init.Omega.IntList
/-- A type synonym for `List Int`, used by `omega` for dense representation of coefficients.

We define algebraic operations,
interpreting `List Int` as a finitely supported function `Nat → Int`.
 -/
Lean.Omega.IntList : Type
-- Init.Data.List.Lemmas
List.reverse_eq_iff : ∀ {α : Type u_1} {as bs : List α}, as.reverse = bs ↔ as = bs.reverse
-- Mathlib.CategoryTheory.Sums.Associator
/-- Further characterizing the composition of the inverse of the associator and the right
inclusion.  -/
CategoryTheory.sum.inlCompInrCompInverseAssociator : (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] →
            (CategoryTheory.Sum.inl_ D E).comp
                ((CategoryTheory.Sum.inr_ C (D ⊕ E)).comp (CategoryTheory.sum.inverseAssociator C D E)) ≅
              (CategoryTheory.Sum.inr_ C D).comp (CategoryTheory.Sum.inl_ (C ⊕ D) E)
-- Init.Data.Array.Lemmas
List.toArray_range' : ∀ {start size step : ℕ}, (List.range' start size step).toArray = Array.range' start size step
-- Mathlib.CategoryTheory.Adjunction.Limits
/-- auxiliary construction for `conesIso`  -/
CategoryTheory.Adjunction.conesIsoComponentInv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {F : CategoryTheory.Functor C D} →
          {G : CategoryTheory.Functor D C} →
            (F ⊣ G) →
              {J : Type u} →
                [inst_2 : CategoryTheory.Category.{v, u} J] →
                  {K : CategoryTheory.Functor J D} →
                    (X : Cᵒᵖ) →
                      ((CategoryTheory.cones J C).obj (K.comp G)).obj X →
                        (F.op.comp ((CategoryTheory.cones J D).obj K)).obj X
-- Mathlib.CategoryTheory.Functor.Derived.PointwiseLeftDerived
/-- If `L : C ⥤ D` is a localization functor for `W` and `e : F ≅ L ⋙ G` is an isomorphism,
then `e.inv` makes `G` a pointwise right Kan extension of `F` along `L` at `L.obj Y`
for any `Y : C`.  -/
CategoryTheory.Functor.isPointwiseRightKanExtensionAtOfIsoOfIsLocalization : {C : Type u₁} →
  {D : Type u₂} →
    {H : Type u₃} →
      [inst : CategoryTheory.Category.{v₁, u₁} C] →
        [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} H] →
            {F : CategoryTheory.Functor C H} →
              {L : CategoryTheory.Functor C D} →
                (W : CategoryTheory.MorphismProperty C) →
                  {G : CategoryTheory.Functor D H} →
                    (e : F ≅ L.comp G) →
                      [L.IsLocalization W] →
                        (Y : C) →
                          (CategoryTheory.Functor.RightExtension.mk G e.inv).IsPointwiseRightKanExtensionAt (L.obj Y)
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.degree_compl : ∀ {V : Type u_1} (G : SimpleGraph V) (v : V) [inst : Fintype ↑(G.neighborSet v)] [inst_1 : Fintype ↑(Gᶜ.neighborSet v)]
  [inst_2 : Fintype V], Gᶜ.degree v = Fintype.card V - 1 - G.degree v
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.DocumentSymbolResult.mk.injEq : ∀ (syms syms_1 : Array Lean.Lsp.DocumentSymbol), ({ syms := syms } = { syms := syms_1 }) = (syms = syms_1)
-- Mathlib.RingTheory.RingHomProperties
RingHom.HasFiniteProducts.and : ∀ {P Q : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  (RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => P) →
    (RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] => Q) →
      RingHom.HasFiniteProducts fun {R S} [CommRing R] [CommRing S] f => P f ∧ Q f
-- Init.Data.Vector.Lemmas
Vector.prod_push : ∀ {α : Type u_1} {n : ℕ} [inst : Mul α] [inst_1 : One α] [Std.Associative fun x1 x2 => x1 * x2]
  [Std.LawfulIdentity (fun x1 x2 => x1 * x2) 1] {xs : Vector α n} {x : α}, (xs.push x).prod = xs.prod * x
-- Mathlib.RingTheory.Regular.RegularSequence
nontrivial_quotSMulTop_of_mem_maximalIdeal : ∀ {R : Type u_7} [inst : CommRing R] [inst_1 : IsLocalRing R] (L : Type u_8) [inst_2 : AddCommGroup L]
  [inst_3 : Module R L] [Module.Finite R L] [Nontrivial L] {x : R},
  x ∈ IsLocalRing.maximalIdeal R → Nontrivial (QuotSMulTop x L)
-- Mathlib.NumberTheory.LSeries.ZMod
/-- The completed L-function of a function `ZMod 1 → ℂ` is a scalar multiple of the completed Riemann
zeta function.
 -/
ZMod.completedLFunction_modOne_eq : ∀ (Φ : ZMod 1 → ℂ) (s : ℂ), ZMod.completedLFunction Φ s = Φ 1 * completedRiemannZeta s
-- Mathlib.Algebra.Module.LinearMap.FiniteRange
LinearMap.FiniteRangeSetoid.equiv_comp : ∀ {K : Type u_1} {V : Type u_2} {V₂ : Type u_4} {V₃ : Type u_6} [inst : CommRing K] [inst_1 : AddCommGroup V]
  [inst_2 : Module K V] [inst_3 : AddCommGroup V₂] [inst_4 : Module K V₂] [inst_5 : AddCommGroup V₃]
  [inst_6 : Module K V₃] {u v : V →ₗ[K] V₂} {u' v' : V₂ →ₗ[K] V₃}, u ≈ v → u' ≈ v' → u' ∘ₗ u ≈ v' ∘ₗ v
-- Mathlib.Analysis.Real.Hyperreal
Hyperreal.isSt_iff_abs_sub_lt_delta : ∀ {x : ℝ*} {r : ℝ}, x.IsSt r ↔ ∀ (δ : ℝ), 0 < δ → |x - ↑r| < ↑δ
-- Init.Data.Int.Order
Int.min_add_left : ∀ (a b c : ℤ), min (a + b) (a + c) = a + min b c
-- Std.Sat.AIG.Basic
Std.Sat.AIG.TernaryInput.mk.inj : ∀ {α : Type} {inst : Hashable α} {inst_1 : DecidableEq α} {aig : Std.Sat.AIG α}
  {discr lhs rhs discr_1 lhs_1 rhs_1 : aig.Ref},
  { discr := discr, lhs := lhs, rhs := rhs } = { discr := discr_1, lhs := lhs_1, rhs := rhs_1 } →
    discr = discr_1 ∧ lhs = lhs_1 ∧ rhs = rhs_1
-- Mathlib.Tactic.ClickSuggestions.GRewrite
/-- The expression that is being rewritten.  -/
Mathlib.Tactic.ClickSuggestions.GrwInfo.subExpr : Mathlib.Tactic.ClickSuggestions.GrwInfo → Lean.Expr
-- Mathlib.CategoryTheory.Triangulated.Basic
CategoryTheory.Pretriangulated.Triangle.sub_hom₁ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.HasShift C ℤ]
  {T₁ T₂ : CategoryTheory.Pretriangulated.Triangle C} [inst_2 : CategoryTheory.Preadditive C]
  [inst_3 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] (f g : T₁ ⟶ T₂), (f - g).hom₁ = f.hom₁ - g.hom₁
-- Init.Data.Range.Polymorphic.UInt
UInt8.instLawfulUpwardEnumerableLT : Std.PRange.LawfulUpwardEnumerableLT UInt8
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.unop_leftUnitor : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] (X : Cᵒᵖ),
  (CategoryTheory.MonoidalCategoryStruct.leftUnitor X).unop =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (Opposite.unop X)).symm
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Point
WeierstrassCurve.Affine.nonsingularPointEquivSubtype_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} {p : W'.Point → Prop}
  (p0 : p WeierstrassCurve.Affine.Point.zero),
  (WeierstrassCurve.Affine.nonsingularPointEquivSubtype p0) ⟨WeierstrassCurve.Affine.Point.zero, p0⟩ = none