mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Opposites
CategoryTheory.Limits.limitOpIsoOpColimit_hom_comp_ι : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {J : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} J]
  (F : CategoryTheory.Functor J C) [inst_2 : CategoryTheory.Limits.HasColimit F] (j : J),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.limitOpIsoOpColimit F).hom
      (CategoryTheory.Limits.colimit.ι F j).op =
    CategoryTheory.Limits.limit.π F.op (Opposite.op j)
-- Mathlib.CategoryTheory.Limits.Shapes.FunctorToTypes
CategoryTheory.FunctorToTypes.prodMk.eq_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {F G : CategoryTheory.Functor C (Type w)} {a : C} (x : F.obj a)
  (y : G.obj a),
  CategoryTheory.FunctorToTypes.prodMk x y =
    (CategoryTheory.ConcreteCategory.hom ((CategoryTheory.FunctorToTypes.binaryProductIso F G).inv.app a)) (x, y)
-- Mathlib.Algebra.Order.Archimedean.Class
ArchimedeanOrder.eq_1 : ∀ (M : Type u_1), ArchimedeanOrder M = M
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
IsPrimitiveRoot.of_map_of_injective : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_6} [inst : CommMonoid M] [inst_1 : CommMonoid N] {k : ℕ} {ζ : M} {f : F}
  [inst_2 : FunLike F M N] [MonoidHomClass F M N], IsPrimitiveRoot (f ζ) k → Function.Injective ⇑f → IsPrimitiveRoot ζ k
-- Mathlib.Algebra.Star.StarRingHom
StarRingEquiv.invFun_eq_symm : ∀ {A : Type u_1} {B : Type u_2} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B] [inst_4 : Star A]
  [inst_5 : Star B] {e : A ≃⋆+* B}, EquivLike.inv e = ⇑e.symm
-- Mathlib.Algebra.Group.Units.Hom
map_units_inv : ∀ {M : Type u} [inst : Monoid M] {α : Type u_1} [inst_1 : DivisionMonoid α] {F : Type u_2} [inst_2 : FunLike F M α]
  [MonoidHomClass F M α] (f : F) (u : Mˣ), f ↑u⁻¹ = (f ↑u)⁻¹
-- Mathlib.Topology.ContinuousOn
IsOpenMap.continuousOn_range_of_leftInverse : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {f : α → β},
  IsOpenMap f → ∀ {finv : β → α}, Function.LeftInverse finv f → ContinuousOn finv (Set.range f)
-- Mathlib.Algebra.GroupWithZero.Associated
Associates.one_eq_mk_one : ∀ {M : Type u_1} [inst : Monoid M], 1 = Associates.mk 1
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Formula
WeierstrassCurve.Jacobian.negDblY_of_Z_eq_zero : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Jacobian R} {P : Fin 3 → R},
  W'.Equation P → P 2 = 0 → W'.negDblY P = -(P 0 ^ 2) ^ 3
-- Mathlib.MeasureTheory.Integral.CircleIntegral
circleMap_neg_radius : ∀ {r x : ℝ} {c : ℂ}, circleMap c (-r) x = circleMap c r (x + Real.pi)
-- Mathlib.Data.W.Constructions
/-- The isomorphism from the `WType` construction of lists to lists  -/
WType.toList : (γ : Type u) → WType (WType.Listβ γ) → List γ
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.get?_union_of_not_mem_right : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k : α}, k ∉ t₂ → (t₁ ∪ t₂).get? k = t₁.get? k
-- Mathlib.Algebra.Group.AddChar
/-- If `n` is a natural number, then `mulShift ψ n x = (ψ x) ^ n`.  -/
AddChar.mulShift_spec' : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : CommMonoid M] (ψ : AddChar R M) (n : ℕ) (x : R),
  (ψ.mulShift ↑n) x = ψ x ^ n
