mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Shapes.Kernels
/-- Every kernel of `f ≫ g` is also a kernel of `f`, as long as `c.ι ≫ f` vanishes.  -/
CategoryTheory.Limits.isKernelOfComp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {f : X ⟶ Y} →
          {W : C} →
            (g : Y ⟶ W) →
              (h : X ⟶ W) →
                {c : CategoryTheory.Limits.KernelFork h} →
                  CategoryTheory.Limits.IsLimit c →
                    (hf : CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Fork.ι c) f = 0) →
                      CategoryTheory.CategoryStruct.comp f g = h →
                        CategoryTheory.Limits.IsLimit
                          (CategoryTheory.Limits.KernelFork.ofι (CategoryTheory.Limits.Fork.ι c) hf)
-- Mathlib.Data.Set.Image
Set.range_id : ∀ {α : Type u_1}, Set.range id = Set.univ
-- Mathlib.Data.Set.Function
Set.BijOn.sdiff_singleton : ∀ {α : Type u_1} {β : Type u_2} {s : Set α} {t : Set β} {f : α → β} {a : α},
  Set.BijOn f s t → a ∈ s → Set.BijOn f (s \ {a}) (t \ {f a})
-- Mathlib.Algebra.Lie.SemiDirect
/-- The canonical projection of the semi-direct sum K ⋊⁅ψ⁆ L to G.  -/
LieAlgebra.SemiDirectSum.projr : {R : Type u_1} →
  [inst : CommRing R] →
    {K : Type u_2} →
      [inst_1 : LieRing K] →
        [inst_2 : LieAlgebra R K] →
          {L : Type u_3} →
            [inst_3 : LieRing L] → [inst_4 : LieAlgebra R L] → (ψ : L →ₗ⁅R⁆ LieDerivation R K K) → K ⋊⁅ψ⁆ L →ₗ⁅R⁆ L
-- Init.Data.SInt.Lemmas
Int64.add_eq_left : ∀ {a b : Int64}, a + b = a ↔ b = 0
-- Mathlib.Algebra.Homology.Additive
CategoryTheory.Functor.mapHomologicalComplex_reflects_iso : ∀ {ι : Type u_1} (W₁ : Type u_3) {W₂ : Type u_4} [inst : CategoryTheory.Category.{v_2, u_3} W₁]
  [inst_1 : CategoryTheory.Category.{v_3, u_4} W₂] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms W₁]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms W₂] (F : CategoryTheory.Functor W₁ W₂)
  [inst_4 : F.PreservesZeroMorphisms] [F.ReflectsIsomorphisms] (c : ComplexShape ι),
  (F.mapHomologicalComplex c).ReflectsIsomorphisms
-- Init.Data.Int.Linear
Int.Internal.Linear.orOver_resolve : ∀ {n : ℕ} {p : ℕ → Prop}, Int.Internal.Linear.OrOver (n + 1) p → ¬p n → Int.Internal.Linear.OrOver n p
-- Mathlib.Topology.Separation.Hausdorff
Continuous.limUnder_eq : ∀ {X : Type u_1} {Y : Type u_2} [inst : TopologicalSpace X] [T2Space X] [inst_2 : TopologicalSpace Y] {f : Y → X},
  Continuous f → ∀ (y : Y), (nhds y).limUnder f = f y
