mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Monoidal.Conv
CategoryTheory.Conv.one_eq : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C] {M N : C}
  [inst_2 : CategoryTheory.ComonObj M] [inst_3 : CategoryTheory.MonObj N],
  1 = CategoryTheory.CategoryStruct.comp CategoryTheory.ComonObj.counit CategoryTheory.MonObj.one
-- Mathlib.Algebra.GroupWithZero.WithZero
WithZero.exp_eq_one : ∀ {M : Type u_4} [inst : AddMonoid M] {x : M}, WithZero.exp x = 1 ↔ x = 0
-- Mathlib.NumberTheory.NumberField.Cyclotomic.Galois
IsCyclotomicExtension.Rat.galEquivZMod.congr_simp : ∀ (n : ℕ) [inst : NeZero n] (K : Type u_1) [inst_1 : Field K] [inst_2 : NumberField K]
  [hK : IsCyclotomicExtension {n} ℚ K],
  IsCyclotomicExtension.Rat.galEquivZMod n K = IsCyclotomicExtension.Rat.galEquivZMod n K
-- Lean.Elab.Tactic.Simp
Lean.Elab.Tactic.Simp.DischargeWrapper.custom.sizeOf_spec : ∀ (ref : IO.Ref Lean.Elab.Term.State) (discharge : Lean.Meta.Simp.Discharge),
  sizeOf (Lean.Elab.Tactic.Simp.DischargeWrapper.custom ref discharge) = 1 + sizeOf ref
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryProducts
CategoryTheory.Limits.WalkingPair.equivBool_symm_apply_true : CategoryTheory.Limits.WalkingPair.equivBool.symm true = CategoryTheory.Limits.WalkingPair.left
-- Mathlib.CategoryTheory.Functor.ReflectsIso.Jointly
CategoryTheory.JointlyReflectMonomorphisms.mk : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_4, u_1} C] {I : Type u_2} {D : I → Type u_3}
  [inst_1 : (i : I) → CategoryTheory.Category.{u_5, u_3} (D i)] {F : (i : I) → CategoryTheory.Functor C (D i)},
  (∀ {X Y : C} (f : X ⟶ Y) [∀ (i : I), CategoryTheory.Mono ((F i).map f)], CategoryTheory.Mono f) →
    CategoryTheory.JointlyReflectMonomorphisms F
-- Init.Data.List.Sublist
List.Sublist.of_cons_cons : ∀ {α : Type u_1} {l₁ l₂ : List α} {a b : α}, (a :: l₁).Sublist (b :: l₂) → l₁.Sublist l₂
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.mk.injEq : ∀ {G : Type u_1} [inst : Group G] [inst_1 : TopologicalSpace G] (toSubgroup : Subgroup G)
  (isOpen' : IsOpen toSubgroup.carrier) (toSubgroup_1 : Subgroup G) (isOpen'_1 : IsOpen toSubgroup_1.carrier),
  ({ toSubgroup := toSubgroup, isOpen' := isOpen' } = { toSubgroup := toSubgroup_1, isOpen' := isOpen'_1 }) =
    (toSubgroup = toSubgroup_1)
-- Mathlib.RingTheory.Ideal.Quotient.Operations
Ideal.quotientMap_algebraMap : ∀ {R₁ : Type u_1} {A : Type u_3} [inst : CommSemiring R₁] [inst_1 : Ring A] [inst_2 : Algebra R₁ A] {S : Type v}
  [inst_3 : Ring S] {J : Ideal A} {I : Ideal S} [inst_4 : I.IsTwoSided] [inst_5 : J.IsTwoSided] {f : A →+* S}
  {H : J ≤ Ideal.comap f I} {x : R₁},
  (Ideal.quotientMap I f H) ((algebraMap R₁ (A ⧸ J)) x) = (Ideal.Quotient.mk I) (f ((algebraMap R₁ A) x))
-- Std.Data.Iterators.Lemmas.Producers.Range
Std.Roi.toList_iter : ∀ {α : Type u_1} [inst : Std.PRange.UpwardEnumerable α] [inst_1 : Std.Rxi.IsAlwaysFinite α]
  [inst_2 : Std.PRange.LawfulUpwardEnumerable α] {r : Std.Roi α}, r.iter.toList = r.toList
