mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.SetTheory.Cardinal.Regular
Cardinal.IsRegular.cof_omega_eq : ∀ {o : Ordinal.{u_1}}, (Cardinal.aleph o).IsRegular → (Ordinal.omega o).cof = Cardinal.aleph o
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.size_ofList : ∀ {α : Type u} {cmp : α → α → Ordering} [Std.TransCmp cmp] {l : List α},
  List.Pairwise (fun a b => ¬cmp a b = Ordering.eq) l → (Std.TreeSet.Raw.ofList l cmp).size = l.length
-- Mathlib.Order.Antisymmetrization
not_antisymmRel_of_lt : ∀ {α : Type u_1} {a b : α} [inst : Preorder α], a < b → ¬AntisymmRel (fun x1 x2 => x1 ≤ x2) a b
-- Init.Data.UInt.Bitwise
instAssociativeUInt64HAnd : Std.Associative fun x1 x2 => x1 &&& x2
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.natTransTruncLTOfLE.congr_simp : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b),
  t.natTransTruncLTOfLE a b h = t.natTransTruncLTOfLE a b h
-- Mathlib.Order.Interval.Set.Basic
Set.Ico_eq_Icc_same_iff : ∀ {α : Type u_1} [inst : Preorder α] {a b : α}, Set.Ico b a = Set.Icc b a ↔ ¬b ≤ a
-- Mathlib.Order.BoundedOrder.Basic
isTop_iff_eq_top : ∀ {α : Type u} [inst : PartialOrder α] [inst_1 : OrderTop α] {a : α}, IsTop a ↔ a = ⊤
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteLimits
CategoryTheory.Limits.hasColimitsOfShape_of_hasFiniteColimits : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [CategoryTheory.Limits.HasFiniteColimits C] (J : Type w)
  [inst_2 : CategoryTheory.SmallCategory J] [CategoryTheory.FinCategory J], CategoryTheory.Limits.HasColimitsOfShape J C
-- Init.Internal.Order.Basic
Lean.Order.MonoBind.mk : ∀ {m : Type u → Type v} [inst : Bind m] [inst_1 : (α : Type u) → Lean.Order.PartialOrder (m α)],
  (∀ {α β : Type u} {a₁ a₂ : m α} {f : α → m β},
      Lean.Order.PartialOrder.rel a₁ a₂ → Lean.Order.PartialOrder.rel (a₁ >>= f) (a₂ >>= f)) →
    (∀ {α β : Type u} {a : m α} {f₁ f₂ : α → m β},
        (∀ (x : α), Lean.Order.PartialOrder.rel (f₁ x) (f₂ x)) → Lean.Order.PartialOrder.rel (a >>= f₁) (a >>= f₂)) →
      Lean.Order.MonoBind m
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
/-- The fork defined in `BinaryBicone.fstKernelFork` is indeed a kernel.  -/
CategoryTheory.Limits.BinaryBicone.isLimitFstKernelFork : {C : Type uC} →
  [inst : CategoryTheory.Category.{uC', uC} C] →
    [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C] →
      {X Y : C} →
        {c : CategoryTheory.Limits.BinaryBicone X Y} →
          CategoryTheory.Limits.IsLimit c.toCone → CategoryTheory.Limits.IsLimit c.fstKernelFork
-- Mathlib.Analysis.BoxIntegral.Box.Basic
BoxIntegral.Box.mem_mk : ∀ {ι : Type u_1} {l u x : ι → ℝ} {H : ∀ (i : ι), l i < u i},
  x ∈ { lower := l, upper := u, lower_lt_upper := H } ↔ ∀ (i : ι), x i ∈ Set.Ioc (l i) (u i)
-- Mathlib.Data.Nat.Prime.Defs
Nat.Primes.instRepr : Repr Nat.Primes
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Oplax
CategoryTheory.Oplax.OplaxTrans.whiskerRight_naturality_naturality_assoc : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {F G : CategoryTheory.OplaxFunctor B C} (η : CategoryTheory.Oplax.OplaxTrans F G) {a b : B} {a' : C} {f g : a ⟶ b}
  (β : f ⟶ g) (h : G.obj b ⟶ a') {Z : F.obj a ⟶ a'}
  (h_1 : CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp (η.app a) (G.map g)) h ⟶ Z),
  CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Bicategory.whiskerRight (CategoryTheory.Bicategory.whiskerRight (F.map₂ β) (η.app b)) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality g) h) h_1) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.whiskerRight (η.naturality f) h)
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map f) h).hom
        (CategoryTheory.CategoryStruct.comp
          (CategoryTheory.Bicategory.whiskerLeft (η.app a) (CategoryTheory.Bicategory.whiskerRight (G.map₂ β) h))
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Bicategory.associator (η.app a) (G.map g) h).inv h_1)))
-- Mathlib.Probability.Kernel.Composition.MapComap
/-- Pullback of a kernel, such that for each set s `comap κ g hg c s = κ (g c) s`.
We include measurability in the assumptions instead of using junk values
to make sure that typeclass inference can infer that the `comap` of a Markov kernel
is again a Markov kernel.  -/
ProbabilityTheory.Kernel.comap : {α : Type u_1} →
  {β : Type u_2} →
    {mα : MeasurableSpace α} →
      {mβ : MeasurableSpace β} →
        {γ : Type u_4} →
          {mγ : MeasurableSpace γ} →
            ProbabilityTheory.Kernel α β → (g : γ → α) → Measurable g → ProbabilityTheory.Kernel γ β
