mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.RingTheory.HopfAlgebra.Basic
HopfAlgebra.toHopfAlgebraStruct : {R : Type u} →
  {A : Type v} → {inst : CommSemiring R} → {inst_1 : Semiring A} → [self : HopfAlgebra R A] → HopfAlgebraStruct R A
-- Mathlib.Combinatorics.SimpleGraph.Clique
SimpleGraph.cliqueSet_mono' : ∀ {α : Type u_1} {G H : SimpleGraph α}, G ≤ H → G.cliqueSet ≤ H.cliqueSet
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKeyD_insert_self : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {k fallback : α} {v : β}, (m.insert k v).getKeyD k fallback = k
-- Mathlib.Data.Finset.Sups
/-- `sᶜˢ` is the finset of elements of the form `aᶜ` where `a ∈ s`.  -/
Finset.compls : {α : Type u_2} → [BooleanAlgebra α] → Finset α → Finset α
-- Mathlib.Analysis.Normed.Algebra.DualNumber
DualNumber.eps.eq_1 : ∀ {R : Type u_1} [inst : Zero R] [inst_1 : One R], DualNumber.eps = TrivSqZeroExt.inr 1
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_zero : ∀ {R : Type u} [inst : Semiring R] {k : ℕ}, (⇑Polynomial.derivative)^[k] 0 = 0
-- Mathlib.CategoryTheory.Preadditive.Mat
CategoryTheory.Functor.mapMatId_inv_app : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Preadditive C]
  (X : CategoryTheory.Mat_ C),
  CategoryTheory.Functor.mapMatId.inv.app X =
    CategoryTheory.CategoryStruct.id ((CategoryTheory.Functor.id C).mapMat_.obj X)
-- Mathlib.RingTheory.Etale.Finite
CommAlgCat.FiniteEtale.equivOfIsSepClosed_functor : ∀ (Ω : Type u) [inst : Field Ω] [inst_1 : IsSepClosed Ω],
  (CommAlgCat.FiniteEtale.equivOfIsSepClosed Ω).functor = CommAlgCat.FiniteEtale.finiteSpec Ω
-- Mathlib.Computability.TuringMachine.Computable
/-- The final configuration corresponding to a list in the output alphabet.  -/
Turing.haltList : (tm : Turing.FinTM2) → List (tm.Γ tm.k₁) → tm.Cfg
-- Mathlib.CategoryTheory.Shift.Basic
CategoryTheory.ShiftMkCore.mk.injEq : ∀ {C : Type u} {A : Type u_1} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : AddMonoid A]
  (F : A → CategoryTheory.Functor C C) (zero : F 0 ≅ CategoryTheory.Functor.id C)
  (add : (n m : A) → F (n + m) ≅ (F n).comp (F m))
  (assoc_hom_app :
    autoParam
      (∀ (m₁ m₂ m₃ : A) (X : C),
        CategoryTheory.CategoryStruct.comp ((add (m₁ + m₂) m₃).hom.app X) ((F m₃).map ((add m₁ m₂).hom.app X)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp ((add m₁ (m₂ + m₃)).hom.app X) ((add m₂ m₃).hom.app ((F m₁).obj X))))
      CategoryTheory.ShiftMkCore.assoc_hom_app._autoParam)
  (zero_add_hom_app :
    autoParam
      (∀ (n : A) (X : C),
        (add 0 n).hom.app X =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((F n).map (zero.inv.app X)))
      CategoryTheory.ShiftMkCore.zero_add_hom_app._autoParam)
  (add_zero_hom_app :
    autoParam
      (∀ (n : A) (X : C),
        (add n 0).hom.app X =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (zero.inv.app ((F n).obj X)))
      CategoryTheory.ShiftMkCore.add_zero_hom_app._autoParam)
  (F_1 : A → CategoryTheory.Functor C C) (zero_1 : F_1 0 ≅ CategoryTheory.Functor.id C)
  (add_1 : (n m : A) → F_1 (n + m) ≅ (F_1 n).comp (F_1 m))
  (assoc_hom_app_1 :
    autoParam
      (∀ (m₁ m₂ m₃ : A) (X : C),
        CategoryTheory.CategoryStruct.comp ((add_1 (m₁ + m₂) m₃).hom.app X) ((F_1 m₃).map ((add_1 m₁ m₂).hom.app X)) =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
            (CategoryTheory.CategoryStruct.comp ((add_1 m₁ (m₂ + m₃)).hom.app X)
              ((add_1 m₂ m₃).hom.app ((F_1 m₁).obj X))))
      CategoryTheory.ShiftMkCore.assoc_hom_app._autoParam)
  (zero_add_hom_app_1 :
    autoParam
      (∀ (n : A) (X : C),
        (add_1 0 n).hom.app X =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) ((F_1 n).map (zero_1.inv.app X)))
      CategoryTheory.ShiftMkCore.zero_add_hom_app._autoParam)
  (add_zero_hom_app_1 :
    autoParam
      (∀ (n : A) (X : C),
        (add_1 n 0).hom.app X =
          CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯) (zero_1.inv.app ((F_1 n).obj X)))
      CategoryTheory.ShiftMkCore.add_zero_hom_app._autoParam),
  ({ F := F, zero := zero, add := add, assoc_hom_app := assoc_hom_app, zero_add_hom_app := zero_add_hom_app,
        add_zero_hom_app := add_zero_hom_app } =
      { F := F_1, zero := zero_1, add := add_1, assoc_hom_app := assoc_hom_app_1,
        zero_add_hom_app := zero_add_hom_app_1, add_zero_hom_app := add_zero_hom_app_1 }) =
    (F = F_1 ∧ zero ≍ zero_1 ∧ add ≍ add_1)
