mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Join.Opposites
/-- Characterize `Join.opEquivInverse` with respect to the left inclusion  -/
CategoryTheory.Join.inclLeftCompOpEquivInverse : (C : Type u₁) →
  (D : Type u₂) →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        (CategoryTheory.Join.inclLeft Dᵒᵖ Cᵒᵖ).comp (CategoryTheory.Join.opEquiv C D).inverse ≅
          (CategoryTheory.Join.inclRight C D).op
-- Mathlib.Topology.Algebra.Constructions
Topology.IsInducing.units_map : ∀ {M : Type u_1} {N : Type u_2} [inst : TopologicalSpace M] [inst_1 : Monoid M] [inst_2 : TopologicalSpace N]
  [inst_3 : Monoid N] {f : M →* N}, Topology.IsInducing ⇑f → Topology.IsInducing ⇑(Units.map f)
-- Mathlib.CategoryTheory.FiberedCategory.BasedCategory
CategoryTheory.BasedNatTrans.homCategory : {𝒮 : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} 𝒮] →
    (𝒳 : CategoryTheory.BasedCategory 𝒮) →
      (𝒴 : CategoryTheory.BasedCategory 𝒮) →
        CategoryTheory.Category.{max u₂ v₃, max (max (max u₂ v₂) u₃) v₃} (CategoryTheory.BasedFunctor 𝒳 𝒴)
-- Mathlib.Topology.Algebra.RestrictedProduct.Basic
RestrictedProduct.instAddCoeOfAddMemClass.eq_1 : ∀ {ι : Type u_1} (R : ι → Type u_2) {𝓕 : Filter ι} {S : ι → Type u_3} [inst : (i : ι) → SetLike (S i) (R i)]
  {B : (i : ι) → S i} [inst_1 : (i : ι) → Add (R i)] [inst_2 : ∀ (i : ι), AddMemClass (S i) (R i)],
  RestrictedProduct.instAddCoeOfAddMemClass R = { add := fun x y => ⟨fun i => x i + y i, ⋯⟩ }
-- Mathlib.Topology.OpenPartialHomeomorph.Continuity
/-- A function is continuous on a set if and only if its composition with an open partial
homeomorphism on the left is continuous on the corresponding set.  -/
OpenPartialHomeomorph.continuousOn_iff_continuousOn_comp_left : ∀ {X : Type u_1} {Y : Type u_3} {Z : Type u_5} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace Y]
  [inst_2 : TopologicalSpace Z] (e : OpenPartialHomeomorph X Y) {f : Z → X} {s : Set Z},
  s ⊆ f ⁻¹' e.source → (ContinuousOn f s ↔ ContinuousOn (↑e ∘ f) s)
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.SymbolKind.boolean.sizeOf_spec : sizeOf Lean.Lsp.SymbolKind.boolean = 1
-- Init.Data.List.Attach
List.find?_subtype : ∀ {α : Type u_1} {p : α → Prop} {l : List { x // p x }} {f : { x // p x } → Bool} {g : α → Bool},
  (∀ (x : α) (h : p x), f ⟨x, h⟩ = g x) → Option.map Subtype.val (List.find? f l) = List.find? g l.unattach
-- Mathlib.NumberTheory.Height.Basic
/-- Consider a finite family `x : (a : α) → ι a → K` of tuples. Then the multiplicative height
of the "multiplication table" `fun (I : (a : α) → ι a ↦ ∏ a, x a (I a))` is the product
of the multiplicative heights of all the `x a`.  -/
Height.mulHeight_fun_prod_eq : ∀ {K : Type u_1} [inst : Field K] [inst_1 : Height.AdmissibleAbsValues K] {α : Type u} [inst_2 : Fintype α]
  {ι : α → Type v} [∀ (a : α), Finite (ι a)] {x : (a : α) → ι a → K},
  (∀ (a : α), x a ≠ 0) → (Height.mulHeight fun I => ∏ a, x a (I a)) = ∏ a, Height.mulHeight (x a)
-- Std.Data.HashMap.Lemmas
Std.HashMap.Equiv.inter_congr : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : Type v} {m₁ m₂ m₃ m₄ : Std.HashMap α β} [EquivBEq α]
  [LawfulHashable α], m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ ∩ m₂).Equiv (m₃ ∩ m₄)
