mathlib-initiative/mathlib-types huggingface dataset:
-- Mathlib.FieldTheory.Galois.IsGaloisGroup
/-- The cardinality of a Galois group equals the degree of the field extension.

See `IsGaloisGroup.card_eq_finrank'` for a ring-theoretic generalization assuming finiteness.  -/
IsGaloisGroup.card_eq_finrank : ∀ (G : Type u_1) (K : Type u_3) (L : Type u_4) [inst : Group G] [inst_1 : Field K] [inst_2 : Field L]
  [inst_3 : Algebra K L] [inst_4 : MulSemiringAction G L] [IsGaloisGroup G K L], Nat.card G = Module.finrank K L
-- Aesop.Script.Tactic
Aesop.Script.STactic.mk : ℕ → (Array (Array Lean.Syntax.Tactic) → Lean.Syntax.Tactic) → Aesop.Script.STactic
-- Mathlib.LinearAlgebra.Prod
Submodule.comap_snd : ∀ {R : Type u} {M : Type v} {M₂ : Type w} [inst : Semiring R] [inst_1 : AddCommMonoid M] [inst_2 : AddCommMonoid M₂]
  [inst_3 : Module R M] [inst_4 : Module R M₂] (q : Submodule R M₂), Submodule.comap (LinearMap.snd R M M₂) q = ⊤.prod q
-- Mathlib.Tactic.Linter.TextBased.UnicodeLinter
/-- Other unicode characters present in Mathlib but not present in any of the above lists
(as of March 17, 2026).