-- Mathlib.Algebra.Order.Group.Synonym
ofDual_vadd' : ∀ {β : Type u_2} {α : Type u_1} [inst : VAdd β α] (b : βᵒᵈ) (a : α), OrderDual.ofDual b +ᵥ a = b +ᵥ a
-- Std.Data.String.ToInt
_private.Std.Data.String.ToInt.0.String.Slice.toInt?.eq_1 : ∀ (s : String.Slice),
  s.toInt? =
    match s.dropPrefix? '-' with
    | some rest => Option.map Int.negOfNat rest.toNat?
    | none => Option.map Int.ofNat s.toNat?
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
/-- Lax unity.  -/
CategoryTheory.Lax.StrongTrans.naturality_id_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.LaxFunctor B C} (self : CategoryTheory.Lax.StrongTrans F G) (a : B) {Z : F.obj a ⟶ G.obj a}
  (h : CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.CategoryStruct.id a)) (self.app a) ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerLeft (self.app a) (G.mapId a))
      (CategoryTheory.CategoryStruct.comp (self.naturality (CategoryTheory.CategoryStruct.id a)).hom h) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.rightUnitor (self.app a)).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.leftUnitor (self.app a)).inv
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (F.mapId a) (self.app a)) h))
-- Mathlib.RingTheory.Polynomial.Pochhammer
Nat.cast_choose_eq_descPochhammer_div : ∀ (K : Type u_1) [inst : DivisionRing K] [CharZero K] (a b : ℕ),
  ↑(a.choose b) = Polynomial.eval (↑a) (descPochhammer K b) / ↑b.factorial
-- Mathlib.Topology.Algebra.Group.Pointwise
subset_interior_mul_right : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Group α] [ContinuousConstSMul α α] {s t : Set α},
  s * interior t ⊆ interior (s * t)
-- Mathlib.Order.Filter.Basic
Filter.iInf_neBot_iff_of_directed' : ∀ {α : Type u} {ι : Sort x} {f : ι → Filter α} [Nonempty ι],
  Directed (fun x1 x2 => x1 ≥ x2) f → ((iInf f).NeBot ↔ ∀ (i : ι), (f i).NeBot)
-- Std.Data.DHashMap.Lemmas
Std.DHashMap.Const.getD_eq_fallback : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m : Std.DHashMap α fun x => β} [EquivBEq α]
  [LawfulHashable α] {a : α} {fallback : β}, a ∉ m → Std.DHashMap.Const.getD m a fallback = fallback
-- Mathlib.Algebra.Order.Ring.Idempotent
instOrderTopSubtypeIsIdempotentElem : {M : Type u_2} → [inst : CommMonoid M] → OrderTop { a // IsIdempotentElem a }
-- Mathlib.Topology.VectorBundle.Basic
VectorBundleCore.localTrivAt_apply : ∀ {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} (Z : VectorBundleCore R B F ι)
  (p : Z.TotalSpace), ↑(Z.localTrivAt p.proj) p = (p.proj, p.snd)
-- Init.Data.Range.Polymorphic.SInt
_private.Init.Data.Range.Polymorphic.SInt.0.Int16.instLawfulUpwardEnumerableLE : Std.PRange.LawfulUpwardEnumerableLE Int16
-- Mathlib.Geometry.Manifold.ContMDiff.Defs
contMDiffAt_iff_source_of_mem_source : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {H : Type u_3} [inst_3 : TopologicalSpace H] {I : ModelWithCorners 𝕜 E H} {M : Type u_4}
  [inst_4 : TopologicalSpace M] [inst_5 : ChartedSpace H M] {E' : Type u_5} [inst_6 : NormedAddCommGroup E']
  [inst_7 : NormedSpace 𝕜 E'] {H' : Type u_6} [inst_8 : TopologicalSpace H'] {I' : ModelWithCorners 𝕜 E' H'}
  {M' : Type u_7} [inst_9 : TopologicalSpace M'] [inst_10 : ChartedSpace H' M'] {f : M → M'} {x x' : M} {n : WithTop ℕ∞}
  [IsManifold I n M],
  x' ∈ (chartAt H x).source →
    (ContMDiffAt I I' n f x' ↔
      ContMDiffWithinAt (modelWithCornersSelf 𝕜 E) I' n (f ∘ ↑(extChartAt I x).symm) (Set.range ↑I)
        (↑(extChartAt I x) x'))
-- Mathlib.Combinatorics.Matroid.Loop
Matroid.closure_insert_isColoop_eq : ∀ {α : Type u_1} {M : Matroid α} {e : α} (X : Set α), M.IsColoop e → M.closure (insert e X) = insert e (M.closure X)
-- Lean.Meta.Tactic.Grind.EqResolution
Lean.Meta.Grind.TopSort.State.result : Lean.Meta.Grind.TopSort.State → Array Lean.Expr
-- Mathlib.CategoryTheory.Groupoid.FreeGroupoidOfCategory
CategoryTheory.FreeGroupoid.lift_comp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {G : Type u₁} [inst_1 : CategoryTheory.Groupoid G]
  {H : Type u₂} [inst_2 : CategoryTheory.Groupoid H] (φ : CategoryTheory.Functor C G) (ψ : CategoryTheory.Functor G H),
  CategoryTheory.FreeGroupoid.lift (φ.comp ψ) = (CategoryTheory.FreeGroupoid.lift φ).comp ψ
-- Init.System.IO
IO.Process.Stdio.inherit.sizeOf_spec : sizeOf IO.Process.Stdio.inherit = 1
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
_private.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.0.Lean.PrettyPrinter.Delaborator.TopDownAnalyze.analyzeAppStagedCore.analyzeFn : Lean.PrettyPrinter.Delaborator.TopDownAnalyze.AnalyzeAppM Unit
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.pow_subset_pow_right : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Monoid α] {s : Finset α} {m n : ℕ}, 1 ∈ s → m ≤ n → s ^ m ⊆ s ^ n
-- Mathlib.AlgebraicTopology.SimplexCategory.GeneratorsRelations.Basic
FreeSimplexQuiver.homRel.δ_comp_σ_of_le : ∀ {n : ℕ} {i : Fin (n + 2)} {j : Fin (n + 1)},
  i ≤ j.castSucc →
    FreeSimplexQuiver.homRel
      (CategoryTheory.CategoryStruct.comp
        ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i.castSucc))
        ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j.succ)))
      (CategoryTheory.CategoryStruct.comp ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.σ j))
        ((CategoryTheory.Paths.of FreeSimplexQuiver).map (FreeSimplexQuiver.δ i)))