-- Mathlib.Order.Hom.Bounded
BotHom.instDistribLattice.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Bot α] [inst_1 : DistribLattice β] [inst_2 : OrderBot β],
  BotHom.instDistribLattice = Function.Injective.distribLattice DFunLike.coe ⋯ ⋯ ⋯ ⋯ ⋯
-- Mathlib.Logic.Equiv.Set
/-- `sigmaPreimageEquiv f` for `f : α → β` is the natural equivalence between
the type of all preimages of points under `f` and the total space `α`.  -/
Equiv.sigmaPreimageEquiv : {α : Type u_3} → {β : Type u_4} → (f : α → β) → (b : β) × ↑(f ⁻¹' {b}) ≃ α
-- Mathlib.CategoryTheory.Sites.Coherent.Equivalence
CategoryTheory.Equivalence.sheafCongrPrecoherent_unitIso_hom_app_hom_app : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {D : Type u_2}
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Precoherent C] (A : Type u_3)
  [inst_3 : CategoryTheory.Category.{v_3, u_3} A] (e : C ≌ D)
  (X : CategoryTheory.Sheaf (CategoryTheory.coherentTopology C) A) (X_1 : Cᵒᵖ),
  ((CategoryTheory.Equivalence.sheafCongrPrecoherent A e).unitIso.hom.app X).hom.app X_1 =
    X.obj.map (e.unitIso.inv.app (Opposite.unop X_1)).op
-- Std.Time.Date.Basic
Std.Time.instHSubOffsetOffset_28 : HSub Std.Time.Hour.Offset Std.Time.Day.Offset Std.Time.Hour.Offset
-- Mathlib.RingTheory.MvPowerSeries.Trunc
/-- The `n`th truncation of a multivariate formal power series to a multivariate polynomial.

If `f : MvPowerSeries σ R` and `n : σ →₀ ℕ` is a (finitely-supported) function from `σ`
to the naturals, then `trunc' R n f` is the multivariable polynomial obtained from `f`
by keeping only the monomials $c\prod_i X_i^{a_i}$ where `a i ≤ n i` for all `i`.  -/
MvPowerSeries.trunc' : {σ : Type u_1} →
  [DecidableEq σ] → (R : Type u_4) → [inst : CommSemiring R] → (σ →₀ ℕ) → MvPowerSeries σ R →ₗ[R] MvPolynomial σ R
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- Variant of `UniqueFactorizationMonoid.count_normalizedFactors_eq` for associated Ideals.  -/
Ideal.count_associates_eq' : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDedekindDomain R] {a x : R},
  Prime x →
    ∀ {n : ℕ},
      x ^ n ∣ a → ¬x ^ (n + 1) ∣ a → (Associates.mk (Ideal.span {x})).count (Associates.mk (Ideal.span {a})).factors = n
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.getElem!_eq_getD_default : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] [inst_2 : Inhabited β] {a : α}, m[a]! = m.getD a default
-- Init.Data.List.Sublist
List.sublist_map_iff : ∀ {β : Type u_1} {α : Type u_2} {l₂ : List α} {l₁ : List β} {f : α → β},
  l₁.Sublist (List.map f l₂) ↔ ∃ l', l'.Sublist l₂ ∧ l₁ = List.map f l'