-- Mathlib.RingTheory.Spectrum.Prime.Basic
PrimeSpectrum.vanishingIdeal_union : ∀ {R : Type u} [inst : CommSemiring R] (t t' : Set (PrimeSpectrum R)),
  PrimeSpectrum.vanishingIdeal (t ∪ t') = PrimeSpectrum.vanishingIdeal t ⊓ PrimeSpectrum.vanishingIdeal t'
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.disjoint_one_right : ∀ {α : Type u_1} (f : Equiv.Perm α), f.Disjoint 1
-- Lean.Elab.Do.Legacy
/-- Given `uvars := #[a_1, ..., a_n, a_{n+1}]` construct term
```
let a_1     := x.1
let x       := x.2
let a_2     := x.1
let x       := x.2
...
let a_n     := x.1
let a_{n+1} := x.2
body
```
Special cases
- `uvars := #[]` => `body`
- `uvars := #[a]` => `let a := x; body`


We use this method when expanding the `for-in` notation.
 -/
_private.Lean.Elab.Do.Legacy.0.Lean.Elab.Term.Do.destructTuple : Array Lean.Elab.Term.Do.Var → Lean.Syntax → Lean.Syntax → Lean.MacroM Lean.Syntax
-- Mathlib.Algebra.Order.Field.Basic
div_le_one : ∀ {α : Type u_2} [inst : Semifield α] [inst_1 : PartialOrder α] [PosMulReflectLT α] {a b : α},
  0 < b → (a / b ≤ 1 ↔ a ≤ b)
-- Mathlib.Analysis.Normed.Lp.WithLp
WithLp.ofLp_bijective : ∀ (p : ENNReal) {V : Type u_4}, Function.Bijective WithLp.ofLp
-- Mathlib.Data.Fin.SuccPred
Fin.sub_castSucc_eq_castSucc_sub_of_le : ∀ {n : ℕ} {a b : Fin n}, b ≤ a → a.castSucc - b.castSucc = (a - b).castSucc
-- Mathlib.CategoryTheory.Sites.Closed
CategoryTheory.topologyOfClosureOperator_sieves : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (c : (X : C) → ClosureOperator (CategoryTheory.Sieve X))
  (hc :
    ∀ ⦃X Y : C⦄ (f : Y ⟶ X) (S : CategoryTheory.Sieve X),
      (c Y) (CategoryTheory.Sieve.pullback f S) = CategoryTheory.Sieve.pullback f ((c X) S))
  (X : C), (CategoryTheory.topologyOfClosureOperator c hc).sieves X = {S | (c X) S = ⊤}
-- Lean.Elab.MatchAltView
Lean.Elab.Term.instInhabitedMatchAltView.default : {k : Lean.SyntaxNodeKinds} → Lean.Elab.Term.MatchAltView k
-- Mathlib.MeasureTheory.MeasurableSpace.EventuallyMeasurable
/-- We say a function is `EventuallyMeasurable` with respect to a given
σ-algebra `m` and σ-filter `l` if the preimage of any measurable set is equal to some
`m`-measurable set modulo `l`.
Warning: This is not always the same as being equal to some `m`-measurable function modulo `l`.
In general it is weaker. See `Measurable.eventuallyMeasurable_of_eventuallyEq`.
*TODO*: Add lemmas about when these are equivalent.  -/
EventuallyMeasurable : {α : Type u_1} →
  MeasurableSpace α → (l : Filter α) → [CountableInterFilter l] → {β : Type u_2} → [MeasurableSpace β] → (α → β) → Prop
-- Mathlib.RingTheory.KrullDimension.Basic
Ring.krullDimLE_iff : ∀ {R : Type u_1} [inst : CommSemiring R] {n : ℕ}, Ring.KrullDimLE n R ↔ ringKrullDim R ≤ ↑n
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- Construct an isomorphism of additive monoid objects by giving an isomorphism between
the underlying objects and checking compatibility with zero and addition only in
the forward direction.  -/
CategoryTheory.AddMon.mkIso : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      {M N : CategoryTheory.AddMon C} →
        (e : M.X ≅ N.X) →
          autoParam
              (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.zero e.hom = CategoryTheory.AddMonObj.zero)
              CategoryTheory.AddMon.mkIso._auto_1 →
            autoParam
                (CategoryTheory.CategoryStruct.comp CategoryTheory.AddMonObj.add e.hom =
                  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.tensorHom e.hom e.hom)
                    CategoryTheory.AddMonObj.add)
                CategoryTheory.AddMon.mkIso._auto_3 →
              (M ≅ N)
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.isEmpty_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp}, t.keys.isEmpty = t.isEmpty
-- Mathlib.Algebra.Algebra.Subalgebra.Unitization
NonUnitalSubring.unitization.eq_1 : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : SetLike S R] [hSR : NonUnitalSubringClass S R] (s : S),
  NonUnitalSubring.unitization s = NonUnitalSubalgebra.unitization s