-- Mathlib.Algebra.Order.Chebyshev
/-- **Chebyshev's Sum Inequality**: When `f` and `g` antivary together (e.g. one is monotone, the
other is antitone), the scalar product of their sum is less than the size of the set times their
scalar product.  -/
AntivaryOn.card_smul_sum_le_sum_smul_sum : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulMono α β] {s : Finset ι} {f : ι → α} {g : ι → β},
  AntivaryOn f g ↑s → s.card • ∑ i ∈ s, f i • g i ≤ (∑ i ∈ s, f i) • ∑ i ∈ s, g i
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.Loopless.ground_eq : ∀ {α : Type u_1} (M : Matroid α) [M.Loopless], M.E = {e | M.IsNonloop e}
-- Mathlib.CategoryTheory.Limits.IsLimit
CategoryTheory.Limits.IsColimit.homEquiv.eq_1 : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} {t : CategoryTheory.Limits.Cocone F} (h : CategoryTheory.Limits.IsColimit t) {W : C},
  h.homEquiv =
    { toFun := fun f => (t.extend f).ι, invFun := fun π => h.desc { pt := W, ι := π }, left_inv := ⋯, right_inv := ⋯ }
-- Mathlib.MeasureTheory.Group.Measure
MeasureTheory.Measure.IsOpenPosMeasure.neg : ∀ {G : Type u_1} [inst : MeasurableSpace G] [inst_1 : TopologicalSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G}
  [inst_3 : AddGroup G] [ContinuousNeg G] [μ.IsOpenPosMeasure], μ.neg.IsOpenPosMeasure
-- Mathlib.Algebra.GroupWithZero.Defs
mul_eq_zero_of_left : ∀ {M₀ : Type u_1} [inst : MulZeroClass M₀] {a : M₀}, a = 0 → ∀ (b : M₀), a * b = 0
-- Mathlib.CategoryTheory.Functor.KanExtension.Preserves
/-- Show that `G` preserves right Kan extensions if it maps some right Kan extension to a left
Kan extension, phrased in terms of `IsUniversal`.  -/
CategoryTheory.Functor.PreservesRightKanExtension.mk_of_preserves_isUniversal : ∀ {A : Type u_1} {B : Type u_2} {C : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} A]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} B] [inst_2 : CategoryTheory.Category.{v_3, u_3} C]
  [inst_3 : CategoryTheory.Category.{v_4, u_4} D] (G : CategoryTheory.Functor B D) (F : CategoryTheory.Functor A B)
  (L : CategoryTheory.Functor A C) (E : L.RightExtension F) (hE : CategoryTheory.CostructuredArrow.IsUniversal E),
  Nonempty
      (CategoryTheory.CostructuredArrow.IsUniversal
        ((CategoryTheory.Functor.RightExtension.postcompose₂ L F G).obj E)) →
    G.PreservesRightKanExtension F L
