mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Bicategory.FunctorBicategory.Oplax
CategoryTheory.Oplax.LaxTrans.OplaxFunctor.bicategory_associator_inv_as_app : ∀ (B : Type u₁) [inst : CategoryTheory.Bicategory B] (C : Type u₂) [inst_1 : CategoryTheory.Bicategory C]
  {x x_1 x_2 : CategoryTheory.OplaxFunctor B C} (x_3 : CategoryTheory.OplaxFunctor B C) (η : x ⟶ x_1) (θ : x_1 ⟶ x_2)
  (ι : x_2 ⟶ x_3) (a : B),
  (CategoryTheory.Bicategory.associator η θ ι).inv.as.app a =
    (CategoryTheory.Bicategory.associator (η.app a) (θ.app a) (ι.app a)).inv
-- Init.Notation
/-- The less-equal relation: `x ≤ y`  -/
«term_<=_» : Lean.TrailingParserDescr
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.get!_empty : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] [inst_1 : Std.LawfulEqCmp cmp]
  {a : α} [inst_2 : Inhabited (β a)], ∅.get! a = default
-- Mathlib.Topology.Order.OrderClosed
le_of_tendsto_of_tendsto' : ∀ {α : Type u} {β : Type v} [inst : TopologicalSpace α] [inst_1 : Preorder α] [t : OrderClosedTopology α] {f g : β → α}
  {b : Filter β} {a₁ a₂ : α} [hb : b.NeBot],
  Filter.Tendsto f b (nhds a₁) → Filter.Tendsto g b (nhds a₂) → (∀ (x : β), f x ≤ g x) → a₁ ≤ a₂
-- Mathlib.CategoryTheory.Subobject.Basic
CategoryTheory.Subobject.mapIsoToOrderIso_symm_apply : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (e : X ≅ Y) (a : CategoryTheory.Subobject Y),
  (RelIso.symm (CategoryTheory.Subobject.mapIsoToOrderIso e)) a = (CategoryTheory.Subobject.map e.inv).obj a
-- Mathlib.LinearAlgebra.AffineSpace.Independent
/-- If a family is affinely independent, we update any one point with a new point does not lie in
the affine span of that family, the new family is affinely independent.  -/
AffineIndependent.affineIndependent_update_of_notMem_affineSpan : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : DivisionRing k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [inst_3 : AddTorsor V P] {ι : Type u_4} [inst_4 : DecidableEq ι] {p : ι → P},
  AffineIndependent k p →
    ∀ {i : ι} {p₀ : P}, p₀ ∉ affineSpan k (p '' {x | x ≠ i}) → AffineIndependent k (Function.update p i p₀)
-- Init.Data.List.Find
_private.Init.Data.List.Find.0.List.of_findIdx?_eq_some.match_1.eq_1 : ∀ {α : Type u_1} (motive : Option α → Sort u_2) (a : α) (h_1 : (a : α) → motive (some a)) (h_2 : Unit → motive none),
  (match some a with
    | some a => h_1 a
    | none => h_2 ()) =
    h_1 a
-- Mathlib.CategoryTheory.Bicategory.Free
CategoryTheory.FreeBicategory.Hom₂.brecOn.eq : ∀ {B : Type u} [inst : Quiver B]
  {motive :
    {a b : CategoryTheory.FreeBicategory B} → (a_1 a_2 : a ⟶ b) → CategoryTheory.FreeBicategory.Hom₂ a_1 a_2 → Sort u_1}
  {a b : CategoryTheory.FreeBicategory B} {a_1 a_2 : a ⟶ b} (t : CategoryTheory.FreeBicategory.Hom₂ a_1 a_2)
  (F_1 :
    {a b : CategoryTheory.FreeBicategory B} →
      (a_3 a_4 : a ⟶ b) →
        (t : CategoryTheory.FreeBicategory.Hom₂ a_3 a_4) →
          CategoryTheory.FreeBicategory.Hom₂.below t → motive a_3 a_4 t),
  CategoryTheory.FreeBicategory.Hom₂.brecOn t F_1 = F_1 a_1 a_2 t (CategoryTheory.FreeBicategory.Hom₂.brecOn.go t F_1).2
