mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.DayConvolution
CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor_inv_app_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {V : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} V]
  [inst_2 : CategoryTheory.MonoidalCategory C] [inst_3 : CategoryTheory.MonoidalCategory V]
  (U : CategoryTheory.Functor C V) [inst_4 : CategoryTheory.MonoidalCategory.DayConvolutionUnit U]
  (F : CategoryTheory.Functor C V)
  [inst_5 :
    ∀ (v : V) (d : C),
      CategoryTheory.Limits.PreservesColimitsOfShape
        (CategoryTheory.CostructuredArrow
          (CategoryTheory.Functor.fromPUnit (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)) d)
        (CategoryTheory.MonoidalCategory.tensorLeft v)]
  [inst_6 : CategoryTheory.MonoidalCategory.DayConvolution F U] (x : C) {Z : V}
  (h : (CategoryTheory.MonoidalCategory.DayConvolution.convolution F U).obj x ⟶ Z),
  CategoryTheory.CategoryStruct.comp ((CategoryTheory.MonoidalCategory.DayConvolutionUnit.rightUnitor U F).inv.app x)
      h =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategoryStruct.rightUnitor (F.obj x)).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj x)
          CategoryTheory.MonoidalCategory.DayConvolutionUnit.can)
        (CategoryTheory.CategoryStruct.comp
          ((CategoryTheory.MonoidalCategory.DayConvolution.unit F U).app
            (x, CategoryTheory.MonoidalCategoryStruct.tensorUnit C))
          (CategoryTheory.CategoryStruct.comp
            ((CategoryTheory.MonoidalCategory.DayConvolution.convolution F U).map
              (CategoryTheory.MonoidalCategoryStruct.rightUnitor x).hom)
            h)))
-- Mathlib.Algebra.Module.Torsion.Free
Module.isTorsionFree_int_iff_isAddTorsionFree : ∀ {M : Type u_3} [inst : AddCommGroup M], Module.IsTorsionFree ℤ M ↔ IsAddTorsionFree M
-- Lean.Compiler.IR.Format
Lean.IR.instToStringIRType : ToString Lean.IR.IRType
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicFrontier_union_intrinsicInterior : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] (s : Set P),
  intrinsicFrontier 𝕜 s ∪ intrinsicInterior 𝕜 s = intrinsicClosure 𝕜 s
-- Mathlib.RepresentationTheory.Rep.Res
/-- The map induced by a monoid homomorphism `f : H →* G` on morphisms between
`G`-representations.  -/
Rep.resMap : {k : Type u} →
  [inst : Semiring k] →
    {G : Type v1} →
      {H : Type v2} →
        [inst_1 : Monoid G] →
          [inst_2 : Monoid H] →
            {X Y : Rep.{u_1, u, v1} k G} →
              (f : H →* G) → (X ⟶ Y) → (Rep.of (MonoidHom.comp X.ρ f) ⟶ Rep.of (MonoidHom.comp Y.ρ f))
-- Lean.Server.FileWorker.InlayHints
Lean.Server.FileWorker.InlayHintState.oldInlayHints : Lean.Server.FileWorker.InlayHintState → Array Lean.Elab.InlayHintInfo
-- Mathlib.Data.Int.Cast.Lemmas
zpowersHom_apply : ∀ (α : Type u_3) [inst : Group α] (x : α) (n : Multiplicative ℤ), ((zpowersHom α) x) n = x ^ Multiplicative.toAdd n
-- Mathlib.Data.NNRat.Defs
NNRat.num_ne_zero : ∀ {q : ℚ≥0}, q.num ≠ 0 ↔ q ≠ 0
-- Mathlib.Algebra.Star.StarAlgHom
StarAlgEquiv.toRingEquiv_eq_coe : ∀ {R : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Add A] [inst_1 : Add B] [inst_2 : Mul A] [inst_3 : Mul B]
  [inst_4 : SMul R A] [inst_5 : SMul R B] [inst_6 : Star A] [inst_7 : Star B] (e : A ≃⋆ₐ[R] B),
  e.toRingEquiv = (↑e).toRingEquiv