-- Mathlib.Tactic.Linarith.Oracle.SimplexAlgorithm.Datatypes
/-- Array containing the free variables' indexes  -/
Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau.free : {matType : ℕ → ℕ → Type} →
  [inst : Mathlib.Tactic.Linarith.SimplexAlgorithm.UsableInSimplexAlgorithm matType] →
    Mathlib.Tactic.Linarith.SimplexAlgorithm.Tableau matType → Array ℕ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.Equiv.constToList_eq : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t₁ t₂ : Std.DTreeMap α (fun x => β) cmp} [Std.TransCmp cmp],
  t₁.Equiv t₂ → Std.DTreeMap.Const.toList t₁ = Std.DTreeMap.Const.toList t₂
-- Mathlib.Analysis.Calculus.ContDiff.FaaDiBruno
/-- Given a formal multilinear series `p`, an ordered partition `c` of `n` and the index `i` of a
block of `c`, we may define a function on `Fin n → E` by picking the variables in the `i`-th block
of `n`, and applying the corresponding coefficient of `p` to these variables. This function is
called `p.applyOrderedFinpartition c v i` for `v : Fin n → E` and `i : Fin c.k`.  -/
OrderedFinpartition.applyOrderedFinpartition : {𝕜 : 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] →
                {n : ℕ} →
                  (c : OrderedFinpartition n) →
                    ((i : Fin c.length) → E [×c.partSize i]→L[𝕜] F) → (Fin n → E) → Fin c.length → F
-- Init.Core
Iff.comm : ∀ {a b : Prop}, (a ↔ b) ↔ (b ↔ a)
-- Mathlib.MeasureTheory.VectorMeasure.Integral
/-- The special case of the pairing integral where the pairing is just the flip of scalar
multiplication by `ℝ` on `F` and `f` is `F`-valued and `μ` is a signed measure.
The resulting integral is `F`-valued. -/
MeasureTheory.VectorMeasure.«term∫ᵛ_,_∂<•_» : Lean.ParserDescr
-- Mathlib.Algebra.Order.Field.Basic
div_le_one_of_ge : ∀ {α : Type u_2} [inst : Field α] [inst_1 : PartialOrder α] [PosMulReflectLT α] [IsStrictOrderedRing α] {a b : α},
  b ≤ a → b ≤ 0 → a / b ≤ 1
-- Mathlib.RingTheory.GradedAlgebra.HomogeneousLocalization
HomogeneousLocalization.val_mul : ∀ {ι : Type u_1} {A : Type u_2} {σ : Type u_3} [inst : CommRing A] [inst_1 : SetLike σ A]
  [inst_2 : AddSubgroupClass σ A] [inst_3 : AddCommMonoid ι] [inst_4 : DecidableEq ι] {𝒜 : ι → σ}
  [inst_5 : GradedRing 𝒜] {x : Submonoid A} (y1 y2 : HomogeneousLocalization 𝒜 x), (y1 * y2).val = y1.val * y2.val
-- Mathlib.Analysis.SpecialFunctions.ContinuousFunctionalCalculus.PosPart.Basic
CFC.posPart_eq_self : ∀ {A : Type u_1} [inst : NonUnitalRing A] [inst_1 : Module ℝ A] [inst_2 : SMulCommClass ℝ A A]
  [inst_3 : IsScalarTower ℝ A A] [inst_4 : StarRing A] [inst_5 : TopologicalSpace A]
  [inst_6 : NonUnitalContinuousFunctionalCalculus ℝ A IsSelfAdjoint] [inst_7 : PartialOrder A] [StarOrderedRing A]
  [NonnegSpectrumClass ℝ A] (a : A), a⁺ = a ↔ 0 ≤ a
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.mod_zero : ∀ {R : Type u} [inst : EuclideanDomain R] (a : R), a % 0 = a
-- Mathlib.Data.Fin.Tuple.Basic
/-- **Alias** of `Fin.forall_fin_succ`. -/
Fin.forall_iff_succ : ∀ {n : ℕ} {P : Fin (n + 1) → Prop}, (∀ (i : Fin (n + 1)), P i) ↔ P 0 ∧ ∀ (i : Fin n), P i.succ
-- Mathlib.Algebra.Polynomial.Module.AEval
Module.AEval.instIsScalarTowerOrigPolynomial : ∀ {R : Type u_1} {A : Type u_3} {M : Type u_2} [inst : CommSemiring R] [inst_1 : Semiring A] (a : A)
  [inst_2 : Algebra R A] [inst_3 : AddCommMonoid M] [inst_4 : Module A M] [inst_5 : Module R M]
  [inst_6 : IsScalarTower R A M], IsScalarTower R (Polynomial R) (Module.AEval R M a)
