mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.arrowCongr'_comp : ∀ {R : Type u_1} {A₁ : Type u_2} {A₂ : Type u_3} {A₃ : Type u_4} {A₁' : Type u_5} {A₂' : Type u_6} {A₃' : Type u_7}
  [inst : Monoid R] [inst_1 : NonUnitalNonAssocSemiring A₁] [inst_2 : DistribMulAction R A₁] [inst_3 : Star A₁]
  [inst_4 : NonUnitalNonAssocSemiring A₂] [inst_5 : DistribMulAction R A₂] [inst_6 : Star A₂]
  [inst_7 : NonUnitalNonAssocSemiring A₃] [inst_8 : DistribMulAction R A₃] [inst_9 : Star A₃]
  [inst_10 : NonUnitalNonAssocSemiring A₁'] [inst_11 : DistribMulAction R A₁'] [inst_12 : Star A₁']
  [inst_13 : NonUnitalNonAssocSemiring A₂'] [inst_14 : DistribMulAction R A₂'] [inst_15 : Star A₂']
  [inst_16 : NonUnitalNonAssocSemiring A₃'] [inst_17 : DistribMulAction R A₃'] [inst_18 : Star A₃'] (e₁ : A₁ ≃⋆ₐ[R] A₁')
  (e₂ : A₂ ≃⋆ₐ[R] A₂') (e₃ : A₃ ≃⋆ₐ[R] A₃') (f : A₁ →⋆ₙₐ[R] A₂) (g : A₂ →⋆ₙₐ[R] A₃),
  (e₁.arrowCongr' e₃) (g.comp f) = ((e₂.arrowCongr' e₃) g).comp ((e₁.arrowCongr' e₂) f)
-- Mathlib.Topology.MetricSpace.Algebra
instIsBoundedSMulSeparationQuotient : ∀ {α : Type u_4} {β : Type u_5} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] [inst_2 : Zero α]
  [inst_3 : Zero β] [inst_4 : SMul α β] [inst_5 : IsBoundedSMul α β], IsBoundedSMul α (SeparationQuotient β)
-- Lean.LocalContext
Lean.LocalContext.foldr : {β : Type u_1} → Lean.LocalContext → (Lean.LocalDecl → β → β) → β → β
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHom_comp : ∀ {C : Type u_1} {D : Type u_2} {inst : CategoryTheory.Category.{v_1, u_1} C}
  {inst_1 : CategoryTheory.Category.{v_2, u_2} D} {inst_2 : CategoryTheory.MonoidalCategory C}
  [self : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] {c c' c'' : C} {d d' d'' : D} (f₁ : c ⟶ c')
  (f₂ : c' ⟶ c'') (g₁ : d ⟶ d') (g₂ : d' ⟶ d''),
  CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom (CategoryTheory.CategoryStruct.comp f₁ f₂)
      (CategoryTheory.CategoryStruct.comp g₁ g₂) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f₁ g₁)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHom f₂ g₂)
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.get?_eq_some_getD : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t.WF → ∀ {a fallback : α}, a ∈ t → t.get? a = some (t.getD a fallback)
-- Mathlib.Geometry.Euclidean.Circumcenter
/-- If there exists a distance that a point has from all vertices of a
simplex, the orthogonal projection of that point onto the subspace
spanned by that simplex is its circumcenter.  -/
Affine.Simplex.orthogonalProjection_eq_circumcenter_of_exists_dist_eq : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {n : ℕ} (s : Affine.Simplex ℝ P n) {p : P},
  (∃ r, ∀ (i : Fin (n + 1)), dist (s.points i) p = r) → ↑(s.orthogonalProjectionSpan p) = s.circumcenter
-- Mathlib.Algebra.Ring.GeomSum
Commute.sub_dvd_pow_sub_pow : ∀ {R : Type u_1} [inst : Ring R] {x y : R}, Commute x y → ∀ (n : ℕ), x - y ∣ x ^ n - y ^ n
-- Lean.Meta.Sym.SymM
/-- Cache for value-level canonicalization (no type reductions applied).  -/
Lean.Meta.Sym.Canon.State.cache : Lean.Meta.Sym.Canon.State → Std.HashMap Lean.Expr Lean.Expr
-- Mathlib.Data.Erased
/-- Collapses two levels of erasure.
 -/
Erased.join : {α : Sort u_1} → Erased (Erased α) → Erased α
-- Mathlib.CategoryTheory.Abelian.SerreClass.Localization
CategoryTheory.ObjectProperty.SerreClassLocalization.map_eq_zero_iff : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C] {D : Type u'}
  [inst_2 : CategoryTheory.Category.{v', u'} D] (L : CategoryTheory.Functor C D) (P : CategoryTheory.ObjectProperty C)
  [inst_3 : P.IsSerreClass] [L.IsLocalization P.isoModSerre] [inst_5 : CategoryTheory.Preadditive D] [L.Additive]
  {X Y : C} (f : X ⟶ Y), L.map f = 0 ↔ P (CategoryTheory.Abelian.image f)
-- Mathlib.CategoryTheory.Abelian.Transfer
CategoryTheory.AsSmall.abelian : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [CategoryTheory.Abelian C] → CategoryTheory.Abelian (CategoryTheory.AsSmall C)
-- Mathlib.Combinatorics.SetFamily.AhlswedeZhang
Finset.truncatedInf_union : ∀ {α : Type u_1} [inst : SemilatticeInf α] {s t : Finset α} {a : α} [inst_1 : DecidableLE α] [inst_2 : BoundedOrder α]
  [inst_3 : DecidableEq α],
  a ∈ upperClosure ↑s → a ∈ upperClosure ↑t → (s ∪ t).truncatedInf a = s.truncatedInf a ⊓ t.truncatedInf a
-- Mathlib.Algebra.ContinuedFractions.ConvergentsEquiv
/-- The auxiliary function `convs'Aux` returns the same value for a sequence and the
corresponding squashed sequence at the squashed position.  -/
GenContFract.succ_succ_nth_conv'Aux_eq_succ_nth_conv'Aux_squashSeq : ∀ {K : Type u_1} {n : ℕ} {s : Stream'.Seq (GenContFract.Pair K)} [inst : DivisionRing K],
  GenContFract.convs'Aux s (n + 2) = GenContFract.convs'Aux (GenContFract.squashSeq s n) (n + 1)
-- Lean.Server.Completion.CompletionCollectors
_private.Lean.Server.Completion.CompletionCollectors.0.Lean.Server.Completion.matchAtomic : Lean.Name → Lean.Name → Bool → Bool
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.SmallCategoryCardinalLT.exists_equivalence : ∀ (κ : Cardinal.{w}) (C : Type u) [inst : CategoryTheory.Category.{v, u} C],
  HasCardinalLT (CategoryTheory.Arrow C) κ →
    ∃ S, Nonempty (CategoryTheory.SmallCategoryCardinalLT.categoryFamily κ S ≌ C)
-- Mathlib.RingTheory.Ideal.Height
_private.Mathlib.RingTheory.Ideal.Height.0.Ideal.primeHeight.congr_simp : ∀ {R : Type u_1} [inst : CommRing R] (I I_1 : Ideal R) (e_I : I = I_1) [hI : I.IsPrime],
  Ideal.primeHeight✝ I = Ideal.primeHeight✝ I_1
-- Init.Data.ByteArray.Lemmas
ByteArray.extract_eq_extract_iff_getElem : ∀ {as bs : ByteArray} {i j len : ℕ} (hi : i + len ≤ as.size) (hj : j + len ≤ bs.size),
  as.extract i (i + len) = bs.extract j (j + len) ↔ ∀ (k : ℕ) (hk : k < len), as[i + k] = bs[j + k]
-- Mathlib.Order.Closure
/-- Every element is less than its closure. This property is sometimes referred to as extensivity or
inflationarity.  -/
ClosureOperator.le_closure : ∀ {α : Type u_1} [inst : Preorder α] (c : ClosureOperator α) (x : α), x ≤ c x
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Basic
/-- The semantics for `BVBinPred`.
 -/
Std.Tactic.BVDecide.BVBinPred.eval : {w : ℕ} → Std.Tactic.BVDecide.BVBinPred → BitVec w → BitVec w → Bool
-- Mathlib.Tactic.Lemma
/-- Implementation of the `lemma` command, by macro expansion to `theorem`.  -/
expandLemma : Lean.Macro
-- Mathlib.Algebra.Group.UniqueProds.Basic
TwoUniqueSums.instForall : ∀ {ι : Type u_2} (G : ι → Type u_1) [inst : (i : ι) → Add (G i)] [∀ (i : ι), TwoUniqueSums (G i)],
  TwoUniqueSums ((i : ι) → G i)
-- Mathlib.Geometry.Euclidean.Sphere.Tangent
EuclideanGeometry.Sphere.IsExtTangentAt.mem_left : ∀ {V : Type u_1} {P : Type u_2} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : MetricSpace P]
  [inst_3 : NormedAddTorsor V P] {s₁ s₂ : EuclideanGeometry.Sphere P} {p : P}, s₁.IsExtTangentAt s₂ p → p ∈ s₁
-- Qq.Match
Qq.Impl.isIrrefutablePattern : Lean.Term → Bool
-- Mathlib.GroupTheory.Commutator.Basic
commutator_def : ∀ (G : Type u_1) [inst : Group G], commutator G = ⁅⊤, ⊤⁆
-- Init.Data.Range.Polymorphic.IntLemmas
Int.getElem!_toArray_roo : ∀ {m n : ℤ} {i : ℕ}, (m<...n).toArray[i]! = if i < (n - (m + 1)).toNat then m + 1 + ↑i else 0
-- Mathlib.Analysis.Calculus.ContDiff.Defs
contDiff_one_iff_fderiv : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F},
  ContDiff 𝕜 1 f ↔ Differentiable 𝕜 f ∧ Continuous (fderiv 𝕜 f)
-- Mathlib.Topology.FiberBundle.Basic
FiberBundleCore.mk_mem_localTrivAt_source : ∀ {ι : Type u_1} {B : Type u_2} {F : Type u_3} [inst : TopologicalSpace B] [inst_1 : TopologicalSpace F]
  (Z : FiberBundleCore ι B F) (b : B) (a : F), ⟨b, a⟩ ∈ (Z.localTrivAt b).source
-- Mathlib.CategoryTheory.SingleObj
/-- Abbreviation that allows writing `CategoryTheory.SingleObj` rather than `Quiver.SingleObj`.
 -/
CategoryTheory.SingleObj : Type u_1 → Type
-- Lean.DocString.Extension
Lean.VersoModuleDocs.Snippet.mk.injEq : ∀ (text : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))
  (sections : Array (ℕ × Lean.DeclarationRange × Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty))
  (declarationRange : Lean.DeclarationRange) (text_1 : Array (Lean.Doc.Block Lean.ElabInline Lean.ElabBlock))
  (sections_1 : Array (ℕ × Lean.DeclarationRange × Lean.Doc.Part Lean.ElabInline Lean.ElabBlock Empty))
  (declarationRange_1 : Lean.DeclarationRange),
  ({ text := text, sections := sections, declarationRange := declarationRange } =
      { text := text_1, sections := sections_1, declarationRange := declarationRange_1 }) =
    (text = text_1 ∧ sections = sections_1 ∧ declarationRange = declarationRange_1)