-- Mathlib.MeasureTheory.VectorMeasure.Decomposition.Lebesgue
MeasureTheory.SignedMeasure.singularPart_smul : ∀ {α : Type u_1} {m : MeasurableSpace α} (s : MeasureTheory.SignedMeasure α) (μ : MeasureTheory.Measure α) (r : ℝ),
  (r • s).singularPart μ = r • s.singularPart μ
-- Mathlib.Algebra.Ring.Subring.MulOpposite
/-- Bijection between a subring `S` and `MulOpposite` of its opposite.  -/
Subring.ringEquivOpMop : {R : Type u_2} → [inst : NonAssocRing R] → (S : Subring R) → ↥S ≃+* (↥S.op)ᵐᵒᵖ
-- Mathlib.Algebra.Homology.DerivedCategory.SingleTriangle
CategoryTheory.ShortComplex.ShortExact.singleTriangle.map_hom₃ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Abelian C]
  [inst_2 : HasDerivedCategory C] {S₁ S₂ : CategoryTheory.ShortComplex C} (h₁ : S₁.ShortExact) (h₂ : S₂.ShortExact)
  (f : S₁ ⟶ S₂),
  (CategoryTheory.ShortComplex.ShortExact.singleTriangle.map h₁ h₂ f).hom₃ =
    (DerivedCategory.singleFunctor C 0).map f.τ₃
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.SplitInfo.getGeneration : Lean.Meta.Grind.SplitInfo → Lean.Meta.Grind.GoalM ℕ
-- Mathlib.Logic.Equiv.Fin.Basic
finSuccEquiv_symm_none : ∀ {n : ℕ}, (finSuccEquiv n).symm none = 0
-- Mathlib.Algebra.Homology.ComplexShape
ComplexShape.instDecidableRelRelUp.eq_1 : ∀ (α : Type u_1) [inst : AddRightCancelSemigroup α] [inst_1 : DecidableEq α] [inst_2 : One α],
  ComplexShape.instDecidableRelRelUp α = id inferInstance
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.sub_modEq_iff_modEq_add : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b c : G}, a - b ≡ c [PMOD p] ↔ a ≡ c + b [PMOD p]
-- Mathlib.Algebra.Group.Conj
ConjClasses.forall_isConj : ∀ {α : Type u} [inst : Monoid α] {p : ConjClasses α → Prop},
  (∀ (a : ConjClasses α), p a) ↔ ∀ (a : α), p (ConjClasses.mk a)