-- Mathlib.AlgebraicGeometry.Spec
/-- The induced map of a ring homomorphism on the ring spectra, as a morphism of sheafed spaces.
 -/
AlgebraicGeometry.Spec.sheafedSpaceMap : {R S : CommRingCat} → (R ⟶ S) → (AlgebraicGeometry.Spec.sheafedSpaceObj S ⟶ AlgebraicGeometry.Spec.sheafedSpaceObj R)
-- Mathlib.Algebra.Order.Group.Abs
min_abs_abs_le_abs_min : ∀ {G : Type u_1} [inst : AddCommGroup G] [inst_1 : LinearOrder G] {a b : G}, min |a| |b| ≤ |min a b|
-- Mathlib.Analysis.InnerProductSpace.PiL2
FiniteDimensional.orthonormalBasisSingleton_repr_apply : ∀ {ι : Type u_1} {𝕜 : Type u_3} [inst : RCLike 𝕜] {E : Type u_4} [inst_1 : NormedAddCommGroup E]
  [inst_2 : InnerProductSpace 𝕜 E] [inst_3 : Fintype ι] [inst_4 : Unique ι] (h : Module.finrank 𝕜 E = 1) {v : E}
  (hv : ‖v‖ = 1) (w : E),
  (FiniteDimensional.orthonormalBasisSingleton ι 𝕜 h v hv).repr w = EuclideanSpace.single default (inner 𝕜 v w)
-- Init.Data.String.Substring
_private.Init.Data.String.Substring.0.Substring.Raw.nextn.match_1.eq_2 : ∀ (motive : Substring.Raw → ℕ → String.Pos.Raw → Sort u_1) (ss : Substring.Raw) (i : ℕ) (p : String.Pos.Raw)
  (h_1 : (x : Substring.Raw) → (p : String.Pos.Raw) → motive x 0 p)
  (h_2 : (ss : Substring.Raw) → (i : ℕ) → (p : String.Pos.Raw) → motive ss i.succ p),
  (match ss, i.succ, p with
    | x, 0, p => h_1 x p
    | ss, i.succ, p => h_2 ss i p) =
    h_2 ss i p
