mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.Internal.List.Associative
Std.Internal.List.getEntry?_eq_none : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] {l : List ((a : α) × β a)} {a : α},
  Std.Internal.List.getEntry? a l = none ↔ Std.Internal.List.containsKey a l = false
-- Mathlib.Computability.RegularExpressions
RegularExpression.char_rmatch_iff : ∀ {α : Type u_1} [inst : DecidableEq α] (a : α) (x : List α), (RegularExpression.char a).rmatch x = true ↔ x = [a]
-- Mathlib.Analysis.AperiodicOrder.Delone.Basic
Delone.DeloneSet.mem_coe : ∀ {X : Type u_1} [inst : MetricSpace X] {D : Delone.DeloneSet X} {x : X}, x ∈ ↑D ↔ x ∈ D
-- Init.Data.FloatArray.Basic
_private.Init.Data.FloatArray.Basic.0.FloatArray.toList.loop : FloatArray → ℕ → List Float → List Float
-- Batteries.Data.List.Basic
/-- `IsChain R l` means that `R` holds between adjacent elements of `l`. Example:
```
IsChain R [a, b, c, d] ↔ R a b ∧ R b c ∧ R c d
```
 -/
List.IsChain : {α : Type u_1} → (α → α → Prop) → List α → Prop
-- Lean.Meta.Tactic.Util
Lean.Meta.TacticResultCNM.modified.sizeOf_spec : ∀ (mvarId : Lean.MVarId), sizeOf (Lean.Meta.TacticResultCNM.modified mvarId) = 1 + sizeOf mvarId
-- Mathlib.CategoryTheory.Comma.Over.Pullback
/-- pullback (𝟙 X) : Over X ⥤ Over X is the identity functor.  -/
CategoryTheory.Over.pullbackId : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {X : C} →
      CategoryTheory.Over.pullback (CategoryTheory.CategoryStruct.id X) ≅
        CategoryTheory.Functor.id (CategoryTheory.Over X)
-- Mathlib.Algebra.Category.ModuleCat.Limits
/-- The forgetful functor from R-modules to abelian groups preserves all limits.  -/
ModuleCat.forget₂AddCommGroup_preservesLimit : ∀ {R : Type u} [inst : Ring R] {J : Type v} [inst_1 : CategoryTheory.Category.{t, v} J]
  (F : CategoryTheory.Functor J (ModuleCat R))
  [Small.{w, max v w} ↑(F.comp (CategoryTheory.forget (ModuleCat R))).sections],
  CategoryTheory.Limits.PreservesLimit F (CategoryTheory.forget₂ (ModuleCat R) AddCommGrpCat)
-- Mathlib.Algebra.BigOperators.Intervals
/-- Telescopic sum over `Fin`.  -/
Fin.sum_Icc_sub : ∀ {M : Type u_3} [inst : AddCommGroup M] {n : ℕ} {a b : Fin n},
  a ≤ b → ∀ (f : Fin (n + 1) → M), ∑ i ∈ Finset.Icc a b, (f i.succ - f i.castSucc) = f b.succ - f a.castSucc
-- Std.Data.HashMap.RawLemmas
Std.HashMap.Raw.not_mem_diff_of_mem_right : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {m₁ m₂ : Std.HashMap.Raw α β} [EquivBEq α]
  [LawfulHashable α], m₁.WF → m₂.WF → ∀ {k : α}, k ∈ m₂ → k ∉ m₁ \ m₂
-- Mathlib.AlgebraicGeometry.Morphisms.LocalClosure
AlgebraicGeometry.sourceLocalClosure.instIsMultiplicativeSchemeOfIsStableUnderBaseChange : ∀ {W P : CategoryTheory.MorphismProperty AlgebraicGeometry.Scheme} [W.IsStableUnderBaseChange]
  [AlgebraicGeometry.Scheme.IsJointlySurjectivePreserving W] [W.IsMultiplicative] [P.IsStableUnderBaseChange]
  [P.IsMultiplicative], (AlgebraicGeometry.sourceLocalClosure W P).IsMultiplicative
-- Mathlib.Algebra.EuclideanDomain.Defs
EuclideanDomain.gcd.eq_def : ∀ {R : Type u} [inst : EuclideanDomain R] [inst_1 : DecidableEq R] (a b : R),
  EuclideanDomain.gcd a b =
    if a0 : a = 0 then b
    else
      have x := ⋯;
      EuclideanDomain.gcd (b % a) a
