mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.CategoryTheory.Limits.Preserves.Shapes.Zero
/-- A zero functor preserves colimits.  -/
CategoryTheory.Functor.preservesColimitsOfSize_of_isZero : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasZeroObject D] [CategoryTheory.Limits.HasZeroMorphisms D] (G : CategoryTheory.Functor C D),
  CategoryTheory.Limits.IsZero G → CategoryTheory.Limits.PreservesColimitsOfSize.{v, u, v₁, v₂, u₁, u₂} G
-- Mathlib.Order.Concept
mem_upperPolar_singleton : ∀ {α : Type u_2} {β : Type u_3} (r : α → β → Prop) {a : α} {b : β}, b ∈ upperPolar r {a} ↔ r a b
-- Aesop.Tree.Data
Aesop.Rapp.setSuccessProbability : Aesop.Percent → Aesop.Rapp → Aesop.Rapp
-- Std.Http.Data.Headers.Basic
/-- Proof that the transfer codings satisfy the chunked placement rules.
 -/
Std.Http.Header.TransferEncoding.isValid : ∀ (self : Std.Http.Header.TransferEncoding), Std.Http.Header.TransferEncoding.Validate self.codings = true
-- Mathlib.Order.GameAdd
/-- `Sym2.GameAdd rα x y` means that `x` can be reached from `y` by decreasing either entry with
respect to the relation `rα`.

See `Prod.GameAdd` for the ordered pair analog.  -/
Sym2.GameAdd : {α : Type u_1} → (α → α → Prop) → Sym2 α → Sym2 α → Prop
-- Mathlib.GroupTheory.GroupAction.Pointwise
vadd_preimage_set_subsetₛₗ : ∀ {M : Type u_1} {N : Type u_2} {F : Type u_3} {α : Type u_4} {β : Type u_5} {σ : M → N} [inst : VAdd M α]
  [inst_1 : VAdd N β] [inst_2 : FunLike F α β] [AddActionSemiHomClass F σ α β] (f : F) (c : M) (t : Set β),
  c +ᵥ ⇑f ⁻¹' t ⊆ ⇑f ⁻¹' (σ c +ᵥ t)
-- Mathlib.Topology.Algebra.Module.ClosedSubmodule
ClosedSubmodule.mem_top : ∀ {R : Type u_2} {M : Type u_3} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : TopologicalSpace M]
  [inst_3 : Module R M] {x : M}, x ∈ ⊤
-- Mathlib.Order.SuccPred.InitialSeg
PrincipalSeg.map_succ : ∀ {α : Type u_1} {β : Type u_2} [inst : PartialOrder α] [inst_1 : PartialOrder β] [inst_2 : SuccOrder α] [NoMaxOrder α]
  [inst_4 : SuccOrder β] (f : α <i β) (a : α), f.toRelEmbedding (Order.succ a) = Order.succ (f.toRelEmbedding a)
