mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Basic
_private.Init.Data.Iterators.Basic.0.Std.Shrink.deflate.eq_1 : ∀ {α : Type u_1} (x : α), Std.Shrink.deflate x = cast ⋯ x
-- Mathlib.Algebra.Homology.BifunctorFlip
HomologicalComplex.ι_mapBifunctorFlipIso_hom : ∀ {C₁ : Type u_1} {C₂ : Type u_2} {D : Type u_3} [inst : CategoryTheory.Category.{v_1, u_1} C₁]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} C₂] [inst_2 : CategoryTheory.Category.{v_3, u_3} D] {I₁ : Type u_4}
  {I₂ : Type u_5} {J : Type u_6} {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms C₁] [inst_4 : CategoryTheory.Limits.HasZeroMorphisms C₂]
  [inst_5 : CategoryTheory.Preadditive D] (K₁ : HomologicalComplex C₁ c₁) (K₂ : HomologicalComplex C₂ c₂)
  (F : CategoryTheory.Functor C₁ (CategoryTheory.Functor C₂ D)) [inst_6 : F.PreservesZeroMorphisms]
  [inst_7 : ∀ (X₁ : C₁), (F.obj X₁).PreservesZeroMorphisms] (c : ComplexShape J) [inst_8 : TotalComplexShape c₁ c₂ c]
  [inst_9 : TotalComplexShape c₂ c₁ c] [inst_10 : TotalComplexShapeSymmetry c₁ c₂ c] [inst_11 : DecidableEq J]
  [inst_12 : K₁.HasMapBifunctor K₂ F c] (i₁ : I₁) (i₂ : I₂) (j : J) (hj : c₂.π c₁ c (i₂, i₁) = j),
  CategoryTheory.CategoryStruct.comp (K₂.ιMapBifunctor K₁ F.flip c i₂ i₁ j hj)
      ((K₁.mapBifunctorFlipIso K₂ F c).hom.f j) =
    c₁.σ c₂ c i₁ i₂ • K₁.ιMapBifunctor K₂ F c i₁ i₂ j ⋯