-- Mathlib.Algebra.MonoidAlgebra.Defs
MonoidAlgebra.coeff_single : ∀ {R : Type u_1} {M : Type u_4} [inst : Semiring R] (m : M) (r : R), (MonoidAlgebra.single m r).coeff = fun₀ | m => r
-- Mathlib.Order.Hom.Basic
Equiv.coe_toOrderIso : ∀ {α : Type u_2} {β : Type u_3} [inst : Preorder α] [inst_1 : Preorder β] (e : α ≃ β) (h₁ : Monotone ⇑e)
  (h₂ : Monotone ⇑e.symm), ⇑(e.toOrderIso h₁ h₂) = ⇑e
-- Mathlib.AlgebraicTopology.SimplicialSet.NonDegenerateSimplicesSubcomplex
/-- When `A` is a subcomplex of a simplicial set `X`,
and `s : A.N` is such that `s.dim = d`, this is a term
that is equal to `s`, but whose dimension if definitionally equal to `d`.  -/
SSet.Subcomplex.N.cast : {X : SSet} → {A : X.Subcomplex} → (s : A.N) → {d : ℕ} → s.dim = d → A.N
-- Mathlib.Algebra.Order.Group.Unbundled.Basic
StrictMono.inv : ∀ {α : Type u} {β : Type u_1} [inst : Group α] [inst_1 : Preorder α] [MulLeftStrictMono α] [MulRightStrictMono α]
  [inst_4 : Preorder β] {f : β → α}, StrictMono f → StrictAnti fun x => (f x)⁻¹
-- Mathlib.AlgebraicGeometry.Cover.MorphismProperty
/-- **Alias** of `CategoryTheory.PreZeroHypercover.id_h₀`. -/
AlgebraicGeometry.Scheme.Cover.id_app : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {S : C} (E : CategoryTheory.PreZeroHypercover S) (x : E.I₀),
  (CategoryTheory.CategoryStruct.id E).h₀ x = CategoryTheory.CategoryStruct.id (E.X x)
-- Mathlib.RingTheory.Ideal.Maps
/-- The pushforward `Ideal.map` as a (semi)ring homomorphism.  -/
Ideal.mapHom : {R : Type u} →
  {S : Type v} →
    {F : Type u_1} →
      [inst : CommSemiring R] →
        [inst_1 : CommSemiring S] → [inst_2 : FunLike F R S] → [rc : RingHomClass F R S] → F → Ideal R →+* Ideal S
-- Lean.Elab.MutualInductive
Lean.Elab.Command.elabInductives : Array (Lean.Elab.Modifiers × Lean.Syntax) → Lean.Elab.Command.CommandElabM Unit
-- Batteries.Recycling.RBTree.Lemmas
RBTree.RBNode.zoom.eq_1 : ∀ {α : Type u_1} (cut : α → Ordering) (x : RBTree.RBNode.Path α),
  RBTree.RBNode.zoom cut RBTree.RBNode.nil x = (RBTree.RBNode.nil, x)
-- Mathlib.Data.Set.FiniteExhaustion
Set.nonempty_finiteExhaustion_iff : ∀ {α : Type u_1} {s : Set α}, Nonempty s.FiniteExhaustion ↔ s.Countable
-- Mathlib.Algebra.Algebra.Unitization
Unitization.instCanLift : ∀ {R : Type u_3} {A : Type u_4} [inst : Zero R], CanLift (Unitization R A) A Unitization.inr fun x => x.toProd.1 = 0
-- Mathlib.CategoryTheory.Sites.Pretopology
CategoryTheory.Pretopology.congr_simp : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Limits.HasPullbacks C],
  CategoryTheory.Pretopology C = CategoryTheory.Pretopology C
-- Mathlib.Probability.Martingale.Centering
MeasureTheory.martingalePart_zero : ∀ {Ω : Type u_1} {E : Type u_2} {m0 : MeasurableSpace Ω} {μ : MeasureTheory.Measure Ω} [inst : NormedAddCommGroup E]
  [inst_1 : NormedSpace ℝ E] {f : ℕ → Ω → E} {ℱ : MeasureTheory.Filtration ℕ m0},
  MeasureTheory.martingalePart f ℱ μ 0 = f 0