-- Mathlib.Analysis.Normed.Group.Basic
enorm_multisetProd_le : ∀ {ε : Type u_9} [inst : TopologicalSpace ε] [inst_1 : ESeminormedCommMonoid ε] (m : Multiset ε),
  ‖m.prod‖ₑ ≤ (Multiset.map (fun x => ‖x‖ₑ) m).sum
-- Mathlib.Order.Monotone.Defs
Monotone.imp : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {a b : α},
  Monotone f → a ≤ b → f a ≤ f b
-- Mathlib.Analysis.Normed.Module.Connected
/-- In a real vector space of dimension `> 1`, the complement of any singleton is path-connected.  -/
isPathConnected_compl_singleton_of_one_lt_rank : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : Module ℝ E] [inst_2 : TopologicalSpace E] [ContinuousAdd E]
  [ContinuousSMul ℝ E], 1 < Module.rank ℝ E → ∀ (x : E), IsPathConnected {x}ᶜ
-- Mathlib.AlgebraicGeometry.Birational.RationalMap
AlgebraicGeometry.Scheme.PartialMap.mk.inj : ∀ {X Y : AlgebraicGeometry.Scheme} {domain : X.Opens} {dense_domain : Dense ↑domain} {hom : ↑domain ⟶ Y}
  {domain_1 : X.Opens} {dense_domain_1 : Dense ↑domain_1} {hom_1 : ↑domain_1 ⟶ Y},
  { domain := domain, dense_domain := dense_domain, hom := hom } =
      { domain := domain_1, dense_domain := dense_domain_1, hom := hom_1 } →
    domain = domain_1 ∧ hom ≍ hom_1
-- Init.Data.UInt.Lemmas
UInt32.toNat_sub_of_le : ∀ (a b : UInt32), b ≤ a → (a - b).toNat = a.toNat - b.toNat
-- Std.Do.Triple.SpecLemmas
Std.Do.Spec.liftWith_OptionT : ∀ {m : Type u → Type v} {ps : Std.Do.PostShape} {α : Type u}
  {Q : Std.Do.PostCond α (Std.Do.PostShape.except PUnit.{u + 1} ps)} [inst : Monad m] [inst_1 : Std.Do.WPMonad m ps]
  (f : ({β : Type u} → OptionT m β → m (Option β)) → m α),
  ⦃(Std.Do.wp (f fun {β} x => x.run)).apply (Q.1, Q.2.2)⦄ MonadControl.liftWith f ⦃Q⦄
