mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.LinearAlgebra.RootSystem.GeckConstruction.Basic
RootPairing.GeckConstruction.cartanSubalgebra_eq_lieSpan : ∀ {ι : 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}
  [inst_5 : P.IsCrystallographic] (b : P.Base) [inst_6 : Fintype ι] [inst_7 : DecidableEq ι],
  RootPairing.GeckConstruction.cartanSubalgebra b =
    LieSubalgebra.lieSpan R (Matrix (↥b.support ⊕ ι) (↥b.support ⊕ ι) R) (Set.range RootPairing.GeckConstruction.h)
-- Mathlib.CategoryTheory.Products.Basic
CategoryTheory.functorProdFunctorEquiv_unitIso : ∀ (A : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} A] (B : Type u₂) [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  (C : Type u₃) [inst_2 : CategoryTheory.Category.{v₃, u₃} C],
  (CategoryTheory.functorProdFunctorEquiv A B C).unitIso = CategoryTheory.functorProdFunctorEquivUnitIso A B C
-- Std.Tactic.BVDecide.LRAT.Internal.Formula.Lemmas
Array.set!.eq_1 : ∀ {α : Type u_1} (xs : Array α) (i : ℕ) (v : α), xs.set! i v = xs.setIfInBounds i v
-- Mathlib.RingTheory.HahnSeries.Basic
HahnSeries.support_truncLT_subset : ∀ {Γ : Type u_1} {R : Type u_3} [inst : Zero R] [inst_1 : PartialOrder Γ] [inst_2 : DecidableLT Γ] (c : Γ)
  (x : HahnSeries Γ R), ((HahnSeries.truncLT c) x).support ⊆ x.support
-- Mathlib.Tactic.FieldSimp
/-- Given an (in)equality `a = b` (respectively, `a ≤ b`, `a < b`), cancel nonzero (resp. positive)
factors to construct a new (in)equality which is logically equivalent to `a = b` (respectively,
`a ≤ b`, `a < b`).  -/
Mathlib.Tactic.FieldSimp.reduceProp : ({u : Lean.Level} → (type : Q(Sort u)) → Lean.MetaM Q(«$type»)) → Lean.Expr → Mathlib.Tactic.AtomM Lean.Meta.Simp.Result
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Under.opEquivOpOver_inverse_obj : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] (X : T) (Y : (CategoryTheory.Over X)ᵒᵖ),
  (CategoryTheory.Under.opEquivOpOver X).inverse.obj Y = CategoryTheory.Under.mk (Opposite.unop Y).hom.op
-- Mathlib.Data.Matrix.Basic
LinearMap.mapMatrix_smul : ∀ {m : Type u_2} {n : Type u_3} {R : Type u_7} {S : Type u_8} {A : Type u_10} {α : Type u_11} {β : Type u_12}
  [inst : Semiring R] [inst_1 : Semiring S] {σᵣₛ : R →+* S} [inst_2 : AddCommMonoid α] [inst_3 : AddCommMonoid β]
  [inst_4 : Module R α] [inst_5 : Module S β] [inst_6 : Monoid A] [inst_7 : DistribMulAction A β]
  [inst_8 : SMulCommClass S A β] (a : A) (f : α →ₛₗ[σᵣₛ] β), (a • f).mapMatrix = a • f.mapMatrix
-- Mathlib.Algebra.MonoidAlgebra.PointwiseSMul
MonoidAlgebra.smul_eq : ∀ {G : Type u_1} {P : Type u_2} {R : Type u_3} {V : Type u_4} [inst : SMul G P] [inst_1 : IsLeftCancelSMul G P]
  [inst_2 : Semiring R] [inst_3 : AddCommMonoid V] [inst_4 : SMulWithZero R V] (f : MonoidAlgebra R G) (x : P → V)
  (p : P) (hp : optParam ((↑f.coeff.support).smulAntidiagonal (Function.support x) p).Finite ⋯),
  (f • x) p = ∑ gh ∈ Finset.SMulAntidiagonal p hp, f.coeff gh.1 • x gh.2
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.invOfUnit_eq : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] (φ : MvPowerSeries σ k) (h : MvPowerSeries.constantCoeff φ ≠ 0),
  φ.invOfUnit (Units.mk0 (MvPowerSeries.constantCoeff φ) h) = φ⁻¹
