mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.AlgebraicGeometry.EllipticCurve.Affine.Formula
WeierstrassCurve.Affine.equation_neg : ∀ {R : Type r} [inst : CommRing R] {W' : WeierstrassCurve.Affine R} (x y : R),
  W'.Equation x (W'.negY x y) ↔ W'.Equation x y
-- Mathlib.Analysis.Convex.Intrinsic
intrinsicFrontier_subset : ∀ {𝕜 : Type u_1} {V : Type u_2} {P : Type u_5} [inst : Ring 𝕜] [inst_1 : AddCommGroup V] [inst_2 : Module 𝕜 V]
  [inst_3 : TopologicalSpace P] [inst_4 : AddTorsor V P] {s : Set P}, IsClosed s → intrinsicFrontier 𝕜 s ⊆ s
-- Std.Data.Iterators.Combinators.Monadic.TakeWhile
_private.Std.Data.Iterators.Combinators.Monadic.TakeWhile.0.Std.Iterators.Types.TakeWhile.instProductivenessRelation : {α : Type w} →
  {m : Type w → Type w'} →
    {β : Type w} →
      [inst : Monad m] →
        [inst_1 : Std.Iterator α m β] →
          [Std.Iterators.Productive α m] →
            {P : β → Std.Iterators.PostconditionT m (ULift.{w, 0} Bool)} →
              Std.Iterators.ProductivenessRelation (Std.Iterators.Types.TakeWhile α m β P) m
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.getKey_beq : ∀ {α : Type u} {β : α → Type v} (m : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α] [EquivBEq α]
  [LawfulHashable α], (↑m).WF → ∀ {a : α} (h' : m.contains a = true), (m.getKey a h' == a) = true
-- Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian.Point
WeierstrassCurve.Jacobian.neg_of_Z_eq_zero : ∀ {F : Type u} [inst : Field F] {W : WeierstrassCurve.Jacobian F} {P : Fin 3 → F},
  W.Nonsingular P → P 2 = 0 → W.neg P = -(P 1 / P 0) • ![1, 1, 0]
-- Init.System.IO
IO.TaskState.running.sizeOf_spec : sizeOf IO.TaskState.running = 1
-- Mathlib.Analysis.Complex.ValueDistribution.LogCounting.Basic
/-- Special case of `logCounting_add_analyticOn`: Adding a constant does not change the logarithmic
counting function for the poles.
 -/
ValueDistribution.logCounting_add_const : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] [inst_1 : ProperSpace 𝕜] {E : Type u_2}
  [inst_2 : NormedAddCommGroup E] [inst_3 : NormedSpace 𝕜 E] {f : 𝕜 → E} {a₀ : E},
  Meromorphic f → ValueDistribution.logCounting (f + fun x => a₀) ⊤ = ValueDistribution.logCounting f ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.BinaryBicone.IsBilimit.mk.injEq : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {P Q : C} {b : CategoryTheory.Limits.BinaryBicone P Q} (isLimit : CategoryTheory.Limits.IsLimit b.toCone)
  (isColimit : CategoryTheory.Limits.IsColimit b.toCocone) (isLimit_1 : CategoryTheory.Limits.IsLimit b.toCone)
  (isColimit_1 : CategoryTheory.Limits.IsColimit b.toCocone),
  ({ isLimit := isLimit, isColimit := isColimit } = { isLimit := isLimit_1, isColimit := isColimit_1 }) =
    (isLimit = isLimit_1 ∧ isColimit = isColimit_1)
-- LeanSearchClient.Syntax
LeanSearchClient.SearchServer.incompleteSearchQuery : LeanSearchClient.SearchServer → String
-- Mathlib.NumberTheory.Chebyshev
Chebyshev.psi_eq_sum_Icc : ∀ (x : ℝ), Chebyshev.psi x = ∑ n ∈ Finset.Icc 0 ⌊x⌋₊, ArithmeticFunction.vonMangoldt n
-- Mathlib.Control.Monad.Cont
ContT.run_monadLift : ∀ {r : Type u} {m : Type u → Type v} [inst : Monad m] {α : Type u} (x : m α) (k : α → m r),
  (monadLift x).run k = x >>= k
