mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.coe_curry : ∀ (R : Type u_1) (M : Type u_5) [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] (V : Type u_9)
  (V₂ : Type u_10), ⇑(LinearEquiv.curry R M V V₂) = Function.curry
-- Mathlib.Data.Finset.Image
/-- `filterMap f s` is a combination filter/map operation on `s`.
The function `f : α → Option β` is applied to each element of `s`;
if `f a` is `some b` then `b` is included in the result, otherwise
`a` is excluded from the resulting finset.

In notation, `filterMap f s` is the finset `{b : β | ∃ a ∈ s, f a = some b}`.  -/
Finset.filterMap : {α : Type u_1} →
  {β : Type u_2} → (f : α → Option β) → Finset α → (∀ (a a' : α), ∀ b ∈ f a, b ∈ f a' → a = a') → Finset β
-- Mathlib.Order.UpperLower.CompleteLattice
LowerSet.map_refl : ∀ {α : Type u_1} [inst : Preorder α], LowerSet.map (OrderIso.refl α) = OrderIso.refl (LowerSet α)
-- Mathlib.Data.Matrix.Block
Matrix.comp_diagonal : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_14} [inst : Zero R] [inst_1 : DecidableEq m] (d : m → Matrix n n R),
  (Matrix.comp m m n n R) (Matrix.diagonal d) =
    (Matrix.reindex (Equiv.prodComm n m) (Equiv.prodComm n m)) (Matrix.blockDiagonal d)
-- Init.Data.Array.Monadic
Array.filterMapM.eq_1 : ∀ {α : Type u} {m : Type u_1 → Type u_2} {β : Type u_1} [inst : Monad m] (f : α → m (Option β)) (as : Array α)
  (start stop : ℕ),
  Array.filterMapM f as start stop =
    Array.foldlM
      (fun bs a => do
        let __do_lift ← f a
        match __do_lift with
          | some b => pure (bs.push b)
          | none => pure bs)
      #[] as start stop
-- Init.Grind.Ring.CommSolver
Lean.Grind.CommRing.Var.revlex.eq_1 : ∀ (x y : Lean.Grind.CommRing.Var),
  x.revlex y = bif Nat.blt x y then Ordering.gt else bif Nat.blt y x then Ordering.lt else Ordering.eq
-- Mathlib.NumberTheory.ModularForms.Basic
CuspFormClass.zero_at_cusps : ∀ {F : Type u_2} {Γ : outParam (Subgroup (GL (Fin 2) ℝ))} {k : outParam ℤ} {inst : FunLike F UpperHalfPlane ℂ}
  [self : CuspFormClass F Γ k] (f : F) {c : OnePoint ℝ}, IsCusp c Γ → c.IsZeroAt (⇑f) k
-- Mathlib.ModelTheory.LanguageMap
FirstOrder.Language.LHom.Injective.onRelation : ∀ {L : FirstOrder.Language} {L' : FirstOrder.Language} {ϕ : L →ᴸ L'},
  ϕ.Injective → ∀ {n : ℕ}, Function.Injective fun R => ϕ.onRelation R
-- Lean.Elab.DocString
/-- Runs a documentation elaborator in the module docstring context.
 -/
Lean.Doc.DocM.execForModule : {α : Type} →
  Lean.Doc.DocM α →
    optParam Lean.Doc.SuggestionMode Lean.Doc.SuggestionMode.interactive →
      Lean.Elab.TermElabM (α × Array Lean.Doc.DeferredCheck)
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Connected
SimpleGraph.Connected.mono : ∀ {V : Type u} {G G' : SimpleGraph V}, G ≤ G' → G.Connected → G'.Connected
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.Const.getD_inter_of_not_mem_left : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ : Std.ExtDHashMap α fun x => β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k : α} {fallback : β},
  k ∉ m₁ → Std.ExtDHashMap.Const.getD (m₁ ∩ m₂) k fallback = fallback
-- Mathlib.Algebra.Ring.IsFormallyReal
IsFormallyReal.not_isSumNonzeroSq_zero : ∀ {R : Type u_1} {inst : AddCommMonoid R} {inst_1 : Mul R} [self : IsFormallyReal R], ¬IsSumNonzeroSq 0
-- Mathlib.Order.Filter.Pointwise
/-- `Filter α` is a `CommSemigroup` under pointwise operations if `α` is.  -/
Filter.commSemigroup : {α : Type u_2} → [CommSemigroup α] → CommSemigroup (Filter α)
-- Mathlib.ModelTheory.Order
/-- A sentence indicating that an order has no bottom element:
$\forall x, \exists y, \neg x \le y$.  -/
FirstOrder.Language.noBotOrderSentence : (L : FirstOrder.Language) → [L.IsOrdered] → L.Sentence
-- Mathlib.Tactic.FieldSimp
_private.Mathlib.Tactic.FieldSimp.0.Mathlib.Tactic.FieldSimp.qNF.mkMulProof.match_1.eq_3 : ∀ {v : Lean.Level} {M : Q(Type v)} (motive : Mathlib.Tactic.FieldSimp.qNF M → Mathlib.Tactic.FieldSimp.qNF M → Sort u_1)
  (a₁ : ℤ) (x₁ : Q(«$M»)) (k₁ : ℕ) (t₁ : List ((ℤ × Q(«$M»)) × ℕ)) (a₂ : ℤ) (x₂ : Q(«$M»)) (k₂ : ℕ)
  (t₂ : List ((ℤ × Q(«$M»)) × ℕ)) (h_1 : (l : Mathlib.Tactic.FieldSimp.qNF M) → motive [] l)
  (h_2 : (l : Mathlib.Tactic.FieldSimp.qNF M) → motive l [])
  (h_3 :
    (a₁ : ℤ) →
      (x₁ : Q(«$M»)) →
        (k₁ : ℕ) →
          (t₁ : List ((ℤ × Q(«$M»)) × ℕ)) →
            (a₂ : ℤ) →
              (x₂ : Q(«$M»)) →
                (k₂ : ℕ) → (t₂ : List ((ℤ × Q(«$M»)) × ℕ)) → motive (((a₁, x₁), k₁) :: t₁) (((a₂, x₂), k₂) :: t₂)),
  (match ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ with
    | [], l => h_1 l
    | l, [] => h_2 l
    | ((a₁, x₁), k₁) :: t₁, ((a₂, x₂), k₂) :: t₂ => h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂) =
    h_3 a₁ x₁ k₁ t₁ a₂ x₂ k₂ t₂
-- Mathlib.RingTheory.MvPolynomial.Basic
MvPolynomial.mem_restrictDegree : ∀ (σ : Type u) {R : Type v} [inst : CommSemiring R] (p : MvPolynomial σ R) (n : ℕ),
  p ∈ MvPolynomial.restrictDegree σ R n ↔ ∀ s ∈ p.support, ∀ (i : σ), s i ≤ n
-- Mathlib.Data.Finset.Grade
Finset.grade_multiset_eq : ∀ {α : Type u_1} (s : Finset α), grade (Multiset α) s = s.val
-- Mathlib.Algebra.Free
FreeSemigroup.recOnPure.eq_1 : ∀ {α : Type u} {C : FreeSemigroup α → Sort l} (x : FreeSemigroup α) (ih1 : (x : α) → C (pure x))
  (ih2 : (x : α) → (y : FreeSemigroup α) → C (pure x) → C y → C (pure x * y)), x.recOnPure ih1 ih2 = x.recOnMul ih1 ih2
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.splitAux.eq_def : ∀ (s : String) (p : Char → Bool) (b i : String.Pos.Raw) (r : List String),
  s.splitAux p b i r =
    if h : String.Pos.Raw.atEnd s i = true then
      have r := String.Pos.Raw.extract s b i :: r;
      r.reverse
    else
      have this := ⋯;
      if p (String.Pos.Raw.get s i) = true then
        have i' := String.Pos.Raw.next s i;
        s.splitAux p i' i' (String.Pos.Raw.extract s b i :: r)
      else s.splitAux p b (String.Pos.Raw.next s i) r
-- Mathlib.LinearAlgebra.CliffordAlgebra.BaseChange
/-- The involution acts only on the right of the tensor product.  -/
CliffordAlgebra.toBaseChange_involute : ∀ {R : Type u_1} (A : Type u_2) {V : Type u_3} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : AddCommGroup V]
  [inst_3 : Algebra R A] [inst_4 : Module R V] [inst_5 : Invertible 2] (Q : QuadraticForm R V)
  (x : CliffordAlgebra (QuadraticForm.baseChange A Q)),
  (CliffordAlgebra.toBaseChange A Q) (CliffordAlgebra.involute x) =
    (TensorProduct.map LinearMap.id CliffordAlgebra.involute.toLinearMap) ((CliffordAlgebra.toBaseChange A Q) x)