-- Mathlib.Data.Stream.Init
Stream'.instInhabited : {α : Type u} → [Inhabited α] → Inhabited (Stream' α)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Equiv.constAlter : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t₁ t₂ : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  (h₁ : t₁.WF) (h₂ : t₂.WF),
  t₁.Equiv t₂ →
    ∀ {k : α} {f : Option β → Option β},
      (Std.DTreeMap.Internal.Impl.Const.alter k f t₁ ⋯).impl.Equiv
        (Std.DTreeMap.Internal.Impl.Const.alter k f t₂ ⋯).impl
-- Mathlib.MeasureTheory.Group.FoelnerFilter
IsAddFoelner.mean_vadd_eq_mean_vadd : ∀ {G : Type u_1} {X : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : AddGroup G]
  [inst_2 : AddAction G X] {ι : Type u_3} {u : Ultrafilter ι} {F : ι → Set X}
  [MeasureTheory.VAddInvariantMeasure G X μ],
  IsAddFoelner G μ (↑u) F → ∀ (g h : G) (s : Set X), IsAddFoelner.mean μ u F (g +ᵥ s) = IsAddFoelner.mean μ u F (h +ᵥ s)
-- Init.Data.String.Lemmas.Splits
String.Pos.splits_prev : ∀ {s : String} (p : s.Pos) (hp : p ≠ s.startPos),
  (p.prev hp).Splits (s.sliceTo (p.prev hp)).copy (String.singleton ((p.prev hp).get ⋯) ++ (s.sliceFrom p).copy)
-- Mathlib.SetTheory.Cardinal.Cofinality.Club
IsClub.sInter_of_cof_le_one : ∀ {α : Type v} [inst : LinearOrder α] {s : Set (Set α)}, Order.cof α ≤ 1 → (∀ x ∈ s, IsClub x) → IsClub (⋂₀ s)
-- Mathlib.Condensed.Light.TopCatAdjunction
_private.Mathlib.Condensed.Light.TopCatAdjunction.0.LightCondSet.coinducingCoprod.match_1.splitter : (X : LightCondSet) →
  (motive : (i : (S : LightProfinite) × X.obj.obj (Opposite.op S)) × ↑i.fst.toTop → Sort u_2) →
    (x : (i : (S : LightProfinite) × X.obj.obj (Opposite.op S)) × ↑i.fst.toTop) →
      ((fst : LightProfinite) → (i : X.obj.obj (Opposite.op fst)) → (s : ↑⟨fst, i⟩.fst.toTop) → motive ⟨⟨fst, i⟩, s⟩) →
        motive x
-- Mathlib.Condensed.Light.Explicit
/-- The light condensed object associated to a presheaf on `LightProfinite` whose postcomposition with
the forgetful functor preserves finite products and satisfies the equalizer condition.
 -/
LightCondensed.ofSheafForgetLightProfinite : {A : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} A] →
    {FA : A → A → Type u_2} →
      {CA : A → Type u_3} →
        [inst_1 : (X Y : A) → FunLike (FA X Y) (CA X) (CA Y)] →
          [inst_2 : CategoryTheory.ConcreteCategory A FA] →
            [CategoryTheory.Limits.ReflectsFiniteLimits (CategoryTheory.forget A)] →
              (F : CategoryTheory.Functor LightProfiniteᵒᵖ A) →
                [CategoryTheory.Limits.PreservesFiniteProducts (F.comp (CategoryTheory.forget A))] →
                  CategoryTheory.regularTopology.EqualizerCondition (F.comp (CategoryTheory.forget A)) →
                    LightCondensed A
