mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.Probability.Kernel.RadonNikodym
ProbabilityTheory.Kernel.measurable_singularPart_fun : ∀ {α : Type u_1} {γ : Type u_2} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  [hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ] (κ η : ProbabilityTheory.Kernel α γ),
  Measurable fun p =>
    ↑(κ.rnDerivAux (κ + η) p.1 p.2).toNNReal - ↑(1 - κ.rnDerivAux (κ + η) p.1 p.2).toNNReal * κ.rnDeriv η p.1 p.2
-- Mathlib.Probability.Distributions.Uniform
PMF.uniformOfFintype.congr_simp : ∀ (α : Type u_2) [inst : Fintype α] [inst_1 : Nonempty α], PMF.uniformOfFintype α = PMF.uniformOfFintype α
-- Mathlib.CategoryTheory.Comma.Over.Basic
/-- A natural transformation `F ⟶ G` induces a natural transformation on
`Under X` up to `Under.map`.  -/
CategoryTheory.Under.postMap : {T : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} T] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {X : T} →
          {F G : CategoryTheory.Functor T D} →
            (e : F ⟶ G) →
              CategoryTheory.Under.post F ⟶ (CategoryTheory.Under.post G).comp (CategoryTheory.Under.map (e.app X))
-- Mathlib.Data.QPF.Multivariate.Constructions.Fix
MvQPF.wrepr_equiv : ∀ {n : ℕ} {F : TypeVec.{u} (n + 1) → Type u} [q : MvQPF F] {α : TypeVec.{u} n} (x : (MvQPF.P F).W α),
  MvQPF.WEquiv (MvQPF.wrepr x) x
-- Mathlib.Combinatorics.SimpleGraph.Walk.Maps
SimpleGraph.Walk.transfer_eq_map_ofLE : ∀ {V : Type u} {G : SimpleGraph V} {u v : V} (p : G.Walk u v) {H : SimpleGraph V} (hp : ∀ e ∈ p.edges, e ∈ H.edgeSet)
  (GH : G ≤ H), p.transfer H hp = SimpleGraph.Walk.map (SimpleGraph.Hom.ofLE GH) p
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
le_sub_comm : ∀ {α : Type u} [inst : AddCommGroup α] [inst_1 : LE α] [AddLeftMono α] {a b c : α}, a ≤ b - c ↔ c ≤ b - a
-- Mathlib.GroupTheory.GroupAction.Basic
AddAction.instDecidablePredMemSetFixedByAddOfDecidableEq : {M : Type u} →
  [inst : AddMonoid M] →
    {β : Type u_1} →
      [inst_1 : AddAction M β] → (m : M) → [DecidableEq β] → DecidablePred fun b => b ∈ AddAction.fixedBy β m
-- Mathlib.CategoryTheory.Limits.Shapes.Images
/-- If `f` and `g` are isomorphic arrows, then an image factorisation of `f`
gives an image factorisation of `g`  -/
CategoryTheory.Limits.ImageFactorisation.ofArrowIso : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {f g : CategoryTheory.Arrow C} →
      CategoryTheory.Limits.ImageFactorisation f.hom →
        (sq : f ⟶ g) → [CategoryTheory.IsIso sq] → CategoryTheory.Limits.ImageFactorisation g.hom
-- Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr
Std.Tactic.BVDecide.BVExpr.Return.mk.inj : ∀ {aig : Std.Sat.AIG Std.Tactic.BVDecide.BVBit} {w : ℕ} {result : aig.ExtendingRefVecEntry w}
  {cache : Std.Tactic.BVDecide.BVExpr.Cache (↑result).aig} {result_1 : aig.ExtendingRefVecEntry w}
  {cache_1 : Std.Tactic.BVDecide.BVExpr.Cache (↑result_1).aig},
  { result := result, cache := cache } = { result := result_1, cache := cache_1 } → result = result_1 ∧ cache ≍ cache_1