-- Mathlib.CategoryTheory.SmallRepresentatives
CategoryTheory.CoreSmallCategoryOfSet.smallCategoryOfSet_comp : ∀ {Ω : Type w} {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (h : CategoryTheory.CoreSmallCategoryOfSet Ω C)
  {X Y Z : ↑h.obj} (f : ↑(h.hom X Y)) (g : ↑(h.hom Y Z)),
  h.smallCategoryOfSet.comp f g = h.homEquiv.symm (CategoryTheory.CategoryStruct.comp (h.homEquiv f) (h.homEquiv g))
-- Lean.Meta.Tactic.Try.Collect
_private.Lean.Meta.Tactic.Try.Collect.0.Lean.Meta.Try.collect.unsafe_1 : Lean.MVarId → Lean.Try.Config → Lean.MetaM Lean.Meta.Try.Collector.Result
-- Std.Sat.AIG.Basic
Std.Sat.AIG.Decl.gate.injEq : ∀ {α : Type} (l r l_1 r_1 : Std.Sat.AIG.Fanin),
  (Std.Sat.AIG.Decl.gate l r = Std.Sat.AIG.Decl.gate l_1 r_1) = (l = l_1 ∧ r = r_1)
-- Mathlib.CategoryTheory.Limits.ExactFunctor
/-- A left exact functor is in particular a functor.  -/
CategoryTheory.LeftExactFunctor.forget : (C : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    (D : Type u₂) →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → CategoryTheory.Functor (C ⥤ₗ D) (CategoryTheory.Functor C D)
-- Mathlib.Analysis.Convex.StdSimplex
stdSimplex.barycenter.congr_simp : ∀ {X : Type u_2} [inst : Fintype X] {𝕜 : Type u_5} [inst_1 : Field 𝕜] [inst_2 : LinearOrder 𝕜]
  [inst_3 : IsStrictOrderedRing 𝕜] [inst_4 : Nonempty X], stdSimplex.barycenter = stdSimplex.barycenter
-- Init.Data.Nat.Lemmas
Nat.sub_sub_self : ∀ {n m : ℕ}, m ≤ n → n - (n - m) = m
-- Mathlib.Order.ConditionallyCompleteLattice.Indexed
/-- **Alias** of `cbiInf_eq_ciInf_subtype`. -/
ciInf_subtype' : ∀ {α : Type u_1} {ι : Sort u_4} [inst : ConditionallyCompleteLattice α] {p : ι → Prop} {f : (i : ι) → p i → α},
  BddBelow (Set.range fun i => f ↑i ⋯) → ⨅ i, f ↑i ⋯ ≤ sInf ∅ → ⨅ i, ⨅ (h : p i), f i h = ⨅ x, f ↑x ⋯
-- Mathlib.Data.List.Sublists
List.length_sublistsLen : ∀ {α : Type u} (n : ℕ) (l : List α), (List.sublistsLen n l).length = l.length.choose n
-- Mathlib.Algebra.Quaternion
Quaternion.imJ_ofScientific : ∀ {R : Type u_1} [inst : Field R] (m : ℕ) (s : Bool) (e : ℕ),
  QuaternionAlgebra.imJ (OfScientific.ofScientific m s e) = 0
-- Mathlib.Topology.Algebra.InfiniteSum.ENNReal
ENNReal.hasSum_toReal : ∀ {α : Type u_1} {f : α → ENNReal}, ∑' (x : α), f x ≠ ⊤ → HasSum (fun x => (f x).toReal) (∑' (x : α), (f x).toReal)
-- Mathlib.Algebra.Colimit.DirectLimit
DirectLimit.map₀_add : ∀ {ι : Type u_2} [inst : Preorder ι] {G : ι → Type u_3} {T : ⦃i j : ι⦄ → i ≤ j → Type u_6}
  {f : (x x_1 : ι) → (h : x ≤ x_1) → T h} [inst_1 : (i j : ι) → (h : i ≤ j) → FunLike (T h) (G i) (G j)]
  [inst_2 : DirectedSystem G fun x1 x2 x3 => ⇑(f x1 x2 x3)] [inst_3 : IsDirectedOrder ι] [inst_4 : (i : ι) → Add (G i)]
  [inst_5 : ∀ (i j : ι) (h : i ≤ j), AddHomClass (T h) (G i) (G j)] [inst_6 : Nonempty ι] (r s : (i : ι) → G i),
  DirectLimit.map₀ f (r + s) = DirectLimit.map₀ f r + DirectLimit.map₀ f s
-- Mathlib.Algebra.Homology.Additive
HomologicalComplex.zsmul_f_apply : ∀ {ι : Type u_1} {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Preadditive V]
  {c : ComplexShape ι} {C D : HomologicalComplex V c} (n : ℤ) (f : C ⟶ D) (i : ι), (n • f).f i = n • f.f i
-- Mathlib.CategoryTheory.Limits.Shapes.Preorder.TransfiniteCompositionOfShape
CategoryTheory.TransfiniteCompositionOfShape.map_incl : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {J : Type w} [inst_2 : LinearOrder J] [inst_3 : OrderBot J] {X Y : C} {f : X ⟶ Y} [inst_4 : SuccOrder J]
  [inst_5 : WellFoundedLT J] (c : CategoryTheory.TransfiniteCompositionOfShape J f) (F : CategoryTheory.Functor C D)
  [inst_6 : CategoryTheory.Limits.PreservesWellOrderContinuousOfShape J F]
  [inst_7 : CategoryTheory.Limits.PreservesColimitsOfShape J F],
  (c.map F).incl =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.whiskerRight c.incl F)
      (CategoryTheory.Functor.constComp J Y F).hom
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.toArray_ric_add_add_eq_append : ∀ {m n : ℕ}, (*...=m + n).toArray = (*...m).toArray ++ (m...=m + n).toArray
-- Lean.Meta.Match.MatcherApp.Basic
Lean.Meta.MatcherApp.altNumParams : Lean.Meta.MatcherApp → Array ℕ
-- Std.Data.Iterators.Lemmas.Producers.Slice
Std.Slice.size_eq_count_iter : ∀ {γ : Type u_1} {α β : Type u_2} [inst : Std.ToIterator (Std.Slice γ) Id α β] [inst_1 : Std.Iterator α Id β]
  {s : Std.Slice γ} [Std.Iterators.Finite α Id] [inst_3 : Std.IteratorLoop α Id Id] [Std.LawfulIteratorLoop α Id Id]
  [inst_5 : Std.Slice.SliceSize γ] [Std.Slice.LawfulSliceSize γ], s.size = s.iter.length
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKeyD_insertIfNew : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp] {k : α} {v : β k}
  {fallback : α},
  (t.insertIfNew k v).minKeyD fallback = t.minKey?.elim k fun k' => if cmp k k' = Ordering.lt then k else k'