-- Mathlib.RingTheory.PrincipalIdealDomain
PrincipalIdealRing.mem_submonoid_of_factors_subset_of_units_subset : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsPrincipalIdealRing R] (s : Submonoid R) {a : R},
  a ≠ 0 → (∀ b ∈ PrincipalIdealRing.factors a, b ∈ s) → (∀ (c : Rˣ), ↑c ∈ s) → a ∈ s
-- Init.Core
Thunk.mk.injEq : ∀ {α : Type u} (fn fn_1 : Unit → α), ({ fn := fn } = { fn := fn_1 }) = (fn = fn_1)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.get_alter!_self : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  [inst_1 : Std.LawfulEqOrd α] (h : t.WF) {k : α} {f : Option (β k) → Option (β k)}
  {hc : k ∈ Std.DTreeMap.Internal.Impl.alter! k f t},
  (Std.DTreeMap.Internal.Impl.alter! k f t).get k hc = (f (t.get? k)).get ⋯
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.equivFun_self : ∀ {ι : Type u_1} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : Finite ι] [inst_4 : DecidableEq ι] (b : Module.Basis ι R M) (i j : ι),
  b.equivFun (b i) j = if i = j then 1 else 0
-- Init.Data.Int.Gcd
Int.gcd_zero : ∀ {a : ℤ}, a.gcd 0 = a.natAbs
-- Mathlib.Topology.Order
TopologicalSpace.generateFrom_anti : ∀ {α : Type u_1} {g₁ g₂ : Set (Set α)}, g₁ ⊆ g₂ → TopologicalSpace.generateFrom g₂ ≤ TopologicalSpace.generateFrom g₁
-- Mathlib.RingTheory.NormalClosure
/-- This is a local instance since it is only used in this file to construct `Ring.NormalClosure`.
 -/
