mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Functor.KanExtension.Basic
CategoryTheory.Functor.instIsLeftKanExtensionLeftKanExtensionLeftKanExtensionUnit : ∀ {C : Type u_1} {H : Type u_3} {D : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_3, u_3} H] [inst_2 : CategoryTheory.Category.{v_4, u_4} D]
  (L : CategoryTheory.Functor C D) (F : CategoryTheory.Functor C H) [inst_3 : L.HasLeftKanExtension F],
  (L.leftKanExtension F).IsLeftKanExtension (L.leftKanExtensionUnit F)
-- Mathlib.Topology.Algebra.ClopenNhdofOne
IsTopologicalGroup.exist_openNormalSubgroup_sub_clopen_nhds_of_one : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] [IsTopologicalGroup G] [CompactSpace G] {W : Set G},
  IsClopen W → 1 ∈ W → ∃ H, ↑H ⊆ W
-- Init.PropLemmas
ite_then_self : ∀ {p q : Prop} [h : Decidable p], (if p then p else q) ↔ ¬p → q
-- Lean.Parser.Basic
/-- `unicodeSymbol sym asciiSym` parses either `sym` or `asciiSym` as a reserved symbol.
The `asciiSym` argument should be an ASCII alternative for `sym`.

- If the `pp.unicode` option is false, then pretty prints using `asciiSym`.
- If the `pp.unicode` option is true, then pretty prints as `sym`,
  unless the `preserveForPP` argument is true, in which case the underlying atom
  is used to decide whether to print using the unicode or ASCII form.
  We take the ASCII form to be the preferred form in this case.
  For example, `pp.unicode.fun` causes the delaborator to use `↦` instead of `=>` for the `fun` arrow.
 -/
Lean.Parser.unicodeSymbol : String → String → optParam Bool false → Lean.Parser.Parser
-- Mathlib.Algebra.Category.Grp.Limits
/-- If `(F ⋙ forget GrpCat).sections` is `u`-small, `F` has a limit.  -/
GrpCat.hasLimit : ∀ {J : Type v} [inst : CategoryTheory.Category.{w, v} J] (F : CategoryTheory.Functor J GrpCat)
  [Small.{u, max u v} ↑(F.comp (CategoryTheory.forget GrpCat)).sections], CategoryTheory.Limits.HasLimit F
-- Mathlib.LinearAlgebra.Finsupp.LSum
Finsupp.domLCongr_trans : ∀ {M : Type u_2} {R : Type u_5} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {α₁ : Type u_9}
  {α₂ : Type u_10} {α₃ : Type u_11} (f : α₁ ≃ α₂) (f₂ : α₂ ≃ α₃),
  Finsupp.domLCongr f ≪≫ₗ Finsupp.domLCongr f₂ = Finsupp.domLCongr (f.trans f₂)
-- Mathlib.RingTheory.Spectrum.Prime.RingHom
/-- Let `f : R →+* S` be a surjective ring homomorphism, then `Spec S` is order-isomorphic to `Z(I)`
where `I = ker f`.  -/
Ideal.primeSpectrumOrderIsoZeroLocusOfSurj : {R : Type u} →
  {S : Type v} →
    [inst : CommRing R] →
      [inst_1 : CommRing S] →
        (f : R →+* S) →
          Function.Surjective ⇑f → {I : Ideal R} → RingHom.ker f = I → PrimeSpectrum S ≃o ↑(PrimeSpectrum.zeroLocus ↑I)