-- Mathlib.Algebra.Algebra.Subalgebra.Lattice
Algebra.sup_toSubsemiring : ∀ {R : Type u} {A : Type v} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Algebra R A] (S T : Subalgebra R A),
  (S ⊔ T).toSubsemiring = S.toSubsemiring ⊔ T.toSubsemiring
-- Init.Meta.Defs
Lean.Meta.ApplyNewGoals.noConfusionType : Sort v✝ → Lean.Meta.ApplyNewGoals → Lean.Meta.ApplyNewGoals → Sort v✝
-- Mathlib.CategoryTheory.Presentable.SharplyLT.Basic
/-- This is the implication (iii) → (iv) in the characterizations
of `SharplyLT κ₁ κ₂` in the docstring of this file.  -/
Cardinal.SharplyLT.exists_isCardinalFiltered_set_of_exists_cofinal : ∀ {κ₁ κ₂ : Cardinal.{w}} [inst : Fact κ₁.IsRegular] [Fact κ₂.IsRegular],
  κ₁ < κ₂ →
    (∀ (X : Type w), HasCardinalLT X κ₂ → ∃ Y, HasCardinalLT (↑Y) κ₂ ∧ IsCofinal Y) →
      ∀ {X : Type w} [inst_2 : PartialOrder X] [CategoryTheory.IsCardinalFiltered X κ₁] (A : Set X),
        HasCardinalLT (↑A) κ₂ → ∃ B, A ⊆ B ∧ CategoryTheory.IsCardinalFiltered (↑B) κ₁ ∧ HasCardinalLT (↑B) κ₂
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.AddMon.comp_hom' : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  {M N K : CategoryTheory.AddMon C} (f : M ⟶ N) (g : N ⟶ K),
  (CategoryTheory.CategoryStruct.comp f g).hom = CategoryTheory.CategoryStruct.comp f.hom g.hom
-- Lean.Message
_private.Lean.Message.0.Lean.Kernel.Exception.mkCtx : Lean.Kernel.Environment → Lean.LocalContext → Lean.Options → Lean.MessageData → Lean.MessageData
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.wfImp_interSmallerFnₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  (m₁ m₂ : Std.DHashMap.Internal.Raw₀ α β),
  Std.DHashMap.Internal.Raw.WFImp ↑m₂ → ∀ (k : α), Std.DHashMap.Internal.Raw.WFImp ↑(m₁.interSmallerFnₘ m₂ k)
-- Mathlib.LinearAlgebra.Matrix.Adjugate
Matrix.det_eq_sum_mul_adjugate_col : ∀ {n : Type v} {α : Type w} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : CommRing α] (A : Matrix n n α)
  (j : n), A.det = ∑ i, A i j * A.adjugate j i
