mathlib-initiative/mathlib-types huggingface dataset:
-- Std.Data.TreeSet.Raw.Lemmas
Std.TreeSet.Raw.max!_le : ∀ {α : Type u} {cmp : α → α → Ordering} {t : Std.TreeSet.Raw α cmp} [Std.TransCmp cmp] [inst : Inhabited α],
  t.WF → t.isEmpty = false → ∀ {k : α}, (cmp t.max! k).isLE = true ↔ ∀ k' ∈ t, (cmp k' k).isLE = true
-- Init.Data.Option.Attach
Option.map_attach_eq_attachWith : ∀ {α : Type u_1} {o : Option α} {p : α → Prop} (f : ∀ (a : α), o = some a → p a),
  Option.map (fun x => ⟨↑x, ⋯⟩) o.attach = o.attachWith p f
-- Mathlib.Data.Multiset.MapFold
Multiset.map_const : ∀ {α : Type u_1} {β : Type v} (s : Multiset α) (b : β),
  Multiset.map (Function.const α b) s = Multiset.replicate s.card b
-- Std.Data.ExtHashMap.Lemmas
Std.ExtHashMap.contains_modify : ∀ {α : Type u} {β : Type v} {x : BEq α} {x_1 : Hashable α} {m : Std.ExtHashMap α β} [inst : EquivBEq α]
  [inst_1 : LawfulHashable α] {k k' : α} {f : β → β}, (m.modify k f).contains k' = m.contains k'
-- Mathlib.Analysis.BoxIntegral.Partition.Split
BoxIntegral.Box.splitUpper_eq_self : ∀ {ι : Type u_1} {I : BoxIntegral.Box ι} {i : ι} {x : ℝ}, I.splitUpper i x = ↑I ↔ x ≤ I.lower i
-- Std.Data.DTreeMap.Raw.Lemmas
Std.DTreeMap.Raw.ofList.eq_1 : ∀ {α : Type u} {β : α → Type v} (l : List ((a : α) × β a)) (cmp : α → α → Ordering),
  Std.DTreeMap.Raw.ofList l cmp = { inner := Std.DTreeMap.Internal.Impl.ofList l }
-- Mathlib.Analysis.Fourier.BoundedContinuousFunctionChar
/-- If `e` and `L` are non-trivial, then `char he hL w, w : W` separates points in `V`.  -/
BoundedContinuousFunction.ext_of_char_eq : ∀ {V : Type u_1} {W : Type u_2} [inst : AddCommGroup V] [inst_1 : Module ℝ V] [inst_2 : TopologicalSpace V]
  [inst_3 : AddCommGroup W] [inst_4 : Module ℝ W] [inst_5 : TopologicalSpace W] {e : AddChar ℝ Circle}
  {L : V →ₗ[ℝ] W →ₗ[ℝ] ℝ} (he : Continuous ⇑e),
  e ≠ 1 →
    ∀ (hL : Continuous fun p => (L p.1) p.2),
      (∀ (v : V), v ≠ 0 → L v ≠ 0) →
        ∀ {v v' : V},
          (∀ (w : W), (BoundedContinuousFunction.char he hL w) v = (BoundedContinuousFunction.char he hL w) v') → v = v'
-- Mathlib.Algebra.Module.Rat
SMulCommClass.rat : ∀ {α : Type u} {M : Type v} [inst : AddCommGroup M] [inst_1 : DistribSMul α M] [inst_2 : Module ℚ M],
  SMulCommClass ℚ α M
-- Mathlib.Probability.Kernel.Composition.IntegralCompProd
ProbabilityTheory.Kernel.integral_integral_sub'_comp : ∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {E : Type u_4} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {mγ : MeasurableSpace γ} [inst : NormedAddCommGroup E] {a : α} {κ : ProbabilityTheory.Kernel α β}
  {η : ProbabilityTheory.Kernel β γ} [inst_1 : NormedSpace ℝ E] ⦃f g : γ → E⦄,
  MeasureTheory.Integrable f ((η.comp κ) a) →
    MeasureTheory.Integrable g ((η.comp κ) a) →
      ∫ (x : β), ∫ (y : γ), (f - g) y ∂η x ∂κ a =
        ∫ (x : β), ∫ (y : γ), f y ∂η x ∂κ a - ∫ (x : β), ∫ (y : γ), g y ∂η x ∂κ a
-- Mathlib.Analysis.SpecialFunctions.Sqrt
fderivWithin_sqrt : ∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : E → ℝ} {s : Set E} {x : E},
  DifferentiableWithinAt ℝ f s x →
    f x ≠ 0 →
      UniqueDiffWithinAt ℝ s x → fderivWithin ℝ (fun x => √(f x)) s x = (1 / (2 * √(f x))) • fderivWithin ℝ f s x
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Assoc
CategoryTheory.Limits.pullbackAssoc_inv_fst_fst_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X₁ X₂ X₃ Y₁ Y₂ : C} (f₁ : X₁ ⟶ Y₁) (f₂ : X₂ ⟶ Y₁)
  (f₃ : X₂ ⟶ Y₂) (f₄ : X₃ ⟶ Y₂) [inst_1 : CategoryTheory.Limits.HasPullback f₁ f₂]
  [inst_2 : CategoryTheory.Limits.HasPullback f₃ f₄]
  [inst_3 :
    CategoryTheory.Limits.HasPullback (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃)
      f₄]
  [inst_4 :
    CategoryTheory.Limits.HasPullback f₁
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂)]
  {Z : C} (h : X₁ ⟶ Z),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullbackAssoc f₁ f₂ f₃ f₄).inv
      (CategoryTheory.CategoryStruct.comp
        (CategoryTheory.Limits.pullback.fst
          (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.snd f₁ f₂) f₃) f₄)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₁ f₂) h)) =
    CategoryTheory.CategoryStruct.comp
      (CategoryTheory.Limits.pullback.fst f₁
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.pullback.fst f₃ f₄) f₂))
      h
