mathlib-initiative/mathlib-types huggingface dataset:
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.String.Legacy.Iterator.forward.match_1.eq_1 : ∀ (motive : String.Legacy.Iterator → ℕ → Sort u_1) (it : String.Legacy.Iterator)
  (h_1 : (it : String.Legacy.Iterator) → motive it 0)
  (h_2 : (it : String.Legacy.Iterator) → (n : ℕ) → motive it n.succ),
  (match it, 0 with
    | it, 0 => h_1 it
    | it, n.succ => h_2 it n) =
    h_1 it
-- Mathlib.Data.Nat.Prime.Infinite
/-- **Alias** of `Nat.not_bddAbove_setOfPred_prime`.

---

A version of `Nat.exists_infinite_primes` using the `BddAbove` predicate.  -/
Nat.not_bddAbove_setOf_prime : ¬BddAbove {p | Nat.Prime p}
-- Lean.Elab.Tactic.Try
/-- Returns `true` if all free variables occurring in `e` are accessible. Over-approximation, since
the free variable may be implicit.
  -/
_private.Lean.Elab.Tactic.Try.0.Lean.Elab.Tactic.Try.isExprAccessible : Lean.Expr → Lean.MetaM Bool
-- Mathlib.Algebra.Homology.LeftResolution.Basic
CategoryTheory.Abelian.LeftResolution.map_chainComplex_d_1_0 : ∀ {A : Type u_1} {C : Type u_2} [inst : CategoryTheory.Category.{v_1, u_2} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_1} A] {ι : CategoryTheory.Functor C A}
  (Λ : CategoryTheory.Abelian.LeftResolution ι) (X : A) [inst_2 : ι.Full] [inst_3 : ι.Faithful]
  [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C] [inst_5 : CategoryTheory.Abelian A],
  ι.map ((Λ.chainComplex X).d 1 0) =
    CategoryTheory.CategoryStruct.comp (ι.map (Λ.chainComplexXOneIso X).hom)
      (CategoryTheory.CategoryStruct.comp (Λ.π.app (CategoryTheory.Limits.kernel (Λ.π.app X)))
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.kernel.ι (Λ.π.app X))
          (ι.map (Λ.chainComplexXZeroIso X).inv)))
-- Mathlib.Tactic.Algebra.Basic
/-- Evaluate the inverse of two normalized expressions in `R` using `ring`.  -/
Mathlib.Tactic.Algebra.RingCompute.inv : {u v : Lean.Level} →
  {R : Q(Type u)} →
    {A : Q(Type v)} →
      {sR : Q(CommSemiring «$R»)} →
        {sA : Q(CommSemiring «$A»)} →
          (sAlg : Q(Algebra «$R» «$A»)) →
            Mathlib.Tactic.Algebra.Cache sR →
              {a : Q(«$A»)} →
                Option Q(CharZero «$A») →
                  (fA : Q(Semifield «$A»)) →
                    Mathlib.Tactic.Algebra.BaseType sAlg a →
                      Mathlib.Tactic.AtomM
                        (Option (Mathlib.Tactic.Ring.Common.Result (Mathlib.Tactic.Algebra.BaseType sAlg) q(«$a»⁻¹)))
-- Mathlib.GroupTheory.HNNExtension
HNNExtension.NormalWord.ReducedWord.mk.sizeOf_spec : ∀ {G : Type u_1} [inst : Group G] {A B : Subgroup G} [inst_1 : SizeOf G] (head : G) (toList : List (ℤˣ × G))
  (chain : List.IsChain (fun a b => a.2 ∈ HNNExtension.toSubgroup A B a.1 → a.1 = b.1) toList),
  sizeOf { head := head, toList := toList, chain := chain } = 1 + sizeOf head + sizeOf toList + sizeOf chain