This list may be extended by more characters for which no VSCode-extension abbreviation exists.
Some guidelines:
- No invisible characters
- No characters affecting text directionality (Mathlib uses left-to-right text).
- No [Private Use Areas](https://en.wikipedia.org/wiki/Private_Use_Areas)

The list `withVSCodeAbbrev` contains characters with abbreviations; if an abbreviation
already has been defined, you might need to update the list `withVSCodeAbbrev`.
Further, consider proposing an abbreviation to [the extension](https://github.com/leanprover/vscode-lean4) for new symbols.

Empty lines for improved readability (otherwise some characters overlap in some fonts).
 -/
_private.Mathlib.Tactic.Linter.TextBased.UnicodeLinter.0.Mathlib.Linter.TextBased.UnicodeLinter.othersInMathlib : Array Char
-- Mathlib.Topology.Closure
mem_frontier_iff_notMem_interior : ∀ {X : Type u} [inst : TopologicalSpace X] {s : Set X} {x : X}, x ∈ s → (x ∈ frontier s ↔ x ∉ interior s)
-- Std.Data.DTreeMap.Internal.Lemmas
Std.DTreeMap.Internal.Impl.getD_inter!_of_contains_right : ∀ {α : Type u} {β : α → Type v} {instOrd : Ord α} {m₁ m₂ : Std.DTreeMap.Internal.Impl α β} [Std.TransOrd α]
  [inst : Std.LawfulEqOrd α],
  m₁.WF →
    m₂.WF →
      ∀ {k : α} {fallback : β k},
        Std.DTreeMap.Internal.Impl.contains k m₂ = true → (m₁.inter! m₂).getD k fallback = m₁.getD k fallback
-- Mathlib.Data.UInt
UInt8.toBitVec_nsmul : ∀ (n : ℕ) (a : UInt8), (n • a).toBitVec = n • a.toBitVec
-- Mathlib.Topology.Order.OrderClosed
not_tendsto_atTop_of_tendsto_nhds : ∀ {α : Type u} {β : Type v} [inst : Preorder α] [NoTopOrder α] [inst_2 : TopologicalSpace α] [ClosedIciTopology α]
  {a : α} {l : Filter β} [l.NeBot] {f : β → α}, Filter.Tendsto f l (nhds a) → ¬Filter.Tendsto f l Filter.atTop
-- Std.Sync.CancellationToken
/-- Waits for cancellation. Returns a task that completes when cancelled.
 -/
Std.CancellationToken.wait : Std.CancellationToken → IO (Std.Async.AsyncTask Unit)
-- Mathlib.Data.ENNReal.BigOperators
ENNReal.ofReal_prod_of_nonneg : ∀ {α : Type u_3} {s : Finset α} {f : α → ℝ},
  (∀ i ∈ s, 0 ≤ f i) → ENNReal.ofReal (∏ i ∈ s, f i) = ∏ i ∈ s, ENNReal.ofReal (f i)
-- Mathlib.Order.LatticeIntervals
Set.Ici.semilatticeInf : {α : Type u_1} → [inst : SemilatticeInf α] → {a : α} → SemilatticeInf ↑(Set.Ici a)
-- Lean.Widget.TaggedText
Lean.Widget.instToJsonTaggedText.toJson : {α : Type u_1} → [Lean.ToJson α] → Lean.Widget.TaggedText α → Lean.Json
-- Mathlib.Combinatorics.Matroid.Map
Matroid.IsBasis.map : ∀ {α : Type u_1} {β : Type u_2} {I : Set α} {M : Matroid α} {X : Set α},
  M.IsBasis I X → ∀ {f : α → β} (hf : Set.InjOn f M.E), (M.map f hf).IsBasis (f '' I) (f '' X)
-- Mathlib.Data.NNReal.Defs
NNReal.one_le_coe : ∀ {r : NNReal}, 1 ≤ ↑r ↔ 1 ≤ r
-- Mathlib.Geometry.Manifold.Diffeomorph
Diffeomorph.toEquiv_coe_symm : ∀ {𝕜 : Type u_1} [inst : NontriviallyNormedField 𝕜] {E : Type u_2} [inst_1 : NormedAddCommGroup E]
  [inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F] {H : Type u_5}
  [inst_5 : TopologicalSpace H] {G : Type u_7} [inst_6 : TopologicalSpace G] {I : ModelWithCorners 𝕜 E H}
  {J : ModelWithCorners 𝕜 F G} {M : Type u_9} [inst_7 : TopologicalSpace M] [inst_8 : ChartedSpace H M] {N : Type u_11}
  [inst_9 : TopologicalSpace N] [inst_10 : ChartedSpace G N] {n : WithTop ℕ∞} (h : Diffeomorph I J M N n),
  ⇑h.symm = ⇑h.symm
-- Mathlib.Data.Finset.Card
Finset.card_sdiff_add_card_inter : ∀ {α : Type u_1} [inst : DecidableEq α] (s t : Finset α), (s \ t).card + (s ∩ t).card = s.card
-- Mathlib.CategoryTheory.Limits.Shapes.RegularMono
/-- Every regular epimorphism is an epimorphism.  -/
CategoryTheory.RegularEpi.epi : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y) (h : CategoryTheory.RegularEpi f),
  CategoryTheory.Epi f
-- Lean.Meta.Tactic.Grind.Types
/-- Number of theorem instances generated so far.  -/
Lean.Meta.Grind.EMatch.State.numInstances : Lean.Meta.Grind.EMatch.State → ℕ
-- Mathlib.Algebra.Group.Subsemigroup.Defs
/-- A substructure satisfying `MulMemClass` is closed under multiplication.  -/
MulMemClass.mul_mem : ∀ {S : Type u_3} {M : outParam (Type u_4)} {inst : Mul M} {inst_1 : SetLike S M} [self : MulMemClass S M] {s : S}
  {a b : M}, a ∈ s → b ∈ s → a * b ∈ s
-- Mathlib.FieldTheory.IntermediateField.Basic
/-- An intermediate field contains the image of the smaller field.  -/
IntermediateField.algebraMap_mem : ∀ {K : Type u_1} {L : Type u_2} [inst : Field K] [inst_1 : Field L] [inst_2 : Algebra K L] (S : IntermediateField K L)
  (x : K), (algebraMap K L) x ∈ S
-- Mathlib.Algebra.Order.Monoid.NatCast
/-- **Alias** of `zero_lt_two`.

---

See `zero_lt_two'` for a version with the type explicit.  -/
two_pos : ∀ {α : Type u_1} [inst : AddMonoidWithOne α] [inst_1 : PartialOrder α] [ZeroLEOneClass α] [NeZero 1] [AddLeftMono α],
  0 < 2
-- Mathlib.Algebra.Notation.Pi.Defs
Pi.inv_comp : ∀ {α : Type u_2} {β : Type u_3} {G : Type u_7} [inst : Inv G] (f : β → G) (g : α → β), f⁻¹ ∘ g = (f ∘ g)⁻¹
-- Mathlib.Algebra.Category.AlgCat.Limits
AlgCat.hasLimits : ∀ {R : Type u} [inst : CommRing R], CategoryTheory.Limits.HasLimits (AlgCat R)
-- Lean.Data.Json.FromToJson.Basic
Lean.UInt64.fromJson? : Lean.Json → Except String UInt64
-- Mathlib.AlgebraicGeometry.Sites.Fpqc
AlgebraicGeometry.Scheme.zariskiPrecoverage_le_fpqcPrecoverage : AlgebraicGeometry.Scheme.zariskiPrecoverage ≤ AlgebraicGeometry.Scheme.fpqcPrecoverage
-- Mathlib.NumberTheory.Padics.PadicVal.Basic
padicValInt_self : ∀ {p : ℕ} [hp : Fact (Nat.Prime p)], padicValInt p ↑p = 1
-- Mathlib.RingTheory.Ideal.Maps
/-- Variant of `Ideal.IsPrime.comap` where ideal is explicit rather than implicit.  -/
Ideal.comap_isPrime : ∀ {R : Type u} {S : Type v} {F : Type u_1} [inst : Semiring R] [inst_1 : Semiring S] [inst_2 : FunLike F R S] (f : F)
  (K : Ideal S) [inst_3 : RingHomClass F R S] [H : K.IsPrime], (Ideal.comap f K).IsPrime
-- Mathlib.Order.Minimal
minimal_mem_image_antitone : ∀ {α : Type u_2} {β : Type u_3} {x : α} [inst : Preorder α] [inst_1 : Preorder β] {s : Set α} {f : α → β},
  (∀ ⦃x y : α⦄, x ∈ s → y ∈ s → (f x ≤ f y ↔ y ≤ x)) → Minimal (fun x => x ∈ s) x → Maximal (fun x => x ∈ f '' s) (f x)
-- Mathlib.Algebra.MonoidAlgebra.ToDirectSum
AddMonoidAlgebra.toDirectSum_single : ∀ {ι : Type u_1} {M : Type u_3} [inst : DecidableEq ι] [inst_1 : Semiring M] (i : ι) (m : M),
  (AddMonoidAlgebra.single i m).toDirectSum = (DirectSum.of (fun x => M) i) m
-- Init.Grind.Module.Basic
Lean.Grind.AddCommMonoid.add_left_comm : ∀ {M : Type u} [inst : Lean.Grind.AddCommMonoid M] (a b c : M), a + (b + c) = b + (a + c)
-- Mathlib.SetTheory.Ordinal.Notation
ONote.repr_zero : ONote.repr 0 = 0
-- Mathlib.Topology.Algebra.SeparationQuotient.Basic
SeparationQuotient.instAddGroup : {G : Type u_1} →
  [inst : TopologicalSpace G] → [inst_1 : AddGroup G] → [IsTopologicalAddGroup G] → AddGroup (SeparationQuotient G)
-- Mathlib.CategoryTheory.Limits.Shapes.Reflexive
CategoryTheory.Limits.WalkingReflexivePair.map_reflexion_comp_map_right_assoc : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (F : CategoryTheory.Functor CategoryTheory.Limits.WalkingReflexivePair C) {Z : C}
  (h : F.obj CategoryTheory.Limits.WalkingReflexivePair.zero ⟶ Z),
  CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.reflexion)
      (CategoryTheory.CategoryStruct.comp (F.map CategoryTheory.Limits.WalkingReflexivePair.Hom.right) h) =
    h
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.torsionBySet_ideal_isTorsion_of_noZeroDivisors : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M]
  [NoZeroDivisors R] [Nontrivial R] {I : Ideal R}, I ≠ ⊥ → Module.IsTorsion R ↥(Submodule.torsionBySet R M ↑I)