-- Mathlib.Probability.Density
MeasureTheory.pdf.quasiMeasurePreserving_hasPDF' : ∀ {Ω : Type u_1} {E : Type u_2} [inst : MeasurableSpace E] {m : MeasurableSpace Ω} {ℙ : MeasureTheory.Measure Ω}
  {μ : MeasureTheory.Measure E} {F : Type u_3} [inst_1 : MeasurableSpace F] {ν : MeasureTheory.Measure F} (X : Ω → E)
  [MeasureTheory.HasPDF X ℙ μ] {g : E → F} [MeasureTheory.SFinite ℙ] [MeasureTheory.SigmaFinite ν],
  MeasureTheory.Measure.QuasiMeasurePreserving g μ ν → MeasureTheory.HasPDF (g ∘ X) ℙ ν
-- Init.MetaTypes
Lean.Meta.instBEqOccurrences.beq : Lean.Meta.Occurrences → Lean.Meta.Occurrences → Bool
-- Mathlib.Algebra.Ring.Rat
Rat.divInt_div_divInt_cancel_left : ∀ {x : ℤ}, x ≠ 0 → ∀ (n d : ℤ), Rat.divInt n x / Rat.divInt d x = Rat.divInt n d
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toArray_rcc_eq_empty_iff : ∀ {m n : ℤ}, (m...=n).toArray = #[] ↔ n < m
-- Mathlib.Logic.Basic
heq_iff_exists_cast_eq : ∀ {α β : Sort u} {a : α} {b : β}, a ≍ b ↔ ∃ (h : α = β), cast h a = b
-- Mathlib.Analysis.Convex.Extreme
/-- A point `x` is an extreme point of a set `A`
iff `x ∈ A` and for any `x₁`, `x₂` such that `x` belongs to the open segment `(x₁, x₂)`,
we have `x₁ = x`.  -/
mem_extremePoints_iff_left : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A : Set E} {x : E},
  x ∈ Set.extremePoints 𝕜 A ↔ x ∈ A ∧ ∀ x₁ ∈ A, ∀ x₂ ∈ A, x ∈ openSegment 𝕜 x₁ x₂ → x₁ = x
-- Mathlib.Algebra.QuadraticAlgebra.Defs
QuadraticAlgebra.im_intCast : ∀ {R : Type u_1} {a b : R} [inst : AddCommGroupWithOne R] (n : ℤ), (↑n).im = 0
-- Mathlib.Algebra.Quaternion
/-- Real part of a quaternion.  -/
QuaternionAlgebra.re : {R : Type u_1} → {a b c : R} → QuaternionAlgebra R a b c → R
-- Mathlib.Algebra.Polynomial.Degree.Defs
Polynomial.degree_sub_lt_left : ∀ {R : Type u} [inst : Ring R] {p q : Polynomial R},
  p.degree = q.degree → p ≠ 0 → p.leadingCoeff = q.leadingCoeff → (p - q).degree < p.degree
-- Init.Data.Range.Polymorphic.NatLemmas
Nat.getElem!_toList_rcc : ∀ {m n i : ℕ}, (m...=n).toList[i]! = if i < n + 1 - m then m + i else 0
-- Mathlib.CategoryTheory.WithTerminal.Cone
_private.Mathlib.CategoryTheory.WithTerminal.Cone.0.CategoryTheory.WithTerminal.coneLift.match_1.eq_2 : ∀ {J : Type u_1} (motive : CategoryTheory.WithTerminal J → Sort u_2)
  (h_1 : (a : J) → motive (CategoryTheory.WithTerminal.of a)) (h_2 : Unit → motive CategoryTheory.WithTerminal.star),
  (match CategoryTheory.WithTerminal.star with
    | CategoryTheory.WithTerminal.of a => h_1 a
    | CategoryTheory.WithTerminal.star => h_2 ()) =
    h_2 ()