-- Init.Data.UInt.Bitwise
UInt64.not_not : ∀ {a : UInt64}, ~~~~~~a = a
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.mk_eq_mk : ∀ {R : Type u} [inst : Ring R] {I : Ideal R} [inst_1 : I.IsTwoSided] (x : R),
  Submodule.Quotient.mk x = (Ideal.Quotient.mk I) x
-- Mathlib.Algebra.Field.Subfield.Basic
Subfield.coe_sSup_of_directedOn : ∀ {K : Type u} [inst : DivisionRing K] {S : Set (Subfield K)},
  S.Nonempty → DirectedOn (fun x1 x2 => x1 ≤ x2) S → ↑(sSup S) = ⋃ s ∈ S, ↑s
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctor.toStrictlyUnitaryPseudofunctor : {B : Type u₁} →
  [inst : CategoryTheory.Bicategory B] →
    {C : Type u₂} →
      [inst_1 : CategoryTheory.Bicategory C] →
        CategoryTheory.StrictPseudofunctor B C → CategoryTheory.StrictlyUnitaryPseudofunctor B C
-- Mathlib.Analysis.Asymptotics.Defs
Asymptotics.isBigOWith_abs_right : ∀ {α : Type u_1} {E : Type u_3} [inst : Norm E] {c : ℝ} {f : α → E} {l : Filter α} {u : α → ℝ},
  (Asymptotics.IsBigOWith c l f fun x => |u x|) ↔ Asymptotics.IsBigOWith c l f u