-- Mathlib.Topology.FiberBundle.Trivialization
/-- Given two bundle trivializations `e`, `e'` of `proj : Z → B` and a set `s : Set B` such that
the base sets of `e` and `e'` intersect `frontier s` on the same set and `e p = e' p` whenever
`proj p ∈ e.baseSet ∩ frontier s`, `e.piecewise e' s Hs Heq` is the bundle trivialization over
`Set.ite s e.baseSet e'.baseSet` that is equal to `e` on `proj ⁻¹ s` and is equal to `e'`
otherwise.  -/
Bundle.Trivialization.piecewise : {B : Type u_1} →
  {F : Type u_2} →
    {Z : Type u_4} →
      [inst : TopologicalSpace B] →
        [inst_1 : TopologicalSpace F] →
          {proj : Z → B} →
            [inst_2 : TopologicalSpace Z] →
              (e e' : Bundle.Trivialization F proj) →
                (s : Set B) →
                  e.baseSet ∩ frontier s = e'.baseSet ∩ frontier s →
                    Set.EqOn (↑e) (↑e') (proj ⁻¹' (e.baseSet ∩ frontier s)) → Bundle.Trivialization F proj
-- Mathlib.Analysis.CStarAlgebra.Exponential
/-- The map from the selfadjoint real subspace to the unitary group. This map only makes sense
over ℂ.  -/
selfAdjoint.expUnitary : {A : Type u_1} →
  [inst : NormedRing A] →
    [inst_1 : NormedAlgebra ℂ A] →
      [inst_2 : StarRing A] →
        [ContinuousStar A] → [CompleteSpace A] → [StarModule ℂ A] → ↥(selfAdjoint A) → ↥(unitary A)
-- Mathlib.Order.SuccPred.Basic
Order.pred_iterate_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : PredOrder α] (k : ℕ) (x : α), Order.pred^[k] x ≤ x
-- Mathlib.CategoryTheory.Filtered.Basic
CategoryTheory.IsFiltered.of_isTerminal : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] {X : C} (h : CategoryTheory.Limits.IsTerminal X),
  CategoryTheory.IsFiltered C
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.«mcasesPat-» : Lean.ParserDescr
-- Mathlib.RepresentationTheory.Homological.GroupHomology.Functoriality
Finsupp.lsingle.eq_1 : ∀ {α : Type u_1} {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (a : α), Finsupp.lsingle a = { toFun := (↑(Finsupp.singleAddHom a)).toFun, map_add' := ⋯, map_smul' := ⋯ }
-- Mathlib.Algebra.Lie.Submodule
LieSubmodule.instAdd : {R : Type u} →
  {L : Type v} →
    {M : Type w} →
      [inst : CommRing R] →
        [inst_1 : LieRing L] →
          [inst_2 : AddCommGroup M] → [inst_3 : Module R M] → [inst_4 : LieRingModule L M] → Add (LieSubmodule R L M)
-- Mathlib.Analysis.LocallyConvex.WeakOperatorTopology
ContinuousLinearMapWOT.toCLM_apply : ∀ {𝕜₁ : Type u_1} {𝕜₂ : Type u_2} [inst : NormedField 𝕜₁] [inst_1 : NormedField 𝕜₂] {σ : 𝕜₁ →+* 𝕜₂} {E : Type u_3}
  {F : Type u_4} [inst_2 : AddCommGroup E] [inst_3 : TopologicalSpace E] [inst_4 : Module 𝕜₁ E]
  [inst_5 : AddCommGroup F] [inst_6 : TopologicalSpace F] [inst_7 : Module 𝕜₂ F] {A : E →SWOT[σ] F} {x : E},
  A.toCLM x = A x
-- Mathlib.Algebra.Category.ModuleCat.Sheaf
CategoryTheory.ObjectProperty.isLocal.homEquiv.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {P P_1 : CategoryTheory.ObjectProperty C} (e_P : P = P_1)
  {X Y : C} {f f_1 : X ⟶ Y} (e_f : f = f_1) (hf : P.isLocal f) (Z : C) (hZ : P Z), hf.homEquiv Z hZ = ⋯.homEquiv Z ⋯
-- Mathlib.Order.Directed
/-- **Alias** of the reverse direction of `directedOn_iff_isDirectedOrder`. -/
DirectedOn.of_isDirectedOrder : ∀ {α : Type u_1} [inst : LE α] {s : Set α}, IsDirectedOrder ↑s → DirectedOn (fun x1 x2 => x1 ≤ x2) s
-- Mathlib.Algebra.Order.Rearrangement
/-- **Equality case of the Rearrangement Inequality**: Pointwise scalar multiplication of `f` and
`g`, which monovary together, is unchanged by a permutation if and only if `f` and `g ∘ σ` monovary
together. Stated by permuting the entries of `g`.  -/
Monovary.sum_smul_comp_perm_eq_sum_smul_iff : ∀ {ι : Type u_1} {α : Type u_2} {β : Type u_3} [inst : Semiring α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α]
  [ExistsAddOfLE α] [inst_4 : AddCommMonoid β] [inst_5 : LinearOrder β] [IsOrderedCancelAddMonoid β]
  [inst_7 : Module α β] [PosSMulStrictMono α β] {σ : Equiv.Perm ι} {f : ι → α} {g : ι → β} [inst_9 : Fintype ι],
  Monovary f g → (∑ i, f i • g (σ i) = ∑ i, f i • g i ↔ Monovary f (g ∘ ⇑σ))
-- Mathlib.CategoryTheory.Monoidal.Internal.FunctorCategory
CategoryTheory.Monoidal.MonFunctorCategoryEquivalence.functorObjObj_mon_one : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_2 : CategoryTheory.MonoidalCategory D] (A : CategoryTheory.Functor C D) [inst_3 : CategoryTheory.MonObj A]
  (X : C), CategoryTheory.MonObj.one = CategoryTheory.MonObj.one.app X
