mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Localization
PresheafOfModules.instIsLocalizationSheafOfModulesSheafificationInverseImageFunctorOppositeAbWToPresheaf : ∀ {C : Type u'} [inst : CategoryTheory.Category.{v', u'} C] {J : CategoryTheory.GrothendieckTopology C}
  {R₀ : CategoryTheory.Functor Cᵒᵖ RingCat} {R : CategoryTheory.Sheaf J RingCat} (α : R₀ ⟶ R.obj)
  [inst_1 : CategoryTheory.Presheaf.IsLocallyInjective J α] [inst_2 : CategoryTheory.Presheaf.IsLocallySurjective J α]
  [inst_3 : J.WEqualsLocallyBijective AddCommGrpCat] [inst_4 : CategoryTheory.HasWeakSheafify J AddCommGrpCat],
  (PresheafOfModules.sheafification α).IsLocalization (J.W.inverseImage (PresheafOfModules.toPresheaf R₀))
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.get?_eq_some_getD : ∀ {α : Type u} {β : α → Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.DHashMap α β} [inst : LawfulBEq α] {a : α}
  {fallback : β a}, a ∈ m → m.get? a = some (m.getD a fallback)
-- Mathlib.Data.Finset.Lattice.Fold
Finset.sup_eq_sSup_image : ∀ {α : Type u_2} {β : Type u_3} [inst : CompleteLattice β] (s : Finset α) (f : α → β), s.sup f = sSup (f '' ↑s)
-- Mathlib.CategoryTheory.EpiMono
CategoryTheory.IsSplitEpi.mk : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} {f : X ⟶ Y},
  Nonempty (CategoryTheory.SplitEpi f) → CategoryTheory.IsSplitEpi f
-- Mathlib.Geometry.Manifold.VectorBundle.Basic
instContMDiffVectorBundleOfNatWithTopENat_1 : ∀ {𝕜 : Type u_1} {B : Type u_2} (F : Type u_4) (E : B → Type u_6) [inst : NontriviallyNormedField 𝕜] {EB : Type u_7}
  [inst_1 : NormedAddCommGroup EB] [inst_2 : NormedSpace 𝕜 EB] {HB : Type u_8} [inst_3 : TopologicalSpace HB]
  {IB : ModelWithCorners 𝕜 EB HB} [inst_4 : TopologicalSpace B] [inst_5 : ChartedSpace HB B]
  [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module 𝕜 (E x)] [inst_8 : NormedAddCommGroup F]
  [inst_9 : NormedSpace 𝕜 F] [inst_10 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_11 : (x : B) → TopologicalSpace (E x)] [inst_12 : FiberBundle F E] [inst_13 : VectorBundle 𝕜 F E],
  ContMDiffVectorBundle 0 F E IB
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
/-- Converts a `Multiseries basis_hd basis_tl` to a `Seq (ℝ × MultiseriesExpansion basis_tl)`.  -/
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.toSeq : {basis_hd : ℝ → ℝ} →
  {basis_tl : Tactic.ComputeAsymptotics.Basis} →
    Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl →
      Stream'.Seq (ℝ × Tactic.ComputeAsymptotics.MultiseriesExpansion basis_tl)
-- Mathlib.Combinatorics.Enumerative.DoubleCounting
Finset.bipartiteAbove_swap : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) (s : Finset α) (b : β) [inst : (a : α) → Decidable (r a b)],
  Finset.bipartiteAbove (Function.swap r) s b = Finset.bipartiteBelow r s b
-- Mathlib.Algebra.Category.MonCat.Basic
AddCommMonCat.instConcreteCategoryAddMonoidHomCarrier : CategoryTheory.ConcreteCategory AddCommMonCat fun x1 x2 => ↑x1 →+ ↑x2
-- Mathlib.SetTheory.Ordinal.Arithmetic
Ordinal.typein_lt_nat : ∀ (x : ℕ), (Ordinal.typein LT.lt).toRelEmbedding x = ↑x
-- Lean.Meta.Tactic.FVarSubst
Lean.Meta.FVarSubst.mk.injEq : ∀ (map map_1 : Lean.AssocList Lean.FVarId Lean.Expr), ({ map := map } = { map := map_1 }) = (map = map_1)
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
CategoryTheory.Functor.OplaxMonoidal.instIsIsoη : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₂} [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) [inst_4 : F.OplaxMonoidal] [CategoryTheory.Limits.PreservesFiniteProducts F],
  CategoryTheory.IsIso (CategoryTheory.Functor.OplaxMonoidal.η F)
