mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Basic
WeierstrassCurve.Affine.equation_iff' : ∀ {R : Type r} [inst : CommRing R] {W : WeierstrassCurve.Affine R} (x y : R),
  W.Equation x y ↔ y ^ 2 + W.a₁ * x * y + W.a₃ * y - (x ^ 3 + W.a₂ * x ^ 2 + W.a₄ * x + W.a₆) = 0
-- Mathlib.Algebra.Module.LocalizedModule.Basic
IsLocalizedModule.mk'_zero : ∀ {R : Type u_1} [inst : CommSemiring R] {S : Submonoid R} {M : Type u_2} {M' : Type u_3} [inst_1 : AddCommMonoid M]
  [inst_2 : AddCommMonoid M'] [inst_3 : Module R M] [inst_4 : Module R M'] (f : M →ₗ[R] M')
  [inst_5 : IsLocalizedModule S f] (s : ↥S), IsLocalizedModule.mk' f 0 s = 0
-- Mathlib.CategoryTheory.Limits.VanKampen
/-- A van Kampen colimit is a colimit.  -/
CategoryTheory.IsVanKampenColimit.isColimit : {J : Type v'} →
  [inst : CategoryTheory.Category.{u', v'} J] →
    {C : Type u} →
      [inst_1 : CategoryTheory.Category.{v, u} C] →
        {F : CategoryTheory.Functor J C} →
          {c : CategoryTheory.Limits.Cocone F} → CategoryTheory.IsVanKampenColimit c → CategoryTheory.Limits.IsColimit c
-- Mathlib.LinearAlgebra.Matrix.Charpoly.Coeff
Matrix.charpolyRev.eq_1 : ∀ {R : Type u} [inst : CommRing R] {n : Type v} [inst_1 : DecidableEq n] [inst_2 : Fintype n] (M : Matrix n n R),
  M.charpolyRev = (1 - Polynomial.X • M.map ⇑Polynomial.C).det
-- Mathlib.RingTheory.Valuation.Basic
Valuation.map_add_eq_of_lt_left : ∀ {R : Type u_3} {Γ₀ : Type u_4} [inst : Ring R] [inst_1 : LinearOrderedCommMonoidWithZero Γ₀] (v : Valuation R Γ₀)
  {x y : R}, v y < v x → v (x + y) = v x
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
isUniformEmbedding_translate_mul : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] (a : α),
  IsUniformEmbedding fun x => x * a
-- Lean.CoreM
Lean.instMonadExceptOfExceptionCoreM : MonadExceptOf Lean.Exception Lean.CoreM
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
/-- The type of continuous additive monoid homomorphisms from `A` to `B`.

When possible, instead of parametrizing results over `(f : ContinuousAddMonoidHom A B)`,
you should parametrize
over `(F : Type*) [FunLike F A B] [ContinuousMapClass F A B] [AddMonoidHomClass F A B] (f : F)`.

When you extend this structure,
make sure to extend `ContinuousMapClass` and/or `AddMonoidHomClass`, if needed.  -/
ContinuousAddMonoidHom : (A : Type u_7) →
  (B : Type u_8) → [AddMonoid A] → [AddMonoid B] → [TopologicalSpace A] → [TopologicalSpace B] → Type (max u_7 u_8)
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.HasPullback
CategoryTheory.Limits.pullbackComparison_comp_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {E : Type u_1} [inst_2 : CategoryTheory.Category.{v_1, u_1} E] (F : CategoryTheory.Functor C D)
  (G : CategoryTheory.Functor D E) {X Y S : C} (f : X ⟶ S) (g : Y ⟶ S) [inst_3 : CategoryTheory.Limits.HasPullback f g]
  [inst_4 : CategoryTheory.Limits.HasPullback (F.map f) (F.map g)]
  [inst_5 : CategoryTheory.Limits.HasPullback (G.map (F.map f)) (G.map (F.map g))]
  [inst_6 : CategoryTheory.Limits.HasPullback ((F.comp G).map f) ((F.comp G).map g)] {Z : E}
  (h : CategoryTheory.Limits.pullback (G.map (F.map f)) (G.map (F.map g)) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison (F.comp G) f g) h =
    CategoryTheory.CategoryStruct.comp (G.map (CategoryTheory.Limits.pullbackComparison F f g))
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackComparison G (F.map f) (F.map g)) h)
-- Init.Data.Range.Polymorphic.UpwardEnumerable
/-- The `n + 1`-th successor of `a` is the successor of the `n`-th successor, given that said
successors actually exist.
 -/