-- Mathlib.Data.DFinsupp.WellFounded
DFinsupp.Colex.wellFoundedLT_of_finite : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : LinearOrder ι] [Finite ι] [inst_2 : (i : ι) → Zero (α i)]
  [inst_3 : (i : ι) → LT (α i)] [hwf : ∀ (i : ι), WellFoundedLT (α i)], WellFoundedLT (Colex (Π₀ (i : ι), α i))
-- Mathlib.Algebra.MonoidAlgebra.Module
AddMonoidAlgebra.supported_eq_span_single : ∀ (R : Type u_1) {M : Type u_3} [inst : Semiring R] (s : Set M),
  AddMonoidAlgebra.supported R R s = Submodule.span R ((fun m => AddMonoidAlgebra.single m 1) '' s)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.get_max? : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [inst : Std.TransCmp cmp] {km : α}
  {hc : t.contains km = true}, t.max?.get ⋯ = km → t.get km hc = km
-- Mathlib.Analysis.Convex.SimplicialComplex.Basic
Geometry.SimplicialComplex.convexHull_inter_convexHull : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommGroup E]
  [inst_3 : Module 𝕜 E] {K : Geometry.SimplicialComplex 𝕜 E} {s t : Finset E},
  s ∈ K.faces → t ∈ K.faces → (convexHull 𝕜) ↑s ∩ (convexHull 𝕜) ↑t = (convexHull 𝕜) (↑s ∩ ↑t)
-- Mathlib.Algebra.Group.End
Equiv.Perm.instMul : {α : Type u_4} → Mul (Equiv.Perm α)
-- Mathlib.Analysis.Complex.UnitDisc.Basic
Complex.UnitClosedDisc.instInhabited : Inhabited Complex.UnitClosedDisc
-- Mathlib.GroupTheory.MonoidLocalization.Basic
/-- A predicate characterizing homomorphisms between monoids `M` and `N` that form a
commutative triangle with the canonical map from `M` to its localization at `S` and
some isomorphism between `N` and the localization.  -/
Submonoid.IsLocalizationMap : {M : Type u_1} → [inst : CommMonoid M] → {N : Type u_2} → [CommMonoid N] → Submonoid M → (M → N) → Prop
-- Mathlib.LinearAlgebra.TensorProduct.Map
LinearMap.rTensor_def : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Type u_7) {N : Type u_8} {P : Type u_9} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : AddCommMonoid P] [inst_4 : Module R M] [inst_5 : Module R N]
  [inst_6 : Module R P] (f : N →ₗ[R] P), LinearMap.rTensor M f = TensorProduct.map f LinearMap.id
-- Mathlib.Order.Bounds.Image
IsLeast.isLeast_image2_of_isGreatest : ∀ {α : Type u} {β : Type v} {γ : Type w} [inst : Preorder α] [inst_1 : Preorder β] [inst_2 : Preorder γ] {f : α → β → γ}
  {s : Set α} {t : Set β} {a : α} {b : β},
  (∀ (b : β), Monotone (Function.swap f b)) →
    (∀ (a : α), Antitone (f a)) → IsLeast s a → IsGreatest t b → IsLeast (Set.image2 f s t) (f a b)