-- Mathlib.Analysis.Normed.Group.Basic
dist_eq_norm_sub : ∀ {E : Type u_5} [inst : SeminormedAddCommGroup E] (a b : E), dist a b = ‖a - b‖
-- Lean.Expr
/-- Return `true` if the given expression is a forall or lambda expression.  -/
Lean.Expr.isBinding : Lean.Expr → Bool
-- Mathlib.SetTheory.Cardinal.Order
/-- A cardinal is a strong pre-limit if it's closed under powersets.

See `IsStrongLimit` for a version excluding `0`.  -/
Cardinal.IsStrongPrelimit : Cardinal.{u_1} → Prop
-- Std.Data.DHashMap.Internal.Raw
Std.DHashMap.Internal.Raw₀.alter.congr_simp : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α]
  (m m_1 : Std.DHashMap.Internal.Raw₀ α β),
  m = m_1 → ∀ (a : α) (f f_1 : Option (β a) → Option (β a)), f = f_1 → m.alter a f = m_1.alter a f_1
-- Mathlib.GroupTheory.Perm.Support
Equiv.Perm.apply_zpow_apply_eq_iff : ∀ {α : Type u_1} (f : Equiv.Perm α) (n : ℤ) {x : α}, f ((f ^ n) x) = (f ^ n) x ↔ f x = x
-- Mathlib.Combinatorics.SimpleGraph.Basic
SimpleGraph.disjoint_edgeSet : ∀ {V : Type u} {G₁ G₂ : SimpleGraph V}, Disjoint G₁.edgeSet G₂.edgeSet ↔ Disjoint G₁ G₂
-- Mathlib.Analysis.SpecialFunctions.Log.Base
Real.logb.eq_1 : ∀ (b x : ℝ), Real.logb b x = Real.log x / Real.log b
-- Mathlib.Order.CompleteLattice.Finset
Finset.maximal_iff_forall_insert : ∀ {α : Type u_2} [inst : DecidableEq α] {P : Finset α → Prop} {s : Finset α},
  (∀ ⦃s t : Finset α⦄, P t → s ⊆ t → P s) → (Maximal P s ↔ P s ∧ ∀ x ∉ s, ¬P (insert x s))
-- Mathlib.Algebra.Order.UpperLower
IsUpperSet.smul_subset : ∀ {α : Type u_1} [inst : CommMonoid α] [inst_1 : Preorder α] [IsOrderedMonoid α] {s : Set α} {x : α},
  IsUpperSet s → 1 ≤ x → x • s ⊆ s
-- Lean.Meta.WHNF
_private.Lean.Meta.WHNF.0.Lean.Meta.isQuotRecStuck? : Lean.QuotVal → Array Lean.Expr → Lean.MetaM (Option Lean.MVarId)
-- Mathlib.Algebra.Homology.HomotopyCategory.SingleFunctors
/-- `HomotopyCategory.singleFunctor C n` is induced by `CochainComplex.singleFunctor C n`.  -/
HomotopyCategory.singleFunctorPostcompQuotientIso : (C : Type u) →
  [inst : CategoryTheory.Category.{v, u} C] →
    [inst_1 : CategoryTheory.Preadditive C] →
      [inst_2 : CategoryTheory.Limits.HasZeroObject C] →
        (n : ℤ) →
          HomotopyCategory.singleFunctor C n ≅
            (CochainComplex.singleFunctor C n).comp (HomotopyCategory.quotient C (ComplexShape.up ℤ))
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.mkHom_hom : ∀ {M N : SemiNormedGrp₁} (f : M ⟶ N), SemiNormedGrp₁.mkHom ↑(SemiNormedGrp₁.Hom.hom f) ⋯ = f
-- Mathlib.Data.Nat.Factorization.Basic
/-- There are exactly `⌊N/n⌋` positive multiples of `n` that are `≤ N`.
See `Nat.card_multiples` for a "shifted-by-one" version.  -/
Nat.card_multiples' : ∀ (N n : ℕ), {k ∈ Finset.range N.succ | k ≠ 0 ∧ n ∣ k}.card = N / n
-- Batteries.Recycling.MonadSatisfying.Basic
MonadSatisfying.instReaderT : {m : Type u_1 → Type u_2} →
  {ρ : Type u_1} → [inst : Monad m] → [inst_1 : LawfulMonad m] → [MonadSatisfying m] → MonadSatisfying (ReaderT ρ m)