-- Mathlib.CategoryTheory.Sites.NonabelianCohomology.H1
CategoryTheory.PresheafOfGroups.Cochain₀.one_apply : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (G : CategoryTheory.Functor Cᵒᵖ GrpCat) {I : Type w'}
  (U : I → C) (i : I), 1 i = 1
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.mul_def : ∀ {R : Type u_1} [inst : Semiring R] {f g : SkewPolynomial R} [inst_1 : MulSemiringAction (Multiplicative ℕ) R],
  f * g = f.sum fun a₁ b₁ => g.sum fun a₂ b₂ => (SkewPolynomial.monomial (a₁ + a₂)) (b₁ * (⇑SkewPolynomial.φ)^[a₁] b₂)
-- Mathlib.LinearAlgebra.SymplecticGroup
SymplecticGroup.inv_left_mul_aux : ∀ {l : Type u_1} {R : Type u_2} [inst : DecidableEq l] [inst_1 : Fintype l] [inst_2 : CommRing R]
  {A : Matrix (l ⊕ l) (l ⊕ l) R}, A ∈ Matrix.symplecticGroup l R → -(Matrix.J l R * A.transpose * Matrix.J l R * A) = 1
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.InlayHintOptions.mk.inj : ∀ {toWorkDoneProgressOptions : Lean.Lsp.WorkDoneProgressOptions} {resolveProvider? : Option Bool}
  {toWorkDoneProgressOptions_1 : Lean.Lsp.WorkDoneProgressOptions} {resolveProvider?_1 : Option Bool},
  { toWorkDoneProgressOptions := toWorkDoneProgressOptions, resolveProvider? := resolveProvider? } =
      { toWorkDoneProgressOptions := toWorkDoneProgressOptions_1, resolveProvider? := resolveProvider?_1 } →
    toWorkDoneProgressOptions = toWorkDoneProgressOptions_1 ∧ resolveProvider? = resolveProvider?_1
-- Mathlib.Algebra.Order.Archimedean.Class
/-- Create a `MulArchimedeanOrder` element from the underlying type.  -/
MulArchimedeanOrder.of : {M : Type u_1} → M ≃ MulArchimedeanOrder M
-- Lean.Meta.LazyDiscrTree
Lean.Meta.LazyDiscrTree.Cache : Type
-- Mathlib.CategoryTheory.Subobject.Classifier.Defs
/-- A monomorphism `truth : Ω₀ ⟶ Ω` is a subobject classifier if, for every monomorphism
`m : U ⟶ X` in `C`, there is a unique map `χ : X ⟶ Ω` such that for some (necessarily unique)
`χ₀ : U ⟶ Ω₀` the following square is a pullback square:
```
      U ---------m----------> X
      |                       |
    χ₀ U                     χ m
      |                       |
      v                       v
      Ω₀ ------truth--------> Ω
```
An equivalent formulation replaces `Ω₀` with the terminal object.
 -/
CategoryTheory.Subobject.Classifier : (C : Type u) → [CategoryTheory.Category.{v, u} C] → Type (max u v)
-- Mathlib.LinearAlgebra.FreeModule.ModN
/-- Given a free module `G` over `ℤ`, construct the corresponding basis
of `G / ⟨n⟩` over `ℤ / nℤ`.  -/
ModN.basis : {G : Type u_1} →
  [inst : AddCommGroup G] →
    {n : ℕ} → [NeZero n] → {ι : Type u_4} → Module.Basis ι ℤ G → Module.Basis ι (ZMod n) (ModN G n)
-- Batteries.Data.List.Basic
/-- Auxiliary for `tailsTR`: `tailsTR.go l acc = acc.toList ++ tails l`.  -/
List.tailsTR.go : {α : Type u_1} → List α → Array (List α) → List (List α)
-- Mathlib.Algebra.Ring.Parity
even_sub_two : ∀ {α : Type u_2} [inst : Ring α] {a : α}, Even (a - 2) ↔ Even a
-- Mathlib.Analysis.Normed.Algebra.UnitizationL1
WithLp.instAlgebraOfNatENNRealUnitizationOfIsScalarTower : {𝕜 : Type u_1} →
  {A : Type u_2} →
    [inst : NormedField 𝕜] →
      [inst_1 : NonUnitalNormedRing A] →
        [inst_2 : NormedSpace 𝕜 A] →
          [inst_3 : IsScalarTower 𝕜 A A] →
            [inst_4 : SMulCommClass 𝕜 A A] →
              {R : Type u_3} →
                [inst_5 : CommSemiring R] →
                  [inst_6 : Algebra R 𝕜] →
                    [inst_7 : DistribMulAction R A] → [IsScalarTower R 𝕜 A] → Algebra R (WithLp 1 (Unitization 𝕜 A))
-- Mathlib.Analysis.Normed.Group.Constructions
pi_norm_comp_le' : ∀ {ι : Type u_1} {E : Type u_2} {F : Type u_3} [inst : Fintype ι] [inst_1 : SeminormedGroup E] [inst_2 : Fintype F]
  (g : ι → E) (f : F → ι), ‖g ∘ f‖ ≤ ‖g‖
-- Mathlib.RepresentationTheory.Intertwining
Representation.IntertwiningMap.coe_snd : ∀ {A : Type u_1} {G : Type u_2} {V : Type u_3} {W : Type u_4} [inst : Semiring A] [inst_1 : Monoid G]
  [inst_2 : AddCommMonoid V] [inst_3 : AddCommMonoid W] [inst_4 : Module A V] [inst_5 : Module A W]
  (ρ : Representation A G V) (σ : Representation A G W), ⇑(Representation.IntertwiningMap.snd A ρ σ) = Prod.snd
-- Mathlib.Algebra.Polynomial.Lifts
/-- **Alias** of `Polynomial.exists_degree_eq_of_mem_lifts`.

---

A polynomial lifts if and only if it can be lifted to a polynomial of the same degree.  -/
Polynomial.mem_lifts_and_degree_eq : ∀ {R : Type u} [inst : Semiring R] {S : Type v} [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial S},
  p ∈ Polynomial.lifts f → ∃ q, Polynomial.map f q = p ∧ q.degree = p.degree
-- Mathlib.Data.Finsupp.Lex
/-- The linear order on `Finsupp`s obtained by the lexicographic ordering.  -/
Finsupp.Lex.linearOrder : {α : Type u_1} → {N : Type u_2} → [inst : Zero N] → [LinearOrder α] → [LinearOrder N] → LinearOrder (Lex (α →₀ N))
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.getD_union : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp],
  t₁.WF → t₂.WF → ∀ {k fallback : α}, (t₁ ∪ t₂).getD k fallback = t₂.getD k (t₁.getD k fallback)