-- Mathlib.Algebra.Group.Hom.Defs
MonoidHom.instMonoidHomClassMulHom_2 : ∀ {M : Type u_10} {N : Type u_11} [inst : Monoid M] [inst_1 : CancelMonoid N], MonoidHomClass (M →ₙ* N) M N
-- Mathlib.GroupTheory.GroupAction.ConjAct
ConjAct.toConjAct_ofConjAct : ∀ {G : Type u_3} [inst : DivInvMonoid G] (x : ConjAct G), ConjAct.toConjAct (ConjAct.ofConjAct x) = x
-- Lean.Meta.Basic
/-- Similar to `orelse`, but merge errors. Note that internal errors are not caught.
The default `mergeRef` uses the `ref` (position information) for the first message.
The default `mergeMsg` combines error messages using `Format.line ++ Format.line` as a separator.  -/
Lean.Meta.orelseMergeErrors : {m : Type → Type u_1} →
  {α : Type} →
    [MonadControlT Lean.MetaM m] →
      [Monad m] →
        m α →
          m α →
            (optParam (Lean.Syntax → Lean.Syntax → Lean.Syntax) fun r₁ x => r₁) →
              (optParam (Lean.MessageData → Lean.MessageData → Lean.MessageData) fun m₁ m₂ =>
                  m₁ ++ Lean.MessageData.ofFormat Std.Format.line ++ Lean.MessageData.ofFormat Std.Format.line ++ m₂) →
                m α
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.updateCol_transpose : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} {M : Matrix m n α} {i : m} {b : n → α} [inst : DecidableEq m],
  M.transpose.updateCol i b = (M.updateRow i b).transpose
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
/-- An `IsFiveWheelLike r k v w₁ w₂ s t` structure in `G` consists of vertices `v w₁ w₂` and `r`-sets
`s` and `t` such that `{v, w₁, w₂}` induces the single edge `w₁w₂` (i.e. they form an
`IsPathGraph3Compl`), `v, w₁, w₂ ∉ s ∪ t`, `s ∪ {v}, t ∪ {v}, s ∪ {w₁}, t ∪ {w₂}` are all
`(r + 1)`-cliques and `#(s ∩ t) = k`. (If `G` is maximally `(r + 2)`-cliquefree and not complete
multipartite then `G` will contain such a structure: see
`exists_isFiveWheelLike_of_maximal_cliqueFree_not_isCompleteMultipartite`.)
 -/
SimpleGraph.IsFiveWheelLike : {α : Type u_1} → [DecidableEq α] → SimpleGraph α → ℕ → ℕ → α → α → α → Finset α → Finset α → Prop
-- Mathlib.Condensed.Discrete.LocallyConstant
CompHausLike.LocallyConstant.functor_obj_obj_obj : ∀ (P : TopCat → Prop) [inst : CompHausLike.HasExplicitFiniteCoproducts P] [inst_1 : CompHausLike.HasExplicitPullbacks P]
  (hs :
    ∀ ⦃X Y : CompHausLike P⦄ (f : X ⟶ Y),
      CategoryTheory.EffectiveEpi f → Function.Surjective ⇑(CategoryTheory.ConcreteCategory.hom f))
  (X : Type (max u w)) (x : (CompHausLike P)ᵒᵖ),
  ((CompHausLike.LocallyConstant.functor P hs).obj X).obj.obj x = LocallyConstant (↑(Opposite.unop x).toTop) X
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Products
CategoryTheory.Limits.instIsIsoPiComparison : ∀ {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} (f : J → C) [inst_2 : CategoryTheory.Limits.HasProduct f]
  [inst_3 : CategoryTheory.Limits.HasProduct fun j => G.obj (f j)]
  [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Discrete.functor f) G],
  CategoryTheory.IsIso (CategoryTheory.Limits.piComparison G f)
