mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- The Hausdorff edistance between two sets is the smallest `r` such that each set
is contained in the `r`-neighborhood of the other one  -/
Metric.hausdorffEDist : {α : Type u_2} → [PseudoEMetricSpace α] → Set α → Set α → ENNReal
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- The equalizer of `(f, g)`, where `f = g`, is an isomorphism.  -/
CategoryTheory.Limits.equalizer.ι_of_eq : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y}
  [inst_1 : CategoryTheory.Limits.HasEqualizer f g],
  f = g → CategoryTheory.IsIso (CategoryTheory.Limits.equalizer.ι f g)
-- Std.Data.DHashMap.Internal.AssocList.Lemmas
_private.Std.Data.DHashMap.Internal.AssocList.Lemmas.0.Std.DHashMap.Internal.AssocList.filter.eq_1 : ∀ {α : Type u} {β : α → Type v} (f : (a : α) → β a → Bool),
  Std.DHashMap.Internal.AssocList.filter f =
    Std.DHashMap.Internal.AssocList.filter.go✝ f Std.DHashMap.Internal.AssocList.nil
-- Mathlib.Algebra.Homology.TotalComplexSymmetry
HomologicalComplex₂.instHasTotalFlip_1 : ∀ {C : Type u_1} {I₁ : Type u_2} {I₂ : Type u_3} {J : Type u_4} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Preadditive C] {c₁ : ComplexShape I₁} {c₂ : ComplexShape I₂}
  (K : HomologicalComplex₂ C c₁ c₂) (c : ComplexShape J) [inst_2 : TotalComplexShape c₁ c₂ c] [K.HasTotal c],
  K.flip.flip.HasTotal c
-- Mathlib.Topology.EMetricSpace.Defs
/-- Consider an extended distance on a topological space, for which the neighborhoods can be
expressed in terms of the distance. Then we define the emetric space structure associated to this
distance, with a topology defeq to the initial one.  -/
PseudoEMetricSpace.ofEDistOfTopology : {α : Type u_2} →
  [inst : TopologicalSpace α] →
    (d : α → α → ENNReal) →
      (∀ (x : α), d x x = 0) →
        (∀ (x y : α), d x y = d y x) →
          (∀ (x y z : α), d x z ≤ d x y + d y z) →
            (∀ (x : α), (nhds x).HasBasis (fun c => 0 < c) fun c => {y | d x y < c}) → PseudoEMetricSpace α
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.range_eq : ∀ {G : Type u_1} {H : Type u_2} [inst : Group G] [inst_1 : Group H] {K : Type u_3} [inst_2 : Group K]
  (f : Monoid.Coprod G H →* K), f.range = (f.comp Monoid.Coprod.inl).range ⊔ (f.comp Monoid.Coprod.inr).range
-- Std.Time.Date.Unit.Weekday
Std.Time.Weekday.instDecidableLeOrdinal : {x y : Std.Time.Weekday.Ordinal} → Decidable (x ≤ y)
-- Mathlib.LinearAlgebra.Matrix.Ideal
TwoSidedIdeal.matrix_ringCon : ∀ {R : Type u_1} (n : Type u_2) [inst : NonUnitalNonAssocRing R] [inst_1 : Fintype n] (I : TwoSidedIdeal R),
  (TwoSidedIdeal.matrix n I).ringCon = RingCon.matrix n I.ringCon
-- Mathlib.CategoryTheory.Sites.LocallyInjective
CategoryTheory.Presheaf.instIsLocallyInjectiveOfIsIsoFunctorOpposite : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u'} [inst_1 : CategoryTheory.Category.{v', u'} D]
  {FD : D → D → Type u_1} {CD : D → Type w} [inst_2 : (X Y : D) → FunLike (FD X Y) (CD X) (CD Y)]
  [inst_3 : CategoryTheory.ConcreteCategory D FD] (J : CategoryTheory.GrothendieckTopology C)
  {F₁ F₂ : CategoryTheory.Functor Cᵒᵖ D} (φ : F₁ ⟶ F₂) [CategoryTheory.IsIso φ],
  CategoryTheory.Presheaf.IsLocallyInjective J φ