-- Mathlib.Data.Matrix.Basic
/-- The `LinearMap` between spaces of matrices induced by a `LinearMap` between their
coefficients. This is `Matrix.map` as a `LinearMap`.  -/
LinearMap.mapMatrix : {m : Type u_2} →
  {n : Type u_3} →
    {R : Type u_7} →
      {S : Type u_8} →
        {α : Type u_11} →
          {β : Type u_12} →
            [inst : Semiring R] →
              [inst_1 : Semiring S] →
                {σᵣₛ : R →+* S} →
                  [inst_2 : AddCommMonoid α] →
                    [inst_3 : AddCommMonoid β] →
                      [inst_4 : Module R α] →
                        [inst_5 : Module S β] → (α →ₛₗ[σᵣₛ] β) → Matrix m n α →ₛₗ[σᵣₛ] Matrix m n β
-- Mathlib.CategoryTheory.Bicategory.Adjunction.Mate
/-- Squares between right adjoints can be composed "horizontally" by pasting.  -/
CategoryTheory.Bicategory.rightAdjointSquare.hcomp : {B : Type u} →
  [inst : CategoryTheory.Bicategory B] →
    {a b c d e f : B} →
      {g : a ⟶ d} →
        {h : b ⟶ e} →
          {k : c ⟶ f} →
            {r₁ : b ⟶ a} →
              {r₂ : e ⟶ d} →
                {r₃ : c ⟶ b} →
                  {r₄ : f ⟶ e} →
                    (CategoryTheory.CategoryStruct.comp r₁ g ⟶ CategoryTheory.CategoryStruct.comp h r₂) →
                      (CategoryTheory.CategoryStruct.comp r₃ h ⟶ CategoryTheory.CategoryStruct.comp k r₄) →
                        (CategoryTheory.CategoryStruct.comp (CategoryTheory.CategoryStruct.comp r₃ r₁) g ⟶
                          CategoryTheory.CategoryStruct.comp k (CategoryTheory.CategoryStruct.comp r₄ r₂))
-- Mathlib.Data.Seq.Basic
Stream'.Seq1.monad : Monad Stream'.Seq1
-- Mathlib.Order.Filter.AtTopBot.Group
Filter.comap_neg_atBot : ∀ {G : Type u_2} [inst : AddCommGroup G] [inst_1 : PartialOrder G] [IsOrderedAddMonoid G],
  Filter.comap Neg.neg Filter.atBot = Filter.atTop