-- Init.Data.Ord.Basic
/-- Equal.  -/
Ordering.eq : Ordering
-- Std.Http.Data.Chunk
Std.Http.instInhabitedChunk : Inhabited Std.Http.Chunk
-- Mathlib.Topology.Algebra.InfiniteSum.Basic
multipliable_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : CommMonoidWithZero α] [inst_1 : TopologicalSpace α] {L : SummationFilter β}
  [L.LeAtTop], Multipliable (fun x => 0) L
-- Mathlib.Algebra.Homology.ComplexShapeSigns
/-- The sign of the vertical differential in the total complex.  -/
ComplexShape.ε₂ : {I₁ : Type u_1} →
  {I₂ : Type u_2} →
    {I₁₂ : Type u_4} →
      (c₁ : ComplexShape I₁) →
        (c₂ : ComplexShape I₂) → (c₁₂ : ComplexShape I₁₂) → [TotalComplexShape c₁ c₂ c₁₂] → I₁ × I₂ → ℤˣ
-- Init.Data.List.OfFn
List.ofFn_add : ∀ {α : Type u_1} {n m : ℕ} {f : Fin (n + m) → α},
  List.ofFn f = (List.ofFn fun i => f (Fin.castLE ⋯ i)) ++ List.ofFn fun i => f (Fin.natAdd n i)
-- Mathlib.Data.Set.Finite.Lemmas
Set.exists_lower_bound_image : ∀ {α : Type u} {β : Type v} [Nonempty α] [inst : LinearOrder β] (s : Set α) (f : α → β),
  s.Finite → ∃ a, ∀ b ∈ s, f a ≤ f b
-- Mathlib.Analysis.Normed.Group.Basic
/-- A scaled ball is a ball.  -/
setOf_div_mem_ball_eq_ball'' : ∀ {E : Type u_5} [inst : SeminormedCommGroup E] {a : E} {r : ℝ}, {x | x / a ∈ Metric.ball 1 r} = Metric.ball a r
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.size_erase : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α],
  (↑m).WF → ∀ {k : α}, (↑(m.erase k)).size = if m.contains k = true then (↑m).size - 1 else (↑m).size
-- Std.Data.DTreeMap.Internal.WF.Lemmas
Std.DTreeMap.Internal.Impl.ordered_inter : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] {l₁ l₂ : Std.DTreeMap.Internal.Impl α β}
  (hlb : l₁.Balanced), l₁.Ordered → (l₁.inter l₂ hlb).Ordered
-- Mathlib.Analysis.Normed.Group.Basic
norm_le_of_mem_closedBall : ∀ {E : Type u_5} [inst : SeminormedAddGroup E] {a b : E} {r : ℝ}, b ∈ Metric.closedBall a r → ‖b‖ ≤ ‖a‖ + r
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- Sum of a multiset of elements in a `Subsemiring` of a `NonAssocSemiring` is
in the `Subsemiring`.  -/
Subsemiring.multiset_sum_mem : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Subsemiring R) (m : Multiset R), (∀ a ∈ m, a ∈ s) → m.sum ∈ s
-- Init.Data.SInt.Lemmas
Int8.neg_mul_comm : ∀ (a b : Int8), -a * b = a * -b
-- Mathlib.ModelTheory.PartialEquiv
_private.Mathlib.ModelTheory.PartialEquiv.0.FirstOrder.Language.PartialEquiv.le_antisymm : ∀ {L : FirstOrder.Language} {M : Type w} {N : Type w'} [inst : L.Structure M] [inst_1 : L.Structure N]
  (f g : L.PartialEquiv M N), f ≤ g → g ≤ f → f = g
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_insert! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF →
    ∀ {k a : α} {v : β k},
      Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insert! k v t) = true →
        compare k a ≠ Ordering.eq → Std.DTreeMap.Internal.Impl.contains a t = true
