mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Data.Multiset.MapFold
Multiset.map_erase : ∀ {α : Type u_1} {β : Type v} [inst : DecidableEq α] [inst_1 : DecidableEq β] (f : α → β),
  Function.Injective f → ∀ (x : α) (s : Multiset α), Multiset.map f (s.erase x) = (Multiset.map f s).erase (f x)
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.not_mem_diff_of_not_mem_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.HashSet.Raw α} [EquivBEq α] [LawfulHashable α],
  m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₁ → k ∉ m₁ \ m₂
-- Mathlib.Algebra.Group.Prod
MulHom.prod.eq_1 : ∀ {M : Type u_3} {N : Type u_4} {P : Type u_5} [inst : Mul M] [inst_1 : Mul N] [inst_2 : Mul P] (f : M →ₙ* N)
  (g : M →ₙ* P), f.prod g = { toFun := Function.prod ⇑f ⇑g, map_mul' := ⋯ }
-- Mathlib.RingTheory.DividedPowers.DPMorphism
DividedPowers.IsDPMorphism.ideal_comp : ∀ {A : Type u_1} {B : Type u_2} [inst : CommSemiring A] [inst_1 : CommSemiring B] {I : Ideal A} {J : Ideal B}
  {hI : DividedPowers I} {hJ : DividedPowers J} {f : A →+* B}, hI.IsDPMorphism hJ f → Ideal.map f I ≤ J
-- Mathlib.CategoryTheory.ConcreteCategory.EpiMono
CategoryTheory.ConcreteCategory.instEpiOfHomCoeHomOfPreservesEpimorphismsForget : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {FC : C → C → Type u_1} {CC : C → Type w}
  [inst_1 : (X Y : C) → FunLike (FC X Y) (CC X) (CC Y)] [inst_2 : CategoryTheory.ConcreteCategory C FC]
  [(CategoryTheory.forget C).PreservesEpimorphisms] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f],
  CategoryTheory.Epi (TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f))
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_27 : HSub Std.Time.Hour.Offset Std.Time.Minute.Offset Std.Time.Minute.Offset
-- Lean.ProjFns
/-- Number of parameters in the structure  -/
Lean.ProjectionFunctionInfo.numParams : Lean.ProjectionFunctionInfo → ℕ
-- Mathlib.LinearAlgebra.Matrix.NonsingularInverse
Matrix.isUnit_det_transpose : ∀ {n : Type u'} {α : Type v} [inst : Fintype n] [inst_1 : DecidableEq n] [inst_2 : CommRing α] (A : Matrix n n α),
  IsUnit A.det → IsUnit A.transpose.det
-- Lean.Log
/-- Log a new error/warning/information message using the given message data and `severity`. The position is provided by `getRef`.  -/
Lean.log : {m : Type → Type} →
  [Monad m] →
    [Lean.MonadLog m] →
      [Lean.AddMessageContext m] →
        [Lean.MonadOptions m] →
          Lean.MessageData → optParam Lean.MessageSeverity Lean.MessageSeverity.error → optParam Bool false → m Unit
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.insertMany.congr_simp : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} [inst : EquivBEq α] [inst_1 : LawfulHashable α] {ρ : Type w}
  [inst_2 : ForIn Id ρ (α × β)] (m m_1 : Std.ExtHashMap α β),
  m = m_1 → ∀ (l l_1 : ρ), l = l_1 → m.insertMany l = m_1.insertMany l_1