-- Mathlib.RingTheory.FractionalIdeal.Operations
/-- If `g` is an equivalence, `map g` is an isomorphism  -/
FractionalIdeal.mapEquiv : {R : Type u_1} →
  [inst : CommRing R] →
    {S : Submonoid R} →
      {P : Type u_2} →
        [inst_1 : CommRing P] →
          [inst_2 : Algebra R P] →
            {P' : Type u_3} →
              [inst_3 : CommRing P'] →
                [inst_4 : Algebra R P'] → (P ≃ₐ[R] P') → FractionalIdeal S P ≃+* FractionalIdeal S P'
-- Init.Data.String.Slice
/-- Checks whether `s1` and `s2` represent the same string, even if they are slices of
different base strings or different slices within the same string.

The implementation is an efficient equivalent of `s1.copy == s2.copy`
 -/
String.Slice.beq : String.Slice → String.Slice → Bool
-- Mathlib.Topology.Category.Sequential
Sequential.isoOfHomeo_inv : ∀ {X Y : Sequential} (f : ↑X.toTop ≃ₜ ↑Y.toTop),
  (Sequential.isoOfHomeo f).inv =
    CategoryTheory.InducedCategory.homMk (TopCat.ofHom { toFun := ⇑f.symm, continuous_toFun := ⋯ })
-- Mathlib.Order.Interval.Set.Basic
Set.Iic_ssubset_Iic : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Iic a ⊂ Set.Iic b ↔ a < b
-- Mathlib.CategoryTheory.Monad.Comonadicity
/-- `f, g` is a coreflexive pair, then `F` preserves limits of `parallelPair f g`.  -/
CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair.out : ∀ {C : Type u₁} {D : Type u₂} {inst : CategoryTheory.Category.{v₁, u₁} C} {inst_1 : CategoryTheory.Category.{v₁, u₂} D}
  {F : CategoryTheory.Functor C D} [self : CategoryTheory.Comonad.PreservesLimitOfIsCoreflexivePair F] ⦃A B : C⦄
  (f g : A ⟶ B) [CategoryTheory.IsCoreflexivePair f g],
  CategoryTheory.Limits.PreservesLimit (CategoryTheory.Limits.parallelPair f g) F
-- Mathlib.NumberTheory.NumberField.InfinitePlace.Embeddings
NumberField.ComplexEmbedding.LiesOver.over_apply : ∀ {K : Type u_3} {L : Type u_4} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (φ : L →+* ℂ) (ψ : K →+* ℂ)
  [NumberField.ComplexEmbedding.LiesOver φ ψ] {x : K}, φ ((algebraMap K L) x) = ψ x
-- Init.Notation
/-- Divisibility. `a ∣ b` (typed as `\|`) means that there is some `c` such that `b = a * c`. 

Conventions for notations in identifiers:

 * The recommended spelling of `∣` in identifiers is `dvd`. -/
«term_∣_» : Lean.TrailingParserDescr
-- Mathlib.AlgebraicTopology.ExtraDegeneracy
SSet.Augmented.StandardSimplex.shift.eq_1 : ∀ {n : ℕ} {Δ : SimplexCategory} (f : { len := n } ⟶ Δ),
  SSet.Augmented.StandardSimplex.shift f =
    SimplexCategory.Hom.mk
      { toFun := SSet.Augmented.StandardSimplex.shiftFun ⇑(SimplexCategory.Hom.toOrderHom f), monotone' := ⋯ }
-- Mathlib.Combinatorics.SimpleGraph.Paths
SimpleGraph.Walk.IsSubwalk.hcongr_8 : ∀ (V V' : Type u_1),
  V = V' →
    ∀ (G : SimpleGraph V) (G' : SimpleGraph V'),
      G ≍ G' →
        ∀ (u₁ : V) (u₁' : V'),
          u₁ ≍ u₁' →
            ∀ (v₁ : V) (v₁' : V'),
              v₁ ≍ v₁' →
                ∀ (u₂ : V) (u₂' : V'),
                  u₂ ≍ u₂' →
                    ∀ (v₂ : V) (v₂' : V'),
                      v₂ ≍ v₂' →
                        ∀ (p : G.Walk u₁ v₁) (p' : G'.Walk u₁' v₁'),
                          p ≍ p' → ∀ (q : G.Walk u₂ v₂) (q' : G'.Walk u₂' v₂'), q ≍ q' → p.IsSubwalk q ≍ p'.IsSubwalk q'
-- Init.Grind.AC
Lean.Grind.AC.hugeFuel : ℕ
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.Basic
ContinuousLinearMap.isHomeomorph_of_isUnit : ∀ {R₁ : Type u_1} [inst : Semiring R₁] {M₁ : Type u_4} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R₁ M₁] {T : M₁ →L[R₁] M₁}, IsUnit T → IsHomeomorph ⇑T
-- Mathlib.Data.Set.Basic
Set.union_inter_distrib_left : ∀ {α : Type u} (s t u : Set α), s ∪ t ∩ u = (s ∪ t) ∩ (s ∪ u)
-- Lean.PrettyPrinter.Delaborator.SubExpr
Lean.PrettyPrinter.Delaborator.SubExpr.getExpr : {m : Type → Type} → [Monad m] → [MonadReaderOf Lean.SubExpr m] → m Lean.Expr
-- Mathlib.Data.List.Perm.Basic
List.rel_perm_imp : ∀ {α : Type u_1} {β : Type u_2} {r : α → β → Prop},
  Relator.RightUnique r →
    Relator.LiftFun (List.Forall₂ r) (Relator.LiftFun (List.Forall₂ r) fun x1 x2 => x1 → x2) List.Perm List.Perm
-- Mathlib.Geometry.Manifold.IntegralCurve.Basic
/-- If `v` is a vector field on `M` and `t₀ : ℝ`, `IsMIntegralCurveAt γ v t₀` means `γ : ℝ → M` is a
local integral curve of `v` in a neighbourhood containing `t₀`. The value of `γ` outside of this
interval is irrelevant and considered junk.  -/
IsMIntegralCurveAt : {E : Type u_1} →
  [inst : NormedAddCommGroup E] →
    [inst_1 : NormedSpace ℝ E] →
      {H : Type u_2} →
        [inst_2 : TopologicalSpace H] →
          {I : ModelWithCorners ℝ E H} →
            {M : Type u_3} →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : ChartedSpace H M] → (ℝ → M) → ((x : M) → TangentSpace I x) → ℝ → Prop
-- Mathlib.Algebra.Module.Submodule.LinearMap
LinearMap.domRestrict_comp_codRestrict : ∀ {R : Type u_1} {R₂ : Type u_3} {R₃ : Type u_4} {M : Type u_5} {M₂ : Type u_7} {M₃ : Type u_8} [inst : Semiring R]
  [inst_1 : Semiring R₂] [inst_2 : Semiring R₃] [inst_3 : AddCommMonoid M] [inst_4 : AddCommMonoid M₂]
  [inst_5 : AddCommMonoid M₃] [inst_6 : Module R M] [inst_7 : Module R₂ M₂] [inst_8 : Module R₃ M₃] {σ₁₂ : R →+* R₂}
  {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [inst_9 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] (g : M₂ →ₛₗ[σ₂₃] M₃) (f : M →ₛₗ[σ₁₂] M₂)
  (p : Submodule R₂ M₂) (h : ∀ (c : M), f c ∈ p), g.domRestrict p ∘ₛₗ LinearMap.codRestrict p f h = g ∘ₛₗ f
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey_eq_getKey! : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Inhabited α],
  t.WF → ∀ {a : α} {h : Std.DTreeMap.Internal.Impl.contains a t = true}, t.getKey a h = t.getKey! a
-- Mathlib.Condensed.Light.Explicit
/-- A light condensed object satisfies the equalizer condition.  -/
LightCondensed.equalizerCondition : ∀ {A : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} A] (X : LightCondensed A),
  CategoryTheory.regularTopology.EqualizerCondition X.obj
-- Mathlib.Order.Filter.Pointwise
Filter.vsub_bot : ∀ {α : Type u_2} {β : Type u_3} [inst : VSub α β] {f : Filter β}, f -ᵥ ⊥ = ⊥
-- Mathlib.Geometry.Convex.ConvexSpace.Defs
Convexity.StdSimplex.restrict_singleton : ∀ {X : Type u_2} {K : Type u_8} [inst : Semifield K] [inst_1 : LinearOrder K] [inst_2 : IsStrictOrderedRing K]
  [IsDomain K] (w : Convexity.StdSimplex K X) (x : X) (hx : ∃ x_1 ∈ {x}, w.weights x_1 ≠ 0),
  w.restrict {x} hx = Convexity.StdSimplex.single x
-- Mathlib.Analysis.Normed.Unbundled.SeminormFromBounded
/-- If `f : R → ℝ` is a nonnegative, multiplicatively bounded, subadditive function that preserves
zero and negation, then `seminormFromBounded' f` is a norm if and only if `f⁻¹' {0} = {0}`.  -/
seminormFromBounded_is_norm_iff : ∀ {R : Type u_1} [inst : CommRing R] {f : R → ℝ} {c : ℝ} (f_zero : f 0 = 0) (f_nonneg : 0 ≤ f)
  (f_mul : ∀ (x y : R), f (x * y) ≤ c * f x * f y) (f_add : ∀ (a b : R), f (a + b) ≤ f a + f b)
  (f_neg : ∀ (x : R), f (-x) = f x),
  (∀ (x : R), (seminormFromBounded f_zero f_nonneg f_mul f_add f_neg).toFun x = 0 → x = 0) ↔ f ⁻¹' {0} = {0}
-- Mathlib.CategoryTheory.ConnectedComponents
CategoryTheory.instIsEquivalenceDecomposedDecomposedTo : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J], (CategoryTheory.decomposedTo J).IsEquivalence
-- Mathlib.RingTheory.IntegralClosure.Algebra.Basic
instSMulDistribClassSubtypeMemSubalgebraIntegralClosure : ∀ {G : Type u_1} {R : Type u_2} {K : Type u_3} [inst : CommRing R] [inst_1 : CommRing K] [inst_2 : Algebra R K]
  [inst_3 : Group G] [inst_4 : MulSemiringAction G K] [inst_5 : SMulCommClass G R K],
  SMulDistribClass G (↥(integralClosure R K)) K