-- Mathlib.Logic.Unique
/-- If the domain of a surjective function is a singleton,
then the codomain is a singleton as well.  -/
Function.Surjective.unique : {β : Sort u_2} → {α : Sort u} → (f : α → β) → Function.Surjective f → [Unique α] → Unique β
-- Mathlib.CategoryTheory.Square
CategoryTheory.Square.mk.sizeOf_spec : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : SizeOf C] {X₁ X₂ X₃ X₄ : C} (f₁₂ : X₁ ⟶ X₂)
  (f₁₃ : X₁ ⟶ X₃) (f₂₄ : X₂ ⟶ X₄) (f₃₄ : X₃ ⟶ X₄)
  (fac : CategoryTheory.CategoryStruct.comp f₁₂ f₂₄ = CategoryTheory.CategoryStruct.comp f₁₃ f₃₄),
  sizeOf { X₁ := X₁, X₂ := X₂, X₃ := X₃, X₄ := X₄, f₁₂ := f₁₂, f₁₃ := f₁₃, f₂₄ := f₂₄, f₃₄ := f₃₄, fac := fac } =
    1 + sizeOf X₁ + sizeOf X₂ + sizeOf X₃ + sizeOf X₄ + sizeOf f₁₂ + sizeOf f₁₃ + sizeOf f₂₄ + sizeOf f₃₄ + sizeOf fac
-- Mathlib.Analysis.Calculus.Gradient.Basic
hasGradientAt_iff_tendsto : ∀ {𝕜 : Type u_1} {F : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedAddCommGroup F] [inst_2 : InnerProductSpace 𝕜 F]
  [inst_3 : CompleteSpace F] {f : F → 𝕜} {f' x : F},
  HasGradientAt f f' x ↔ Filter.Tendsto (fun x' => ‖x' - x‖⁻¹ * ‖f x' - f x - inner 𝕜 f' (x' - x)‖) (nhds x) (nhds 0)
-- Mathlib.Topology.Category.TopCat.Limits.Products
TopCat.prodIsoProd_hom_apply : ∀ {X Y : TopCat} (x : ↑(X ⨯ Y)),
  (CategoryTheory.ConcreteCategory.hom (X.prodIsoProd Y).hom) x =
    ((CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.fst) x,
      (CategoryTheory.ConcreteCategory.hom CategoryTheory.Limits.prod.snd) x)
-- Mathlib.Topology.VectorBundle.Basic
Bundle.Trivialization.symmₗ_apply_of_notMem : ∀ {R : Type u_1} {B : Type u_2} {F : Type u_3} {E : B → Type u_4} [inst : Semiring R] [inst_1 : TopologicalSpace F]
  [inst_2 : TopologicalSpace B] [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)] [inst_4 : AddCommMonoid F]
  [inst_5 : Module R F] [inst_6 : (x : B) → AddCommMonoid (E x)] [inst_7 : (x : B) → Module R (E x)]
  (e : Bundle.Trivialization F Bundle.TotalSpace.proj) [inst_8 : Bundle.Trivialization.IsLinear R e] {b : B},
  b ∉ e.baseSet → ∀ (y : F), (Bundle.Trivialization.symmₗ R e b) y = 0
-- Std.Time.Format.Modifier
Std.Time.Modifier.u.injEq : ∀ (presentation presentation_1 : Std.Time.Year),
  (Std.Time.Modifier.u presentation = Std.Time.Modifier.u presentation_1) = (presentation = presentation_1)
-- Mathlib.Algebra.SkewMonoidAlgebra.Lift
SkewMonoidAlgebra.coeff_equivMapDomain : ∀ {k : Type u_1} {G : Type u_2} {H : Type u_3} [inst : AddCommMonoid k] (f : G ≃ H) (l : SkewMonoidAlgebra k G),
  (SkewMonoidAlgebra.equivMapDomain f l).coeff = Finsupp.equivMapDomain f l.coeff
-- Std.Data.Internal.List.Associative
_private.Std.Data.Internal.List.Associative.0.Std.Internal.List.antisymm_subtype : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] [Std.TransOrd α] [inst_2 : BEq α] [Std.LawfulBEqOrd α]
  {l : List ((a : α) × β a)}, Std.Internal.List.DistinctKeys l → Std.Antisymm fun x1 x2 => x1 ≤ x2