-- Mathlib.Algebra.Module.Equiv.Basic
LinearEquiv.conj_refl : ∀ {R : Type u_1} {M : Type u_5} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (f : Module.End R M), (LinearEquiv.refl R M).conj f = f
-- Init.Data.String.Basic
String.Pos.offset_sliceFrom : ∀ {s : String} {p₀ pos : s.Pos} {h : p₀ ≤ pos}, (p₀.sliceFrom pos h).offset = pos.offset.unoffsetBy p₀.offset
-- Mathlib.Analysis.Normed.Group.Seminorm
/-- **Alias** of `smul_apply`. -/
NonarchAddGroupSeminorm.smul_apply : ∀ {M : Type u_1} {F : Type u_2} {α : outParam (Type u_3)} {β : outParam (Type u_4)} {inst : FunLike F α β}
  {inst_1 : SMul M β} {inst_2 : SMul M F} [self : IsSMulApply M F α β] (f : F) (r : M) (x : α), (r • f) x = r • f x
-- Init.Data.UInt.Lemmas
instLawfulIdentityUInt16HAddOfNat : Std.LawfulIdentity (fun x1 x2 => x1 + x2) 0
-- Mathlib.Algebra.Category.CommHopfAlgCat
CommHopfAlgCat.ofHom_id : ∀ {R : Type u} [inst : CommRing R] {X : Type v} [inst_1 : CommRing X] [inst_2 : HopfAlgebra R X],
  CommHopfAlgCat.ofHom (BialgHom.id R X) =
    CategoryTheory.CategoryStruct.id { X := X, commRing := inst_1, hopfAlgebra := inst_2 }
-- Mathlib.LinearAlgebra.Basis.Defs
Module.Basis.coe_reindex : ∀ {ι : Type u_1} {ι' : Type u_2} {R : Type u_3} {M : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] (b : Module.Basis ι R M) (e : ι ≃ ι'), ⇑(b.reindex e) = ⇑b ∘ ⇑e.symm
-- Mathlib.Order.CompleteLattice.Basic
biSup_ge_eq_iSup : ∀ {α : Type u_1} [inst : CompleteLattice α] {ι : Type u_8} [inst_1 : Preorder ι] {f : ι → α},
  ⨆ i, ⨆ j, ⨆ (_ : j ≥ i), f j = ⨆ i, f i
-- Mathlib.Algebra.Vertex.HVertexOperator
HahnSeries.ofIterate.eq_1 : ∀ {Γ : Type u_1} {Γ' : Type u_2} {R : Type u_3} [inst : PartialOrder Γ] [inst_1 : Zero R] [inst_2 : PartialOrder Γ']
  (x : HahnSeries Γ (HahnSeries Γ' R)), x.ofIterate = { coeff := fun g => (x.coeff g.1).coeff g.2, isPWO_support' := ⋯ }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.toList_filterMap : ∀ {α : Type u} {β : Type v} {γ : Type w} {cmp : α → α → Ordering} {t : Std.TreeMap α β cmp} {f : α → β → Option γ},
  (Std.TreeMap.filterMap f t).toList = List.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) t.toList
-- Init.Data.UInt.Lemmas
USize.mod_def : ∀ (a b : USize), a % b = { toBitVec := a.toBitVec % b.toBitVec }
-- Mathlib.NumberTheory.BernoulliPolynomials
Polynomial.bernoulli_eval_one : ∀ (n : ℕ), Polynomial.eval 1 (Polynomial.bernoulli n) = bernoulli' n
-- Mathlib.Algebra.Order.Monoid.PNat
PNat.equivNonZeroDivisorsNat_apply_coe : ∀ (x : ℕ+), ↑(PNat.equivNonZeroDivisorsNat x) = ↑x
-- Mathlib.Topology.Algebra.UniformMulAction
UniformSpace.Completion.instMulActionOfUniformContinuousConstSMul.eq_1 : ∀ (M : Type v) (X : Type x) [inst : UniformSpace X] [inst_1 : Monoid M] [inst_2 : MulAction M X]
  [inst_3 : UniformContinuousConstSMul M X],
  UniformSpace.Completion.instMulActionOfUniformContinuousConstSMul M X =
    { toSMul := UniformSpace.Completion.instSMul M X, mul_smul := ⋯, one_smul := ⋯ }