-- Mathlib.Topology.MetricSpace.BundledFun
PseudoMetric.sup_apply : ∀ {X : Type u_1} {R : Type u_2} [inst : AddZeroClass R] [inst_1 : SemilatticeSup R] [inst_2 : AddLeftMono R]
  [inst_3 : AddRightMono R] (d d' : PseudoMetric X R) (x y : X), (d ⊔ d') x y = d x y ⊔ d' x y
-- Mathlib.RingTheory.DedekindDomain.Ideal.Lemmas
/-- **Chinese remainder theorem** for a Dedekind domain: if the ideal `I` factors as
`∏ i ∈ s, P i ^ e i`, then `R ⧸ I` factors as `Π (i : s), R ⧸ (P i ^ e i)`.

This is a version of `IsDedekindDomain.quotientEquivPiOfProdEq` where we restrict
the product to a finite subset `s` of a potentially infinite indexing type `ι`.
 -/
IsDedekindDomain.quotientEquivPiOfFinsetProdEq : {R : Type u_1} →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      {ι : Type u_4} →
        {s : Finset ι} →
          (I : Ideal R) →
            (P : ι → Ideal R) →
              (e : ι → ℕ) →
                (∀ i ∈ s, Prime (P i)) →
                  (∀ i ∈ s, ∀ j ∈ s, i ≠ j → P i ≠ P j) →
                    ∏ i ∈ s, P i ^ e i = I → R ⧸ I ≃+* ((i : ↥s) → R ⧸ P ↑i ^ e ↑i)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getKeyD_diff!_of_contains_eq_false_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k fallback : α},
        Std.DTreeMap.Internal.Impl.contains k m₂ = false → (m₁.diff! m₂).getKeyD k fallback = m₁.getKeyD k fallback
-- Mathlib.CategoryTheory.Functor.FullyFaithful
CategoryTheory.Functor.FullyFaithful.mk.congr_simp : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {F : CategoryTheory.Functor C D} (preimage preimage_1 : {X Y : C} → (F.obj X ⟶ F.obj Y) → (X ⟶ Y))
  (e_preimage : preimage = preimage_1) (map_preimage : ∀ {X Y : C} (f : F.obj X ⟶ F.obj Y), F.map (preimage f) = f)
  (preimage_map : ∀ {X Y : C} (f : X ⟶ Y), preimage (F.map f) = f),
  { preimage := preimage, map_preimage := map_preimage, preimage_map := preimage_map } =
    { preimage := preimage_1, map_preimage := ⋯, preimage_map := ⋯ }
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.Path.Ordered.insert : ∀ {α : Type u_1} {cmp : α → α → Ordering} {v : α} {path : RBTree.RBNode.Path α} {t : RBTree.RBNode α},
  RBTree.RBNode.Path.Ordered cmp path →
    RBTree.RBNode.Ordered cmp t →
      RBTree.RBNode.All (RBTree.RBNode.Path.RootOrdered cmp path) t →
        RBTree.RBNode.Path.RootOrdered cmp path v →
          RBTree.RBNode.OnRoot (RBTree.RBNode.cmpEq cmp v) t → RBTree.RBNode.Ordered cmp (path.insert t v)
-- Mathlib.Data.Multiset.Basic
Multiset.mem_toList : ∀ {α : Type u_1} {a : α} {s : Multiset α}, a ∈ s.toList ↔ a ∈ s
-- Mathlib.Algebra.AddConstMap.Basic
AddConstMapClass.map_ofNat' : ∀ {F : Type u_1} {G : Type u_2} {H : Type u_3} [inst : FunLike F G H] {b : H} [inst_1 : AddMonoidWithOne G]
  [inst_2 : AddMonoid H] [AddConstMapClass F G H 1 b] (f : F) (n : ℕ) [inst_4 : n.AtLeastTwo],
  f (OfNat.ofNat n) = f 0 + OfNat.ofNat n • b
-- Mathlib.CategoryTheory.Profunctor.Basic
CategoryTheory.Profunctor.ofCore_obj_map : ∀ {C : Type u₁} {D : Type u₂} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  (P : CategoryTheory.ProfunctorCore.{w, v₁, v₂, u₁, u₂} C D) (X : C) {X_1 Y : Dᵒᵖ} (f : X_1 ⟶ Y),
  ((CategoryTheory.Profunctor.ofCore P).obj X).map f = P.map (CategoryTheory.CategoryStruct.id X) f.unop