Std.PRange.LawfulUpwardEnumerable.succMany?_add_one : ∀ {α : Type u} {inst : Std.PRange.UpwardEnumerable α} [self : Std.PRange.LawfulUpwardEnumerable α] (n : ℕ) (a : α),
  Std.PRange.succMany? (n + 1) a = (Std.PRange.succMany? n a).bind Std.PRange.succ?
-- Mathlib.Topology.Algebra.StarSubalgebra
StarAlgebra.elemental.le_of_mem : ∀ {R : Type u_1} {A : Type u_2} [inst : CommSemiring R] [inst_1 : StarRing R] [inst_2 : TopologicalSpace A]
  [inst_3 : Semiring A] [inst_4 : StarRing A] [inst_5 : IsSemitopologicalSemiring A] [inst_6 : ContinuousStar A]
  [inst_7 : Algebra R A] [inst_8 : StarModule R A] {S : StarSubalgebra R A},
  IsClosed ↑S → ∀ {x : A}, x ∈ S → StarAlgebra.elemental R x ≤ S
-- Mathlib.MeasureTheory.Measure.MeasureSpace
MeasureTheory.Measure.instInfSet : {α : Type u_1} → {x : MeasurableSpace α} → InfSet (MeasureTheory.Measure α)
-- Mathlib.SetTheory.Cardinal.Defs
Cardinal.sum.eq_1 : ∀ {ι : Type u_1} (f : ι → Cardinal.{u_2}), Cardinal.sum f = Cardinal.mk ((i : ι) × Quotient.out (f i))
-- Mathlib.CategoryTheory.Monoidal.CommMon_
CategoryTheory.CommMon.uniqueHomFromTrivial : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      [inst_2 : CategoryTheory.BraidedCategory C] →
        (A : CategoryTheory.CommMon C) → Unique (CategoryTheory.CommMon.trivial C ⟶ A)
-- Mathlib.Analysis.CStarAlgebra.CStarMatrix
CStarMatrix.uniformEmbedding_ofMatrix : ∀ {m : Type u_1} {n : Type u_2} {A : Type u_3} [inst : NonUnitalCStarAlgebra A],
  IsUniformEmbedding ⇑CStarMatrix.ofMatrix
-- Mathlib.AlgebraicGeometry.Morphisms.Integral
/-- **Alias** of `AlgebraicGeometry.IsIntegralHom.isIntegral_app`. -/
AlgebraicGeometry.Scheme.Hom.isIntegral_app : ∀ {X Y : AlgebraicGeometry.Scheme} (f : X ⟶ Y) [self : AlgebraicGeometry.IsIntegralHom f] (U : Y.Opens),
  AlgebraicGeometry.IsAffineOpen U → (CommRingCat.Hom.hom (AlgebraicGeometry.Scheme.Hom.app f U)).IsIntegral
-- Mathlib.Topology.Algebra.InfiniteSum.NatInt
HasProd.of_add_one_of_neg_add_one : ∀ {M : Type u_1} [inst : CommMonoid M] [inst_1 : TopologicalSpace M] {m m' : M} [ContinuousMul M] {f : ℤ → M},
  HasProd (fun n => f (↑n + 1)) m → HasProd (fun n => f (-(↑n + 1))) m' → HasProd f (m * f 0 * m')
-- Mathlib.Algebra.BigOperators.Expect
Finset.expect_add_distrib : ∀ {ι : Type u_1} {M : Type u_4} [inst : AddCommMonoid M] [inst_1 : Module ℚ≥0 M] (s : Finset ι) (f g : ι → M),
  (s.expect fun i => f i + g i) = (s.expect fun i => f i) + s.expect fun i => g i
-- Mathlib.RepresentationTheory.Continuous.Basic
ContIntertwiningMap.instAdd : {R : Type u_1} →
  {G : Type u_2} →
    {V : Type u_3} →
      {W : Type u_4} →
        [inst : Monoid G] →
          [inst_1 : Ring R] →
            [inst_2 : AddCommGroup V] →
              [inst_3 : TopologicalSpace V] →
                [inst_4 : IsTopologicalAddGroup V] →
                  [inst_5 : Module R V] →
                    [inst_6 : AddCommGroup W] →
                      [inst_7 : TopologicalSpace W] →
                        [inst_8 : IsTopologicalAddGroup W] →
                          [inst_9 : Module R W] →
                            {π₁ : ContRepresentation R G V} →
                              {π₂ : ContRepresentation R G W} → Add (ContIntertwiningMap π₁ π₂)