-- Mathlib.AlgebraicGeometry.IdealSheaf.Basic
AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals_mono : ∀ {X : AlgebraicGeometry.Scheme}, Monotone AlgebraicGeometry.Scheme.IdealSheafData.ofIdeals
-- Aesop.Stats.Basic
Aesop.ScriptGenerated.perfect : Aesop.ScriptGenerated → Bool
-- Mathlib.Order.LiminfLimsup
Filter.liminf_bot : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] (f : β → α), Filter.liminf f ⊥ = ⊤
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.eq_1 : ∀ {β : Type u_1} {α : Type u_2} [inst : LE β] [inst_1 : DecidableLE β] (f : α → β) (y : α) (ys : List α)
  (h_2 : y :: ys ≠ []), List.minIdxOn f (y :: ys) h_2 = List.minIdxOn.go✝ f y 0 1 ys
-- Init.GrindInstances.ToInt
Lean.Grind.toInt_bitVec : ∀ {v : ℕ} (x : BitVec v), ↑x = ↑x.toNat
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.StructuredArrow.pre_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {B : Type u₄} [inst_2 : CategoryTheory.Category.{v₄, u₄} B] (S : D) (F : CategoryTheory.Functor B C)
  (G : CategoryTheory.Functor C D) (X : CategoryTheory.Comma (CategoryTheory.Functor.fromPUnit S) (F.comp G)),
  ((CategoryTheory.StructuredArrow.pre S F G).obj X).hom = X.hom
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.continuousOn_symm : ∀ {𝕜 : 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) {s : Set E},
  ContinuousOn (↑I.symm) s