-- Mathlib.Order.BooleanSubalgebra
/-- A Boolean subalgebra of a lattice inherits a Heyting implication.  -/
BooleanSubalgebra.instHImpCoe : {α : Type u_2} → [inst : BooleanAlgebra α] → {L : BooleanSubalgebra α} → HImp ↥L
-- Std.Data.DHashMap.Internal.Model
_private.Std.Data.DHashMap.Internal.Model.0.Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit.eq_1 : ∀ {α : Type u} {ρ : Type w} [inst : ForIn Id ρ α] [inst_1 : BEq α] [inst_2 : Hashable α]
  (m : Std.DHashMap.Internal.Raw₀ α fun x => Unit) (l : ρ),
  Std.DHashMap.Internal.Raw₀.Const.insertManyIfNewUnit m l =
    (have r := ⟨m, ⋯⟩;
      do
      let __s ←
        forIn l r fun a __s =>
            let r := __s;
            have r := ⟨(↑r).insertIfNew a (), ⋯⟩;
            pure (ForInStep.yield r)
      have r :
        { m' //
          ∀ (P : (Std.DHashMap.Internal.Raw₀ α fun x => Unit) → Prop),
            (∀ {m'' : Std.DHashMap.Internal.Raw₀ α fun x => Unit} {a : α} {b : Unit}, P m'' → P (m''.insertIfNew a b)) →
              P m → P m' } :=
        __s
      pure r).run
-- Mathlib.Data.Set.Image
Set.coe_comp_rangeFactorization : ∀ {β : Type u_2} {ι : Sort u_4} (f : ι → β), Subtype.val ∘ Set.rangeFactorization f = f
-- Mathlib.MeasureTheory.Constructions.Pi
MeasureTheory.Measure.tprod_tprod : ∀ {δ : Type u_4} {X : δ → Type u_5} [inst : (i : δ) → MeasurableSpace (X i)] (l : List δ)
  (μ : (i : δ) → MeasureTheory.Measure (X i)) [∀ (i : δ), MeasureTheory.SigmaFinite (μ i)] (s : (i : δ) → Set (X i)),
  (MeasureTheory.Measure.tprod l μ) (Set.tprod l s) = (List.map (fun i => (μ i) (s i)) l).prod
-- Mathlib.Topology.Semicontinuity.Defs
/-- **Alias** of the reverse direction of `upperSemicontinuousOn_iff_frequently`. -/
UpperSemicontinuousOn.of_frequently : ∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace α] [inst_1 : LinearOrder β] {f : α → β} {s : Set α},
  (∀ x ∈ s, ∀ (y : β), (∃ᶠ (x' : α) in nhdsWithin x s, f x' ≥ y) → f x ≥ y) → UpperSemicontinuousOn f s
-- Mathlib.Tactic.Positivity.Core
Mathlib.Meta.Positivity.Strictness.positive.sizeOf_spec : ∀ {u : Lean.Level} {α : Q(Type u)} {zα : Q(Zero «$α»)} {e : Q(«$α»)} {pα : Q(PartialOrder «$α»)} (pf : Q(0 < «$e»)),
  sizeOf (Mathlib.Meta.Positivity.Strictness.positive pf) = 1 + sizeOf pα + sizeOf pf
-- Init.Data.List.Lemmas
List.head?_reverse : ∀ {α : Type u_1} {l : List α}, l.reverse.head? = l.getLast?
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.AddGrpObj.lift_neg_comp_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {A B : C} [inst_2 : CategoryTheory.AddGrpObj A] [inst_3 : CategoryTheory.AddGrpObj B] (f : A ⟶ B)
  [CategoryTheory.IsAddMonHom f],
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.CartesianMonoidalCategory.lift f
        (CategoryTheory.CategoryStruct.comp CategoryTheory.AddGrpObj.neg f))
      CategoryTheory.AddMonObj.add =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SemiCartesianMonoidalCategory.toUnit A)
      CategoryTheory.AddMonObj.zero
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.transpose_involutive : ∀ (n : Type u_3) (α : Type v), Function.Involutive Matrix.transpose
-- Lean.Data.Lsp.Workspace
Lean.Lsp.FileEvent.mk.injEq : ∀ (uri : Lean.Lsp.DocumentUri) (type : Lean.Lsp.FileChangeType) (uri_1 : Lean.Lsp.DocumentUri)
  (type_1 : Lean.Lsp.FileChangeType),
  ({ uri := uri, type := type } = { uri := uri_1, type := type_1 }) = (uri = uri_1 ∧ type = type_1)