-- Mathlib.Algebra.Group.Pi.Basic
Pi.divisionCommMonoid : {I : Type u} → {f : I → Type v₁} → [(i : I) → DivisionCommMonoid (f i)] → DivisionCommMonoid ((i : I) → f i)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
Mathlib.Tactic.BicategoryLike.instInhabitedCoherenceHom : Inhabited Mathlib.Tactic.BicategoryLike.CoherenceHom
-- Lean.Meta.Tactic.Grind.Types
Lean.Meta.Grind.NewFact.fact.sizeOf_spec : ∀ (prop proof : Lean.Expr) (generation : ℕ),
  sizeOf (Lean.Meta.Grind.NewFact.fact prop proof generation) = 1 + sizeOf prop + sizeOf proof + sizeOf generation
-- Mathlib.Algebra.Ring.CentroidHom
CentroidHom.instModule : {R : Type u_4} →
  {α : Type u_5} →
    [inst : NonUnitalNonAssocSemiring α] →
      [inst_1 : Semiring R] →
        [inst_2 : Module R α] → [SMulCommClass R α α] → [IsScalarTower R α α] → Module R (CentroidHom α)
-- Mathlib.RingTheory.Bialgebra.Equiv
/-- The proposition that the function preserves multiplication  -/
BialgEquiv.map_mul' : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} {B : Type w} [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (self : A ≃ₐc[R] B) (x y : A), self.toFun (x * y) = self.toFun x * self.toFun y
-- Mathlib.Algebra.Module.Submodule.Map
/-- If `p ≤ q`, then `p` as a subgroup of `q` is isomorphic to `p`.  -/
Submodule.submoduleOfEquivOfLe : {R : Type u_1} →
  {M : Type u_5} →
    [inst : Semiring R] →
      [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → {p q : Submodule R M} → p ≤ q → ↥(p.submoduleOf q) ≃ₗ[R] ↥p
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.contains_of_contains_insert : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α] (h : t.WF)
  {k a : α} {v : β k},
  Std.DTreeMap.Internal.Impl.contains a (Std.DTreeMap.Internal.Impl.insert k v t ⋯).impl = true →
    compare k a ≠ Ordering.eq → Std.DTreeMap.Internal.Impl.contains a t = true
-- Lean.Elab.SyntheticMVars
Lean.Elab.Term.instReprPostponeBehavior : Repr Lean.Elab.Term.PostponeBehavior
-- Mathlib.Data.Real.ConjExponents
NNReal.HolderTriple.symm : ∀ {p q r : NNReal}, p.HolderTriple q r → q.HolderTriple p r
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt
_private.Lean.Meta.Tactic.Grind.Arith.Cutsat.ToInt.0.Lean.Meta.Grind.Arith.Cutsat.toInt'.processDivMod : Lean.Expr → Bool → Lean.Expr → Lean.Expr → Lean.Meta.Grind.Arith.Cutsat.ToIntM (Lean.Expr × Lean.Expr)
-- Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass
PeriodPair.g₂.eq_1 : ∀ (L : PeriodPair), L.g₂ = 60 * L.G 4
-- Mathlib.Dynamics.PeriodicPts.Defs
Function.periodicOrbit_apply_eq : ∀ {α : Type u_1} {f : α → α} {x : α},
  x ∈ Function.periodicPts f → Function.periodicOrbit f (f x) = Function.periodicOrbit f x
-- Mathlib.Data.EReal.Basic
instTopEReal : Top EReal
-- Mathlib.Topology.ContinuousMap.Star
Homeomorph.compStarAlgEquiv'_symm_apply : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] (𝕜 : Type u_3)
  [inst_2 : CommSemiring 𝕜] (A : Type u_4) [inst_3 : TopologicalSpace A] [inst_4 : Semiring A]
  [inst_5 : IsTopologicalSemiring A] [inst_6 : StarRing A] [inst_7 : ContinuousStar A] [inst_8 : Algebra 𝕜 A]
  (f : X ≃ₜ Y) (a : C(X, A)),
  (Homeomorph.compStarAlgEquiv' 𝕜 A f).symm a = (ContinuousMap.compStarAlgHom' 𝕜 A ↑f.symm) a