-- Std.Do.SPred.SVal
Std.Do.SVal.curry_uncurry : ∀ {α : Type u} {σs : List (Type u)} {f : Std.Do.SVal σs α}, Std.Do.SVal.curry f.uncurry = f
-- Mathlib.ModelTheory.Satisfiability
FirstOrder.Language.Theory.IsMaximal.isComplete : ∀ {L : FirstOrder.Language} {T : L.Theory}, T.IsMaximal → T.IsComplete
-- Mathlib.Topology.AlexandrovDiscrete
alexandrovDiscrete_iSup : ∀ {ι : Sort u_1} {α : Type u_3} {t : ι → TopologicalSpace α}, (∀ (i : ι), AlexandrovDiscrete α) → AlexandrovDiscrete α
-- Mathlib.Algebra.Category.ModuleCat.Sheaf.Generators
/-- A sheaf of modules is of finite type if locally, it is generated by finitely
many sections.  -/
SheafOfModules.IsFiniteType : {C : Type u'} →
  [inst : CategoryTheory.Category.{v', u'} C] →
    {J : CategoryTheory.GrothendieckTopology C} →
      {R : CategoryTheory.Sheaf J RingCat} →
        [∀ (X : C), CategoryTheory.HasWeakSheafify (J.over X) AddCommGrpCat] →
          [∀ (X : C), (J.over X).WEqualsLocallyBijective AddCommGrpCat] → SheafOfModules R → Prop
-- Mathlib.Algebra.Order.Monoid.Unbundled.Basic
StrictMono.add_const : ∀ {α : Type u_1} {β : Type u_2} [inst : Add α] [inst_1 : Preorder α] [inst_2 : Preorder β] {f : β → α}
  [AddRightStrictMono α], StrictMono f → ∀ (c : α), StrictMono fun x => f x + c
-- Mathlib.CategoryTheory.Bicategory.LocallyGroupoid
CategoryTheory.Bicategory.Pith.pseudofunctorToPith_mapComp_inv_iso_inv : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {B' : Type u₂} [inst_1 : CategoryTheory.Bicategory B']
  [inst_2 : CategoryTheory.Bicategory.IsLocallyGroupoid B'] (F : CategoryTheory.Pseudofunctor B' B) {a b c : B'}
  (f : a ⟶ b) (g : b ⟶ c),
  ((CategoryTheory.Bicategory.Pith.pseudofunctorToPith F).mapComp f g).inv.iso.inv = (F.mapComp f g).hom
-- Mathlib.Tactic.NormNum.Ineq
/-- The `norm_num` extension which identifies expressions of the form `a ≤ b`,
such that `norm_num` successfully recognises both `a` and `b`.  -/
Mathlib.Meta.NormNum.evalLE : Mathlib.Meta.NormNum.NormNumExt
-- Mathlib.CategoryTheory.Bicategory.Grothendieck
CategoryTheory.Pseudofunctor.Grothendieck.map_id_eq : ∀ {𝒮 : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} 𝒮]
  (F : CategoryTheory.Pseudofunctor (CategoryTheory.LocallyDiscrete 𝒮) CategoryTheory.Cat),
  CategoryTheory.Pseudofunctor.Grothendieck.map (CategoryTheory.CategoryStruct.id F) =
    CategoryTheory.Functor.id F.Grothendieck
-- Lean.Language.Basic
Lean.Language.SnapshotTree.mk.injEq : ∀ (element : Lean.Language.Snapshot) (children : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree))
  (element_1 : Lean.Language.Snapshot) (children_1 : Array (Lean.Language.SnapshotTask Lean.Language.SnapshotTree)),
  ({ element := element, children := children } = { element := element_1, children := children_1 }) =
    (element = element_1 ∧ children = children_1)
-- Mathlib.Order.Interval.Set.Infinite
Set.Iio_infinite : ∀ {α : Type u_1} [inst : Preorder α] [NoMinOrder α] (a : α), (Set.Iio a).Infinite
-- Mathlib.Algebra.Category.Grp.Preadditive
AddCommGrpCat.homAddEquiv_apply : ∀ {M N : AddCommGrpCat} (a : M ⟶ N), AddCommGrpCat.homAddEquiv a = CategoryTheory.ConcreteCategory.hom a
-- Mathlib.Algebra.BigOperators.ModEq
Int.ModEq.listProd_one : ∀ {n : ℤ} {l : List ℤ}, (∀ x ∈ l, x ≡ 1 [ZMOD n]) → l.prod ≡ 1 [ZMOD n]
-- Mathlib.Probability.Independence.CharacteristicFunction
ProbabilityTheory.iIndepFun.charFun_map_sum_eq_prod : ∀ {Ω : Type u_1} {mΩ : MeasurableSpace Ω} {P : MeasureTheory.Measure Ω} {ι : Type u_2} {E : Type u_3}
  [inst : MeasurableSpace E] [inst_1 : NormedAddCommGroup E] [BorelSpace E] [SecondCountableTopology E] {X : ι → Ω → E}
  [inst_4 : Fintype ι] [inst_5 : InnerProductSpace ℝ E],
  (∀ (i : ι), AEMeasurable (X i) P) →
    ProbabilityTheory.iIndepFun X P →
      MeasureTheory.charFun (MeasureTheory.Measure.map (∑ i, X i) P) =
        ∏ i, MeasureTheory.charFun (MeasureTheory.Measure.map (X i) P)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.Const.get?_eq_some_get! : ∀ {α : Type u} {instOrd : Ord α} {β : Type v} {t : Std.DTreeMap.Internal.Impl α fun x => β} [Std.TransOrd α]
  [inst : Inhabited β],
  t.WF → ∀ {a : α}, a ∈ t → Std.DTreeMap.Internal.Impl.Const.get? t a = some (Std.DTreeMap.Internal.Impl.Const.get! t a)