-- Mathlib.Order.Filter.AtTopBot.Archimedean
Filter.Tendsto.atBot_zsmul_const : ∀ {α : Type u_1} {R : Type u_2} {l : Filter α} {r : R} [inst : AddCommGroup R] [inst_1 : LinearOrder R]
  [IsOrderedAddMonoid R] [Archimedean R] {f : α → ℤ},
  0 < r → Filter.Tendsto f l Filter.atBot → Filter.Tendsto (fun x => f x • r) l Filter.atBot
-- Init.Data.UInt.Bitwise
USize.shiftLeft_eq_shiftLeft_mod : ∀ (a b : USize), a <<< b = a <<< (b % USize.ofNat System.Platform.numBits)
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.npow.eq_1 : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : One α] [inst_2 : Mul α],
  Finset.npow = { pow := fun s n => npowRec n s }
-- Mathlib.Analysis.Normed.Ring.WithAbs
WithAbs.ofAbs_injective : ∀ {R : Type u_1} {S : Type u_2} [inst : Semiring S] [inst_1 : PartialOrder S] [inst_2 : Semiring R]
  (v : AbsoluteValue R S), Function.Injective WithAbs.ofAbs
-- Mathlib.Data.Set.Card
Set.three_lt_ncard_iff : ∀ {α : Type u_1} {s : Set α},
  autoParam s.Finite Set.three_lt_ncard_iff._auto_1 →
    (3 < s.ncard ↔ ∃ a b c d, a ∈ s ∧ b ∈ s ∧ c ∈ s ∧ d ∈ s ∧ a ≠ b ∧ a ≠ c ∧ a ≠ d ∧ b ≠ c ∧ b ≠ d ∧ c ≠ d)
-- Std.Data.Iterators.Lemmas.Equivalence.HetT
Std.Iterators.HetT.map_eq_pure_bind : ∀ {m : Type w → Type w'} [inst : Monad m] [LawfulMonad m] {α : Type u} {β : Type v} {f : α → β}
  {x : Std.Iterators.HetT m α}, Std.Iterators.HetT.map f x = x.bind (Std.Iterators.HetT.pure ∘ f)
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.forIn_iterM_id : ∀ {n : Type (max u_1 u_2) → Type u_3} {ps : Std.Do.PostShape} [inst : Monad n] [inst_1 : Std.Do.WPMonad n ps]
  {α β γ : Type (max u_1 u_2)} [inst_2 : Std.Iterator α Id β] [Std.Iterators.Finite α Id]
  [inst_4 : Std.IteratorLoop α Id n] [Std.LawfulIteratorLoop α Id n] {init : γ} {f : β → γ → n (ForInStep γ)}
  {it : Std.IterM Id β} (inv : Std.Do.Invariant it.toList.run γ ps),
  (∀ (pref : List β) (cur : β) (suff : List β) (h : it.toList.run = pref ++ cur :: suff) (b : γ),
      ⦃inv.1 ({ «prefix» := pref, suffix := cur :: suff, property := ⋯ }, b)⦄
        f cur b ⦃(fun r =>
          match r with
          | ForInStep.yield b' => inv.1 ({ «prefix» := pref ++ [cur], suffix := suff, property := ⋯ }, b')
          | ForInStep.done b' => inv.1 ({ «prefix» := it.toList.run, suffix := [], property := ⋯ }, b'),
          inv.2)⦄) →
    ⦃inv.1 ({ «prefix» := [], suffix := it.toList.run, property := ⋯ }, init)⦄
      forIn it init f ⦃(fun b => inv.1 ({ «prefix» := it.toList.run, suffix := [], property := ⋯ }, b), inv.2)⦄
-- Init.Data.UInt.Lemmas
UInt8.toUInt32_ofBitVec : ∀ {b : BitVec 8}, { toBitVec := b }.toUInt32 = { toBitVec := BitVec.setWidth 32 b }
-- Std.Data.TreeMap.Lemmas
Std.TreeMap.Equiv.of_forall_contains_unit_eq : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] [Std.LawfulEqCmp cmp] {t₁ t₂ : Std.TreeMap α Unit cmp},
  (∀ (k : α), t₁.contains k = t₂.contains k) → t₁.Equiv t₂
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.toList_filterMap! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {γ : Type w} {t : Std.DTreeMap.Internal.Impl α fun x => β}
  {f : α → β → Option γ},
  t.WF →
    Std.DTreeMap.Internal.Impl.Const.toList (Std.DTreeMap.Internal.Impl.filterMap! f t) =
      List.filterMap (fun p => Option.map (fun x => (p.1, x)) (f p.1 p.2)) (Std.DTreeMap.Internal.Impl.Const.toList t)
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.get!_eq_default : ∀ {α : Type u} {β : α → Type v} {m : Std.DHashMap.Raw α β} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : LawfulBEq α],
  m.WF → ∀ {a : α} [inst_3 : Inhabited (β a)], a ∉ m → m.get! a = default
