mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.List.ToArray
_private.Init.Data.List.ToArray.0.Array.zipWithAll.go.eq_def : ∀ {α : Type u} {β : Type u_1} {γ : Type u_2} (f : Option α → Option β → γ) (as : Array α) (bs : Array β) (i : ℕ)
  (cs : Array γ),
  Array.zipWithAll.go✝ f as bs i cs =
    if i < max as.size bs.size then
      have a := as[i]?;
      have b := bs[i]?;
      Array.zipWithAll.go✝ f as bs (i + 1) (cs.push (f a b))
    else cs
-- Mathlib.Topology.DenseEmbedding
/-- A dense embedding is an embedding with dense image.  -/
IsDenseEmbedding : {α : Type u_1} → {β : Type u_2} → [TopologicalSpace α] → [TopologicalSpace β] → (α → β) → Prop
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
LinearMap.BilinForm.IsometryEquiv.map_app' : ∀ {R : Type u_1} {M₁ : Type u_3} {M₂ : Type u_4} [inst : CommSemiring R] [inst_1 : AddCommMonoid M₁]
  [inst_2 : AddCommMonoid M₂] [inst_3 : Module R M₁] [inst_4 : Module R M₂] {B₁ : LinearMap.BilinForm R M₁}
  {B₂ : LinearMap.BilinForm R M₂} (self : B₁.IsometryEquiv B₂) (n m : M₁),
  (B₂ ((↑self.toLinearEquiv).toFun n)) ((↑self.toLinearEquiv).toFun m) = (B₁ n) m
-- Mathlib.Tactic.LinearCombination.Lemmas
Mathlib.Tactic.LinearCombination.div_le_const : ∀ {α : Type u_1} {b c : α} [inst : Semifield α] [inst_1 : LinearOrder α] [IsStrictOrderedRing α],
  b ≤ c → ∀ {a : α}, 0 ≤ a → b / a ≤ c / a
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.UnitLike.State.mk : Lean.PHashMap Lean.Meta.Sym.ExprPtr (Option Lean.Expr) → Lean.Meta.Grind.UnitLike.State
-- Mathlib.AlgebraicTopology.ModelCategory.RightHomotopy
/-- The right homotopy relation on morphisms in a category with weak equivalences.  -/
HomotopicalAlgebra.RightHomotopyRel : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [HomotopicalAlgebra.CategoryWithWeakEquivalences C] → HomRel C
-- Std.Http.Protocol.H1.Message
Std.Http.Protocol.H1.instEmptyCollectionHead : {dir : Std.Http.Protocol.H1.Direction} → EmptyCollection (Std.Http.Protocol.H1.Message.Head dir)
-- Std.Data.DTreeMap.Internal.Zipper
_private.Std.Data.DTreeMap.Internal.Zipper.0.List.filter.match_1.eq_1 : ∀ (motive : Bool → Sort u_1) (h_1 : Unit → motive true) (h_2 : Unit → motive false),
  (match true with
    | true => h_1 ()
    | false => h_2 ()) =
    h_1 ()
-- Mathlib.Data.DFinsupp.Sigma
DFinsupp.sigmaUncurry_smul : ∀ {ι : Type u} {γ : Type w} {α : ι → Type u_2} {δ : (i : ι) → α i → Type v} [inst : DecidableEq ι] [inst_1 : Monoid γ]
  [inst_2 : (i : ι) → (j : α i) → AddMonoid (δ i j)] [inst_3 : (i : ι) → (j : α i) → DistribMulAction γ (δ i j)] (r : γ)
  (f : Π₀ (i : ι) (j : α i), δ i j), (r • f).sigmaUncurry = r • f.sigmaUncurry
-- Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar
bijective_rootsOfUnityAddChar : ∀ (n : ℕ) [inst : NeZero n], Function.Bijective ⇑(ZMod.rootsOfUnityAddChar n)
-- Init.Prelude
/-- Computations in the monad `m` can be run in the monad `n`. These translations are inserted
automatically by the compiler.