-- Mathlib.RingTheory.Polynomial.Chebyshev
_private.Mathlib.RingTheory.Polynomial.Chebyshev.0.Polynomial.Chebyshev.T.match_1.eq_1 : ∀ (motive : ℤ → Sort u_1) (h_1 : Unit → motive 0) (h_2 : Unit → motive 1)
  (h_3 : (n : ℕ) → motive (Int.ofNat n.succ.succ)) (h_4 : (n : ℕ) → motive (Int.negSucc n)),
  (match 0 with
    | 0 => h_1 ()
    | 1 => h_2 ()
    | Int.ofNat n.succ.succ => h_3 n
    | Int.negSucc n => h_4 n) =
    h_1 ()
-- Mathlib.Order.Partition.Finpartition
/-- `⊥` is the partition in singletons, aka discrete partition.  -/
Finpartition.instBotFinset : {α : Type u_1} → [inst : DecidableEq α] → (s : Finset α) → Bot (Finpartition s)
-- Mathlib.LinearAlgebra.RootSystem.Finite.G2
RootPairing.EmbeddedG2.instIsG2OfIsIrreducible : ∀ {ι : Type u_1} {R : Type u_2} {M : Type u_3} {N : Type u_4} [inst : CommRing R] [inst_1 : AddCommGroup M]
  [inst_2 : Module R M] [inst_3 : AddCommGroup N] [inst_4 : Module R N] (P : RootPairing ι R M N) [P.EmbeddedG2]
  [P.IsIrreducible], P.IsG2
-- Mathlib.Algebra.Field.Defs
/-- However `NNRat.cast` is defined, it must be propositionally equal to `a / b`.

Do not use this lemma directly. Use `NNRat.cast_def` instead.  -/
Semifield.nnratCast_def : ∀ {K : Type u_2} [self : Semifield K] (q : ℚ≥0), ↑q = ↑q.num / ↑q.den
-- Mathlib.CategoryTheory.Monad.Algebra
CategoryTheory.Monad.Algebra.Hom.ext : ∀ {C : Type u₁} {inst : CategoryTheory.Category.{v₁, u₁} C} {T : CategoryTheory.Monad C} {A B : T.Algebra}
  {x y : A.Hom B}, x.f = y.f → x = y
-- Init.Data.Int.Gcd
Int.gcd_pow_right_of_gcd_eq_one : ∀ {n m : ℤ} {k : ℕ}, n.gcd m = 1 → n.gcd (m ^ k) = 1
-- Mathlib.NumberTheory.Real.Irrational
Irrational.natCast_add : ∀ {x : ℝ}, Irrational x → ∀ (m : ℕ), Irrational (↑m + x)
-- Init.Data.Bool
Bool.not_and_self : ∀ (x : Bool), (!x && x) = false
-- Mathlib.Order.SupClosed
SemilatticeSup.toCompleteSemilatticeSup.eq_1 : ∀ {α : Type u_3} [inst : SemilatticeSup α] (sSup : Set α → α) (h : ∀ (s : Set α), SupClosed s → IsLUB s (sSup s)),
  SemilatticeSup.toCompleteSemilatticeSup sSup h =
    { toPartialOrder := inst.toPartialOrder, sSup := fun s => sSup (supClosure s), isLUB_sSup := ⋯ }
-- Aesop.Frontend.RuleExpr
Aesop.Frontend.RuleConfig.validateForAdditionalRules : {m : Type → Type} →
  [Monad m] → [Lean.MonadError m] → Aesop.Frontend.RuleConfig → Aesop.RuleSetName → m Aesop.Frontend.RuleConfig
-- Mathlib.Analysis.CStarAlgebra.GelfandNaimarkSegal
/-- The Hilbert space constructed from a positive linear functional on a C⋆-algebra.
 -/
PositiveLinearMap.GNS : {A : Type u_1} →
  [inst : NonUnitalCStarAlgebra A] → [inst_1 : PartialOrder A] → (A →ₚ[ℂ] ℂ) → [StarOrderedRing A] → Type u_1