-- Lean.Expr
Lean.instReprExpr.repr : Lean.Expr → ℕ → Std.Format
-- Mathlib.Order.InitialSeg
InitialSeg.exists_eq_iff_rel : ∀ {α : Type u_1} {β : Type u_2} {r : α → α → Prop} {s : β → β → Prop} (f : InitialSeg r s) {a : α} {b : β},
  s b (f a) ↔ ∃ a', f a' = b ∧ r a' a
-- Mathlib.NumberTheory.NumberField.Completion.InfinitePlace
NumberField.InfinitePlace.Completion.liesOver_extensionEmbedding_apply : ∀ {K : Type u_1} [inst : Field K] {L : Type u_2} [inst_1 : Field L] (w : NumberField.InfinitePlace L)
  (v : NumberField.InfinitePlace K) [inst_2 : Algebra v.Completion w.Completion] {φ : w.Completion →+* ℂ}
  [NumberField.ComplexEmbedding.LiesOver φ (NumberField.InfinitePlace.Completion.extensionEmbedding v)]
  {x : v.Completion},
  φ ((algebraMap v.Completion w.Completion) x) = (NumberField.InfinitePlace.Completion.extensionEmbedding v) x
-- Mathlib.Algebra.GroupWithZero.Units.Basic
div_mul_cancel₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] {b : G₀} (a : G₀), b ≠ 0 → a / b * b = a
-- Mathlib.LinearAlgebra.TensorProduct.RightExactness
/-- The direct map in `lTensor.equiv`  -/
lTensor.toFun : {R : Type u_1} →
  {M : Type u_2} →
    {N : Type u_3} →
      {P : Type u_4} →
        [inst : CommRing R] →
          [inst_1 : AddCommGroup M] →
            [inst_2 : AddCommGroup N] →
              [inst_3 : AddCommGroup P] →
                [inst_4 : Module R M] →
                  [inst_5 : Module R N] →
                    [inst_6 : Module R P] →
                      {f : M →ₗ[R] N} →
                        {g : N →ₗ[R] P} →
                          (Q : Type u_5) →
                            [inst_7 : AddCommGroup Q] →
                              [inst_8 : Module R Q] →
                                Function.Exact ⇑f ⇑g →
                                  TensorProduct R Q N ⧸ (LinearMap.lTensor Q f).range →ₗ[R] TensorProduct R Q P
-- Mathlib.CategoryTheory.EssentialImage
/-- Get the witnessing object that `Y` is in the subcategory given by `F`.  -/
CategoryTheory.Functor.essImage.witness : {C : Type u₁} →
  {D : Type u₂} →
    [inst : CategoryTheory.Category.{v₁, u₁} C] →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] → {F : CategoryTheory.Functor C D} → {Y : D} → F.essImage Y → C
-- Mathlib.Order.RelSeries
/-- Given two series of the form `a₀ -r→ ... -r→ X` and `X -r→ b ---> ...`,
then `a₀ -r→ ... -r→ X -r→ b ...` is another series obtained by combining the given two.
 -/