-- Mathlib.CategoryTheory.Abelian.GrothendieckCategory.EnoughInjectives
/-- Given an object `G : C`, this is the family of morphisms in `C`
given by the inclusions of all subobjects of `G`. If `G` is a separator,
and `C` is a Grothendieck abelian category, then any monomorphism in `C`
is a transfinite composition of pushouts of monomorphisms in this family
(see `generatingMonomorphisms.exists_transfiniteCompositionOfShape`).  -/
CategoryTheory.IsGrothendieckAbelian.generatingMonomorphisms : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → C → CategoryTheory.MorphismProperty C
-- Mathlib.Algebra.Group.Pointwise.Set.Lattice
Set.iInter_vsub_subset : ∀ {α : Type u_2} {β : Type u_3} {ι : Sort u_5} [inst : VSub α β] (s : ι → Set β) (t : Set β),
  (⋂ i, s i) -ᵥ t ⊆ ⋂ i, s i -ᵥ t
-- Init.Data.Vector.Zip
Vector.unzip_zip_left : ∀ {α : Type u_1} {n : ℕ} {β : Type u_2} {as : Vector α n} {bs : Vector β n}, (as.zip bs).unzip.1 = as
-- Init.Data.SInt.Lemmas
Int16.add_mul : ∀ {a b c : Int16}, (a + b) * c = a * c + b * c
-- Mathlib.Algebra.Order.GroupWithZero.Canonical
/-- The exponential map as an order isomorphism between `G` and `Gᵐ⁰ˣ`.  -/
WithZero.expOrderIso : {G : Type u_3} → [inst : Preorder G] → [inst_1 : AddGroup G] → G ≃o (WithZero (Multiplicative G))ˣ
-- Mathlib.CategoryTheory.Limits.Fubini
/-- Given a functor `G : J × K ⥤ C` such that `(curry.obj G ⋙ lim)` makes sense and has a limit,
we can construct a cone over `G` with `limit (curry.obj G ⋙ lim)` as a cone point  -/
CategoryTheory.Limits.coneOfHasLimitCurryCompLim : {J : Type u_1} →
  {K : Type u_2} →
    [inst : CategoryTheory.Category.{v_1, u_1} J] →
      [inst_1 : CategoryTheory.Category.{v_2, u_2} K] →
        {C : Type u_3} →
          [inst_2 : CategoryTheory.Category.{v_3, u_3} C] →
            (G : CategoryTheory.Functor (J × K) C) →
              [inst_3 : CategoryTheory.Limits.HasLimitsOfShape K C] →
                [CategoryTheory.Limits.HasLimit ((CategoryTheory.Functor.curry.obj G).comp CategoryTheory.Limits.lim)] →
                  CategoryTheory.Limits.Cone G
-- Mathlib.Analysis.Convex.Extreme
IsExtreme.subset : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : SMul 𝕜 E] {A B : Set E}, IsExtreme 𝕜 A B → B ⊆ A
-- Mathlib.RingTheory.Ideal.Operations
/-- See also `isUnit_iff_eq_one`.  -/
Ideal.isUnit_iff : ∀ {R : Type u} [inst : CommSemiring R] {I : Ideal R}, IsUnit I ↔ I = ⊤
-- Mathlib.Topology.Instances.AddCircle.Defs
/-- If functions on AddCircle agree on the image of the interval `[a, a + p)` then they are equal  -/
AddCircle.Ico_ext : ∀ {𝕜 : Type u_1} [inst : AddCommGroup 𝕜] (p : 𝕜) [inst_1 : LinearOrder 𝕜] [IsOrderedAddMonoid 𝕜] [hp : Fact (0 < p)]
  [Archimedean 𝕜] {α : Type u_3} {f g : AddCircle p → α} (a : 𝕜), (∀ x ∈ Set.Ico a (a + p), f ↑x = g ↑x) → f = g