-- Mathlib.Analysis.Convex.Extreme
instIsPartialOrderSetIsExtreme : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E], IsPartialOrder (Set E) (IsExtreme 𝕜)
-- Init.Data.BitVec.Lemmas
BitVec.extractLsb'_append_eq_right : ∀ {w w' : ℕ} {a : BitVec w} {b : BitVec w'}, BitVec.extractLsb' 0 w' (a ++ b) = b
-- Mathlib.Order.CompleteLattice.Lemmas
ULift.down_iSup : ∀ {α : Type u_1} {ι : Sort u_4} [inst : SupSet α] (f : ι → ULift.{v, u_1} α), (⨆ i, f i).down = ⨆ i, (f i).down
-- Mathlib.Algebra.BigOperators.Finprod
finsum_eq_single : ∀ {M : Type u_2} {α : Sort u_4} [inst : AddCommMonoid M] (f : α → M) (a : α),
  (∀ (x : α), x ≠ a → f x = 0) → ∑ᶠ (x : α), f x = f a
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono
/-- An auxiliary lemma to show that one can always use the simplicial identities to simplify a term
in the form `δ ≫ σ` into either an identity, or a term of the form `σ ≫ δ`. This is the crucial
special case to induct on to get an epi-mono factorization for all morphisms.  -/
_private.Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.EpiMono.0.SimplexCategoryGenRel.switch_δ_σ : ∀ {n : ℕ} (i : Fin (n + 2)) (i' : Fin (n + 3)),
  CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i') (SimplexCategoryGenRel.σ i) =
      CategoryTheory.CategoryStruct.id (SimplexCategoryGenRel.mk (n + 1)) ∨
    ∃ j j',
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i') (SimplexCategoryGenRel.σ i) =
        CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.σ j) (SimplexCategoryGenRel.δ j')
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintOptions : Type
-- Mathlib.Tactic.NormNum.Inv
/-- Helper function to synthesize a typed `CharZero α` expression given `DivisionRing α`.  -/
Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing : {u : Lean.Level} →
  {α : Q(Type u)} →
    (_i : autoParam Q(DivisionRing «$α») Mathlib.Meta.NormNum.inferCharZeroOfDivisionRing._auto_1) →
      Lean.MetaM Q(CharZero «$α»)
-- Init.Data.SInt.Lemmas
ISize.mod_self : ∀ {a : ISize}, a % a = 0
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.closure_union_congr_right : ∀ {α : Type u_2} {M : Matroid α} {X Y Y' : Set α}, M.closure Y = M.closure Y' → M.closure (X ∪ Y) = M.closure (X ∪ Y')
-- Mathlib.Topology.Continuous
Continuous.comp : ∀ {X : Type u_1} {Y : Type u_2} {Z : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] {f : X → Y} {g : Y → Z}, Continuous g → Continuous f → Continuous (g ∘ f)
-- Mathlib.GroupTheory.Coset.Basic
AddSubgroup.quotientEquivProdOfLE'_apply : ∀ {α : Type u_1} [inst : AddGroup α] {s t : AddSubgroup α} (h_le : s ≤ t) (f : α ⧸ t → α)
  (hf : Function.RightInverse f QuotientAddGroup.mk) (a : α ⧸ s),
  (AddSubgroup.quotientEquivProdOfLE' h_le f hf) a =
    (Quotient.map' id ⋯ a, Quotient.map' (fun g => ⟨-f (Quotient.mk'' g) + g, ⋯⟩) ⋯ a)
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
IsTranscendenceBasis.of_subsingleton : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [Subsingleton R] [Nonempty ι], IsTranscendenceBasis R x
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.CartesianMonoidalCategory.comp_lift : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {V W X Y : C} (f : V ⟶ W) (g : W ⟶ X) (h : W ⟶ Y),
  CategoryTheory.CategoryStruct.comp f (CategoryTheory.CartesianMonoidalCategory.lift g h) =
    CategoryTheory.CartesianMonoidalCategory.lift (CategoryTheory.CategoryStruct.comp f g)
      (CategoryTheory.CategoryStruct.comp f h)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.instNonUnitalCommRingOfNonUnitalRingHomClass : {ι : Type u_2} →
  [inst : Preorder ι] →
    {G : ι → Type u_3} →
      {T : ⦃i j : ι⦄ → i ≤ j → Type u_6} →
        {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} →
          [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)] →
            [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] →
              [inst_3 : IsDirectedOrder ι] →
                [Nonempty ι] →
                  [inst_5 : (i : ι) → NonUnitalCommRing (G i)] →
                    [∀ (i j : ι) (h : i ≤ j), NonUnitalRingHomClass (T h) (G i) (G j)] →
                      NonUnitalCommRing (DirectLimit G f)
-- Batteries.Data.String.Lemmas
Substring.Raw.ValidFor.foldr : ∀ {α : Type u_1} {l m r : List Char} (f : Char → α → α) (init : α) {s : Substring.Raw},
  Substring.Raw.ValidFor l m r s → Substring.Raw.Legacy.foldr f init s = List.foldr f init m
-- Mathlib.Topology.UniformSpace.AbstractCompletion
AbstractCompletion.uniformContinuous_extend : ∀ {α : Type uα} [inst : UniformSpace α] (pkg : AbstractCompletion.{vα, uα} α) {β : Type uβ} [inst_1 : UniformSpace β]
  {f : α → β} [CompleteSpace β], UniformContinuous (pkg.extend f)
-- Mathlib.Analysis.Normed.Module.Bases
SchauderBasis.succSub.eq_1 : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {X : Type u_2} [inst_1 : NormedAddCommGroup X]
  [inst_2 : NormedSpace 𝕜 X] (P : ℕ → X →L[𝕜] X) (n : ℕ), SchauderBasis.succSub P n = P (n + 1) - P n
-- Mathlib.CategoryTheory.Action.Basic
Action.functorCategoryEquivalence_functor : ∀ (V : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} V] (G : Type u_2) [inst_1 : Monoid G],
  (Action.functorCategoryEquivalence V G).functor = Action.FunctorCategoryEquivalence.functor
-- Mathlib.Combinatorics.Enumerative.Composition
List.getElem_splitWrtComposition : ∀ {n : ℕ} {α : Type u_1} (l : List α) (c : Composition n) (i : ℕ) (h : i < (l.splitWrtComposition c).length),
  (l.splitWrtComposition c)[i] = List.drop (c.sizeUpTo i) (List.take (c.sizeUpTo (i + 1)) l)
-- Mathlib.Order.Interval.Finset.Basic
Finset.uIcc_of_le : ∀ {α : Type u_2} [inst : Lattice α] [inst_1 : LocallyFiniteOrder α] {a b : α}, a ≤ b → Finset.uIcc a b = Finset.Icc a b
-- Init.Data.List.Sort.Basic
_private.Init.Data.List.Sort.Basic.0.List.merge.match_1.eq_3 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : α) (xs : List α) (y : α) (ys : List α)
  (h_1 : (ys : List α) → motive [] ys) (h_2 : (xs : List α) → motive xs [])
  (h_3 : (x : α) → (xs : List α) → (y : α) → (ys : List α) → motive (x :: xs) (y :: ys)),
  (match x :: xs, y :: ys with
    | [], ys => h_1 ys
    | xs, [] => h_2 xs
    | x :: xs, y :: ys => h_3 x xs y ys) =
    h_3 x xs y ys
-- Mathlib.Topology.MetricSpace.Bounded
Metric.diam_zero : ∀ {α : Type u} [inst : PseudoMetricSpace α] [inst_1 : Zero α], Metric.diam 0 = 0
-- Mathlib.RingTheory.HahnSeries.Addition
HahnSeries.addOppositeEquiv_support : ∀ {Γ : Type u_1} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : AddMonoid R] (x : HahnSeries Γ Rᵃᵒᵖ),
  (AddOpposite.unop (HahnSeries.addOppositeEquiv x)).support = x.support
-- Mathlib.Algebra.Order.Antidiag.Pi
Finset.finsetCongr_piAntidiag_eq_antidiag : ∀ {μ : Type u_2} [inst : AddCommMonoid μ] [inst_1 : Finset.HasAntidiagonal μ] [inst_2 : DecidableEq μ] (n : μ),
  (Equiv.boolArrowEquivProd μ).finsetCongr (Finset.univ.piAntidiag n) = Finset.HasAntidiagonal.antidiagonal n
-- Std.Internal.Do.PredTrans
/-- `PredTrans` is a lawful monad: all monad laws hold definitionally.  -/
Std.Internal.Do.instLawfulMonadPredTrans : ∀ (Pred : Type u) (EPred : Type v), LawfulMonad (Std.Internal.Do.PredTrans Pred EPred)
-- Std.Async.TCP
/-- Sends multiple data buffers through the client socket.
 -/
Std.Async.TCP.Socket.Client.sendAll : Std.Async.TCP.Socket.Client → Array ByteArray → Std.Async.Async Unit
-- Mathlib.Data.Fintype.Card
Fintype.card_subtype_compl : ∀ {α : Type u_1} [inst : Fintype α] (p : α → Prop) [inst_1 : Fintype { x // p x }] [inst_2 : Fintype { x // ¬p x }],
  Fintype.card { x // ¬p x } = Fintype.card α - Fintype.card { x // p x }
-- Mathlib.Data.Matrix.Basis
/-- `M` is a scalar matrix if it commutes with every non-diagonal `single`.  -/
Matrix.mem_range_scalar_of_commute_single : ∀ {n : Type u_3} {α : Type u_7} [inst : DecidableEq n] [inst_1 : Fintype n] [inst_2 : Semiring α] {M : Matrix n n α},
  (Pairwise fun i j => Commute (Matrix.single i j 1) M) → M ∈ Set.range ⇑(Matrix.scalar n)
-- Mathlib.GroupTheory.SpecificGroups.Cyclic.Basic
AddSubgroup.le_zmultiples_iff : ∀ {G : Type u_2} [inst : AddGroup G] (g : G) (H : AddSubgroup G),
  H ≤ AddSubgroup.zmultiples g ↔ ∃ n, H = AddSubgroup.zmultiples (n • g)
-- Lean.Meta.Sym.MaxFVar
_private.Lean.Meta.Sym.MaxFVar.0.Lean.Meta.Sym.check : Lean.Expr → Lean.Meta.Sym.SymM (Option Lean.FVarId) → Lean.Meta.Sym.SymM (Option Lean.FVarId)
-- Init.Data.String.Basic
/-- Given a slice and two valid positions within the slice, obtain a new slice on the same underlying
string formed by the new bounds, or panic if the given end is strictly less than the given start.  -/
String.Slice.slice! : (s : String.Slice) → s.Pos → s.Pos → String.Slice
-- Init.Data.Int.Linear
Int.Internal.Linear.eq_le_subst_nonpos_cert.eq_1 : ∀ (x : Int.Internal.Linear.Var) (p₁ p₂ p₃ : Int.Internal.Linear.Poly),
  Int.Internal.Linear.eq_le_subst_nonpos_cert x p₁ p₂ p₃ =
    ((p₁.coeff x).ble' 0).and' (p₃.beq' (Int.Internal.Linear.Poly.combine_mul_k (p₂.coeff x) (-p₁.coeff x) p₁ p₂))
-- Mathlib.Algebra.Category.Grp.Limits
GrpCat.Forget₂.createsLimit.eq_1 : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat),
  GrpCat.Forget₂.createsLimit F =
    CategoryTheory.createsLimitOfReflectsIso fun c' t =>
      have this := ⋯;
      have this_1 := ⋯;
      {
        liftedCone :=
          { pt := GrpCat.of (CategoryTheory.Limits.Types.Small.limitCone (F.comp (CategoryTheory.forget GrpCat))).pt,
            π :=
              { app := fun j => GrpCat.ofHom (MonCat.limitπMonoidHom (F.comp (CategoryTheory.forget₂ GrpCat MonCat)) j),
                naturality := ⋯ } },
        validLift :=
          (MonCat.HasLimits.limitConeIsLimit (F.comp (CategoryTheory.forget₂ GrpCat MonCat))).uniqueUpToIso t,
        makesLimit :=
          CategoryTheory.Limits.IsLimit.ofFaithful (CategoryTheory.forget₂ GrpCat MonCat)
            (MonCat.HasLimits.limitConeIsLimit (F.comp (CategoryTheory.forget₂ GrpCat MonCat)))
            (fun x =>
              {
                hom' :=
                  {
                    toFun := fun v =>
                      EquivLike.coe
                        (equivShrink
                          ↑((F.comp (CategoryTheory.forget₂ GrpCat MonCat)).comp
                                (CategoryTheory.forget MonCat)).sections)
                        ⟨fun j =>
                          (CategoryTheory.ConcreteCategory.hom
                              (((CategoryTheory.forget MonCat).mapCone
                                      ((CategoryTheory.forget₂ GrpCat MonCat).mapCone x)).π.app
                                j))
                            v,
                          ⋯⟩,
                    map_one' := ⋯, map_mul' := ⋯ } })
            ⋯ }
-- Mathlib.RingTheory.Localization.Basic
instAlgebraLocalizationAlgebraMapSubmonoid : {R : Type u_1} →
  [inst : CommSemiring R] →
    (M : Submonoid R) →
      (S : Type u_2) →
        [inst_1 : CommSemiring S] →
          [inst_2 : Algebra R S] → Algebra (Localization M) (Localization (Algebra.algebraMapSubmonoid S M))
-- Mathlib.Algebra.Group.PUnit
PUnit.instSub_mathlib : Sub PUnit.{u_1 + 1}
-- Mathlib.Algebra.Group.Subsemigroup.Defs
Subsemigroup.ofClass.eq_1 : ∀ {S : Type u_3} {M : Type u_4} [inst : Mul M] [inst_1 : SetLike S M] [inst_2 : MulMemClass S M] (s : S),
  Subsemigroup.ofClass s = { carrier := ↑s, mul_mem' := ⋯ }
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instRing : {R : Type u_1} →
  {A : Type u_2} →
    [inst : CommRing R] →
      [inst_1 : NonUnitalRing A] →
        [inst_2 : Module R A] → [IsScalarTower R A A] → [SMulCommClass R A A] → Ring (Unitization R A)
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.instInhabitedHomOfPreadditive : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [CategoryTheory.Preadditive C] → (P Q : CategoryTheory.Idempotents.Karoubi C) → Inhabited (P.Hom Q)
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.mem_roots_sub_C : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R} {a x : R},
  0 < p.degree → (x ∈ (p - Polynomial.C a).roots ↔ Polynomial.eval x p = a)
-- Mathlib.Algebra.Order.Module.Defs
SMulPosMono.mk : ∀ {α : Type u_1} {β : Type u_2} [inst : SMul α β] [inst_1 : Preorder α] [inst_2 : Preorder β] [inst_3 : Zero β],
  (∀ ⦃b : β⦄, 0 ≤ b → ∀ ⦃a₁ a₂ : α⦄, a₁ ≤ a₂ → a₁ • b ≤ a₂ • b) → SMulPosMono α β
-- Mathlib.FieldTheory.Normal.Closure
normalClosure.restrictScalars_eq : ∀ (F : Type u_1) (K : Type u_2) (L : Type u_3) [inst : Field F] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra F K] [inst_4 : Algebra F L] [inst_5 : Algebra K L] [inst_6 : IsScalarTower F K L],
  IntermediateField.restrictScalars F
      (IsScalarTower.toAlgHom K (↥(IntermediateField.normalClosure F K L)) L).fieldRange =
    IntermediateField.normalClosure F K L
-- Init.Data.BitVec.Lemmas
BitVec.msb_extractLsb : ∀ {w hi lo : ℕ} {x : BitVec w},
  (BitVec.extractLsb hi lo x).msb = (decide (max hi lo < w) && x.getMsbD (w - 1 - max hi lo))
-- Init.Data.UInt.Lemmas
USize.ofNatClamp_toNat : ∀ (n : USize), USize.ofNatClamp n.toNat = n
-- Init.Data.Vector.Attach
Vector.unattach_append : ∀ {α : Type u_1} {n m : ℕ} {p : α → Prop} {xs : Vector { x // p x } n} {ys : Vector { x // p x } m},
  (xs ++ ys).unattach = xs.unattach ++ ys.unattach
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.RelativeCellComplex
/-- Given a cell `c` of rank `j` for a rank function `f` for a proper
pairing of a subcomplex of a simplicial set, this is the inclusion of
`c.horn` into `f.sigmaHorn j`.  -/
SSet.Subcomplex.Pairing.RankFunction.Cell.ιSigmaHorn : {X : SSet} →
  {A : X.Subcomplex} →
    {P : A.Pairing} →
      {ι : Type v} →
        [inst : LinearOrder ι] →
          {f : P.RankFunction ι} → [inst_1 : P.IsProper] → {j : ι} → (c : f.Cell j) → c.horn.toSSet ⟶ f.sigmaHorn j
-- Mathlib.AlgebraicTopology.SimplicialObject.Basic
CategoryTheory.SimplicialObject.instHasLimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasLimits C],
  CategoryTheory.Limits.HasLimits (CategoryTheory.SimplicialObject C)
-- Init.Data.UInt.Lemmas
UInt16.ofNatLT_toNat : ∀ (n : UInt16), UInt16.ofNatLT n.toNat ⋯ = n
-- Mathlib.Algebra.ContinuedFractions.Computation.Approximations
GenContFract.zero_le_of_contsAux_b : ∀ {K : Type u_1} {v : K} {n : ℕ} [inst : Field K] [inst_1 : LinearOrder K] [IsStrictOrderedRing K]
  [inst_3 : FloorRing K], 0 ≤ ((GenContFract.of v).contsAux n).b