-- Mathlib.Data.Fin.SuccPred
Fin.range_castLE : ∀ {n k : ℕ} (h : n ≤ k), Set.range (Fin.castLE h) = {i | ↑i < n}
-- Mathlib.Algebra.GroupWithZero.Action.Defs
/-- Compose a `DistribSMul` with a function, with scalar multiplication `f r' • m`.
See note [reducible non-instances].  -/
DistribSMul.compFun : {M : Type u_1} →
  {N : Type u_6} → (A : Type u_7) → [inst : AddZeroClass A] → [DistribSMul M A] → (N → M) → DistribSMul N A
-- Mathlib.Algebra.Polynomial.Reverse
Polynomial.reverse_add_C : ∀ {R : Type u_1} [inst : Semiring R] (p : Polynomial R) (t : R),
  (p + Polynomial.C t).reverse = p.reverse + Polynomial.C t * Polynomial.X ^ p.natDegree
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
/-- If the image under the seminorm is zero, then the argument is zero.  -/
RingNorm.eq_zero_of_map_eq_zero' : ∀ {R : Type u_2} [inst : NonUnitalNonAssocRing R] (self : RingNorm R) (x : R), self.toFun x = 0 → x = 0
-- Mathlib.Topology.Compactness.SigmaCompact
CompactExhaustion.mk.inj : ∀ {X : Type u_4} {inst : TopologicalSpace X} {toFun : ℕ → Set X} {isCompact' : ∀ (n : ℕ), IsCompact (toFun n)}
  {subset_interior_succ' : ∀ (n : ℕ), toFun n ⊆ interior (toFun (n + 1))} {iUnion_eq' : ⋃ n, toFun n = Set.univ}
  {toFun_1 : ℕ → Set X} {isCompact'_1 : ∀ (n : ℕ), IsCompact (toFun_1 n)}
  {subset_interior_succ'_1 : ∀ (n : ℕ), toFun_1 n ⊆ interior (toFun_1 (n + 1))}
  {iUnion_eq'_1 : ⋃ n, toFun_1 n = Set.univ},
  { toFun := toFun, isCompact' := isCompact', subset_interior_succ' := subset_interior_succ',
        iUnion_eq' := iUnion_eq' } =
      { toFun := toFun_1, isCompact' := isCompact'_1, subset_interior_succ' := subset_interior_succ'_1,
        iUnion_eq' := iUnion_eq'_1 } →
    toFun = toFun_1
-- Init.Data.Fin.Basic
/-- Bitwise left shift of bounded numbers, with wraparound on overflow.

Examples:
* `(1 : Fin 10) <<< (1 : Fin 10) = (2 : Fin 10)`
* `(1 : Fin 10) <<< (3 : Fin 10) = (8 : Fin 10)`
* `(1 : Fin 10) <<< (4 : Fin 10) = (6 : Fin 10)`
 -/
Fin.shiftLeft : {n : ℕ} → Fin n → Fin n → Fin n
-- Mathlib.LinearAlgebra.Matrix.Unique
Matrix.uniqueEquiv_symm_apply : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} [inst : Unique m] [inst_1 : Unique n] (a : A),
  Matrix.uniqueEquiv.symm a = Matrix.of fun x x_1 => a
-- Init.Tactics
/-- `push_cast` rewrites the goal to move certain coercions (*casts*) inward, toward the leaf nodes.
This uses `norm_cast` lemmas in the forward direction.
For example, `↑(a + b)` will be written to `↑a + ↑b`.
- `push_cast` moves casts inward in the goal.
- `push_cast at h` moves casts inward in the hypothesis `h`.
It can be used with extra simp lemmas with, for example, `push_cast [Int.add_zero]`.

Example:
```lean
example (a b : Nat)
    (h1 : ((a + b : Nat) : Int) = 10)
    (h2 : ((a + b + 0 : Nat) : Int) = 10) :
    ((a + b : Nat) : Int) = 10 := by
  /-
  h1 : ↑(a + b) = 10
  h2 : ↑(a + b + 0) = 10
  ⊢ ↑(a + b) = 10
  -/
  push_cast
  /- Now
  ⊢ ↑a + ↑b = 10
  -/
  push_cast at h1
  push_cast [Int.add_zero] at h2
  /- Now
  h1 h2 : ↑a + ↑b = 10
  -/
  exact h1
```

See also `norm_cast`.
 -/
Lean.Parser.Tactic.pushCast : Lean.ParserDescr
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
/-- Restriction of a non-unital ring homomorphism to a non-unital subsemiring of the codomain.  -/
NonUnitalRingHom.codRestrict : {R : Type u} →
  {S : Type v} →
    [inst : NonUnitalNonAssocSemiring R] →
      {F : Type u_1} →
        [inst_1 : FunLike F R S] →
          [inst_2 : NonUnitalNonAssocSemiring S] →
            [NonUnitalRingHomClass F R S] →
              {S' : Type u_2} →
                [inst_4 : SetLike S' S] →
                  [inst_5 : NonUnitalSubsemiringClass S' S] → (f : F) → (s : S') → (∀ (x : R), f x ∈ s) → R →ₙ+* ↥s
-- Init.Data.String.Basic
String.instDecidableIsValidForSlice : {s : String.Slice} → {p : String.Pos.Raw} → Decidable (String.Pos.Raw.IsValidForSlice s p)
-- Mathlib.LinearAlgebra.Matrix.RowCol
Matrix.transpose_replicateCol : ∀ {m : Type u_2} {α : Type v} {ι : Type u_6} (v : m → α), (Matrix.replicateCol ι v).transpose = Matrix.replicateRow ι v
-- Mathlib.Data.Prod.Basic
Prod.swap_eq_iff_eq_swap : ∀ {α : Type u_1} {β : Type u_2} {x : α × β} {y : β × α}, x.swap = y ↔ x = y.swap
-- Mathlib.CategoryTheory.Bicategory.Functor.Pseudofunctor
CategoryTheory.Pseudofunctor.whiskerLeft_mapId_inv_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.Pseudofunctor B C) {a b : B} (f : a ⟶ b) {Z : F.obj a ⟶ F.obj b}
  (h : CategoryTheory.CategoryStruct.comp (F.map f) (F.map (CategoryTheory.CategoryStruct.id b)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (F.map f) (F.mapId b).inv) h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (F.map f)).hom
      (CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.Bicategory.rightUnitor f).inv)
        (CategoryTheory.CategoryStruct.comp (F.mapComp f (CategoryTheory.CategoryStruct.id b)).hom h))
-- Mathlib.FieldTheory.Extension
IntermediateField.exists_algHom_of_splits_of_aeval : ∀ {F : Type u_1} {E : Type u_2} {K : Type u_3} [inst : Field F] [inst_1 : Field E] [inst_2 : Field K]
  [inst_3 : Algebra F E] [inst_4 : Algebra F K],
  (∀ (s : E), IsIntegral F s ∧ (Polynomial.map (algebraMap F K) (minpoly F s)).Splits) →
    ∀ {x : E} {y : K}, (Polynomial.aeval y) (minpoly F x) = 0 → ∃ φ, φ x = y
-- Mathlib.LinearAlgebra.Matrix.GeneralLinearGroup.Card
/-- Equivalence between `GL n F` and `n` vectors of length `n` that are linearly independent. Given
by sending a matrix to its columns.  -/
Matrix.equiv_GL_linearindependent : {𝔽 : Type u_1} → [inst : Field 𝔽] → [Fintype 𝔽] → (n : ℕ) → GL (Fin n) 𝔽 ≃ { s // LinearIndependent 𝔽 s }
-- Mathlib.Algebra.Ring.Divisibility.Basic
dvd_sub_comm : ∀ {α : Type u_1} [inst : NonUnitalRing α] {a b c : α}, a ∣ b - c ↔ a ∣ c - b
-- Mathlib.Data.Finset.Insert
Finset.nontrivial_iff_ne_singleton : ∀ {α : Type u_1} {s : Finset α} {a : α}, a ∈ s → (s.Nontrivial ↔ s ≠ {a})
-- Mathlib.Testing.Plausible.Functions
Plausible.InjectiveFunction.sliceSizes.eq_def : ∀ (x : ℕ),
  Plausible.InjectiveFunction.sliceSizes x =
    let n := x;
    if h : 0 < n then
      have this := ⋯;
      MLList.cons ⟨n, h⟩ (Plausible.InjectiveFunction.sliceSizes (n / 2))
    else MLList.nil
-- Mathlib.Topology.Neighborhoods
pure_le_nhds : ∀ {X : Type u} [inst : TopologicalSpace X], pure ≤ nhds
-- Lean.Elab.MutualDef
Lean.Elab.Term.MutualClosure.FixPoint.run : Array Lean.FVarId → Lean.Elab.Term.MutualClosure.UsedFVarsMap → Lean.Elab.Term.MutualClosure.UsedFVarsMap
-- Mathlib.AlgebraicTopology.ModelCategory.CofibrantObjectHomotopy
HomotopicalAlgebra.CofibrantObject.HoCat.localizerMorphismResolution_functor : ∀ (C : Type u_1) [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : HomotopicalAlgebra.ModelCategory C],
  (HomotopicalAlgebra.CofibrantObject.HoCat.localizerMorphismResolution C).functor =
    HomotopicalAlgebra.CofibrantObject.HoCat.resolution
-- Mathlib.CategoryTheory.Localization.Resolution
/-- The canonical map `Φ.LeftResolution X₂ → Φ.op.RightResolution (Opposite.op X₂)`.  -/
CategoryTheory.LocalizerMorphism.LeftResolution.op : {C₁ : Type u_1} →
  {C₂ : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} C₁] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] →
        {W₁ : CategoryTheory.MorphismProperty C₁} →
          {W₂ : CategoryTheory.MorphismProperty C₂} →
            {Φ : CategoryTheory.LocalizerMorphism W₁ W₂} →
              {X₂ : C₂} → Φ.LeftResolution X₂ → Φ.op.RightResolution (Opposite.op X₂)
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
ContMDiffOn.of_succ : ∀ {𝕜 : 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 + 1) f s → ContMDiffOn I I' n f s
-- Mathlib.Algebra.FiniteSupport.Basic
Function.HasFiniteSupport.sup : ∀ {α : Type u_1} {M : Type u_2} [inst : Zero M] [inst_1 : SemilatticeSup M] {f g : α → M},
  Function.HasFiniteSupport f → Function.HasFiniteSupport g → Function.HasFiniteSupport fun a => f a ⊔ g a
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Prepartition.splitMany_insert : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι) (s : Finset (ι × ℝ)) (p : ι × ℝ),
  BoxIntegral.Prepartition.splitMany I (insert p s) =
    BoxIntegral.Prepartition.splitMany I s ⊓ BoxIntegral.Prepartition.split I p.1 p.2