Ring.instAlgebraNormalClosureSubtypeAlgebraicClosureFractionRingMemIntermediateFieldNormalClosure : (R : Type u_1) →
  (S : Type u_2) →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        [inst_2 : IsDomain R] →
          [inst_3 : IsDomain S] →
            [inst_4 : Algebra R S] →
              [inst_5 : Module.IsTorsionFree R S] →
                Algebra (Ring.NormalClosure R S)
                  ↥(IntermediateField.normalClosure (FractionRing R) (FractionRing S)
                      (AlgebraicClosure (FractionRing S)))
-- Mathlib.Algebra.CubicDiscriminant
Cubic.mk.inj : ∀ {R : Type u_1} {a b c d a_1 b_1 c_1 d_1 : R},
  { a := a, b := b, c := c, d := d } = { a := a_1, b := b_1, c := c_1, d := d_1 } →
    a = a_1 ∧ b = b_1 ∧ c = c_1 ∧ d = d_1
-- Std.Time.DateTime.WallTime
Std.Time.WallTime.instHAddOffset_1 : HAdd Std.Time.WallTime Std.Time.Week.Offset Std.Time.WallTime
-- Mathlib.Algebra.MonoidAlgebra.Module
/-- The image of an element `m : M` in `R[M]` belongs the submodule generated by
`s : Set M` if and only if `m ∈ s`.  -/
AddMonoidAlgebra.of'_mem_span : ∀ {R : Type u_1} {M : Type u_3} [inst : Semiring R] [Nontrivial R] {m : M} {s : Set M},
  AddMonoidAlgebra.of' R M m ∈ Submodule.span R (AddMonoidAlgebra.of' R M '' s) ↔ m ∈ s