RelSeries.smash : {α : Type u_1} → {r : SetRel α α} → (p q : RelSeries r) → p.last = q.head → RelSeries r
-- Mathlib.Data.Set.Card
Set.encard_exchange : ∀ {α : Type u_1} {s : Set α} {a b : α}, a ∉ s → b ∈ s → (insert a (s \ {b})).encard = s.encard
-- Mathlib.GroupTheory.GroupAction.SubMulAction
/-- The natural `MulActionHom` over `R` from a `SubMulAction` of `M` to `M`.  -/
SubMulAction.SMulMemClass.subtype : {R : Type u} →
  {M : Type v} →
    [inst : Monoid R] →
      [inst_1 : MulAction R M] →
        {A : Type u_1} → [inst_2 : SetLike A M] → [hA : SMulMemClass A R M] → (S' : A) → ↥S' →ₑ[id] M
-- Mathlib.GroupTheory.OrderOfElement
AddRightCancelMonoid.injective_nsmul_iff_not_isOfFinAddOrder : ∀ {G : Type u_1} [inst : AddRightCancelMonoid G] {x : G}, (Function.Injective fun n => n • x) ↔ ¬IsOfFinAddOrder x
-- Mathlib.Algebra.Module.Submodule.Defs
Submodule.mk.sizeOf_spec : ∀ {R : Type u} {M : Type v} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] [inst_3 : SizeOf R]
  [inst_4 : SizeOf M] (toAddSubmonoid : AddSubmonoid M)
  (smul_mem' : ∀ (c : R) {x : M}, x ∈ toAddSubmonoid.carrier → c • x ∈ toAddSubmonoid.carrier),
  sizeOf { toAddSubmonoid := toAddSubmonoid, smul_mem' := smul_mem' } = 1 + sizeOf toAddSubmonoid
-- Init.GrindInstances.ToInt
Lean.Grind.instLTInt32SintOfNatNat : Lean.Grind.ToInt.LT Int32 (Lean.Grind.IntInterval.sint 32)
-- Mathlib.Data.ENNReal.Real
ENNReal.le_ofReal_iff_toReal_le : ∀ {a : ENNReal} {b : ℝ}, a ≠ ⊤ → 0 ≤ b → (a ≤ ENNReal.ofReal b ↔ a.toReal ≤ b)
-- Mathlib.Topology.Homeomorph.Defs
/-- Predicate saying that `f` is a homeomorphism.

This should be used only when `f` is a concrete function whose continuous inverse is not easy to
write down. Otherwise, `Homeomorph` should be preferred as it bundles the continuous inverse.

Having both `Homeomorph` and `IsHomeomorph` is justified by the fact that so many function
properties are unbundled in the topology part of the library, and by the fact that a homeomorphism
is not merely a continuous bijection, that is `IsHomeomorph f` is not equivalent to
`Continuous f ∧ Bijective f` but to `Continuous f ∧ Bijective f ∧ IsOpenMap f`.  -/
IsHomeomorph : {X : Type u_1} → {Y : Type u_2} → [TopologicalSpace X] → [TopologicalSpace Y] → (X → Y) → Prop
-- Mathlib.MeasureTheory.Group.Arithmetic
AEMeasurable.const_vadd : ∀ {M : Type u_2} {X : Type u_3} {α : Type u_4} [inst : MeasurableSpace X] [inst_1 : VAdd M X] {m : MeasurableSpace α}
  {μ : MeasureTheory.Measure α} {g : α → X} [MeasurableConstVAdd M X],
  AEMeasurable g μ → ∀ (c : M), AEMeasurable (c +ᵥ g) μ
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.minKey!_le_minKey!_erase : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} [Std.TransCmp cmp]
  [inst : Inhabited α] {k : α}, (t.erase k).isEmpty = false → (cmp t.minKey! (t.erase k).minKey!).isLE = true
-- Init.Data.Ord.Basic
Ordering.isEq_then : ∀ {o₁ o₂ : Ordering}, (o₁.then o₂).isEq = (o₁.isEq && o₂.isEq)
-- Mathlib.Algebra.Order.Kleene
/-- **Alias** of the reverse direction of `add_eq_right_iff_le`. -/
LE.le.add_eq_right : ∀ {α : Type u_1} [inst : IdemSemiring α] {a b : α}, a ≤ b → a + b = b
-- Mathlib.SetTheory.Ordinal.Veblen
Ordinal.le_invVeblen₂_iff : ∀ {a x : Ordinal.{u}}, a ≤ x.invVeblen₂ ↔ Ordinal.veblen x.invVeblen₁ a ≤ Ordinal.omega0 ^ x
-- Mathlib.Topology.FiberBundle.Basic
/-- Characterization of continuous functions (at a point, within a set) into a fiber bundle.  -/
FiberBundle.continuousWithinAt_totalSpace : ∀ {B : Type u_2} (F : Type u_3) {X : Type u_4} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace B]
  [inst_2 : TopologicalSpace F] {E : B → Type u_5} [inst_3 : TopologicalSpace (Bundle.TotalSpace F E)]
  [inst_4 : (b : B) → TopologicalSpace (E b)] [inst_5 : FiberBundle F E] (f : X → Bundle.TotalSpace F E) {s : Set X}
  {x₀ : X},
  ContinuousWithinAt f s x₀ ↔
    ContinuousWithinAt (fun x => (f x).proj) s x₀ ∧
      ContinuousWithinAt (fun x => (↑(trivializationAt F E (f x₀).proj) (f x)).2) s x₀