Usually, `n` consists of some number of monad transformers applied to `m`, but this is not
mandatory.

This is the reflexive, transitive closure of `MonadLift`. Clients that require one monad to be
liftable into another should request an instance of `MonadLiftT`. New instances should instead be
defined for `MonadLift` itself.
 -/
MonadLiftT : (Type u → Type v) → (Type u → Type w) → Type (max (max (u + 1) v) w)
-- Mathlib.RingTheory.Bialgebra.TensorProduct
Bialgebra.TensorProduct.rid_symm_apply : ∀ {R : Type u_1} {S : Type u_2} {A : Type u_3} [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Semiring A]
  [inst_3 : Bialgebra S A] [inst_4 : Algebra R A] [inst_5 : Algebra R S] [inst_6 : IsScalarTower R S A] (a : A),
  (Bialgebra.TensorProduct.rid R S A).symm a = a ⊗ₜ[R] 1
-- Std.Http.Protocol.H1.Config
/-- The `Server` header value injected into outgoing responses (receiving mode) or the
`User-Agent` header value injected into outgoing requests (sending mode).
`none` suppresses the header entirely.
 -/
Std.Http.Protocol.H1.Config.agentName : Std.Http.Protocol.H1.Config → Option Std.Http.Header.Value
-- Mathlib.RingTheory.AlgebraicIndependent.Basic
AlgebraicIndependent.aeval_comp_mvPolynomialOptionEquivPolynomialAdjoin : ∀ {ι : Type u} {R : Type u_2} {A : Type v} {x : ι → A} [inst : CommRing R] [inst_1 : CommRing A] [inst_2 : Algebra R A]
  (hx : AlgebraicIndependent R x) (a : A),
  (↑(Polynomial.aeval a)).comp hx.mvPolynomialOptionEquivPolynomialAdjoin.toRingHom =
    ↑(MvPolynomial.aeval fun o => o.elim a x)
-- Mathlib.Topology.VectorBundle.Basic
/-- The trivial vector bundle core, in which all the changes of coordinates are the
identity.  -/
trivialVectorBundleCore : (R : Type u_1) →
  (B : Type u_2) →
    (F : Type u_3) →
      [inst : NontriviallyNormedField R] →
        [inst_1 : NormedAddCommGroup F] →
          [inst_2 : NormedSpace R F] →
            [inst_3 : TopologicalSpace B] → (ι : Type u_5) → [Inhabited ι] → VectorBundleCore R B F ι
-- Mathlib.RingTheory.Coprime.Basic
IsCoprime.add_mul_right_left : ∀ {R : Type u} [inst : CommRing R] {x y : R}, IsCoprime x y → ∀ (z : R), IsCoprime (x + z * y) y
-- Lean.Compiler.IR.Basic
Lean.IR.Expr.box.injEq : ∀ (ty : Lean.IR.IRType) (x : Lean.IR.VarId) (ty_1 : Lean.IR.IRType) (x_1 : Lean.IR.VarId),
  (Lean.IR.Expr.box ty x = Lean.IR.Expr.box ty_1 x_1) = (ty = ty_1 ∧ x = x_1)
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.Functor.mapCommMonNatIso.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C] {D : Type u₂} [inst_3 : CategoryTheory.Category.{v₂, u₂} D]
  [inst_4 : CategoryTheory.MonoidalCategory D] [inst_5 : CategoryTheory.BraidedCategory D]
  {F F' : CategoryTheory.Functor C D} [inst_6 : F.LaxBraided] [inst_7 : F'.LaxBraided] (e e_1 : F ≅ F') (e_e : e = e_1)
  [inst_8 : CategoryTheory.NatTrans.IsMonoidal e.hom],
  CategoryTheory.Functor.mapCommMonNatIso e = CategoryTheory.Functor.mapCommMonNatIso e_1
-- Mathlib.CategoryTheory.Core
CategoryTheory.Functor.coreComp_hom_app_iso_inv : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u₃} [inst_2 : CategoryTheory.Category.{v₃, u₃} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) (X : CategoryTheory.Core C),
  ((F.coreComp G).hom.app X).iso.inv = CategoryTheory.CategoryStruct.id (G.obj (F.obj X.of))