-- Mathlib.Tactic.ToDual
lt_of_lt_of_eq'' : ∀ {α : Type u_1} {a b c : α} [inst : LT α], b < a → b = c → c < a
-- Mathlib.NumberTheory.LegendreSymbol.ZModChar
/-- If `n % 4 = 1`, then `χ₄ n = 1`.  -/
ZMod.χ₄_int_one_mod_four : ∀ {n : ℤ}, n % 4 = 1 → ZMod.χ₄ ↑n = 1
-- Mathlib.Algebra.Homology.QuasiIso
isoOfQuasiIsoAt_inv_hom_id_assoc : ∀ {ι : Type u_1} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] {c : ComplexShape ι} {K L : HomologicalComplex C c} (f : K ⟶ L)
  (i : ι) [inst_2 : K.HasHomology i] [inst_3 : L.HasHomology i] [inst_4 : QuasiIsoAt f i] {Z : C}
  (h : L.homology i ⟶ Z),
  CategoryTheory.CategoryStruct.comp (isoOfQuasiIsoAt f i).inv
      (CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap f i) h) =
    h
-- Mathlib.SetTheory.ZFC.VonNeumann
ZFSet.vonNeumann_zero : ZFSet.vonNeumann 0 = ∅
-- Mathlib.Algebra.Group.Equiv.Basic
MulEquiv.monoidHomCongrLeftEquiv_apply : ∀ {M₁ : Type u_5} {M₂ : Type u_6} {N : Type u_8} [inst : MulOneClass M₁] [inst_1 : MulOneClass M₂] [inst_2 : Monoid N]
  (e : M₁ ≃* M₂) (f : M₁ →* N), e.monoidHomCongrLeftEquiv f = f.comp e.symm.toMonoidHom
-- Mathlib.Algebra.Group.Hom.Defs
map_zero : ∀ {M : Type u_4} {N : Type u_5} {F : Type u_9} [inst : Zero M] [inst_1 : Zero N] [inst_2 : FunLike F M N]
  [ZeroHomClass F M N] (f : F), f 0 = 0
-- Std.Data.ExtTreeSet.Basic
/-- Transforms an array into a tree set.  -/
Std.ExtTreeSet.ofArray : {α : Type u} → Array α → (cmp : autoParam (α → α → Ordering) Std.ExtTreeSet.ofArray._auto_1) → Std.ExtTreeSet α cmp
-- Mathlib.RingTheory.DedekindDomain.AdicValuation
IsDedekindDomain.HeightOneSpectrum.algebraMap_adicCompletion_toCompletion : ∀ (R : Type u_1) [inst : CommRing R] [inst_1 : IsDedekindDomain R] (K : Type u_2) {S : Type u_3} [inst_2 : Field K]
  [inst_3 : CommSemiring S] [inst_4 : Algebra R K] [inst_5 : IsFractionRing R K]
  (v : IsDedekindDomain.HeightOneSpectrum R) [inst_6 : Algebra S K] (r : S),
  ((algebraMap S (IsDedekindDomain.HeightOneSpectrum.adicCompletion K v)) r).toCompletion =
    (algebraMap S (IsDedekindDomain.HeightOneSpectrum.valuation K v).Completion) r
-- Lean.PrettyPrinter.Delaborator.TopDownAnalyze
Lean.getPPAnalyzeTrustOfScientific : Lean.Options → Bool
-- Mathlib.Algebra.Group.Subgroup.Lattice
Subgroup.closure_union_one : ∀ {G : Type u_1} [inst : Group G] (s : Set G), Subgroup.closure (s ∪ {1}) = Subgroup.closure s
-- Mathlib.NumberTheory.Padics.PadicIntegers
PadicInt.coe_eq_zero : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)] {x : ℤ_[p]}, ↑x = 0 ↔ x = 0
-- Mathlib.Algebra.Group.Opposite
MulOpposite.instAddCommMonoid : {α : Type u_1} → [AddCommMonoid α] → AddCommMonoid αᵐᵒᵖ
-- Mathlib.CategoryTheory.Comma.Basic
/-- Taking the comma category of two functors into `Discrete PUnit` results in something
is equivalent to their product.  -/
CategoryTheory.Comma.equivProd : {A : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} A] →
    {B : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} B] →
        (L : CategoryTheory.Functor A (CategoryTheory.Discrete PUnit.{u_1 + 1})) →
          (R : CategoryTheory.Functor B (CategoryTheory.Discrete PUnit.{u_1 + 1})) → CategoryTheory.Comma L R ≌ A × B