-- Mathlib.CategoryTheory.Limits.Shapes.Images
CategoryTheory.Limits.MonoFactorisation.isoComp_e : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] {X Y : C} {f : X ⟶ Y}
  (F : CategoryTheory.Limits.MonoFactorisation f) {X' : C} (g : X' ⟶ X),
  (F.isoComp g).e = CategoryTheory.CategoryStruct.comp g F.e
-- Mathlib.Order.BourbakiWitt
ChainCompletePartialOrder.IsExtremePt.bot_isChain : ∀ {α : Type u_1} [inst : ChainCompletePartialOrder α] {x : α} {f : α → α},
  (∀ (x : α), x ≤ f x) → IsChain (fun x1 x2 => x1 ≤ x2) (ChainCompletePartialOrder.bot x f)
-- Mathlib.LinearAlgebra.Matrix.Dual
/-- The dot product as a linear equivalence to the dual.  -/
dotProductEquiv : (R : Type u_1) →
  (n : Type u_2) → [inst : CommSemiring R] → [Fintype n] → [DecidableEq n] → (n → R) ≃ₗ[R] Module.Dual R (n → R)
-- Mathlib.RingTheory.MvPolynomial.Symmetric.Defs
/-- The `n`th elementary symmetric `MvPolynomial σ R`.
It is the sum over all the degree n squarefree monomials in `MvPolynomial σ R`.  -/
MvPolynomial.esymm : (σ : Type u_5) → (R : Type u_6) → [inst : CommSemiring R] → [Fintype σ] → ℕ → MvPolynomial σ R
-- Mathlib.RingTheory.Valuation.FiniteField
/-- **Alias** of `FiniteField.valuation_algebraMap_le_one`. -/
Valuation.FiniteField.algebraMap_le_one : ∀ {Fq : Type u_1} {A : Type u_2} {Γ : Type u_3} [inst : Field Fq] [Finite Fq] [inst_2 : Ring A] [inst_3 : Algebra Fq A]
  [inst_4 : LinearOrderedCommMonoidWithZero Γ] (v : Valuation A Γ) (a : Fq), v ((algebraMap Fq A) a) ≤ 1
-- Mathlib.RingTheory.DedekindDomain.FiniteAdeleRing
/-- The support of an element `k` of the field of fractions of a Dedekind domain is
the set of maximal ideals of the Dedekind domain at which `k` is not integral.
 -/
IsDedekindDomain.HeightOneSpectrum.Support : (R : Type u_1) →
  [inst : CommRing R] →
    [IsDedekindDomain R] →
      {K : Type u_2} →
        [inst_2 : Field K] →
          [inst_3 : Algebra R K] → [IsFractionRing R K] → K → Set (IsDedekindDomain.HeightOneSpectrum R)
-- Mathlib.CategoryTheory.Comma.StructuredArrow.Basic
CategoryTheory.CostructuredArrow.proj_reflectsIsomorphisms : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {D : Type u₂} [inst_1 : CategoryTheory.Category.{v₂, u₂} D]
  {T : D} {S : CategoryTheory.Functor C D}, (CategoryTheory.CostructuredArrow.proj S T).ReflectsIsomorphisms
-- Mathlib.MeasureTheory.SpecificCodomains.ContinuousMap
/-- A natural criterion for `HasFiniteIntegral` of a `C(Y, E)`-valued function is the existence
of some positive function with finite integral such that `∀ᵐ x ∂μ, ∀ y : Y, ‖f x y‖ ≤ bound x`.
Note that there is no dominated convergence here (hence no first-countability assumption
on `Y`). We are just using the properties of Banach-space-valued integration.  -/
ContinuousMap.hasFiniteIntegral_of_bound : ∀ {X : Type u_1} {Y : Type u_2} [inst : MeasurableSpace X] {μ : MeasureTheory.Measure X} [inst_1 : TopologicalSpace Y]
  {E : Type u_3} [inst_2 : NormedAddCommGroup E] [inst_3 : CompactSpace Y] (f : X → C(Y, E)) (bound : X → ℝ),
  MeasureTheory.HasFiniteIntegral bound μ →
    (∀ᵐ (x : X) ∂μ, ∀ (y : Y), ‖(f x) y‖ ≤ bound x) → MeasureTheory.HasFiniteIntegral f μ