-- Mathlib.Analysis.BoxIntegral.Box.Basic
/-- Each lower coordinate is less than its upper coordinate: i.e., the box is non-empty  -/
BoxIntegral.Box.lower_lt_upper : ∀ {ι : Type u_2} (self : BoxIntegral.Box ι) (i : ι), self.lower i < self.upper i
-- Mathlib.Algebra.Group.Submonoid.Basic
/-- An induction principle for closure membership for predicates with two arguments.  -/
Submonoid.closure_induction₂ : ∀ {M : Type u_1} [inst : MulOneClass M] {s : Set M}
  {motive : (x y : M) → x ∈ Submonoid.closure s → y ∈ Submonoid.closure s → Prop},
  (∀ (x y : M) (hx : x ∈ s) (hy : y ∈ s), motive x y ⋯ ⋯) →
    (∀ (x : M) (hx : x ∈ Submonoid.closure s), motive 1 x ⋯ hx) →
      (∀ (x : M) (hx : x ∈ Submonoid.closure s), motive x 1 hx ⋯) →
        (∀ (x y z : M) (hx : x ∈ Submonoid.closure s) (hy : y ∈ Submonoid.closure s) (hz : z ∈ Submonoid.closure s),
            motive x z hx hz → motive y z hy hz → motive (x * y) z ⋯ hz) →
          (∀ (x y z : M) (hx : x ∈ Submonoid.closure s) (hy : y ∈ Submonoid.closure s) (hz : z ∈ Submonoid.closure s),
              motive z x hz hx → motive z y hz hy → motive z (x * y) hz ⋯) →
            ∀ {x y : M} (hx : x ∈ Submonoid.closure s) (hy : y ∈ Submonoid.closure s), motive x y hx hy
-- Batteries.Logic
funext₃ : ∀ {α : Sort u_1} {β : α → Sort u_2} {γ : (a : α) → β a → Sort u_3} {δ : (a : α) → (b : β a) → γ a b → Sort u_4}
  {f g : (a : α) → (b : β a) → (c : γ a b) → δ a b c}, (∀ (a : α) (b : β a) (c : γ a b), f a b c = g a b c) → f = g
-- Lean.Data.Lsp.LanguageFeatures
Lean.Lsp.Color.green : Lean.Lsp.Color → Float
-- Mathlib.Data.Fin.Tuple.Basic
Fin.snoc.eq_1 : ∀ {n : ℕ} {α : Fin (n + 1) → Sort u_1} (p : (i : Fin n) → α i.castSucc) (x : α (Fin.last n)) (i : Fin (n + 1)),
  Fin.snoc p x i = if h : ↑i < n then cast ⋯ (p (i.castLT h)) else cast ⋯ x
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.mem_of_get?_eq_some : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k k' : α},
  t.get? k = some k' → k' ∈ t
-- Mathlib.LinearAlgebra.Eigenspace.Basic
Module.End.hasUnifEigenvalue_iff_mem_spectrum : ∀ {K : Type v} {V : Type w} [inst : Field K] [inst_1 : AddCommGroup V] [inst_2 : Module K V] [FiniteDimensional K V]
  {f : Module.End K V} {μ : K}, f.HasUnifEigenvalue μ 1 ↔ μ ∈ spectrum K f
-- Mathlib.CategoryTheory.Limits.Shapes.Multiequalizer
/-- The canonical injection `multiequalizer I ⟶ ∏ᶜ I.left`.  -/
CategoryTheory.Limits.Multiequalizer.ιPi : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {J : CategoryTheory.Limits.MulticospanShape} →
      (I : CategoryTheory.Limits.MulticospanIndex J C) →
        [inst_1 : CategoryTheory.Limits.HasMultiequalizer I] →
          [inst_2 : CategoryTheory.Limits.HasProduct I.left] →
            [CategoryTheory.Limits.HasProduct I.right] → CategoryTheory.Limits.multiequalizer I ⟶ ∏ᶜ I.left
-- Mathlib.Algebra.Polynomial.Taylor
Polynomial.eq_zero_of_hasseDeriv_eq_zero : ∀ {R : Type u_1} [inst : Semiring R] (f : Polynomial R) (r : R),
  (∀ (k : ℕ), Polynomial.eval r ((Polynomial.hasseDeriv k) f) = 0) → f = 0