-- Mathlib.Topology.Algebra.Group.Pointwise
closure_subset_mul_left_of_mem_nhds_one_of_inv : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : Group G] [SeparatelyContinuousMul G] {s : Set G} (s' : Set G),
  s ∈ nhds 1 → (∀ x ∈ s, x⁻¹ ∈ s) → closure s' ⊆ s * s'
-- Mathlib.Algebra.Module.StablyFree.FreeOfInvertible
/-- Let `R` be a commutative ring, `M` be a finite stably free `R`-module.
Then `M` is free if it is invertible.  -/
Module.free_of_isStablyFree_of_invertible : ∀ (R : Type u_1) [inst : CommRing R] (M : Type u_2) [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [Module.IsStablyFree R M] [Module.Invertible R M], Module.Free R M
-- Mathlib.Data.Multiset.MapFold
Multiset.map_coe : ∀ {α : Type u_1} {β : Type v} (f : α → β) (l : List α), Multiset.map f ↑l = ↑(List.map f l)
-- Mathlib.Order.Bounds.Basic
isCofinalFor_or_isCofinalFor_of_directedOn_union : ∀ {α : Type u_1} [inst : Preorder α] {s t : Set α},
  DirectedOn (fun x1 x2 => x1 ≤ x2) (s ∪ t) → IsCofinalFor t s ∨ IsCofinalFor s t
-- Lean.Meta.WrapInstance
/-- Projects application of a structure type to corresponding application of a parent structure.  -/
_private.Lean.Meta.WrapInstance.0.Lean.Meta.getParentStructType? : Lean.Name → Lean.Name → Lean.Expr → Lean.MetaM (Option Lean.Expr)
-- Mathlib.Tactic.Ring.Common
/-- The result of extracting the coefficient is a monic monomial.  -/
Mathlib.Tactic.Ring.Common.ExtractCoeff.e' : {e : Q(ℕ)} → Mathlib.Tactic.Ring.Common.ExtractCoeff e → Q(ℕ)
-- Mathlib.Algebra.Ring.Subring.Pointwise
Subring.pointwise_smul_le_iff₀ : ∀ {M : Type u_1} {R : Type u_2} [inst : GroupWithZero M] [inst_1 : Ring R] [inst_2 : MulSemiringAction M R] {a : M},
  a ≠ 0 → ∀ {S T : Subring R}, a • S ≤ T ↔ S ≤ a⁻¹ • T
-- Lean.Parser.Term.Doc
Lean.Parser.Term.Doc.RecommendedSpelling.mk.sizeOf_spec : ∀ («notation» recommendedSpelling : String) (additionalInformation? : Option String),
  sizeOf
      { «notation» := «notation», recommendedSpelling := recommendedSpelling,
        additionalInformation? := additionalInformation? } =
    1 + sizeOf «notation» + sizeOf recommendedSpelling + sizeOf additionalInformation?
-- Mathlib.Topology.MetricSpace.IsometricSMul
Multiplicative.isIsIsometricVAdd'' : ∀ {M : Type u} [inst : Add M] [inst_1 : PseudoEMetricSpace M] [IsIsometricVAdd Mᵃᵒᵖ M],
  IsIsometricSMul (Multiplicative M)ᵐᵒᵖ (Multiplicative M)
-- Lean.Meta.Tactic.Grind.Arith.Cutsat.Types
Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combineDivCoeffs.sizeOf_spec : ∀ (c₁ c₂ : Lean.Meta.Grind.Arith.Cutsat.LeCnstr) (k : ℤ),
  sizeOf (Lean.Meta.Grind.Arith.Cutsat.LeCnstrProof.combineDivCoeffs c₁ c₂ k) = 1 + sizeOf c₁ + sizeOf c₂ + sizeOf k
-- Init.Data.List.Sublist
List.IsPrefix.ne_nil : ∀ {α : Type u_1} {xs ys : List α}, xs <+: ys → xs ≠ [] → ys ≠ []
-- Mathlib.Algebra.MonoidAlgebra.Basic
MonoidAlgebra.mapDomainRingHom_comp_algebraMap : ∀ {R : Type u_1} {A : Type u_4} {M : Type u_7} {N : Type u_8} [inst : CommSemiring R] [inst_1 : Semiring A]
  [inst_2 : Algebra R A] [inst_3 : Monoid M] [inst_4 : Monoid N] (f : M →* N),
  (MonoidAlgebra.mapDomainRingHom A f).comp (algebraMap R (MonoidAlgebra A M)) = algebraMap R (MonoidAlgebra A N)
-- Mathlib.LinearAlgebra.BilinearForm.IsometryEquiv
/-- The inverse isometric equivalence of an isometric equivalence between two bilinear forms.  -/
LinearMap.BilinForm.IsometryEquiv.symm : {R : Type u_1} →
  {M₁ : Type u_3} →
    {M₂ : Type u_4} →
      [inst : CommSemiring R] →
        [inst_1 : AddCommMonoid M₁] →
          [inst_2 : AddCommMonoid M₂] →
            [inst_3 : Module R M₁] →
              [inst_4 : Module R M₂] →
                {B₁ : LinearMap.BilinForm R M₁} →
                  {B₂ : LinearMap.BilinForm R M₂} → B₁.IsometryEquiv B₂ → B₂.IsometryEquiv B₁
-- Mathlib.RingTheory.Bialgebra.Equiv
BialgEquiv.symm_apply_apply : ∀ {R : Type u} {A : Type v} {B : Type w} [inst : CommSemiring R] [inst_1 : Semiring A] [inst_2 : Semiring B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : CoalgebraStruct R A] [inst_6 : CoalgebraStruct R B]
  (e : A ≃ₐc[R] B) (x : A), e.symm (e x) = x
-- Mathlib.RingTheory.Regular.Category
ModuleCat.smulShortComplex_f_hom_apply : ∀ {R : Type u} [inst : CommRing R] (M : ModuleCat R) (r : R) (x2 : ↑M),
  (ModuleCat.Hom.hom (M.smulShortComplex r).f) x2 = r • x2
-- Mathlib.Logic.Basic
forall_or_exists_not : ∀ {α : Sort u_1} (P : α → Prop), (∀ (a : α), P a) ∨ ∃ a, ¬P a
-- Std.Data.ExtDTreeMap.Basic
/-- Tries to retrieve the mapping for the given key, returning `none` if no such mapping is present.

Uses the `LawfulEqCmp` instance to cast the retrieved value to the correct type.
 -/
Std.ExtDTreeMap.Const.get? : {α : Type u} →
  {cmp : α → α → Ordering} → {β : Type v} → [Std.TransCmp cmp] → Std.ExtDTreeMap α (fun x => β) cmp → α → Option β
-- Std.Http.Data.Status
/-- Returns the standard reason phrase for an HTTP status code as defined in RFC 9110.
For known status codes this returns the canonical phrase (e.g., "OK" for 200).
For unknown codes (`other n s`), returns the caller-supplied reason phrase `s`.
 -/
Std.Http.Status.reasonPhrase : Std.Http.Status → String
-- Mathlib.MeasureTheory.OuterMeasure.Basic
MeasureTheory.measure_eq_top_mono : ∀ {α : Type u_1} {F : Type u_3} [inst : FunLike F (Set α) ENNReal] [MeasureTheory.OuterMeasureClass F α] {μ : F}
  {s t : Set α}, s ⊆ t → μ s = ⊤ → μ t = ⊤
-- Mathlib.Tactic.FieldSimp.Lemmas
Mathlib.Tactic.FieldSimp.NF.mul_eq_eval₁ : ∀ {M : Type u_1} [inst : CommGroupWithZero M] (a₁ : ℤ × M) {a₂ : ℤ × M} {l₁ l₂ l : Mathlib.Tactic.FieldSimp.NF M},
  l₁.eval * (a₂ ::ᵣ l₂).eval = l.eval → (a₁ ::ᵣ l₁).eval * (a₂ ::ᵣ l₂).eval = (a₁ ::ᵣ l).eval
-- Mathlib.Analysis.Calculus.FDeriv.Const
hasFDerivAt_ofNat : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : AddCommGroup E] [inst_2 : Module 𝕜 E]
  [inst_3 : TopologicalSpace E] {F : Type u_3} [inst_4 : AddCommGroup F] [inst_5 : Module 𝕜 F]
  [inst_6 : TopologicalSpace F] (n : ℕ) [inst_7 : OfNat F n] (x : E), HasFDerivAt (OfNat.ofNat n) 0 x
-- Std.Data.ExtDTreeMap.Lemmas
Std.ExtDTreeMap.Const.size_modify : ∀ {α : Type u} {cmp : α → α → Ordering} [inst : Std.TransCmp cmp] {β : Type v} {t : Std.ExtDTreeMap α (fun x => β) cmp}
  {k : α} {f : β → β}, (Std.ExtDTreeMap.Const.modify t k f).size = t.size
-- Mathlib.GroupTheory.GroupAction.Blocks
MulAction.IsBlock.smul_eq_smul_of_subset : ∀ {G : Type u_1} {X : Type u_2} [inst : SMul G X] {B : Set X} {g₁ g₂ : G},
  MulAction.IsBlock G B → g₁ • B ⊆ g₂ • B → g₁ • B = g₂ • B
-- Init.Control.ExceptCps
/-- Adds exceptions of type `ε` to a monad `m`.

Instead of using `Except ε` to model exceptions, this implementation uses continuation passing
style. This has different performance characteristics from `ExceptT ε`.
 -/
ExceptCpsT : Type u → (Type u → Type v) → Type u → Type (max (u + 1) v)
-- Mathlib.Topology.EMetricSpace.BoundedVariation
eVariationOn.constant_on : ∀ {α : Type u_1} [inst : LinearOrder α] {E : Type u_2} [inst_1 : PseudoEMetricSpace E] {f : α → E} {s : Set α},
  (f '' s).Subsingleton → eVariationOn f s = 0
-- Mathlib.Analysis.Normed.Group.Uniform
lipschitzOnWith_inv_iff : ∀ {α : Type u_4} {E : Type u_5} [inst : SeminormedCommGroup E] [inst_1 : PseudoEMetricSpace α] {K : NNReal} {f : α → E}
  {s : Set α}, LipschitzOnWith K f⁻¹ s ↔ LipschitzOnWith K f s
-- Mathlib.Analysis.Complex.UpperHalfPlane.MoebiusAction
UpperHalfPlane.σ_mul : ∀ (g g' : GL (Fin 2) ℝ) (z : ℂ), (UpperHalfPlane.σ (g * g')) z = (UpperHalfPlane.σ g) ((UpperHalfPlane.σ g') z)
-- Init.Data.SInt.Lemmas
Int8.one_mul : ∀ (a : Int8), 1 * a = a
-- Init.Data.UInt.Lemmas
USize.toUInt16_ofNatClamp_of_le : ∀ {n : ℕ},
  USize.size ≤ n →
    (USize.ofNatClamp n).toUInt16 = UInt16.ofNatLT (UInt16.size - 1) UInt32.toUInt16_ofNatClamp_of_le._proof_1
-- Mathlib.Algebra.Field.Basic
Lex.instRatCast : {K : Type u_1} → [RatCast K] → RatCast (Lex K)
-- Mathlib.Topology.Algebra.Module.ContinuousLinearMap.PiProd
ContinuousLinearMap.coe_snd : ∀ {R : Type u_1} [inst : Semiring R] {M₁ : Type u_2} [inst_1 : TopologicalSpace M₁] [inst_2 : AddCommMonoid M₁]
  [inst_3 : Module R M₁] {M₂ : Type u_3} [inst_4 : TopologicalSpace M₂] [inst_5 : AddCommMonoid M₂]
  [inst_6 : Module R M₂], ↑(ContinuousLinearMap.snd R M₁ M₂) = LinearMap.snd R M₁ M₂
-- Mathlib.Topology.Algebra.Monoid
/-- Let `M` be a topological space with a continuous multiplication operation and a `0`.
Let `l` be a filter on `M × M` which is both disjoint from the cocompact filter and less than or
equal to `(𝓝 0).coprod (𝓝 0)`. Then the multiplication map `M × M → M` tends to zero on `l`.  -/
tendsto_mul_nhds_zero_of_disjoint_cocompact : ∀ {M : Type u_3} [inst : TopologicalSpace M] [inst_1 : MulZeroClass M] [ContinuousMul M] {l : Filter (M × M)},
  Disjoint l (Filter.cocompact (M × M)) → l ≤ (nhds 0).coprod (nhds 0) → Filter.Tendsto (fun x => x.1 * x.2) l (nhds 0)
-- Mathlib.LinearAlgebra.Complex.Module
skewAdjoint.negISMul_apply_coe : ∀ {A : Type u_1} [inst : AddCommGroup A] [inst_1 : Module ℂ A] [inst_2 : StarAddMonoid A] [inst_3 : StarModule ℂ A]
  (a : ↥(skewAdjoint A)), ↑(skewAdjoint.negISMul a) = -Complex.I • ↑a
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.isEmpty_alter : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp],
  t.WF →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Raw.Const.alter t k f).isEmpty =
        ((t.isEmpty || t.size == 1 && t.contains k) && (f (Std.DTreeMap.Raw.Const.get? t k)).isNone)