-- Mathlib.Algebra.Homology.ShortComplex.ModuleCat
CategoryTheory.ShortComplex.moduleCatCyclesIso_inv_iCycles_assoc_apply : ∀ {R : Type u} [inst : Ring R] (S : CategoryTheory.ShortComplex (ModuleCat R)) {Z : ModuleCat R} (h : S.X₂ ⟶ Z)
  (x : ↑S.moduleCatLeftHomologyData.K),
  (CategoryTheory.ConcreteCategory.hom h)
      ((CategoryTheory.ConcreteCategory.hom S.iCycles)
        ((CategoryTheory.ConcreteCategory.hom S.moduleCatCyclesIso.inv) x)) =
    (CategoryTheory.ConcreteCategory.hom h) ((CategoryTheory.ConcreteCategory.hom S.moduleCatLeftHomologyData.i) x)
-- Init.Data.Iterators.Lemmas.Combinators.FlatMap
Std.Iter.flatMap.eq_1 : ∀ {α β α₂ γ : Type w} [inst : Std.Iterator α Id β] [inst_1 : Std.Iterator α₂ Id γ] (f : β → Std.Iter γ)
  (it : Std.Iter β), Std.Iter.flatMap f it = Std.Iter.flatMapAfter f it none
-- Init.Data.Order.Ord
/-- If two values compare equal, then they are boolean equal.  -/
Std.LawfulBEqCmp.compare_eq_iff_beq : ∀ {α : Type u} {inst : BEq α} {cmp : α → α → Ordering} [self : Std.LawfulBEqCmp cmp] {a b : α},
  cmp a b = Ordering.eq ↔ (a == b) = true
-- Mathlib.Analysis.Convex.Function
/-- A linear map is concave.  -/
LinearMap.concaveOn : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : Module 𝕜 E] [inst_6 : Module 𝕜 β] (f : E →ₗ[𝕜] β)
  {s : Set E}, Convex 𝕜 s → ConcaveOn 𝕜 s ⇑f
-- Mathlib.Analysis.Normed.Group.Pointwise
singleton_add_closedBall_zero : ∀ {E : Type u_1} [inst : SeminormedAddCommGroup E] (δ : ℝ) (x : E), {x} + Metric.closedBall 0 δ = Metric.closedBall x δ
-- Mathlib.Probability.ProbabilityMassFunction.Basic
PMF.toOuterMeasure_apply_fintype : ∀ {α : Type u_1} (p : PMF α) (s : Set α) [inst : Fintype α], p.toOuterMeasure s = ∑ x, s.indicator (⇑p) x
-- Mathlib.Tactic.Abel
/-- Interpret a negated expression in `abel`'s normal form.
 -/
Mathlib.Tactic.Abel.evalNeg : Mathlib.Tactic.Abel.NormalExpr → Mathlib.Tactic.Abel.M (Mathlib.Tactic.Abel.NormalExpr × Lean.Expr)
-- Mathlib.Data.Fin.Embedding
Fin.natAdd_castLEEmb_apply_val : ∀ {n m : ℕ} (hmn : n ≤ m) (a : Fin n), ↑((Fin.natAdd_castLEEmb hmn) a) = ↑a + (m - n)
-- Mathlib.FieldTheory.Finite.Basic
ZMod.sq_add_sq : ∀ (p : ℕ) [hp : Fact (Nat.Prime p)] (x : ZMod p), ∃ a b, a ^ 2 + b ^ 2 = x
-- Lean.Server.Requests
Lean.Server.statefulRequestHandlers : IO.Ref (Lean.PersistentHashMap String Lean.Server.StatefulRequestHandler)
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.symm_refl : ∀ {G : Type u_1} [inst : Add G] (a : G), (AddConstEquiv.refl a).symm = AddConstEquiv.refl a
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.id_def : ∀ {B : Type u} [inst : Quiver B] {a : CategoryTheory.FreeBicategory B},
  CategoryTheory.FreeBicategory.Hom.id a = CategoryTheory.CategoryStruct.id a