-- Mathlib.Tactic.ClickSuggestions.FindPremises
/-- Is the choice non-empty?  -/
_private.Mathlib.Tactic.ClickSuggestions.FindPremises.0.Mathlib.Tactic.ClickSuggestions.Choice.any : Mathlib.Tactic.ClickSuggestions.Choice → Bool
-- Init.Data.Dyadic.Basic
Int.trailingZeros_two_mul_add_one : ∀ (i : ℤ), (2 * i + 1).trailingZeros = 0
-- Mathlib.Topology.MetricSpace.Algebra
Pi.instIsBoundedSMul : ∀ {ι : Type u_3} [inst : Fintype ι] {α : Type u_4} {β : ι → Type u_5} [inst_1 : PseudoMetricSpace α]
  [inst_2 : (i : ι) → PseudoMetricSpace (β i)] [inst_3 : Zero α] [inst_4 : (i : ι) → Zero (β i)]
  [inst_5 : (i : ι) → SMul α (β i)] [∀ (i : ι), IsBoundedSMul α (β i)], IsBoundedSMul α ((i : ι) → β i)
-- Mathlib.CategoryTheory.Category.Bipointed
Bipointed.swapEquiv_symm : Bipointed.swapEquiv.symm = Bipointed.swapEquiv
-- Mathlib.CategoryTheory.Groupoid.Subgroupoid
CategoryTheory.Subgroupoid.comap_mono : ∀ {C : Type u} [inst : CategoryTheory.Groupoid C] {D : Type u_1} [inst_1 : CategoryTheory.Groupoid D]
  (φ : CategoryTheory.Functor C D) (S T : CategoryTheory.Subgroupoid D),
  S ≤ T → CategoryTheory.Subgroupoid.comap φ S ≤ CategoryTheory.Subgroupoid.comap φ T
-- Mathlib.Order.Filter.Ultrafilter.Defs
/-- An ultrafilter is a minimal (maximal in the set order) proper filter.  -/
Ultrafilter : Type u_2 → Type u_2
-- Mathlib.Topology.LocallyFinsupp
/-- A proof that the support is locally finite within `U`  -/
Function.locallyFinsuppWithin.supportLocallyFiniteWithinDomain' : ∀ {X : Type u_1} [inst : TopologicalSpace X] {U : Set X} {Y : Type u_2} [inst_1 : Zero Y]
  (self : Function.locallyFinsuppWithin U Y), ∀ z ∈ U, ∃ t ∈ nhds z, (t ∩ Function.support self.toFun).Finite
-- Mathlib.Algebra.Ring.Equiv
RingEquiv.coe_toEquiv : ∀ {R : Type u_4} {S : Type u_5} [inst : Mul R] [inst_1 : Mul S] [inst_2 : Add R] [inst_3 : Add S] (f : R ≃+* S),
  ⇑↑f = ⇑f