-- Mathlib.Analysis.LocallyConvex.StrongTopology
UniformConvergenceCLM.locallyConvexSpace : ∀ (R : Type u_1) {𝕜₁ : Type u_2} {𝕜₂ : Type u_3} {E : Type u_4} {F : Type u_5} [inst : AddCommGroup E]
  [inst_1 : TopologicalSpace E] [inst_2 : AddCommGroup F] [inst_3 : TopologicalSpace F]
  [inst_4 : IsTopologicalAddGroup F] [inst_5 : Semiring R] [inst_6 : PartialOrder R] [inst_7 : NormedField 𝕜₁]
  [inst_8 : NormedField 𝕜₂] [inst_9 : Module 𝕜₁ E] [inst_10 : Module 𝕜₂ F] {σ : 𝕜₁ →+* 𝕜₂} [inst_11 : Module R F]
  [inst_12 : ContinuousConstSMul R F] [LocallyConvexSpace R F] [inst_14 : SMulCommClass 𝕜₂ R F] (𝔖 : Set (Set E)),
  𝔖.Nonempty → DirectedOn (fun x1 x2 => x1 ⊆ x2) 𝔖 → LocallyConvexSpace R (UniformConvergenceCLM σ F 𝔖)
-- Mathlib.Topology.Category.TopCat.Basic
TopCat.ext : ∀ {X Y : TopCat} {f g : X ⟶ Y},
  (∀ (x : ↑X), (CategoryTheory.ConcreteCategory.hom f) x = (CategoryTheory.ConcreteCategory.hom g) x) → f = g