-- Mathlib.Data.Set.Image
Set.mem_image_iff_of_inverse : ∀ {α : Type u_1} {β : Type u_2} {f : α → β} {g : β → α} {b : β} {s : Set α},
  Function.LeftInverse g f → Function.RightInverse g f → (b ∈ f '' s ↔ g b ∈ s)
-- Mathlib.Data.Nat.Totient
/-- Extension for `Nat.totient`.  -/
Mathlib.Meta.Positivity.evalNatTotient : Mathlib.Meta.Positivity.PositivityExt
-- Init.Omega.IntList
Lean.Omega.IntList.bmod_length : ∀ (x : Lean.Omega.IntList) (m : ℕ), List.length (x.bmod m) ≤ List.length x
-- Mathlib.Algebra.Homology.SpectralSequence.Basic
CategoryTheory.SpectralSequence.Hom.comm : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{u_3, u_1} C] [inst_1 : CategoryTheory.Abelian C] {κ : Type u_2}
  {c : ℤ → ComplexShape κ} {r₀ : ℤ} {E E' : CategoryTheory.SpectralSequence C c r₀} (self : E.Hom E') (r r' : ℤ)
  (pq : κ) (hrr' : autoParam (r + 1 = r') CategoryTheory.SpectralSequence.Hom._auto_5)
  (hr : autoParam (r₀ ≤ r) CategoryTheory.SpectralSequence.Hom._auto_7),
  CategoryTheory.CategoryStruct.comp (HomologicalComplex.homologyMap (self.hom r ⋯) pq) (E'.iso r r' pq ⋯ ⋯).hom =
    CategoryTheory.CategoryStruct.comp (E.iso r r' pq ⋯ ⋯).hom ((self.hom r' ⋯).f pq)
-- Mathlib.Computability.Primrec.Basic
Primrec.or : Primrec₂ or
-- Mathlib.CategoryTheory.Monoidal.Mon
CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj.eq_1 : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.MonoidalCategory C]
  (A : CategoryTheory.Mon C),
  CategoryTheory.Mon.EquivLaxMonoidalFunctorPUnit.instLaxMonoidalDiscretePUnitMonToLaxMonoidalObj A =
    { ε := CategoryTheory.MonObj.one, μ := fun x x_1 => CategoryTheory.MonObj.mul, μ_natural_left := ⋯,
      μ_natural_right := ⋯, associativity := ⋯, left_unitality := ⋯, right_unitality := ⋯ }
-- Mathlib.Control.LawfulFix
Pi.lawfulFix' : {α : Type u_1} →
  {β : α → Type u_2} →
    {γ : (a : α) → β a → Type u_3} →
      [inst : (x : α) → (y : β x) → OmegaCompletePartialOrder (γ x y)] →
        [LawfulFix ((x : Sigma β) → γ x.fst x.snd)] → LawfulFix ((x : α) → (y : β x) → γ x y)
-- Mathlib.Data.Nat.ModEq
/-- Cancel right multiplication in the modulus.

For cancelling right multiplication on both sides of the `≡`, see `nat.modeq.mul_right_cancel'`.  -/
Nat.ModEq.of_mul_right : ∀ {n a b : ℕ} (m : ℕ), a ≡ b [MOD n * m] → a ≡ b [MOD n]
-- Mathlib.Topology.UniformSpace.Basic
IsOpen.relInv : ∀ {α : Type ua} {β : Type ub} [inst : TopologicalSpace α] [inst_1 : TopologicalSpace β] {s : SetRel α β},
  IsOpen s → IsOpen s.inv
-- Mathlib.CategoryTheory.Category.Pairwise
CategoryTheory.instDecidableEqPairwise.decEq : {ι : Type u_1} → [DecidableEq ι] → (x x_1 : CategoryTheory.Pairwise ι) → Decidable (x = x_1)
-- Mathlib.AlgebraicTopology.SimplicialSet.HomotopyCat
/-- For a simplicial set `X`, the underlying type of `hoFunctor.obj X` is equivalent to `X _⦋0⦌`.  -/
SSet.hoFunctor.obj.equiv : (X : SSet) → ↑(SSet.hoFunctor.obj X) ≃ X.obj (Opposite.op { len := 0 })
-- Std.Data.DHashMap.Raw
/-- Computes the difference of the given hash maps.