-- Mathlib.Algebra.BigOperators.Group.Finset.Basic
/-- The difference with `Finset.prod_ninvolution` is that the involution is allowed to use
membership of the domain of the product, rather than being a non-dependent function.  -/
Finset.prod_involution : ∀ {ι : Type u_1} {M : Type u_4} {s : Finset ι} [inst : CommMonoid M] {f : ι → M} (g : (a : ι) → a ∈ s → ι),
  (∀ (a : ι) (ha : a ∈ s), f a * f (g a ha) = 1) →
    (∀ (a : ι) (ha : a ∈ s), f a ≠ 1 → g a ha ≠ a) →
      ∀ (g_mem : ∀ (a : ι) (ha : a ∈ s), g a ha ∈ s), (∀ (a : ι) (ha : a ∈ s), g (g a ha) ⋯ = a) → ∏ x ∈ s, f x = 1
-- Mathlib.Order.Hom.WithTopBot
SupHom.withTop_id : ∀ {α : Type u_1} [inst : SemilatticeSup α], (SupHom.id α).withTop = SupHom.id (WithTop α)
-- Mathlib.CategoryTheory.Monoidal.Arrow
CategoryTheory.MonoidalCategory.Arrow.PushoutProduct.whiskerRight_def : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPushouts C]
  [inst_2 : CategoryTheory.Limits.HasInitial C] [inst_3 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_4 : CategoryTheory.MonoidalClosed C] [inst_5 : CategoryTheory.BraidedCategory C]
  {X₁ X₂ : CategoryTheory.Arrow C} (f : X₁ ⟶ X₂) (X : CategoryTheory.Arrow C),
  CategoryTheory.MonoidalCategoryStruct.whiskerRight f X =
    (CategoryTheory.MonoidalCategory.Arrow.pushoutProduct.map f).app X
-- Mathlib.Topology.Sheaves.SheafCondition.EqualizerProducts
TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse_obj_pt : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasProducts C] {X : TopCat}
  (F : TopCat.Presheaf C X) {ι : Type v'} (U : ι → TopologicalSpace.Opens ↑X)
  (c : CategoryTheory.Limits.Cone (TopCat.Presheaf.SheafConditionEqualizerProducts.diagram F U)),
  ((TopCat.Presheaf.SheafConditionPairwiseIntersections.coneEquivInverse F U).obj c).pt = c.pt
-- Mathlib.Topology.Connected.PathConnected
/-- The path component of `x` in `F` is the set of points that can be joined to `x` in `F`.  -/
pathComponentIn : {X : Type u_1} → [TopologicalSpace X] → Set X → X → Set X
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NF.oadd_zero : ∀ (e : ONote) (n : ℕ+) [h : e.NF], (e.oadd n 0).NF
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.Slice.intercalateGo_append : ∀ {s t : String} {u : String.Slice} {l : List String.Slice},
  String.Slice.intercalate.go✝ (s ++ t) u l = s ++ String.Slice.intercalate.go✝ t u l
-- Mathlib.LinearAlgebra.Matrix.Hadamard
Matrix.hadamard_one_eq_zero_iff : ∀ {α : Type u_1} {n : Type u_3} [inst : DecidableEq n] [inst_1 : MulZeroOneClass α] {A : Matrix n n α},
  A.hadamard 1 = 0 ↔ A.diag = 0
-- Mathlib.Analysis.InnerProductSpace.Adjoint
LinearMap.adjoint.congr_simp : ∀ {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : InnerProductSpace 𝕜 E] [inst_4 : InnerProductSpace 𝕜 F]
  [inst_5 : FiniteDimensional 𝕜 E] [inst_6 : FiniteDimensional 𝕜 F], LinearMap.adjoint = LinearMap.adjoint
-- Mathlib.Analysis.LocallyConvex.Bounded
Bornology.IsVonNBounded.of_boundedSpace : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : SMul 𝕜 E] [inst_2 : Zero E]
  [inst_3 : TopologicalSpace E] [BoundedSpace 𝕜] {s : Set E}, Bornology.IsVonNBounded 𝕜 s
-- Std.Sync.Channel
/-- Errors that may be thrown while interacting with the channel API.
 -/