-- Mathlib.Algebra.Homology.ShortComplex.PreservesHomology
CategoryTheory.ShortComplex.mapHomologyIso'_hom_naturality_assoc : ∀ {C : Type u_1} {D : Type u_2} [inst : CategoryTheory.Category.{v_1, u_1} C]
  [inst_1 : CategoryTheory.Category.{v_2, u_2} D] [inst_2 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_3 : CategoryTheory.Limits.HasZeroMorphisms D] {S₁ S₂ : CategoryTheory.ShortComplex C} (φ : S₁ ⟶ S₂)
  (F : CategoryTheory.Functor C D) [inst_4 : F.PreservesZeroMorphisms] [inst_5 : S₁.HasHomology]
  [inst_6 : S₂.HasHomology] [inst_7 : (S₁.map F).HasHomology] [inst_8 : (S₂.map F).HasHomology]
  [inst_9 : F.PreservesRightHomologyOf S₁] [inst_10 : F.PreservesRightHomologyOf S₂] {Z : D}
  (h : F.obj S₂.homology ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.ShortComplex.homologyMap (F.mapShortComplex.map φ))
      (CategoryTheory.CategoryStruct.comp (S₂.mapHomologyIso' F).hom h) =
    CategoryTheory.CategoryStruct.comp (S₁.mapHomologyIso' F).hom
      (CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.ShortComplex.homologyMap φ)) h)
-- Mathlib.MeasureTheory.VectorMeasure.BoundedVariation
BoundedVariationOn.vectorMeasure.congr_simp : ∀ {α : Type u_1} [inst : LinearOrder α] [inst_1 : DenselyOrdered α] [inst_2 : TopologicalSpace α]
  [inst_3 : OrderTopology α] [inst_4 : SecondCountableTopology α] [inst_5 : CompactIccSpace α] [hα : MeasurableSpace α]
  [inst_6 : BorelSpace α] {E : Type u_2} [inst_7 : NormedAddCommGroup E] [inst_8 : CompleteSpace E] {f f_1 : α → E}
  (e_f : f = f_1) (hf : BoundedVariationOn f Set.univ), hf.vectorMeasure = ⋯.vectorMeasure
-- Init.Control.StateCps
StateCpsT.instMonadLiftOfMonad : {σ : Type u} → {m : Type u → Type v} → [Monad m] → MonadLift m (StateCpsT σ m)
-- Mathlib.CategoryTheory.Galois.IsFundamentalgroup
CategoryTheory.PreGaloisCategory.action_ext_of_isGalois : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{u₂, u₁} C] (F : CategoryTheory.Functor C FintypeCat) {G : Type u_1}
  [inst_1 : Group G] [inst_2 : (X : C) → MulAction G (F.obj X).obj] [CategoryTheory.PreGaloisCategory.IsNaturalSMul F G]
  [inst_4 : CategoryTheory.GaloisCategory C] [CategoryTheory.PreGaloisCategory.FiberFunctor F] {t : F ⟶ F} {X : C}
  [CategoryTheory.PreGaloisCategory.IsGalois X] {g : G} (x : (F.obj X).obj),
  g • x = (CategoryTheory.ConcreteCategory.hom (t.app X)) x →
    ∀ (y : (F.obj X).obj), g • y = (CategoryTheory.ConcreteCategory.hom (t.app X)) y
-- Mathlib.Algebra.Group.Pointwise.Finset.Basic
Finset.image_add_left' : ∀ {α : Type u_2} [inst : DecidableEq α] [inst_1 : AddGroup α] {t : Finset α} {a : α},
  Finset.image (fun b => -a + b) t = t.preimage (fun b => a + b) ⋯
-- Std.Data.TreeMap.Raw.Lemmas
Std.TreeMap.Raw.getElem?_erase : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.TreeMap.Raw α β cmp} [Std.TransCmp cmp],
  t.WF → ∀ {k a : α}, (t.erase k)[a]? = if cmp k a = Ordering.eq then none else t[a]?
-- Mathlib.RingTheory.Spectrum.Prime.ConstructibleSet
PrimeSpectrum.BasicConstructibleSetData.instDecidableEq : {R : Type u_1} → DecidableEq (PrimeSpectrum.BasicConstructibleSetData R)
-- Mathlib.RingTheory.HahnSeries.Lex
HahnSeries.embDomainOrderEmbedding_apply : ∀ {Γ : Type u_1} {R : Type u_2} [inst : LinearOrder Γ] [inst_1 : PartialOrder R] {Γ' : Type u_3}
  [inst_2 : LinearOrder Γ'] (f : Γ ↪o Γ') [inst_3 : Zero R] (a : Lex (HahnSeries Γ R)),
  (HahnSeries.embDomainOrderEmbedding f) a = toLex (HahnSeries.embDomain f (ofLex a))
-- Mathlib.Algebra.Ring.Int.Defs
Int.instIsDomain : IsDomain ℤ
-- Init.Data.BitVec.Basic
BitVec.natCast_eq_ofNat : ∀ (w x : ℕ), ↑x = BitVec.ofNat w x
-- Mathlib.Topology.Order.Basic
nhdsGE_eq_iInf_inf_principal : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : Preorder α] [OrderTopology α] (a : α),
  nhdsWithin a (Set.Ici a) = (⨅ u, ⨅ (_ : a < u), Filter.principal (Set.Iio u)) ⊓ Filter.principal (Set.Ici a)