-- Mathlib.GroupTheory.FinitelyPresentedGroup
/-- `Multiplicative ℤ` is finitely presented.  -/
Group.IsFinitelyPresented.instMultiplicativeInt : Group.IsFinitelyPresented (Multiplicative ℤ)
-- Mathlib.Order.Hom.Lex
/-- Lexicographic product type with `Unique` type on the left is `OrderIso` to the right.  -/
Prod.Lex.uniqueProd : (α : Type u_2) → (β : Type u_3) → [inst : Preorder α] → [Unique α] → [inst_2 : LE β] → Lex (α × β) ≃o β
-- Mathlib.Analysis.Calculus.ContDiff.Defs
AnalyticOn.contDiff : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {n : WithTop ℕ∞}, AnalyticOn 𝕜 f Set.univ → ContDiff 𝕜 n f
-- Mathlib.RingTheory.AlgebraicIndependent.TranscendenceBasis
AlgebraicIndependent.matroid.congr_simp : ∀ (R : Type u_1) (A : Type w) [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  [inst_3 : FaithfulSMul R A] [inst_4 : NoZeroDivisors A],
  AlgebraicIndependent.matroid R A = AlgebraicIndependent.matroid R A
-- Mathlib.CategoryTheory.Preadditive.AdditiveFunctor
CategoryTheory.Functor.additive_of_comp_faithful : ∀ {C : Type u_1} {D : Type u_2} {E : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Category.{v_3, u_3} E]
  [inst_3 : CategoryTheory.Preadditive C] [inst_4 : CategoryTheory.Preadditive D]
  [inst_5 : CategoryTheory.Preadditive E] (F : CategoryTheory.Functor C D) (G : CategoryTheory.Functor D E) [G.Additive]
  [(F.comp G).Additive] [G.Faithful], F.Additive
-- Mathlib.Analysis.Normed.Lp.ProdLp
WithLp.prodContinuousLinearEquiv_symm_apply_ofLp : ∀ (p : ENNReal) (𝕜 : Type u_1) (α : Type u_2) (β : Type u_3) [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β]
  [inst_2 : Semiring 𝕜] [inst_3 : AddCommGroup α] [inst_4 : AddCommGroup β] [inst_5 : Module 𝕜 α] [inst_6 : Module 𝕜 β]
  (a : α × β), ((WithLp.prodContinuousLinearEquiv p 𝕜 α β).symm a).ofLp = a
-- Mathlib.Algebra.Group.Opposite
AddOpposite.instRightCancelSemigroup : {α : Type u_1} → [RightCancelSemigroup α] → RightCancelSemigroup αᵃᵒᵖ
-- Mathlib.RingTheory.IntegralClosure.IntegralRestrict
Algebra.intNorm_eq_of_isLocalization : ∀ {A : Type u_1} {B : Type u_6} [inst : CommRing A] [inst_1 : CommRing B] [inst_2 : Algebra A B] {Aₘ : Type u_9}
  {Bₘ : Type u_10} [inst_3 : CommRing Aₘ] [inst_4 : CommRing Bₘ] [inst_5 : Algebra Aₘ Bₘ] [inst_6 : Algebra A Aₘ]
  [inst_7 : Algebra B Bₘ] [inst_8 : Algebra A Bₘ] [IsScalarTower A Aₘ Bₘ] [IsScalarTower A B Bₘ] (M : Submonoid A)
  [IsLocalization M Aₘ] [IsLocalization (Algebra.algebraMapSubmonoid B M) Bₘ] [inst_13 : IsIntegrallyClosed A]
  [inst_14 : IsDomain A] [inst_15 : IsDomain B] [inst_16 : IsIntegrallyClosed B] [inst_17 : Algebra.IsIntegral A B]
  [inst_18 : Module.IsTorsionFree A B] [inst_19 : IsDomain Aₘ] [inst_20 : IsIntegrallyClosed Aₘ] [inst_21 : IsDomain Bₘ]
  [inst_22 : IsIntegrallyClosed Bₘ] [inst_23 : Module.IsTorsionFree Aₘ Bₘ] [inst_24 : Algebra.IsIntegral Aₘ Bₘ]
  [FiniteDimensional (FractionRing A) (FractionRing B)] (x : B),
  (algebraMap A Aₘ) ((Algebra.intNorm A B) x) = (Algebra.intNorm Aₘ Bₘ) ((algebraMap B Bₘ) x)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LetRecToLift.termination : Lean.Elab.Term.LetRecToLift → Lean.Elab.TerminationHints
-- Init.Data.Vector.Lemmas
Vector.toArray_reverse : ∀ {α : Type u_1} {n : ℕ} (xs : Vector α n), xs.reverse.toArray = xs.toArray.reverse
-- Mathlib.Algebra.MvPolynomial.Equiv
MvPolynomial.eval₂_const_uniqueAlgEquiv : ∀ {σ : Type u_1} {R : Type u_2} {S : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Unique σ]
  {f : MvPolynomial σ R} {φ : R →+* S} {a : S},
  Polynomial.eval₂ φ a ((MvPolynomial.uniqueAlgEquiv R σ) f) = MvPolynomial.eval₂ φ (fun x => a) f
-- Mathlib.Data.WSeq.Basic
_private.Mathlib.Data.WSeq.Basic.0.Stream'.WSeq.drop.match_1.eq_1 : ∀ (motive : ℕ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match 0 with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_1 ()
-- Mathlib.Data.TypeVec
TypeVec.prod.diag.eq_1 : ∀ (n : ℕ) (α : TypeVec.{u} n.succ) (a : Fin2 n) (x_4 : α a.fs), TypeVec.prod.diag a.fs x_4 = TypeVec.prod.diag a x_4
-- Mathlib.Algebra.FreeMonoid.Basic
FreeMonoid.of_injective : ∀ {α : Type u_1}, Function.Injective FreeMonoid.of
-- Mathlib.Topology.UniformSpace.Equiv
UniformEquiv.piCongrRight_symm : ∀ {ι : Type u_4} {β₁ : ι → Type u_5} {β₂ : ι → Type u_6} [inst : (i : ι) → UniformSpace (β₁ i)]
  [inst_1 : (i : ι) → UniformSpace (β₂ i)] (F : (i : ι) → β₁ i ≃ᵤ β₂ i),
  (UniformEquiv.piCongrRight F).symm = UniformEquiv.piCongrRight fun i => (F i).symm
-- Mathlib.Order.ModularLattice
Disjoint.isCompl_sup_right_of_isCompl_sup_left : ∀ {α : Type u_1} {a b c : α} [inst : Lattice α] [inst_1 : BoundedOrder α] [IsModularLattice α],
  Disjoint a b → IsCompl (a ⊔ b) c → IsCompl a (b ⊔ c)
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
SimplexCategoryGenRel.δ_comp_δ_assoc : ∀ {n : ℕ} {i j : Fin (n + 2)},
  i ≤ j →
    ∀ {Z : SimplexCategoryGenRel} (h : SimplexCategoryGenRel.mk (n + 1 + 1) ⟶ Z),
      CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i)
          (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ j.succ) h) =
        CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ j)
          (CategoryTheory.CategoryStruct.comp (SimplexCategoryGenRel.δ i.castSucc) h)