-- Mathlib.Tactic.Translate.Core
/-- Monad used by `applyReplacementFun`.
- The reader stores the free variables on which nothing should be translated.
- The state stores the free variables on which something has been translated.
- The cache caches the results on subexpressions.  -/
Mathlib.Tactic.Translate.ReplacementM : Type → Type
-- Mathlib.Computability.TuringMachine.StackTuringMachine
Turing.TM2to1.stWrite.eq_2 : ∀ {K : Type u_1} {Γ : K → Type u_2} {σ : Type u_4} {k : K} (v : σ) (l : List (Γ k)) (f : σ → Option (Γ k) → σ),
  Turing.TM2to1.stWrite v l (Turing.TM2to1.StAct.peek f) = l
-- Mathlib.Data.List.Nodup
List.nodup_reverse : ∀ {α : Type u} {l : List α}, l.reverse.Nodup ↔ l.Nodup
-- Aesop.RuleTac.RuleTerm
Aesop.RuleTerm.const.injEq : ∀ (decl decl_1 : Lean.Name), (Aesop.RuleTerm.const decl = Aesop.RuleTerm.const decl_1) = (decl = decl_1)
-- Mathlib.Tactic.Widget.StringDiagram
/-- The underlying expression of the node.  -/
Mathlib.Tactic.Widget.StringDiagram.IdNode.id : Mathlib.Tactic.Widget.StringDiagram.IdNode → Mathlib.Tactic.BicategoryLike.Atom₁
-- Mathlib.Topology.Sheaves.CommRingCat
TopCat.Presheaf.instAlgebraCarrierObjOppositeOpensCarrierCommRingCatLocalizationPresheaf : {X : TopCat} →
  {F : TopCat.Presheaf CommRingCat X} →
    (G : F.SubmonoidPresheaf) → (U : (TopologicalSpace.Opens ↑X)ᵒᵖ) → Algebra ↑(F.obj U) ↑(G.localizationPresheaf.obj U)