-- Mathlib.LinearAlgebra.Lagrange
/-- This is the first barycentric form of the Lagrange interpolant.  -/
Lagrange.eval_interpolate_not_at_node : ∀ {F : Type u_1} [inst : Field F] {ι : Type u_2} [inst_1 : DecidableEq ι] {s : Finset ι} {v : ι → F} (r : ι → F)
  {x : F},
  (∀ i ∈ s, x ≠ v i) →
    Polynomial.eval x ((Lagrange.interpolate s v) r) =
      Polynomial.eval x (Lagrange.nodal s v) * ∑ i ∈ s, Lagrange.nodalWeight s v i * (x - v i)⁻¹ * r i
-- Init.Data.Repr
/-- Turns `a` into a `String` using its `Repr` instance, rendering the `Format` at the default width of
120 columns.

The precedence level is initially set to 0.
 -/
reprStr : {α : Type u_1} → [Repr α] → α → String
-- Init.Data.String.Lemmas.Splits
String.Slice.Pos.splits_ofEqAppend : ∀ {s : String.Slice} {t₁ t₂ : String} (h : s.copy = t₁ ++ t₂), (String.Slice.Pos.ofEqAppend h).Splits t₁ t₂
-- Mathlib.LinearAlgebra.AffineSpace.Combination
/-- The value of `weightedVSub`, where the given points are equal and the sum of the weights
is 0.  -/
Finset.weightedVSub_apply_const : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P] {ι : Type u_4} (s : Finset ι) (w : ι → k) (p : P),
  ∑ i ∈ s, w i = 0 → (s.weightedVSub fun x => p) w = 0
-- Mathlib.GroupTheory.SemidirectProduct
SemidirectProduct.right_inl : ∀ {N : Type u_1} {G : Type u_2} [inst : Group N] [inst_1 : Group G] {φ : G →* MulAut N} (n : N),
  (SemidirectProduct.inl n).right = 1
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
/-- The product of a strictly monotone function and a monotone function is strictly monotone.  -/
StrictMono.mul_monotone' : ∀ {α : Type u_1} {β : Type u_2} [inst : Mul α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f g : β → α} [MulLeftMono α]
  [MulRightStrictMono α], StrictMono f → Monotone g → StrictMono fun x => f x * g x
-- Init.Data.List.Sublist
List.IsInfix.trans : ∀ {α : Type u_1} {l₁ l₂ l₃ : List α}, l₁ <:+: l₂ → l₂ <:+: l₃ → l₁ <:+: l₃
-- Aesop.Forward.Match.Types
Aesop.ForwardRuleMatch.mk : Aesop.ForwardRule → Aesop.CompleteMatch → Aesop.ForwardRuleMatch
-- Mathlib.GroupTheory.GroupAction.Jordan
_private.Mathlib.GroupTheory.GroupAction.Jordan.0.Equiv.Perm.alternatingGroup_le_of_isPreprimitive_of_isCycle_mem : {α : Type u_1} →
  {G : Subgroup (Equiv.Perm α)} →
    [inst : Fintype α] →
      [inst_1 : DecidableEq α] →
        MulAction.IsPreprimitive (↥G) α →
          {p : ℕ} →
            Nat.Prime p →
              p + 3 ≤ Nat.card α →
                {g : Equiv.Perm α} → g.IsCycle → g.support.card = p → g ∈ G → ProofWanted (alternatingGroup α ≤ G)