-- Lean.Meta.Sym.Pattern
_private.Lean.Meta.Sym.Pattern.0.Lean.Meta.Sym.UnifyM.Context.mk.inj : ∀ {pattern : Lean.Meta.Sym.Pattern} {unify zetaDelta : Bool} {pattern_1 : Lean.Meta.Sym.Pattern}
  {unify_1 zetaDelta_1 : Bool},
  { pattern := pattern, unify := unify, zetaDelta := zetaDelta } =
      { pattern := pattern_1, unify := unify_1, zetaDelta := zetaDelta_1 } →
    pattern = pattern_1 ∧ unify = unify_1 ∧ zetaDelta = zetaDelta_1
-- Mathlib.CategoryTheory.Sites.Descent.DescentDataPrime
CategoryTheory.Pseudofunctor.DescentData'.pullHom'_hom_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  {F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete Cᵒᵖ) CategoryTheory.Cat} {ι : Type t} {S : C}
  {X : ι → C} {f : (i : ι) → X i ⟶ S} {sq : (i j : ι) → CategoryTheory.Limits.ChosenPullback (f i) (f j)}
  {sq₃ : (i₁ i₂ i₃ : ι) → CategoryTheory.Limits.ChosenPullback₃ (sq i₁ i₂) (sq i₂ i₃) (sq i₁ i₃)}
  (self : F.DescentData' sq sq₃) (i₁ i₂ i₃ : ι)
  {Z : ↑(F.obj { as := Opposite.op (sq₃ i₁ i₂ i₃).chosenPullback.pullback })}
  (h : (F.map (sq₃ i₁ i₂ i₃).p₃.op.toLoc).toFunctor.obj (self.obj i₃) ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.DescentData'.pullHom' self.hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₂
        ⋯ ⋯)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Pseudofunctor.DescentData'.pullHom' self.hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₂
          (sq₃ i₁ i₂ i₃).p₃ ⋯ ⋯)
        h) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Pseudofunctor.DescentData'.pullHom' self.hom (sq₃ i₁ i₂ i₃).p (sq₃ i₁ i₂ i₃).p₁ (sq₃ i₁ i₂ i₃).p₃
        ⋯ ⋯)
      h
-- Mathlib.Topology.Homotopy.Path
/-- `Path.Homotopic.Quotient.mk` is the simp normal form.  -/
Path.Homotopic.Quotient.mk'_eq_mk : ∀ {X : Type u} [inst : TopologicalSpace X] {x₀ x₁ : X} (p : Path x₀ x₁), Quotient.mk' p = Path.Homotopic.Quotient.mk p
-- Init.Data.Rat.Basic
/-- Division of rational numbers. Note: `div a 0 = 0`.  -/
Rat.div : ℚ → ℚ → ℚ
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.get_insert_self : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α] {k : α}
  {v : β k}, (m.insert k v).get k ⋯ = v
-- Mathlib.Analysis.Complex.ReImTopology
/-- **Alias** of `Complex.interior_setOfPred_le_im`. -/
Complex.interior_setOf_le_im : ∀ (a : ℝ), interior {z | a ≤ z.im} = {z | a < z.im}
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.packingRadius_pos : ∀ {X : Type u_3} [inst : MetricSpace X] (self : Delone.DeloneSet X), 0 < self.packingRadius
-- Mathlib.GroupTheory.GroupExtension.Defs
/-- The underlying function  -/
AddGroupExtension.Section.toFun : {N : Type u_1} →
  {E : Type u_2} →
    {G : Type u_3} →
      [inst : AddGroup N] →
        [inst_1 : AddGroup E] → [inst_2 : AddGroup G] → {S : AddGroupExtension N E G} → S.Section → G → E