-- Mathlib.CategoryTheory.Subobject.MonoOver
CategoryTheory.MonoOver.forget_obj_hom : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X : C} {f : CategoryTheory.MonoOver X},
  ((CategoryTheory.MonoOver.forget X).obj f).hom = f.arrow
-- Mathlib.CategoryTheory.Limits.Types.ColimitType
/-- a family of maps to `pt`  -/
CategoryTheory.Functor.CoconeTypes.ι : {J : Type u} →
  [inst : CategoryTheory.Category.{v, u} J] →
    {F : CategoryTheory.Functor J (Type w₀)} → (self : F.CoconeTypes) → (j : J) → F.obj j → self.pt
-- Mathlib.CategoryTheory.Sites.Sheaf
/-- This is stated as a lemma to prevent class search from forming a loop since a sheaf morphism is
monic if and only if it is monic as a presheaf morphism (under suitable assumption).  -/
CategoryTheory.Sheaf.Hom.mono_of_presheaf_mono : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] (J : CategoryTheory.GrothendieckTopology C) (A : Type u₂)
  [inst_1 : CategoryTheory.Category.{v₂, u₂} A] {F G : CategoryTheory.Sheaf J A} (f : F ⟶ G)
  [h : CategoryTheory.Mono f.hom], CategoryTheory.Mono f