-- Mathlib.Algebra.Order.CauSeq.Completion
CauSeq.Completion.ofRat_injective : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [inst_2 : IsStrictOrderedRing α] {β : Type u_2}
  [inst_3 : Ring β] {abv : β → α} [inst_4 : IsAbsoluteValue abv], Function.Injective CauSeq.Completion.ofRat
-- Mathlib.Algebra.Homology.DerivedCategory.Ext.ExactSequences
CategoryTheory.Abelian.Ext.mono_postcomp_mk₀_of_mono : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : CategoryTheory.HasExt C] (L : C) {M N : C} (f : M ⟶ N) [hf : CategoryTheory.Mono f],
  CategoryTheory.Mono (AddCommGrpCat.ofHom ((CategoryTheory.Abelian.Ext.mk₀ f).postcomp L ⋯))
-- Mathlib.Data.PNat.Xgcd
PNat.XgcdType.instSizeOf : SizeOf PNat.XgcdType
-- Lean.Elab.InfoTree.Types
Lean.Elab.Info.ofOptionInfo.inj : ∀ {i i_1 : Lean.Elab.OptionInfo}, Lean.Elab.Info.ofOptionInfo i = Lean.Elab.Info.ofOptionInfo i_1 → i = i_1
-- Mathlib.Algebra.Divisibility.Basic
/-- A monoid is a decomposition monoid if every element is primal. An integral domain whose
multiplicative monoid is a decomposition monoid, is called a pre-Schreier domain; it is a
Schreier domain if it is moreover integrally closed.  -/
DecompositionMonoid : (α : Type u_1) → [Semigroup α] → Prop
-- Mathlib.Algebra.Module.LocalizedModule.IsLocalization
/-- `IsLocalization.mk'` agrees with `IsLocalizedModule.mk'`.  -/
IsLocalization.mk'_eq_mk' : ∀ {R : Type u_1} [inst : CommSemiring R] (S : Submonoid R) (A : Type u_2) [inst_1 : CommSemiring A]
  [inst_2 : Algebra R A] [inst_3 : IsLocalization S A] (x : R) (s : ↥S),
  IsLocalization.mk' A x s = IsLocalizedModule.mk' (Algebra.linearMap R A) x s