-- Batteries.Data.Array.Scan
List.toArray_scanl : ∀ {β : Type u_1} {α : Type u_2} {init : β} {f : β → α → β} {as : List α},
  (List.scanl f init as).toArray = Array.scanl f init as.toArray
-- Mathlib.Logic.Nontrivial.Defs
/-- Pushforward a `Nontrivial` instance along an injective function.  -/
Function.Injective.nontrivial : ∀ {α : Type u_1} {β : Type u_2} [Nontrivial α] {f : α → β}, Function.Injective f → Nontrivial β
-- Init.Data.String.Lemmas.Slice
String.Slice.Pos.get?_eq_none : ∀ {s : String.Slice} {p : s.Pos}, p = s.endPos → p.get? = none
-- Mathlib.Data.Part
Part.bind_none : ∀ {α : Type u_1} {β : Type u_2} (f : α → Part β), Part.none.bind f = Part.none
-- Mathlib.Order.SuccPred.Limit
/-- A value can be built by building it on minimal elements, successors,
and successor limits.  -/
Order.isSuccLimitRecOn : {α : Type u_1} →
  (b : α) →
    {motive : α → Sort u_2} →
      [inst : PartialOrder α] →
        [inst_1 : SuccOrder α] →
          ((a : α) → IsMin a → motive a) →
            ((a : α) → ¬IsMax a → motive (Order.succ a)) → ((a : α) → Order.IsSuccLimit a → motive a) → motive b