-- Mathlib.ModelTheory.Semantics
_private.Mathlib.ModelTheory.Semantics.0.FirstOrder.Language.Term.restrictVar.match_1.eq_2 : ∀ {L : FirstOrder.Language} {α : Type u_3} {β : Type u_5} [inst : DecidableEq α]
  (motive : (x : L.Term α) → (↥x.varFinset → β) → Sort u_4) (l : ℕ) (F : L.Functions l) (ts : Fin l → L.Term α)
  (f : ↥(FirstOrder.Language.func F ts).varFinset → β)
  (h_1 : (a : α) → (f : ↥(FirstOrder.Language.var a).varFinset → β) → motive (FirstOrder.Language.var a) f)
  (h_2 :
    (l : ℕ) →
      (F : L.Functions l) →
        (ts : Fin l → L.Term α) →
          (f : ↥(FirstOrder.Language.func F ts).varFinset → β) → motive (FirstOrder.Language.func F ts) f),
  (match FirstOrder.Language.func F ts, f with
    | FirstOrder.Language.var a, f => h_1 a f
    | FirstOrder.Language.func F ts, f => h_2 l F ts f) =
    h_2 l F ts f
-- Init.Data.Range.Polymorphic.Lemmas
Std.Roc.toList_eq_match : ∀ {α : Type u} {r : Std.Roc α} [inst : LE α] [inst_1 : DecidableLE α] [inst_2 : Std.PRange.UpwardEnumerable α]
  [inst_3 : Std.PRange.LawfulUpwardEnumerable α] [Std.PRange.LawfulUpwardEnumerableLE α]
  [inst_5 : Std.Rxc.IsAlwaysFinite α],
  r.toList =
    match Std.PRange.succ? r.lower with
    | none => []
    | some next => if next ≤ r.upper then next :: (next<...=r.upper).toList else []
-- Lean.Data.Lsp.Internal
/-- The dependency that is stale.  -/
Lean.Lsp.LeanStaleDependencyParams.staleDependency : Lean.Lsp.LeanStaleDependencyParams → Lean.Lsp.DocumentUri
-- Mathlib.Topology.Order.PartialSups
Continuous.partialSups_apply : ∀ {L : Type u_1} [inst : SemilatticeSup L] [inst_1 : TopologicalSpace L] [ContinuousSup L] {X : Type u_2}
  [inst_3 : TopologicalSpace X] {f : ℕ → X → L} {n : ℕ},
  (∀ k ≤ n, Continuous (f k)) → Continuous fun a => (partialSups fun x => f x a) n
-- Mathlib.Algebra.Group.Submonoid.Defs
Submonoid.copy_eq : ∀ {M : Type u_1} [inst : MulOneClass M] {S : Submonoid M} {s : Set M} (hs : s = ↑S), S.copy s hs = S
-- Mathlib.Algebra.Symmetrized
SymAlg.sym_eq_zero_iff : ∀ {α : Type u_1} [inst : Zero α] (a : α), SymAlg.sym a = 0 ↔ a = 0
-- Mathlib.Geometry.RingedSpace.Stalks
AlgebraicGeometry.PresheafedSpace.stalkMap.stalkSpecializes_stalkMap_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasColimits C]
  {X Y : AlgebraicGeometry.PresheafedSpace C} (f : X ⟶ Y) {x y : ↑↑X} (h : x ⤳ y) {Z : C}
  (h_1 : X.presheaf.stalk x ⟶ Z),
  CategoryTheory.CategoryStruct.comp (Y.presheaf.stalkSpecializes ⋯)
      (CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f x) h_1) =
    CategoryTheory.CategoryStruct.comp (AlgebraicGeometry.PresheafedSpace.Hom.stalkMap f y)
      (CategoryTheory.CategoryStruct.comp (X.presheaf.stalkSpecializes h) h_1)