This function always iterates through the smaller map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.DHashMap.Raw.diff : {α : Type u} →
  {β : α → Type v} → [BEq α] → [Hashable α] → Std.DHashMap.Raw α β → Std.DHashMap.Raw α β → Std.DHashMap.Raw α β
-- Mathlib.Lean.Meta.CongrTheorems
Lean.Meta.instFastIsEmptyFalse : Lean.Meta.FastIsEmpty False
-- Mathlib.Algebra.Order.BigOperators.Group.List
List.all_zero_of_le_zero_le_of_sum_eq_zero : ∀ {M : Type u_3} [inst : AddCommMonoid M] [inst_1 : PartialOrder M] [IsOrderedAddMonoid M] {l : List M},
  (∀ x ∈ l, 0 ≤ x) → l.sum = 0 → ∀ {x : M}, x ∈ l → x = 0
-- Mathlib.CategoryTheory.Limits.Constructions.LimitsOfProductsAndEqualizers
/-- If G preserves coequalizers and finite coproducts, it preserves finite colimits.  -/
CategoryTheory.Limits.preservesFiniteColimits_of_preservesCoequalizers_and_finiteCoproducts : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  [CategoryTheory.Limits.HasCoequalizers C] [CategoryTheory.Limits.HasFiniteCoproducts C]
  (G : CategoryTheory.Functor C D)
  [CategoryTheory.Limits.PreservesColimitsOfShape CategoryTheory.Limits.WalkingParallelPair G]
  [CategoryTheory.Limits.PreservesFiniteCoproducts G], CategoryTheory.Limits.PreservesFiniteColimits G
-- Mathlib.RingTheory.AdicCompletion.AsTensorProduct
/-- The natural `AdicCompletion I R`-linear map from `AdicCompletion I R ⊗[R] M` to
the adic completion of `M`.  -/
AdicCompletion.ofTensorProduct : {R : Type u_1} →
  [inst : CommRing R] →
    (I : Ideal R) →
      (M : Type u_2) →
        [inst_1 : AddCommGroup M] →
          [inst_2 : Module R M] → TensorProduct R (AdicCompletion I R) M →ₗ[AdicCompletion I R] AdicCompletion I M
-- Mathlib.Order.UpperLower.CompleteLattice
UpperSet.instLinearOrder : {α : Type u_1} → [inst : LinearOrder α] → LinearOrder (UpperSet α)
-- Mathlib.RingTheory.PowerSeries.WeierstrassPreparation
PowerSeries.IsWeierstrassDivisionAt.coeff_f_sub_r_mem : ∀ {A : Type u_1} [inst : CommRing A] {f g q : PowerSeries A} {r : Polynomial A} {I : Ideal A},
  f.IsWeierstrassDivisionAt g q r I →
    ∀ {i : ℕ}, i < ((PowerSeries.map (Ideal.Quotient.mk I)) g).order.toNat → (PowerSeries.coeff i) (f - ↑r) ∈ I
-- Init.Data.Array.Lemmas
Array.set!_eq_setIfInBounds : ∀ {α : Type u_1} {xs : Array α} {i : ℕ} {v : α}, xs.set! i v = xs.setIfInBounds i v
-- Mathlib.Algebra.Category.Ring.Colimits
CommRingCat.Colimits.Relation.add_1 : ∀ {J : Type v} [inst : CategoryTheory.SmallCategory J] {F : CategoryTheory.Functor J CommRingCat}
  (x x' y : CommRingCat.Colimits.Prequotient F),
  CommRingCat.Colimits.Relation F x x' → CommRingCat.Colimits.Relation F (x.add y) (x'.add y)
-- Init.Grind.Ring.CommSemiringAdapter
Lean.Grind.CommRing.Poly.NonnegCoeffs.add : ∀ (a : ℤ) (m : Lean.Grind.CommRing.Mon) (p : Lean.Grind.CommRing.Poly),
  a ≥ 0 → p.NonnegCoeffs → (Lean.Grind.CommRing.Poly.add a m p).NonnegCoeffs