-- Mathlib.NumberTheory.Padics.Hensel
_private.Mathlib.NumberTheory.Padics.Hensel.0.T_def : ∀ {p : ℕ} [inst : Fact (Nat.Prime p)] {R : Type u_1} [inst_1 : CommSemiring R] [inst_2 : Algebra R ℤ_[p]]
  {F : Polynomial R} {a : ℤ_[p]},
  T_gen✝ p F a = ‖(Polynomial.aeval a) F‖ / ‖(Polynomial.aeval a) (Polynomial.derivative F)‖ ^ 2
-- Init.Data.Order.Ord
/-- A typeclass for comparison functions `cmp` for which `cmp a a = .eq` for all `a`.  -/
Std.ReflCmp : {α : Type u} → (α → α → Ordering) → Prop
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.Term.realize.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} (motive : L.Term α → Sort u_4) (l : ℕ) (f : L.Functions l)
  (ts : Fin l → L.Term α) (h_1 : (k : α) → motive (FirstOrder.Language.var k))
  (h_2 : (l : ℕ) → (f : L.Functions l) → (ts : Fin l → L.Term α) → motive (FirstOrder.Language.func f ts)),
  (match FirstOrder.Language.func f ts with
    | FirstOrder.Language.var k => h_1 k
    | FirstOrder.Language.func f ts => h_2 l f ts) =
    h_2 l f ts
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.instMin : {R : Type u} →
  {L : Type v} → [inst : CommRing R] → [inst_1 : LieRing L] → [inst_2 : LieAlgebra R L] → Min (LieSubalgebra R L)
-- Mathlib.RingTheory.Coalgebra.Hom
CoalgHom.id_apply : ∀ (R : Type u_1) (A : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid A] [inst_2 : Module R A]
  [inst_3 : CoalgebraStruct R A] (x : A), (CoalgHom.id R A) x = x