-- Mathlib.CategoryTheory.Shift.ShiftedHom
/-- The composition of `f : X ⟶ Y⟦a⟧` and `g : Y ⟶ Z⟦b⟧`, as a morphism `X ⟶ Z⟦c⟧`
when `b + a = c`.  -/
CategoryTheory.ShiftedHom.comp : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {M : Type u_4} →
      [inst_1 : AddMonoid M] →
        [inst_2 : CategoryTheory.HasShift C M] →
          {X Y Z : C} →
            {a b c : M} →
              CategoryTheory.ShiftedHom X Y a →
                CategoryTheory.ShiftedHom Y Z b → b + a = c → CategoryTheory.ShiftedHom X Z c
-- Mathlib.Analysis.Normed.Group.Basic
eq_of_norm_sub_le_zero : ∀ {E : Type u_5} [inst : NormedAddGroup E] {a b : E}, ‖a - b‖ ≤ 0 → a = b
-- Mathlib.Algebra.Category.Semigrp.Basic
/-- **Alias** of `CategoryTheory.ConcreteCategory.forget_map_eq_ofHom`. -/
Semigrp.forget_map : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {FC : outParam (C → C → Type u_2)}
  {CC : outParam (C → Type w)} [inst_1 : outParam ((X Y : C) → FunLike (FC X Y) (CC X) (CC Y))]
  [inst_2 : CategoryTheory.ConcreteCategory C FC] {X Y : C} (f : X ⟶ Y),
  (CategoryTheory.forget C).map f = TypeCat.ofHom ⇑(CategoryTheory.ConcreteCategory.hom f)
-- Mathlib.Data.Set.Basic
/-- `Set α` almost never has decidable equality.
In fact, for an inhabited type `α`, `Set α` has decidable equality iff
all propositions are decidable. We add a global instance that `Set α` has decidable equality,
coming from the choice axiom, so that we don't have to provide `[DecidableEq (Set α)]` arguments
in lemma statements.  -/
Set.decidableEq : {α : Type u} → DecidableEq (Set α)
-- Init.Data.SInt.Bitwise
Int8.toBitVec_abs : ∀ (a : Int8), a.abs.toBitVec = a.toBitVec.abs
-- Mathlib.RingTheory.MvPowerSeries.Inverse
MvPowerSeries.coeff_inv : ∀ {σ : Type u_1} {k : Type u_3} [inst : Field k] [inst_1 : DecidableEq σ] (n : σ →₀ ℕ) (φ : MvPowerSeries σ k),
  (MvPowerSeries.coeff n) φ⁻¹ =
    if n = 0 then (MvPowerSeries.constantCoeff φ)⁻¹
    else
      -(MvPowerSeries.constantCoeff φ)⁻¹ *
        ∑ x ∈ Finset.HasAntidiagonal.antidiagonal n,
          if x.2 < n then (MvPowerSeries.coeff x.1) φ * (MvPowerSeries.coeff x.2) φ⁻¹ else 0
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
/-- Projection to `AlternatingMap`s.  -/
ContinuousAlternatingMap.toAlternatingMap : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {ι : Type u_4} →
        [inst : Semiring R] →
          [inst_1 : AddCommMonoid M] →
            [inst_2 : Module R M] →
              [inst_3 : TopologicalSpace M] →
                [inst_4 : AddCommMonoid N] →
                  [inst_5 : Module R N] → [inst_6 : TopologicalSpace N] → M [⋀^ι]→L[R] N → M [⋀^ι]→ₗ[R] N
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
AbstractSimplicialComplex.ext_iff : ∀ {ι : Type u_1} {x y : AbstractSimplicialComplex ι}, x = y ↔ x.faces = y.faces
-- Mathlib.Order.Interval.Finset.Fin
Fin.map_succEmb_Icc : ∀ {n : ℕ} (i j : Fin n), Finset.map (Fin.succEmb n) (Finset.Icc i j) = Finset.Icc i.succ j.succ
-- Mathlib.CategoryTheory.SmallObject.Iteration.FunctorOfCocone
CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso_hom_naturality : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] {J : Type u} [inst_1 : LinearOrder J] {j : J}
  {F : CategoryTheory.Functor (↑(Set.Iio j)) C} (c : CategoryTheory.Limits.Cocone F) (i₁ i₂ : J) (hi : i₁ ≤ i₂)
  (hi₂ : i₂ < j),
  CategoryTheory.CategoryStruct.comp
      ((CategoryTheory.SmallObject.SuccStruct.ofCocone c).map (CategoryTheory.homOfLE hi))
      (CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso c i₂ hi₂).hom =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.SmallObject.SuccStruct.ofCoconeObjIso c i₁ ⋯).hom
      (F.map (CategoryTheory.homOfLE hi))