-- Init.Data.Bool
Bool.beq_comm : ∀ {α : Type u_1} [inst : BEq α] [LawfulBEq α] {a b : α}, (a == b) = (b == a)
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.Const.getD_insertMany_list_of_contains_eq_false : ∀ {α : Type u} {cmp : α → α → Ordering} {β : Type v} {t : Std.DTreeMap.Raw α (fun x => β) cmp} [Std.TransCmp cmp]
  [inst : BEq α] [Std.LawfulBEqCmp cmp],
  t.WF →
    ∀ {l : List (α × β)} {k : α} {fallback : β},
      (List.map Prod.fst l).contains k = false →
        Std.DTreeMap.Raw.Const.getD (Std.DTreeMap.Raw.Const.insertMany t l) k fallback =
          Std.DTreeMap.Raw.Const.getD t k fallback
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore.le₃₃' : ∀ {ι : Type u_2} {κ : Type u_3} [inst : Preorder ι] {c : ℤ → ComplexShape κ} {r₀ : ℤ}
  (data : CategoryTheory.Abelian.SpectralObject.SpectralSequenceDataCore ι c r₀) {r r' : ℤ} (hrr' : r + 1 = r')
  (hr : r₀ ≤ r) (pq' : κ) {i₃ i₃' : ι}, i₃ = data.i₃ r pq' ⋯ → i₃' = data.i₃ r' pq' ⋯ → i₃ ≤ i₃'
-- Mathlib.Order.Filter.Pointwise
Filter.vaddAssocClass : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : VAdd α β] [inst_1 : VAdd α γ] [inst_2 : VAdd β γ]
  [VAddAssocClass α β γ], VAddAssocClass α β (Filter γ)
-- Mathlib.NumberTheory.ZetaValues
antideriv_bernoulliFun : ∀ (k : ℕ) (x : ℝ), HasDerivAt (fun x => bernoulliFun (k + 1) x / (↑k + 1)) (bernoulliFun k x) x
-- Mathlib.Data.Nat.GCD.Basic
Nat.Coprime.of_dvd_left : ∀ {a₁ a₂ b : ℕ}, a₁ ∣ a₂ → a₂.Coprime b → a₁.Coprime b
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.mk_zpow : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G] (x : G) (n : ℤ),
  SeparationQuotient.mk (x ^ n) = SeparationQuotient.mk x ^ n
-- Mathlib.Order.Monotone.Basic
StrictAnti.isMin_of_apply : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [inst_1 : Preorder β] {f : α → β} {a : α},
  StrictAnti f → IsMax (f a) → IsMin a
-- Mathlib.Algebra.Order.Sub.Defs
/-- See `tsub_tsub_cancel_of_le` for the equality.  -/
tsub_tsub_le : ∀ {α : Type u_1} [inst : Preorder α] [inst_1 : AddCommSemigroup α] [inst_2 : Sub α] [OrderedSub α] {a b : α},
  b - (b - a) ≤ a
-- Mathlib.Algebra.Group.Pointwise.Set.Basic
/-- The singleton operation as a `MulHom`.  -/
Set.singletonMulHom : {α : Type u_2} → [inst : Mul α] → α →ₙ* Set α
-- Mathlib.Algebra.Polynomial.Basic
Polynomial.sum_monomial_eq : ∀ {R : Type u} [inst : Semiring R] (p : Polynomial R), (p.sum fun n a => (Polynomial.monomial n) a) = p
-- Mathlib.Topology.Algebra.Group.Basic
/-- Let `A` and `B` be topological groups, and let `φ : A → B` be a continuous surjective group
homomorphism. Assume furthermore that `φ` is a quotient map (i.e., `V ⊆ B`
is open iff `φ⁻¹ V` is open). Then `φ` is an open quotient map, and in particular an open map.  -/
MonoidHom.isOpenQuotientMap_of_isQuotientMap : ∀ {A : Type u_1} [inst : Group A] [inst_1 : TopologicalSpace A] [ContinuousMul A] {B : Type u_2} [inst_3 : Group B]
  [inst_4 : TopologicalSpace B] {F : Type u_3} [inst_5 : FunLike F A B] [MonoidHomClass F A B] {φ : F},
  Topology.IsQuotientMap ⇑φ → IsOpenQuotientMap ⇑φ
-- Std.Data.DHashMap.Internal.RawLemmas
Std.DHashMap.Internal.Raw₀.Const.get!_inter_of_contains_eq_false_left : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.DHashMap.Internal.Raw₀ α fun x => β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited β],
  (↑m₁).WF →
    (↑m₂).WF → ∀ {k : α}, m₁.contains k = false → Std.DHashMap.Internal.Raw₀.Const.get! (m₁.inter m₂) k = default