-- Mathlib.Data.Seq.Computation
Computation.destruct_eq_think : ∀ {α : Type u} {s s' : Computation α}, s.destruct = Sum.inr s' → s = s'.think
-- Lean.Data.Name
Lean.Name.components : Lean.Name → List Lean.Name
-- Mathlib.Analysis.Calculus.ContDiff.Basic
contDiffAt_id : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {n : WithTop ℕ∞} {x : E}, ContDiffAt 𝕜 n id x
-- Mathlib.Analysis.Calculus.VectorField
/-- The pullback within a set of a vector field under a function, defined
as `(f^* V) (x) = Df(x)^{-1} (V (f x))` where `Df(x)` is the derivative of `f` within `s`.
If `Df(x)` is not invertible, we use the junk value `0`.
 -/
VectorField.pullbackWithin : (𝕜 : Type u_1) →
  [inst : NontriviallyNormedField 𝕜] →
    {E : Type u_2} →
      [inst_1 : NormedAddCommGroup E] →
        [NormedSpace 𝕜 E] →
          {F : Type u_3} → [inst_3 : NormedAddCommGroup F] → [NormedSpace 𝕜 F] → (E → F) → (F → F) → Set E → E → E
-- Mathlib.CategoryTheory.Limits.Comma
CategoryTheory.Arrow.hasColimits : ∀ {T : Type u₃} [inst : CategoryTheory.Category.{v₃, u₃} T] [CategoryTheory.Limits.HasColimits T],
  CategoryTheory.Limits.HasColimits (CategoryTheory.Arrow T)
-- Mathlib.Analysis.Calculus.FormalMultilinearSeries
_private.Mathlib.Analysis.Calculus.FormalMultilinearSeries.0.FormalMultilinearSeries.removeZero.match_1.eq_2 : ∀ (motive : ℕ → Sort u_1) (n : ℕ) (h_1 : Unit → motive 0) (h_2 : (n : ℕ) → motive n.succ),
  (match n.succ with
    | 0 => h_1 ()
    | n.succ => h_2 n) =
    h_2 n
-- Mathlib.CategoryTheory.Monoidal.Mon
/-- The addition morphism of an additive monoid object.  -/
CategoryTheory.AddMonObj.«termσ[_]» : Lean.ParserDescr
-- Mathlib.Algebra.Category.Grp.Limits
/-- The forgetful functor from commutative groups to commutative monoids preserves all limits.
(That is, the underlying commutative monoids could have been computed instead as limits
in the category of commutative monoids.)
 -/
CommGrpCat.forget₂CommMon_preservesLimitsOfSize : ∀ [UnivLE.{v, u}],
  CategoryTheory.Limits.PreservesLimitsOfSize.{w, v, u, u, u + 1, u + 1} (CategoryTheory.forget₂ CommGrpCat CommMonCat)
-- Mathlib.Algebra.Group.Torsion
/-- Alias of `zsmul_right_inj`, for ease of discovery alongside `zsmul_le_zsmul_iff'`
and `zsmul_lt_zsmul_iff'`.  -/
zsmul_eq_zsmul_iff' : ∀ {G : Type u_2} [inst : AddGroup G] [IsAddTorsionFree G] {n : ℤ} {a b : G}, n ≠ 0 → (n • a = n • b ↔ a = b)
-- Mathlib.CategoryTheory.MorphismProperty.Representable
CategoryTheory.Functor.relativelyRepresentable.pullback₃.map_p₁_comp_assoc : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} [inst_2 : F.Full] {A₁ A₂ A₃ : C} {X : D} {f₁ : F.obj A₁ ⟶ X}
  (hf₁ : F.relativelyRepresentable f₁) (f₂ : F.obj A₂ ⟶ X) (f₃ : F.obj A₃ ⟶ X)
  [inst_3 : CategoryTheory.Limits.HasPullback (hf₁.fst' f₂) (hf₁.fst' f₃)] {Z : D} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.Functor.relativelyRepresentable.pullback₃.p₁ hf₁ f₂ f₃))
      (CategoryTheory.CategoryStruct.comp f₁ h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Functor.relativelyRepresentable.pullback₃.π hf₁ f₂ f₃) h
-- Mathlib.Topology.VectorBundle.Riemannian
/-- Given two continuous maps into the same fibers of a continuous Riemannian bundle,
their inner product is continuous. Version with `ContinuousAt`.  -/
ContinuousAt.inner_bundle : ∀ {B : Type u_1} [inst : TopologicalSpace B] {F : Type u_2} [inst_1 : NormedAddCommGroup F] [inst_2 : NormedSpace ℝ F]
  {E : B → Type u_3} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : (x : B) → NormedAddCommGroup (E x)]
  [inst_5 : (x : B) → InnerProductSpace ℝ (E x)] [inst_6 : FiberBundle F E] [inst_7 : VectorBundle ℝ F E] {M : Type u_4}
  [inst_8 : TopologicalSpace M] [h : IsContinuousRiemannianBundle F E] {b : M → B} {v w : (x : M) → E (b x)} {x : M},
  ContinuousAt (fun m => ⟨b m, v m⟩) x →
    ContinuousAt (fun m => ⟨b m, w m⟩) x → ContinuousAt (fun b_1 => inner ℝ (v b_1) (w b_1)) x
-- Mathlib.Data.DFinsupp.BigOperators
DFinsupp.liftAddHom_symm_apply : ∀ {ι : Type u} {γ : Type w} {β : ι → Type v} [inst : DecidableEq ι] [inst_1 : (i : ι) → AddZeroClass (β i)]
  [inst_2 : AddCommMonoid γ] (F : (Π₀ (i : ι), β i) →+ γ) (i : ι),
  DFinsupp.liftAddHom.symm F i = F.comp (DFinsupp.singleAddHom β i)
-- Mathlib.AlgebraicGeometry.EllipticCurve.Projective.Point
WeierstrassCurve.Projective.Point.toAffineLift_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Projective F},
  WeierstrassCurve.Projective.Point.toAffineLift 0 = 0