-- Mathlib.Data.Set.Pairwise.Basic
Set.InjOn.pairwiseDisjoint_image : ∀ {α : Type u_1} {ι : Type u_4} {ι' : Type u_5} [inst : PartialOrder α] [inst_1 : OrderBot α] {f : ι → α} {g : ι' → ι}
  {s : Set ι'}, Set.InjOn g s → ((g '' s).PairwiseDisjoint f ↔ s.PairwiseDisjoint (f ∘ g))
-- Mathlib.Data.EReal.Operations
EReal.sub_lt_sub_of_lt_of_le : ∀ {x y z t : EReal}, x < y → z ≤ t → z ≠ ⊥ → t ≠ ⊤ → x - t < y - z
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- If `CommMonoid` homs `g : M →* P, l : P →* A` induce maps of localizations, the composition
of the induced maps equals the map of localizations induced by `l ∘ g`.  -/
Submonoid.LocalizationMap.map_map : ∀ {M : Type u_1} [inst : CommMonoid M] {S : Submonoid M} {N : Type u_2} [inst_1 : CommMonoid N] {P : Type u_3}
  [inst_2 : CommMonoid P] (f : S.LocalizationMap N) {g : M →* P} {T : Submonoid P} (hy : ∀ (y : ↥S), g ↑y ∈ T)
  {Q : Type u_4} [inst_3 : CommMonoid Q] {k : T.LocalizationMap Q} {A : Type u_5} [inst_4 : CommMonoid A]
  {U : Submonoid A} {R : Type u_6} [inst_5 : CommMonoid R] (j : U.LocalizationMap R) {l : P →* A}
  (hl : ∀ (w : ↥T), l ↑w ∈ U) (x : N), (k.map hl j) ((f.map hy k) x) = (f.map ⋯ j) x
-- Mathlib.Analysis.Calculus.ContDiff.Defs
ContDiffAt.eventually : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {f : E → F}
  {x : E} {n : WithTop ℕ∞}, ContDiffAt 𝕜 n f x → n ≠ ↑⊤ → ∀ᶠ (y : E) in nhds x, ContDiffAt 𝕜 n f y
-- Mathlib.Data.List.Sigma
List.NodupKeys.kerase : ∀ {α : Type u} {β : α → Type v} {l : List (Sigma β)} [inst : DecidableEq α] (a : α),
  l.NodupKeys → (List.kerase a l).NodupKeys
-- Mathlib.Algebra.Order.Ring.Defs
IsOrderedRing.of_mul_nonneg : ∀ {R : Type u} [inst : Ring R] [inst_1 : PartialOrder R] [IsOrderedAddMonoid R] [ZeroLEOneClass R],
  (∀ (a b : R), 0 ≤ a → 0 ≤ b → 0 ≤ a * b) → IsOrderedRing R
-- Mathlib.Data.Fintype.CardEmbedding
/-- The cardinality of embeddings from an infinite type to a finite type is zero.
This is a re-statement of the pigeonhole principle.  -/
Fintype.card_embedding_eq_of_infinite : ∀ {α : Type u_1} {β : Type u_2} [Infinite α] [Finite β] [inst : Fintype (α ↪ β)], Fintype.card (α ↪ β) = 0
-- Init.Data.BitVec.Lemmas
BitVec.not_zero : ∀ {n : ℕ}, ~~~0#n = BitVec.allOnes n
-- Mathlib.RingTheory.MvPowerSeries.Substitution
MvPowerSeries.HasSubst.X_pow : ∀ {σ : Type u_1} {S : Type u_5} [inst : CommRing S] {n : ℕ},
  n ≠ 0 → MvPowerSeries.HasSubst fun s => MvPowerSeries.X s ^ n
-- Mathlib.ModelTheory.Encoding
_private.Mathlib.ModelTheory.Encoding.0.FirstOrder.Language.BoundedFormula.listDecode.match_1.eq_1 : ∀ {L : FirstOrder.Language} {α : Type u_3}
  (motive : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ) → Sort u_4) (n : ℕ)
  (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ))
  (h_1 :
    (n : ℕ) →
      (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
        motive (Sum.inr (Sum.inr n.succ.succ) :: l))
  (h_2 :
    (n₁ : ℕ) →
      (t₁ : L.Term (α ⊕ Fin n₁)) →
        (n₂ : ℕ) →
          (t₂ : L.Term (α ⊕ Fin n₂)) →
            (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
              motive (Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l))
  (h_3 :
    (n : ℕ) →
      (R : L.Relations n) →
        (k : ℕ) →
          (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) →
            motive (Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l))
  (h_4 : (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive (Sum.inr (Sum.inr 0) :: l))
  (h_5 : (l : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive (Sum.inr (Sum.inr 1) :: l))
  (h_6 : (x : List ((k : ℕ) × L.Term (α ⊕ Fin k) ⊕ (n : ℕ) × L.Relations n ⊕ ℕ)) → motive x),
  (match Sum.inr (Sum.inr n.succ.succ) :: l with
    | Sum.inr (Sum.inr n.succ.succ) :: l => h_1 n l
    | Sum.inl ⟨n₁, t₁⟩ :: Sum.inl ⟨n₂, t₂⟩ :: l => h_2 n₁ t₁ n₂ t₂ l
    | Sum.inr (Sum.inl ⟨n, R⟩) :: Sum.inr (Sum.inr k) :: l => h_3 n R k l
    | Sum.inr (Sum.inr 0) :: l => h_4 l
    | Sum.inr (Sum.inr 1) :: l => h_5 l
    | x => h_6 x) =
    h_1 n l