-- Mathlib.Order.Sublattice
Sublattice.coe_top : ∀ {α : Type u_2} [inst : Lattice α], ↑⊤ = Set.univ
-- Mathlib.CategoryTheory.Whiskering
CategoryTheory.Functor.whiskeringRight_obj_id : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {E : Type u₃} [inst_1 : CategoryTheory.Category.{v₃, u₃} E],
  (CategoryTheory.Functor.whiskeringRight E C C).obj (CategoryTheory.Functor.id C) =
    CategoryTheory.Functor.id (CategoryTheory.Functor E C)
-- Mathlib.Data.Nat.Cast.SetInterval
Nat.image_cast_int_Iic : ∀ (a : ℕ), Nat.cast '' Set.Iic a = Set.Icc 0 ↑a
-- Mathlib.Probability.Distributions.Fernique
ProbabilityTheory.Fernique.normThreshold_eq : ∀ {a : ℝ} (n : ℕ), ProbabilityTheory.Fernique.normThreshold a n = a * (1 + √2) * (√2 ^ (n + 1) - 1)
-- Mathlib.Topology.MetricSpace.Snowflaking
Metric.Snowflaking.instMetricSpace : {X : Type u_1} →
  {α : ℝ} → {hα₀ : 0 < α} → {hα₁ : α ≤ 1} → [MetricSpace X] → MetricSpace (Metric.Snowflaking X α hα₀ hα₁)