-- Mathlib.Algebra.Algebra.NonUnitalHom
NonUnitalAlgHom.coe_restrictScalars' : ∀ (R : Type u_1) {S : Type u_2} {A : Type u_3} {B : Type u_4} [inst : Monoid R] [inst_1 : Monoid S]
  [inst_2 : NonUnitalNonAssocSemiring A] [inst_3 : NonUnitalNonAssocSemiring B] [inst_4 : MulAction R S]
  [inst_5 : DistribMulAction S A] [inst_6 : DistribMulAction S B] [inst_7 : DistribMulAction R A]
  [inst_8 : DistribMulAction R B] [inst_9 : IsScalarTower R S A] [inst_10 : IsScalarTower R S B] (f : A →ₙₐ[S] B),
  ⇑(NonUnitalAlgHom.restrictScalars R f) = ⇑f
-- Lean.Elab.Term.TermElabM
Lean.Elab.Term.MVarErrorKind.custom.injEq : ∀ (msgData msgData_1 : Lean.MessageData),
  (Lean.Elab.Term.MVarErrorKind.custom msgData = Lean.Elab.Term.MVarErrorKind.custom msgData_1) = (msgData = msgData_1)
-- Init.Data.SInt.Bitwise
instIdempotentOpInt16HOr : Std.IdempotentOp fun x1 x2 => x1 ||| x2
-- Lean.Data.Lsp.Basic
Lean.Lsp.instFromJsonStaticRegistrationOptions : Lean.FromJson Lean.Lsp.StaticRegistrationOptions
-- Mathlib.AlgebraicGeometry.ZariskisMainTheorem
AlgebraicGeometry.Scheme.Hom.mem_quasiFiniteLocus : ∀ {X Y : AlgebraicGeometry.Scheme} {f : X ⟶ Y} [inst : AlgebraicGeometry.LocallyOfFiniteType f] {x : ↥X},
  x ∈ AlgebraicGeometry.Scheme.Hom.quasiFiniteLocus f ↔ AlgebraicGeometry.Scheme.Hom.QuasiFiniteAt f x
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.add_def : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : Add α] {s t : Finset α},
  s + t = Finset.image (fun p => p.1 + p.2) (s ×ˢ t)