-- Mathlib.CategoryTheory.EssentiallySmall
CategoryTheory.instSmallArrowOfLocallySmall : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [Small.{w, u} C] [CategoryTheory.LocallySmall.{w, v, u} C],
  Small.{w, max u v} (CategoryTheory.Arrow C)
-- Mathlib.Topology.MetricSpace.HausdorffDistance
/-- **Alias** of `Metric.infEDist_le_edist_of_mem`.

---

The edist to a set is bounded above by the edist to any of its points  -/
EMetric.infEdist_le_edist_of_mem : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x y : α} {s : Set α}, y ∈ s → Metric.infEDist x s ≤ edist x y
-- Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer
_private.Mathlib.CategoryTheory.Limits.Shapes.FiniteMultiequalizer.0.CategoryTheory.Limits.WalkingMulticospan.instFinCategoryOfLOfDecidableEqR.match_7.eq_1 : ∀ {J : CategoryTheory.Limits.MulticospanShape}
  (motive :
    (b : J.R) →
      (a : J.L) →
        (CategoryTheory.Limits.WalkingMulticospan.left a ⟶ CategoryTheory.Limits.WalkingMulticospan.right b) →
          J.fst b = a → J.snd b = a → Sort u_3)
  (a : J.R) (h₁ : J.fst a = J.fst a) (h₂ : J.snd a = J.fst a)
  (h_1 :
    (a : J.R) →
      (h₁ : J.fst a = J.fst a) →
        (h₂ : J.snd a = J.fst a) → motive a (J.fst a) (CategoryTheory.Limits.WalkingMulticospan.Hom.fst a) h₁ h₂)
  (h_2 :
    (a : J.R) →
      (h₁ : J.fst a = J.snd a) →
        (h₂ : J.snd a = J.snd a) → motive a (J.snd a) (CategoryTheory.Limits.WalkingMulticospan.Hom.snd a) h₁ h₂),
  (match a, J.fst a, CategoryTheory.Limits.WalkingMulticospan.Hom.fst a, h₁, h₂ with
    | a, .(J.fst a), CategoryTheory.Limits.WalkingMulticospan.Hom.fst .(a), h₁, h₂ => h_1 a h₁ h₂
    | a, .(J.snd a), CategoryTheory.Limits.WalkingMulticospan.Hom.snd .(a), h₁, h₂ => h_2 a h₁ h₂) =
    h_1 a h₁ h₂
-- Mathlib.MeasureTheory.VectorMeasure.SetIntegral
/-- For a function `f` and a measurable set `s`, the integral of `indicator s f`
over the whole space is equal to `∫ᵛ x in s, f x ∂[B; μ]`
defined as `∫ᵛ x, f x ∂[B; μ.restrict s]`.  -/
MeasureTheory.VectorMeasure.integral_indicator : ∀ {X : Type u_2} {E : Type u_3} {F : Type u_4} {G : Type u_5} {mX : MeasurableSpace X} [inst : NormedAddCommGroup E]
  [inst_1 : NormedAddCommGroup F] [inst_2 : NormedAddCommGroup G] {μ : MeasureTheory.VectorMeasure X F} {f : X → E}
  {s : Set X} [inst_3 : NormedSpace ℝ E] [inst_4 : NormedSpace ℝ F] [inst_5 : NormedSpace ℝ G] {B : E →L[ℝ] F →L[ℝ] G},
  MeasurableSet s → ∫ᵛ (x : X), s.indicator f x ∂[B; μ] = ∫ᵛ (x : X) in s, f x ∂[B; μ]
-- Std.Time.DateTime
Std.Time.DateTime.instHAddOffset_4 : HAdd Std.Time.DateTime Std.Time.Second.Offset Std.Time.DateTime
-- Mathlib.MeasureTheory.Group.Arithmetic
MeasurableInv.mk : ∀ {G : Type u_2} [inst : Inv G] [inst_1 : MeasurableSpace G], Measurable Inv.inv → MeasurableInv G
-- Mathlib.Algebra.Lie.Weights.Chain
LieModule.coe_chainBot : ∀ {R : Type u_1} {L : Type u_2} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] {M : Type u_3}
  [inst_3 : AddCommGroup M] [inst_4 : Module R M] [inst_5 : LieRingModule L M] [inst_6 : LieModule R L M]
  [inst_7 : LieRing.IsNilpotent L] [inst_8 : IsAddTorsionFree R] [inst_9 : IsDomain R]
  [inst_10 : Module.IsTorsionFree R M] [inst_11 : IsNoetherian R M] (α : L → R) (β : LieModule.Weight R L M),
  ⇑(LieModule.chainBot α β) = -↑(LieModule.chainBotCoeff α β) • α + ⇑β