-- Mathlib.Algebra.Ring.Defs
CommRing.toRing : {α : Type u} → [self : CommRing α] → Ring α
-- Init.Data.Option.Attach
Option.map_attach_eq_pmap : ∀ {α : Type u_1} {β : Type u_2} {o : Option α} (f : { x // o = some x } → β),
  Option.map f o.attach = Option.pmap (fun a h => f ⟨a, h⟩) o ⋯
-- Mathlib.MeasureTheory.Group.MeasurableEquiv
MeasurableEquiv.symm_mulLeft : ∀ {G : Type u_1} [inst : Group G] [inst_1 : MeasurableSpace G] [inst_2 : MeasurableMul G] (g : G),
  (MeasurableEquiv.mulLeft g).symm = MeasurableEquiv.mulLeft g⁻¹
-- Init.Data.String.Lemmas.Intercalate
_private.Init.Data.String.Lemmas.Intercalate.0.String.intercalate.go.match_1.eq_1 : ∀ (motive : List String → Sort u_1) (a : String) (as : List String)
  (h_1 : (a : String) → (as : List String) → motive (a :: as)) (h_2 : Unit → motive []),
  (match a :: as with
    | a :: as => h_1 a as
    | [] => h_2 ()) =
    h_1 a as
-- Mathlib.Data.Set.Pairwise.Basic
Set.exists_lt_mem_inter_of_not_pairwiseDisjoint : ∀ {α : Type u_1} {ι : Type u_4} {s : Set ι} [inst : LinearOrder ι] {f : ι → Set α},
  ¬s.PairwiseDisjoint f → ∃ i ∈ s, ∃ j ∈ s, i < j ∧ ∃ x, x ∈ f i ∩ f j
-- Mathlib.Order.CompleteLattice.Basic
iSup_pair : ∀ {α : Type u_1} {β : Type u_2} [inst : CompleteLattice α] {f : β → α} {a b : β}, ⨆ x ∈ {a, b}, f x = f a ⊔ f b
-- Mathlib.MeasureTheory.MeasurableSpace.Instances
Rat.instMeasurableSingletonClass : MeasurableSingletonClass ℚ
-- Mathlib.SetTheory.Ordinal.Basic
Ordinal.type_empty : Ordinal.type emptyRelation = 0
-- Mathlib.Analysis.Calculus.Deriv.AffineMap
AffineMap.hasDerivAt_lineMap : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {a b : E} {x : 𝕜}, HasDerivAt (⇑(AffineMap.lineMap a b)) (b - a) x
-- Mathlib.Data.Multiset.Fold
Multiset.fold_hom : ∀ {α : Type u_1} {β : Type u_2} (op : α → α → α) [hc : Std.Commutative op] [ha : Std.Associative op] {op' : β → β → β}
  [inst : Std.Commutative op'] [inst_1 : Std.Associative op'] {m : α → β},
  (∀ (x y : α), m (op x y) = op' (m x) (m y)) →
    ∀ (b : α) (s : Multiset α), Multiset.fold op' (m b) (Multiset.map m s) = m (Multiset.fold op b s)
-- Init.Data.UInt.Lemmas
UInt16.toUInt8_mul : ∀ (a b : UInt16), (a * b).toUInt8 = a.toUInt8 * b.toUInt8
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.size_unitOfList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → (Std.TreeMap.Raw.unitOfList l cmp).size = l.length
-- Mathlib.Algebra.Homology.Embedding.ExtendHomology
HomologicalComplex.extend.d_comp_eq_zero_iff : ∀ {ι : Type u_1} {ι' : Type u_2} {c : ComplexShape ι} {c' : ComplexShape ι'} {C : Type u_3}
  [inst : CategoryTheory.Category.{v_1, u_3} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] (K : HomologicalComplex C c) (e : c.Embedding c') {i j : ι}
  {i' j' : ι'} (hj' : e.f j = j'),
  c.prev j = i →
    c'.prev j' = i' →
      ∀ ⦃W : C⦄ (φ : K.X j ⟶ W),
        CategoryTheory.CategoryStruct.comp (K.d i j) φ = 0 ↔
          CategoryTheory.CategoryStruct.comp ((K.extend e).d i' j')
              (CategoryTheory.CategoryStruct.comp (K.extendXIso e hj').hom φ) =
            0
-- Batteries.Data.String.Lemmas
_private.Batteries.Data.String.Lemmas.0.Substring.Raw.toLegacyIterator.match_1.eq_1 : ∀ (motive : Substring.Raw → Sort u_1) (s : String) (b stopPos : String.Pos.Raw)
  (h_1 : (s : String) → (b stopPos : String.Pos.Raw) → motive { str := s, startPos := b, stopPos := stopPos }),
  (match { str := s, startPos := b, stopPos := stopPos } with
    | { str := s, startPos := b, stopPos := stopPos } => h_1 s b stopPos) =
    h_1 s b stopPos
-- Mathlib.Algebra.Homology.ShortComplex.SnakeLemma
CategoryTheory.ShortComplex.SnakeInput.Hom.comm₁₂ : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  {S₁ S₂ : CategoryTheory.ShortComplex.SnakeInput C} (self : S₁.Hom S₂),
  CategoryTheory.CategoryStruct.comp self.f₁ S₂.v₁₂ = CategoryTheory.CategoryStruct.comp S₁.v₁₂ self.f₂
-- Mathlib.RingTheory.Ideal.KrullsHeightTheorem
/-- If `P` lies over `p`, the height of `P` is bounded by the height of `p` plus
the height of the image of `P` in `S ⧸ p S`.
Equality holds if `S` satisfies going-down as an `R`-algebra
(see `Ideal.height_eq_height_add_of_liesOver_of_hasGoingDown`).
 -/
Ideal.height_le_height_add_of_liesOver : ∀ {R : Type u_1} [inst : CommRing R] [IsNoetherianRing R] {S : Type u_2} [inst_2 : CommRing S] [inst_3 : Algebra R S]
  [IsNoetherianRing S] (p : Ideal R) [p.IsPrime] (P : Ideal S) [P.IsPrime] [P.LiesOver p],
  P.height ≤ p.height + (Ideal.map (Ideal.Quotient.mk (Ideal.map (algebraMap R S) p)) P).height
-- Mathlib.Algebra.MonoidAlgebra.Degree
AddMonoidAlgebra.leadingCoeff_add_eq_right : ∀ {R : Type u_1} {A : Type u_3} {B : Type u_5} [inst : Semiring R] [inst_1 : LinearOrder B] [inst_2 : OrderBot B]
  {p q : AddMonoidAlgebra R A} {D : A → B} [inst_3 : AddZeroClass A],
  AddMonoidAlgebra.supDegree D p < AddMonoidAlgebra.supDegree D q →
    AddMonoidAlgebra.leadingCoeff D (p + q) = AddMonoidAlgebra.leadingCoeff D q
-- Mathlib.Data.Fintype.Inv
Function.Injective.invOfMemRange.congr_simp : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype α] {inst_1 : DecidableEq β} [inst_2 : DecidableEq β] {f : α → β}
  (hf : Function.Injective f) (a a_1 : ↑(Set.range f)), a = a_1 → hf.invOfMemRange a = hf.invOfMemRange a_1
-- Mathlib.LinearAlgebra.FiniteDimensional.Defs
/-- The submodule generated by a finset is finite-dimensional.  -/
FiniteDimensional.span_finset : ∀ (K : Type u) {V : Type v} [inst : DivisionRing K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] (s : Finset V),
  FiniteDimensional K ↥(Submodule.span K ↑s)
-- Mathlib.Tactic.NormNum.Irrational
/-- Finds `k` such that `k ^ n < m < (k + 1) ^ n` using bisection method. It assumes `n > 0`.  -/
Mathlib.Meta.NormNum.findNotPowerCertificateCore : ℕ → ℕ → Option ℕ
-- Mathlib.SetTheory.Cardinal.Cofinality.Ordinal
/-- The cofinality on an ordinal is the `Order.cof` of any isomorphic linear order.

In particular, `cof 0 = 0` and `cof (succ o) = 1`.  -/
Ordinal.cof : Ordinal.{u} → Cardinal.{u}
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
/-- **Alias** of the reverse direction of `Left.neg_pos_iff`.

---

Uses `left` co(ntra)variant.  -/
neg_pos_of_neg : ∀ {α : Type u} [inst : AddGroup α] [inst_1 : LT α] [AddLeftStrictMono α] {a : α}, a < 0 → 0 < -a
-- Mathlib.Algebra.Group.Submonoid.Operations
Submonoid.equivMapOfInjective.eq_1 : ∀ {N : Type u_2} [inst : MulOneClass N] {M : Type u_5} [inst_1 : MulOneClass M] (S : Submonoid M) (f : M →* N)
  (hf : Function.Injective ⇑f), S.equivMapOfInjective f hf = { toEquiv := Equiv.Set.image (⇑f) (↑S) hf, map_mul' := ⋯ }
-- Mathlib.Logic.Equiv.Defs
Equiv.trans_cancel_right : ∀ {α : Sort u} {β : Sort v} {γ : Sort w} (e : α ≃ β) (f : β ≃ γ) (g : α ≃ γ), e.trans f = g ↔ e = g.trans f.symm
-- Mathlib.CategoryTheory.Subobject.ArtinianObject
/-- The monomorphism from the arbitrary simple subobject of a non-zero Artinian object.  -/
CategoryTheory.simpleSubobjectArrow : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        {X : C} →
          [inst_3 : CategoryTheory.IsArtinianObject X] →
            (h : ¬CategoryTheory.Limits.IsZero X) → CategoryTheory.simpleSubobject h ⟶ X
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- The type of morphisms in the category `Under`.  -/
CategoryTheory.Under.Hom : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {X : T} → CategoryTheory.Under X → CategoryTheory.Under X → Type (max 0 v₁)
-- Mathlib.Topology.Order.Hom.Esakia
EsakiaHom.comp_id : ∀ {α : Type u_2} {β : Type u_3} [inst : TopologicalSpace α] [inst_1 : Preorder α] [inst_2 : TopologicalSpace β]
  [inst_3 : Preorder β] (f : EsakiaHom α β), f.comp (EsakiaHom.id α) = f
-- Mathlib.LinearAlgebra.Complex.Module
/-- The scalar action of `ℝ` on a `ℂ`-module `E` induced by `Module.complexToReal` commutes with
another scalar action of `M` on `E` whenever the action of `ℂ` commutes with the action of `M`.  -/
SMulCommClass.complexToReal : ∀ {M : Type u_1} {E : Type u_2} [inst : AddCommGroup E] [inst_1 : Module ℂ E] [inst_2 : SMul M E] [SMulCommClass ℂ M E],
  SMulCommClass ℝ M E
-- Mathlib.Analysis.SpecialFunctions.Trigonometric.DerivHyp
/-- **Alias** of the reverse direction of `Real.sinh_nonneg_iff`. -/
Mathlib.Meta.Positivity.sinh_nonneg_of_nonneg : ∀ {x : ℝ}, 0 ≤ x → 0 ≤ Real.sinh x
-- Mathlib.ModelTheory.Syntax
FirstOrder.Language.Term.subst.eq_def : ∀ {L : FirstOrder.Language} {α : Type u'} {β : Type v'} (x : L.Term α) (x_1 : α → L.Term β),
  x.subst x_1 =
    match x, x_1 with
    | FirstOrder.Language.var a, tf => tf a
    | FirstOrder.Language.func f ts, tf => FirstOrder.Language.func f fun i => (ts i).subst tf
-- Mathlib.Order.ModularLattice
IsModularLattice.complementedLattice_Iic : ∀ {α : Type u_1} [inst : Lattice α] [IsModularLattice α] {a : α} [inst_2 : BoundedOrder α] [ComplementedLattice α],
  ComplementedLattice ↑(Set.Iic a)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.minKey_insertIfNew_of_isEmpty : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {t : Std.DTreeMap.Internal.Impl α β} [inst : Std.TransOrd α]
  (h : t.WF) {k : α} {v : β k}, t.isEmpty = true → (Std.DTreeMap.Internal.Impl.insertIfNew k v t ⋯).impl.minKey ⋯ = k
-- Lean.Data.Json.FromToJson.Basic
Lean.instToJsonUSize : Lean.ToJson USize
-- Mathlib.NumberTheory.ModularForms.QExpansion
/-- The qExpansion map as a map from the graded ring of modular forms to power series over `ℂ`.  -/
ModularForm.qExpansionRingHom : {Γ : Subgroup (GL (Fin 2) ℝ)} →
  (h : ℝ) →
    [inst : Γ.HasDetPlusMinusOne] →
      0 < h → h ∈ Γ.strictPeriods → (DirectSum ℤ fun k => ModularForm Γ k) →+* PowerSeries ℂ
-- Init.Data.Slice.List.Lemmas
List.mkSlice_roo_eq_mkSlice_rco : ∀ {α : Type u_1} {xs : List α} {lo hi : ℕ},
  (Std.Roo.Sliceable.mkSlice xs lo<...hi) = Std.Rco.Sliceable.mkSlice xs (lo + 1)...hi
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Mon
CategoryTheory.MonObj.one_eq_one : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  (M : C) [inst_2 : CategoryTheory.MonObj M], CategoryTheory.MonObj.one = 1
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.continuousAt_logb_iff : ∀ {b x : ℝ}, 0 < b → b ≠ 1 → (ContinuousAt (Real.logb b) x ↔ x ≠ 0)
-- Mathlib.Logic.Pairwise
Pairwise.eq : ∀ {α : Type u_1} {r : α → α → Prop} {a b : α}, Pairwise r → ¬r a b → a = b
-- Mathlib.CategoryTheory.Monoidal.Braided.Multifunctor
/-- The bottom right map in the reverse hexagon identity.  -/
CategoryTheory.BraidedCategory.ofBifunctor.Reverse.secondMap₃ : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.MonoidalCategory C] →
      (CategoryTheory.MonoidalCategory.curriedTensor C ≅ (CategoryTheory.MonoidalCategory.curriedTensor C).flip) →
        (CategoryTheory.BraidedCategory.Hexagon.functor₁₃₂ C ⟶ CategoryTheory.BraidedCategory.Hexagon.functor₃₁₂ C)
-- Lean.Compiler.ExternAttr
Lean.instHashableExternEntry.hash : Lean.ExternEntry → UInt64
-- Init.Data.UInt.IntToBitVec
USize.toBitVec64_xor : ∀ (a b : USize) (h : System.Platform.numBits = 64), (a ^^^ b).toBitVec64 h = a.toBitVec64 h ^^^ b.toBitVec64 h
-- Mathlib.RingTheory.LocalProperties.Submodule
Submodule.eq_top_of_localization₀_maximal : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  (Mₚ : (P : Ideal R) → [P.IsMaximal] → Type u_5) [inst_3 : (P : Ideal R) → [inst : P.IsMaximal] → AddCommMonoid (Mₚ P)]
  [inst_4 : (P : Ideal R) → [inst_4 : P.IsMaximal] → Module R (Mₚ P)]
  (f : (P : Ideal R) → [inst_5 : P.IsMaximal] → M →ₗ[R] Mₚ P)
  [inst_5 : ∀ (P : Ideal R) [inst_5 : P.IsMaximal], IsLocalizedModule P.primeCompl (f P)] (N : Submodule R M),
  (∀ (P : Ideal R) [inst_6 : P.IsMaximal], Submodule.localized₀ P.primeCompl (f P) N = ⊤) → N = ⊤
-- Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable
_private.Mathlib.NumberTheory.ModularForms.EisensteinSeries.E2.Summable.0.EisensteinSeries.aux_tsum_identity_2 : ∀ (z : UpperHalfPlane) (d : ℕ+),
  ∑' (m : ℕ+), (1 / (↑↑m * ↑z - ↑↑d) + 1 / (-↑↑m * ↑z + -↑↑d) - 1 / (↑↑m * ↑z + ↑↑d) - 1 / (-↑↑m * ↑z + ↑↑d)) =
    2 / ↑z * ∑' (m : ℕ+), (1 / (-↑↑d / ↑z - ↑↑m) + 1 / (-↑↑d / ↑z + ↑↑m))
-- Mathlib.Probability.Process.HittingTime
MeasureTheory.hittingBtwn_eq_end_iff : ∀ {Ω : Type u_1} {β : Type u_2} {ι : Type u_3} [inst : ConditionallyCompleteLinearOrder ι] {u : ι → Ω → β} {s : Set β}
  {n : ι} {ω : Ω} {m : ι},
  MeasureTheory.hittingBtwn u s n m ω = m ↔ (∃ j ∈ Set.Icc n m, u j ω ∈ s) → sInf (Set.Icc n m ∩ {i | u i ω ∈ s}) = m
-- Mathlib.Tactic.Determinant.Bird.Cert
/-- Build a zero certificate from a proof `lhs = 0`.  -/
Mathlib.Tactic.Determinant.zeroCertOfProof : {u : Lean.Level} →
  {α : Q(Type u)} → {rα : Q(CommRing «$α»)} → {lhs : Q(«$α»)} → Q(«$lhs» = 0) → Mathlib.Tactic.Determinant.Cert rα
-- Std.Http.Data.Response
Std.Http.Response.instToStringHead : ToString Std.Http.Response.Head
-- Mathlib.Tactic.NormDet
/-- Normalize the determinant of `A` from its `entries` in row-major order  -/
_private.Mathlib.Tactic.NormDet.0.normalizeDetFromEntries : {u : Lean.Level} →
  {α : Q(Type u)} →
    {n : Q(ℕ)} →
      Q(CommRing «$α») → Q(Matrix (Fin «$n») (Fin «$n») «$α») → Array Q(«$α») → Lean.MetaM Lean.Meta.Simp.Result
-- Mathlib.SetTheory.Lists
/-- Copy over the decidability to the `Setoid` instance.  -/
Lists.instDecidableRelEquiv : {α : Type u_1} → [DecidableEq α] → DecidableRel fun x1 x2 => x1 ≈ x2
-- Mathlib.Topology.EMetricSpace.Defs
edist_congr_right : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y z : α}, edist x y = 0 → edist x z = edist y z
-- Mathlib.CategoryTheory.Monad.Types
CategoryTheory.kleisliCatEquivKleisli_inverse_map : ∀ (m : Type u → Type u) [inst : Monad m] [inst_1 : LawfulMonad m]
  {X Y : CategoryTheory.Kleisli (CategoryTheory.ofTypeMonad m)} (f : X ⟶ Y) (x : X.of),
  (CategoryTheory.kleisliCatEquivKleisli m).inverse.map f x = (CategoryTheory.ConcreteCategory.hom f.of) x
-- Lean.Parser.Attr
/-- Sets the tactic's name.

Ordinarily, tactic names are automatically set to the first token in the tactic's parser. If this
process fails, or if the tactic's name should be multiple tokens (e.g. `let rec`), then this
attribute can be used to provide a name.

The tactic's name is used in documentation as well as in completion. Thus, the name should be a
valid prefix of the tactic's syntax.
 -/
Lean.Parser.Attr.tactic_name : Lean.Parser.Parser
-- Mathlib.Order.Interval.Finset.Floor
Int.cast_mem_Ioc_iff : ∀ {α : Type u_1} [inst : Ring α] [inst_1 : LinearOrder α] [inst_2 : FloorRing α] {a b : α} {n : ℤ},
  ↑n ∈ Set.Ioc a b ↔ n ∈ Finset.Ioc ⌊a⌋ ⌊b⌋
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.max?_eq_none_iff : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet α cmp} [Std.TransCmp cmp], t.max? = none ↔ t.isEmpty = true
-- Mathlib.Data.Bool.Basic
Bool.xor_iff_ne : ∀ {x y : Bool}, (x ^^ y) = true ↔ x ≠ y
-- Std.Data.HashSet.RawLemmas
Std.HashSet.Raw.size_insertMany_list_le : ∀ {α : Type u} {m : Std.HashSet.Raw α} [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α] [LawfulHashable α],
  m.WF → ∀ {l : List α}, (m.insertMany l).size ≤ m.size + l.length
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.instIsGEObjTruncLT : ∀ {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) [CategoryTheory.IsTriangulated C] (X : C) (a b : ℤ) [t.IsGE X a],
  t.IsGE ((t.truncLT b).obj X) a
-- Mathlib.Order.InitialSeg
PrincipalSeg.instCoeOutRelEmbedding : {α : Type u_1} → {β : Type u_2} → {r : α → α → Prop} → {s : β → β → Prop} → CoeOut (PrincipalSeg r s) (r ↪r s)
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem_toArray_rcc : ∀ {m n i : ℕ} (_h : i < (m...=n).toArray.size), (m...=n).toArray[i] = m + i
-- Init.Data.Range.Polymorphic.RangeIterator
Std.Rxc.Iterator.isPlausibleOutput_next : ∀ {α : Type u} {a : α} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : LE α] [inst_2 : DecidableLE α]
  {it : Std.Iter α}, it.internalState.next = some a → a ≤ it.internalState.upperBound → it.IsPlausibleOutput a
-- Mathlib.Data.List.AList
/-- Replace a key with a given value in an association list.
If the key is not present it does nothing.  -/
AList.replace : {α : Type u} → {β : α → Type v} → [DecidableEq α] → (a : α) → β a → AList β → AList β
-- Mathlib.SetTheory.Ordinal.Principal
/-- **Alias** of `Ordinal.isPrincipal_mul_omega0_opow_opow`. -/
Ordinal.principal_mul_omega0_opow_opow : ∀ (o : Ordinal.{u_1}), Ordinal.IsPrincipal (fun x1 x2 => x1 * x2) (Ordinal.omega0 ^ Ordinal.omega0 ^ o)
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.mono_homMk : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {U V : CategoryTheory.Over X} {f : U.left ⟶ V.left}
  [CategoryTheory.Mono f] (w : CategoryTheory.CategoryStruct.comp f V.hom = U.hom),
  CategoryTheory.Mono (CategoryTheory.Over.homMk f w)
-- Mathlib.MeasureTheory.Constructions.BorelSpace.Order
AEMeasurable.biInf : ∀ {α : Type u_1} {δ : Type u_4} [inst : TopologicalSpace α] {mα : MeasurableSpace α} [BorelSpace α]
  {mδ : MeasurableSpace δ} [inst_2 : ConditionallyCompleteLinearOrder α] [OrderTopology α] [SecondCountableTopology α]
  {ι : Type u_5} {μ : MeasureTheory.Measure δ} (s : Set ι) {f : ι → δ → α},
  s.Countable → (∀ i ∈ s, AEMeasurable (f i) μ) → AEMeasurable (fun b => ⨅ i ∈ s, f i b) μ
-- Mathlib.Data.Multiset.AddSub
Multiset.mem_erase_of_ne : ∀ {α : Type u_1} [inst : DecidableEq α] {a b : α} {s : Multiset α}, a ≠ b → (a ∈ s.erase b ↔ a ∈ s)
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.Even.eq_1 : ∀ {S : Type u_2} [inst : CommRing S] {m : ℕ} (ψ : DirichletCharacter S m), ψ.Even = (ψ (-1) = 1)
-- Mathlib.Combinatorics.Additive.AP.Three.Behrend
Behrend.nValue_pos : ∀ {N : ℕ}, 2 ≤ N → 0 < Behrend.nValue N
-- Mathlib.Geometry.Group.Growth.LinearLowerBound
Finset.nsmul_ssubset_nsmul_succ_of_nsmul_ne_closure : ∀ {G : Type u_1} [inst : AddGroup G] [inst_1 : DecidableEq G] {X : Finset G} {n : ℕ},
  0 ∈ X → X.Nontrivial → n • ↑X ≠ ↑(AddSubgroup.closure ↑X) → n • X ⊂ (n + 1) • X
-- Mathlib.Algebra.Star.Basic
isRegular_star_iff : ∀ {R : Type u} [inst : Mul R] [inst_1 : StarMul R] {x : R}, IsRegular (star x) ↔ IsRegular x
-- Mathlib.CategoryTheory.Galois.GaloisObjects
/-- A morphism from a connected object to a Galois object induces a map on automorphism
groups. This is a group homomorphism (see `autMapHom`).  -/
CategoryTheory.PreGaloisCategory.autMap : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {A B : C} →
        [CategoryTheory.PreGaloisCategory.IsConnected A] →
          [CategoryTheory.PreGaloisCategory.IsGalois B] → (A ⟶ B) → CategoryTheory.Aut A → CategoryTheory.Aut B
-- Std.Data.DTreeMap.Internal.Operations
Std.DTreeMap.Internal.Impl.BalancedTree.mk.sizeOf_spec : ∀ {α : Type u} {β : α → Type v} [inst : SizeOf α] [inst_1 : (a : α) → SizeOf (β a)]
  (impl : Std.DTreeMap.Internal.Impl α β) (balanced_impl : impl.Balanced),
  sizeOf { impl := impl, balanced_impl := balanced_impl } = 1 + sizeOf impl + sizeOf balanced_impl
-- Mathlib.Topology.Algebra.Group.Basic
Filter.tendsto_add_const_iff : ∀ {G : Type w} {α : Type u} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [SeparatelyContinuousAdd G] (b : G)
  {c : G} {f : α → G} {l : Filter α}, Filter.Tendsto (fun x => f x + b) l (nhds (c + b)) ↔ Filter.Tendsto f l (nhds c)
-- Mathlib.CategoryTheory.Monoidal.CommGrp_
CategoryTheory.CommGrp.trivial_grp_mul : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  [inst_2 : CategoryTheory.BraidedCategory C],
  CategoryTheory.MonObj.mul =
    (CategoryTheory.MonoidalCategoryStruct.leftUnitor (CategoryTheory.MonoidalCategoryStruct.tensorUnit C)).hom
-- Init.System.IOError
IO.Error.permissionDenied.sizeOf_spec : ∀ (filename : Option String) (osCode : UInt32) (details : String),
  sizeOf (IO.Error.permissionDenied filename osCode details) = 1 + sizeOf filename + sizeOf osCode + sizeOf details