-- Mathlib.CategoryTheory.Comma.Arrow
/-- `homMk''` is the dual of `homMk`, which we need for `to_dual`.
Please avoid using this directly.  -/
CategoryTheory.Arrow.homMk'' : {T : Type u} →
  [inst : CategoryTheory.Category.{v, u} T] →
    {f g : CategoryTheory.Arrow T} →
      (u : g.right ⟶ f.right) →
        (v : g.left ⟶ f.left) →
          autoParam (CategoryTheory.CategoryStruct.comp g.hom u = CategoryTheory.CategoryStruct.comp v f.hom)
              CategoryTheory.Arrow.homMk''._auto_1 →
            (g ⟶ f)
-- Mathlib.Algebra.Lie.Free
/-- The quotient map as a `NonUnitalAlgHom`.  -/
FreeLieAlgebra.mk : (R : Type u) →
  {X : Type v} → [inst : CommRing R] → FreeNonUnitalNonAssocAlgebra R X →ₙₐ[R] CommutatorRing (FreeLieAlgebra R X)
-- Mathlib.RingTheory.Polynomial.Chebyshev
Polynomial.Chebyshev.add_one_mul_self_mul_T_eq_poly_in_T : ∀ {R : Type u_1} [inst : CommRing R] (n : ℤ),
  (↑n + 1) * ↑n * Polynomial.Chebyshev.T R (n + 1) =
    ↑n * Polynomial.X * Polynomial.derivative (Polynomial.Chebyshev.T R (n + 1)) -
      (↑n + 1) * Polynomial.derivative (Polynomial.Chebyshev.T R n)
-- Mathlib.Algebra.Module.Submodule.Ker
LinearEquiv.ker_comp : ∀ {R : Type u_1} {R₂ : Type u_2} {R₃ : Type u_3} {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₃] {module_M : Module R M} {module_M₂ : Module R₂ M₂} {module_M₃ : Module R₃ M₃}
  {σ₁₂ : R →+* R₂} {σ₂₃ : R₂ →+* R₃} {σ₁₃ : R →+* R₃} [inst_6 : RingHomCompTriple σ₁₂ σ₂₃ σ₁₃] {σ₃₂ : R₃ →+* R₂}
  {re₂₃ : RingHomInvPair σ₂₃ σ₃₂} {re₃₂ : RingHomInvPair σ₃₂ σ₂₃} (e'' : M₂ ≃ₛₗ[σ₂₃] M₃) (l : M →ₛₗ[σ₁₂] M₂),
  (↑e'' ∘ₛₗ l).ker = l.ker
-- Std.Data.DTreeMap.Raw.Basic
/-- Tries to retrieve the key-value pair with the largest key in the tree map, panicking if the map is
empty.
 -/
Std.DTreeMap.Raw.Const.maxEntry! : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Inhabited (α × β)] → Std.DTreeMap.Raw α (fun x => β) cmp → α × β
-- Mathlib.Algebra.Category.ModuleCat.ChangeOfRings
ModuleCat.restrictScalarsId'App_inv_naturality : ∀ {R : Type u₁} [inst : Ring R] (f : R →+* R) (hf : f = RingHom.id R) {M N : ModuleCat R} (φ : M ⟶ N),
  CategoryTheory.CategoryStruct.comp φ (ModuleCat.restrictScalarsId'App f hf N).inv =
    CategoryTheory.CategoryStruct.comp (ModuleCat.restrictScalarsId'App f hf M).inv
      ((ModuleCat.restrictScalars f).map φ)
-- Mathlib.Order.CompleteLattice.Defs
ofDual_iInf : ∀ {α : Type u_1} {ι : Sort u_4} [inst : SupSet α] (f : ι → αᵒᵈ),
  OrderDual.ofDual (⨅ i, f i) = ⨆ i, OrderDual.ofDual (f i)
-- Mathlib.Computability.StateTransition
StateTransition.FRespects.eq_1 : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} (f₂ : σ₂ → Option σ₂) (tr : σ₁ → σ₂) (a₂ : σ₂) (b₁ : σ₁),
  StateTransition.FRespects f₂ tr a₂ (some b₁) = StateTransition.Reaches₁ f₂ a₂ (tr b₁)
-- Mathlib.Tactic.Translate.ToDual
/-- Environment extension used for guessing the translation of a name.  -/
Mathlib.Tactic.ToDual.guessNameExt : Mathlib.Tactic.GuessName.GuessNameExt
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Terminal
/-- Preserving the terminal object implies preserving all limits of the empty diagram.  -/
CategoryTheory.Limits.preservesLimitsOfShape_pempty_of_preservesTerminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (G : CategoryTheory.Functor C D) [CategoryTheory.Limits.PreservesLimit (CategoryTheory.Functor.empty C) G],
  CategoryTheory.Limits.PreservesLimitsOfShape (CategoryTheory.Discrete PEmpty.{1}) G
-- Mathlib.Topology.ContinuousMap.Bounded.Normed
BoundedContinuousFunction.coe_zsmulRec : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : SeminormedAddCommGroup β]
  (f : BoundedContinuousFunction α β) (z : ℤ), ⇑(zsmulRec (fun x1 x2 => x1 • x2) z f) = z • ⇑f