-- Mathlib.MeasureTheory.Measure.Lebesgue.EqHaar
/-- The set `[0,1]^ι` as a compact set with non-empty interior.  -/
TopologicalSpace.PositiveCompacts.piIcc01 : (ι : Type u_1) → [Finite ι] → TopologicalSpace.PositiveCompacts (ι → ℝ)
-- Mathlib.Lean.Expr.Basic
/-- Construct the term of type `α` for a given integer
(doing typeclass search for the `OfNat` and `Neg` instances required).  -/
Lean.Expr.ofInt : Lean.Expr → ℤ → Lean.MetaM Lean.Expr
-- Init.Data.Int.Order
Int.lt_add_of_neg_add_lt : ∀ {a b c : ℤ}, -b + a < c → a < b + c
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.isOpen_upperHalfPlaneSet : IsOpen UpperHalfPlane.upperHalfPlaneSet
-- Mathlib.MeasureTheory.Integral.Bochner.Basic
MeasureTheory.exists_ne_zero_of_integral_ne_zero : ∀ {α : Type u_1} {G : Type u_5} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {f : α → G}, ∫ (a : α), f a ∂μ ≠ 0 → ∃ a, f a ≠ 0
-- Mathlib.NumberTheory.ModularForms.Basic
/-- Cast for cusp forms, which is useful for avoiding `Heq`s. Optionally transports along
an equality of subgroups.  -/
CuspForm.mcast : {a b : ℤ} →
  {Γ Γ' : Subgroup (GL (Fin 2) ℝ)} → a = b → CuspForm Γ a → autoParam (Γ' = Γ) CuspForm.mcast._auto_1 → CuspForm Γ' b
-- Mathlib.Algebra.Order.Group.OrderIso
OrderIso.mulRight_apply : ∀ {α : Type u} [inst : Group α] [inst_1 : LE α] [inst_2 : MulRightMono α] (a x : α), (OrderIso.mulRight a) x = x * a
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.getKey!_inter_of_not_mem_right : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] {m₁ m₂ : Std.DHashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α] [inst_4 : Inhabited α], m₁.WF → m₂.WF → ∀ {k : α}, k ∉ m₂ → (m₁ ∩ m₂).getKey! k = default
-- Mathlib.CategoryTheory.GuitartExact.Basic
/-- Given `w : TwoSquare T L R B` and a morphism `g : R.obj X₂ ⟶ B.obj X₃`, this is the
category `StructuredArrow (CostructuredArrow.mk g) (w.costructuredArrowRightwards X₃)`,
see the constructor `StructuredArrowRightwards.mk` for the data that is involved.  -/
CategoryTheory.TwoSquare.StructuredArrowRightwards : {C₁ : Type u₁} →
  {C₂ : Type u₂} →
    {C₃ : Type u₃} →
      {C₄ : Type u₄} →
        [inst : CategoryTheory.Category.{v₁, u₁} C₁] →
          [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] →
            [inst_2 : CategoryTheory.Category.{v₃, u₃} C₃] →
              [inst_3 : CategoryTheory.Category.{v₄, u₄} C₄] →
                {T : CategoryTheory.Functor C₁ C₂} →
                  {L : CategoryTheory.Functor C₁ C₃} →
                    {R : CategoryTheory.Functor C₂ C₄} →
                      {B : CategoryTheory.Functor C₃ C₄} →
                        CategoryTheory.TwoSquare T L R B →
                          {X₂ : C₂} → {X₃ : C₃} → (R.obj X₂ ⟶ B.obj X₃) → Type (max (max u₁ v₃) v₂)
-- Mathlib.RingTheory.PolynomialLaw.Basic
/-- The map `M → N` associated with a `f : M →ₚₗ[R] N` (essentially, `f.toFun' R`)  -/
PolynomialLaw.ground : {R : Type u} →
  [inst : CommSemiring R] →
    {M : Type u_1} →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {N : Type u_2} → [inst_3 : AddCommMonoid N] → [inst_4 : Module R N] → (M →ₚₗ[R] N) → M → N