-- Mathlib.Order.Category.NonemptyFinLinOrd
/-- Typecheck a `OrderHom` as a morphism in `NonemptyFinLinOrd`.  -/
NonemptyFinLinOrd.ofHom : {X Y : Type u} →
  [inst : Nonempty X] →
    [inst_1 : LinearOrder X] →
      [inst_2 : Fintype X] →
        [inst_3 : Nonempty Y] →
          [inst_4 : LinearOrder Y] → [inst_5 : Fintype Y] → (X →o Y) → (NonemptyFinLinOrd.of X ⟶ NonemptyFinLinOrd.of Y)
-- Mathlib.RingTheory.Ideal.Over
Ideal.under_under : ∀ {A : Type u_2} [inst : CommSemiring A] {B : Type u_3} [inst_1 : CommSemiring B] {C : Type u_4} [inst_2 : Semiring C]
  [inst_3 : Algebra A B] [inst_4 : Algebra B C] [inst_5 : Algebra A C] [IsScalarTower A B C] (𝔓 : Ideal C),
  Ideal.under A (Ideal.under B 𝔓) = Ideal.under A 𝔓
-- Init.Data.List.Sublist
List.infix_filter_iff : ∀ {α : Type u_1} {p : α → Bool} {l₁ l₂ : List α}, l₂ <:+: List.filter p l₁ ↔ ∃ l, l <:+: l₁ ∧ l₂ = List.filter p l
-- Mathlib.Topology.Constructions
continuousAt_pi : ∀ {X : Type u} {ι : Type u_5} {A : ι → Type u_6} [inst : TopologicalSpace X] [T : (i : ι) → TopologicalSpace (A i)]
  {f : X → (i : ι) → A i} {x : X}, ContinuousAt f x ↔ ∀ (i : ι), ContinuousAt (fun y => f y i) x
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.true_intro : ∀ {σs : List (Type u)} {P : Std.Do.SPred σs}, P ⊢ₛ ⌜True⌝
-- Mathlib.Topology.Order.Lattice
Filter.Tendsto.inf_nhds : ∀ {L : Type u_1} [inst : TopologicalSpace L] {α : Type u_3} {l : Filter α} {f g : α → L} {x y : L} [inst_1 : Min L]
  [ContinuousInf L],
  Filter.Tendsto f l (nhds x) → Filter.Tendsto g l (nhds y) → Filter.Tendsto (fun i => f i ⊓ g i) l (nhds (x ⊓ y))