-- Mathlib.Probability.Process.Stopping
MeasureTheory.stoppedProcess_stoppedProcess : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : Nonempty ι] {u : ι → Ω → β} {τ σ : Ω → WithTop ι}
  [inst_1 : LinearOrder ι],
  MeasureTheory.stoppedProcess (MeasureTheory.stoppedProcess u τ) σ = MeasureTheory.stoppedProcess u (σ ⊓ τ)
-- Mathlib.MeasureTheory.SetSemiring
MeasureTheory.IsSetSemiring.subset_of_mem_disjointOfUnion : ∀ {α : Type u_1} {C : Set (Set α)} {j : Set α} {J : Finset (Set α)} (hC : MeasureTheory.IsSetSemiring C) (hJ : ↑J ⊆ C),
  j ∈ J → ∀ {x : Set α}, x ∈ hC.disjointOfUnion hJ j → x ⊆ j
-- Mathlib.Data.Finset.Powerset
/-- `s.biUnion id ⊆ t` iff every member of `s` is a subset of `t`, i.e. `s ⊆ t.powerset`.  -/
Finset.biUnion_id_subset_iff_subset_powerset : ∀ {α : Type u_1} {t : Finset α} [inst : DecidableEq α] {s : Finset (Finset α)}, s.biUnion id ⊆ t ↔ s ⊆ t.powerset
-- Mathlib.RingTheory.Ideal.Norm.AbsNorm
Ideal.absNorm_span_singleton : ∀ {S : Type u_1} [inst : CommRing S] [inst_1 : IsDedekindDomain S] [inst_2 : Module.Free ℤ S] [Module.Finite ℤ S]
  (r : S), Ideal.absNorm (Ideal.span {r}) = ((Algebra.norm ℤ) r).natAbs
-- Mathlib.NumberTheory.Modular
/-- For every `τ : ℍ` there is some `γ ∈ SL(2, ℤ)` that sends it to an element whose
imaginary part is at least `1/2` and such that `denom γ τ` has norm at most 1.  -/
ModularGroup.exists_one_half_le_im_smul_and_norm_denom_le : ∀ (τ : UpperHalfPlane),
  ∃ γ,
    1 / 2 ≤ (γ • τ).im ∧
      ‖UpperHalfPlane.denom (Matrix.SpecialLinearGroup.toGL ((Matrix.SpecialLinearGroup.map (Int.castRingHom ℝ)) γ))
            ↑τ‖ ≤
        1
-- Mathlib.Data.Sigma.Lex
Sigma.instIrreflLex : ∀ {ι : Type u_1} {α : ι → Type u_2} {r : ι → ι → Prop} {s : (i : ι) → α i → α i → Prop} [Std.Irrefl r]
  [∀ (i : ι), Std.Irrefl (s i)], Std.Irrefl (Sigma.Lex r s)
-- Mathlib.Data.Finset.NoncommProd
Finset.noncommSum_insert_of_notMem : ∀ {α : Type u_3} {β : Type u_4} [inst : AddMonoid β] [inst_1 : DecidableEq α] (s : Finset α) (a : α) (f : α → β)
  (comm : (↑(insert a s)).Pairwise (Function.onFun AddCommute f)),
  a ∉ s → (insert a s).noncommSum f comm = f a + s.noncommSum f ⋯
-- Batteries.Data.String.Legacy
/-- Checks whether the Boolean predicate `p` returns `true` for every character in a string.

Short-circuits at the first character for which `p` returns `false`.

This is an old implementation, preserved here for users of the lemmas in
`Batteries.Data.String.Lemmas`.

Examples:
 * `"brown".all (·.isLetter) = true`
 * `"brown and orange".all (·.isLetter) = false`
 * `"".all (fun _ => false) = true`
 -/