-- Init.Simproc
/-- Auxiliary attribute for builtin symbolic evaluation procedures.
 -/
Lean.Parser.Attr.sevalprocBuiltinAttr : Lean.ParserDescr
-- Mathlib.Algebra.Group.Basic
zpow_mul' : ∀ {α : Type u_1} [inst : DivisionMonoid α] (a : α) (m n : ℤ), a ^ (m * n) = (a ^ n) ^ m
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalLeftAction.actionHomRight_hom_inv' : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalLeftAction C D] (x : C) {y z : D} (f : y ⟶ z)
  [inst_4 : CategoryTheory.IsIso f],
  CategoryTheory.CategoryStruct.comp (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x f)
      (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionHomRight x (CategoryTheory.inv f)) =
    CategoryTheory.CategoryStruct.id (CategoryTheory.MonoidalCategory.MonoidalLeftActionStruct.actionObj x y)
-- Mathlib.Tactic.WithoutCDot
_private.Mathlib.Tactic.WithoutCDot.0.Lean.Elab.Term.withoutCDotContents : Lean.Parser.Parser
-- Mathlib.Data.Int.ModEq
Int.neg_modEq_neg : ∀ {n a b : ℤ}, -a ≡ -b [ZMOD n] ↔ a ≡ b [ZMOD n]
-- Mathlib.CategoryTheory.Limits.ConeCategory
CategoryTheory.Limits.Cone.toStructuredArrowCompToUnderCompForget_inv_app : ∀ {J : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} J] {C : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} C]
  {F : CategoryTheory.Functor J C} (c : CategoryTheory.Limits.Cone F) (X : J),
  c.toStructuredArrowCompToUnderCompForget.inv.app X = CategoryTheory.CategoryStruct.id (F.obj X)