-- Lean.Parser.Term.Basic
Lean.Parser.Tactic.tacticSeq1Indented : Lean.Parser.Parser
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.Ioo_subset_coe : ∀ {ι : Type u_1} (I : BoxIntegral.Box ι), BoxIntegral.Box.Ioo I ⊆ ↑I
-- Mathlib.Data.List.Chain
List.IsChain.rel_getLast_head_of_append : ∀ {α : Type u_1} {R : α → α → Prop} {l₁ l₂ : List α},
  List.IsChain R (l₁ ++ l₂) → ∀ (h₁ : l₁ ≠ []) (h₂ : l₂ ≠ []), R (l₁.getLast h₁) (l₂.head h₂)
-- Mathlib.Order.PFilter
Order.PFilter.sInf_gc : ∀ {P : Type u_1} [inst : CompleteSemilatticeInf P],
  GaloisConnection (fun x => OrderDual.toDual (Order.PFilter.principal x)) fun F => sInf ↑(OrderDual.ofDual F)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
FormalMultilinearSeries.coeff_eq_zero : ∀ {𝕜 : Type u} {E : Type v} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {p : FormalMultilinearSeries 𝕜 𝕜 E} {n : ℕ}, p.coeff n = 0 ↔ p n = 0
-- Lean.Elab.Tactic.Grind.Basic
/-- Save the current tactic state for a token `stx`.
This method is a no-op if `stx` has no position information.
We use this method to save the tactic state at punctuation such as `;`
 -/