-- Lean.DocString.Parser
_private.Lean.DocString.Parser.0.Lean.Doc.Parser.block_command.eatSpaces : Lean.Parser.ParserFn
-- Mathlib.Algebra.Ring.Subsemiring.Basic
/-- The elements of the subsemiring closure of `M` are exactly the elements of the additive closure
of a multiplicative submonoid `M`.  -/
Subsemiring.coe_closure_eq : ∀ {R : Type u} [inst : NonAssocSemiring R] (s : Set R),
  ↑(Subsemiring.closure s) = ↑(AddSubmonoid.closure ↑(Submonoid.closure s))
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKey?_maxKeyD : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  t.WF → t.isEmpty = false → ∀ {fallback : α}, t.getKey? (t.maxKeyD fallback) = some (t.maxKeyD fallback)
-- Mathlib.Analysis.InnerProductSpace.SingularValues
LinearMap.singularValues_pos_iff_lt_finrank_range : ∀ {𝕜 : Type u_1} [inst : RCLike 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  [inst_3 : FiniteDimensional 𝕜 E] {F : Type u_3} [inst_4 : NormedAddCommGroup F] [inst_5 : InnerProductSpace 𝕜 F]
  [inst_6 : FiniteDimensional 𝕜 F] (T : E →ₗ[𝕜] F) {n : ℕ}, 0 < T.singularValues n ↔ n < Module.finrank 𝕜 ↥T.range
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.isLeftRegular_iff_nonsingular : ∀ {R : Type u_1} {n : Type u_3} [inst : CommSemiring R] [inst_1 : Fintype n] [inst_2 : DecidableEq n] {A : Matrix n n R}
  [IsCancelAdd R], IsLeftRegular A ↔ A.Nonsingular
-- Mathlib.AlgebraicTopology.SimplexCategory.Basic
SimplexCategory.coe_σ : ∀ {n : ℕ} (i : Fin (n + 1)), ⇑(CategoryTheory.ConcreteCategory.hom (SimplexCategory.σ i)) = i.predAbove
-- Mathlib.Combinatorics.SimpleGraph.Walk.Decomp
SimpleGraph.Walk.takeUntil_nil : ∀ {V : Type u} {G : SimpleGraph V} [inst : DecidableEq V] {u : V} {h : u ∈ SimpleGraph.Walk.nil.support},
  SimpleGraph.Walk.nil.takeUntil u h = SimpleGraph.Walk.nil
-- Mathlib.CategoryTheory.Sites.Coherent.RegularSheaves
CategoryTheory.regularTopology.mapToEqualizer.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (P : CategoryTheory.Functor Cᵒᵖ (Type u_4)) {W X B : C}
  (f f_1 : X ⟶ B) (e_f : f = f_1) (g₁ g₂ : W ⟶ X)
  (w : CategoryTheory.CategoryStruct.comp g₁ f = CategoryTheory.CategoryStruct.comp g₂ f),
  CategoryTheory.regularTopology.mapToEqualizer P f g₁ g₂ w =
    CategoryTheory.regularTopology.mapToEqualizer P f_1 g₁ g₂ ⋯
-- Mathlib.Topology.Algebra.ContinuousAffineMap
ContinuousAffineMap.sub_contLinear : ∀ {R : Type u_1} {V : Type u_2} {W : Type u_3} {P : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup V]
  [inst_2 : Module R V] [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] [inst_5 : AddCommGroup W]
  [inst_6 : Module R W] [inst_7 : TopologicalSpace W] [inst_8 : IsTopologicalAddGroup W] [inst_9 : TopologicalSpace V]
  [inst_10 : IsTopologicalAddTorsor P] (f g : P →ᴬ[R] W), (f - g).contLinear = f.contLinear - g.contLinear
-- Mathlib.Topology.Order.WithTop
WithBot.neBotHomeomorph.eq_1 : ∀ (ι : Type u_1) [inst : LinearOrder ι] [inst_1 : TopologicalSpace ι] [inst_2 : OrderTopology ι],
  WithBot.neBotHomeomorph ι = { toEquiv := Equiv.withBotSubtypeNe, continuous_toFun := ⋯, continuous_invFun := ⋯ }
-- Mathlib.Topology.Connected.LocallyConnected
/-- A locally connected compact space has finitely many connected components.  -/
instFiniteConnectedComponentsOfLocallyConnectedSpaceOfCompactSpace : ∀ {α : Type u} [inst : TopologicalSpace α] [LocallyConnectedSpace α] [CompactSpace α], Finite (ConnectedComponents α)
-- Mathlib.Order.RelSeries
RelSeries.last_take : ∀ {α : Type u_1} {r : SetRel α α} (p : RelSeries r) (i : Fin (p.length + 1)), (p.take i).last = p.toFun i
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Cospan
/-- The right point of the walking span.  -/
CategoryTheory.Limits.WalkingSpan.right : CategoryTheory.Limits.WalkingSpan
-- Mathlib.Analysis.Complex.Basic
Complex.natCast_mem_slitPlane : ∀ {n : ℕ}, ↑n ∈ Complex.slitPlane ↔ n ≠ 0
-- Mathlib.Combinatorics.Matroid.Rank.Finite
Matroid.IsRkFinite.insert : ∀ {α : Type u_1} {M : Matroid α} {X : Set α}, M.IsRkFinite X → ∀ (e : α), M.IsRkFinite (insert e X)