-- Mathlib.Data.Multiset.Bind
Multiset.prod_map_product_eq_prod_prod : ∀ {α : Type u_1} {β : Type v} {M : Type u_4} [inst : CommMonoid M] (s : Multiset α) (t : Multiset β) (f : α × β → M),
  (Multiset.map f (s ×ˢ t)).prod = (Multiset.map (fun i => (Multiset.map (fun j => f (i, j)) t).prod) s).prod
-- Mathlib.Algebra.Order.Group.Indicator
Set.le_mulIndicator : ∀ {α : Type u_2} {M : Type u_3} [inst : LE M] [inst_1 : One M] {s : Set α} {f g : α → M},
  (∀ a ∈ s, f a ≤ g a) → (∀ a ∉ s, f a ≤ 1) → f ≤ s.mulIndicator g
-- Mathlib.Topology.GDelta.Basic
isGδ_iff_eq_iInter_nat : ∀ {X : Type u_1} [inst : TopologicalSpace X] {s : Set X}, IsGδ s ↔ ∃ f, (∀ (n : ℕ), IsOpen (f n)) ∧ s = ⋂ n, f n
-- Mathlib.Analysis.Normed.Group.Pointwise
ediam_add_le : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (x y : Set E), Metric.ediam (x + y) ≤ Metric.ediam x + Metric.ediam y
-- Mathlib.CategoryTheory.Skeletal
/-- An inverse to `fromSkeleton C` that forms an equivalence with it.  -/
CategoryTheory.toSkeletonFunctor : (C : Type u₁) → [inst : CategoryTheory.Category.{v₁, u₁} C] → CategoryTheory.Functor C (CategoryTheory.Skeleton C)
-- Init.Data.Vector.OfFn
_private.Init.Data.Vector.OfFn.0.Vector.ofFnM.go.induct_unfolding : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} {n : ℕ} [inst : Monad m] (f : Fin n → m α)
  (motive : (i : ℕ) → i ≤ n → (acc : Array α) → acc.size = i → m (Vector α n) → Prop),
  (∀ (acc : Array α) (h' : acc.size ≤ n) (h : acc.size < n),
      (∀ (__do_lift : α),
          motive (acc.size + 1) ⋯ (acc.push __do_lift) ⋯ (Vector.ofFnM.go✝ f (acc.size + 1) ⋯ (acc.push __do_lift) ⋯)) →
        motive acc.size h' acc ⋯ do
          let __do_lift ← f ⟨acc.size, h⟩
          Vector.ofFnM.go✝ f (acc.size + 1) ⋯ (acc.push __do_lift) ⋯) →
    (∀ (acc : Array α) (h' : acc.size ≤ n) (h : ¬acc.size < n), motive acc.size h' acc ⋯ (pure (Vector.mk acc ⋯))) →
      ∀ (i : ℕ) (h' : i ≤ n) (acc : Array α) (w : acc.size = i), motive i h' acc w (Vector.ofFnM.go✝ f i h' acc w)
-- Mathlib.Topology.MetricSpace.Similarity
/-- Similarity holds if and only if all extended distances are proportional.  -/
similar_iff_exists_edist_eq : ∀ {ι : Type u_1} {P₁ : Type u_3} {P₂ : Type u_4} {v₁ : ι → P₁} {v₂ : ι → P₂} [inst : PseudoEMetricSpace P₁]
  [inst_1 : PseudoEMetricSpace P₂],
  Similar v₁ v₂ ↔ ∃ r, r ≠ 0 ∧ ∀ (i₁ i₂ : ι), edist (v₁ i₁) (v₁ i₂) = ↑r * edist (v₂ i₁) (v₂ i₂)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.mulSingle.eq_1 : ∀ {ι : Type u_1} {S : ι → Type u_3} {G : ι → Type u_4} [inst : (i : ι) → SetLike (S i) (G i)] (A : (i : ι) → S i)
  [inst_1 : DecidableEq ι] [inst_2 : (i : ι) → One (G i)] [inst_3 : ∀ (i : ι), OneMemClass (S i) (G i)] (i : ι)
  (x : G i), RestrictedProduct.mulSingle A i x = ⟨Pi.mulSingle i x, ⋯⟩
-- Mathlib.Algebra.Homology.TotalComplex
HomologicalComplex₂.D₂_shape : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C] {I₁ : Type u_2}
  {I₂ : Type u_3} {I₁₂ : Type u_4} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂} (K : HomologicalComplex₂ C c₁ c₂)
  (c₁₂ : ComplexShape I₁₂) [inst_2 : TotalComplexShape c₁ c₂ c₁₂] [inst_3 : DecidableEq I₁₂] [inst_4 : K.HasTotal c₁₂]
  (i₁₂ i₁₂' : I₁₂), ¬c₁₂.Rel i₁₂ i₁₂' → K.D₂ c₁₂ i₁₂ i₁₂' = 0
-- Init.Data.Sum.Lemmas
Sum.liftRel_swap_iff : ∀ {β : Type u_1} {β_1 : Type u_2} {s : β → β_1 → Prop} {α : Type u_3} {α_1 : Type u_4} {r : α → α_1 → Prop} {x : α ⊕ β}
  {y : α_1 ⊕ β_1}, Sum.LiftRel s r x.swap y.swap ↔ Sum.LiftRel r s x y
-- Mathlib.Algebra.Category.ModuleCat.Differentials.Presheaf
PresheafOfModules.Derivation.Universal.mk : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {S : CategoryTheory.Functor Cᵒᵖ CommRingCat} →
          {F : CategoryTheory.Functor C D} →
            {R : CategoryTheory.Functor Dᵒᵖ CommRingCat} →
              {M : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
                {φ : S ⟶ F.op.comp R} →
                  {d : M.Derivation φ} →
                    (desc :
                        {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))} →
                          M'.Derivation φ → (M ⟶ M')) →
                      autoParam
                          (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))}
                            (d' : M'.Derivation φ), d.postcomp (desc d') = d')
                          PresheafOfModules.Derivation.Universal.fac._autoParam →
                        autoParam
                            (∀ {M' : PresheafOfModules (R.comp (CategoryTheory.forget₂ CommRingCat RingCat))}
                              (φ_1 φ' : M ⟶ M'), d.postcomp φ_1 = d.postcomp φ' → φ_1 = φ')
                            PresheafOfModules.Derivation.Universal.postcomp_injective._autoParam →
                          d.Universal
-- Mathlib.Algebra.Category.BialgCat.Monoidal
/-- The data needed to induce a `MonoidalCategory` structure via
`BialgCat.instMonoidalCategoryStruct` and the forgetful functor to algebras.  -/
BialgCat.MonoidalCategory.inducingFunctorData : (R : Type u) →
  [inst : CommRing R] → CategoryTheory.Monoidal.InducingFunctorData (CategoryTheory.forget₂ (BialgCat R) (AlgCat R))
-- Mathlib.CategoryTheory.Galois.Basic
/-- The fiber of the binary product is the binary product of the fibers.  -/
CategoryTheory.PreGaloisCategory.fiberBinaryProductEquiv : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    (F : CategoryTheory.Functor C FintypeCat) →
      [inst_1 : CategoryTheory.PreGaloisCategory C] →
        [CategoryTheory.PreGaloisCategory.FiberFunctor F] →
          (X Y : C) → (F.obj (X ⨯ Y)).obj ≃ (F.obj X).obj × (F.obj Y).obj
-- Mathlib.Order.Hom.Lattice
InfHom.comp_assoc : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} {δ : Type u_5} [inst : Min α] [inst_1 : Min β] [inst_2 : Min γ]
  [inst_3 : Min δ] (f : InfHom γ δ) (g : InfHom β γ) (h : InfHom α β), (f.comp g).comp h = f.comp (g.comp h)
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.getKey_congr : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} [inst : Std.TransCmp cmp] {k₁ k₂ : α}
  (h' : cmp k₁ k₂ = Ordering.eq) (h₁ : k₁ ∈ t), t.getKey k₁ h₁ = t.getKey k₂ ⋯
-- Std.Tactic.BVDecide.LRAT.Internal.Assignment
Std.Tactic.BVDecide.LRAT.Internal.Assignment.has_remove_irrelevant : ∀ (assignment : Std.Tactic.BVDecide.LRAT.Internal.Assignment) (b : Bool),
  Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b
        (Std.Tactic.BVDecide.LRAT.Internal.Assignment.removeAssignment (!b) assignment) =
      true →
    Std.Tactic.BVDecide.LRAT.Internal.Assignment.hasAssignment b assignment = true
-- Mathlib.Combinatorics.SimpleGraph.FiveWheelLike
/-- If `G` is `Kᵣ₊₂`-free and contains a `Wᵣ,ₖ` together with a vertex `x` adjacent to all but at most
two vertices of `Wᵣ,ₖ`, including all of its common clique vertices, then `G` contains a `Wᵣ,ₖ₊₁`.
 -/
SimpleGraph.IsFiveWheelLike.exists_isFiveWheelLike_succ_of_not_adj_le_two : ∀ {α : Type u_1} {G : SimpleGraph α} {r k : ℕ} {x v w₁ w₂ : α} {s t : Finset α} [inst : DecidableEq α],
  G.IsFiveWheelLike r k v w₁ w₂ s t →
    G.CliqueFree (r + 2) →
      ∀ [inst_1 : DecidableRel G.Adj],
        (∀ ⦃y : α⦄, y ∈ s ∩ t → G.Adj x y) →
          {z ∈ {v} ∪ ({w₁} ∪ ({w₂} ∪ (s ∪ t))) | ¬G.Adj x z}.card ≤ 2 →
            ∃ a b, G.IsFiveWheelLike r (k + 1) v w₁ w₂ (insert x (s.erase a)) (insert x (t.erase b))
-- Mathlib.LinearAlgebra.Trace
LinearMap.trace_smulRight : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Free R M]
  [Module.Finite R M] (f : M →ₗ[R] R) (x : M), (LinearMap.trace R M) (f.smulRight x) = f x