-- Mathlib.Geometry.Convex.Cone.Basic
convexHull_toCone_eq_sInf : ∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] (s : Set M), Convex.toCone ((convexHull 𝕜) s) ⋯ = sInf {t | s ⊆ ↑t}
-- Mathlib.Order.BoundedOrder.Basic
top_unique : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, ⊤ ≤ a → a = ⊤
-- Mathlib.SetTheory.ZFC.PSet
PSet.mem_def : ∀ {x y : PSet.{u_1}}, x ∈ y ↔ ∃ b, x.Equiv (y.Func b)
-- Mathlib.AlgebraicGeometry.ProjectiveSpectrum.Topology
ProjectiveSpectrum.sup_vanishingIdeal_le : ∀ {A : Type u_1} {σ : Type u_2} [inst : CommRing A] [inst_1 : SetLike σ A] [inst_2 : AddSubmonoidClass σ A] (𝒜 : ℕ → σ)
  [inst_3 : GradedRing 𝒜] (t t' : Set (ProjectiveSpectrum 𝒜)),
  ProjectiveSpectrum.vanishingIdeal t ⊔ ProjectiveSpectrum.vanishingIdeal t' ≤
    ProjectiveSpectrum.vanishingIdeal (t ∩ t')
-- Mathlib.Algebra.Group.Equiv.TypeTags
AddEquiv.toMultiplicativeLeft_apply_apply : ∀ {G : Type u_2} {H : Type u_3} [inst : AddZeroClass G] [inst_1 : MulOneClass H] (f : G ≃+ Additive H)
  (a : Multiplicative G), (AddEquiv.toMultiplicativeLeft f) a = (AddMonoidHom.toMultiplicativeLeft f.toAddMonoidHom) a
-- Std.Data.HashMap.Lemmas
Std.HashMap.getElem_congr : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {a b : α} (hab : (a == b) = true) {h' : a ∈ m}, m[a] = m[b]
-- Mathlib.Algebra.Group.Submonoid.Units
Subgroup.mem_ofUnits_iff_exists_isUnit : ∀ {M : Type u_1} [inst : Monoid M] (S : Subgroup Mˣ) (x : M), x ∈ S.ofUnits ↔ ∃ (h : IsUnit x), h.unit ∈ S
-- Mathlib.Computability.TuringMachine.PostTuringMachine
_private.Mathlib.Computability.TuringMachine.PostTuringMachine.0.Turing.TM1to0.trCfg.match_1.splitter : {Γ : Type u_1} →
  {Λ : Type u_2} →
    {σ : Type u_3} →
      [inst : Inhabited Γ] →
        (motive : Turing.TM1.Cfg Γ Λ σ → Sort u_4) →
          (x : Turing.TM1.Cfg Γ Λ σ) →
            ((l : Option Λ) → (v : σ) → (T : Turing.Tape Γ) → motive { l := l, var := v, Tape := T }) → motive x
-- Mathlib.Data.Num.Basic
/-- `bit0 n` appends a `0` to the end of `n`, where `bit0 n = n0`.  -/
Num.bit0 : Num → Num
-- Mathlib.Algebra.Polynomial.Eval.Degree
/-- Variant of `natDegree_map_lt` that assumes `0 < natDegree p` instead of `map f p ≠ 0`.  -/
Polynomial.natDegree_map_lt' : ∀ {R : Type u} {S : Type v} [inst : Semiring R] [inst_1 : Semiring S] {f : R →+* S} {p : Polynomial R},
  f p.leadingCoeff = 0 → 0 < p.natDegree → (Polynomial.map f p).natDegree < p.natDegree
-- Mathlib.AlgebraicTopology.SimplicialSet.PiZero
SSet.π₀Functor_map : ∀ {X Y : SSet} (f : X ⟶ Y), SSet.π₀Functor.map f = TypeCat.ofHom (SSet.mapπ₀ f)
-- Mathlib.Order.Lattice
/-- Transfer `Preorder` across an `Equiv`.  -/
Equiv.preorder : {α : Type u} → {β : Type v} → α ≃ β → [Preorder β] → Preorder α
-- Mathlib.Algebra.Polynomial.Roots
Polynomial.roots_eq_of_degree_le_card_of_ne_zero : ∀ {R : Type u} [inst : CommRing R] [inst_1 : IsDomain R] {p : Polynomial R} {S : Finset R},
  (∀ x ∈ S, Polynomial.eval x p = 0) → p.degree ≤ ↑S.card → p ≠ 0 → p.roots = S.val
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.cylinderEvents_mono : ∀ {ι : Type u_2} {X : ι → Type u_3} [m : (i : ι) → MeasurableSpace (X i)] {Δ₁ Δ₂ : Set ι},
  Δ₁ ⊆ Δ₂ → MeasureTheory.cylinderEvents Δ₁ ≤ MeasureTheory.cylinderEvents Δ₂
-- Init.Data.Iterators.Combinators.Monadic.FlatMap
Std.Iterators.Types.Flatten.instIterator : {α α₂ β : Type w} →
  {m : Type w → Type w'} →
    [Monad m] →
      [Std.Iterator α m (Std.IterM m β)] →
        [Std.Iterator α₂ m β] → Std.Iterator (Std.Iterators.Types.Flatten α α₂ β m) m β
-- Mathlib.MeasureTheory.SpecificCodomains.WithLp
MeasureTheory.snd_integral_withLp : ∀ {X : Type u_1} {mX : MeasurableSpace X} {μ : MeasureTheory.Measure X} {q : ENNReal} [inst : Fact (1 ≤ q)]
  {E : Type u_2} {F : Type u_3} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedAddCommGroup F]
  {f : X → WithLp q (E × F)} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [CompleteSpace E],
  MeasureTheory.Integrable f μ → (∫ (x : X), f x ∂μ).snd = ∫ (x : X), (f x).snd ∂μ
-- Mathlib.Order.Lattice
SemilatticeInf.ext_inf : ∀ {α : Type u_1} {A B : SemilatticeInf α}, (∀ (y x : α), y ≤ x ↔ y ≤ x) → ∀ (x y : α), x ⊓ y = x ⊓ y
-- Mathlib.Data.Vector.Zip
List.Vector.sum_add_sum_eq_sum_zipWith : ∀ {α : Type u_1} {n : ℕ} [inst : AddCommMonoid α] (x y : List.Vector α n),
  x.toList.sum + y.toList.sum = (List.Vector.zipWith (fun x1 x2 => x1 + x2) x y).toList.sum
-- Mathlib.MeasureTheory.Integral.IntervalIntegral.Basic
intervalIntegral.integral_same : ∀ {E : Type u_5} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a : ℝ} {f : ℝ → E}
  {μ : MeasureTheory.Measure ℝ}, ∫ (x : ℝ) in a..a, f x ∂μ = 0
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.Equiv.of_keysArray_unit_perm : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.TreeMap.Raw α Unit cmp},
  t₁.keysArray.Perm t₂.keysArray → t₁.Equiv t₂
-- Mathlib.SetTheory.Ordinal.Notation
ONote.NFBelow.below.oadd' : ∀ {motive : (a : ONote) → (a_1 : Ordinal.{0}) → a.NFBelow a_1 → Prop} {e : ONote} {n : ℕ+} {a : ONote}
  {eb b : Ordinal.{0}} (a_1 : e.NFBelow eb) (a_2 : a.NFBelow e.repr) (a_3 : e.repr < b),
  ONote.NFBelow.below a_1 → motive e eb a_1 → ONote.NFBelow.below a_2 → motive a e.repr a_2 → ONote.NFBelow.below ⋯
-- Mathlib.Algebra.Group.ConjFinite
instFiniteConjClasses : ∀ {α : Type u_1} [inst : Monoid α] [Finite α], Finite (ConjClasses α)
-- Mathlib.Algebra.Group.WithOne.Basic
/-- A version of `Equiv.optionCongr` for `WithOne`.  -/
MulEquiv.withOneCongr : {α : Type u} → {β : Type v} → [inst : Mul α] → [inst_1 : Mul β] → α ≃* β → WithOne α ≃* WithOne β
-- Mathlib.RingTheory.FreeRing
FreeRing.hom_ext_iff : ∀ {α : Type u} {R : Type v} [inst : Ring R] {f g : FreeRing α →+* R},
  f = g ↔ ∀ (x : α), f (FreeRing.of x) = g (FreeRing.of x)
-- Init.Data.SInt.Lemmas
Int32.sub_eq_iff_eq_add : ∀ {a b c : Int32}, a - b = c ↔ a = c + b
-- Mathlib.RingTheory.TensorProduct.DirectLimitFG
/-- When `Q` ranges over finitely generated submodules of `N`,
the modules of the form `M ⊗[R] Q` form a directed system.  -/
Submodule.FG.lTensor.directedSystem : ∀ (R : Type u) (M : Type u_1) (N : Type u_2) [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [inst_3 : AddCommMonoid N] [inst_4 : Module R N],
  DirectedSystem (fun Q => TensorProduct R M ↥↑Q) fun x x_1 hPQ => ⇑(LinearMap.lTensor M (Submodule.inclusion hPQ))
-- Mathlib.Algebra.GroupWithZero.Basic
/-- Dividing `a` by the result of dividing `a` by itself results in
`a` (whether or not `a` is zero).  -/
div_div_self : ∀ {G₀ : Type u_2} [inst : GroupWithZero G₀] (a : G₀), a / (a / a) = a
-- Mathlib.Analysis.Normed.Unbundled.RingSeminorm
RingSeminorm.exists_index_pow_le : ∀ {R : Type u_1} [inst : CommRing R] (p : RingSeminorm R),
  IsNonarchimedean ⇑p →
    ∀ (x y : R) (n : ℕ), ∃ m < n + 1, p ((x + y) ^ n) ^ (1 / ↑n) ≤ (p (x ^ m) * p (y ^ (n - m))) ^ (1 / ↑n)
-- Mathlib.RingTheory.WittVector.MulCoeff
WittVector.wittPolyProdRemainder.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] (n n_1 : ℕ),
  n = n_1 → WittVector.wittPolyProdRemainder p n = WittVector.wittPolyProdRemainder p_1 n_1
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.inl_snd_assoc : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {d e f : ℤ} (γ : CochainComplex.HomComplex.Cochain G K d) (he : 0 + d = e) (hf : -1 + e = f),
  (CochainComplex.mappingCone.inl φ).comp ((CochainComplex.mappingCone.snd φ).comp γ he) hf = 0
-- Lean.Meta.SizeOf
_private.Lean.Meta.SizeOf.0.Lean.Meta.mkLocalInstances.loop : {α : Type} → Array Lean.Expr → (Array Lean.Expr → Lean.MetaM α) → ℕ → Array Lean.Expr → Lean.MetaM α
-- Mathlib.CategoryTheory.Monoidal.Action.Basic
CategoryTheory.MonoidalCategory.MonoidalRightAction.actionHomLeft_tensor : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.MonoidalCategory C]
  [inst_3 : CategoryTheory.MonoidalCategory.MonoidalRightAction C D] {z z' : D} (f : z ⟶ z') (x y : C),
  CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f
      (CategoryTheory.MonoidalCategoryStruct.tensorObj x y) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso z x y).hom
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft
          (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionHomLeft f x) y)
        (CategoryTheory.MonoidalCategory.MonoidalRightActionStruct.actionAssocIso z' x y).inv)
-- Lean.Util.FindExpr
Lean.Expr.FindStep.noConfusionType : Sort v✝ → Lean.Expr.FindStep → Lean.Expr.FindStep → Sort v✝
-- Mathlib.Algebra.MvPolynomial.Degrees
MvPolynomial.mem_degreesLE : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] {p : MvPolynomial σ R} {s : Multiset σ},
  p ∈ MvPolynomial.degreesLE R σ s ↔ p.degrees ≤ s
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Tripartite
SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint.inj₁ : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {t : Finset (α × β × γ)}
  [self : SimpleGraph.TripartiteFromTriangles.ExplicitDisjoint t] ⦃a : α⦄ ⦃b : β⦄ ⦃c : γ⦄ ⦃b' : β⦄,
  (a, b, c) ∈ t → (a, b', c) ∈ t → b = b'
-- Std.Data.Iterators.Lemmas.Producers.Monadic.Vector
Vector.length_iterM : ∀ {m : Type w → Type w'} [inst : Monad m] {β : Type w} {n : ℕ} [LawfulMonad m] {xs : Vector β n},
  (xs.iterM m).length = pure { down := n }
-- Lean.Setup
Lean.IRPhases.comptime.sizeOf_spec : sizeOf Lean.IRPhases.comptime = 1
-- Mathlib.Probability.Kernel.IonescuTulcea.PartialTraj
ProbabilityTheory.Kernel.partialTraj.eq_1 : ∀ {X : ℕ → Type u_1} {mX : (n : ℕ) → MeasurableSpace (X n)}
  (κ : (n : ℕ) → ProbabilityTheory.Kernel ((i : ↥(Finset.Iic n)) → X ↑i) (X (n + 1))) (a b : ℕ),
  ProbabilityTheory.Kernel.partialTraj κ a b =
    if h : b ≤ a then ProbabilityTheory.Kernel.deterministic (Preorder.frestrictLe₂ h) ⋯
    else
      Nat.leRec ProbabilityTheory.Kernel.id
        (fun k x κ_k =>
          ((ProbabilityTheory.Kernel.id.prod ((κ k).map ⇑(MeasurableEquiv.piSingleton k))).comp κ_k).map
            (IicProdIoc k (k + 1)))
        ⋯
-- Mathlib.Data.Fintype.Vector
List.Vector.instFintype : {α : Type u_1} → [Fintype α] → {n : ℕ} → Fintype (List.Vector α n)
-- Init.Data.Range.Polymorphic.Int
Std.PRange.instLawfulUpwardEnumerableInt : Std.PRange.LawfulUpwardEnumerable ℤ
-- Mathlib.NumberTheory.NumberField.CanonicalEmbedding.FundamentalCone
NumberField.mixedEmbedding.fundamentalCone.integerSetTorsionSMul_smul_coe : ∀ {K : Type u_1} [inst : Field K] [inst_1 : NumberField K] (x : ↥(NumberField.Units.torsion K))
  (x_1 : ↑(NumberField.mixedEmbedding.fundamentalCone.integerSet K)), ↑(x • x_1) = ↑x • ↑x_1
-- Mathlib.Combinatorics.SimpleGraph.Finite
SimpleGraph.edgeFinset_eq_empty : ∀ {V : Type u_1} {G : SimpleGraph V} [inst : Fintype ↑G.edgeSet], G.edgeFinset = ∅ ↔ G = ⊥
-- Mathlib.RingTheory.Valuation.ValuativeRel.Basic
ValuativeRel.veq_rfl : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : ValuativeRel R] {x : R}, x =ᵥ x
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.exists_iff_exists_finsupp : ∀ {R : Type u} [inst : Semiring R] (P : Polynomial R → Prop), (∃ p, P p) ↔ ∃ q, P { toFinsupp := q }
-- Mathlib.Topology.MetricSpace.Lipschitz
LipschitzOnWith.mk_one : ∀ {α : Type u} {β : Type v} [inst : PseudoMetricSpace α] [inst_1 : PseudoMetricSpace β] {s : Set α} {f : α → β},
  (∀ x ∈ s, ∀ y ∈ s, dist (f x) (f y) ≤ dist x y) → LipschitzOnWith 1 f s
-- Mathlib.Combinatorics.SimpleGraph.Ends.Properties
SimpleGraph.instIsEmptyElemForallObjOppositeFinsetComponentComplFunctorEndOfFinite : ∀ {V : Type} (G : SimpleGraph V) [Finite V], IsEmpty ↑G.end
-- Mathlib.CategoryTheory.ObjectProperty.EpiMono
CategoryTheory.ObjectProperty.instIsClosedUnderIsomorphisms_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (P : CategoryTheory.ObjectProperty C)
  [P.IsClosedUnderQuotients], P.IsClosedUnderIsomorphisms
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.bot_lt_mul : ∀ {α : Type u_1} [inst : DecidableEq α] [inst_1 : MulZeroClass α] [inst_2 : LT α] {a b : WithBot α},
  ⊥ < a → ⊥ < b → ⊥ < a * b
-- Mathlib.Algebra.Order.UpperLower
_private.Mathlib.Algebra.Order.UpperLower.0.UpperSet.one_mul : ∀ {α : Type u_1} [inst : CommGroup α] [inst_1 : Preorder α] [inst_2 : IsOrderedMonoid α] (s : UpperSet α), 1 * s = s
-- Mathlib.Algebra.Group.Subgroup.Map
AddSubgroup.map_equiv_eq_comap_symm' : ∀ {G : Type u_1} [inst : AddGroup G] {N : Type u_5} [inst_1 : AddGroup N] (f : G ≃+ N) (K : AddSubgroup G),
  AddSubgroup.map f.toAddMonoidHom K = AddSubgroup.comap f.symm.toAddMonoidHom K
-- Mathlib.Algebra.Order.Interval.Basic
instNegInterval : {α : Type u_2} → [inst : AddCommGroup α] → [inst_1 : PartialOrder α] → [IsOrderedAddMonoid α] → Neg (Interval α)
-- Std.Do.SPred.SPred
Std.Do.SPred.not_nil : ∀ {P : Std.Do.SPred []}, spred(¬P) = { down := ¬P.down }
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
/-- Constructor for morphisms to `(t.truncLT n₁).obj Y`.  -/
CategoryTheory.Triangulated.TStructure.liftTruncLT : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} 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] →
              (t : CategoryTheory.Triangulated.TStructure C) →
                {X Y : C} → (X ⟶ Y) → (n₀ n₁ : ℤ) → n₀ + 1 = n₁ → [t.IsLE X n₀] → X ⟶ (t.truncLT n₁).obj Y