-- Mathlib.Analysis.Convex.Exposed
/-- For nontrivial `𝕜`, if `B` is an exposed subset of `A`, then `B` is the intersection of `A` with
some closed half-space. The converse is *not* true. It would require that the corresponding open
half-space doesn't intersect `A`.  -/
IsExposed.eq_inter_halfSpace : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : TopologicalSpace 𝕜] [inst_1 : Ring 𝕜] [inst_2 : PartialOrder 𝕜]
  [inst_3 : AddCommMonoid E] [inst_4 : TopologicalSpace E] [inst_5 : Module 𝕜 E] [IsOrderedRing 𝕜] [Nontrivial 𝕜]
  {A B : Set E}, IsExposed 𝕜 A B → ∃ l a, B = {x | x ∈ A ∧ a ≤ l x}
-- Init.Data.String.Lemmas.Pattern.String.ForwardSearcher
_private.Init.Data.String.Lemmas.Pattern.String.ForwardSearcher.0.String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable.push : ∀ {b : ByteArray} {v : Array ℕ},
  String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable✝ b v →
    ∀ {d : ℕ} (hle : v.size + 1 ≤ b.size),
      d = String.Slice.Pattern.Model.ForwardSliceSearcher.prefixFunction✝ b v.size ⋯ →
        String.Slice.Pattern.Model.ForwardSliceSearcher.IsTable✝ b (v.push d)
-- Mathlib.MeasureTheory.Measure.Typeclasses.Finite
MeasureTheory.Measure.finiteSpanningSetsInOpen'_def : ∀ {α : Type u_5} [inst : TopologicalSpace α] [inst_1 : SecondCountableTopology α] {m : MeasurableSpace α}
  (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.IsLocallyFiniteMeasure μ],
  μ.finiteSpanningSetsInOpen' =
    have H := ⋯;
    H.some
-- Mathlib.Algebra.Group.Units.Hom
IsAddUnit.liftRight_neg_add : ∀ {M : Type u_3} {N : Type u_4} [inst : AddMonoid M] [inst_1 : AddMonoid N] (f : M →+ N)
  (h : ∀ (x : M), IsAddUnit (f x)) (x : M), ↑(-(IsAddUnit.liftRight f h) x) + f x = 0
-- Init.Data.BitVec.Lemmas
BitVec.toNat_cpop_cons : ∀ {w : ℕ} {x : BitVec w} {b : Bool}, (BitVec.cons b x).cpop.toNat = b.toNat + x.cpop.toNat
-- Mathlib.CategoryTheory.Monoidal.Transport
/-- Transport a monoidal structure along an equivalence of (plain) categories.
 -/
CategoryTheory.Monoidal.transportStruct : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    [CategoryTheory.MonoidalCategory C] →
      {D : Type u₂} → [inst_2 : CategoryTheory.Category.{v₂, u₂} D] → (C ≌ D) → CategoryTheory.MonoidalCategoryStruct D
-- Init.Data.UInt.Lemmas
UInt16.le_iff_toBitVec_le : ∀ {a b : UInt16}, a ≤ b ↔ a.toBitVec ≤ b.toBitVec
-- Mathlib.Order.Monotone.Defs
strictMonoOn_univ : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β},
  StrictMonoOn f Set.univ ↔ StrictMono f
-- Lean.Elab.DocString
Lean.Doc.instFromDocArgDataValue : Lean.Doc.FromDocArg Lean.DataValue
-- Mathlib.Algebra.Ring.Opposite
/-- A non-unital ring homomorphism `f : R →ₙ* S` such that `f x` commutes with `f y` for all `x, y`
defines a non-unital ring homomorphism from `Rᵐᵒᵖ`.  -/
NonUnitalRingHom.fromOpposite : {R : Type u_2} →
  {S : Type u_3} →
    [inst : NonUnitalNonAssocSemiring R] →
      [inst_1 : NonUnitalNonAssocSemiring S] → (f : R →ₙ+* S) → (∀ (x y : R), Commute (f x) (f y)) → Rᵐᵒᵖ →ₙ+* S
-- Mathlib.Data.List.Sort
StrictMono.sortedLE_listMap : ∀ {α : Type u_1} {β : Type u_2} [inst : LinearOrder α] [inst_1 : Preorder β] {f : α → β} {l : List α},
  StrictMono f → ((List.map f l).SortedLE ↔ l.SortedLE)