-- Mathlib.Geometry.Manifold.MFDeriv.SpecificFunctions
MDifferentiableOn.inv : ∀ {𝕜 : 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] {s : Set M} {F' : Type u_21}
  [inst_6 : NormedDivisionRing F'] [inst_7 : NormedAlgebra 𝕜 F'] {p : M → F'},
  MDiff[s] p → (∀ z ∈ s, p z ≠ 0) → MDiff[s] p⁻¹
-- Mathlib.GroupTheory.QuotientGroup.Basic
QuotientAddGroup.quotientBot.eq_1 : ∀ {G : Type u} [inst : AddGroup G],
  QuotientAddGroup.quotientBot = QuotientAddGroup.quotientKerEquivOfRightInverse (AddMonoidHom.id G) id ⋯
-- Std.Do.SPred.DerivedLaws
Std.Do.SPred.Tactic.Have.dup : ∀ {σs : List (Type u)} {P Q H T : Std.Do.SPred σs}, (P ⊣⊢ₛ Q ∧ H) → (P ∧ H ⊢ₛ T) → P ⊢ₛ T
-- Std.Data.TreeMap.Iterator
_private.Std.Data.TreeMap.Iterator.0.Std.TreeMap.iter.eq_1 : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} (m : Std.TreeMap α β cmp),
  m.iter = Std.Iter.map (fun e => (e.fst, e.snd)) m.inner.iter
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.insertMany_list_equiv_foldl : ∀ {α : Type u} {β : α → Type v} (m₁ : Std.DHashMap.Internal.Raw₀ α β) [inst : BEq α] [inst_1 : Hashable α]
  {l : List ((a : α) × β a)}, (↑↑(m₁.insertMany l)).Equiv (List.foldl (fun acc p => acc.insert p.fst p.snd) (↑m₁) l)
-- Mathlib.Topology.Category.TopCat.Opens
TopologicalSpace.Opens.mapMapIso_functor : ∀ {X Y : TopCat} (H : X ≅ Y), (TopologicalSpace.Opens.mapMapIso H).functor = TopologicalSpace.Opens.map H.hom
-- Mathlib.RepresentationTheory.Continuous.TopRep
/-- The `G`-invariant topologicalsubmodule of a topological representation.  -/
TopRep.invariants : {k : Type u} →
  [inst : TopologicalSpace k] → [inst_1 : Ring k] → {G : Type v} → [inst_2 : Group G] → TopRep k G → TopModuleCat k
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.CatCospanTransform
CategoryTheory.Limits.CatCospanTransform.inv_left : ∀ {A : Type u₁} {B : Type u₂} {C : Type u₃} {A' : Type u₄} {B' : Type u₅} {C' : Type u₆}
  [inst : CategoryTheory.Category.{v₁, u₁} A] [inst_1 : CategoryTheory.Category.{v₂, u₂} B]
  [inst_2 : CategoryTheory.Category.{v₃, u₃} C] {F : CategoryTheory.Functor A B} {G : CategoryTheory.Functor C B}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} A'] [inst_4 : CategoryTheory.Category.{v₅, u₅} B']
  [inst_5 : CategoryTheory.Category.{v₆, u₆} C'] {F' : CategoryTheory.Functor A' B'} {G' : CategoryTheory.Functor C' B'}
  {ψ' : CategoryTheory.Limits.CatCospanTransform F G F' G'} (f : ψ' ⟶ ψ') [inst_6 : CategoryTheory.IsIso f],
  CategoryTheory.inv f.left = (CategoryTheory.inv f).left
-- Mathlib.Analysis.InnerProductSpace.Basic
inner_eq_norm_sq_right_iff : ∀ {F : Type u_3} [inst : SeminormedAddCommGroup F] [inst_1 : InnerProductSpace ℝ F] {v w : F},
  inner ℝ v w = ‖w‖ ^ 2 ↔ inner ℝ (v - w) w = 0
-- Mathlib.Analysis.Normed.Module.Ball.Pointwise
ediam_smul₀ : ∀ {𝕜 : Type u_1} {E : Type u_2} [inst : NormedDivisionRing 𝕜] [inst_1 : SeminormedAddCommGroup E] [inst_2 : Module 𝕜 E]
  [NormSMulClass 𝕜 E] (c : 𝕜) (s : Set E), Metric.ediam (c • s) = ‖c‖₊ • Metric.ediam s
-- Mathlib.Analysis.Convex.Extreme
/-- **Alias** of the forward direction of `isExtreme_singleton`.

---

`x` is an extreme point to `A` iff `{x}` is an extreme set of `A`.  -/
IsExtreme.mem_extremePoints : ∀ {𝕜 : 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}, IsExtreme 𝕜 A {x} → x ∈ Set.extremePoints 𝕜 A
-- Mathlib.LinearAlgebra.LinearPMap
LinearPMap.fst_apply : ∀ {R : Type u_1} [inst : Ring R] {E : Type u_4} [inst_1 : AddCommGroup E] [inst_2 : Module R E] {F : Type u_5}
  [inst_3 : AddCommGroup F] [inst_4 : Module R F] (p : Submodule R E) (p' : Submodule R F) (x : ↥(p.prod p')),
  ↑(LinearPMap.fst p p') x = (↑x).1