String.Legacy.all : String → (Char → Bool) → Bool
-- Mathlib.Analysis.Calculus.FDeriv.Prod
DifferentiableAt.prodMap : ∀ {𝕜 : 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] {G' : Type u_5} [inst_7 : NormedAddCommGroup G']
  [inst_8 : NormedSpace 𝕜 G'] {f : E → F} {f₂ : G → G'} (p : E × G),
  DifferentiableAt 𝕜 f p.1 → DifferentiableAt 𝕜 f₂ p.2 → DifferentiableAt 𝕜 (fun p => (f p.1, f₂ p.2)) p
-- Mathlib.CategoryTheory.Monoidal.NaturalTransformation
CategoryTheory.LaxMonoidalFunctor.Hom.isMonoidal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {D : Type u₂}
  [inst_2 : CategoryTheory.Category.{v₂, u₂} D] [inst_3 : CategoryTheory.MonoidalCategory D]
  {F G : CategoryTheory.LaxMonoidalFunctor C D} (self : F.Hom G), CategoryTheory.NatTrans.IsMonoidal self.hom
-- Mathlib.Algebra.Homology.Embedding.RestrictionHomology
/-- The isomorphism `(K.restriction e).sc' i j k ≅ K.sc' i' j' k'` when
`e` is an embedding of complex shapes, `i'`, `j`, `k`' are the respective
images of `i`, `j`, `k` by `e.f`, `j` is the previous index of `i`, etc.  -/
HomologicalComplex.restriction.sc'Iso : {ι : Type u_1} →
  {ι' : Type u_2} →
    {c : ComplexShape ι} →
      {c' : ComplexShape ι'} →
        {C : Type u_3} →
          [inst : CategoryTheory.Category.{v_1, u_3} C] →
            [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
              (K : HomologicalComplex C c') →
                (e : c.Embedding c') →
                  [inst_2 : e.IsRelIff] →
                    (i j k : ι) →
                      {i' j' k' : ι'} →
                        e.f i = i' →
                          e.f j = j' →
                            e.f k = k' →
                              c'.prev j' = i' → c'.next j' = k' → ((K.restriction e).sc' i j k ≅ K.sc' i' j' k')
-- Mathlib.LinearAlgebra.Dual.Defs
Module.equiv : ∀ {R : Type u_3} {M : Type u_4} {N : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid N] [inst_3 : Module R M] [inst_4 : Module R N] [Module.IsReflexive R M] (e : M ≃ₗ[R] N),
  Module.IsReflexive R N
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Adj
CategoryTheory.Bicategory.Adj.Hom₂.mk.injEq : ∀ {B : Type u} [inst : CategoryTheory.Bicategory B] {a b : CategoryTheory.Bicategory.Adj B} {α β : a ⟶ b}
  (τl : α.l ⟶ β.l) (τr : β.r ⟶ α.r)
  (conjugateEquiv_τl :
    autoParam ((CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) τl = τr)
      CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τl._autoParam)
  (τl_1 : α.l ⟶ β.l) (τr_1 : β.r ⟶ α.r)
  (conjugateEquiv_τl_1 :
    autoParam ((CategoryTheory.Bicategory.conjugateEquiv β.adj α.adj) τl_1 = τr_1)
      CategoryTheory.Bicategory.Adj.Hom₂.conjugateEquiv_τl._autoParam),
  ({ τl := τl, τr := τr, conjugateEquiv_τl := conjugateEquiv_τl } =
      { τl := τl_1, τr := τr_1, conjugateEquiv_τl := conjugateEquiv_τl_1 }) =
    (τl = τl_1 ∧ τr = τr_1)
-- Mathlib.Analysis.CStarAlgebra.Matrix
Matrix.ofLp_toEuclideanCLM : ∀ {𝕜 : Type u_1} {n : Type u_3} [inst : RCLike 𝕜] [inst_1 : Fintype n] [inst_2 : DecidableEq n] (A : Matrix n n 𝕜)
  (x : EuclideanSpace 𝕜 n), ((Matrix.toEuclideanCLM A) x).ofLp = A.mulVec x.ofLp
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.insertListIfNewUnit.eq_def : ∀ {α : Type u} [inst : BEq α] (l : List ((_ : α) × Unit)) (toInsert : List α),
  Std.Internal.List.insertListIfNewUnit l toInsert =
    match toInsert with
    | [] => l
    | hd :: tl => Std.Internal.List.insertListIfNewUnit (Std.Internal.List.insertEntryIfNew hd () l) tl
-- Mathlib.Geometry.Manifold.Notation
/-- The expression for the normed space itself.  -/
Manifold.Elab.NormedSpaceInfo.normedSpace : Manifold.Elab.NormedSpaceInfo → Lean.Expr
-- Mathlib.Data.Fintype.Defs
Fintype.decidableMemRangeFintype : {α : Type u_1} → {β : Type u_2} → [Fintype α] → [DecidableEq β] → (f : α → β) → DecidablePred fun x => x ∈ Set.range f
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.NormLeOne
/-- A fixed equiv between `Fin (rank K)` and `{w : InfinitePlace K // w ≠ w₀}`.
 -/
NumberField.mixedEmbedding.fundamentalCone.equivFinRank : {K : Type u_1} →
  [inst : Field K] →
    [inst_1 : NumberField K] → Fin (NumberField.Units.rank K) ≃ { w // w ≠ NumberField.Units.dirichletUnitTheorem.w₀ }
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_roo_eq_if : ∀ {m n : ℤ}, (m<...n).toArray = if m + 1 < n then #[m + 1] ++ ((m + 1)<...n).toArray else #[]
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roo.toArray_eq_match : ∀ {α : Type u} {r : Std.Roo α} [LE α] [inst : LT α] [inst_1 : DecidableLT α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLT α]
  [inst_5 : Std.Rxo.IsAlwaysFinite α],
  r.toArray =
    match Std.PRange.succ? r.lower with
    | none => #[]
    | some next => if next < r.upper then #[next] ++ (next<...r.upper).toArray else #[]
-- Mathlib.RingTheory.Extension.Presentation.Basic
Algebra.Presentation.compRelationAux.eq_1 : ∀ {R : Type u} {S : Type v} {ι : Type w} {σ : Type t} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  {ι' : Type u_1} {σ' : Type u_2} {T : Type u_3} [inst_3 : CommRing T] [inst_4 : Algebra S T]
  (Q : Algebra.Presentation S T ι' σ') (P : Algebra.Presentation R S ι σ) (r : σ'),
  Q.compRelationAux P r =
    (Q.relation r).coeff.sum fun x j =>
      (MvPolynomial.rename Sum.inr) (P.σ j) * (MvPolynomial.monomial (Finsupp.mapDomain Sum.inl x)) 1
-- Mathlib.Data.TypeVec
TypeVec.repeat_eq_nil : ∀ (α : TypeVec.{u_1} 0), α.repeatEq = TypeVec.nilFun
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Char
String.eq_append_of_dropPrefix?_char_eq_some : ∀ {c : Char} {s : String} {res : String.Slice}, s.dropPrefix? c = some res → s = String.singleton c ++ res.copy
-- Mathlib.CategoryTheory.Functor.KanExtension.Adjunction
CategoryTheory.Functor.instIsIsoAppRanCounit : ∀ {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] (L : CategoryTheory.Functor C D) {H : Type u_3}
  [inst_2 : CategoryTheory.Category.{v_3, u_3} H] [L.Full] [L.Faithful] (F : CategoryTheory.Functor C H) (X : C)
  [L.HasPointwiseRightKanExtension F] [inst_6 : ∀ (F : CategoryTheory.Functor C H), L.HasRightKanExtension F],
  CategoryTheory.IsIso ((L.ranCounit.app F).app X)
-- Mathlib.Order.Interval.Set.Image
MonotoneOn.image_Icc_subset : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : Preorder α] [inst_1 : Preorder β] {a b : α},
  MonotoneOn f (Set.Icc a b) → f '' Set.Icc a b ⊆ Set.Icc (f a) (f b)
-- Mathlib.Algebra.Homology.HomotopyCategory.ShortExact
CochainComplex.mappingCone.descShortComplex.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (S : CategoryTheory.ShortComplex (CochainComplex C ℤ)),
  CochainComplex.mappingCone.descShortComplex S = CochainComplex.mappingCone.desc S.f 0 S.g ⋯
-- Batteries.Data.List.Lemmas
List.unzip_findIdxsValues : ∀ {α : Type u_1} {xs : List α} {p : α → Bool} {s : ℕ},
  (List.findIdxsValues p xs s).unzip = (List.findIdxs p xs s, List.filter p xs)
-- Mathlib.CategoryTheory.Abelian.NonPreadditive
CategoryTheory.NonPreadditiveAbelian.sub_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.NonPreadditiveAbelian C] {X Y : C}
  (a b : X ⟶ Y),
  a - b =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.prod.lift a b) CategoryTheory.NonPreadditiveAbelian.σ
-- Mathlib.Order.Category.BoolAlg
/-- Use the `ConcreteCategory.hom` projection for `@[simps]` lemmas.  -/
BoolAlg.Hom.Simps.hom : (X Y : BoolAlg) → X.Hom Y → BoundedLatticeHom ↑X ↑Y
-- Mathlib.Tactic.Widget.CongrM
/-- Return the link text and inserted text above and below of the congrm widget.  -/
makeCongrMString : Array Lean.SubExpr.GoalsLocation →
  Lean.Expr → SelectInsertParams → Lean.MetaM (String × String × Option (String.Pos.Raw × String.Pos.Raw))
-- Lean.Parser.Extra
Lean.Parser.withoutForbidden.formatter : Lean.PrettyPrinter.Formatter → Lean.PrettyPrinter.Formatter
-- Lean.Meta.Tactic.Grind.Arith.Linear.StructId
_private.Lean.Meta.Tactic.Grind.Arith.Linear.StructId.0.Lean.Meta.Grind.Arith.Linear.mkOne? : Lean.Level → Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.Data.Set.MulAntidiagonal
Set.mulAntidiagonal_mono_right : ∀ {α : Type u_1} [inst : Mul α] {s t₁ t₂ : Set α} {a : α}, t₁ ⊆ t₂ → s.mulAntidiagonal t₁ a ⊆ s.mulAntidiagonal t₂ a
-- Mathlib.Logic.Equiv.PartialEquiv
PartialEquiv.coe_trans_symm : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} (e : PartialEquiv α β) (e' : PartialEquiv β γ),
  ↑(e.trans e').symm = ↑e.symm ∘ ↑e'.symm
-- Mathlib.AlgebraicTopology.SimplicialSet.Nonsingular
/-- [Kerodon Tag 02MT](https://kerodon.net/tag/02MT) -/
SSet.instNonsingularNerve : ∀ (T : Type u_1) [inst : PartialOrder T], (CategoryTheory.nerve T).Nonsingular
-- Mathlib.Topology.Algebra.Group.CompactOpen
ContinuousMonoidHom.compRight.eq_1 : ∀ (A : Type u_2) {E : Type u_6} [inst : Monoid A] [inst_1 : CommGroup E] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace E] [inst_4 : IsTopologicalGroup E] {B : Type u_7} [inst_5 : CommGroup B]
  [inst_6 : TopologicalSpace B] [inst_7 : IsTopologicalGroup B] (f : B →ₜ* E),
  ContinuousMonoidHom.compRight A f =
    { toFun := fun g => f.comp g, map_one' := ⋯, map_mul' := ⋯, continuous_toFun := ⋯ }
-- Mathlib.Algebra.Algebra.Operations
SetSemiring.singletonMonoidHom.eq_1 : ∀ {α : Type u_1} [inst : Monoid α],
  SetSemiring.singletonMonoidHom = { toFun := fun a => Set.up {a}, map_one' := ⋯, map_mul' := ⋯ }
-- Batteries.Data.String.Lemmas
String.Pos.Raw.extract.go₂_append_left : ∀ (s t : List Char) (i e : ℕ),
  e = String.utf8Len s + i → String.Pos.Raw.extract.go₂ (s ++ t) { byteIdx := i } { byteIdx := e } = s
-- Mathlib.CategoryTheory.Discrete.Basic
/-- Extract the equation from a morphism in a discrete category.  -/
CategoryTheory.Discrete.eq_of_hom : ∀ {α : Type u₁} {X Y : CategoryTheory.Discrete α} (i : X ⟶ Y), X.as = Y.as
-- Mathlib.SetTheory.Cardinal.ENat
Cardinal.ofENat_eq_one : ∀ {m : ℕ∞}, ↑m = 1 ↔ m = 1
-- Mathlib.Util.AssertNoSorry
/-- Throws an error if the given identifier uses sorryAx.  -/
commandAssert_no_sorry_ : Lean.ParserDescr
-- Mathlib.CategoryTheory.EpiMono
/-- This is a theorem saying if five faces of a cube commute and one edge is an epimorphism,
then the sixth face must also commute.  -/
CategoryTheory.cube_lemma_of_epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {M000 M001 M010 M011 M100 M101 M110 M111 : C}
  (f00x : M000 ⟶ M001) (f01x : M010 ⟶ M011) (f10x : M100 ⟶ M101) (f11x : M110 ⟶ M111) (f0x0 : M000 ⟶ M010)
  (f0x1 : M001 ⟶ M011) (f1x0 : M100 ⟶ M110) (f1x1 : M101 ⟶ M111) (fx00 : M000 ⟶ M100) (fx01 : M001 ⟶ M101)
  (fx10 : M010 ⟶ M110) (fx11 : M011 ⟶ M111),
  CategoryTheory.CategoryStruct.comp f0x0 f01x = CategoryTheory.CategoryStruct.comp f00x f0x1 →
    CategoryTheory.CategoryStruct.comp f1x0 f11x = CategoryTheory.CategoryStruct.comp f10x f1x1 →
      CategoryTheory.CategoryStruct.comp fx00 f10x = CategoryTheory.CategoryStruct.comp f00x fx01 →
        CategoryTheory.CategoryStruct.comp fx10 f11x = CategoryTheory.CategoryStruct.comp f01x fx11 →
          CategoryTheory.CategoryStruct.comp f0x0 fx10 = CategoryTheory.CategoryStruct.comp fx00 f1x0 →
            ∀ [CategoryTheory.Epi f00x],
              CategoryTheory.CategoryStruct.comp f0x1 fx11 = CategoryTheory.CategoryStruct.comp fx01 f1x1
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Internal.ComputableSmall.deflate_inflate : ∀ {α : Type v} [self : Std.Internal.ComputableSmall α] {a : Std.Internal.ComputableSmall.Target α},
  Std.Internal.ComputableSmall.deflate (Std.Internal.ComputableSmall.inflate a) = a
-- Mathlib.Topology.MetricSpace.ThickenedIndicator
/-- Pointwise, the multiplicative indicators of closed δ-thickenings of a set eventually coincide
with the multiplicative indicator of the set as δ tends to zero.  -/
mulIndicator_cthickening_eventually_eq_mulIndicator_closure : ∀ {α : Type u_1} [inst : PseudoEMetricSpace α] {β : Type u_2} [inst_1 : One β] (f : α → β) (E : Set α) (x : α),
  ∀ᶠ (δ : ℝ) in nhds 0, (Metric.cthickening δ E).mulIndicator f x = (closure E).mulIndicator f x