-- Mathlib.Algebra.Category.CoalgCat.Basic
/-- Turn a morphism in `CoalgCat` back into a `CoalgHom`.  -/
CoalgCat.Hom.toCoalgHom : {R : Type u} → [inst : CommRing R] → {X Y : CoalgCat R} → X.Hom Y → ↑X.toModuleCat →ₗc[R] ↑Y.toModuleCat
-- Mathlib.FieldTheory.RatFunc.Basic
RatFunc.map_apply_ofFractionRing_mk : ∀ {R : Type u_3} {S : Type u_4} {F : Type u_5} [inst : CommRing R] [inst_1 : CommRing S]
  [inst_2 : FunLike F (Polynomial R) (Polynomial S)] [inst_3 : MonoidHomClass F (Polynomial R) (Polynomial S)] (φ : F)
  (hφ : nonZeroDivisors (Polynomial R) ≤ Submonoid.comap φ (nonZeroDivisors (Polynomial S))) (n : Polynomial R)
  (d : ↥(nonZeroDivisors (Polynomial R))),
  (RatFunc.map φ hφ) { toFractionRing := Localization.mk n d } = { toFractionRing := Localization.mk (φ n) ⟨φ ↑d, ⋯⟩ }
-- Mathlib.Util.Notation3
Mathlib.Notation3.instReprDelabKey.repr : Mathlib.Notation3.DelabKey → ℕ → Std.Format
-- Mathlib.FieldTheory.IsSepClosed
/-- Every separable polynomial splits in the field extension `f : k →+* K` if `K` is
separably closed.

See also `IsSepClosed.splits_domain` for the case where `k` is separably closed.
 -/
IsSepClosed.splits_codomain : ∀ {k : Type u} [inst : Field k] {K : Type v} [inst_1 : Field K] [IsSepClosed K] {f : k →+* K} (p : Polynomial k),
  p.Separable → (Polynomial.map f p).Splits
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.X_ne_zero : ∀ {R : Type u_1} [inst : Semiring R] [Nontrivial R], SkewPolynomial.X ≠ 0
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_mergeWith : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : Std.LawfulEqOrd α]
  {t₁ t₂ : Std.DTreeMap.Internal.Impl α β} {f : (a : α) → β a → β a → β a} (htb : t₁.Balanced),
  t₁.Ordered → (Std.DTreeMap.Internal.Impl.mergeWith f t₁ t₂ htb).impl.Ordered
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
/-- A structure on an oplax transformation that promotes it to a strong transformation.

See `StrongTrans.mkOfOplax`.  -/
CategoryTheory.Oplax.OplaxTrans.StrongCore : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {F G : CategoryTheory.OplaxFunctor B C} → (F ⟶ G) → Type (max (max u₁ v₁) w₂)
-- Init.Data.Int.Linear
_private.Init.Data.Int.Linear.0.Int.Internal.Linear.Expr.denote.match_1.eq_6 : ∀ (motive : Int.Internal.Linear.Expr → Sort u_1) (k : ℤ) (e : Int.Internal.Linear.Expr)
  (h_1 : (a b : Int.Internal.Linear.Expr) → motive (a.add b))
  (h_2 : (a b : Int.Internal.Linear.Expr) → motive (a.sub b)) (h_3 : (a : Int.Internal.Linear.Expr) → motive a.neg)
  (h_4 : (k : ℤ) → motive (Int.Internal.Linear.Expr.num k))
  (h_5 : (v : Int.Internal.Linear.Var) → motive (Int.Internal.Linear.Expr.var v))
  (h_6 : (k : ℤ) → (e : Int.Internal.Linear.Expr) → motive (Int.Internal.Linear.Expr.mulL k e))
  (h_7 : (e : Int.Internal.Linear.Expr) → (k : ℤ) → motive (e.mulR k)),
  (match Int.Internal.Linear.Expr.mulL k e with
    | a.add b => h_1 a b
    | a.sub b => h_2 a b
    | a.neg => h_3 a
    | Int.Internal.Linear.Expr.num k => h_4 k
    | Int.Internal.Linear.Expr.var v => h_5 v
    | Int.Internal.Linear.Expr.mulL k e => h_6 k e
    | e.mulR k => h_7 e k) =
    h_6 k e