-- Mathlib.CategoryTheory.MorphismProperty.Factorization
/-- The term in `FactorizationData W₁ W₂` that is deduced from a functorial factorization.  -/
CategoryTheory.MorphismProperty.FunctorialFactorizationData.factorizationData : {C : Type u_1} →
  [inst : CategoryTheory.Category.{v_1, u_1} C] →
    {W₁ W₂ : CategoryTheory.MorphismProperty C} → W₁.FunctorialFactorizationData W₂ → W₁.FactorizationData W₂
-- Aesop.Search.Expansion.Norm
Aesop.NormRuleResult.succeeded : Lean.MVarId → Option (Array Aesop.Script.LazyStep) → Aesop.NormRuleResult
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.star_apply : ∀ {ι : Type u_1} {R : ι → Type u_6} [inst : (i : ι) → Star (R i)] (x : (i : ι) → R i) (i : ι), star x i = star (x i)
-- Init.Prelude
/-- Auxiliary axiom used to implement the `sorry` term and tactic.

The `sorry` term/tactic expands to `sorryAx _ (synthetic := false)`.
It is intended for stubbing-out incomplete parts of a value or proof while still having a syntactically correct skeleton.
Lean will give a warning whenever a declaration uses `sorry`, so you aren't likely to miss it,
but you can check if a declaration depends on `sorry` either directly or indirectly by looking for `sorryAx` in the output
of the `#print axioms my_thm` command.

The `synthetic` flag is false when a `sorry` is written explicitly by the user, but it is
set to `true` when a tactic fails to prove a goal, or if there is a type error
in the expression. A synthetic `sorry` acts like a regular one, except that it
suppresses follow-up errors in order to prevent an error from causing a cascade
of other errors because the desired term was not constructed.
 -/
sorryAx : (α : Sort u) → Bool → α
-- Mathlib.NumberTheory.ArithmeticFunction.Zeta
/-- `@[simp]`-normal form of `coe_zeta_smul_apply`.  -/
ArithmeticFunction.sum_divisorsAntidiagonal_eq_sum_divisors : ∀ {R : Type u_1} {M : Type u_2} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : MulAction R M]
  {f : ArithmeticFunction M} {x : ℕ},
  (∑ x ∈ x.divisorsAntidiagonal, if x.1 = 0 then 0 • f x.2 else f x.2) = ∑ i ∈ x.divisors, f i
-- Mathlib.CategoryTheory.Enriched.FunctorCategory
/-- The condition that the end `diagram V F₁ F₂` exists, see `enrichedHom`.  -/
CategoryTheory.Enriched.FunctorCategory.HasEnrichedHom : (V : Type u₁) →
  [inst : CategoryTheory.Category.{v₁, u₁} V] →
    [inst_1 : CategoryTheory.MonoidalCategory V] →
      {C : Type u₂} →
        [inst_2 : CategoryTheory.Category.{v₂, u₂} C] →
          {J : Type u₃} →
            [inst_3 : CategoryTheory.Category.{v₃, u₃} J] →
              [CategoryTheory.EnrichedOrdinaryCategory V C] →
                CategoryTheory.Functor J C → CategoryTheory.Functor J C → Prop
-- Lean.Meta.SizeOf
/-- Create a "sizeOf" function with name `declName` using the recursor `recName`.
 -/
Lean.Meta.mkSizeOfFn : Lean.Name → Lean.Name → Lean.MetaM Unit
-- Mathlib.Algebra.MonoidAlgebra.MapDomain
/-- This isn't marked as simp to avoid looping with unfolding `coeff`.  -/
MonoidAlgebra.ofCoeff_mapRange : ∀ {R : Type u_3} {S : Type u_4} {M : Type u_6} [inst : Semiring R] [inst_1 : Semiring S] (f : R →+ S) (x : M →₀ R),
  MonoidAlgebra.ofCoeff (Finsupp.mapRange ⇑f ⋯ x) = MonoidAlgebra.map f (MonoidAlgebra.ofCoeff x)
-- Init.Data.SInt.Lemmas
ISize.toInt16_ofIntTruncate : ∀ {n : ℤ},
  -2 ^ (System.Platform.numBits - 1) ≤ n →
    n < 2 ^ (System.Platform.numBits - 1) → (ISize.ofIntClamp n).toInt16 = Int16.ofInt n