-- Mathlib.Analysis.Fourier.AddCircle
/-- If the sequence of Fourier coefficients of `f` is summable, then the Fourier series of `f`
converges everywhere pointwise to `f`.  -/
has_pointwise_sum_fourier_series_of_summable : ∀ {T : ℝ} [hT : Fact (0 < T)] {f : C(AddCircle T, ℂ)},
  Summable (fourierCoeff ⇑f) → ∀ (x : AddCircle T), HasSum (fun i => fourierCoeff (⇑f) i • (fourier i) x) (f x)
-- Mathlib.RingTheory.ZariskisMainTheorem
/-- [Stacks Tag 00PT](https://stacks.math.columbia.edu/tag/00PT) -/
exists_isIntegral_sub_of_isIntegralElem_of_mul_mem_range : ∀ {R : Type u_1} {S : Type u_2} [inst : CommRing R] [inst_1 : CommRing S] [inst_2 : Algebra R S]
  (φ : Polynomial R →ₐ[R] S) (t : S) (p : Polynomial R),
  φ.IsIntegralElem t → p.Monic → φ p * t ∈ φ.range → ∃ q, IsIntegral R (t - φ q)
-- Std.Http.Server.Handler
/-- Builds a `StatelessHandler` from a request-handling function.
 -/
Std.Http.Server.Handler.ofFn : (Std.Http.Request Std.Http.Body.Stream → Std.Async.ContextAsync (Std.Http.Response Std.Http.Body.Any)) →
  Std.Http.Server.StatelessHandler
-- Mathlib.Analysis.BoxIntegral.Basic
BoxIntegral.Integrable.smul : ∀ {ι : Type u} {E : Type v} {F : Type w} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
  [inst_2 : NormedAddCommGroup F] [inst_3 : NormedSpace ℝ F] {I : BoxIntegral.Box ι} [inst_4 : Fintype ι]
  {l : BoxIntegral.IntegrationParams} {f : (ι → ℝ) → E} {vol : BoxIntegral.BoxAdditiveMap ι (E →L[ℝ] F) ⊤},
  BoxIntegral.Integrable I l f vol → ∀ (c : ℝ), BoxIntegral.Integrable I l (c • f) vol
-- Mathlib.RingTheory.Trace.Quotient
_private.Mathlib.RingTheory.Trace.Quotient.0.termPS : Lean.ParserDescr
-- Mathlib.Algebra.Homology.HomotopyCategory.MappingCone
CochainComplex.mappingCone.descCochain.eq_1 : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v, u_1} C] [inst_1 : CategoryTheory.Preadditive C]
  {F G : CochainComplex C ℤ} (φ : F ⟶ G) [inst_2 : HomologicalComplex.HasHomotopyCofiber φ] {K : CochainComplex C ℤ}
  {n m : ℤ} (α : CochainComplex.HomComplex.Cochain F K m) (β : CochainComplex.HomComplex.Cochain G K n) (h : m + 1 = n),
  CochainComplex.mappingCone.descCochain φ α β h =
    (↑(CochainComplex.mappingCone.fst φ)).comp α ⋯ + (CochainComplex.mappingCone.snd φ).comp β ⋯