-- Std.Tactic.BVDecide.Reflect
Std.Tactic.BVDecide.Reflect.BitVec.extract_congr : ∀ (start len w : ℕ) (x x' : BitVec w), x = x' → BitVec.extractLsb' start len x' = BitVec.extractLsb' start len x
-- Mathlib.Probability.ProductMeasure
/-- `partialTraj κ a b` is a kernel which up to an equivalence is equal to
`Kernel.id ×ₖ (κ a ⊗ₖ ... ⊗ₖ κ (b - 1))`. This lemma therefore states that if the kernels `κ`
are constant then their composition-product is the product measure.  -/
MeasureTheory.partialTraj_const_restrict₂ : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)} (μ : (n : ℕ) → MeasureTheory.Measure (X n))
  [hμ : ∀ (n : ℕ), MeasureTheory.IsProbabilityMeasure (μ n)] {a b : ℕ},
  (ProbabilityTheory.Kernel.partialTraj
          (fun n => ProbabilityTheory.Kernel.const ((i : ↥(Finset.Iic n)) → X ↑i) (μ (n + 1))) a b).map
      (Finset.restrict₂ ⋯) =
    ProbabilityTheory.Kernel.const ((i : ↥(Finset.Iic a)) → X ↑i) (MeasureTheory.Measure.pi fun i => μ ↑i)
-- Mathlib.Data.Multiset.Sort
Multiset.sort_singleton : ∀ {α : Type u_1} (a : α) (r : α → α → Prop) [inst : DecidableRel r] [inst_1 : IsTrans α r] [inst_2 : Std.Antisymm r]
  [inst_3 : Std.Total r], {a}.sort r = [a]
-- Mathlib.GroupTheory.GroupAction.Quotient
AddAction.injective_ofQuotientStabilizer : ∀ (G : Type u) {X : Type v} [inst : AddGroup G] [inst_1 : AddAction G X] (x : X),
  Function.Injective (AddAction.ofQuotientStabilizer G x)
-- Mathlib.MeasureTheory.Measure.Hausdorff
MeasureTheory.OuterMeasure.coe_mkMetric : ∀ {X : Type u_2} [inst : EMetricSpace X] [inst_1 : MeasurableSpace X] [inst_2 : BorelSpace X] (m : ENNReal → ENNReal),
  ⇑(MeasureTheory.OuterMeasure.mkMetric m) = ⇑(MeasureTheory.Measure.mkMetric m)
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCocone
CochainComplex.mappingCocone.liftCochain.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {K L : CochainComplex C ℤ} (φ : K ⟶ L) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {M : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain M K n) (β : CochainComplex.HomComplex.Cochain M L m) (h : m + 1 = n),
  CochainComplex.mappingCocone.liftCochain φ α β h =
    (CochainComplex.mappingCone.liftCochain φ α β h).rightShift (-1) n ⋯
-- Mathlib.CategoryTheory.Comma.Arrow
CategoryTheory.Arrow.isIso_right : ∀ {T : Type u} [inst : CategoryTheory.Category.{v, u} T] {f g : CategoryTheory.Arrow T} (sq : g ⟶ f)
  [CategoryTheory.IsIso sq], CategoryTheory.IsIso (CategoryTheory.Arrow.Hom.right sq)
-- Mathlib.RingTheory.FractionalIdeal.Basic
FractionalIdeal.isFractional_of_le_one : ∀ {R : Type u_1} [inst : CommRing R] {S : Submonoid R} {P : Type u_2} [inst_1 : CommRing P] [inst_2 : Algebra R P],
  ∀ I ≤ 1, IsFractional S I