-- Mathlib.LinearAlgebra.Prod
Submodule.ker_inl : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂], (LinearMap.inl R M M₂).ker = ⊥
-- Batteries.Util.Cache
/-- Get matches from both the discrimination tree for declarations in the current file,
and for the imports.

Note that if you are calling this multiple times with the same environment,
it will rebuild the discrimination tree for the current file multiple times,
and it would be more efficient to call `c.get` once,
and then call `DiscrTree.getMatch` multiple times.
 -/
Batteries.Tactic.DiscrTreeCache.getMatch : {α : Type} → Batteries.Tactic.DiscrTreeCache α → Lean.Expr → Lean.MetaM (Array α)
-- Mathlib.Data.Nat.Factorial.Basic
Nat.factorial_pos : ∀ (n : ℕ), 0 < n.factorial
-- Init.Core
/-- `a ∩ b` is the intersection of `a` and `b`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∩` in identifiers is `inter`. -/
Inter.inter : {α : Type u} → [self : Inter α] → α → α → α
-- Mathlib.GroupTheory.SpecificGroups.Cyclic
IsAddCyclic.index_nsmulAddMonoidHom_range : ∀ (G : Type u_2) [inst : AddCommGroup G] [IsAddCyclic G] [Finite G] (d : ℕ),
  (nsmulAddMonoidHom d).range.index = (Nat.card G).gcd d
-- Mathlib.RingTheory.Etale.Kaehler
Algebra.tensorH1CotangentOfIsLocalization_toLinearMap : ∀ (R : Type u_1) {S : Type u_2} (T : Type u_3) [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : CommRing T]
  [inst_3 : Algebra R S] [inst_4 : Algebra R T] [inst_5 : Algebra S T] [inst_6 : IsScalarTower R S T] (M : Submonoid S)
  [inst_7 : IsLocalization M T],
  ↑(Algebra.tensorH1CotangentOfIsLocalization R T M) = LinearMap.liftBaseChange T (Algebra.H1Cotangent.map R R S T)
-- Std.Sync.Semaphore
_private.Std.Sync.Semaphore.0.Std.SemaphoreState : Type
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.inv_vle_one : ∀ {K : Type u_2} [inst : DivisionRing K] [inst_1 : ValuativeRel K] {x : K}, x ≠ 0 → (x⁻¹ ≤ᵥ 1 ↔ 1 ≤ᵥ x)
-- Init.Data.List.Basic
_private.Init.Data.List.Basic.0.List.getLast?.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (a : α) (as : List α) (h_1 : Unit → motive [])
  (h_2 : (a : α) → (as : List α) → motive (a :: as)),
  (match a :: as with
    | [] => h_1 ()
    | a :: as => h_2 a as) =
    h_2 a as
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.maxKeyD_alter_eq_self : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.ExtDTreeMap α β cmp} [inst : Std.TransCmp cmp]
  [inst_1 : Std.LawfulEqCmp cmp] {k : α} {f : Option (β k) → Option (β k)},
  t.alter k f ≠ ∅ →
    ∀ {fallback : α},
      (t.alter k f).maxKeyD fallback = k ↔ (f (t.get? k)).isSome = true ∧ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Mathlib.AlgebraicTopology.EilenbergSteenrod
TopPair.HomologyPretheory.inv_hom_iso_homₚ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {ι : Type u_2} {c : ComplexShape ι} {HP HP' : TopPair.HomologyPretheory C c} (f : HP ⟶ HP') (i : ι),
  CategoryTheory.CategoryStruct.comp (HP.iso i).inv (CategoryTheory.CategoryStruct.comp (f.hom i) (HP'.iso i).hom) =
    TopPair.incl.whiskerLeft (f.homₚ i)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.toBitVec_minValueSealed_eq_intMinSealed : Int16.minValueSealed✝.toBitVec = BitVec.Signed.intMinSealed✝ 16
-- Mathlib.LinearAlgebra.Transvection.Basic
/-- Characterization of transvections within dilatransvections.  -/
LinearEquiv.mem_transvections_iff_mem_dilatransvections_and_fixedReduce_eq_one : ∀ {V : Type u_2} [inst : AddCommGroup V] {K : Type u_3} [inst_1 : DivisionRing K] [inst_2 : Module K V]
  [Module.Finite K V] (e : V ≃ₗ[K] V),
  e ∈ LinearEquiv.transvections K V ↔ e ∈ LinearEquiv.dilatransvections K V ∧ e.fixedReduce = 1
-- Mathlib.CategoryTheory.Limits.Types.Colimits
CategoryTheory.Functor.CoconeTypes.isColimit_iff : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] {F : CategoryTheory.Functor J (Type u)} (c : F.CoconeTypes),
  c.IsColimit ↔ Nonempty (CategoryTheory.Limits.IsColimit (F.coconeTypesEquiv c))
-- Mathlib.Control.Traversable.Instances
List.traverse.eq_2 : ∀ {F : Type u_1 → Type u_2} {α : Type u_3} {β : Type u_1} [inst : Applicative F] (f : α → F β) (a : α) (l : List α),
  List.traverse f (a :: l) = List.cons <$> f a <*> List.traverse f l
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.tendsto_nhds_zero : ∀ {α : Type u_1} {f : Filter α} {u : α → ENNReal}, Filter.Tendsto u f (nhds 0) ↔ ∀ ε > 0, ∀ᶠ (x : α) in f, u x ≤ ε
-- Lean.Data.Lsp.Diagnostics
/-- Deprecated or obsolete code. Rendered with a strike-through.  -/
Lean.Lsp.DiagnosticTag.deprecated : Lean.Lsp.DiagnosticTag
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.ofFinsupp_pow : ∀ {R : Type u} [inst : Semiring R] (a : AddMonoidAlgebra R ℕ) (n : ℕ), { toFinsupp := a ^ n } = { toFinsupp := a } ^ n
-- Mathlib.CategoryTheory.Limits.HasLimits
/-- Functoriality of colimits.

Usually this morphism should be accessed through `colim.map`,
but may be needed separately when you have specified colimits for the source and target functors,
but not necessarily for all functors of shape `J`.
 -/
CategoryTheory.Limits.colimMap : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F G : CategoryTheory.Functor J C} →
          [inst_2 : CategoryTheory.Limits.HasColimit F] →
            [inst_3 : CategoryTheory.Limits.HasColimit G] →
              (G ⟶ F) → (CategoryTheory.Limits.colimit G ⟶ CategoryTheory.Limits.colimit F)
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.instIsOrderedAddMonoidLex : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : PartialOrder R] [inst_2 : AddCommMonoid R]
  [AddLeftStrictMono R], IsOrderedAddMonoid (Lex (HahnSeries Γ R))
-- Mathlib.Data.Multiset.MapFold
Multiset.map_subset_map : ∀ {α : Type u_1} {β : Type v} {f : α → β} {s t : Multiset α}, s ⊆ t → Multiset.map f s ⊆ Multiset.map f t
-- Mathlib.CategoryTheory.Sites.DenseSubsite.Basic
CategoryTheory.Functor.IsCoverDense.Types.sheafIso_inv_hom : ∀ {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] {K : CategoryTheory.GrothendieckTopology D}
  {G : CategoryTheory.Functor C D} [inst_2 : G.IsCoverDense K] [inst_3 : G.IsLocallyFull K]
  {ℱ ℱ' : CategoryTheory.Sheaf K (Type v)} (i : G.op.comp ℱ.obj ≅ G.op.comp ℱ'.obj),
  (CategoryTheory.Functor.IsCoverDense.Types.sheafIso i).inv.hom =
    (CategoryTheory.Functor.IsCoverDense.Types.presheafIso i).inv