Std.CloseableChannel.Error : Type
-- Mathlib.Topology.Order.Category.AlexDisc
/-- Construct a bundled `AlexDisc` from the underlying topological space.  -/
AlexDisc.of : (X : Type u_1) → [inst : TopologicalSpace X] → [AlexandrovDiscrete X] → AlexDisc
-- Mathlib.RingTheory.Finiteness.Cardinality
/-- A module over a finite ring has finite dimension iff it is finite.  -/
Module.finite_iff_finite : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [Finite R],
  Module.Finite R M ↔ Finite M
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.nonUnitalCommRing.eq_1 : ∀ {R : Type u_1} {M : Type u_4} [inst : CommRing R] [inst_1 : CommSemigroup M],
  MonoidAlgebra.nonUnitalCommRing = { toNonUnitalRing := MonoidAlgebra.nonUnitalRing, mul_comm := ⋯ }
-- Mathlib.Algebra.Homology.DerivedCategory.Basic
/-- The localization functor `CochainComplex C ℤ ⥤ DerivedCategory C`.  -/
DerivedCategory.Q : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Abelian C] →
      [inst_2 : HasDerivedCategory C] → CategoryTheory.Functor (CochainComplex C ℤ) (DerivedCategory C)
-- Mathlib.Topology.Order.Compact
instCompactIccSpaceForall : ∀ {ι : Type u_2} {α : ι → Type u_3} [inst : (i : ι) → Preorder (α i)] [inst_1 : (i : ι) → TopologicalSpace (α i)]
  [∀ (i : ι), CompactIccSpace (α i)], CompactIccSpace ((i : ι) → α i)
-- Mathlib.Algebra.Group.Pi.Lemmas
MonoidHom.piMap.eq_1 : ∀ {ι : Type u_1} {M : ι → Type u_3} {N : ι → Type u_4} [inst : (i : ι) → MulOneClass (M i)]
  [inst_1 : (i : ι) → MulOneClass (N i)] (g : (i : ι) → M i →* N i),
  MonoidHom.piMap g = MonoidHom.pi fun i => (g i).comp (Pi.evalMonoidHom M i)
-- Mathlib.Analysis.Normed.Group.Pointwise
add_ball_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (s : Set E), s + Metric.ball 0 δ = Metric.thickening δ s
-- Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity
/-- A subgroup containing all coefficients of all polynomials of a given induction object for
Chevalley's theorem with complexity.

Note that we force `1` to lie in that subgroup so that `fun n ↦ e.coeffSubmodule ^ n` is
increasing.  -/
_private.Mathlib.RingTheory.Spectrum.Prime.ChevalleyComplexity.0.ChevalleyThm.PolynomialC.InductionObj.coeffSubmodule : (R₀ : Type u_1) →
  {R : Type u_2} →
    [inst : CommRing R₀] →
      [inst_1 : CommRing R] →
        [inst_2 : Algebra R₀ R] → {n : ℕ} → ChevalleyThm.PolynomialC.InductionObj✝ R n → Submodule R₀ R
-- Mathlib.Topology.UrysohnsLemma
Urysohns.CU.approx_nonneg : ∀ {X : Type u_1} [inst : TopologicalSpace X] {P : Set X → Set X → Prop} (c : Urysohns.CU P) (n : ℕ) (x : X),
  0 ≤ Urysohns.CU.approx n c x
-- Mathlib.Combinatorics.Quiver.Arborescence
Quiver.shortestPath.congr_simp : ∀ {V : Type u} [inst : Quiver V] (r : V) [inst_1 : Quiver.RootedConnected r] (b : V),
  Quiver.shortestPath r b = Quiver.shortestPath r b
-- Mathlib.Analysis.InnerProductSpace.Orthonormal
/-- A linear combination of some subset of an orthonormal set is orthogonal to other members of the
set.  -/
Orthonormal.inner_finsupp_eq_zero : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {ι : Type u_4} {v : ι → E},
  Orthonormal 𝕜 v →
    ∀ {s : Set ι} {i : ι},
      i ∉ s → ∀ {l : ι →₀ 𝕜}, l ∈ Finsupp.supported 𝕜 𝕜 s → inner 𝕜 ((Finsupp.linearCombination 𝕜 v) l) (v i) = 0
-- Mathlib.Tactic.Attr.Register
/-- Simplification procedure  -/
Parser.Attr.monad_norm_proc : Lean.ParserDescr
-- Mathlib.Data.Sum.Order
Sum.LiftRel.trans : ∀ {α : Type u_1} {β : Type u_2} (r : α → α → Prop) (s : β → β → Prop) [IsTrans α r] [IsTrans β s] {a b c : α ⊕ β},
  Sum.LiftRel r s a b → Sum.LiftRel r s b c → Sum.LiftRel r s a c