-- Mathlib.RingTheory.TensorProduct.Maps
Algebra.TensorProduct.tensorTensorTensorComm_toLinearEquiv : ∀ {R : Type uR} {R' : Type u_1} {S : Type uS} {T : Type u_2} {A : Type uA} {B : Type uB} {C : Type uC} {D : Type uD}
  [inst : CommSemiring R] [inst_1 : CommSemiring S] [inst_2 : Algebra R S] [inst_3 : Semiring A] [inst_4 : Algebra R A]
  [inst_5 : Algebra S A] [inst_6 : IsScalarTower R S A] [inst_7 : Semiring B] [inst_8 : Algebra R B]
  [inst_9 : Semiring C] [inst_10 : Algebra R C] [inst_11 : Algebra S C] [inst_12 : IsScalarTower R S C]
  [inst_13 : Semiring D] [inst_14 : Algebra R D] [inst_15 : CommSemiring T] [inst_16 : Algebra R T]
  [inst_17 : Algebra T A] [inst_18 : IsScalarTower R T A] [inst_19 : SMulCommClass S T A] [inst_20 : Algebra S T]
  [inst_21 : IsScalarTower S T A] [inst_22 : CommSemiring R'] [inst_23 : Algebra R R'] [inst_24 : Algebra R' T]
  [inst_25 : Algebra R' A] [inst_26 : Algebra R' B] [inst_27 : IsScalarTower R R' A] [inst_28 : SMulCommClass S R' A]
  [inst_29 : SMulCommClass R' S A] [inst_30 : IsScalarTower R' T A] [inst_31 : IsScalarTower R R' B],
  ↑(Algebra.TensorProduct.tensorTensorTensorComm R R' S T A B C D) =
    TensorProduct.AlgebraTensorModule.tensorTensorTensorComm R R' S T A B C D
-- Mathlib.Computability.TuringMachine.Config
Turing.ToPartrec.Code.id_eval : ∀ (v : List ℕ), Turing.ToPartrec.Code.id.eval v = pure v
-- Mathlib.Algebra.AddConstMap.Equiv
AddConstEquiv.refl_apply : ∀ {G : Type u_1} [inst : Add G] (a a_1 : G), (AddConstEquiv.refl a) a_1 = a_1
-- Std.Data.HashSet.Lemmas
Std.HashSet.get?_ofList_of_mem : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} [EquivBEq α] [LawfulHashable α] {l : List α} {k k' : α},
  (k == k') = true → List.Pairwise (fun a b => (a == b) = false) l → k ∈ l → (Std.HashSet.ofList l).get? k' = some k
-- Std.Time.Format.DateFormat
/-- Short day-period strings for the `b` pattern (AM, PM, noon, midnight).
Used by `b`/`bb`/`bbb`.
 -/
Std.Time.DateFormatSymbols.dayPeriodShort : Std.Time.DateFormatSymbols → Std.Time.DayPeriodSymbols
-- Init.Data.List.Basic
List.filter.eq_def : ∀ {α : Type u} (p : α → Bool) (x : List α),
  List.filter p x =
    match x with
    | [] => []
    | a :: as =>
      match p a with
      | true => a :: List.filter p as
      | false => List.filter p as
-- Mathlib.Geometry.Manifold.IsManifold.Basic
ModelWithCorners.uniqueDiffWithinAt_image : ∀ {𝕜 : 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) {x : H},
  UniqueDiffWithinAt 𝕜 (Set.range ↑I) (↑I x)
-- Init.Data.String.Decode
ByteArray.utf8DecodeChar?.assemble₂Unchecked.eq_1 : ∀ (w x : UInt8), ByteArray.utf8DecodeChar?.assemble₂Unchecked w x = (w &&& 31).toUInt32 <<< 6 ||| (x &&& 63).toUInt32
-- Init.MetaTypes
/-- Transparency mode for reduction. Default: `all`.  -/
Lean.Meta.Command.ReduceConfig.transparency : Lean.Meta.Command.ReduceConfig → Lean.Meta.TransparencyMode
-- Std.Time.Date.PlainDate
/-- Creates a `PlainDate` from the number of days since January 1st, 1970.
 -/
Std.Time.PlainDate.ofEpochDay : Std.Time.Day.Offset → Std.Time.PlainDate
-- Mathlib.RingTheory.NonUnitalSubsemiring.Basic
/-- The image under a ring homomorphism of the subsemiring generated by a set equals
the subsemiring generated by the image of the set.  -/
NonUnitalRingHom.map_sclosure : ∀ {R : Type u} {S : Type v} [inst : NonUnitalNonAssocSemiring R] {F : Type u_1} [inst_1 : FunLike F R S]
  [inst_2 : NonUnitalNonAssocSemiring S] [inst_3 : NonUnitalRingHomClass F R S] (f : F) (s : Set R),
  NonUnitalSubsemiring.map f (NonUnitalSubsemiring.closure s) = NonUnitalSubsemiring.closure (⇑f '' s)
-- Mathlib.Probability.Distributions.Gaussian.Real
/-- All the moments of a real Gaussian distribution are finite. That is, the identity is in Lp for
all finite `p`.  -/
ProbabilityTheory.memLp_id_gaussianReal : ∀ {μ : ℝ} {v : NNReal} (p : NNReal), MeasureTheory.MemLp id (↑p) (ProbabilityTheory.gaussianReal μ v)
-- Mathlib.Data.Nat.Choose.Sum
Finset.sum_choose_succ_nsmul : ∀ {M : Type u_2} [inst : AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ),
  ∑ i ∈ Finset.range (n + 2), (n + 1).choose i • f i (n + 1 - i) =
    ∑ i ∈ Finset.range (n + 1), n.choose i • f i (n + 1 - i) +
      ∑ i ∈ Finset.range (n + 1), n.choose i • f (i + 1) (n - i)
-- Mathlib.AlgebraicGeometry.Morphisms.FlatDescent
/-- fpqc descent implies fppf descent  -/
AlgebraicGeometry.instDescendsAlongSchemeMinMorphismPropertySurjectiveFlatLocallyOfFinitePresentationOfQuasiCompactOfIsZariskiLocalAtTarget : ∀ (P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme)
  [P.DescendsAlong (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.QuasiCompact)]
  [AlgebraicGeometry.IsZariskiLocalAtTarget P],
  P.DescendsAlong
    (@AlgebraicGeometry.Surjective ⊓ @AlgebraicGeometry.Flat ⊓ @AlgebraicGeometry.LocallyOfFinitePresentation)
-- Mathlib.CategoryTheory.Localization.SmallShiftedHom
CategoryTheory.LocalizerMorphism.smallShiftedHomMap_mk : ∀ {C₁ : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C₁] {C₂ : Type u₂}
  [inst_1 : CategoryTheory.Category.{v₂, u₂} C₂] {W₁ : CategoryTheory.MorphismProperty C₁}
  {W₂ : CategoryTheory.MorphismProperty C₂} (Φ : CategoryTheory.LocalizerMorphism W₁ W₂) {M : Type w'}
  [inst_2 : AddMonoid M] [inst_3 : CategoryTheory.HasShift C₁ M] [inst_4 : CategoryTheory.HasShift C₂ M]
  [inst_5 : Φ.functor.CommShift M] {X₁ Y₁ : C₁} {X₂ Y₂ : C₂}
  [inst_6 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₁ M X₁ Y₁]
  [inst_7 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ X₂]
  [inst_8 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M X₂ Y₂]
  [inst_9 : CategoryTheory.Localization.HasSmallLocalizedShiftedHom W₂ M Y₂ Y₂] (eX : Φ.functor.obj X₁ ≅ X₂)
  (eY : Φ.functor.obj Y₁ ≅ Y₂) [W₁.IsCompatibleWithShift M] [W₂.IsCompatibleWithShift M] {m : M}
  (f : CategoryTheory.ShiftedHom X₁ Y₁ m),
  Φ.smallShiftedHomMap eX eY (CategoryTheory.Localization.SmallShiftedHom.mk W₁ f) =
    CategoryTheory.Localization.SmallShiftedHom.mk W₂
      ((CategoryTheory.ShiftedHom.mk₀ 0 ⋯ eX.inv).comp
        ((f.map Φ.functor).comp (CategoryTheory.ShiftedHom.mk₀ 0 ⋯ eY.hom) ⋯) ⋯)
-- Mathlib.GroupTheory.Perm.Subgroup
Equiv.Perm.sumCongrHom.card_range : ∀ {α : Type u_1} {β : Type u_2} [inst : Fintype ↥(Equiv.Perm.sumCongrHom α β).range]
  [inst_1 : Fintype (Equiv.Perm α × Equiv.Perm β)],
  Fintype.card ↥(Equiv.Perm.sumCongrHom α β).range = Fintype.card (Equiv.Perm α × Equiv.Perm β)
-- Mathlib.GroupTheory.Commutator.Basic
Subgroup.commutator_characteristic : ∀ {G : Type u_1} [inst : Group G] (H₁ H₂ : Subgroup G) [h₁ : H₁.Characteristic] [h₂ : H₂.Characteristic],
  ⁅H₁, H₂⁆.Characteristic
-- Init.Data.SInt.Bitwise
ISize.toUSize_xor : ∀ (a b : ISize), (a ^^^ b).toUSize = a.toUSize ^^^ b.toUSize
-- Mathlib.Data.Num.Lemmas
PosNum.size.eq_def : ∀ (x : PosNum),
  x.size =
    match x with
    | PosNum.one => 1
    | n.bit0 => n.size.succ
    | n.bit1 => n.size.succ
-- Mathlib.Order.Hom.BoundedLattice
InfTopHom.instOrderTop.eq_1 : ∀ {α : Type u_2} {β : Type u_3} [inst : Min α] [inst_1 : Top α] [inst_2 : SemilatticeInf β] [inst_3 : OrderTop β],
  InfTopHom.instOrderTop = { top := { toInfHom := ⊤, map_top' := ⋯ }, le_top := ⋯ }
-- Std.Http.Data.Headers.Basic
/-- The `Host` header.

Represents the authority component of a URI:
host [ ":" port ]

Reference: https://www.rfc-editor.org/rfc/rfc9110.html#name-host-and-authority
 -/
Std.Http.Header.Host : Type
-- Init.Grind.Config
Lean.Grind.instBEqConfig.beq : Lean.Grind.Config → Lean.Grind.Config → Bool
-- Mathlib.Data.ZMod.Basic
ZMod.unitOfCoprime.congr_simp : ∀ {n : ℕ} (x x_1 : ℕ) (e_x : x = x_1) (h : x.Coprime n), ZMod.unitOfCoprime x h = ZMod.unitOfCoprime x_1 ⋯
-- Mathlib.CategoryTheory.Comma.Over.Basic
CategoryTheory.Over.inv_left_hom_left : ∀ {T : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} T] {X : T} {f g : CategoryTheory.Over X} (e : f ≅ g),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Over.Hom.left e.inv) (CategoryTheory.Over.Hom.left e.hom) =
    CategoryTheory.CategoryStruct.id g.left
-- Mathlib.Algebra.Free
FreeSemigroup.pure_bind : ∀ {α β : Type u} (f : α → FreeSemigroup β) (x : α), pure x >>= f = f x
-- Lean.Server.CodeActions.Attr
Lean.CodeAction.CommandCodeActionEntry.mk.injEq : ∀ (declName : Lean.Name) (cmdKinds : Array Lean.Name) (declName_1 : Lean.Name) (cmdKinds_1 : Array Lean.Name),
  ({ declName := declName, cmdKinds := cmdKinds } = { declName := declName_1, cmdKinds := cmdKinds_1 }) =
    (declName = declName_1 ∧ cmdKinds = cmdKinds_1)
-- Mathlib.Geometry.Manifold.Sheaf.Smooth
smoothSheafCommRing.forgetStalk_inv_comp_eval_apply : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {EM : Type u_2} [inst_1 : NormedAddCommGroup EM]
  [inst_2 : NormedSpace 𝕜 EM] {HM : Type u_3} [inst_3 : TopologicalSpace HM] (IM : ModelWithCorners 𝕜 EM HM)
  {E : Type u_4} [inst_4 : NormedAddCommGroup E] [inst_5 : NormedSpace 𝕜 E] {H : Type u_5} [inst_6 : TopologicalSpace H]
  (I : ModelWithCorners 𝕜 E H) (M : Type u) [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace HM M] (R : Type u)
  [inst_9 : TopologicalSpace R] [inst_10 : ChartedSpace H R] [inst_11 : CommRing R] [inst_12 : ContMDiffRing I (↑⊤) R]
  (x : ↑(TopCat.of M)) (x_1 : (smoothSheaf IM I M R).presheaf.stalk x),
  (CommRingCat.Hom.hom (smoothSheafCommRing.evalHom IM I M R x))
      ((CategoryTheory.ConcreteCategory.hom (smoothSheafCommRing.forgetStalk IM I M R x).inv) x_1) =
    (CategoryTheory.ConcreteCategory.hom (smoothSheaf.evalHom IM I R x)) x_1
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.monadMap_StateT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {σ : Type u} [Monad m] [inst : Std.Do.WP m ps]
  (f : {β : Type u} → m β → m β) {α : Type u} (x : StateT σ m α) (Q : Std.Do.PostCond α (Std.Do.PostShape.arg σ ps)),
  ⦃fun s =>
    (Std.Do.wp (f (x.run s))).apply
      (fun x =>
        match x with
        | (a, s) => Q.1 a s,
        Q.2)⦄
    MonadFunctor.monadMap (fun {β} => f) x ⦃Q⦄
-- Mathlib.Topology.MetricSpace.GromovHausdorffRealized
_private.Mathlib.Topology.MetricSpace.GromovHausdorffRealized.0.GromovHausdorff.HD_optimalGHDist_le : ∀ (X : Type u) (Y : Type v) [inst : MetricSpace X] [inst_1 : CompactSpace X] [inst_2 : Nonempty X]
  [inst_3 : MetricSpace Y] [inst_4 : CompactSpace Y] [inst_5 : Nonempty Y],
  ∀ g ∈ GromovHausdorff.candidatesB✝ X Y, GromovHausdorff.HD (GromovHausdorff.optimalGHDist✝ X Y) ≤ GromovHausdorff.HD g
-- Mathlib.RingTheory.Algebraic.Basic
isAlgebraic_one : ∀ {R : Type u} {A : Type v} [inst : CommRing R] [inst_1 : Ring A] [inst_2 : Algebra R A] [Nontrivial R], IsAlgebraic R 1
-- Mathlib.CategoryTheory.Galois.Prorepresentability
/-- An element of the fiber of `obj`.  -/
CategoryTheory.PreGaloisCategory.PointedGaloisObject.pt : {C : Type u₁} →
  [inst : CategoryTheory.Category.{u₂, u₁} C] →
    [inst_1 : CategoryTheory.GaloisCategory C] →
      {F : CategoryTheory.Functor C FintypeCat} →
        (self : CategoryTheory.PreGaloisCategory.PointedGaloisObject F) → (F.obj self.obj).obj
-- Mathlib.Order.Sublattice
Sublattice.map_inf_le : ∀ {α : Type u_2} {β : Type u_3} [inst : Lattice α] [inst_1 : Lattice β] (L M : Sublattice α) (f : LatticeHom α β),
  Sublattice.map f (L ⊓ M) ≤ Sublattice.map f L ⊓ Sublattice.map f M
-- Std.Data.Internal.List.Associative
Std.Internal.List.containsKey_insertEntry_of_beq : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [PartialEquivBEq α] {l : List ((a : α) × β a)} {k a : α} {v : β k},
  (k == a) = true → Std.Internal.List.containsKey a (Std.Internal.List.insertEntry k v l) = true
-- Mathlib.Data.NNReal.Defs
/-- If `a` is a nonnegative real number, then the closed interval `[0, a]` in `ℝ` is order
isomorphic to the interval `Set.Iic a`.  -/
NNReal.orderIsoIccZeroCoe : (a : NNReal) → ↑(Set.Icc 0 ↑a) ≃o ↑(Set.Iic a)
-- Mathlib.AlgebraicGeometry.Scheme
AlgebraicGeometry.Scheme.basicOpen_mul : ∀ (X : AlgebraicGeometry.Scheme) {U : X.Opens} (f g : ↑(X.presheaf.obj (Opposite.op U))),
  X.basicOpen (f * g) = X.basicOpen f ⊓ X.basicOpen g
-- Mathlib.Data.ENat.Basic
ENat.map_one : ∀ {α : Type u_1} (f : ℕ → α), ENat.map f 1 = ↑(f 1)
-- Lean.Data.JsonRpc
Lean.JsonRpc.Response.mk : {α : Type u} → Lean.JsonRpc.RequestID → α → Lean.JsonRpc.Response α
-- Mathlib.LinearAlgebra.AffineSpace.AffineSubspace.Defs
/-- The span of the empty set is `⊥`.  -/
AffineSubspace.span_empty : ∀ (k : Type u_1) (V : Type u_2) (P : Type u_3) [inst : Ring k] [inst_1 : AddCommGroup V] [inst_2 : Module k V]
  [S : AddTorsor V P], affineSpan k ∅ = ⊥
-- Mathlib.CategoryTheory.ConnectedComponents
/-- Every functor to a discrete category gives a function from connected components  -/
CategoryTheory.ConnectedComponents.liftFunctor : (J : Type u_2) →
  [inst : CategoryTheory.Category.{v_1, u_2} J] →
    {X : Type u_1} → CategoryTheory.Functor J (CategoryTheory.Discrete X) → CategoryTheory.ConnectedComponents J → X
-- Init.Data.Int.Order
Int.instIdempotentOpMin : Std.IdempotentOp min
-- Mathlib.Order.Filter.Defs
Filter.ext : ∀ {α : Type u_1} {f g : Filter α}, (∀ (s : Set α), s ∈ f ↔ s ∈ g) → f = g
-- Mathlib.CategoryTheory.Limits.FunctorCategory.Shapes.Products
CategoryTheory.Limits.ι_comp_sigmaObjIso_inv : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₁} [inst_1 : CategoryTheory.Category.{v₁, u₁} D]
  {α : Type w} [inst_2 : CategoryTheory.Limits.HasColimitsOfShape (CategoryTheory.Discrete α) C]
  (f : α → CategoryTheory.Functor D C) (d : D) (s : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Sigma.ι (fun s => (f s).obj d) s)
      (CategoryTheory.Limits.sigmaObjIso f d).inv =
    (CategoryTheory.Limits.Sigma.ι f s).app d
-- Mathlib.Tactic.ClickSuggestions.GRewrite
Mathlib.Tactic.ClickSuggestions.GrwInfo.mk.inj : ∀ {rootExpr subExpr : Lean.Expr} {rflTarget? : Option Lean.Expr} {gpos : Array Mathlib.Tactic.ClickSuggestions.GrwPos}
  {rwKind : Mathlib.Tactic.ClickSuggestions.RwKind} {rootExpr_1 subExpr_1 : Lean.Expr} {rflTarget?_1 : Option Lean.Expr}
  {gpos_1 : Array Mathlib.Tactic.ClickSuggestions.GrwPos} {rwKind_1 : Mathlib.Tactic.ClickSuggestions.RwKind},
  { rootExpr := rootExpr, subExpr := subExpr, rflTarget? := rflTarget?, gpos := gpos, rwKind := rwKind } =
      { rootExpr := rootExpr_1, subExpr := subExpr_1, rflTarget? := rflTarget?_1, gpos := gpos_1, rwKind := rwKind_1 } →
    rootExpr = rootExpr_1 ∧ subExpr = subExpr_1 ∧ rflTarget? = rflTarget?_1 ∧ gpos = gpos_1 ∧ rwKind = rwKind_1
-- Mathlib.Algebra.Homology.ShortComplex.RightHomology
/-- A left homology data for a short complex `S` induces a right homology data for `S.op`.  -/
CategoryTheory.ShortComplex.LeftHomologyData.op : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {S : CategoryTheory.ShortComplex C} → S.LeftHomologyData → S.op.RightHomologyData