-- Mathlib.Analysis.Seminorm
Seminorm.ball_zero_absorbs_ball_zero : ∀ {𝕜 : Type u_3} {E : Type u_7} [inst : NormedDivisionRing 𝕜] [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  (p : Seminorm 𝕜 E) {r₁ r₂ : ℝ}, 0 < r₁ → Absorbs 𝕜 (p.ball 0 r₁) (p.ball 0 r₂)
-- Mathlib.Algebra.Ring.Commute
Units.sq_eq_sq_iff_eq_or_eq_neg : ∀ {R : Type u} [inst : CommRing R] [NoZeroDivisors R] {a b : Rˣ}, a ^ 2 = b ^ 2 ↔ a = b ∨ a = -b
-- Mathlib.GroupTheory.Congruence.Defs
Con.Quotient.eq_1 : ∀ {M : Type u_1} [inst : Mul M] (c : Con M), c.Quotient = Quotient c.toSetoid
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.contains_toList : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [inst : BEq α] [Std.LawfulBEqCmp cmp]
  [Std.TransCmp cmp], t.WF → ∀ {k : α}, t.toList.contains k = t.contains k
-- Std.Sync.StreamMap
_private.Std.Sync.StreamMap.0.Std.StreamMap.mk.injEq : ∀ {α β : Type} (streams streams_1 : Array (α × Std.Async.Selector β × IO Unit)),
  ({ streams := streams } = { streams := streams_1 }) = (streams = streams_1)
-- Mathlib.CategoryTheory.Sites.LocallySurjective
CategoryTheory.Presheaf.pullback_imageSieve : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {A : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} A]
  {FA : A → A → Type u_1} {CA : A → Type w'} [inst_2 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)]
  [inst_3 : CategoryTheory.ConcreteCategory A FA] {F G : CategoryTheory.Functor Cᵒᵖ A} (f : F ⟶ G) {U : C}
  (s : CategoryTheory.ToType (G.obj (Opposite.op U))) {V : C} (g : V ⟶ U),
  CategoryTheory.Sieve.pullback g (CategoryTheory.Presheaf.imageSieve f s) =
    CategoryTheory.Presheaf.imageSieve f ((CategoryTheory.ConcreteCategory.hom (G.map g.op)) s)
-- Init.Data.Int.Gcd
Int.lcm_mul_right_left_eq_mul_of_lcm_eq_mul : ∀ {n m k : ℤ}, n.lcm m = n.natAbs * m.natAbs → (n * k).lcm m = n.natAbs * k.lcm m
-- Mathlib.CategoryTheory.Functor.FunctorHom
/-- Composition of `f : HomObj F G A` with `g : HomObj G M A`.  -/
CategoryTheory.Functor.HomObj.comp : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {D : Type u'} →
      [inst_1 : CategoryTheory.Category.{v', u'} D] →
        {F G : CategoryTheory.Functor C D} →
          {A : CategoryTheory.Functor C (Type w)} →
            {M : CategoryTheory.Functor C D} → F.HomObj G A → G.HomObj M A → F.HomObj M A
-- Init.Data.UInt.Lemmas
UInt8.toUInt64_ofNat : ∀ {n : ℕ}, n < 256 → (OfNat.ofNat n).toUInt64 = OfNat.ofNat n
-- Mathlib.RingTheory.MvPowerSeries.Basic
MvPolynomial.coe_zero : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R], ↑0 = 0
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
CategoryTheory.Limits.Multicofork.IsColimit.mk_desc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {J : CategoryTheory.Limits.MultispanShape}
  {I : CategoryTheory.Limits.MultispanIndex J C} (K : CategoryTheory.Limits.Multicofork I)
  (desc : (E : CategoryTheory.Limits.Multicofork I) → K.pt ⟶ E.pt)
  (fac :
    ∀ (E : CategoryTheory.Limits.Multicofork I) (i : J.R), CategoryTheory.CategoryStruct.comp (K.π i) (desc E) = E.π i)
  (uniq :
    ∀ (E : CategoryTheory.Limits.Multicofork I) (m : K.pt ⟶ E.pt),
      (∀ (i : J.R), CategoryTheory.CategoryStruct.comp (K.π i) m = E.π i) → m = desc E)
  (E : CategoryTheory.Limits.Multicofork I),
  (CategoryTheory.Limits.Multicofork.IsColimit.mk K desc fac uniq).desc E = desc E
-- Mathlib.Algebra.Polynomial.Module.AEval
/-- Given and `R`-module `M` and a linear map `φ : M →ₗ[R] M`, `Module.AEval' φ` is loosely speaking
the `R[X]`-module with elements `m : M`, where the action of a polynomial $f$ is given by
$f • m = f(a) • m$.

More precisely, `Module.AEval' φ` has elements `Module.AEval'.of φ m` for `m : M`,
and the action of `f` is `f • (of φ m) = of φ ((aeval φ f) • m)`.

`Module.AEval'` is defined as a special case of `Module.AEval` in which the `R`-algebra is
`M →ₗ[R] M`. Lemmas involving `Module.AEval` may be applied to `Module.AEval'`.
 -/
Module.AEval' : {R : Type u_1} →
  {M : Type u_2} → [inst : CommSemiring R] → [inst_1 : AddCommMonoid M] → [inst_2 : Module R M] → (M →ₗ[R] M) → Type u_2
-- Mathlib.Algebra.Homology.ShortComplex.QuasiIso
CategoryTheory.ShortComplex.quasiIso_iff_comp_right : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {S₁ S₂ S₃ : CategoryTheory.ShortComplex C} [inst_2 : S₁.HasHomology] [inst_3 : S₂.HasHomology]
  [inst_4 : S₃.HasHomology] (φ : S₁ ⟶ S₂) (φ' : S₂ ⟶ S₃) [hφ' : CategoryTheory.ShortComplex.QuasiIso φ'],
  CategoryTheory.ShortComplex.QuasiIso (CategoryTheory.CategoryStruct.comp φ φ') ↔
    CategoryTheory.ShortComplex.QuasiIso φ
-- Mathlib.Data.Finsupp.Basic
Nat.cast_finsupp_sum : ∀ {α : Type u_1} {M : Type u_5} {R : Type u_10} [inst : Zero M] (f : α →₀ M) [inst_1 : AddCommMonoidWithOne R]
  (g : α → M → ℕ), ↑(f.sum g) = f.sum fun a b => ↑(g a b)
-- Mathlib.GroupTheory.MonoidLocalization.Maps
/-- Given a Localization map `f : M →+ N` for an AddSubmonoid `S ⊆ M` and a map of
`AddCommMonoid`s `g : M →+ P` such that `g y` is invertible for all `y : S`, the homomorphism
induced from `N` to `P` maps `f x - f y` to `g x - g y` for all `x : M, y ∈ S`.  -/
AddSubmonoid.LocalizationMap.lift_mk' : ∀ {M : Type u_1} [inst : AddCommMonoid M] {S : AddSubmonoid M} {N : Type u_2} [inst_1 : AddCommMonoid N] {P : Type u_3}
  [inst_2 : AddCommMonoid P] (f : S.LocalizationMap N) {g : M →+ P} (hg : ∀ (y : ↥S), IsAddUnit (g ↑y)) (x : M)
  (y : ↥S), (f.lift hg) (f.mk' x y) = g x + ↑(-(IsAddUnit.liftRight (g.domRestrict S) hg) y)
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw.alter_eq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : LawfulBEq α] [inst_2 : Hashable α] {m : Std.DHashMap.Raw α β}
  (h : m.WF) {k : α} {f : Option (β k) → Option (β k)}, m.alter k f = ↑(Std.DHashMap.Internal.Raw₀.alter ⟨m, ⋯⟩ k f)
-- Mathlib.Tactic.CategoryTheory.Coherence.Datatypes
/-- The expression for `Iso.hom η`.  -/
Mathlib.Tactic.BicategoryLike.MonadMor₂.atomHomM : {m : Type → Type} →
  [self : Mathlib.Tactic.BicategoryLike.MonadMor₂ m] →
    Mathlib.Tactic.BicategoryLike.AtomIso → m Mathlib.Tactic.BicategoryLike.Atom
-- Mathlib.Order.Partition.Finpartition
Finpartition.ext : ∀ {α : Type u_1} {inst : Lattice α} {inst_1 : OrderBot α} {a : α} {x y : Finpartition a}, x.parts = y.parts → x = y
-- Mathlib.Analysis.InnerProductSpace.ExteriorPower
_private.Mathlib.Analysis.InnerProductSpace.ExteriorPower.0.exteriorPower.innerProductForm.eq_1 : ∀ {n : ℕ} {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : InnerProductSpace ℝ E],
  exteriorPower.innerProductForm✝ = exteriorPower.pairingDual ℝ E n ∘ₗ exteriorPower.map n (innerₗ E)
-- Init.Data.String.Basic
String.Slice.Pos.str_lt_str_iff : ∀ {s : String.Slice} {p q : s.Pos}, p.str < q.str ↔ p < q
-- Mathlib.Control.Monad.Cont
StateT.callCC.eq_1 : ∀ {m : Type u → Type v} {σ : Type u} [inst : MonadCont m] {α β : Type u}
  (f : MonadCont.Label α (StateT σ m) β → StateT σ m α),
  StateT.callCC f = StateT.mk fun r => MonadCont.callCC fun f' => (f (StateT.mkLabel f')).run r
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.smul_set_iInter_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : SMul α β] (a : α) (t : ι → Set β), a • ⋂ i, t i ⊆ ⋂ i, a • t i
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Defs
Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.destruct_eq_none : ∀ {basis_hd : ℝ → ℝ} {basis_tl : Tactic.ComputeAsymptotics.Basis}
  {ms : Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries basis_hd basis_tl},
  ms.destruct = none → ms = Tactic.ComputeAsymptotics.MultiseriesExpansion.Multiseries.nil