-- Mathlib.Order.Disjoint
Disjoint.left_le_of_le_sup_right : ∀ {α : Type u_1} [inst : DistribLattice α] [inst_1 : OrderBot α] {a b c : α}, a ≤ b ⊔ c → Disjoint a c → a ≤ b
-- Mathlib.GroupTheory.OreLocalization.Cardinality
OreLocalization.cardinalMk_le_lift_cardinalMk_of_commute : ∀ {R : Type u} [inst : Monoid R] (S : Submonoid R) [inst_1 : OreLocalization.OreSet S] (X : Type v)
  [inst_2 : MulAction R X],
  (∀ (s s' : ↥S), Commute s s') → Cardinal.mk (OreLocalization S X) ≤ Cardinal.lift.{u, v} (Cardinal.mk X)
-- Mathlib.Combinatorics.HalesJewett
/-- The type of collections of lines such that
- each line is only one color except possibly at its endpoint
- the lines all have the same endpoint
- the colors of the lines are distinct.

Used in the proof `exists_mono_in_high_dimension`.  -/
Combinatorics.Line.ColorFocused : {α : Type u_5} → {ι : Type u_6} → {κ : Type u_7} → ((ι → Option α) → κ) → Type (max (max u_5 u_6) u_7)
-- Mathlib.Data.QPF.Univariate.Basic
QPF.abs_repr : ∀ {F : Type u → Type v} [self : QPF F] {α : Type u} (x : F α), QPF.abs (QPF.repr x) = x
-- Mathlib.Probability.ProbabilityMassFunction.Constructions
PMF.mem_support_seq_iff : ∀ {α : Type u_1} {β : Type u_2} (q : PMF (α → β)) (p : PMF α) (b : β),
  b ∈ (q.seq p).support ↔ ∃ f ∈ q.support, b ∈ f '' p.support
-- Lean.Server.InfoUtils
Lean.Elab.InfoWithCtx.children : Lean.Elab.InfoWithCtx → Lean.PersistentArray Lean.Elab.InfoTree
-- Mathlib.ModelTheory.Syntax
/-- Take the disjunction of finitely many formulas.

Note that this is an arbitrary formula defined using the axiom of choice. It is only well-defined up
to equivalence of formulas.  -/
FirstOrder.Language.Formula.iSup : {L : FirstOrder.Language} → {α : Type u'} → {β : Type v'} → [Finite α] → (α → L.Formula β) → L.Formula β
-- Mathlib.Topology.Order.Lattice
Continuous.finset_inf_apply : ∀ {L : Type u_1} {X : Type u_2} [inst : TopologicalSpace L] [inst_1 : TopologicalSpace X] {ι : Type u_3}
  [inst_2 : SemilatticeInf L] [inst_3 : OrderTop L] [ContinuousInf L] {s : Finset ι} {f : ι → X → L},
  (∀ i ∈ s, Continuous (f i)) → Continuous fun a => s.inf fun x => f x a
-- Mathlib.Data.ENat.Basic
AddHom.ENatMap_apply : ∀ {N : Type u_2} [inst : Add N] (f : ℕ →ₙ+ N), ⇑f.ENatMap = ENat.map ⇑f
-- Mathlib.Computability.Partrec
Computable.list_concat : ∀ {α : Type u_1} [inst : Primcodable α], Computable₂ fun l a => l ++ [a]
-- Init.Data.List.Impl
List.zipIdx_eq_zipIdxTR : @List.zipIdx = @List.zipIdxTR
-- Mathlib.Analysis.Convex.SpecificFunctions.Basic
strictConcaveOn_log_Iio : StrictConcaveOn ℝ (Set.Iio 0) Real.log
-- Init.Data.SInt.Basic
/-- Converts an 32-bit signed integer into the 32-bit unsigned integer that is its two's complement
encoding.
 -/
Int32.toUInt32 : Int32 → UInt32
-- Mathlib.RingTheory.HahnSeries.Summable
HahnSeries.SummableFamily.embDomain_apply : ∀ {Γ : Type u_1} {R : Type u_3} {α : Type u_5} {β : Type u_6} [inst : PartialOrder Γ] [inst_1 : AddCommMonoid R]
  (s : HahnSeries.SummableFamily Γ R α) (f : α ↪ β) {b : β},
  (s.embDomain f) b = if h : b ∈ Set.range ⇑f then s (Classical.choose h) else 0
-- Mathlib.RingTheory.Ideal.Quotient.Defs
Ideal.Quotient.instCoeQuotient : {R : Type u} → [inst : Ring R] → {I : Ideal R} → [I.IsTwoSided] → Coe R (R ⧸ I)
-- Mathlib.Analysis.SpecialFunctions.Pow.Integral
/-- An application of the layer cake formula / Cavalieri's principle / tail probability formula:

For a nonnegative function `f` on a measure space, the Lebesgue integral of `f` can
be written (roughly speaking) as: `∫⁻ f^p ∂μ = p * ∫⁻ t in 0..∞, t^(p-1) * μ {ω | f(ω) ≥ t}`.

See `MeasureTheory.lintegral_rpow_eq_lintegral_meas_lt_mul` for a version with sets of the form
`{ω | f(ω) > t}` instead.  -/
MeasureTheory.lintegral_rpow_eq_lintegral_meas_le_mul : ∀ {α : Type u_1} [inst : MeasurableSpace α] (μ : MeasureTheory.Measure α) {f : α → ℝ},
  0 ≤ᵐ[μ] f →
    AEMeasurable f μ →
      ∀ {p : ℝ},
        0 < p →
          ∫⁻ (ω : α), ENNReal.ofReal (f ω ^ p) ∂μ =
            ENNReal.ofReal p * ∫⁻ (t : ℝ) in Set.Ioi 0, μ {a | t ≤ f a} * ENNReal.ofReal (t ^ (p - 1))
-- Mathlib.LinearAlgebra.SymmetricAlgebra.Basic
/-- For any linear map `f : M →ₗ[R] A`, `SymmetricAlgebra.lift f` lifts the linear map to an
R-algebra homomorphism from `SymmetricAlgebra R M` to `A`.  -/
SymmetricAlgebra.lift : {R : Type u_1} →
  {M : Type u_2} →
    [inst : CommSemiring R] →
      [inst_1 : AddCommMonoid M] →
        [inst_2 : Module R M] →
          {A : Type u_3} →
            [inst_3 : CommSemiring A] → [inst_4 : Algebra R A] → (M →ₗ[R] A) ≃ (SymmetricAlgebra R M →ₐ[R] A)
-- Mathlib.GroupTheory.GroupAction.Blocks
/-- An orbit is a fixed block.  -/
MulAction.IsFixedBlock.orbit : ∀ {G : Type u_1} [inst : Group G] {X : Type u_2} [inst_1 : MulAction G X] (a : X),
  MulAction.IsFixedBlock G (MulAction.orbit G a)
-- Mathlib.Combinatorics.SimpleGraph.Sum
SimpleGraph.Colorable.sum_max : ∀ {V : Type u_3} {W : Type u_5} {G : SimpleGraph V} {H : SimpleGraph W} {n m : ℕ},
  G.Colorable n → H.Colorable m → (G ⊕g H).Colorable (max n m)
-- Mathlib.Analysis.Normed.Unbundled.SpectralNorm
/-- If `K` is a field complete with respect to a nontrivial nonarchimedean multiplicative norm and
`L/K` is an algebraic normed field extension, then the norm on `L` coincides with the spectral
norm.  -/
NormedAlgebra.norm_eq_spectralNorm : ∀ (K : Type u) [inst : NontriviallyNormedField K] [hu : IsUltrametricDist K] {L : Type u_2} [inst_1 : NormedField L]
  [inst_2 : NormedAlgebra K L] [Algebra.IsAlgebraic K L] [CompleteSpace K] (x : L), ‖x‖ = spectralNorm K L x
-- Mathlib.Topology.Algebra.Algebra
Subalgebra.topologicalClosure_map_le : ∀ {R : Type u_1} [inst : CommSemiring R] {A : Type u_2} [inst_1 : Semiring A] [inst_2 : TopologicalSpace A]
  {B : Type u_3} [inst_3 : Semiring B] [inst_4 : TopologicalSpace B] [inst_5 : Algebra R A] [inst_6 : Algebra R B]
  [inst_7 : IsSemitopologicalSemiring A] [inst_8 : IsSemitopologicalSemiring B] (f : A →ₐ[R] B),
  IsClosedMap ⇑f →
    ∀ (s : Subalgebra R A), (Subalgebra.map f s).topologicalClosure ≤ Subalgebra.map f s.topologicalClosure
-- Mathlib.Data.Finset.Update
Function.updateFinset_def : ∀ {ι : Type u_1} {π : ι → Sort u_2} {x : (i : ι) → π i} [inst : DecidableEq ι] {s : Finset ι} {y : (i : ↥s) → π ↑i},
  Function.updateFinset x s y = fun i => if hi : i ∈ s then y ⟨i, hi⟩ else x i
-- Mathlib.CategoryTheory.Subterminal
/-- If `A` is subterminal, the unique morphism from it to a terminal object is a monomorphism.
The converse of `isSubterminal_of_mono_isTerminal_from`.
 -/
CategoryTheory.IsSubterminal.mono_isTerminal_from : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {A : C},
  CategoryTheory.IsSubterminal A → ∀ {T : C} (hT : CategoryTheory.Limits.IsTerminal T), CategoryTheory.Mono (hT.from A)
-- Mathlib.Algebra.Category.ModuleCat.Images
ModuleCat.imageIsoRange_inv_image_ι_apply : ∀ {R : Type u} [inst : Ring R] {G H : ModuleCat R} (f : G ⟶ H) (x : ↥(ModuleCat.Hom.hom f).range),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.Limits.image.ι f))
      ((CategoryTheory.ConcreteCategory.hom (ModuleCat.imageIsoRange f).inv) x) =
    ↑x