-- Std.Data.ExtHashSet.Lemmas
Std.ExtHashSet.mem_insertMany_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashSet α} {ρ : Type v} [inst : ForIn Id ρ α]
  [inst_1 : EquivBEq α] [inst_2 : LawfulHashable α] {l : ρ} {k : α}, k ∈ m → k ∈ m.insertMany l
-- Mathlib.RingTheory.Localization.Integer
/-- **Alias** of `IsLocalization.integerMultiple_injective`. -/
IsLocalization.integerMultipleMultiple_injective : ∀ {R : Type u_1} [inst : CommSemiring R] (M : Submonoid R) {S : Type u_2} [inst_1 : CommSemiring S]
  [inst_2 : Algebra R S] [inst_3 : IsLocalization M S] {ι : Type u_4} (s : Finset ι) (f : ι → S),
  Function.Injective f → Function.Injective (IsLocalization.integerMultiple M s f)
-- Mathlib.Order.TypeTags
_private.Mathlib.Order.TypeTags.0.WithTop.instRepr.match_1.eq_1 : ∀ {α : Type u_1} (motive : WithTop α → Sort u_2) (h_1 : Unit → motive none) (h_2 : (a : α) → motive (some a)),
  (match none with
    | none => h_1 ()
    | some a => h_2 a) =
    h_1 ()
-- Mathlib.GroupTheory.Coprod.Basic
Monoid.Coprod.lift.eq_1 : ∀ {M : Type u_1} {N : Type u_2} {P : Type u_3} [inst : MulOneClass M] [inst_1 : MulOneClass N] [inst_2 : Monoid P]
  (f : M →* P) (g : N →* P), Monoid.Coprod.lift f g = Monoid.Coprod.clift (FreeMonoid.lift (Sum.elim ⇑f ⇑g)) ⋯ ⋯ ⋯ ⋯
-- Mathlib.Algebra.Group.ModEq
AddCommGroup.modEq_sub_iff_add_modEq : ∀ {G : Type u_1} [inst : AddCommGroup G] {p a b c : G}, a ≡ b - c [PMOD p] ↔ a + c ≡ b [PMOD p]
-- Mathlib.Algebra.Category.CommBialgCat
CommBialgCat.forget₂_commAlgCat_obj : ∀ {R : Type u} [inst : CommRing R] (A : CommBialgCat R),
  (CategoryTheory.forget₂ (CommBialgCat R) (CommAlgCat R)).obj A = CommAlgCat.of R ↑A
-- Lean.Meta.CoeAttr
/-- The environment extension for tracking coercion functions for delaboration  -/
Lean.Meta.coeExt : Lean.SimpleScopedEnvExtension (Lean.Name × Lean.Meta.CoeFnInfo) (Lean.NameMap Lean.Meta.CoeFnInfo)
-- Mathlib.CategoryTheory.Limits.FormalCoproducts.Basic
CategoryTheory.Limits.FormalCoproduct.Hom.mk.inj : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {X Y : CategoryTheory.Limits.FormalCoproduct C} {f : X.I → Y.I}
  {φ : (i : X.I) → X.obj i ⟶ Y.obj (f i)} {f_1 : X.I → Y.I} {φ_1 : (i : X.I) → X.obj i ⟶ Y.obj (f_1 i)},
  { f := f, φ := φ } = { f := f_1, φ := φ_1 } → f = f_1 ∧ φ ≍ φ_1
-- Mathlib.Order.Filter.Defs
/-- If `F` is a filter on `α`, and `U` a subset of `α` then we can write `U ∈ F` as on paper.  -/
Filter.instMembership : {α : Type u_1} → Membership (Set α) (Filter α)
-- Mathlib.Algebra.Polynomial.Derivative
Polynomial.iterate_derivative_intCast_mul : ∀ {R : Type u} [inst : Ring R] {n : ℤ} {k : ℕ} {f : Polynomial R},
  (⇑Polynomial.derivative)^[k] (↑n * f) = ↑n * (⇑Polynomial.derivative)^[k] f