-- Mathlib.Data.Finset.Lattice.Fold
Finset.inf_image : ∀ {α : Type u_2} {β : Type u_3} {γ : Type u_4} [inst : SemilatticeInf α] [inst_1 : OrderTop α] [inst_2 : DecidableEq β]
  (s : Finset γ) (f : γ → β) (g : β → α), (Finset.image f s).inf g = s.inf (g ∘ f)
-- Lean.Data.Lsp.TextSync
Lean.Lsp.DidChangeTextDocumentParams.textDocument : Lean.Lsp.DidChangeTextDocumentParams → Lean.Lsp.VersionedTextDocumentIdentifier
-- Mathlib.Algebra.Homology.SpectralObject.HasSpectralSequence
CategoryTheory.Abelian.SpectralObject.instHasSpectralSequenceEIntProdNatCoreE₂HomologicalNat : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] [inst_1 : CategoryTheory.Abelian C]
  (Y : CategoryTheory.Abelian.SpectralObject C EInt) [Y.IsThirdQuadrant],
  Y.HasSpectralSequence CategoryTheory.Abelian.SpectralObject.coreE₂HomologicalNat
-- Mathlib.RingTheory.RootsOfUnity.PrimitiveRoots
/-- The sub-algebra generated by two roots of unity of order `k₁` and `k₂` resp. is the same as the one
generated by a root of unity of order `lcm k₁ k₂`.
See `IsPrimitiveRoot.pow_mul_pow_lcm` for how to construct a root of unity of order `lcm k₁ k₂`
from roots of unity of order `k₁` and `k₂`.
 -/
IsPrimitiveRoot.adjoin_pair_eq : ∀ {R : Type u_4} [inst : CommRing R] [IsDomain R] (S : Type u_7) [inst_2 : CommSemiring S] [inst_3 : Algebra S R]
  {ζ₁ ζ₂ : R} {k₁ k₂ : ℕ},
  IsPrimitiveRoot ζ₁ k₁ →
    IsPrimitiveRoot ζ₂ k₂ → k₁ ≠ 0 → k₂ ≠ 0 → ∀ {ζ : R}, IsPrimitiveRoot ζ (k₁.lcm k₂) → S[ζ₁, ζ₂] = S[ζ]
-- Mathlib.Algebra.Order.Ring.Unbundled.Basic
/-- Binary **rearrangement inequality**.  -/
mul_add_mul_le_mul_add_mul : ∀ {R : Type u} [inst : Semiring R] [inst_1 : PartialOrder R] {a b c d : R} [ExistsAddOfLE R] [MulPosMono R]
  [AddLeftMono R] [AddLeftReflectLE R], a ≤ b → c ≤ d → a * d + b * c ≤ a * c + b * d
-- Mathlib.Topology.Bases
Topology.IsInducing.firstCountableTopology : ∀ {α : Type u} [t : TopologicalSpace α] {β : Type u_1} [inst : TopologicalSpace β] [FirstCountableTopology β]
  {f : α → β}, Topology.IsInducing f → FirstCountableTopology α
-- Mathlib.Tactic.DepRewrite
/-- Compute the motive that casts `e` back to `te[p/x, rfl/h, …]`.  -/
_private.Mathlib.Tactic.DepRewrite.0.Mathlib.Tactic.DepRewrite.castBack?.motive : Lean.Expr → Lean.Expr → Lean.Expr → Array (Lean.FVarId × Lean.Expr) → Std.HashSet Lean.FVarId → Lean.MetaM Lean.Expr
-- Batteries.Tactic.Lint.Frontend
/-- The command `#list_linters` prints a list of all available linters.  -/
Batteries.Tactic.Lint.«command#list_linters» : Lean.ParserDescr
-- Mathlib.Algebra.Module.Torsion.Basic
Submodule.iSup_torsionBySet_ideal_eq_torsionBySet_iInf : ∀ {R : Type u_1} {M : Type u_2} [inst : CommSemiring R] [inst_1 : AddCommMonoid M] [inst_2 : Module R M] {ι : Type u_3}
  {p : ι → Ideal R} {S : Finset ι},
  ((↑S).Pairwise fun i j => p i ⊔ p j = ⊤) →
    ⨆ i ∈ S, Submodule.torsionBySet R M ↑(p i) = Submodule.torsionBySet R M ↑(⨅ i ∈ S, p i)