-- Mathlib.RingTheory.Polynomial.Nilpotent
Polynomial.isNilpotent_reverse_iff : ∀ {R : Type u_1} [inst : CommRing R] {P : Polynomial R}, IsNilpotent P.reverse ↔ IsNilpotent P
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
CategoryTheory.Limits.Fork.IsLimit.mk_lift : ∀ {C : Type u} {X Y : C} [inst : CategoryTheory.Category.{v, u} C] {f g : X ⟶ Y} (t : CategoryTheory.Limits.Fork f g)
  (lift : (s : CategoryTheory.Limits.Fork f g) → s.pt ⟶ t.pt)
  (fac : ∀ (s : CategoryTheory.Limits.Fork f g), CategoryTheory.CategoryStruct.comp (lift s) t.ι = s.ι)
  (uniq :
    ∀ (s : CategoryTheory.Limits.Fork f g) (m : s.pt ⟶ t.pt),
      CategoryTheory.CategoryStruct.comp m t.ι = s.ι → m = lift s)
  (s : CategoryTheory.Limits.Fork f g), (CategoryTheory.Limits.Fork.IsLimit.mk t lift fac uniq).lift s = lift s
-- Mathlib.Data.Nat.Sqrt
Nat.sqrt_le_add : ∀ (n : ℕ), n ≤ n.sqrt * n.sqrt + n.sqrt + n.sqrt
-- Init.Data.Vector.Lex
Vector.map_lt : ∀ {α : Type u_1} {β : Type u_2} {n : ℕ} [inst : LT α] [inst_1 : LT β] {xs ys : Vector α n} {f : α → β},
  (∀ (x y : α), x < y → f x < f y) → xs < ys → Vector.map f xs < Vector.map f ys
-- Mathlib.CategoryTheory.Limits.Shapes.SingleObj
CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints_symm_apply : ∀ {M : Type v} [inst : Monoid M] (J : CategoryTheory.Functor (CategoryTheory.SingleObj M) (Type u))
  (a : ↑(MulAction.fixedPoints M (J.obj (CategoryTheory.SingleObj.star M)))),
  (CategoryTheory.Limits.SingleObj.Types.limitEquivFixedPoints J).symm a =
    (CategoryTheory.Limits.Types.limitEquivSections J).symm
      ((CategoryTheory.Limits.SingleObj.Types.sections.equivFixedPoints J).symm a)
-- Mathlib.Data.List.Lattice
_private.Mathlib.Data.List.Lattice.0.List.bagInter.match_1.eq_2 : ∀ {α : Type u_1} (motive : List α → List α → Sort u_2) (x : List α) (h_1 : (x : List α) → motive [] x)
  (h_2 : (x : List α) → motive x []) (h_3 : (a : α) → (l₁ l₂ : List α) → motive (a :: l₁) l₂),
  (x = [] → False) →
    (match x, [] with
      | [], x => h_1 x
      | x, [] => h_2 x
      | a :: l₁, l₂ => h_3 a l₁ l₂) =
      h_2 x
-- Mathlib.Data.Set.Pairwise.Basic
/-- See also `Set.Pairwise.image`.  -/
Set.InjOn.pairwise_image : ∀ {α : Type u_1} {ι : Type u_4} {r : α → α → Prop} {f : ι → α} {s : Set ι},
  Set.InjOn f s → ((f '' s).Pairwise r ↔ s.Pairwise (Function.onFun r f))
-- Mathlib.Data.Set.PowersetCard
/-- If `0 < n < ENat.card α`, then `powersetCard α n` is nontrivial.  -/
Set.powersetCard.nontrivial : ∀ {α : Type u_1} {n : ℕ}, 0 < n → ↑n < ENat.card α → Nontrivial ↑(Set.powersetCard α n)
-- Mathlib.Data.Finset.Range
Finset.mem_range : ∀ {n m : ℕ}, m ∈ Finset.range n ↔ m < n
-- Mathlib.Algebra.GroupWithZero.Action.Pointwise.Finset
/-- A nonempty set is scaled by zero to the singleton set containing zero.  -/
Finset.zero_smul_finset : ∀ {α : Type u_1} {β : Type u_2} [inst : DecidableEq β] [inst_1 : Zero α] [inst_2 : Zero β] [inst_3 : SMulWithZero α β]
  {s : Finset β}, s.Nonempty → 0 • s = 0