-- Mathlib.Computability.Ackermann
ack.eq_3 : ∀ (m n : ℕ), ack m.succ n.succ = ack m (ack (m + 1) n)
-- Std.Data.HashMap.Lemmas
Std.HashMap.getKey_insertMany_list_of_mem : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.HashMap α β} [EquivBEq α] [LawfulHashable α]
  {l : List (α × β)} {k k' : α},
  (k == k') = true →
    List.Pairwise (fun a b => (a.1 == b.1) = false) l →
      k ∈ List.map Prod.fst l → ∀ {h : k' ∈ m.insertMany l}, (m.insertMany l).getKey k' h = k
-- Mathlib.Algebra.Free
FreeAddSemigroup.mk.sizeOf_spec : ∀ {α : Type u} [inst : SizeOf α] (head : α) (tail : List α),
  sizeOf { head := head, tail := tail } = 1 + sizeOf head + sizeOf tail
-- Init.Data.Range.Polymorphic.IntLemmas
Int.toList_roc_eq_nil_iff : ∀ {m n : ℤ}, (m<...=n).toList = [] ↔ n ≤ m
-- Mathlib.Topology.Algebra.OpenSubgroup
OpenSubgroup.instInhabited : {G : Type u_1} → [inst : Group G] → [inst_1 : TopologicalSpace G] → Inhabited (OpenSubgroup G)
-- Mathlib.Topology.MetricSpace.MetricSeparated
/-- **Alias** of `Metric.IsSeparated.of_subsingleton`. -/
Set.Subsingleton.isSeparated : ∀ {X : Type u_1} [inst : PseudoEMetricSpace X] {s : Set X} {ε : ENNReal}, s.Subsingleton → Metric.IsSeparated ε s
-- Mathlib.Topology.Algebra.Group.Pointwise
IsOpen.sub_left : ∀ {G : Type w} [inst : TopologicalSpace G] [inst_1 : AddGroup G] [IsTopologicalAddGroup G] {s t : Set G},
  IsOpen t → IsOpen (s - t)
-- Std.Internal.Do.Order.Basic
Lean.Order.CompleteLattice.ofProp_apply_3 : ∀ {σ₁ : Type u_1} {σ₂ : Type u_2} {σ₃ : Type u_3} (p : Prop) (s₁ : σ₁) (s₂ : σ₂) (s₃ : σ₃),
  Lean.Order.CompleteLattice.ofProp p s₁ s₂ s₃ = p
-- Mathlib.RingTheory.TensorProduct.Basic
TensorProduct.instStarMul : {R : Type u_1} →
  {A : Type u_2} →
    {B : Type u_3} →
      [inst : CommSemiring R] →
        [inst_1 : NonUnitalNonAssocSemiring A] →
          [inst_2 : NonUnitalNonAssocSemiring B] →
            [inst_3 : Module R A] →
              [inst_4 : Module R B] →
                [inst_5 : SMulCommClass R A A] →
                  [inst_6 : SMulCommClass R B B] →
                    [inst_7 : IsScalarTower R A A] →
                      [inst_8 : IsScalarTower R B B] →
                        [inst_9 : StarRing R] →
                          [inst_10 : StarRing A] →
                            [inst_11 : StarRing B] → [StarModule R A] → [StarModule R B] → StarMul (TensorProduct R A B)
-- Mathlib.GroupTheory.Perm.Subgroup
Equiv.Perm.sigmaCongrRightHom.decidableMemRange : {α : Type u_1} →
  {β : α → Type u_2} →
    [DecidableEq α] →
      [(a : α) → DecidableEq (β a)] →
        [Fintype α] → [(a : α) → Fintype (β a)] → DecidablePred fun x => x ∈ (Equiv.Perm.sigmaCongrRightHom β).range
-- Mathlib.Order.Completion
DedekindCut.lowerBounds_right : ∀ {α : Type u_1} [inst : Preorder α] (A : DedekindCut α), lowerBounds A.right = A.left
-- Mathlib.Algebra.Category.Grp.Basic
AddGrpCat.ofHom_comp : ∀ {X Y Z : Type u} [inst : AddGroup X] [inst_1 : AddGroup Y] [inst_2 : AddGroup Z] (f : X →+ Y) (g : Y →+ Z),
  AddGrpCat.ofHom (g.comp f) = CategoryTheory.CategoryStruct.comp (AddGrpCat.ofHom f) (AddGrpCat.ofHom g)
-- Init.Grind.Ordered.Linarith
_private.Init.Grind.Ordered.Linarith.0.Lean.Grind.Linarith.instBEqPoly.beq.match_1.eq_3 : ∀ (motive : Lean.Grind.Linarith.Poly → Lean.Grind.Linarith.Poly → Sort u_1) (x x_1 : Lean.Grind.Linarith.Poly)
  (h_1 : Unit → motive Lean.Grind.Linarith.Poly.nil Lean.Grind.Linarith.Poly.nil)
  (h_2 :
    (a : ℤ) →
      (a_1 : Lean.Grind.Linarith.Var) →
        (a_2 : Lean.Grind.Linarith.Poly) →
          (b : ℤ) →
            (b_1 : Lean.Grind.Linarith.Var) →
              (b_2 : Lean.Grind.Linarith.Poly) →
                motive (Lean.Grind.Linarith.Poly.add a a_1 a_2) (Lean.Grind.Linarith.Poly.add b b_1 b_2))
  (h_3 : (x x_2 : Lean.Grind.Linarith.Poly) → motive x x_2),
  (x = Lean.Grind.Linarith.Poly.nil → x_1 = Lean.Grind.Linarith.Poly.nil → False) →
    (∀ (a : ℤ) (a_1 : Lean.Grind.Linarith.Var) (a_2 : Lean.Grind.Linarith.Poly) (b : ℤ) (b_1 : Lean.Grind.Linarith.Var)
        (b_2 : Lean.Grind.Linarith.Poly),
        x = Lean.Grind.Linarith.Poly.add a a_1 a_2 → x_1 = Lean.Grind.Linarith.Poly.add b b_1 b_2 → False) →
      (match x, x_1 with
        | Lean.Grind.Linarith.Poly.nil, Lean.Grind.Linarith.Poly.nil => h_1 ()
        | Lean.Grind.Linarith.Poly.add a a_1 a_2, Lean.Grind.Linarith.Poly.add b b_1 b_2 => h_2 a a_1 a_2 b b_1 b_2
        | x, x_4 => h_3 x x_4) =
        h_3 x x_1
-- Mathlib.Analysis.Normed.Group.SemiNormedGrp
SemiNormedGrp₁.iso_isometry : ∀ {V W : SemiNormedGrp₁} (i : V ≅ W), Isometry ⇑↑(SemiNormedGrp₁.Hom.hom i.hom)
-- Mathlib.RingTheory.FractionalIdeal.Extended
FractionalIdeal.extended_eq_zero_iff : ∀ {A : Type u_1} [inst : CommRing A] {B : Type u_2} [inst_1 : CommRing B] {f : A →+* B} {K : Type u_3} {M : Submonoid A}
  [inst_2 : CommRing K] [inst_3 : Algebra A K] [inst_4 : IsLocalization M K] (L : Type u_4) {N : Submonoid B}
  [inst_5 : CommRing L] [inst_6 : Algebra B L] [inst_7 : IsLocalization N L] (hf : M ≤ Submonoid.comap f N)
  {I : FractionalIdeal M K} [IsDomain B], Function.Injective ⇑f → 0 ∉ N → (FractionalIdeal.extended L hf I = 0 ↔ I = 0)
-- Mathlib.AlgebraicTopology.SimplicialSet.Skeleton
SSet.skeletonOfMono_succ : ∀ {X Y : SSet} (i : X ⟶ Y) (n : ℕ),
  (SSet.skeletonOfMono i) (n + 1) =
    (SSet.skeletonOfMono i) n ⊔
      ⨆ x, ⨆ (_ : ↑x ∉ (SSet.Subcomplex.range i).obj (Opposite.op { len := n })), SSet.Subcomplex.ofSimplex ↑x
-- Mathlib.Geometry.Manifold.Instances.Real
instIsManifoldRealEuclideanSpaceFinOfNatNatEuclideanHalfSpaceModelWithCornersEuclideanHalfSpaceElemIcc : ∀ {n : WithTop ℕ∞}, IsManifold (modelWithCornersEuclideanHalfSpace 1) n ↑(Set.Icc 0 1)
-- Mathlib.CategoryTheory.Monad.Kleisli
CategoryTheory.Kleisli.mk : {C : Type u} → [inst : CategoryTheory.Category.{v, u} C] → (T : CategoryTheory.Monad C) → C → CategoryTheory.Kleisli T
-- Mathlib.NumberTheory.Zsqrtd.Basic
Zsqrtd.mk.inj : ∀ {d re im re_1 im_1 : ℤ}, { re := re, im := im } = { re := re_1, im := im_1 } → re = re_1 ∧ im = im_1
-- Mathlib.Analysis.Normed.Group.Defs
AddGroupSeminorm.toSeminormedAddGroup.eq_1 : ∀ {E : Type u_5} [inst : AddGroup E] (f : AddGroupSeminorm E),
  f.toSeminormedAddGroup =
    { norm := ⇑f, toAddGroup := inst, dist := fun x y => f (-x + y), dist_self := ⋯, dist_comm := ⋯, dist_triangle := ⋯,
      edist_dist := ⋯, uniformity_dist := ⋯, cobounded_sets := ⋯, dist_eq := ⋯ }
-- Mathlib.GroupTheory.OrderOfElement
Pi.addOrderOf_eq_sInf : ∀ {ι : Type u_6} {α : ι → Type u_7} [inst : (i : ι) → AddMonoid (α i)] (x : (i : ι) → α i),
  addOrderOf x = sInf {n | n > 0 ∧ ∀ (i : ι), addOrderOf (x i) ∣ n}
-- Mathlib.AlgebraicTopology.SimplicialSet.AnodyneExtensions.PairingCore
SSet.Subcomplex.PairingCore.nonDegenerate₁ : ∀ {X : SSet} {A : X.Subcomplex} (self : A.PairingCore) (s : self.ι), self.simplex s ∈ X.nonDegenerate (self.dim s + 1)
-- Mathlib.Data.Finset.Sym
Finset.mk_mem_sym2_iff : ∀ {α : Type u_1} {s : Finset α} {a b : α}, s(a, b) ∈ s.sym2 ↔ a ∈ s ∧ b ∈ s
-- Init.Data.List.Perm
List.perm_append_left_iff : ∀ {α : Type u_1} {l₁ l₂ : List α} (l : List α), (l ++ l₁).Perm (l ++ l₂) ↔ l₁.Perm l₂
-- Mathlib.MeasureTheory.Measure.AEMeasurable
AEMeasurable.comp_measurable : ∀ {α : Type u_2} {β : Type u_3} {δ : Type u_5} {m0 : MeasurableSpace α} [inst : MeasurableSpace β]
  [inst_1 : MeasurableSpace δ] {μ : MeasureTheory.Measure α} {f : α → δ} {g : δ → β},
  AEMeasurable g (MeasureTheory.Measure.map f μ) → Measurable f → AEMeasurable (g ∘ f) μ
-- Mathlib.Analysis.Calculus.FDeriv.Basic
/-- **Alias** of the reverse direction of `hasFDerivWithinAt_insert`. -/
HasFDerivWithinAt.insert' : ∀ {𝕜 : 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] {f : E → F} {f' : E →L[𝕜] F} {x : E} {s : Set E} [T1Space E] {y : E},
  HasFDerivWithinAt f f' s x → HasFDerivWithinAt f f' (insert y s) x
-- Mathlib.Data.Set.Finite.Basic
Finite.Set.finite_insert : ∀ {α : Type u} (a : α) (s : Set α) [Finite ↑s], Finite ↑(insert a s)
-- Mathlib.Order.Interval.Set.Pi
Set.image_update_Ioc_left : ∀ {ι : Type u_1} {α : ι → Type u_2} [inst : DecidableEq ι] [inst_1 : (i : ι) → PartialOrder (α i)] (f : (i : ι) → α i)
  (i : ι) (a : α i), Function.update f i '' Set.Ioc a (f i) = Set.Ioc (Function.update f i a) f
-- Mathlib.CategoryTheory.Category.TwoP
TwoP_swap_comp_forget_to_Bipointed : TwoP.swap.comp (CategoryTheory.forget₂ TwoP Bipointed) = (CategoryTheory.forget₂ TwoP Bipointed).comp Bipointed.swap
-- Mathlib.Order.Filter.Germ.Basic
Filter.Germ.instSemiring : {α : Type u_1} → {l : Filter α} → {R : Type u_5} → [Semiring R] → Semiring (l.Germ R)
-- Mathlib.Data.List.Cycle
Cycle.toFinset_toMultiset : ∀ {α : Type u_1} [inst : DecidableEq α] (s : Cycle α), s.toMultiset.toFinset = s.toFinset
-- Std.Data.ExtTreeSet.Lemmas
Std.ExtTreeSet.get?_union_of_not_mem_left : ∀ {α : Type u} {cmp : α → α → Ordering} {t₁ t₂ : Std.ExtTreeSet α cmp} [inst : Std.TransCmp cmp] {k : α},
  k ∉ t₁ → (t₁ ∪ t₂).get? k = t₂.get? k
-- Mathlib.Analysis.Convex.Function
StrictConvexOn.subset : ∀ {𝕜 : Type u_1} {E : Type u_2} {β : Type u_5} [inst : Semiring 𝕜] [inst_1 : PartialOrder 𝕜] [inst_2 : AddCommMonoid E]
  [inst_3 : AddCommMonoid β] [inst_4 : PartialOrder β] [inst_5 : SMul 𝕜 E] [inst_6 : SMul 𝕜 β] {s : Set E} {f : E → β}
  {t : Set E}, StrictConvexOn 𝕜 t f → s ⊆ t → Convex 𝕜 s → StrictConvexOn 𝕜 s f
-- Mathlib.Topology.Algebra.AsymptoticCone
AffineSpace.asymptoticNhds_zero : ∀ {k : Type u_1} {V : Type u_2} {P : Type u_3} [inst : Field k] [inst_1 : LinearOrder k] [inst_2 : AddCommGroup V]
  [inst_3 : Module k V] [inst_4 : AddTorsor V P] [inst_5 : TopologicalSpace V] [inst_6 : TopologicalSpace k]
  [OrderTopology k] [IsStrictOrderedRing k] [IsTopologicalAddGroup V] [ContinuousSMul k V],
  AffineSpace.asymptoticNhds k P 0 = ⊤
-- Mathlib.Data.Real.ConjExponents
/-- For `r`, instead of `p`  -/
NNReal.HolderTriple.inv_pos' : ∀ {p q r : NNReal}, p.HolderTriple q r → 0 < r⁻¹
-- Mathlib.Order.Heyting.Hom
HeytingHom.instHeytingHomClass : ∀ {α : Type u_2} {β : Type u_3} [inst : HeytingAlgebra α] [inst_1 : HeytingAlgebra β],
  HeytingHomClass (HeytingHom α β) α β
-- Mathlib.Data.Nat.Choose.Sum
Finset.sum_antidiagonal_choose_succ_nsmul : ∀ {M : Type u_2} [inst : AddCommMonoid M] (f : ℕ → ℕ → M) (n : ℕ),
  ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal (n + 1), (n + 1).choose ij.1 • f ij.1 ij.2 =
    ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, n.choose ij.1 • f ij.1 (ij.2 + 1) +
      ∑ ij ∈ Finset.HasAntidiagonal.antidiagonal n, n.choose ij.2 • f (ij.1 + 1) ij.2
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanImportClosureParams.mk : Array Lean.Lsp.DocumentUri → Lean.Lsp.LeanImportClosureParams
-- Mathlib.Analysis.CStarAlgebra.CompletelyPositiveMap
CompletelyPositiveMap.mk : {A₁ : Type u_1} →
  {A₂ : Type u_2} →
    [inst : NonUnitalCStarAlgebra A₁] →
      [inst_1 : NonUnitalCStarAlgebra A₂] →
        [inst_2 : PartialOrder A₁] →
          [inst_3 : PartialOrder A₂] →
            [inst_4 : StarOrderedRing A₁] →
              [inst_5 : StarOrderedRing A₂] →
                (toLinearMap : A₁ →ₗ[ℂ] A₂) →
                  (∀ (k : ℕ) (M : CStarMatrix (Fin k) (Fin k) A₁), 0 ≤ M → 0 ≤ M.map ⇑toLinearMap) →
                    CompletelyPositiveMap A₁ A₂
-- Init.Data.List.MinMaxIdx
_private.Init.Data.List.MinMaxIdx.0.List.minIdxOn.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → Sort u_2) (y : α) (ys : List α) (h_1 : Unit → motive [])
  (h_2 : (y : α) → (ys : List α) → motive (y :: ys)),
  (match y :: ys with
    | [] => h_1 ()
    | y :: ys => h_2 y ys) =
    h_2 y ys
-- Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
Finset.sum_ite_eq_of_mem : ∀ {ι : Type u_1} {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : DecidableEq ι] (s : Finset ι) (a : ι) (b : ι → M),
  a ∈ s → (∑ x ∈ s, if a = x then b x else 0) = b a
-- Mathlib.Data.List.Sigma
List.perm_nodupKeys : ∀ {α : Type u} {β : α → Type v} {l₁ l₂ : List (Sigma β)}, l₁.Perm l₂ → (l₁.NodupKeys ↔ l₂.NodupKeys)
-- Mathlib.CategoryTheory.Limits.Shapes.ZeroMorphisms
CategoryTheory.Limits.instMonoι_1 : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {β : Type w} [inst_2 : DecidableEq β] (f : β → C) [inst_3 : CategoryTheory.Limits.HasProduct f] (b : β),
  CategoryTheory.Mono (CategoryTheory.Limits.Pi.ι f b)
-- Init.Data.BitVec.Lemmas
BitVec.xor_cast : ∀ {w w' : ℕ} {x y : BitVec w} (h : w = w'), BitVec.cast h x ^^^ BitVec.cast h y = BitVec.cast h (x ^^^ y)
-- Mathlib.MeasureTheory.OuterMeasure.Caratheodory
MeasureTheory.OuterMeasure.top_caratheodory : ∀ {α : Type u_1}, ⊤.caratheodory = ⊤
-- Mathlib.Order.WellFoundedSet
Set.PartiallyWellOrderedOn.ProdLex_iff : ∀ {α : Type u_2} {β : Type u_3} [inst : PartialOrder α] [inst_1 : Preorder β] {s : Set (Lex (α × β))},
  s.IsPWO ↔ ((fun x => (ofLex x).1) '' s).IsPWO ∧ ∀ (a : α), {y | toLex (a, y) ∈ s}.IsPWO