-- Std.Time.Zoned.Database.TzIf
/-- The count of UT local indicators in the file.
 -/
Std.Time.TimeZone.TZif.Header.isutcnt : Std.Time.TimeZone.TZif.Header → UInt32
-- Init.Data.BitVec.Decidable
BitVec.instDecidableExistsBitVecSucc : {n : ℕ} →
  (P : BitVec (n + 1) → Prop) →
    [DecidablePred P] → [Decidable (∀ (x : Bool) (v : BitVec n), ¬P (BitVec.cons x v))] → Decidable (∃ v, P v)
-- Lean.Expr
/-- Returns the "raw" natural number `.lit (.natVal n)`.
This is not the default representation used by the Lean frontend.
See `mkNatLit`.
 -/
Lean.mkRawNatLit : ℕ → Lean.Expr
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get?_insertMany_list_of_mem : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m : Std.DHashMap.Raw α fun x => β} [EquivBEq α]
  [LawfulHashable α],
  m.WF →
    ∀ {l : List (α × β)} {k k' : α},
      (k == k') = true →
        ∀ {v : β},
          List.Pairwise (fun a b => (a.1 == b.1) = false) l →
            (k, v) ∈ l → Std.DHashMap.Raw.Const.get? (Std.DHashMap.Raw.Const.insertMany m l) k' = some v
-- Mathlib.CategoryTheory.Limits.Cones
CategoryTheory.Limits.Cone.mk.inj : ∀ {J : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} J} {C : Type u₃} {inst_1 : CategoryTheory.Category.{v₃, u₃} C}
  {F : CategoryTheory.Functor J C} {pt : C} {π : (CategoryTheory.Functor.const J).obj pt ⟶ F} {pt_1 : C}
  {π_1 : (CategoryTheory.Functor.const J).obj pt_1 ⟶ F},
  { pt := pt, π := π } = { pt := pt_1, π := π_1 } → pt = pt_1 ∧ π ≍ π_1
-- Mathlib.Algebra.Group.Irreducible.Indecomposable
IsMulIndecomposable.mem_or_inv_mem_closure_baseOf : ∀ {ι : Type u_1} {G : Type u_3} {S : Type u_4} [inst : CommGroup G] [inst_1 : LinearOrder S] [Finite ι]
  [inst_3 : InvolutiveInv ι] [inst_4 : CommGroup S] [IsOrderedMonoid S] (v : ι → G) (f : G →* S) (i : ι),
  f (v i) ≠ 1 →
    v i⁻¹ = (v i)⁻¹ →
      v i ∈ Submonoid.closure (v '' IsMulIndecomposable.baseOf v f) ∨
        (v i)⁻¹ ∈ Submonoid.closure (v '' IsMulIndecomposable.baseOf v f)