-- Mathlib.Topology.UnitInterval
Set.Icc.convexComb_assoc_coeff₂'.eq_1 : ∀ (s t : ↑unitInterval),
  Set.Icc.convexComb_assoc_coeff₂' s t =
    unitInterval.symm (Set.Icc.convexComb_assoc_coeff₁ (unitInterval.symm t) (unitInterval.symm s))
-- Lean.Elab.Tactic.BuiltinTactic
Lean.Elab.Tactic.evalRotateLeft : Lean.Elab.Tactic.Tactic
-- Mathlib.Data.Finmap
/-- Erase a key from the map. If the key is not present it does nothing.  -/
Finmap.erase : {α : Type u} → {β : α → Type v} → [DecidableEq α] → α → Finmap β → Finmap β
-- Mathlib.CategoryTheory.Abelian.Pseudoelements
/-- The arrows with codomain `P` equipped with the equivalence relation of being pseudo-equal.  -/
CategoryTheory.Abelian.Pseudoelement.setoid : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] → [CategoryTheory.Abelian C] → (P : C) → Setoid (CategoryTheory.Over P)
-- Mathlib.CategoryTheory.Limits.Shapes.Terminal
/-- To show a category is an `InitialMonoClass` it suffices to show the unique morphism from the
initial object to a terminal object is a monomorphism.  -/
CategoryTheory.Limits.InitialMonoClass.of_terminal : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasInitial C]
  [inst_2 : CategoryTheory.Limits.HasTerminal C],
  CategoryTheory.Mono (CategoryTheory.Limits.initial.to (⊤_ C)) → CategoryTheory.Limits.InitialMonoClass C
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.vadd_domain : ∀ {R : Type u_1} {S : Type u_2} [inst : Ring R] [inst_1 : Ring S] {σ : R →+* S} {E : Type u_4} [inst_2 : AddCommGroup E]
  [inst_3 : Module R E] {F : Type u_5} [inst_4 : AddCommGroup F] [inst_5 : Module S F] (f : E →ₛₗ[σ] F)
  (g : E →ₛₗ.[σ] F), (f +ᵥ g).domain = g.domain