-- Mathlib.Topology.Algebra.InfiniteSum.Order
isLUB_hasSum' : ∀ {ι : Type u_1} {α : Type u_3} [inst : AddCommMonoid α] [inst_1 : PartialOrder α] [CanonicallyOrderedAdd α]
  [inst_3 : TopologicalSpace α] [OrderClosedTopology α] {f : ι → α} {a : α},
  HasSum f a → IsLUB (Set.range fun s => ∑ i ∈ s, f i) a
-- Mathlib.Algebra.Order.Interval.Finset.SuccPred
Finset.insert_Icc_sub_one_right_eq_Icc : ∀ {α : Type u_2} [inst : LinearOrder α] [inst_1 : One α] [inst_2 : LocallyFiniteOrder α] [inst_3 : Sub α]
  [PredSubOrder α] {a b : α}, a ≤ b → insert b (Finset.Icc a (b - 1)) = Finset.Icc a b
-- Mathlib.Algebra.Order.Monoid.Unbundled.TypeTags
Additive.toMul_top : ∀ {α : Type u_1} [inst : LE α] [inst_1 : OrderTop α], Additive.toMul ⊤ = ⊤
-- Mathlib.Data.Ordmap.Invariants
Ordnode.foldr.eq_2 : ∀ {α : Type u_1} {β : Sort u_2} (f : α → β → β) (x : β) (size : ℕ) (l : Ordnode α) (x_2 : α) (r : Ordnode α),
  Ordnode.foldr f (Ordnode.node size l x_2 r) x = Ordnode.foldr f l (f x_2 (Ordnode.foldr f r x))