-- Mathlib.RingTheory.WittVector.Defs
WittVector.wittAdd.congr_simp : ∀ (p p_1 : ℕ) (e_p : p = p_1) [hp : Fact (Nat.Prime p)] (a a_1 : ℕ),
  a = a_1 → WittVector.wittAdd p a = WittVector.wittAdd p_1 a_1
-- Mathlib.Combinatorics.SimpleGraph.Triangle.Basic
/-- **Alias** of the forward direction of `SimpleGraph.farFromTriangleFree_iff`. -/
SimpleGraph.farFromTriangleFree.le_card_sub_card : ∀ {α : Type u_1} {𝕜 : Type u_3} [inst : Field 𝕜] [inst_1 : LinearOrder 𝕜] {G : SimpleGraph α} {ε : 𝕜}
  [inst_2 : Fintype α] [inst_3 : DecidableRel G.Adj],
  G.FarFromTriangleFree ε →
    ∀ ⦃H : SimpleGraph α⦄ [inst_4 : DecidableRel H.Adj],
      H ≤ G → H.CliqueFree 3 → ε * ↑(Fintype.card α ^ 2) ≤ ↑G.edgeFinset.card - ↑H.edgeFinset.card
-- Std.Data.HashSet.Lemmas
Std.HashSet.contains_inter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m₁ m₂ : Std.HashSet α} [EquivBEq α] [LawfulHashable α] {k : α},
  (m₁ ∩ m₂).contains k = (m₁.contains k && m₂.contains k)