-- Mathlib.Topology.UniformSpace.Closeds
TopologicalSpace.Compacts.continuous_toCloseds : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : T2Space α], Continuous TopologicalSpace.Compacts.toCloseds
-- Mathlib.CategoryTheory.ObjectProperty.ClosedUnderIsomorphisms
CategoryTheory.ObjectProperty.prop_isoClosure : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {P : CategoryTheory.ObjectProperty C} {X Y : C},
  P X → ∀ (e : X ⟶ Y) [CategoryTheory.IsIso e], P.isoClosure Y
-- Mathlib.Algebra.Polynomial.Degree.Lemmas
Polynomial.natDegree_map_eq_iff : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial R},
  (Polynomial.map f p).natDegree = p.natDegree ↔ f p.leadingCoeff ≠ 0 ∨ p.natDegree = 0
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.instIsDenseSubsiteCoherentTopologyInverse : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Precoherent C] (e : C ≌ D),
  CategoryTheory.Functor.IsDenseSubsite (CategoryTheory.coherentTopology D) (CategoryTheory.coherentTopology C)
    e.inverse
-- Mathlib.CategoryTheory.MorphismProperty.Composition
/-- `multiplicativeClosure' W` is multiplicative.  -/
CategoryTheory.MorphismProperty.instIsMultiplicativeMultiplicativeClosure' : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (W : CategoryTheory.MorphismProperty C),
  W.multiplicativeClosure'.IsMultiplicative