-- Mathlib.RingTheory.Polynomial.SeparableDegree
/-- The `HasSeparableContraction.contraction` is indeed a separable contraction.  -/
Polynomial.HasSeparableContraction.isSeparableContraction : ∀ {F : Type u_1} [inst : CommSemiring F] {q : ℕ} {f : Polynomial F} (hf : Polynomial.HasSeparableContraction q f),
  Polynomial.IsSeparableContraction q f hf.contraction
-- Init.Data.Slice.Array.Iterator
Array.instToStringSubarray : {α : Type u} → [ToString α] → ToString (Subarray α)
-- Mathlib.Topology.Algebra.Monoid
isClosed_setOfPred_map_add : ∀ (M₁ : Type u_6) (M₂ : Type u_7) [inst : TopologicalSpace M₂] [T2Space M₂] [inst_2 : Add M₁] [inst_3 : Add M₂]
  [ContinuousAdd M₂], IsClosed {f | ∀ (x y : M₁), f (x + y) = f x + f y}
-- Mathlib.Algebra.Ring.InjSurj
/-- Pullback a `NonUnitalCommRing` instance along an injective function.  -/
Function.Injective.nonUnitalCommRing : {R : Type u_1} →
  {S : Type u_2} →
    [inst : Add S] →
      [inst_1 : Mul S] →
        [inst_2 : Zero S] →
          [inst_3 : Neg S] →
            [inst_4 : Sub S] →
              [inst_5 : SMul ℕ S] →
                [inst_6 : SMul ℤ S] →
                  [inst_7 : NonUnitalCommRing R] →
                    (f : S → R) →
                      Function.Injective f →
                        f 0 = 0 →
                          (∀ (x y : S), f (x + y) = f x + f y) →
                            (∀ (x y : S), f (x * y) = f x * f y) →
                              (∀ (x : S), f (-x) = -f x) →
                                (∀ (x y : S), f (x - y) = f x - f y) →
                                  (∀ (n : ℕ) (x : S), f (n • x) = n • f x) →
                                    (∀ (n : ℤ) (x : S), f (n • x) = n • f x) → NonUnitalCommRing S
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.toList_filterMap : ∀ {α : Type u} {β : α → Type v} {γ : α → Type w} {cmp : α → α → Ordering} {t : Std.DTreeMap.Raw α β cmp}
  {f : (a : α) → β a → Option (γ a)},
  t.WF →
    (Std.DTreeMap.Raw.filterMap f t).toList =
      List.filterMap (fun p => Option.map (fun x => ⟨p.fst, x⟩) (f p.fst p.snd)) t.toList
-- Mathlib.Algebra.DirectSum.Decomposition
DirectSum.decompose_of_mem_ne : ∀ {ι : Type u_1} {M : Type u_3} {σ : Type u_4} [inst : DecidableEq ι] [inst_1 : AddCommMonoid M] [inst_2 : SetLike σ M]
  [inst_3 : AddSubmonoidClass σ M] (ℳ : ι → σ) [inst_4 : DirectSum.Decomposition ℳ] {x : M} {i j : ι},
  x ∈ ℳ i → i ≠ j → ↑(((DirectSum.decompose ℳ) x) j) = 0
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.isSome_apply_of_mem_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp]
  {f : α → β → Option γ} {k : α} (h : k ∈ Std.ExtTreeMap.filterMap f t), (f (t.getKey k ⋯) t[k]).isSome = true
-- Mathlib.Analysis.Convex.Side
/-- **Alias** of the forward direction of `AffineSubspace.sOppSide_comm`. -/
AffineSubspace.SOppSide.symm : ∀ {R : Type u_1} {V : Type u_2} {P : Type u_4} [inst : CommRing R] [inst_1 : PartialOrder R]
  [inst_2 : IsStrictOrderedRing R] [inst_3 : AddCommGroup V] [inst_4 : Module R V] [inst_5 : AddTorsor V P]
  {s : AffineSubspace R P} {x y : P}, s.SOppSide x y → s.SOppSide y x