-- Mathlib.Algebra.Group.AddChar
AddChar.one_apply : ∀ {A : Type u_1} {M : Type u_3} [inst : AddMonoid A] [inst_1 : Monoid M] (a : A), 1 a = 1
-- Mathlib.Analysis.MellinInversion
_private.Mathlib.Analysis.MellinInversion.0.rexp_neg_injOn_aux : Set.InjOn (Real.exp ∘ Neg.neg) Set.univ
-- Init.Data.Fin.Lemmas
Fin.cast_natAdd_right : ∀ {n n' m : ℕ} (i : Fin n') (h : m + n' = m + n), Fin.cast h (Fin.natAdd m i) = Fin.natAdd m (Fin.cast ⋯ i)
-- Lean.Elab.DocString
_private.Lean.Elab.DocString.0.Lean.Doc.docElementMessage.isBuiltin : Lean.Name → BaseIO Bool
-- Lean.Language.Lean.Types
/-- State after the module header has been parsed.  -/
Lean.Language.Lean.HeaderParsedSnapshot : Type
-- Mathlib.Order.Disjoint
Prod.disjoint_iff : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : OrderBot α]
  [inst_3 : OrderBot β] {x y : α × β}, Disjoint x y ↔ Disjoint x.1 y.1 ∧ Disjoint x.2 y.2
-- Mathlib.LinearAlgebra.Multilinear.Curry
/-- If `s : Finset (Fin n)` is a finite set of cardinality `k` and its complement has cardinality
`l`, then the space of multilinear maps on `fun i : Fin n => M'` is isomorphic to the space of
multilinear maps on `fun i : Fin k => M'` taking values in the space of multilinear maps
on `fun i : Fin l => M'`.  -/
MultilinearMap.curryFinFinset : (R : Type uR) →
  (M₂ : Type v₂) →
    (M' : Type v') →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M'] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M'] →
              [inst_4 : Module R M₂] →
                {k l n : ℕ} →
                  {s : Finset (Fin n)} →
                    s.card = k →
                      sᶜ.card = l →
                        MultilinearMap R (fun x => M') M₂ ≃ₗ[R]
                          MultilinearMap R (fun x => M') (MultilinearMap R (fun x => M') M₂)
-- Init.Data.Range.Polymorphic.Lemmas
Std.Rco.pairwise_toList_upwardEnumerableLt : ∀ {α : Type u} {r : Std.Rco α} [LE α] [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α], List.Pairwise (fun a b => Std.PRange.UpwardEnumerable.LT a b) r.toList
-- Mathlib.NumberTheory.Height.Basic
Height.logHeight₁_eq_log_mulHeight₁ : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] (x : K),
  Height.logHeight₁ x = Real.log (Height.mulHeight₁ x)