-- Mathlib.Order.UpperLower.Closure
UpperSet.iInf_Ici : ∀ {α : Type u_1} [inst : Preorder α] (s : Set α), ⨅ a ∈ s, UpperSet.Ici a = upperClosure s
-- Mathlib.Topology.Sets.Opens
TopologicalSpace.Opens.comap_injective : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] [T0Space β],
  Function.Injective TopologicalSpace.Opens.comap
-- Mathlib.GroupTheory.Finiteness
GroupFG.iff_add_fg : ∀ {G : Type u_3} [inst : Group G], Group.FG G ↔ AddGroup.FG (Additive G)
-- Mathlib.AlgebraicGeometry.Morphisms.Flat
AlgebraicGeometry.Flat.instOfIsOpenImmersion : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [AlgebraicGeometry.IsOpenImmersion f], AlgebraicGeometry.Flat f
-- Lean.Meta.Sym.AlphaShareBuilder
/-- `mkAppNS f #[a₀, ..., aₙ]` constructs `f a₀ ... aₙ` with max sharing.  -/
Lean.Meta.Sym.Internal.mkAppNS : {m : Type → Type} → [Lean.Meta.Sym.Internal.MonadShareCommon m] → [Monad m] → Lean.Expr → Array Lean.Expr → m Lean.Expr
-- Mathlib.Algebra.Group.Units.Defs
/-- Additive units of an additive monoid form a `SubNegMonoid`.  -/
AddUnits.instSubNegAddMonoid : {α : Type u} → [inst : AddMonoid α] → SubNegMonoid (AddUnits α)
-- Mathlib.Combinatorics.Additive.CovBySMul
CovByVAdd.subset : ∀ {M : Type u_1} {X : Type u_3} [inst : AddMonoid M] [inst_1 : AddAction M X] {K : ℝ} {A₁ A₂ B₁ B₂ : Set X},
  A₁ ⊆ A₂ → B₁ ⊆ B₂ → CovByVAdd M K A₂ B₁ → CovByVAdd M K A₁ B₂