-- Mathlib.Analysis.Complex.Basic
Complex.ofRealLI_apply : ∀ (x : ℝ), Complex.ofRealLI x = ↑x
-- Mathlib.Algebra.Polynomial.FieldDivision
Polynomial.mul_mod : ∀ {R : Type u} [inst : Field R] (p₁ p₂ q : Polynomial R), p₁ * p₂ % q = p₁ % q * (p₂ % q) % q
-- Mathlib.Topology.Algebra.UniformField
UniformSpace.Completion.coe_inv : ∀ {K : Type u_1} [inst : Field K] [inst_1 : UniformSpace K] [IsTopologicalDivisionRing K] [CompletableTopField K]
  (x : K), (↑x)⁻¹ = ↑x⁻¹
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.naturality'_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {n : ℕ} {F G : CategoryTheory.ComposableArrows C n}
  (φ : F ⟶ G) (i j : ℕ) (hij : autoParam (i ≤ j) CategoryTheory.ComposableArrows.naturality'._auto_1)
  (hj : autoParam (j ≤ n) CategoryTheory.ComposableArrows.naturality'._auto_3) {Z : C} (h : G.obj' j hj ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map' i j hij hj)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.app' φ j hj) h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ComposableArrows.app' φ i ⋯)
      (CategoryTheory.CategoryStruct.comp (G.map' i j hij hj) h)
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Limits.Types.colimit_eq : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)}
  [inst_1 : CategoryTheory.Limits.HasColimit F] {j j' : J} {x : F.obj j} {x' : F.obj j'},
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j)) x =
      (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.colimit.ι F j')) x' →
    Relation.EqvGen F.ColimitTypeRel ⟨j, x⟩ ⟨j', x'⟩
-- Mathlib.Algebra.Order.SuccPred
Order.le_sub_one_of_lt : ∀ {α : Type u_1} {x y : α} [inst : Preorder α] [inst_1 : Sub α] [inst_2 : One α] [PredSubOrder α], x < y → x ≤ y - 1
-- Batteries.Recycling.RBTree.Basic
/-- We say that `x < y` under the comparator `cmp` if `cmp x y = .lt`.

* In order to avoid assuming the comparator is always lawful, we use a
  local `∀ [Std.TransCmp cmp]` binder in the relation so that the ordering
  properties of the tree only need to hold if the comparator is lawful.
* The `Nonempty` wrapper is a no-op because this is already a proposition,
  but it prevents the `[Std.TransCmp cmp]` binder from being introduced when we don't want it.
 -/
RBTree.RBNode.cmpLT : {α : Type u_1} → (α → α → Ordering) → α → α → Prop
-- Mathlib.Algebra.Category.Ring.Colimits
/-- The Relation on `Prequotient` saying when two expressions are equal
because of the ring laws, or
because one element is mapped to another by a morphism in the diagram.
 -/
RingCat.Colimits.Relation : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] →
    (F : CategoryTheory.Functor J RingCat) → RingCat.Colimits.Prequotient F → RingCat.Colimits.Prequotient F → Prop
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.contains_erase : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp] {k a : α},
  (t.erase k).contains a = (cmp k a != Ordering.eq && t.contains a)
-- Mathlib.Algebra.Group.Subgroup.MulOpposite
Subgroup.unop_inj : ∀ {G : Type u_2} [inst : Group G] {S T : Subgroup Gᵐᵒᵖ}, S.unop = T.unop ↔ S = T
-- Mathlib.AlgebraicGeometry.Pullbacks
AlgebraicGeometry.Scheme.Pullback.cocycle_fst_fst_fst : ∀ {X Y Z : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (f : X ⟶ Z) (g : Y ⟶ Z)
  [inst : ∀ (i : 𝒰.I₀), CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g]
  (i j k : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g i j k)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g j k i)
        (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Pullback.t' 𝒰 f g k i j)
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
              (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
            (CategoryTheory.CategoryStruct.comp
              (CategoryTheory.Limits.pullback.fst
                (CategoryTheory.CategoryStruct.comp
                  (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
                (𝒰.f j))
              (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g))))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i j)
        (AlgebraicGeometry.Scheme.Pullback.fV 𝒰 f g i k))
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp
            (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g) (𝒰.f i))
          (𝒰.f j))
        (CategoryTheory.Limits.pullback.fst (CategoryTheory.CategoryStruct.comp (𝒰.f i) f) g))