-- Mathlib.CategoryTheory.Limits.Shapes.End
CategoryTheory.Limits.multispanShapeCoend_R : ∀ (J : Type u) [inst : CategoryTheory.Category.{v, u} J], (CategoryTheory.Limits.multispanShapeCoend J).R = J
-- Mathlib.LinearAlgebra.RootSystem.Base
RootPairing.Base.isPos_of_mem_support : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] {P : RootPairing ι R M N} {b : P.Base}
  [inst_5 : CharZero R] {i : ι}, i ∈ b.support → b.IsPos i
-- Mathlib.Geometry.Manifold.IsManifold.ExtChartAt
/-- If we're boundaryless, `(extChartAt I x).target` is a neighborhood of any of its points  -/
extChartAt_target_mem_nhds' : ∀ {𝕜 : Type u_1} {E : Type u_2} {M : Type u_3} {H : Type u_4} [inst : NontriviallyNormedField 𝕜]
  [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace 𝕜 E] [inst_3 : TopologicalSpace H] [inst_4 : TopologicalSpace M]
  {I : ModelWithCorners 𝕜 E H} [inst_5 : ChartedSpace H M] [I.Boundaryless] {x : M} {y : E},
  y ∈ (extChartAt I x).target → (extChartAt I x).target ∈ nhds y
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Udiv
Std.Tactic.BVDecide.BVExpr.bitblast.blastUdiv.BlastUdivOutput.mk.sizeOf_spec : ∀ {α : Type} [inst : Hashable α] [inst_1 : DecidableEq α] {old : Std.Sat.AIG α} {w : ℕ} [inst_2 : SizeOf α]
  (aig : Std.Sat.AIG α) (q r : aig.RefVec w) (hle : old.decls.size ≤ aig.decls.size),
  sizeOf { aig := aig, q := q, r := r, hle := hle } = 1 + sizeOf aig + sizeOf q + sizeOf r + sizeOf hle
-- Mathlib.Order.Interval.Set.LinearOrder
Set.Ioc_union_Ioc : ∀ {α : Type u_1} [inst : LinearOrder α] {a b c d : α},
  min a b ≤ max c d → min c d ≤ max a b → Set.Ioc a b ∪ Set.Ioc c d = Set.Ioc (min a c) (max b d)
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- Register the equational theorems for the given definition.  -/
Lean.Meta.SimpTheorems.registerDeclToUnfoldThms : Lean.Meta.SimpTheorems → Lean.Name → Array Lean.Name → Lean.Meta.SimpTheorems
-- Mathlib.Topology.Homeomorph.Lemmas
IsHomeomorph.isQuotientMap : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y] {f : X → Y},
  IsHomeomorph f → Topology.IsQuotientMap f