Lean.Elab.Tactic.Grind.saveTacticInfoForToken : Lean.Syntax → Lean.Elab.Tactic.Grind.GrindTacticM Unit
-- Std.Data.DTreeMap.Internal.Balancing
_private.Std.Data.DTreeMap.Internal.Balancing.0.Std.DTreeMap.Internal.Impl.balanceLErase.match_5.splitter : {α : Type u_1} →
  {β : α → Type u_2} →
    (rs : ℕ) →
      (k : α) →
        (v : β k) →
          (l r : Std.DTreeMap.Internal.Impl α β) →
            (motive :
                (l_1 : Std.DTreeMap.Internal.Impl α β) →
                  l_1.Balanced →
                    Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l_1.size
                        (Std.DTreeMap.Internal.Impl.inner rs k v l r).size →
                      Sort u_3) →
              (l_1 : Std.DTreeMap.Internal.Impl α β) →
                (hlb : l_1.Balanced) →
                  (hlr :
                      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond l_1.size
                        (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                    ((hlb : Std.DTreeMap.Internal.Impl.leaf.Balanced) →
                        (hlr :
                            Std.DTreeMap.Internal.Impl.BalanceLErasePrecond Std.DTreeMap.Internal.Impl.leaf.size
                              (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                          motive Std.DTreeMap.Internal.Impl.leaf hlb hlr) →
                      ((ls : ℕ) →
                          (lk : α) →
                            (lv : β lk) →
                              (ll lr : Std.DTreeMap.Internal.Impl α β) →
                                (hlb : (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).Balanced) →
                                  (hlr :
                                      Std.DTreeMap.Internal.Impl.BalanceLErasePrecond
                                        (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr).size
                                        (Std.DTreeMap.Internal.Impl.inner rs k v l r).size) →
                                    motive (Std.DTreeMap.Internal.Impl.inner ls lk lv ll lr) hlb hlr) →
                        motive l_1 hlb hlr
-- Mathlib.Algebra.Group.Subsemigroup.Operations
Subsemigroup.range_subtype : ∀ {M : Type u_1} [inst : Mul M] (s : Subsemigroup M), (MulMemClass.subtype s).srange = s
-- Mathlib.Analysis.Distribution.TestFunction
/-- **Alias** of `FunLike.coe_sub`. -/
TestFunction.coe_sub : ∀ {F : Type u_3} {α : Type u_5} {β : Type u_6} [inst : FunLike F α β] [inst_1 : Sub F] [inst_2 : Sub β]
  [IsSubApply F α β] (f g : F), ⇑(f - g) = ⇑f - ⇑g
-- Mathlib.Analysis.Normed.Operator.Prod
/-- `ContinuousLinearMap.prod` as a `LinearIsometryEquiv`.  -/
ContinuousLinearMap.prodₗᵢ : {𝕜 : Type u_1} →
  {E : Type u_2} →
    {F : Type u_3} →
      {G : Type u_4} →
        [inst : NontriviallyNormedField 𝕜] →
          [inst_1 : SeminormedAddCommGroup E] →
            [inst_2 : SeminormedAddCommGroup F] →
              [inst_3 : SeminormedAddCommGroup G] →
                [inst_4 : NormedSpace 𝕜 E] →
                  [inst_5 : NormedSpace 𝕜 F] →
                    [inst_6 : NormedSpace 𝕜 G] →
                      (R : Type u_5) →
                        [inst_7 : Semiring R] →
                          [inst_8 : Module R F] →
                            [inst_9 : Module R G] →
                              [inst_10 : ContinuousConstSMul R F] →
                                [inst_11 : ContinuousConstSMul R G] →
                                  [inst_12 : SMulCommClass 𝕜 R F] →
                                    [inst_13 : SMulCommClass 𝕜 R G] → (E →L[𝕜] F) × (E →L[𝕜] G) ≃ₗᵢ[R] E →L[𝕜] F × G
-- Init.Data.String.Basic
String.Pos.Raw.isValidForSlice_stringSliceTo : ∀ {s : String} {p : s.Pos} {q : String.Pos.Raw},
  String.Pos.Raw.IsValidForSlice (s.sliceTo p) q ↔ q ≤ p.offset ∧ String.Pos.Raw.IsValid s q
-- Init.Data.SInt.Basic
instSubInt16 : Sub Int16
-- Mathlib.Analysis.Calculus.FDeriv.Equiv
ContinuousLinearEquiv.comp_differentiableAt_iff : ∀ {𝕜 : 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] {G : Type u_4}
  [inst_5 : NormedAddCommGroup G] [inst_6 : NormedSpace 𝕜 G] (iso : E ≃L[𝕜] F) {f : G → E} {x : G},
  DifferentiableAt 𝕜 (⇑iso ∘ f) x ↔ DifferentiableAt 𝕜 f x
-- Mathlib.Algebra.Ring.Commute
mul_self_sub_one : ∀ {R : Type u} [inst : NonAssocRing R] (a : R), a * a - 1 = (a + 1) * (a - 1)
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.truncGEδLT_comp_truncLTι_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (n : ℤ) (X : C),
  CategoryTheory.CategoryStruct.comp ((t.truncGEδLT n).app X)
      ((CategoryTheory.shiftFunctor C 1).map ((t.truncLTι n).app X)) =
    0
-- Init.Omega.LinearCombo
Lean.Omega.LinearCombo.coordinate_eval_0 : ∀ {a0 : ℤ} {t : List ℤ}, (Lean.Omega.LinearCombo.coordinate 0).eval (Lean.Omega.Coeffs.ofList (a0 :: t)) = a0
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Pretrivialization.linearMapAt_def_of_notMem : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : AddCommMonoid F] [inst_4 : Module R F]
  [inst_5 : (x : B) → AddCommMonoid (E x)] [inst_6 : (x : B) → Module R (E x)]
  (e : Bundle.Pretrivialization F Bundle.TotalSpace.proj) [inst_7 : Bundle.Pretrivialization.IsLinear R e] {b : B},
  b ∉ e.baseSet → Bundle.Pretrivialization.linearMapAt R e b = 0
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf
/-- We will define the structure sheaf as the subsheaf of all dependent functions in
`Π x : U, HomogeneousLocalization 𝒜 x` consisting of those functions which can locally be expressed
as a ratio of `A` of same grading.  -/
AlgebraicGeometry.ProjectiveSpectrum.StructureSheaf.isLocallyFraction : {A : Type u_1} →
  {σ : Type u_2} →
    [inst : CommRing A] →
      [inst_1 : SetLike σ A] →
        [inst_2 : AddSubgroupClass σ A] →
          (𝒜 : ℕ → σ) →
            [inst_3 : GradedRing 𝒜] →
              TopCat.LocalPredicate fun x => HomogeneousLocalization.AtPrime 𝒜 x.asHomogeneousIdeal.toIdeal
-- Mathlib.Analysis.Calculus.ContDiff.Operations
ContDiffOn.inv : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {s : Set E} {n : WithTop ℕ∞} {𝕜' : Type u_4} [inst_3 : NormedField 𝕜']
  [inst_4 : NormedAlgebra 𝕜 𝕜'] {f : E → 𝕜'}, ContDiffOn 𝕜 n f s → (∀ x ∈ s, f x ≠ 0) → ContDiffOn 𝕜 n f⁻¹ s
-- Init.Data.List.Lemmas
List.eq_nil_of_map_eq_nil : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {l : List α}, List.map f l = [] → l = []
-- Mathlib.Order.Category.HeytAlg
HeytAlg.ofHom_id : ∀ {X : Type u} [inst : HeytingAlgebra X],
  HeytAlg.ofHom (HeytingHom.id X) = CategoryTheory.CategoryStruct.id (HeytAlg.of X)
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
/-- Composition of oplax functors.  -/
CategoryTheory.OplaxFunctor.comp : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        {D : Type u₃} →
          [inst_2 : CategoryTheory.Bicategory D] →
            CategoryTheory.OplaxFunctor B C → CategoryTheory.OplaxFunctor C D → CategoryTheory.OplaxFunctor B D
-- Mathlib.Algebra.Category.MonCat.Basic
/-- Construct a bundled `AddMonCat` from the underlying type and typeclass.  -/
AddMonCat.of : (M : Type u) → [AddMonoid M] → AddMonCat
-- Mathlib.RingTheory.UniqueFactorizationDomain.FactorSet
/-- Evaluates the product of a `FactorSet` to be the product of the corresponding multiset,
or `0` if there is none.  -/
Associates.FactorSet.prod : {α : Type u_1} → [inst : CommMonoidWithZero α] → Associates.FactorSet α → Associates α
-- Mathlib.LinearAlgebra.Dimension.Free
/-- A free module of rank zero is trivial.  -/
Module.subsingleton_of_rank_zero : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Module.Free R M]
  [StrongRankCondition R], Module.rank R M = 0 → Subsingleton M
-- Mathlib.Data.List.ProdSigma
List.length_product : ∀ {α : Type u_1} {β : Type u_2} (l₁ : List α) (l₂ : List β), (l₁ ×ˢ l₂).length = l₁.length * l₂.length
-- Mathlib.ModelTheory.Basic
/-- A language is relational when it has no function symbols.  -/
FirstOrder.Language.IsRelational : FirstOrder.Language → Prop
-- Mathlib.GroupTheory.SpecificGroups.ZGroup
/-- An extension of coprime Z-groups is a Z-group.  -/
isZGroup_of_coprime : ∀ {G : Type u_1} {G' : Type u_2} {G'' : Type u_3} [inst : Group G] [inst_1 : Group G'] [inst_2 : Group G'']
  {f : G →* G'} {f' : G' →* G''} [Finite G] [IsZGroup G] [IsZGroup G''],
  f'.ker ≤ f.range → (Nat.card G).Coprime (Nat.card G'') → IsZGroup G'