-- Mathlib.CategoryTheory.Monoidal.Action.Opposites
CategoryTheory.MonoidalCategory.MonoidalRightAction.rightActionOfOppositeRightAction_actionRight_unop : ∀ (C : Type u_1) (D : Type u_2) [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.MonoidalCategory C] [inst_2 : CategoryTheory.Category.{v_2, u_2} D]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction Cᵒᵖ Dᵒᵖ] (d : Dᵒᵖ) {c c' : Cᵒᵖ} (f : c ⟶ c'),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight (Opposite.unop d) f.unop =
    Opposite.unop (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomRight d f)
-- Mathlib.Data.Matrix.Mul
Matrix.vecMul_ofNat : ∀ {m : Type u_2} {α : Type v} [inst : NonAssocSemiring α] [inst_1 : Fintype m] [inst_2 : DecidableEq m] (x : ℕ)
  [inst_3 : x.AtLeastTwo] (v : m → α), Matrix.vecMul v (OfNat.ofNat x) = MulOpposite.op (OfNat.ofNat x) • v
-- Init.Data.UInt.Bitwise
UInt8.neg_one_shiftLeft_and_shiftLeft : ∀ {a b : UInt8}, (-1) <<< b &&& a <<< b = a <<< b
-- Mathlib.CategoryTheory.Localization.CalculusOfFractions.Fractions
/-- the numerator of the third left fraction  -/
CategoryTheory.MorphismProperty.LeftFraction₃.f'' : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W : CategoryTheory.MorphismProperty C} → {X Y : C} → (self : W.LeftFraction₃ X Y) → X ⟶ self.Y'
-- Mathlib.CategoryTheory.Sites.SheafCohomology.MayerVietoris
CategoryTheory.GrothendieckTopology.MayerVietorisSquare.sequence_exact : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C}
  [inst_1 : CategoryTheory.HasWeakSheafify J (Type v)] [inst_2 : CategoryTheory.HasSheafify J AddCommGrpCat]
  [inst_3 : CategoryTheory.HasExt (CategoryTheory.Sheaf J AddCommGrpCat)] (S : J.MayerVietorisSquare)
  (F : CategoryTheory.Sheaf J AddCommGrpCat) (n₀ n₁ : ℕ) (h : n₀ + 1 = n₁), (S.sequence F n₀ n₁ h).Exact
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.Angle
/-- The tangent of a `Real.Angle`.  -/
Real.Angle.tan : Real.Angle → ℝ
-- Mathlib.GroupTheory.MonoidLocalization.Basic
Submonoid.LocalizationMap.instFunLike.eq_1 : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N],
  Submonoid.LocalizationMap.instFunLike = { coe := fun f => ⇑f.toMonoidHom, coe_injective := ⋯ }
-- Init.Core
/-- `a \ b` is the set difference of `a` and `b`,
consisting of all elements in `a` that are not in `b`.