-- Mathlib.Algebra.Order.GroupWithZero.Basic
one_le_inv_iff₀ : ∀ {G₀ : Type u_3} [inst : GroupWithZero G₀] [inst_1 : PartialOrder G₀] [PosMulReflectLT G₀] {a : G₀}
  [ZeroLEOneClass G₀], 1 ≤ a⁻¹ ↔ 0 < a ∧ a ≤ 1
-- Lean.Compiler.IR.Basic
Lean.IR.CtorInfo.mk.sizeOf_spec : ∀ (name : Lean.Name) (cidx size usize ssize : ℕ),
  sizeOf { name := name, cidx := cidx, size := size, usize := usize, ssize := ssize } =
    1 + sizeOf name + sizeOf cidx + sizeOf size + sizeOf usize + sizeOf ssize
-- Mathlib.SetTheory.Ordinal.Notation
ONote.split_add_lt : ∀ {o e : ONote} {n : ℕ+} {a : ONote} {m : ℕ} [o.NF], o.split = (e.oadd n a, m) → a.repr + ↑m < Ordinal.omega0 ^ e.repr
-- Init.Data.Int.Linear
Int.Internal.Linear.Expr.toPoly'.go.eq_3 : ∀ (coeff : ℤ) (a b : Int.Internal.Linear.Expr),
  Int.Internal.Linear.Expr.toPoly'.go coeff (a.add b) =
    Int.Internal.Linear.Expr.toPoly'.go coeff a ∘ Int.Internal.Linear.Expr.toPoly'.go coeff b
-- Mathlib.AlgebraicTopology.SimplicialComplex.Basic
/-- the faces of this simplicial complex: currently, given by their spanning vertices  -/
PreAbstractSimplicialComplex.faces : {ι : Type u_1} → PreAbstractSimplicialComplex ι → Set (Finset ι)
-- Mathlib.CategoryTheory.Comma.Presheaf.Basic
/-- Intermediate stage of assembling the counit.  -/
CategoryTheory.OverPresheafAux.counitAux : {C : Type u} →
  [inst : CategoryTheory.Category.{v, u} C] →
    {A : CategoryTheory.Functor Cᵒᵖ (Type v)} →
      (F : CategoryTheory.Functor (CategoryTheory.CostructuredArrow CategoryTheory.yoneda A)ᵒᵖ (Type v)) →
        F ≅
          CategoryTheory.OverPresheafAux.restrictedYonedaObj
            (CategoryTheory.OverPresheafAux.yonedaCollectionPresheafToA F)
-- Mathlib.CategoryTheory.Monoidal.Grp
CategoryTheory.GrpObj.ext_iff : ∀ {C : Type u₁} [inst : CategoryTheory.Category.{v₁, u₁} C] [inst_1 : CategoryTheory.CartesianMonoidalCategory C]
  {X : C} {h₁ h₂ : CategoryTheory.GrpObj X}, h₁ = h₂ ↔ h₁.toMonObj = h₂.toMonObj
-- Std.Data.DTreeMap.Internal.WF.Lemmas
_private.Std.Data.DTreeMap.Internal.WF.Lemmas.0.Std.DTreeMap.Internal.Impl.Const.getThenInsertIfNew?.match_1.splitter : {β : Type u_1} →
  (motive : Option β → Sort u_2) → (x : Option β) → (Unit → motive none) → ((b : β) → motive (some b)) → motive x
-- Aesop.Builder.Cases
Aesop.RuleBuilderOptions.casesPatterns : Aesop.RuleBuilderOptions → Array Aesop.CasesPattern
-- Init.Tactics
/-- `‹t›` resolves to an (arbitrary) hypothesis of type `t`.
It is useful for referring to hypotheses without accessible names.
`t` may contain holes that are solved by unification with the expected type;
in particular, `‹_›` is a shortcut for `by assumption`.
 -/