-- Mathlib.Order.Filter.Pointwise
/-- Inversion is involutive on `Filter α` if it is on `α`.  -/
Filter.instInvolutiveInv : {α : Type u_2} → [InvolutiveInv α] → InvolutiveInv (Filter α)
-- Mathlib.Topology.Algebra.ContinuousMonoidHom
ContinuousMonoidHom.coe_coe : ∀ {A : Type u_2} {B : Type u_3} [inst : Monoid A] [inst_1 : Monoid B] [inst_2 : TopologicalSpace A]
  [inst_3 : TopologicalSpace B] {F : Type u_7} [inst_4 : FunLike F A B] [inst_5 : MonoidHomClass F A B]
  [inst_6 : ContinuousMapClass F A B] (f : F), ⇑↑f = ⇑f
-- Mathlib.AlgebraicGeometry.Gluing
AlgebraicGeometry.Scheme.Cover.gluedCoverT'_snd_snd : ∀ {X : AlgebraicGeometry.Scheme} (𝒰 : X.OpenCover) (x y z : 𝒰.I₀),
  CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.Scheme.Cover.gluedCoverT' 𝒰 x y z)
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.snd (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f z))
          (CategoryTheory.Limits.pullback.fst (𝒰.f y) (𝒰.f x)))
        (CategoryTheory.Limits.pullback.snd (𝒰.f y) (𝒰.f x))) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
        (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f z)))
      (CategoryTheory.Limits.pullback.fst (𝒰.f x) (𝒰.f y))