-- Mathlib.Analysis.Complex.Norm
Complex.re_neg_ne_zero_of_one_lt_re : ∀ {s : ℂ}, 1 < s.re → (-s).re ≠ 0
-- Mathlib.Combinatorics.SimpleGraph.Regularity.Bound
SzemerediRegularity.seven_le_initialBound : ∀ (ε : ℝ) (l : ℕ), 7 ≤ SzemerediRegularity.initialBound ε l
-- Mathlib.RingTheory.Nilpotent.Defs
isNilpotent_of_pos_nilpotencyClass : ∀ {R : Type u_1} {x : R} [inst : Zero R] [inst_1 : Pow R ℕ], 0 < nilpotencyClass x → IsNilpotent x
-- Init.Data.Fin.Lemmas
_private.Init.Data.Fin.Lemmas.0.Fin.reverseInduction.go.match_1.splitter : {n : ℕ} →
  {motive : Fin (n + 1) → Sort u_2} →
    (i : Fin (n + 1)) →
      (motive_1 : (j : ℕ) → (h : j < n + 1) → ↑i ≤ j → motive ⟨j, h⟩ → ¬↑i = j → Sort u_1) →
        (j : ℕ) →
          (h : j < n + 1) →
            (h2 : ↑i ≤ j) →
              (x : motive ⟨j, h⟩) →
                (hi : ¬↑i = j) →
                  ((h : 0 < n + 1) → (h2 : ↑i ≤ 0) → (x : motive ⟨0, h⟩) → (hi : ¬↑i = 0) → motive_1 0 h h2 x hi) →
                    ((j : ℕ) →
                        (h : j + 1 < n + 1) →
                          (h2 : ↑i ≤ j + 1) →
                            (x : motive ⟨j + 1, h⟩) → (hi : ¬↑i = j + 1) → motive_1 j.succ h h2 x hi) →
                      motive_1 j h h2 x hi
-- Mathlib.MeasureTheory.MeasurableSpace.Constructions
MeasurableEq.measurableSet_diagonal : ∀ {α : Type u_1} {inst : MeasurableSpace α} [self : MeasurableEq α], MeasurableSet (Set.diagonal α)
-- Mathlib.CategoryTheory.Sites.Hypercover.Homotopy
CategoryTheory.PreOneHypercover.Homotopy.map_eq_map : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] (J : CategoryTheory.GrothendieckTopology C) {S : C}
  {E F : J.OneHypercover S} {f g : E ⟶ F} (H : CategoryTheory.PreOneHypercover.Homotopy f g),
  (CategoryTheory.GrothendieckTopology.OneHypercover.toHOneHypercover J S).map f =
    (CategoryTheory.GrothendieckTopology.OneHypercover.toHOneHypercover J S).map g
-- Std.Data.DHashMap.RawLemmas
Std.DHashMap.Raw.Const.get!_map_of_getKey?_eq_some : ∀ {α : Type u} [inst : BEq α] [inst_1 : Hashable α] {β : Type v} {γ : Type w} {m : Std.DHashMap.Raw α fun x => β}
  [EquivBEq α] [LawfulHashable α] [inst_4 : Inhabited γ] {f : α → β → γ} {k k' : α},
  m.WF →
    m.getKey? k = some k' →
      Std.DHashMap.Raw.Const.get! (Std.DHashMap.Raw.map f m) k =
        (Option.map (f k') (Std.DHashMap.Raw.Const.get? m k)).get!
-- Mathlib.Computability.Primrec.Basic
/-- A `Primcodable` type is, essentially, an `Encodable` type for which
the encode/decode functions are primitive recursive.
However, such a definition is circular.

Instead, we ask that the composition of `decode : ℕ → Option α` with
`encode : Option α → ℕ` is primitive recursive. Said composition is
the identity function, restricted to the image of `encode`.
Thus, in a way, the added requirement ensures that no predicates
can be smuggled in through a cunning choice of the subset of `ℕ` into
which the type is encoded.  -/
Primcodable : Type u_1 → Type u_1
-- Mathlib.Data.Ordmap.Ordset
/-- O(1). The empty set.  -/
Ordset.nil : {α : Type u_1} → [inst : Preorder α] → Ordset α
-- Mathlib.Algebra.MvPolynomial.Basic
MvPolynomial.support_sdiff_support_subset_support_add : ∀ {R : Type u} {σ : Type u_1} [inst : CommSemiring R] [inst_1 : DecidableEq σ] (p q : MvPolynomial σ R),
  p.support \ q.support ⊆ (p + q).support