-- Mathlib.Algebra.Ring.Idempotent
IsIdempotentElem.one_sub_mul_self : ∀ {R : Type u_1} [inst : NonAssocRing R] {a : R}, IsIdempotentElem a → (1 - a) * a = 0
-- Aesop.RuleTac.Forward.Basic
Aesop.ForwardHypData.mk.sizeOf_spec : ∀ (depths : Std.HashMap Lean.FVarId ℕ), sizeOf { depths := depths } = 1 + sizeOf depths
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.exp_neg_two_mul_le : ∀ {x : ℝ}, 0 < x → Real.exp (-2 * x) < Real.exp (2 - ↑⌈x⌉₊) / ↑⌈x⌉₊
-- Mathlib.SetTheory.ZFC.PSet
PSet.not_subset_of_mem : ∀ {x y : PSet.{u_1}}, x ∈ y → ¬y ⊆ x
-- Mathlib.Logic.Function.Basic
Function.extend_apply' : ∀ {α : Sort u_1} {β : Sort u_2} {γ : Sort u_3} {f : α → β} (g : α → γ) (e' : β → γ) (b : β),
  (¬∃ a, f a = b) → Function.extend f g e' b = e' b
-- Mathlib.Data.Rat.Lemmas
Rat.num_div_eq_of_coprime : ∀ {a b : ℤ}, 0 < b → a.natAbs.Coprime b.natAbs → (↑a / ↑b).num = a
-- Lean.Elab.PreDefinition.Main
_private.Lean.Elab.PreDefinition.Main.0.Lean.Elab.ensureNoUnassignedLevelMVarsAtPreDef : Lean.Elab.PreDefinition → Lean.Elab.TermElabM Lean.Elab.PreDefinition
-- Std.Time.Zoned.ZoneRules
Std.Time.TimeZone.Transition.mk.sizeOf_spec : ∀ (time : Std.Time.Second.Offset) (localTimeType : Std.Time.TimeZone.LocalTimeType),
  sizeOf { time := time, localTimeType := localTimeType } = 1 + sizeOf time + sizeOf localTimeType
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.isConstant_coe_const : ∀ {α : Type u_1} {β : Type u_2} {l : Filter α} {b : β}, (↑fun x => b).IsConstant
-- Mathlib.CategoryTheory.Shift.SingleFunctors
/-- The functor `SingleFunctors C D A ⥤ SingleFunctors C E A` given by the postcomposition
by a functor `G : D ⥤ E` which commutes with the shift.  -/
CategoryTheory.SingleFunctors.postcompFunctor : (C : Type u_1) →
  {D : Type u_2} →
    {E : Type u_3} →
      [inst : CategoryTheory.Category.{v_1, u_1} C] →
        [inst_1 : CategoryTheory.Category.{v_2, u_2} D] →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} E] →
            (A : Type u_5) →
              [inst_3 : AddMonoid A] →
                [inst_4 : CategoryTheory.HasShift D A] →
                  [inst_5 : CategoryTheory.HasShift E A] →
                    (G : CategoryTheory.Functor D E) →
                      [G.CommShift A] →
                        CategoryTheory.Functor (CategoryTheory.SingleFunctors C D A)
                          (CategoryTheory.SingleFunctors C E A)