-- Mathlib.CategoryTheory.Functor.Functorial
/-- `G ∘ F` is a functorial if both `F` and `G` are.
 -/
CategoryTheory.functorial_comp : {C : Type u₁} →
  [inst : CategoryTheory.Category.{v₁, u₁} C] →
    {D : Type u₂} →
      [inst_1 : CategoryTheory.Category.{v₂, u₂} D] →
        {E : Type u₃} →
          [inst_2 : CategoryTheory.Category.{v₃, u₃} E] →
            (F : C → D) →
              [CategoryTheory.Functorial F] →
                (G : D → E) → [CategoryTheory.Functorial G] → CategoryTheory.Functorial (G ∘ F)
-- Mathlib.Analysis.Calculus.ContDiff.FTaylorSeries
norm_iteratedFDerivWithin_one : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] {E : Type uE} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type uF} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {s : Set E}
  {x : E} (f : E → F), UniqueDiffWithinAt 𝕜 s x → ‖iteratedFDerivWithin 𝕜 1 f s x‖ = ‖fderivWithin 𝕜 f s x‖
-- Mathlib.Data.Fintype.EquivFin
instInfiniteNat : Infinite ℕ
-- Mathlib.NumberTheory.RamificationInertia.Inertia
/-- **Alias** of `Ideal.absNorm_eq_pow_inertiaDeg'_of_liesOver`. -/
Ideal.absNorm_eq_pow_inertiaDeg_of_liesOver : ∀ {R : Type u} [inst : CommRing R] {S : Type u_1} [inst_1 : CommRing S] [inst_2 : IsDedekindDomain S]
  [inst_3 : Module.Free ℤ S] [inst_4 : IsDedekindDomain R] [inst_5 : Module.Free ℤ R] [inst_6 : Algebra S R]
  [Module.Finite S R] (P : Ideal R) (p : Ideal S) [P.LiesOver p],
  p.IsPrime → p ≠ ⊥ → Ideal.absNorm P = Ideal.absNorm p ^ p.inertiaDeg' P
-- Mathlib.MeasureTheory.Function.LpSpace.DomAct.Basic
DomAddAct.mk_vadd_indicatorConstLp : ∀ {M : Type u_1} {α : Type u_3} {E : Type u_4} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
  {μ : MeasureTheory.Measure α} {p : ENNReal} [inst_2 : VAdd M α] [inst_3 : MeasureTheory.VAddInvariantMeasure M α μ]
  [inst_4 : MeasurableConstVAdd M α] (c : M) {s : Set α} (hs : MeasurableSet s) (hμs : μ s ≠ ⊤) (b : E),
  DomAddAct.mk c +ᵥ MeasureTheory.indicatorConstLp p hs hμs b = MeasureTheory.indicatorConstLp p ⋯ ⋯ b
-- Init.Internal.Order.Basic
Lean.Order.CCPO.csup_spec : ∀ {α : Sort u} [inst : Lean.Order.CCPO α] {c : α → Prop} (hc : Lean.Order.chain c),
  Lean.Order.is_sup c (Lean.Order.CCPO.csup hc)
-- Init.Data.UInt.Bitwise
UInt64.zero_and : ∀ {a : UInt64}, 0 &&& a = 0
-- Mathlib.Analysis.InnerProductSpace.EuclideanDist
Euclidean.nhds_basis_ball : ∀ {E : Type u_1} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E] [inst_2 : IsTopologicalAddGroup E]
  [inst_3 : T2Space E] [inst_4 : Module ℝ E] [inst_5 : ContinuousSMul ℝ E] [inst_6 : FiniteDimensional ℝ E] {x : E},
  (nhds x).HasBasis (fun r => 0 < r) (Euclidean.ball x)