Conventions for notations in identifiers:

 * The recommended spelling of `\` in identifiers is `sdiff`. -/
SDiff.sdiff : {α : Type u} → [self : SDiff α] → α → α → α
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.map_functor_eq : ∀ {X : TopCat} {U : TopologicalSpace.Opens ↑X} (V : TopologicalSpace.Opens ↥U),
  (TopologicalSpace.Opens.map U.inclusion').obj (⋯.functor.obj V) = V
-- Mathlib.Data.Fintype.Sum
image_subtype_ne_univ_eq_image_erase : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] [inst_1 : DecidableEq β] (k : β) (b : α → β),
  Finset.image (fun i => b ↑i) Finset.univ = (Finset.image b Finset.univ).erase k
-- Mathlib.Algebra.Module.NatInt
/-- `zsmul` is equal to any other module structure via a cast.  -/
Int.cast_smul_eq_zsmul : ∀ (R : Type u_1) {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] (n : ℤ) (b : M),
  ↑n • b = n • b
-- Mathlib.MeasureTheory.Function.AEEqFun
MeasureTheory.AEEqFun.comp_mk : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
  [inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace γ] (g : β → γ) (hg : Continuous g) (f : α → β)
  (hf : MeasureTheory.AEStronglyMeasurable f μ),
  MeasureTheory.AEEqFun.comp g hg (MeasureTheory.AEEqFun.mk f hf) = MeasureTheory.AEEqFun.mk (g ∘ f) ⋯
-- Init.Tactics
/-- `repeat1' tac` recursively applies to `tac` on all of the goals so long as it succeeds,
but `repeat1' tac` fails if `tac` succeeds on none of the initial goals.

See also:
* `repeat tac` simply applies `tac` repeatedly.
* `repeat' tac` is like `repeat1' tac` but it does not require that `tac` succeed at least once.
 -/
Lean.Parser.Tactic.repeat1' : Lean.ParserDescr
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.getMethods : Lean.Meta.Grind.GrindM Lean.Meta.Grind.Methods
-- Mathlib.RingTheory.DedekindDomain.Different
FractionalIdeal.dual_inv : ∀ (A : Type u_1) (K : Type u_2) {L : Type u} {B : Type u_3} [inst : CommRing A] [inst_1 : Field K] [inst_2 : CommRing B]
  [inst_3 : Field L] [inst_4 : Algebra A K] [inst_5 : Algebra B L] [inst_6 : Algebra A B] [inst_7 : Algebra K L]
  [inst_8 : Algebra A L] [inst_9 : IsScalarTower A K L] [inst_10 : IsScalarTower A B L] [inst_11 : IsDomain A]
  [inst_12 : IsFractionRing A K] [inst_13 : FiniteDimensional K L] [inst_14 : Algebra.IsSeparable K L]
  [inst_15 : IsIntegralClosure B A L] [inst_16 : IsFractionRing B L] [inst_17 : IsIntegrallyClosed A]
  [inst_18 : IsDedekindDomain B] {I : FractionalIdeal (nonZeroDivisors B) L},
  FractionalIdeal.dual A K I⁻¹ = FractionalIdeal.dual A K 1 * I
-- Mathlib.CategoryTheory.Bicategory.Basic
CategoryTheory.Bicategory.pentagon_inv : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b c d e : B} (f : a ⟶ b) (g : b ⟶ c) (h : c ⟶ d) (i : d ⟶ e),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerLeft f (CategoryTheory.Bicategory.associator g h i).inv)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Bicategory.associator f (CategoryTheory.CategoryStruct.comp g h) i).inv
        (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.associator f g h).inv i)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.associator f g (CategoryTheory.CategoryStruct.comp h i)).inv
      (CategoryTheory.Bicategory.associator (CategoryTheory.CategoryStruct.comp f g) h i).inv
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
mul_nonneg_iff_right_nonneg_of_pos : ∀ {R : Type u} [inst : Semiring R] [inst_1 : LinearOrder R] {a b : R} [PosMulStrictMono R], 0 < a → (0 ≤ a * b ↔ 0 ≤ b)
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_top : ∀ {R : Type u} [inst : NonAssocRing R], ↑⊤ = Set.univ
-- Mathlib.CategoryTheory.FiberedCategory.Fiber
CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf_hom_app : ∀ {𝒮 : Type u₁} {𝒳 : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] [inst_1 : CategoryTheory.Category.{v₂, u₂} 𝒳]
  {p : CategoryTheory.Functor 𝒳 𝒮} {S : 𝒮} {C : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor C 𝒳} (hF : F.comp p = (CategoryTheory.Functor.const C).obj S) (X : C),
  (CategoryTheory.Functor.Fiber.inducedFunctorCompIsoSelf hF).hom.app X =
    CategoryTheory.CategoryStruct.id
      (CategoryTheory.Functor.Fiber.fiberInclusion.obj ((CategoryTheory.Functor.Fiber.inducedFunctor hF).obj X))