-- Lean.Meta.Tactic.Grind.Arith.Linear.Reify
Lean.Meta.Grind.Arith.Linear.isAddInst : Lean.Meta.Grind.Arith.Linear.Struct → Lean.Expr → Bool
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
/-- `(X₁ ⨿[Z₁] X₂) ⨿[Z₂] X₃` is the pushout `(X₁ ⨿[Z₁] X₂) ×[X₂] (X₂ ⨿[Z₂] X₃)`.  -/
CategoryTheory.Limits.pushoutPushoutLeftIsPushout : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X₁ X₂ X₃ Z₁ Z₂ : C} →
      (g₁ : Z₁ ⟶ X₁) →
        (g₂ : Z₁ ⟶ X₂) →
          (g₃ : Z₂ ⟶ X₂) →
            (g₄ : Z₂ ⟶ X₃) →
              [inst_1 : CategoryTheory.Limits.HasPushout g₁ g₂] →
                [inst_2 : CategoryTheory.Limits.HasPushout g₃ g₄] →
                  [inst_3 :
                      CategoryTheory.Limits.HasPushout
                        (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄] →
                    CategoryTheory.Limits.IsColimit
                      (CategoryTheory.Limits.PushoutCocone.mk
                        (CategoryTheory.Limits.pushout.inl
                          (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
                        (CategoryTheory.Limits.pushout.desc
                          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pushout.inr g₁ g₂)
                            (CategoryTheory.Limits.pushout.inl
                              (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄))
                          (CategoryTheory.Limits.pushout.inr
                            (CategoryTheory.CategoryStruct.comp g₃ (CategoryTheory.Limits.pushout.inr g₁ g₂)) g₄)
                          ⋯)
                        ⋯)
-- Mathlib.Algebra.Group.TypeTags.Basic
Multiplicative.div : {α : Type u} → [Sub α] → Div (Multiplicative α)
-- Init.Data.SInt.Lemmas
Int32.ofIntLE_int64ToInt : ∀ (x : Int64) {h₁ : Int32.minValue.toInt ≤ x.toInt} {h₂ : x.toInt ≤ Int32.maxValue.toInt},
  Int32.ofIntLE x.toInt h₁ h₂ = x.toInt32
-- Mathlib.Analysis.Normed.Group.Basic
enorm'_le_iff_norm_le : ∀ {E : Type u_5} {F : Type u_6} [inst : SeminormedGroup E] [inst_1 : SeminormedGroup F] {x : E} {y : F},
  ‖x‖ₑ ≤ ‖y‖ₑ ↔ ‖x‖ ≤ ‖y‖
-- Aesop.RuleSet.Member
Aesop.BaseRuleSetMember.normForwardRule.inj : ∀ {r₁ : Aesop.ForwardRule} {r₂ : Aesop.NormRule} {r₁_1 : Aesop.ForwardRule} {r₂_1 : Aesop.NormRule},
  Aesop.BaseRuleSetMember.normForwardRule r₁ r₂ = Aesop.BaseRuleSetMember.normForwardRule r₁_1 r₂_1 →
    r₁ = r₁_1 ∧ r₂ = r₂_1
-- Init.Data.List.Impl
_private.Init.Data.List.Impl.0.List.takeWhileTR.go.eq_def : ∀ {α : Type u_1} (p : α → Bool) (l a : List α) (a_1 : Array α),
  List.takeWhileTR.go✝ p l a a_1 =
    match a, a_1 with
    | [], x => l
    | a :: as, acc => bif p a then List.takeWhileTR.go✝ p l as (acc.push a) else acc.toList
-- Lean.LibrarySuggestions.Basic
/-- An optional arbitrary "hint" to the premise selection algorithm.
There is no guarantee that the algorithm will make any use of the hint.

Potential use cases include a natural language comment provided by the user
(e.g. allowing use of the premise selector as a search engine)
or including context from the current proof and/or file.

We may later split these use cases into separate fields if necessary.
 -/
Lean.LibrarySuggestions.Config.hint : Lean.LibrarySuggestions.Config → Option String
-- Mathlib.Data.Quot
Trunc.exists_rep : ∀ {α : Sort u_1} (q : Trunc α), ∃ a, Trunc.mk a = q
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.instInhabited : (A : Type u_2) →
  (B : Type u_3) →
    [inst : Monoid A] →
      [inst_1 : Monoid B] → [inst_2 : TopologicalSpace A] → [inst_3 : TopologicalSpace B] → Inhabited (A →ₜ* B)
-- Mathlib.Algebra.Field.Subfield.Basic
/-- Subfield closure of a set is monotone in its argument: if `s ⊆ t`,
then `closure s ≤ closure t`.  -/
Subfield.closure_mono : ∀ {K : Type u} [inst : DivisionRing K] ⦃s t : Set K⦄, s ⊆ t → Subfield.closure s ≤ Subfield.closure t
-- Mathlib.FieldTheory.SplittingField.Construction
Polynomial.irreducible_factor : ∀ {K : Type v} [inst : Field K] (f : Polynomial K), Irreducible f.factor
-- Init.Data.Format.Basic
Std.Format.append.inj : ∀ {a a_1 a_2 a_3 : Std.Format}, a.append a_1 = a_2.append a_3 → a = a_2 ∧ a_1 = a_3
-- Mathlib.Algebra.Star.BigOperators
star_prod : ∀ {R : Type u_1} [inst : CommMonoid R] [inst_1 : StarMul R] {α : Type u_2} (s : Finset α) (f : α → R),
  star (∏ x ∈ s, f x) = ∏ x ∈ s, star (f x)