-- Mathlib.CategoryTheory.Limits.Cones
/-- Postcomposing a cone by the composite natural transformation `α ≫ β` is the same as
postcomposing by `α` and then by `β`.  -/
CategoryTheory.Limits.Cone.postcomposeComp : {J : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} J] →
    {C : Type u₃} →
      [inst_1 : CategoryTheory.Category.{v₃, u₃} C] →
        {F G H : CategoryTheory.Functor J C} →
          (α : F ⟶ G) →
            (β : G ⟶ H) →
              CategoryTheory.Limits.Cone.postcompose (CategoryTheory.CategoryStruct.comp α β) ≅
                (CategoryTheory.Limits.Cone.postcompose α).comp (CategoryTheory.Limits.Cone.postcompose β)
-- Batteries.Control.Nondet.Basic
/-- Convert a value to the singleton nondeterministic value.  -/
Nondet.singleton : {σ : Type} → {m : Type → Type} → [Monad m] → [inst : Lean.MonadBacktrack σ m] → {α : Type} → α → Nondet m α
-- Batteries.Data.Nat.Basic
/-- Strong recursor via a `Nat`-valued measure
 -/
Nat.strongRecMeasure : {α : Sort u_1} →
  (f : α → ℕ) → {motive : α → Sort u_2} → ((x : α) → ((y : α) → f y < f x → motive y) → motive x) → (x : α) → motive x
-- Mathlib.Order.SupIndep
/-- If the elements of a set are independent, then any pair within that set is disjoint.  -/
iSupIndep.pairwiseDisjoint : ∀ {α : Type u_1} {ι : Type u_3} [inst : CompleteLattice α] {t : ι → α},
  iSupIndep t → Pairwise (Function.onFun Disjoint t)
-- Mathlib.Topology.Instances.ENNReal.Lemmas
ENNReal.continuous_const_mul : ∀ {a : ENNReal}, a ≠ ⊤ → Continuous fun x => a * x
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Basic
ExteriorAlgebra.ι_inj : ∀ (R : Type u1) [inst : CommRing R] {M : Type u2} [inst_1 : AddCommGroup M] [inst_2 : Module R M] (x y : M),
  (ExteriorAlgebra.ι R) x = (ExteriorAlgebra.ι R) y ↔ x = y
-- Init.Data.Int.DivMod.Lemmas
_private.Init.Data.Int.DivMod.Lemmas.0.Int.tdiv.match_1.splitter : (motive : ℤ → ℤ → Sort u_1) →
  (x x_1 : ℤ) →
    ((m n : ℕ) → motive (Int.ofNat m) (Int.ofNat n)) →
      ((m n : ℕ) → motive (Int.ofNat m) (Int.negSucc n)) →
        ((m n : ℕ) → motive (Int.negSucc m) (Int.ofNat n)) →
          ((m n : ℕ) → motive (Int.negSucc m) (Int.negSucc n)) → motive x x_1
-- Init.Data.Fin.Lemmas
Fin.val_add : ∀ {n : ℕ} (a b : Fin n), ↑(a + b) = (↑a + ↑b) % n
-- Lean.Server.Requests
Lean.Server.instMonadLiftEIOExceptionRequestM : MonadLift (EIO Lean.Exception) Lean.Server.RequestM
-- Mathlib.CategoryTheory.LocallyCartesianClosed.ChosenPullbacksAlong
CategoryTheory.ChosenPullbacksAlong.condition_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {Y Z X : C} {f : Y ⟶ X} {g : Z ⟶ X}
  [inst_1 : CategoryTheory.ChosenPullbacksAlong g] {Z_1 : C} (h : X ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.fst f g)
      (CategoryTheory.CategoryStruct.comp f h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.ChosenPullbacksAlong.snd f g)
      (CategoryTheory.CategoryStruct.comp g h)
-- Mathlib.Algebra.Group.Action.Defs
/-- Note that the `IsScalarTower α β β` and `SMulCommClass α β β` typeclass arguments are usually
satisfied by `Algebra α β`.  -/
mul_smul_mul_comm : ∀ {α : Type u_5} {β : Type u_6} [inst : Mul α] [inst_1 : Mul β] [inst_2 : SMul α β] [IsScalarTower α β β]
  [IsScalarTower α α β] [SMulCommClass α β β] (a b : α) (c d : β), (a * b) • (c * d) = a • c * b • d