«term‹_›» : Lean.ParserDescr
-- Mathlib.CategoryTheory.Limits.Shapes.Pullback.Categorical.Basic
CategoryTheory.Limits.CategoricalPullback.natTrans_ext_iff : ∀ {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} {X : Type u₄}
  [inst_3 : CategoryTheory.Category.{v₄, u₄} X]
  {J K : CategoryTheory.Functor X (CategoryTheory.Limits.CategoricalPullback F G)} {α β : J ⟶ K},
  α = β ↔
    CategoryTheory.Functor.whiskerRight α (CategoryTheory.Limits.CategoricalPullback.π₁ F G) =
        CategoryTheory.Functor.whiskerRight β (CategoryTheory.Limits.CategoricalPullback.π₁ F G) ∧
      CategoryTheory.Functor.whiskerRight α (CategoryTheory.Limits.CategoricalPullback.π₂ F G) =
        CategoryTheory.Functor.whiskerRight β (CategoryTheory.Limits.CategoricalPullback.π₂ F G)
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
/-- The tactic `exact volume`, to be used in optional (`autoParam`) arguments.  -/
MeasureTheory.tacticVolume_tac : Lean.ParserDescr
-- Mathlib.Data.W.Basic
WType.elim_injective : ∀ {α : Type u_1} {β : α → Type u_2} (γ : Type u_3) (fγ : (a : α) × (β a → γ) → γ),
  Function.Injective fγ → Function.Injective (WType.elim γ fγ)
-- Std.Data.Iterators.Consumers.Set
/-- Traverses the given iterator and stores the emitted values in a {name}`TreeSet`.

If the iterator is not finite, this function might run forever. Given {givenInstance}`Finite α Id`,
the variant {lean}`it.ensureTermination.toTreeSet cmp` always terminates after finitely many steps.
 -/
Std.Iter.toTreeSet : {α β : Type w} →
  [inst : Std.Iterator α Id β] →
    [Std.IteratorLoop α Id Id] →
      Std.Iter β → (cmp : autoParam (β → β → Ordering) Std.Iter.toTreeSet._auto_1) → Std.TreeSet β cmp
-- Mathlib.MeasureTheory.Measure.MeasureSpaceDef
MeasureTheory.Measure.instOuterMeasureClass : ∀ {α : Type u_1} [inst : MeasurableSpace α], MeasureTheory.OuterMeasureClass (MeasureTheory.Measure α) α
-- Init.Data.Iterators.Lemmas.Producers.Monadic.List
_private.Init.Data.Iterators.Lemmas.Producers.Monadic.List.0.Std.Iterators.Types.ListIterator.instIterator.match_3.eq_1 : ∀ {m : Type u_1 → Type u_2} {α : Type u_1} (motive : Std.IterM m α → Sort u_3)
  (h_1 : Unit → motive { internalState := { list := [] } })
  (h_2 : (x : α) → (xs : List α) → motive { internalState := { list := x :: xs } }),
  (match { internalState := { list := [] } } with
    | { internalState := { list := [] } } => h_1 ()
    | { internalState := { list := x :: xs } } => h_2 x xs) =
    h_1 ()
-- Mathlib.Data.Ordering.Lemmas
Ordering.ite_eq_gt_distrib : ∀ (c : Prop) [inst : Decidable c] (a b : Ordering),
  ((if c then a else b) = Ordering.gt) = if c then a = Ordering.gt else b = Ordering.gt
-- Std.Data.ExtTreeMap.Lemmas
Std.ExtTreeMap.foldlM_eq_foldlM_keys : ∀ {α : Type u} {β : Type v} {cmp : α → α → Ordering} {t : Std.ExtTreeMap α β cmp} {δ : Type w} {m : Type w → Type w'}
  [inst : Std.TransCmp cmp] [inst_1 : Monad m] [inst_2 : LawfulMonad m] {f : δ → α → m δ} {init : δ},
  Std.ExtTreeMap.foldlM (fun d a x => f d a) init t = List.foldlM f init t.keys
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.braiding_map_braiding_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  [inst_2 : CategoryTheory.Limits.HasBinaryBiproducts C] {W X Y Z : C} (f : W ⟶ Y) (g : X ⟶ Z) {Z_1 : C}
  (h : Z ⊞ Y ⟶ Z_1),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding X W).hom
      (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map f g)
        (CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.braiding Y Z).hom h)) =
    CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.biprod.map g f) h