-- Mathlib.Analysis.RCLike.ContinuousMap
ContinuousMap.realToRCLike_monotone : ∀ (X : Type u_1) (𝕜 : Type u_2) [inst : TopologicalSpace X] [inst_1 : RCLike 𝕜], Monotone (ContinuousMap.realToRCLike 𝕜)
-- Mathlib.Analysis.Convex.Segment
left_mem_openSegment_iff : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Ring 𝕜] [inst_1 : LinearOrder 𝕜] [IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup E] [inst_4 : Module 𝕜 E] {x y : E} [DenselyOrdered 𝕜] [Module.IsTorsionFree 𝕜 E],
  x ∈ openSegment 𝕜 x y ↔ x = y
-- Mathlib.Topology.Category.Profinite.Nobeling.Span
Profinite.NobelingProof.factors_prod_eq_basis_of_eq : ∀ {I : Type u} (C : Set (I → Bool)) [inst : LinearOrder I] (s : Finset I)
  {x y : ↑(Profinite.NobelingProof.π C fun x => x ∈ s)}, y = x → (Profinite.NobelingProof.factors C s x).prod y = 1
-- Mathlib.AlgebraicTopology.SimplexCategory.DeltaZeroIter
/-- If `n + i = m`, this is the morphism `⦋m⦌ ⟶ ⦋n⦌` in the simplex category
which is obtained as the `i`th iteration of `σ 0`.  -/
SimplexCategory.σ₀Iter : (i : ℕ) → {n m : ℕ} → autoParam (n + i = m) SimplexCategory.σ₀Iter._auto_1 → ({ len := m } ⟶ { len := n })
-- Mathlib.Topology.UniformSpace.Cauchy
/-- A complete space is defined here using uniformities. A uniform space
is complete if every Cauchy filter converges.  -/
CompleteSpace : (α : Type u) → [UniformSpace α] → Prop
-- Mathlib.MeasureTheory.Constructions.Cylinders
MeasureTheory.eq_of_cylinder_eq_of_subset : ∀ {ι : Type u_1} {α : ι → Type u_2} [h_nonempty : Nonempty ((i : ι) → α i)] {I J : Finset ι} {S : Set ((i : ↥I) → α ↑i)}
  {T : Set ((i : ↥J) → α ↑i)},
  MeasureTheory.cylinder I S = MeasureTheory.cylinder J T → ∀ (hJI : J ⊆ I), S = Finset.restrict₂ hJI ⁻¹' T
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.toListModel_interSmallerₘ : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [EquivBEq α] [inst_2 : Hashable α] [LawfulHashable α]
  (m₁ : Std.DHashMap.Internal.Raw₀ α β) (m₂ : Std.DHashMap.Raw α β),
  Std.DHashMap.Internal.Raw.WFImp ↑m₁ →
    (Std.DHashMap.Internal.toListModel (↑(m₁.interSmallerₘ m₂)).buckets).Perm
      (Std.Internal.List.interSmaller (Std.DHashMap.Internal.toListModel (↑m₁).buckets)
        (Std.DHashMap.Internal.toListModel m₂.buckets))
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.ImageMap.ext_iff : ∀ {C : Type u} {inst : CategoryTheory.Category.{v, u} C} {f g : CategoryTheory.Arrow C}
  {inst_1 : CategoryTheory.Limits.HasImage f.hom} {inst_2 : CategoryTheory.Limits.HasImage g.hom} {sq : f ⟶ g}
  {x y : CategoryTheory.Limits.ImageMap sq}, x = y ↔ x.map = y.map
-- Lean.Meta.Tactic.Simp.SimpTheorems
/-- An `Origin` is an identifier for simp theorems which indicates roughly
what action the user took which lead to this theorem existing in the simp set.
 -/