-- Mathlib.SetTheory.ZFC.Ordinal
ZFSet.IsOrdinal.isTrans : ∀ {x : ZFSet.{u}}, x.IsOrdinal → IsTrans (↥x) (Subrel (fun x1 x2 => x1 ∈ x2) fun x_1 => x_1 ∈ x)
-- Mathlib.Data.List.Nodup
List.Nodup.ne_singleton_iff : ∀ {α : Type u} {l : List α}, l.Nodup → ∀ (x : α), l ≠ [x] ↔ l = [] ∨ ∃ y ∈ l, y ≠ x
-- Mathlib.Order.Hom.Bounded
/-- The type of `⊤`-preserving functions from `α` to `β`.  -/
TopHom : (α : Type u_6) → (β : Type u_7) → [Top α] → [Top β] → Type (max u_6 u_7)
-- Std.Data.DTreeMap.Internal.WF.Defs
Std.DTreeMap.Internal.Impl.WF.insertManyIfNew : ∀ {α : Type u} {β : α → Type v} [inst : Ord α] {ρ : Type u_1} [inst_1 : ForIn Id ρ ((a : α) × β a)]
  {t : Std.DTreeMap.Internal.Impl α β} {l : ρ} {h : t.Balanced}, t.WF → (↑(t.insertManyIfNew l h)).WF
-- Init.Grind.Attr
/-- The `norm` modifier instructs `grind` to use a theorem as a normalization rule. That is,
the theorem is applied during the preprocessing step.
This feature is meant for advanced users who understand how the preprocessor and `grind`'s search
procedure interact with each other.
New users can still benefit from this feature by restricting its use to theorems that completely
eliminate a symbol from the goal. Example:
```
theorem max_def : max n m = if n ≤ m then m else n
```
For a negative example, consider:
```
opaque f : Int → Int → Int → Int
theorem fax1 : f x 0 1 = 1 := sorry
theorem fax2 : f 1 x 1 = 1 := sorry
attribute [grind norm] fax1
attribute [grind =] fax2

example (h : c = 1) : f c 0 c = 1 := by
  grind -- fails
```
In this example, `fax1` is a normalization rule, but it is not applicable to the input goal since
`f c 0 c` is not an instance of `f x 0 1`. However, `f c 0 c` matches the pattern `f 1 x 1` modulo
the equality `c = 1`. Thus, `grind` instantiates `fax2` with `x := 0`, producing the equality
`f 1 0 1 = 1`, which the normalizer simplifies to `True`. As a result, nothing useful is learned.
In the future, we plan to include linters to automatically detect issues like these.
Example:
```
opaque f : Nat → Nat
opaque g : Nat → Nat

@[grind norm] axiom fax : f x = x + 2
@[grind norm ←] axiom fg : f x = g x

example : f x ≥ 2 := by grind
example : f x ≥ g x := by grind
example : f x + g x ≥ 4 := by grind
```
 -/
Lean.Parser.Attr.grindNorm : Lean.ParserDescr
-- Mathlib.RingTheory.Congruence.Opposite
RingCon.opOrderIso_symm_apply : ∀ {R : Type u_1} [inst : Add R] [inst_1 : Mul R] (c : RingCon Rᵐᵒᵖ), (RelIso.symm RingCon.opOrderIso) c = c.unop
-- Std.Data.DTreeMap.Basic
/-- Tries to retrieve the smallest key in the tree map, panicking if the map is empty.
 -/
Std.DTreeMap.minKey! : {α : Type u} → {β : α → Type v} → {cmp : α → α → Ordering} → [Inhabited α] → Std.DTreeMap α β cmp → α
-- Mathlib.Algebra.Star.CHSH
IsCHSHTuple.A₀B₀_commutes : ∀ {R : Type u_1} [inst : Monoid R] [inst_1 : StarMul R] {A₀ A₁ B₀ B₁ : R}, IsCHSHTuple A₀ A₁ B₀ B₁ → A₀ * B₀ = B₀ * A₀
-- Mathlib.Analysis.Normed.Group.Seminorm
AddGroupSeminorm.mk : {G : Type u_6} →
  [inst : AddGroup G] →
    (toFun : G → ℝ) →
      toFun 0 = 0 →
        (∀ (r s : G), toFun (r + s) ≤ toFun r + toFun s) → (∀ (r : G), toFun (-r) = toFun r) → AddGroupSeminorm G