-- Std.Time.DateTime.PlainDateTime
Std.Time.PlainDateTime.mk.injEq : ∀ (date : Std.Time.PlainDate) (time : Std.Time.PlainTime) (date_1 : Std.Time.PlainDate) (time_1 : Std.Time.PlainTime),
  ({ date := date, time := time } = { date := date_1, time := time_1 }) = (date = date_1 ∧ time = time_1)
-- Lean.Elab.Term.TermElabM
Lean.Elab.Tactic.TacticFinishedSnapshot.toSnapshot : Lean.Elab.Tactic.TacticFinishedSnapshot → Lean.Language.Snapshot
-- Mathlib.Analysis.InnerProductSpace.Adjoint
/-- An idempotent operator is self-adjoint iff it is normal.  -/
ContinuousLinearMap.IsIdempotentElem.isSelfAdjoint_iff_isStarNormal : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup E] [inst_2 : InnerProductSpace 𝕜 E]
  {T : E →L[𝕜] E} [inst_3 : CompleteSpace E], IsIdempotentElem T → (IsSelfAdjoint T ↔ IsStarNormal T)
-- Mathlib.Algebra.Polynomial.Expand
/-- Expansion is injective.  -/
Polynomial.expand_injective : ∀ {R : Type u} [inst : CommSemiring R] {n : ℕ}, 0 < n → Function.Injective ⇑(Polynomial.expand R n)
-- Mathlib.CategoryTheory.Subobject.Lattice
CategoryTheory.Subobject.inf_le_right : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C] {A : C}
  (f g : CategoryTheory.Subobject A), (CategoryTheory.Subobject.inf.obj f).obj g ≤ g
-- Mathlib.Topology.Order.LeftRight
nhdsGT_sup_nhdsLE : ∀ {α : Type u_1} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] (a : α),
  nhdsWithin a (Set.Ioi a) ⊔ nhdsWithin a (Set.Iic a) = nhds a
-- Mathlib.RingTheory.MvPolynomial.MonomialOrder
MonomialOrder.coeff_degree_eq_zero_iff : ∀ {σ : Type u_1} {m : MonomialOrder σ} {R : Type u_2} [inst : CommSemiring R] {f : MvPolynomial σ R},
  MvPolynomial.coeff (m.degree f) f = 0 ↔ f = 0