Lean.Meta.Origin : Type
-- Mathlib.Data.ENat.Basic
ENat.map_eq_top_iff : ∀ {n : ℕ∞} {α : Type u_1} {f : ℕ → α}, ENat.map f n = ⊤ ↔ n = ⊤
-- Init.Grind.Ordered.Linarith
Lean.Grind.Linarith.lt_lt_combine_cert : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Bool
-- Lean.Data.Lsp.Extra
Lean.Lsp.LeanImportMetaKind.meta.sizeOf_spec : sizeOf Lean.Lsp.LeanImportMetaKind.meta = 1
-- Mathlib.Algebra.Lie.Engel
/-- Engel's theorem.  -/
LieModule.isNilpotent_iff_forall' : ∀ {R : Type u₁} {L : Type u₂} {M : Type u₄} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L]
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [IsNoetherian R M], LieModule.IsNilpotent L M ↔ ∀ (x : L), IsNilpotent ((LieModule.toEnd R L M) x)
-- Std.Data.TreeSet.Lemmas
Std.TreeSet.Equiv.beq_congr : ∀ {α : Type u} {cmp : α → α → Ordering} {m₁ m₂ : Std.TreeSet α cmp} [Std.TransCmp cmp] {m₃ m₄ : Std.TreeSet α cmp},
  m₁.Equiv m₃ → m₂.Equiv m₄ → (m₁ == m₂) = (m₃ == m₄)
-- Lean.Meta.Sym.Arith.Types
Lean.Meta.Sym.Arith.Semiring.mk.inj : ∀ {id : ℕ} {type : Lean.Expr} {u : Lean.Level} {semiringInst : Lean.Expr}
  {addFn? mulFn? powFn? natCastFn? : Option Lean.Expr} {id_1 : ℕ} {type_1 : Lean.Expr} {u_1 : Lean.Level}
  {semiringInst_1 : Lean.Expr} {addFn?_1 mulFn?_1 powFn?_1 natCastFn?_1 : Option Lean.Expr},
  { id := id, type := type, u := u, semiringInst := semiringInst, addFn? := addFn?, mulFn? := mulFn?, powFn? := powFn?,
        natCastFn? := natCastFn? } =
      { id := id_1, type := type_1, u := u_1, semiringInst := semiringInst_1, addFn? := addFn?_1, mulFn? := mulFn?_1,
        powFn? := powFn?_1, natCastFn? := natCastFn?_1 } →
    id = id_1 ∧
      type = type_1 ∧
        u = u_1 ∧
          semiringInst = semiringInst_1 ∧
            addFn? = addFn?_1 ∧ mulFn? = mulFn?_1 ∧ powFn? = powFn?_1 ∧ natCastFn? = natCastFn?_1
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
hasMFDerivAt_inl : ∀ {𝕜 : 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] {M' : Type u_21} [inst_6 : TopologicalSpace M']
  [inst_7 : ChartedSpace H M'] {p : M ⊕ M'} {q : M},
  HasMFDerivAt% Sum.inl q (ContinuousLinearMap.id 𝕜 (TangentSpace I p))
-- Mathlib.Combinatorics.Matroid.Closure
Matroid.freeOn_closure_eq : ∀ {α : Type u_2} (E X : Set α), (Matroid.freeOn E).closure X = X ∩ E
-- Lean.DocString.Markdown
/-- Renders a custom inline element to Markdown. It receives a renderer for inline content, the saved
`Dynamic` description of the custom element, and the element's fallback content.
 -/
Lean.Doc.InlineMdRenderer : Type
-- Mathlib.CategoryTheory.Bicategory.Functor.StrictPseudofunctor
CategoryTheory.StrictPseudofunctorCore.map₂_left_unitor : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  (self : CategoryTheory.StrictPseudofunctorCore B C) {a b : B} (f : a ⟶ b),
  self.map₂ (CategoryTheory.Bicategory.leftUnitor f).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.eqToHom ⋯)
      (CategoryTheory.Bicategory.leftUnitor (self.map f)).hom