-- Mathlib.Geometry.Manifold.MFDeriv.Basic
ContMDiffOn.mdifferentiableOn : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {s : Set M}
  {n : WithTop ℕ∞}, ContMDiffOn I I' n f s → n ≠ 0 → MDiff[s] f
-- Mathlib.CategoryTheory.Sites.Limits
CategoryTheory.Sheaf.instHasFiniteLimits : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.GrothendieckTopology C} {D : Type w}
  [inst_1 : CategoryTheory.Category.{w', w} D] [CategoryTheory.Limits.HasFiniteLimits D],
  CategoryTheory.Limits.HasFiniteLimits (CategoryTheory.Sheaf J D)
-- Lean.Environment
Lean.Environment.isSafeDefinition : Lean.Environment → Lean.Name → Bool
-- Mathlib.Algebra.Group.Basic
zpow_mul_comm : ∀ {G : Type u_3} [inst : Group G] (a : G) (m n : ℤ), a ^ m * a ^ n = a ^ n * a ^ m
-- Std.Data.DHashMap.Basic
/-- Removes all mappings of the hash map for which the given function returns `false`.  -/
Std.DHashMap.filter : {α : Type u} →
  {β : α → Type v} → {x : BEq α} → {x_1 : Hashable α} → ((a : α) → β a → Bool) → Std.DHashMap α β → Std.DHashMap α β
-- Mathlib.LinearAlgebra.Multilinear.Basic
LinearEquiv.multilinearMapCongrRight_apply : ∀ {R : Type uR} (S : Type uS) {ι : Type uι} {M₁ : ι → Type v₁} {M₂ : Type v₂} {M₃ : Type v₃} [inst : Semiring R]
  [inst_1 : (i : ι) → AddCommMonoid (M₁ i)] [inst_2 : (i : ι) → Module R (M₁ i)] [inst_3 : AddCommMonoid M₂]
  [inst_4 : Module R M₂] [inst_5 : Semiring S] [inst_6 : Module S M₂] [inst_7 : SMulCommClass R S M₂]
  [inst_8 : AddCommMonoid M₃] [inst_9 : Module S M₃] [inst_10 : Module R M₃] [inst_11 : SMulCommClass R S M₃]
  [inst_12 : LinearMap.CompatibleSMul M₂ M₃ S R] [inst_13 : LinearMap.CompatibleSMul M₃ M₂ S R] (g : M₂ ≃ₗ[R] M₃)
  (f : MultilinearMap R M₁ M₂), (LinearEquiv.multilinearMapCongrRight S g) f = (↑g).compMultilinearMap f
-- Mathlib.Topology.Algebra.InfiniteSum.Module
MulAction.automorphize.eq_1 : ∀ {α : Type u_1} {β : Type u_2} {M : Type u_11} [inst : TopologicalSpace M] [inst_1 : AddCommMonoid M]
  [inst_2 : Group α] [inst_3 : MulAction α β] (f : β → M),
  MulAction.automorphize f = Quotient.lift (fun b => ∑' (a : α), f (a • b)) ⋯
-- Mathlib.Analysis.Complex.Exponential
/-- scoped notation for the complex exponential function  -/
Complex.termCexp : Lean.ParserDescr
-- Mathlib.Topology.Algebra.MulAction
ContinuousOn.smul : ∀ {M : Type u_1} {X : Type u_2} {Y : Type u_3} [inst : TopologicalSpace M] [inst_1 : TopologicalSpace X]
  [inst_2 : TopologicalSpace Y] [inst_3 : SMul M X] [ContinuousSMul M X] {f : Y → M} {g : Y → X} {s : Set Y},
  ContinuousOn f s → ContinuousOn g s → ContinuousOn (f • g) s
-- Init.Prelude
/-- The homogeneous version of `HSub`: `a - b : α` where `a b : α`.  -/
Sub : Type u → Type u