-- Lean.Meta.Tactic.Grind.Extension
Lean.Meta.Grind.SymbolPriorities.mk.sizeOf_spec : ∀ (map : Lean.PHashMap Lean.Name ℕ), sizeOf { map := map } = 1 + sizeOf map
-- Mathlib.Algebra.Homology.Embedding.HomEquiv
ComplexShape.Embedding.homRestrict_f : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} (e : c.Embedding c') {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {K : HomologicalComplex C c'} {L : HomologicalComplex C c}
  [inst_3 : e.IsRelIff] (ψ : K ⟶ L.extend e) {i : ι} {i' : ι'} (h : e.f i = i'),
  (e.homRestrict ψ).f i =
    CategoryTheory.CategoryStruct.comp (K.restrictionXIso e h).hom
      (CategoryTheory.CategoryStruct.comp (ψ.f i') (L.extendXIso e h).hom)
-- Mathlib.Algebra.BigOperators.RingEquiv
RingEquiv.map_list_sum : ∀ {R : Type u_2} {S : Type u_3} [inst : NonUnitalNonAssocSemiring R] [inst_1 : NonUnitalNonAssocSemiring S]
  (f : R ≃+* S) (l : List R), f l.sum = (List.map (⇑f) l).sum
-- Lean.Elab.Arg
/-- Named arguments created using the notation `(x := val)`.  -/
Lean.Elab.Term.NamedArg : Type
-- Mathlib.Probability.Process.Filtration
MeasureTheory.Filtration.instTop : {Ω : Type u_1} → {ι : Type u_2} → {m : MeasurableSpace Ω} → [inst : Preorder ι] → Top (MeasureTheory.Filtration ι m)
-- Mathlib.Algebra.Lie.DirectSum
/-- Given a family of Lie algebras `L i`, together with a family of morphisms of Lie algebras
`f i : L i →ₗ⁅R⁆ L'` into a fixed Lie algebra `L'`, we have a natural linear map:
`(⨁ i, L i) →ₗ[R] L'`. If in addition `⁅f i x, f j y⁆ = 0` for any `x ∈ L i` and `y ∈ L j` (`i ≠ j`)
then this map is a morphism of Lie algebras.  -/
DirectSum.toLieAlgebra : {R : Type u} →
  {ι : Type v} →
    [inst : CommRing R] →
      {L : ι → Type w} →
        [inst_1 : (i : ι) → LieRing (L i)] →
          [inst_2 : (i : ι) → LieAlgebra R (L i)] →
            [DecidableEq ι] →
              (L' : Type w₁) →
                [inst_4 : LieRing L'] →
                  [inst_5 : LieAlgebra R L'] →
                    (f : (i : ι) → L i →ₗ⁅R⁆ L') →
                      (Pairwise fun i j => ∀ (x : L i) (y : L j), ⁅(f i) x, (f j) y⁆ = 0) →
                        (DirectSum ι fun i => L i) →ₗ⁅R⁆ L'
-- Mathlib.Data.Set.Lattice.Image
Set.univ_subtype : ∀ {α : Type u_1} {p : α → Prop}, Set.univ = ⋃ x, ⋃ (h : p x), {⟨x, h⟩}
-- Init.Data.List.Nat.TakeDrop
List.dropLast_take : ∀ {α : Type u_1} {i : ℕ} {l : List α}, i < l.length → (List.take i l).dropLast = List.take (i - 1) l
-- Mathlib.Geometry.RingedSpace.PresheafedSpace
AlgebraicGeometry.PresheafedSpace.restrictTopIso_hom : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : AlgebraicGeometry.PresheafedSpace C),
  X.restrictTopIso.hom = X.ofRestrict ⋯
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.IsTheta.isBigO : ∀ {α : Type u_1} {E : Type u_3} {F : Type u_4} [inst : Norm E] [inst_1 : Norm F] {f : α → E} {g : α → F} {l : Filter α},
  f =Θ[l] g → f =O[l] g
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.sumZeroHom_piSingle : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → Zero (β i)]
  [inst_2 : AddCommMonoid γ] (i : ι) (φ : ZeroHom (β i) γ),
  DFinsupp.sumZeroHom (Pi.single i φ) = φ.comp { toFun := fun x => x i, map_zero' := ⋯ }
-- Mathlib.CategoryTheory.Comma.Basic
CategoryTheory.Comma.fst_map : ∀ {A : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} A] {B : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  {T : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} T] (L : CategoryTheory.Functor A T)
  (R : CategoryTheory.Functor B T) {X Y : CategoryTheory.Comma L R} (f : X ⟶ Y),
  (CategoryTheory.Comma.fst L R).map f = f.left
-- Mathlib.Data.Fin.SuccPred
Fin.predAbove_castSucc_of_le : ∀ {n : ℕ} (p i : Fin n), i ≤ p → p.predAbove i.castSucc = i
-- Std.Data.DTreeMap.Basic
/-- Transforms an array of keys into a tree map.  -/
Std.DTreeMap.Const.unitOfArray : {α : Type u} →
  Array α →
    (cmp : autoParam (α → α → Ordering) Std.DTreeMap.Const.unitOfArray._auto_1) → Std.DTreeMap α (fun x => Unit) cmp
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the smallest key that is greater than or equal to the
given key, panicking if no such pair exists.
 -/
Std.DTreeMap.Raw.Const.getEntryGE! : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap.Raw α (fun x => β) cmp → α → α × β
-- Mathlib.RingTheory.NonUnitalSubsemiring.Defs
NonUnitalSubsemiringClass.toAddSubmonoidClass : ∀ {S : Type u_1} {R : outParam (Type u)} {inst : NonUnitalNonAssocSemiring R} {inst_1 : SetLike S R}
  [self : NonUnitalSubsemiringClass S R], AddSubmonoidClass S R
-- Mathlib.CategoryTheory.Sites.Coherent.Basic
/-- For `X`, `Y`, `Z`, `f`, `g` like in the diagram, where `g` is an effective epi, there exists
an object `W`, an effective epi `h : W ⟶ X` and a morphism `i : W ⟶ Z` making the diagram
commute.
```
W --i-→ Z
|       |
h       g
↓       ↓
X --f-→ Y
```
 -/
CategoryTheory.Preregular.exists_fac : ∀ {C : Type u_1} {inst : CategoryTheory.Category.{v_1, u_1} C} [self : CategoryTheory.Preregular C] {X Y Z : C}
  (f : X ⟶ Y) (g : Z ⟶ Y) [CategoryTheory.EffectiveEpi g],
  ∃ W h,
    ∃ (_ : CategoryTheory.EffectiveEpi h),
      ∃ i, CategoryTheory.CategoryStruct.comp i g = CategoryTheory.CategoryStruct.comp h f
-- Init.Data.Nat.ToString
Nat.toNat_digitChar_sub_48_of_lt_ten : ∀ {n : ℕ}, n < 10 → n.digitChar.toNat - 48 = n
-- Init.Data.Iterators.Lemmas.Combinators.FilterMap
Std.Iter.all_map : ∀ {α β β' : Type w} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Std.IteratorLoop α Id Id]
  [Std.LawfulIteratorLoop α Id Id] {it : Std.Iter β} {f : β → β'} {p : β' → Bool},
  Std.Iter.all p (Std.Iter.map f it) = Std.Iter.all (fun x => p (f x)) it
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.prop_of_epi : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderQuotients] {X Y : C} (f : X ⟶ Y) [CategoryTheory.Epi f], P X → P Y
-- Mathlib.Analysis.Polynomial.MahlerMeasure
Polynomial.intervalIntegrable_mahlerMeasure : ∀ (p : Polynomial ℂ),
  IntervalIntegrable (fun x => Real.log ‖Polynomial.eval (circleMap 0 1 x) p‖) MeasureTheory.volume 0 (2 * Real.pi)
-- Mathlib.Algebra.Homology.Double
HomologicalComplex.from_double_hom_ext_iff : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] {X₀ X₁ : C} {f : X₀ ⟶ X₁} {ι : Type u_2} {c : ComplexShape ι}
  {i₀ i₁ : ι} {hi₀₁ : c.Rel i₀ i₁} {K : HomologicalComplex C c} {φ φ' : HomologicalComplex.double f hi₀₁ ⟶ K},
  φ = φ' ↔ φ.f i₀ = φ'.f i₀ ∧ φ.f i₁ = φ'.f i₁
-- Init.Data.String.Slice
/-- Interprets a slice as the decimal representation of an integer, returning it. Returns `none` if
the string does not contain a decimal integer.

A string can be interpreted as a decimal integer if it only consists of at least one decimal digit
and optionally `-` in front. Leading `+` characters are not allowed.

Use `Slice.isInt` to check whether `Slice.toInt?` would return `some`.
`Slice.toInt!` is an alternative that panics instead of
returning `none` when the string is not an integer.

Examples:

* `"".toSlice.toInt? = none`

* `"-".toSlice.toInt? = none`

* `"0".toSlice.toInt? = some 0`

* `"5".toSlice.toInt? = some 5`

* `"-5".toSlice.toInt? = some (-5)`

* `"587".toSlice.toInt? = some 587`

* `"-587".toSlice.toInt? = some (-587)`

* `" 5".toSlice.toInt? = none`

* `"2-3".toSlice.toInt? = none`

* `"0xff".toSlice.toInt? = none`

* `"-0_1".toSlice.toInt? = some (-1)`

* `"-_1".toSlice.toInt? = none`
 -/
String.Slice.toInt? : String.Slice → Option ℤ
-- Aesop.Tree.Data
Aesop.Rapp.introducedMVars : Aesop.Rapp → Aesop.UnorderedArraySet Lean.MVarId
-- Mathlib.Combinatorics.SimpleGraph.Basic
/-- A simple graph is an irreflexive symmetric relation `Adj` on a vertex type `V`.
The relation describes which pairs of vertices are adjacent.
There is exactly one edge for every pair of adjacent vertices;
see `SimpleGraph.edgeSet` for the corresponding edge set.
 -/
SimpleGraph : Type u → Type u
-- Mathlib.Algebra.Module.Submodule.Map
Submodule.comap_mono : ∀ {R : Type u_1} {R₂ : Type u_3} {M : Type u_5} {M₂ : Type u_7} [inst : Semiring R] [inst_1 : Semiring R₂]
  [inst_2 : AddCommMonoid M] [inst_3 : AddCommMonoid M₂] [inst_4 : Module R M] [inst_5 : Module R₂ M₂] {σ₁₂ : R →+* R₂}
  {f : M →ₛₗ[σ₁₂] M₂} {q q' : Submodule R₂ M₂}, q ≤ q' → Submodule.comap f q ≤ Submodule.comap f q'
-- Mathlib.LinearAlgebra.BilinearMap
/-- A version of `Function.Surjective.comp` for composition of a bilinear map with a linear map.  -/
LinearMap.surjective_compr₂ₛₗ_of_exists_rightInverse : ∀ {R : Type u_2} [inst : CommSemiring R] {R₂ : Type u_14} {R₃ : Type u_15} {R₄ : Type u_16} {M : Type u_17}
  {N : Type u_18} {P : Type u_19} {Q : Type u_20} [inst_1 : CommSemiring R₂] [inst_2 : CommSemiring R₃]
  [inst_3 : CommSemiring R₄] [inst_4 : AddCommMonoid M] [inst_5 : AddCommMonoid N] [inst_6 : AddCommMonoid P]
  [inst_7 : AddCommMonoid Q] [inst_8 : Module R M] [inst_9 : Module R₂ N] [inst_10 : Module R₃ P]
  [inst_11 : Module R₄ Q] {σ₁₃ : R →+* R₃} {σ₁₄ : R →+* R₄} {σ₂₃ : R₂ →+* R₃} {σ₂₄ : R₂ →+* R₄} {σ₃₄ : R₃ →+* R₄}
  {σ₄₃ : R₄ →+* R₃} [inst_12 : RingHomCompTriple σ₂₃ σ₃₄ σ₂₄] [inst_13 : RingHomCompTriple σ₁₃ σ₃₄ σ₁₄]
  [RingHomCompTriple σ₂₄ σ₄₃ σ₂₃] [inst_15 : RingHomInvPair σ₃₄ σ₄₃] (f : M →ₛₗ[σ₁₃] N →ₛₗ[σ₂₃] P) (g : P →ₛₗ[σ₃₄] Q),
  Function.Surjective ⇑f → (∃ g', g ∘ₛₗ g' = LinearMap.id) → Function.Surjective ⇑(f.compr₂ₛₗ g)
-- Mathlib.Algebra.Homology.HomotopyCategory.HomComplex
/-- the condition on the two integers  -/
CochainComplex.HomComplex.Triplet.hpq : ∀ {n : ℤ} (self : CochainComplex.HomComplex.Triplet n), self.p + n = self.q
-- Mathlib.RingTheory.Finiteness.Cofinite
/-- If `S` and `T` are co-disjoint and `S` is FG, then `T` is CoFG.  -/
Submodule.FG.cofg_of_codisjoint : ∀ {R : Type u_1} [inst : Ring R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] {S T : Submodule R M},
  Codisjoint S T → S.FG → T.CoFG
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.concat.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → α → Sort u_2) (a : α) (as : List α) (b : α) (h_1 : (b : α) → motive [] b)
  (h_2 : (a : α) → (as : List α) → (b : α) → motive (a :: as) b),
  (match a :: as, b with
    | [], b => h_1 b
    | a :: as, b => h_2 a as b) =
    h_2 a as b
-- Mathlib.Algebra.Group.Subgroup.Defs
add_mem_cancel_left : ∀ {G : Type u_1} [inst : AddGroup G] {S : Type u_4} {H : S} [inst_1 : SetLike S G] [AddSubgroupClass S G] {x y : G},
  x ∈ H → (x + y ∈ H ↔ y ∈ H)
-- Mathlib.Analysis.SpecialFunctions.Complex.Circle
Circle.angleDiff_lt_two_pi : ∀ (x y : Circle), x.angleDiff y < 2 * Real.pi
-- Mathlib.Algebra.Jordan.Basic
commute_lmul_lmul_sq : ∀ {A : Type u_1} [inst : NonUnitalNonAssocRing A] [IsJordan A] (a : A),
  Commute (AddMonoid.End.mulLeft a) (AddMonoid.End.mulLeft (a * a))
-- Lean.DocString.Extension
Lean.addInheritedDocString : {m : Type → Type} → [Monad m] → [Lean.MonadError m] → [Lean.MonadEnv m] → Lean.Name → Lean.Name → m Unit
-- Mathlib.Analysis.Normed.Operator.LinearIsometry
LinearIsometryEquiv.image_ball : ∀ {R : Type u_1} {R₂ : Type u_2} {E : Type u_5} {E₂ : Type u_6} [inst : Semiring R] [inst_1 : Semiring R₂]
  {σ₁₂ : R →+* R₂} {σ₂₁ : R₂ →+* R} [inst_2 : RingHomInvPair σ₁₂ σ₂₁] [inst_3 : RingHomInvPair σ₂₁ σ₁₂]
  [inst_4 : SeminormedAddCommGroup E] [inst_5 : SeminormedAddCommGroup E₂] [inst_6 : Module R E] [inst_7 : Module R₂ E₂]
  (e : E ≃ₛₗᵢ[σ₁₂] E₂) (x : E) (r : ℝ), ⇑e '' Metric.ball x r = Metric.ball (e x) r
-- Mathlib.CategoryTheory.Sites.IsSheafFor
CategoryTheory.Presieve.isAmalgamation_restrict : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {P : CategoryTheory.Functor Cᵒᵖ (Type w)} {X : C}
  {R₁ R₂ : CategoryTheory.Presieve X} (h : R₁ ≤ R₂) (x : CategoryTheory.Presieve.FamilyOfElements P R₂)
  (t : P.obj (Opposite.op X)),
  x.IsAmalgamation t → (CategoryTheory.Presieve.FamilyOfElements.restrict h x).IsAmalgamation t
-- Mathlib.Logic.Equiv.Set
Equiv.strictMono_setCongr : ∀ {α : Type u_3} [inst : Preorder α] {S T : Set α} (h : S = T), StrictMono ⇑(Equiv.setCongr h)
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.supSpanSingleton_apply_of_mem : ∀ {E : Type u_4} [inst : AddCommGroup E] {F : Type u_5} [inst_1 : AddCommGroup F] {K : Type u_7} {L : Type u_8}
  [inst_2 : DivisionRing K] [inst_3 : DivisionRing L] {σ : K →+* L} [inst_4 : Module K E] [inst_5 : Module L F]
  (f : E →ₛₗ.[σ] F) {x : E} (y : F) (hx : x ∉ f.domain) (x' : ↥(f.supSpanSingleton x y hx).domain)
  (hx' : ↑x' ∈ f.domain), ↑(f.supSpanSingleton x y hx) x' = ↑f ⟨↑x', hx'⟩
-- Batteries.Recycling.RBTree.Depth
RBTree.RBNode.depth.eq_1 : ∀ {α : Type u_1}, RBTree.RBNode.nil.depth = 0
-- Mathlib.RingTheory.UniqueFactorizationDomain.ClassGroup
/-- **Alias** of `IsGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal`. -/
NormalizedGCDMonoid.isPrincipal_of_exists_mul_ne_zero_isPrincipal : ∀ {R : Type u_1} [inst : CommRing R] [IsDomain R] [IsGCDMonoid R] {J : Ideal R},
  (∃ K, J * K ≠ 0 ∧ Submodule.IsPrincipal (J * K)) → Submodule.IsPrincipal J
-- Mathlib.Algebra.Order.Group.Synonym
OrderDual.instDivInvMonoid : {α : Type u_1} → [DivInvMonoid α] → DivInvMonoid αᵒᵈ
-- Std.Http.Transport
_private.Std.Http.Transport.0.Std.Http.Internal.Mock.Server.mk.sizeOf_spec : ∀ (shared : Std.Http.Internal.Mock.SharedState✝), sizeOf { shared := shared } = 1 + sizeOf shared
-- Mathlib.Topology.Algebra.LinearTopology
isLinearTopology_iff_hasBasis_open_submodule : ∀ {R : Type u_1} {M : Type u_3} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : TopologicalSpace M] [ContinuousAdd M],
  IsLinearTopology R M ↔ (nhds 0).HasBasis (fun N => IsOpen ↑N) fun N => ↑N
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The multiplication morphism of a monoid object.  -/
CategoryTheory.MonObj.«termμ[_]» : Lean.ParserDescr
-- Mathlib.CategoryTheory.WithTerminal.Basic
CategoryTheory.WithTerminal.equivComma_inverse_map_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u_1} [inst_1 : CategoryTheory.Category.{v_1, u_1} D]
  {X Y : CategoryTheory.Comma (CategoryTheory.Functor.id (CategoryTheory.Functor C D)) (CategoryTheory.Functor.const C)}
  (φ : X ⟶ Y) (x : CategoryTheory.WithTerminal C),
  (CategoryTheory.WithTerminal.equivComma.inverse.map φ).app x =
    match x with
    | CategoryTheory.WithTerminal.of x => φ.left.app x
    | CategoryTheory.WithTerminal.star => φ.right
-- Mathlib.Data.Multiset.UnionInter
Multiset.add_eq_union_iff_disjoint : ∀ {α : Type u_1} [inst : DecidableEq α] {s t : Multiset α}, s + t = s ∪ t ↔ Disjoint s t
-- Lean.Environment
_private.Lean.Environment.0.Lean.Environment.enableRealizationsForConst.unsafe_1 : Lean.Environment → NonScalar
-- Mathlib.Topology.Algebra.ProperAction.Basic
/-- If `H` is a closed subgroup of `G` and `G` acts properly on `X`, then so does `H`.  -/
instProperVAddSubtypeMemAddSubgroupOfIsClosedCoe : ∀ {G : Type u_1} {X : Type u_2} [inst : AddGroup G] [inst_1 : AddAction G X] [inst_2 : TopologicalSpace G]
  [inst_3 : TopologicalSpace X] {H : AddSubgroup G} [ProperVAdd G X] [H_closed : IsClosed ↑H], ProperVAdd (↥H) X
-- Mathlib.Algebra.Group.Subgroup.MulOppositeLemmas
Subgroup.unop_iSup : ∀ {ι : Sort u_1} {G : Type u_2} [inst : Group G] (S : ι → Subgroup Gᵐᵒᵖ), (iSup S).unop = ⨆ i, (S i).unop