-- Mathlib.Algebra.Polynomial.Splits
Polynomial.splits_iff_exists_multiset : ∀ {R : Type u_1} [inst : CommRing R] {f : Polynomial R},
  f.Splits ↔ ∃ m, f = Polynomial.C f.leadingCoeff * (Multiset.map (fun x => Polynomial.X - Polynomial.C x) m).prod
-- Mathlib.Geometry.Manifold.VectorBundle.Tangent
tangentBundleModelSpaceHomeomorph_coe_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_4} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H},
  ⇑(tangentBundleModelSpaceHomeomorph I).symm = ⇑(Bundle.TotalSpace.toProd H E).symm
-- Mathlib.LinearAlgebra.Matrix.Defs
Matrix.addSemigroup : {m : Type u_2} → {n : Type u_3} → {α : Type v} → [AddSemigroup α] → AddSemigroup (Matrix m n α)
-- Mathlib.CategoryTheory.Triangulated.Triangulated
CategoryTheory.Triangulated.Octahedron.triangleMorphism₂_hom₃ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} 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]
  {X₁ X₂ X₃ Z₁₂ Z₂₃ Z₁₃ : C} {u₁₂ : X₁ ⟶ X₂} {u₂₃ : X₂ ⟶ X₃} {u₁₃ : X₁ ⟶ X₃}
  {comm : CategoryTheory.CategoryStruct.comp u₁₂ u₂₃ = u₁₃} {v₁₂ : X₂ ⟶ Z₁₂}
  {w₁₂ : Z₁₂ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₂ : CategoryTheory.Pretriangulated.Triangle.mk u₁₂ v₁₂ w₁₂ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₂₃ : X₃ ⟶ Z₂₃} {w₂₃ : Z₂₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₂}
  {h₂₃ : CategoryTheory.Pretriangulated.Triangle.mk u₂₃ v₂₃ w₂₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  {v₁₃ : X₃ ⟶ Z₁₃} {w₁₃ : Z₁₃ ⟶ (CategoryTheory.shiftFunctor C 1).obj X₁}
  {h₁₃ : CategoryTheory.Pretriangulated.Triangle.mk u₁₃ v₁₃ w₁₃ ∈ CategoryTheory.Pretriangulated.distinguishedTriangles}
  (h : CategoryTheory.Triangulated.Octahedron comm h₁₂ h₂₃ h₁₃), h.triangleMorphism₂.hom₃ = h.m₃
-- Std.Data.HashSet.DecidableEquiv
Std.HashSet.instDecidableEquivOfLawfulBEq : {α : Type u} →
  [inst : BEq α] → [LawfulBEq α] → [inst_2 : Hashable α] → (m₁ m₂ : Std.HashSet α) → Decidable (m₁.Equiv m₂)
-- Mathlib.Analysis.LocallyConvex.Bounded
/-- If a topology `t'` is coarser than `t`, then any set `s` that is bounded with respect to
`t` is bounded with respect to `t'`.  -/
Bornology.IsVonNBounded.of_topologicalSpace_le : ∀ {𝕜 : Type u_1} {E : Type u_3} [inst : SeminormedRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  {t t' : TopologicalSpace E}, t ≤ t' → ∀ {s : Set E}, Bornology.IsVonNBounded 𝕜 s → Bornology.IsVonNBounded 𝕜 s
-- Mathlib.SetTheory.Cardinal.Basic
Cardinal.powerlt_min : ∀ {a b c : Cardinal.{u_1}}, a ^< min b c = min (a ^< b) (a ^< c)
-- Mathlib.RingTheory.PowerSeries.Basic
PowerSeries.mul_X_injective : ∀ {R : Type u_1} [inst : Semiring R], Function.Injective fun x => x * PowerSeries.X
-- Mathlib.FieldTheory.RatFunc.Luroth
/-- A choice of coefficient index `i` such that `φ.coeff i` is not in `K`.  -/
_private.Mathlib.FieldTheory.RatFunc.Luroth.0.RatFunc.Luroth.generatorIndex : {K : Type u_1} → [inst : Field K] → {E : IntermediateField K (RatFunc K)} → E ≠ ⊥ → ℕ