-- Lean.Meta.Tactic.Grind.EMatch
/-- At `processDelayed`, `lhs` is extracted using `instantiateMVars`. We know it is structurally equal to a term in `assignment`, but
it is not necessarily pointer equal. This can happen when the type of `lhs` depends on previous parameters, and we have a
metavariable application.
If the `lhs` has already been internalized, nothing needs to be done. Otherwise, we traverse the assignment looking for
a term that is structurally equal.
**Note**: If this solution is not robust enough, we should store the original `lhs` when we perform an delayed assignment.
 -/
_private.Lean.Meta.Tactic.Grind.EMatch.0.Lean.Meta.Grind.EMatch.findOriginalGeneralizedPatternLhs : Lean.Expr → OptionT (StateT Lean.Meta.Grind.EMatch.Choice Lean.Meta.Grind.EMatch.M) Lean.Expr
-- Mathlib.CategoryTheory.Triangulated.Subcategory
/-- Given `P : ObjectProperty C` with `C` a pretriangulated category, this
is the property that whenever `X₁ ⟶ X₂ ⟶ X₃ ⟶ X₁⟦1⟧` is a distinguished triangle
such that `P X₁` and `P X₃` hold, then `P.isoClosure X₂` holds.  -/
CategoryTheory.ObjectProperty.IsTriangulatedClosed₂ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroObject C] →
      [inst_2 : CategoryTheory.HasShift C ℤ] →
        [inst_3 : CategoryTheory.Preadditive C] →
          [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] →
            [CategoryTheory.Pretriangulated C] → CategoryTheory.ObjectProperty C → Prop
-- Init.Data.Vector.Algebra
Vector.getElem_hmul : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {n : ℕ} [inst : HMul α β γ] (c : α) (xs : Vector β n) (i : ℕ)
  (h : i < n), (c * xs)[i] = c * xs[i]
-- Init.Data.Repr
ReprTuple.mk : {α : Type u} → (α → List Std.Format → List Std.Format) → ReprTuple α
-- Init.Data.Fin.Lemmas
Fin.addCases.eq_1 : ∀ {m n : ℕ} {motive : Fin (m + n) → Sort u} (left : (i : Fin m) → motive (Fin.castAdd n i))
  (right : (i : Fin n) → motive (Fin.natAdd m i)) (i : Fin (m + n)),
  Fin.addCases left right i = if hi : ↑i < m then ⋯ ▸ left (i.castLT hi) else ⋯ ▸ right (Fin.subNat m (Fin.cast ⋯ i) ⋯)
-- Mathlib.NumberTheory.EulerProduct.DirichletLSeries
/-- When `s.re > 1`, the map `n ↦ χ(n) * n^(-s)` is norm-summable.  -/
summable_dirichletSummand : ∀ {s : ℂ} {N : ℕ} (χ : DirichletCharacter ℂ N) (hs : 1 < s.re), Summable fun n => ‖(dirichletSummandHom χ ⋯) n‖
-- Init.Data.Nat.Coprime
Nat.Coprime.gcd_mul_left_cancel_right : ∀ {k m : ℕ} (n : ℕ), k.Coprime m → m.gcd (k * n) = m.gcd n
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientInfEquivSumNormalizerQuotient.eq_1 : ∀ {G : Type u} [inst : AddGroup G] (H N : AddSubgroup G) (hLE : H ≤ AddSubgroup.normalizer ↑N),
  QuotientAddGroup.quotientInfEquivSumNormalizerQuotient H N hLE =
    (QuotientAddGroup.quotientAddEquivOfEq ⋯).trans
      (QuotientAddGroup.quotientKerEquivOfSurjective
        ((QuotientAddGroup.mk' (N.addSubgroupOf (H ⊔ N))).comp (AddSubgroup.inclusion ⋯)) ⋯)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.Const.toListModel_alterₘ : ∀ {α : Type u} {β : Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α fun x => β},
  Std.DHashMap.Internal.Raw.WFImp ↑m →
    ∀ {a : α} {f : Option β → Option β},
      (Std.DHashMap.Internal.toListModel (↑(Std.DHashMap.Internal.Raw₀.Const.alterₘ m a f)).buckets).Perm
        (Std.Internal.List.Const.alterKey a f (Std.DHashMap.Internal.toListModel (↑m).buckets))