-- Mathlib.Algebra.Group.Action.End
mulAutArrow_apply_symm_apply : ∀ {G : Type u_1} {M : Type u_2} {A : Type u_4} [inst : Group G] [inst_1 : MulAction G A] [inst_2 : Monoid M] (x : G)
  (a : A → M) (a_1 : A), (MulEquiv.symm (mulAutArrow x)) a a_1 = (x⁻¹ • a) a_1
-- Mathlib.LinearAlgebra.ExteriorAlgebra.Grading
/-- The union of the images of the maps `ExteriorAlgebra.ιMulti R n` for `n` running through
all natural numbers spans the exterior algebra.  -/
ExteriorAlgebra.ιMulti_span : ∀ (R : Type u_1) (M : Type u_2) [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M],
  Submodule.span R (Set.range fun x => (ExteriorAlgebra.ιMulti R x.fst) x.snd) = ⊤
-- Mathlib.Analysis.SpecialFunctions.Pochhammer
/-- Special case of **Jensen's inequality** for `Nat.choose`.  -/
descPochhammer_eval_div_factorial_le_sum_choose : ∀ {n : ℕ},
  n ≠ 0 →
    ∀ {ι : Type u_2} {t : Finset ι} (p : ι → ℕ) (w : ι → ℝ),
      (∀ i ∈ t, 0 ≤ w i) →
        ∑ i ∈ t, w i = 1 →
          ↑n - 1 ≤ ∑ i ∈ t, w i * ↑(p i) →
            Polynomial.eval (∑ i ∈ t, w i * ↑(p i)) (descPochhammer ℝ n) / ↑n.factorial ≤
              ∑ i ∈ t, w i * ↑((p i).choose n)
-- Mathlib.Data.Finset.Erase
Finset.subset_erase : ∀ {α : Type u_1} [inst : DecidableEq α] {a : α} {s t : Finset α}, s ⊆ t.erase a ↔ s ⊆ t ∧ a ∉ s
-- Mathlib.MeasureTheory.Measure.Haar.Unique
MeasureTheory.Measure.measure_isHaarMeasure_eq_smul_of_isEverywherePos : ∀ {G : Type u_1} [inst : TopologicalSpace G] [inst_1 : Group G] [inst_2 : IsTopologicalGroup G]
  [inst_3 : MeasurableSpace G] [inst_4 : BorelSpace G] [LocallyCompactSpace G] (μ' μ : MeasureTheory.Measure G)
  [inst_6 : μ.IsHaarMeasure] [inst_7 : μ'.IsHaarMeasure] {s : Set G},
  MeasurableSet s → μ.IsEverywherePos s → μ' s = μ'.haarScalarFactor μ • μ s
-- Mathlib.LinearAlgebra.Matrix.Defs
/-- The top-right `u × r` part of a `(u+d) × (l+r)` matrix.  -/
Matrix.subUpRight : {α : Type v} → {d u l r : ℕ} → Matrix (Fin (u + d)) (Fin (l + r)) α → Matrix (Fin u) (Fin r) α
-- Lean.Level
_private.Lean.Level.0.Lean.Level.geq.go.eq_def : ∀ (u v : Lean.Level),
  Lean.Level.geq.go✝ u v =
    (u == v ||
      have k := fun x =>
        match v with
        | v₁.imax v₂ => Lean.Level.geq.go✝ u v₁ && Lean.Level.geq.go✝ u v₂
        | x =>
          have v' := v.getLevelOffset;
          (u.getLevelOffset == v' || v'.isZero) && decide (u.getOffset ≥ v.getOffset);
      match u, v with
      | x, Lean.Level.zero => true
      | u, v₁.max v₂ => Lean.Level.geq.go✝ u v₁ && Lean.Level.geq.go✝ u v₂
      | u₁.max u₂, v => Lean.Level.geq.go✝ u₁ v || Lean.Level.geq.go✝ u₂ v || k ()
      | a.imax u₂, v => Lean.Level.geq.go✝ u₂ v
      | u.succ, v.succ => Lean.Level.geq.go✝ u v
      | x, x_1 => k ())