-- Mathlib.CategoryTheory.Bicategory.Functor.Lax
CategoryTheory.LaxFunctor.PseudoCore.mk.inj : ∀ {B : Type u₁} {inst : CategoryTheory.Bicategory B} {C : Type u₂} {inst_1 : CategoryTheory.Bicategory C}
  {F : CategoryTheory.LaxFunctor B C}
  {mapIdIso : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a)}
  {mapCompIso :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          F.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)}
  {mapIdIso_inv :
    autoParam (∀ {a : B}, (mapIdIso a).inv = F.mapId a) CategoryTheory.LaxFunctor.PseudoCore.mapIdIso_inv._autoParam}
  {mapCompIso_inv :
    autoParam (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso f g).inv = F.mapComp f g)
      CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv._autoParam}
  {mapIdIso_1 : (a : B) → F.map (CategoryTheory.CategoryStruct.id a) ≅ CategoryTheory.CategoryStruct.id (F.obj a)}
  {mapCompIso_1 :
    {a b c : B} →
      (f : a ⟶ b) →
        (g : b ⟶ c) →
          F.map (CategoryTheory.CategoryStruct.comp f g) ≅ CategoryTheory.CategoryStruct.comp (F.map f) (F.map g)}
  {mapIdIso_inv_1 :
    autoParam (∀ {a : B}, (mapIdIso_1 a).inv = F.mapId a) CategoryTheory.LaxFunctor.PseudoCore.mapIdIso_inv._autoParam}
  {mapCompIso_inv_1 :
    autoParam (∀ {a b c : B} (f : a ⟶ b) (g : b ⟶ c), (mapCompIso_1 f g).inv = F.mapComp f g)
      CategoryTheory.LaxFunctor.PseudoCore.mapCompIso_inv._autoParam},
  { mapIdIso := mapIdIso, mapCompIso := mapCompIso, mapIdIso_inv := mapIdIso_inv, mapCompIso_inv := mapCompIso_inv } =
      { mapIdIso := mapIdIso_1, mapCompIso := mapCompIso_1, mapIdIso_inv := mapIdIso_inv_1,
        mapCompIso_inv := mapCompIso_inv_1 } →
    mapIdIso = mapIdIso_1 ∧ mapCompIso = mapCompIso_1
-- Mathlib.Algebra.Ring.Hom.Defs
NonUnitalRingHom.comp_apply : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : NonUnitalNonAssocSemiring α]
  [inst_1 : NonUnitalNonAssocSemiring β] [inst_2 : NonUnitalNonAssocSemiring γ] (g : β →ₙ+* γ) (f : α →ₙ+* β) (x : α),
  (g.comp f) x = g (f x)
-- Mathlib.Order.Hom.Basic
OrderEmbedding.monotone : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (f : α ↪o β), Monotone ⇑f
-- Init.Notation
/-- `a ≥ b` is an abbreviation for `b ≤ a`. 

Conventions for notations in identifiers:

 * The recommended spelling of `≥` in identifiers is `ge`. -/
«term_≥_» : Lean.TrailingParserDescr
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- Corollary of the Chinese remainder theorem: given elements `x i : R / P i ^ e i`,
we can choose a representative `y : R` such that `y ≡ x i (mod P i ^ e i)`.  -/
IsDedekindDomain.exists_representative_mod_finset : ∀ {R : Type u_1} [inst : CommRing R] [IsDedekindDomain R] {ι : Type u_4} {s : Finset ι} (P : ι → Ideal R) (e : ι → ℕ),
  (∀ i ∈ s, Prime (P i)) →
    (∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j) →
      ∀ (x : (i : ↥s) → R ⧸ P ↑i ^ e ↑i), ∃ y, ∀ (i : ι) (hi : i ∈ s), (Ideal.Quotient.mk (P i ^ e i)) y = x ⟨i, hi⟩
-- Lean.Elab.Do.Legacy
Lean.Elab.Term.Do.getLetIdVars : Lean.Syntax → Array Lean.Elab.Term.Do.Var
-- Mathlib.Algebra.Regular.Basic
/-- An element `a` is left-regular if and only if a positive power of `a` is left-regular.  -/
IsLeftRegular.pow_iff : ∀ {R : Type u_1} [inst : Monoid R] {a : R} {n : ℕ}, 0 < n → (IsLeftRegular (a ^ n) ↔ IsLeftRegular a)
-- Mathlib.Data.Finset.Prod
Finset.image_swap_product : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq (α × β)] (s : Finset α) (t : Finset β),
  Finset.image Prod.swap (t ×ˢ s) = s ×ˢ t