-- Mathlib.Analysis.SpecialFunctions.Log.Basic
Real.image_log_Ioc_zero : ∀ {a : ℝ}, 0 < a → Real.log '' Set.Ioc 0 a = Set.Iic (Real.log a)
-- Std.Data.DHashMap.Internal.WF
Std.DHashMap.Internal.Raw₀.getKeyₘ_eq_getKey : ∀ {α : Type u} {β : α → Type v} [inst : BEq α] [inst_1 : Hashable α] [inst_2 : EquivBEq α] [inst_3 : LawfulHashable α]
  {m : Std.DHashMap.Internal.Raw₀ α β} (hm : Std.DHashMap.Internal.Raw.WFImp ↑m) {a : α} {h : m.contains a = true},
  m.getKeyₘ a h = Std.Internal.List.getKey a (Std.DHashMap.Internal.toListModel (↑m).buckets) ⋯
-- Aesop.Tree.UnsafeQueue
Aesop.UnsafeQueueEntry.unsafeRule.injEq : ∀ (r r_1 : Aesop.IndexMatchResult Aesop.UnsafeRule),
  (Aesop.UnsafeQueueEntry.unsafeRule r = Aesop.UnsafeQueueEntry.unsafeRule r_1) = (r = r_1)
-- Lean.ScopedEnvExtension
Lean.SimpleScopedEnvExtension.Descr.mk : {α σ : Type} →
  autoParam Lean.Name Lean.SimpleScopedEnvExtension.Descr.name._autoParam →
    (σ → α → σ) →
      σ → (σ → σ) → (Lean.Environment → α → Lean.OLeanEntries (Option α)) → Lean.SimpleScopedEnvExtension.Descr α σ
-- Mathlib.Algebra.Algebra.Spectrum.Quasispectrum
/-- If `φ` is non-unital algebra homomorphism over a scalar ring `R`, then
`quasispectrum R (φ a) ⊆ quasispectrum R a`.  -/
NonUnitalAlgHom.quasispectrum_apply_subset : ∀ {F : Type u_3} {R : Type u_4} {A : Type u_5} {B : Type u_6} [inst : CommRing R] [inst_1 : NonUnitalRing A]
  [inst_2 : NonUnitalRing B] [inst_3 : Module R A] [inst_4 : Module R B] [inst_5 : FunLike F A B]
  [NonUnitalAlgHomClass F R A B] (φ : F) (a : A), quasispectrum R (φ a) ⊆ quasispectrum R a
-- Lean.Data.Lsp.Internal
Lean.Lsp.LeanModuleQuery.mk.injEq : ∀ (identifier : String) (openNamespaces : Array Lean.Lsp.OpenNamespace) (identifier_1 : String)
  (openNamespaces_1 : Array Lean.Lsp.OpenNamespace),
  ({ identifier := identifier, openNamespaces := openNamespaces } =
      { identifier := identifier_1, openNamespaces := openNamespaces_1 }) =
    (identifier = identifier_1 ∧ openNamespaces = openNamespaces_1)
-- Mathlib.CategoryTheory.Types.Basic
CategoryTheory.types_comp_apply : ∀ {X Y Z : Type u} (f : X ⟶ Y) (g : Y ⟶ Z) (x : X),
  (CategoryTheory.ConcreteCategory.hom (CategoryTheory.CategoryStruct.comp f g)) x =
    (CategoryTheory.ConcreteCategory.hom g) ((CategoryTheory.ConcreteCategory.hom f) x)
-- Mathlib.LinearAlgebra.Matrix.ConjTranspose
Matrix.conjTranspose_inj : ∀ {m : Type u_2} {n : Type u_3} {α : Type v} [inst : InvolutiveStar α] {A B : Matrix m n α},
  A.conjTranspose = B.conjTranspose ↔ A = B
-- Mathlib.RingTheory.TwoSidedIdeal.Operations
Ideal.toTwoSided_asIdeal : ∀ {R : Type u_1} [inst : Ring R] (I : TwoSidedIdeal R), (TwoSidedIdeal.asIdeal I).toTwoSided = I
-- Init.Omega.Int
Lean.Omega.Fin.not_lt : ∀ {n : ℕ} {i j : Fin n}, ¬i < j ↔ j ≤ i