-- Mathlib.GroupTheory.MonoidLocalization.Maps
AddLocalization.addEquivOfQuotient_apply : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N]
  {f : S.LocalizationMap N} (x : AddLocalization S),
  (AddLocalization.addEquivOfQuotient f) x = ((AddLocalization.addMonoidOf S).lift ⋯) x
-- Mathlib.RingTheory.Bialgebra.Quotient
Bialgebra.Quotient.comulAlgHom.congr_simp : ∀ {R : Type u_1} {A : Type u_2} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Bialgebra R A] (I : Ideal A)
  [inst_3 : I.IsTwoSided] [inst_4 : (Submodule.restrictScalars R I).IsCoideal],
  Bialgebra.Quotient.comulAlgHom I = Bialgebra.Quotient.comulAlgHom I
-- Mathlib.MeasureTheory.Function.LpSeminorm.LpNorm
MeasureTheory.toReal_eLpNorm : ∀ {α : Type u_1} {E : Type u_2} {m : MeasurableSpace α} {p : ENNReal} {μ : MeasureTheory.Measure α}
  [inst : NormedAddCommGroup E] {f : α → E},
  MeasureTheory.AEStronglyMeasurable f μ → (MeasureTheory.eLpNorm f p μ).toReal = MeasureTheory.lpNorm f p μ