-- Init.Data.Iterators.Lemmas.Combinators.Monadic.FilterMap
Std.IterM.toListRev_mapM_eq_toListRev_filterMapM : ∀ {α β γ : Type w} {m : Type w → Type w'} {n : Type w → Type w''} [inst : Monad m] [LawfulMonad m] [inst_2 : Monad n]
  [inst_3 : MonadAttach n] [LawfulMonad n] [WeaklyLawfulMonadAttach n] [inst_6 : MonadLiftT m n] [LawfulMonadLiftT m n]
  [inst : Std.Iterator α m β] [Std.Iterators.Finite α m] {f : β → n γ} {it : Std.IterM m β},
  (Std.IterM.mapM f it).toListRev = (Std.IterM.filterMapM (fun b => some <$> f b) it).toListRev
-- Mathlib.Algebra.Jordan.Basic
_private.Mathlib.Algebra.Jordan.Basic.0.aux0 : ∀ {A : Type u_1} [inst : NonUnitalNonAssocCommRing A] {a b c : A},
  ⁅AddMonoid.End.mulLeft (a + b + c), AddMonoid.End.mulLeft ((a + b + c) * (a + b + c))⁆ =
    ⁅AddMonoid.End.mulLeft a + AddMonoid.End.mulLeft b + AddMonoid.End.mulLeft c,
      AddMonoid.End.mulLeft (a * a) + AddMonoid.End.mulLeft (b * b) + AddMonoid.End.mulLeft (c * c) +
            2 • AddMonoid.End.mulLeft (a * b) +
          2 • AddMonoid.End.mulLeft (c * a) +
        2 • AddMonoid.End.mulLeft (b * c)⁆
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- The natural transformation `t.truncLT n ⟶ 𝟭 C` when `t` is a t-structure
on a category `C` and `n : ℤ`.  -/
CategoryTheory.Triangulated.TStructure.truncLTι : {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 : ℤ) → t.truncLT n ⟶ CategoryTheory.Functor.id C
-- Std.Time.Date.ValidDate
Std.Time.instOrientedOrdValidDate : ∀ {leap : Bool}, Std.OrientedOrd (Std.Time.ValidDate leap)
-- Std.Tactic.Do.Syntax
Lean.Parser.Tactic.MRefinePat.one.sizeOf_spec : ∀ (name : Lean.TSyntax `Lean.binderIdent), sizeOf (Lean.Parser.Tactic.MRefinePat.one name) = 1 + sizeOf name
-- Init.Data.List.Attach
List.filter_wfParam : ∀ {α : Type u_1} {xs : List α} {f : α → Bool}, List.filter f (wfParam xs) = List.filter f xs.attach.unattach
-- Mathlib.Algebra.Homology.DerivedCategory.ShortExact
/-- The morphism `triangleOfSES h₁ ⟶ triangleOfSES h₂` that is induced by a morphism of short
exact sequences of cochain complexes.
 -/
DerivedCategory.triangleOfSES.map : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] →
        {S₁ S₂ : CategoryTheory.ShortComplex (CochainComplex C ℤ)} →
          (h₁ : S₁.ShortExact) →
            (h₂ : S₂.ShortExact) → (S₁ ⟶ S₂) → (DerivedCategory.triangleOfSES h₁ ⟶ DerivedCategory.triangleOfSES h₂)
-- Init.Data.List.TakeDrop
_private.Init.Data.List.TakeDrop.0.List.filterMap.match_1.eq_1 : ∀ {β : Type u_1} (motive : Option β → Sort u_2) (h_1 : Unit → motive none) (h_2 : (b : β) → motive (some b)),
  (match none with
    | none => h_1 ()
    | some b => h_2 b) =
    h_1 ()
-- Mathlib.Algebra.WithConv
WithConv.linearEquiv_apply : ∀ {R : Type u_1} {A : Type u_2} [inst : AddCommMonoid A] [inst_1 : Semiring R] [inst_2 : Module R A] (a : WithConv A),
  (WithConv.linearEquiv R A) a = a.ofConv
-- Mathlib.Combinatorics.SimpleGraph.Connectivity.Finite
SimpleGraph.instFintypeConnectedComponent : {V : Type u} → (G : SimpleGraph V) → [DecidableEq V] → [Fintype V] → [DecidableRel G.Adj] → Fintype G.ConnectedComponent
-- Mathlib.CategoryTheory.ComposableArrows.Basic
CategoryTheory.ComposableArrows.hom_ext₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {f g : CategoryTheory.ComposableArrows C 3}
  {φ φ' : f ⟶ g},
  CategoryTheory.ComposableArrows.app' φ 0 _proof_297✝ = CategoryTheory.ComposableArrows.app' φ' 0 _proof_297✝ →
    CategoryTheory.ComposableArrows.app' φ 1 _proof_298✝ = CategoryTheory.ComposableArrows.app' φ' 1 _proof_298✝ →
      CategoryTheory.ComposableArrows.app' φ 2 _proof_299✝ = CategoryTheory.ComposableArrows.app' φ' 2 _proof_299✝ →
        CategoryTheory.ComposableArrows.app' φ 3 _proof_300✝ = CategoryTheory.ComposableArrows.app' φ' 3 _proof_300✝ →
          φ = φ'
-- Mathlib.AlgebraicGeometry.EllipticCurve.DivisionPolynomial.Degree
WeierstrassCurve.coeff_preΨ : ∀ {R : Type u} [inst : CommRing R] (W : WeierstrassCurve R) (n : ℤ),
  (W.preΨ n).coeff ((n.natAbs ^ 2 - if Even n then 4 else 1) / 2) = ↑(if Even n then n / 2 else n)
-- Lean.Meta.ArgsPacker
_private.Lean.Meta.ArgsPacker.0.Lean.Meta.ArgsPacker.Unary.curry.go : Lean.Expr → Lean.Expr → Lean.Expr → Array Lean.Expr → List Lean.Name → Lean.MetaM Lean.Expr
-- Mathlib.Computability.Language
Language.instSingletonList : {α : Type u_1} → Singleton (List α) (Language α)
-- Mathlib.Algebra.Module.LinearMap.Defs
/-- The type of linear maps is an additive group.  -/
LinearMap.addCommGroup : {R₁ : Type u_2} →
  {R₂ : Type u_3} →
    {M : Type u_8} →
      {N₂ : Type u_12} →
        [inst : Semiring R₁] →
          [inst_1 : Semiring R₂] →
            [inst_2 : AddCommMonoid M] →
              [inst_3 : AddCommGroup N₂] →
                [inst_4 : Module R₁ M] → [inst_5 : Module R₂ N₂] → {σ₁₂ : R₁ →+* R₂} → AddCommGroup (M →ₛₗ[σ₁₂] N₂)
-- Init.Prelude
/-- The empty list, usually written `[]`. 

Conventions for notations in identifiers:

 * The recommended spelling of `[]` in identifiers is `nil`. -/
List.nil : {α : Type u} → List α
-- Mathlib.RingTheory.Finiteness.Basic
RingHom.Finite.of_surjective : ∀ {A : Type u_1} {B : Type u_2} [inst : CommRing A] [inst_1 : CommRing B] (f : A →+* B),
  Function.Surjective ⇑f → f.Finite
-- Mathlib.Topology.Algebra.Group.Basic
isOpenMap_sub_right : ∀ {G : Type w} [inst : AddGroup G] [inst_1 : TopologicalSpace G] [IsTopologicalAddGroup G] (a : G),
  IsOpenMap fun x => x - a
-- Mathlib.AlgebraicGeometry.AffineSpace
AlgebraicGeometry.AffineSpace.map_over : ∀ {n : Type u} {S T : AlgebraicGeometry.Scheme} (f : S ⟶ T),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace.map n f) (AlgebraicGeometry.AffineSpace n T ↘ T) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.AffineSpace n S ↘ S) f
-- Mathlib.Order.RelSeries
finiteDimensionalOrder_or_infiniteDimensionalOrder : ∀ (α : Type u_1) [inst : Preorder α] [Nonempty α], FiniteDimensionalOrder α ∨ InfiniteDimensionalOrder α
-- Mathlib.MeasureTheory.Integral.SetToL1
MeasureTheory.L1.setToL1_add_left' : ∀ {α : Type u_1} {E : Type u_2} {F : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
  [inst_4 : CompleteSpace F] {T T' T'' : Set α → E →L[ℝ] F} {C C' C'' : ℝ}
  (hT : MeasureTheory.DominatedFinMeasAdditive μ T C) (hT' : MeasureTheory.DominatedFinMeasAdditive μ T' C')
  (hT'' : MeasureTheory.DominatedFinMeasAdditive μ T'' C''),
  (∀ (s : Set α), MeasurableSet s → μ s < ⊤ → T'' s = T s + T' s) →
    ∀ (f : ↥(MeasureTheory.Lp E 1 μ)),
      (MeasureTheory.L1.setToL1 hT'') f = (MeasureTheory.L1.setToL1 hT) f + (MeasureTheory.L1.setToL1 hT') f
-- Mathlib.AlgebraicTopology.CechNerve
/-- The augmented Čech nerve construction is right adjoint to the `toArrow` functor.  -/
CategoryTheory.SimplicialObject.cechNerveAdjunction : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 :
        ∀ (n : ℕ) (f : CategoryTheory.Arrow C),
          CategoryTheory.Limits.HasWidePullback f.right (fun x => f.left) fun x => f.hom] →
      CategoryTheory.SimplicialObject.Augmented.toArrow ⊣ CategoryTheory.SimplicialObject.augmentedCechNerve
-- Init.Data.SInt.Lemmas
Int8.toNatClampNeg_eq_zero_iff : ∀ {n : Int8}, n.toNatClampNeg = 0 ↔ n ≤ 0
-- Mathlib.Computability.TuringMachine.PostTuringMachine
Turing.TM1.Stmt.inhabited : (Γ : Type u_1) → (Λ : Type u_2) → (σ : Type u_3) → Inhabited (Turing.TM1.Stmt Γ Λ σ)
-- Mathlib.Order.FixedPoints
OrderHom.lfp_le : ∀ {α : Type u} [inst : CompleteLattice α] (f : α →o α) {a : α}, f a ≤ a → OrderHom.lfp f ≤ a
-- Mathlib.Data.Matrix.Block
Matrix.blockDiagonal'_submatrix_eq_blockDiagonal : ∀ {m : Type u_2} {n : Type u_3} {o : Type u_4} {α : Type u_12} [inst : DecidableEq o] [inst_1 : Zero α]
  (M : o → Matrix m n α),
  (Matrix.blockDiagonal' M).submatrix (Prod.toSigma ∘ Prod.swap) (Prod.toSigma ∘ Prod.swap) = Matrix.blockDiagonal M
-- Mathlib.CategoryTheory.Bicategory.Functor.Oplax
CategoryTheory.OplaxFunctor.mapId'.eq_1 : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (F : CategoryTheory.OplaxFunctor B C) {b : B} (f : b ⟶ b) (hf : f = CategoryTheory.CategoryStruct.id b),
  F.mapId' f hf = CategoryTheory.CategoryStruct.comp (F.map₂ (CategoryTheory.eqToHom ⋯)) (F.mapId b)
-- Mathlib.Order.Filter.Basic
Filter.exists_mem_and_iff : ∀ {α : Type u} {f : Filter α} {P Q : Set α → Prop},
  Antitone P → Antitone Q → (((∃ u ∈ f, P u) ∧ ∃ u ∈ f, Q u) ↔ ∃ u ∈ f, P u ∧ Q u)
-- Mathlib.RepresentationTheory.Continuous.Basic
/-- Any continuous representation is equivalent to itself.  -/
ContRepresentation.Equiv.refl : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      [inst : Monoid G] →
        [inst_1 : Ring R] →
          [inst_2 : AddCommGroup V] →
            [inst_3 : TopologicalSpace V] →
              [inst_4 : IsTopologicalAddGroup V] → [inst_5 : Module R V] → (ρ : ContRepresentation R G V) → ρ.Equiv ρ
-- Mathlib.Data.Fintype.Prod
/-- Non-dependent version of `Pi.infinite_of_exists_right` and `Pi.infinite_of_right`.  -/
Function.infinite_of_right : ∀ {ι : Sort u_4} {π : Type u_5} [Infinite π] [Nonempty ι], Infinite (ι → π)
-- Mathlib.CategoryTheory.SmallObject.Construction
CategoryTheory.SmallObject.ιFunctorObj_πFunctorObj_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {I : Type w} {A B : I → C} (f : (i : I) → A i ⟶ B i) {S X : C}
  (πX : X ⟶ S)
  [inst_1 :
    CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete (CategoryTheory.SmallObject.FunctorObjIndex f πX))
      C]
  [inst_2 :
    CategoryTheory.Limits.HasPushout (CategoryTheory.SmallObject.functorObjTop f πX)
      (CategoryTheory.SmallObject.functorObjLeft f πX)]
  {Z : C} (h : S ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.ιFunctorObj f πX)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.πFunctorObj f πX) h) =
    CategoryTheory.CategoryStruct.comp πX h
-- Init.Data.Option.Lemmas
Option.max_eq_left : ∀ {α : Type u_1} [inst : LE α] [inst_1 : Max α],
  (∀ (x y : α), x ≤ y → x ⊔ y = y) → ∀ {a b : Option α}, a ≤ b → a ⊔ b = b
-- Mathlib.Geometry.Euclidean.Angle.Oriented.Basic
/-- If the sign of the angle between two vectors is negative, the second vector is nonzero.  -/
Orientation.right_ne_zero_of_oangle_sign_eq_neg_one : ∀ {V : Type u_1} [inst : NormedAddCommGroup V] [inst_1 : InnerProductSpace ℝ V] [inst_2 : Fact (Module.finrank ℝ V = 2)]
  (o : Orientation ℝ V (Fin 2)) {x y : V}, (o.oangle x y).sign = -1 → y ≠ 0
-- Mathlib.Tactic.Explode.Datatypes
/-- Length of our entries.  -/
Mathlib.Explode.Entries.size : Mathlib.Explode.Entries → ℕ
-- Mathlib.LinearAlgebra.Projectivization.Constructions
Projectivization.cross_orthogonal_left : ∀ {F : Type u_1} [inst : Field F] [inst_1 : DecidableEq F] {v w : Projectivization F (Fin 3 → F)},
  v ≠ w → (v.cross w).orthogonal v
-- Mathlib.RingTheory.QuasiFinite.Basic
Algebra.QuasiFinite.instIsArtinianRingFiber : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  [Algebra.QuasiFinite R S] (P : Ideal R) [inst_4 : P.IsPrime], IsArtinianRing (P.Fiber S)
-- Mathlib.Algebra.Module.CharacterModule
CharacterModule.int.divByNat.eq_1 : ∀ (n : ℕ),
  CharacterModule.int.divByNat n = (LinearMap.toSpanSingleton ℤ (ℚ ⧸ AddSubgroup.zmultiples 1) ↑(↑n)⁻¹).toAddMonoidHom
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.LVal.fieldIdx.inj : ∀ {ref : Lean.Syntax} {i : ℕ} {levels : List Lean.Level} {ref_1 : Lean.Syntax} {i_1 : ℕ} {levels_1 : List Lean.Level},
  Lean.Elab.Term.LVal.fieldIdx ref i levels = Lean.Elab.Term.LVal.fieldIdx ref_1 i_1 levels_1 →
    ref = ref_1 ∧ i = i_1 ∧ levels = levels_1
-- Mathlib.NumberTheory.DirichletCharacter.GaussSum
gaussSum_aux_of_mulShift : ∀ {N : ℕ} [inst : NeZero N] {R : Type u_1} [inst_1 : CommRing R] (e : AddChar (ZMod N) R) (χ : DirichletCharacter R N)
  {d : ℕ} (hd : d ∣ N),
  e.mulShift ↑d = 1 → ∀ {u : (ZMod N)ˣ}, (ZMod.unitsMap hd) u = 1 → χ ↑u * gaussSum χ e = gaussSum χ e
-- Mathlib.Topology.Category.FinTopCat
/-- carrier of a finite topological space.  -/
FinTopCat.toTop : FinTopCat → TopCat
-- Mathlib.Order.Iterate
Function.Commute.iterate_pos_lt_of_map_lt' : ∀ {α : Type u_1} [inst : Preorder α] {f g : α → α},
  Function.Commute f g → StrictMono f → Monotone g → ∀ {x : α}, f x < g x → ∀ {n : ℕ}, 0 < n → f^[n] x < g^[n] x
-- Mathlib.AlgebraicGeometry.Limits
/-- The underlying topological space of the coproduct is homeomorphic to the disjoint union.  -/
AlgebraicGeometry.sigmaMk : {ι : Type u} → (f : ι → AlgebraicGeometry.Scheme) → (i : ι) × ↥(f i) ≃ₜ ↥(∐ f)
-- Mathlib.Algebra.Order.Group.Synonym
Colex.instPow : {α : Type u_1} → {β : Type u_2} → [Pow α β] → Pow (Colex α) β
-- Init.Data.Nat.Gcd
Nat.gcd_mul_left_left : ∀ (m n : ℕ), (m * n).gcd n = n
-- Mathlib.Analysis.Analytic.Linear
ContinuousLinearMap.analyticOnNhd_bilinear : ∀ {𝕜 : 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] (f : E →L[𝕜] F →L[𝕜] G) (s : Set (E × F)),
  AnalyticOnNhd 𝕜 (fun x => (f x.1) x.2) s
-- Mathlib.AlgebraicGeometry.Morphisms.ClosedImmersion
AlgebraicGeometry.instIsClosedImmersionMorphismRestrict : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) (V : Y.Opens) [AlgebraicGeometry.IsClosedImmersion f],
  AlgebraicGeometry.IsClosedImmersion (f ∣_ V)
-- Mathlib.Data.Finset.Insert
Finset.toList_eq_singleton_iff : ∀ {α : Type u_1} {a : α} {s : Finset α}, s.toList = [a] ↔ s = {a}
-- Mathlib.Order.SuccPred.Basic
Order.succ_min : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : SuccOrder α] (a b : α),
  Order.succ (min a b) = min (Order.succ a) (Order.succ b)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- Turn an element of a type `F` satisfying `MulSemiringActionHomClass F M R S` into an actual
`MulSemiringActionHom`. This is declared as the default coercion from `F` to
`MulSemiringActionHom M X Y`.  -/
MulSemiringActionHomClass.toMulSemiringActionHom : {M : Type u_1} →
  [inst : Monoid M] →
    {N : Type u_2} →
      [inst_1 : Monoid N] →
        {φ : M →* N} →
          {R : Type u_10} →
            [inst_2 : Semiring R] →
              [inst_3 : MulSemiringAction M R] →
                {S : Type u_12} →
                  [inst_4 : Semiring S] →
                    [inst_5 : MulSemiringAction N S] →
                      {F : Type u_15} →
                        [inst_6 : FunLike F R S] → [MulSemiringActionSemiHomClass F (⇑φ) R S] → F → R →ₑ+*[φ] S
-- Mathlib.CategoryTheory.Preadditive.Comma
CategoryTheory.instAdditiveArrowLeftFunc : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [inst_1 : CategoryTheory.Preadditive T],
  CategoryTheory.Arrow.leftFunc.Additive
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instAddActionOfUniformContinuousConstVAdd.eq_1 : ∀ (M : Type v) (X : Type x) [inst : UniformSpace X] [inst_1 : AddMonoid M] [inst_2 : AddAction M X]
  [inst_3 : UniformContinuousConstVAdd M X],
  UniformSpace.Completion.instAddActionOfUniformContinuousConstVAdd M X =
    { toVAdd := UniformSpace.Completion.instVAdd M X, add_vadd := ⋯, zero_vadd := ⋯ }
-- Mathlib.Computability.EpsilonNFA
NFA.toεNFA_εClosure : ∀ {α : Type u} {σ : Type v} (M : NFA α σ) (S : Set σ), M.toεNFA.εClosure S = S
-- Mathlib.LinearAlgebra.Matrix.Nonsingular
Matrix.nonsingular_iff_det_ne_zero : ∀ {n : Type u_3} [inst : Fintype n] [inst_1 : DecidableEq n] {R : Type u_4} [inst_2 : CommRing R] [IsDomain R]
  {A : Matrix n n R}, A.Nonsingular ↔ A.det ≠ 0
-- Mathlib.Algebra.Group.Submonoid.Saturation
Submonoid.le_toSubmonoid_saturation : ∀ {M : Type u_1} [inst : MulOneClass M] {a : Submonoid M}, a ≤ a.saturation.toSubmonoid
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.IsPullback.BicartesianSq
/-- ```
   0 -----0---> X
   |            |
   0           inl
   |            |
   v            v
   Y --inr--> X ⊞ Y
```
is a bi-Cartesian square.
 -/
CategoryTheory.BicartesianSq.of_has_biproduct₂ : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasZeroObject C]
  [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C] {X Y : C} [inst_3 : CategoryTheory.Limits.HasBinaryBiproduct X Y],
  CategoryTheory.BicartesianSq 0 0 CategoryTheory.Limits.biprod.inl CategoryTheory.Limits.biprod.inr
-- Mathlib.RingTheory.Congruence.Defs
RingCon.mk.sizeOf_spec : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] [inst_2 : SizeOf R] (toCon : Con R)
  (add' : ∀ {w x y z : R}, toCon.toSetoid w x → toCon.toSetoid y z → toCon.toSetoid (w + y) (x + z)),
  sizeOf { toCon := toCon, add' := add' } = 1 + sizeOf toCon
-- Init.Data.Array.Lex.Lemmas
Array.le_append_left : ∀ {α : Type u_1} [inst : LT α] [Std.Irrefl fun x1 x2 => x1 < x2] {xs ys : Array α}, xs ≤ xs ++ ys
-- Mathlib.Logic.Equiv.Basic
/-- If two predicates `p` and `q` are pointwise equivalent, then `{x // p x}` is equivalent to
`{x // q x}`.  -/
Equiv.subtypeEquivRight : {α : Sort u_1} → {p q : α → Prop} → (∀ (x : α), p x ↔ q x) → { x // p x } ≃ { x // q x }
-- Mathlib.Order.Heyting.Hom
BiheytingHom.instInhabited : {α : Type u_2} → [inst : BiheytingAlgebra α] → Inhabited (BiheytingHom α α)
-- Mathlib.Analysis.Normed.Lp.ProdLp
IsometryEquiv.withLpUniqueProd_apply : ∀ (p : ENNReal) (α : Type u_2) (β : Type u_3) [hp : Fact (1 ≤ p)] [inst : PseudoEMetricSpace α]
  [inst_1 : PseudoEMetricSpace β] [inst_2 : Unique α] (a : WithLp p (α × β)),
  (IsometryEquiv.withLpUniqueProd p α β) a = a.snd
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.piObj.congr_simp : ∀ {β : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (f f_1 : β → C) (e_f : f = f_1)
  [inst_1 : CategoryTheory.Limits.HasProduct f], ∏ᶜ f = ∏ᶜ f_1
-- Mathlib.SetTheory.Cardinal.Order
Cardinal.succ_ne_zero : ∀ (c : Cardinal.{u_1}), Order.succ c ≠ 0
-- Mathlib.RingTheory.KrullDimension.Regular
/-- If `M` is a finite module over a commutative ring `R`, `x ∈ M` is not in any minimal prime of
`M`, then `dim M/xM + 1 ≤ dim M`.  -/
Module.supportDim_quotSMulTop_succ_le_of_notMem_minimalPrimes : ∀ {R : Type u_1} [inst : CommRing R] {M : Type u_2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] [Module.Finite R M]
  {x : R},
  (∀ p ∈ (Module.annihilator R M).minimalPrimes, x ∉ p) →
    Module.supportDim R (QuotSMulTop x M) + 1 ≤ Module.supportDim R M
-- Init.Data.Array.MapIdx
Array.getElem_mapFinIdx : ∀ {α : Type u_1} {β : Type u_2} {xs : Array α} {f : (i : ℕ) → α → i < xs.size → β} {i : ℕ}
  (h : i < (xs.mapFinIdx f).size), (xs.mapFinIdx f)[i] = f i xs[i] ⋯
-- Mathlib.Data.ENNReal.Inv
ENNReal.inv_mul_le_iff : ∀ {x y z : ENNReal}, x ≠ 0 → x ≠ ⊤ → (x⁻¹ * y ≤ z ↔ y ≤ x * z)
-- Init.Data.Iterators.Lemmas.Consumers.Loop
Std.Iter.allM_eq_not_anyM_not : ∀ {α β : Type w} {m : Type → Type w'} [inst : Std.Iterator α Id β] [Std.Iterators.Finite α Id] [inst_2 : Monad m]
  [LawfulMonad m] [inst_4 : Std.IteratorLoop α Id m] [Std.LawfulIteratorLoop α Id m] {it : Std.Iter β} {p : β → m Bool},
  Std.Iter.allM p it = (fun x => !x) <$> Std.Iter.anyM (fun x => (fun x => !x) <$> p x) it
-- Mathlib.Algebra.Order.Group.Pointwise.Interval
Set.preimage_const_mul_Icc_of_neg : ∀ {α : Type u_1} [inst : Field α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α] (a b : α) {c : α},
  c < 0 → (fun x => c * x) ⁻¹' Set.Icc a b = Set.Icc (b / c) (a / c)
-- Mathlib.Algebra.MonoidAlgebra.Defs
AddMonoidAlgebra.smul_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] {A : Type u_8} [inst_1 : SMulZeroClass A R] (a : A) (m : M) (r : R),
  a • AddMonoidAlgebra.single m r = AddMonoidAlgebra.single m (a • r)
-- Mathlib.Algebra.Group.Submonoid.Units
AddSubmonoid.addUnits_left_inverse : ∀ {M : Type u_1} [inst : AddMonoid M], Function.LeftInverse AddSubmonoid.addUnits AddSubgroup.ofAddUnits
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getKey?_modify_self : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k : α} {f : β → β}, (t.modify k f).getKey? k = if k ∈ t then some k else none
-- Init.Data.String.Basic
/-- Given a slice and two valid positions within the slice, obtain a new slice on the same underlying
string formed by the new bounds.  -/
String.Slice.slice : (s : String.Slice) → (newStart newEnd : s.Pos) → newStart ≤ newEnd → String.Slice
-- Mathlib.RingTheory.Derivation.DifferentialRing
/-- A derivation from a ring to itself, as a typeclass.  -/
Differential : (R : Type u_1) → [CommRing R] → Type u_1
-- Mathlib.MeasureTheory.Function.SimpleFunc
MeasureTheory.SimpleFunc.const_zero : ∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : Zero β], MeasureTheory.SimpleFunc.const α 0 = 0
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.maxVar : (X : Type u) → (Y : Type v) → [MetricSpace X] → [MetricSpace Y] → NNReal