-- Mathlib.RingTheory.AdicCompletion.Basic
Submodule.factor.eq_1 : ∀ {R : Type u_1} {M : Type u_2} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : Module R M] {p p' : Submodule R M}
  (H : p ≤ p'), Submodule.factor H = p.mapQ p' LinearMap.id H
-- Mathlib.CategoryTheory.Monoidal.Cartesian.Basic
/-- Naturality of the `prodComparison` morphism in the right argument.  -/
CategoryTheory.CartesianMonoidalCategory.prodComparison_natural_whiskerLeft : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {D : Type u₁} [inst_2 : CategoryTheory.Category.{v₁, u₁} D] [inst_3 : CategoryTheory.CartesianMonoidalCategory D]
  (F : CategoryTheory.Functor C D) {A B B' : C} (g : B ⟶ B'),
  CategoryTheory.CategoryStruct.comp (F.map (CategoryTheory.MonoidalCategoryStruct.whiskerLeft A g))
      (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B') =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.CartesianMonoidalCategory.prodComparison F A B)
      (CategoryTheory.MonoidalCategoryStruct.whiskerLeft (F.obj A) (F.map g))
-- Mathlib.Algebra.GroupWithZero.NonZeroDivisors
Associated.setoid.eq_1 : ∀ (M : Type u_2) [inst : Monoid M], Associated.setoid M = { r := Associated, iseqv := ⋯ }
-- Mathlib.LinearAlgebra.Matrix.Circulant
/-- If `circulant v` is symmetric, `∀ i j : I, v (- i) = v i`.  -/
Matrix.circulant_isSymm_apply : ∀ {α : Type u_1} {n : Type u_3} [inst : SubtractionMonoid n] {v : n → α},
  (Matrix.circulant v).IsSymm → ∀ (i : n), v (-i) = v i
-- Mathlib.Algebra.Algebra.Operations
/-- Dependent version of `Submodule.pow_induction_on_left`.  -/
Submodule.pow_induction_on_left' : ∀ {R : Type u} [inst : CommSemiring R] {A : Type v} [inst_1 : Semiring A] [inst_2 : Algebra R A] (M : Submodule R A)
  {C : (n : ℕ) → (x : A) → x ∈ M ^ n → Prop},
  (∀ (r : R), C 0 ((algebraMap R A) r) ⋯) →
    (∀ (x y : A) (i : ℕ) (hx : x ∈ M ^ i) (hy : y ∈ M ^ i), C i x hx → C i y hy → C i (x + y) ⋯) →
      (∀ (m : A) (hm : m ∈ M) (i : ℕ) (x : A) (hx : x ∈ M ^ i), C i x hx → C i.succ (m * x) ⋯) →
        ∀ {n : ℕ} {x : A} (hx : x ∈ M ^ n), C n x hx
-- Init.Data.Array.Lemmas
Array.getElem_of_mem : ∀ {α : Type u_1} {a : α} {xs : Array α}, a ∈ xs → ∃ i, ∃ (h : i < xs.size), xs[i] = a
-- Mathlib.NumberTheory.Real.GoldenRatio
/-- The inverse of the golden ratio is the opposite of its conjugate.  -/
Real.inv_goldenRatio : Real.goldenRatio⁻¹ = -Real.goldenConj
-- Mathlib.Geometry.Convex.Cone.Basic
convexHull_toCone_isLeast : ∀ {𝕜 : Type u_1} {M : Type u_4} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] [inst_2 : IsStrictOrderedRing 𝕜]
  [inst_3 : AddCommGroup M] [inst_4 : Module 𝕜 M] (s : Set M), IsLeast {t | s ⊆ ↑t} (Convex.toCone ((convexHull 𝕜) s) ⋯)