-- Mathlib.GroupTheory.DoubleCoset
/-- Quotient of `G` by the double coset relation, i.e. `H \ G / K`  -/
DoubleCoset.Quotient : {G : Type u_1} → [Group G] → Set G → Set G → Type u_1
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_sInf : ∀ {R : Type u} [inst : NonAssocRing R] (S : Set (Subring R)), ↑(sInf S) = ⋂ s ∈ S, ↑s
-- Mathlib.RingTheory.NonUnitalSubring.Basic
/-- The ring equiv between the top element of `NonUnitalSubring R` and `R`.  -/
NonUnitalSubring.topEquiv : {R : Type u} → [inst : NonUnitalNonAssocRing R] → ↥⊤ ≃+* R
-- Mathlib.Algebra.GroupWithZero.Action.Defs
left_ne_zero_of_smul : ∀ {M₀ : Type u_2} {A : Type u_7} [inst : Zero M₀] [inst_1 : Zero A] [inst_2 : SMulWithZero M₀ A] {a : M₀} {b : A},
  a • b ≠ 0 → a ≠ 0
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.Splits.comp_of_degree_le_one_of_invertible : ∀ {R : Type u_1} [inst : CommSemiring R] {f g : Polynomial R},
  f.Splits → g.degree ≤ 1 → ∀ (h : Invertible g.leadingCoeff), (f.comp g).Splits
-- Mathlib.Algebra.Group.Hom.Defs
/-- Turn an element of a type `F` satisfying `MonoidHomClass F M N` into an actual
`MonoidHom`. This is declared as the default coercion from `F` to `M →* N`.  -/
MonoidHomClass.toMonoidHom : {M : Type u_4} →
  {N : Type u_5} →
    {F : Type u_9} →
      [inst : MulOne M] → [inst_1 : MulOne N] → [inst_2 : FunLike F M N] → [MonoidHomClass F M N] → F → M →* N
-- Mathlib.CategoryTheory.Bicategory.Product
/-- `snd` is the strict pseudofunctor given by projection to the second factor.  -/
CategoryTheory.Bicategory.Prod.snd : (B : Type u₁) →
  [inst : CategoryTheory.Bicategory B] →
    (C : Type u₂) → [inst_1 : CategoryTheory.Bicategory C] → CategoryTheory.StrictPseudofunctor (B × C) C
-- Init.Data.List.Lemmas
List.getElem?_eq_some_iff : ∀ {α : Type u_1} {i : ℕ} {a : α} {l : List α}, l[i]? = some a ↔ ∃ (h : i < l.length), l[i] = a
-- Mathlib.Topology.MetricSpace.Thickening
Metric.closure_thickening_subset_cthickening : ∀ {α : Type u} [inst : PseudoEMetricSpace α] (δ : ℝ) (E : Set α),
  closure (Metric.thickening δ E) ⊆ Metric.cthickening δ E
-- Mathlib.RingTheory.FormalGroup.Basic
/-- The underlying power series $F(X, Y)$ in two variables.  -/
FormalGroup.toPowerSeries : {R : Type u_1} → [inst : CommRing R] → FormalGroup R → MvPowerSeries (Fin 2) R
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.Shrink.instCategoryShrink : (C : Type u) →
  [CategoryTheory.Category.{v, u} C] → [inst : Small.{w, u} C] → CategoryTheory.Category.{v, w} (Shrink.{w, u} C)
-- Mathlib.Data.Subtype
Subtype.val_injective : ∀ {α : Sort u_1} {p : α → Prop}, Function.Injective Subtype.val
-- Init.Grind.Attr
/-- Similar to `genPattern` but for the heterogeneous case  -/
Lean.Grind.genHEqPattern : {α β : Sort u} → Prop → α → β → α
-- Mathlib.Data.Fintype.Sets
/-- **Alias** of the reverse direction of `Set.toFinset_nonempty`. -/
Set.Aesop.toFinset_nonempty_of_nonempty : ∀ {α : Type u_1} {s : Set α} [inst : Fintype ↑s], s.Nonempty → s.toFinset.Nonempty
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.coeff_inv_aux : ∀ {σ : Type u_1} {R : Type u_2} [inst : Ring R] [inst_1 : DecidableEq σ] (n : σ →₀ ℕ) (a : R) (φ : MvPowerSeries σ R),
  (MvPowerSeries.coeff n) (MvPowerSeries.inv.aux a φ) =
    if n = 0 then a
    else
      -a *
        ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n,
          if x.2 < n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) (MvPowerSeries.inv.aux a φ) else 0