mathlib-initiative/mathlib-types huggingface dataset:
-- Init.Data.Iterators.Basic
Std.IterStep.skip.injEq : ∀ {α : Sort u_1} {β : Sort u_2} (it it_1 : α), (Std.IterStep.skip it = Std.IterStep.skip it_1) = (it = it_1)
-- Mathlib.LinearAlgebra.AffineSpace.AffineEquiv
AffineEquiv.prodCongr_apply : ∀ {k : Type u_1} {P₁ : Type u_2} {P₂ : Type u_3} {P₃ : Type u_4} {P₄ : Type u_5} {V₁ : Type u_6} {V₂ : Type u_7}
  {V₃ : Type u_8} {V₄ : Type u_9} [inst : Ring k] [inst_1 : AddCommGroup V₁] [inst_2 : AddCommGroup V₂]
  [inst_3 : AddCommGroup V₃] [inst_4 : AddCommGroup V₄] [inst_5 : Module k V₁] [inst_6 : Module k V₂]
  [inst_7 : Module k V₃] [inst_8 : Module k V₄] [inst_9 : AddTorsor V₁ P₁] [inst_10 : AddTorsor V₂ P₂]
  [inst_11 : AddTorsor V₃ P₃] [inst_12 : AddTorsor V₄ P₄] (e₁ : P₁ ≃ᵃ[k] P₂) (e₂ : P₃ ≃ᵃ[k] P₄) (p : P₁ × P₃),
  (e₁.prodCongr e₂) p = (e₁ p.1, e₂ p.2)
-- Init.Data.String.Lemmas.Pattern.TakeDrop.Basic
String.Slice.skipPrefixWhile_eq_skipWhile_startPos : ∀ {ρ : Type} {pat : ρ} [inst : String.Slice.Pattern.ForwardPattern pat] {s : String.Slice},
  s.skipPrefixWhile pat = s.startPos.skipWhile pat
-- Mathlib.Algebra.SkewPolynomial.Basic
SkewPolynomial.monomial_mul_X_pow : ∀ {R : Type u_1} [inst : Semiring R] [inst_1 : MulSemiringAction (Multiplicative ℕ) R] (n : ℕ) (r : R) (k : ℕ),
  (SkewPolynomial.monomial n) r * SkewPolynomial.X ^ k = (SkewPolynomial.monomial (n + k)) r
-- Mathlib.Data.Finset.Lattice.Fold
Finset.coe_sup' : ∀ {α : Type u_2} {β : Type u_3} [inst : SemilatticeSup α] {s : Finset β} (H : s.Nonempty) (f : β → α),
  ↑(s.sup' H f) = s.sup (WithBot.some ∘ f)
-- Mathlib.Combinatorics.SimpleGraph.AdjMatrix
Matrix.isSymm_compl : ∀ {α : Type u_1} {V : Type u_2} [inst : DecidableEq α] [inst_1 : DecidableEq V] (A : Matrix V V α) [inst_2 : Zero α]
  [inst_3 : One α], A.IsSymm → A.compl.IsSymm
-- Mathlib.ModelTheory.Syntax
/-- The equality of two terms as a bounded formula.  -/
FirstOrder.«term_='_» : Lean.TrailingParserDescr
-- Mathlib.MeasureTheory.Function.StronglyMeasurable.Basic
MeasureTheory.stronglyMeasurable_const : ∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} [inst : TopologicalSpace β] {b : β},
  MeasureTheory.StronglyMeasurable fun x => b
-- Std.Data.DTreeMap.Lemmas
Std.DTreeMap.get!_filterMap : ∀ {α : Type u} {β : α → Type v} {cmp : α → α → Ordering} {t : Std.DTreeMap α β cmp} {γ : α → Type w} [Std.TransCmp cmp]
  [inst : Std.LawfulEqCmp cmp] {f : (a : α) → β a → Option (γ a)} {k : α} [inst_1 : Inhabited (γ k)],
  (Std.DTreeMap.filterMap f t).get! k = ((t.get? k).bind (f k)).get!
-- Lean.Elab.InfoTree.InlayHints
Lean.Elab.InlayHintLabel.parts.inj : ∀ {p p_1 : Array Lean.Elab.InlayHintLabelPart},
  Lean.Elab.InlayHintLabel.parts p = Lean.Elab.InlayHintLabel.parts p_1 → p = p_1
-- Mathlib.CategoryTheory.Limits.Shapes.BinaryBiproducts
CategoryTheory.Limits.biprod.inl_fst_assoc : ∀ {C : Type uC} [inst : CategoryTheory.Category.{uC', uC} C] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms C]
  {X Y : C} [inst_2 : CategoryTheory.Limits.HasBinaryBiproduct X Y] {Z : C} (h : X ⟶ Z),
  CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.inl
      (CategoryTheory.CategoryStruct.comp CategoryTheory.Limits.biprod.fst h) =
    h
-- Mathlib.Topology.EMetricSpace.Defs
Metric.eball_subset_closedEBall : ∀ {α : Type u} [inst : PseudoEMetricSpace α] {x : α} {ε : ENNReal}, Metric.eball x ε ⊆ Metric.closedEBall x ε
-- Mathlib.Algebra.Category.Ring.FilteredColimits
/-- The bundled ring giving the filtered colimit of a diagram.  -/
RingCat.FilteredColimits.colimit : {J : Type v} →
  [inst : CategoryTheory.SmallCategory J] → [CategoryTheory.IsFiltered J] → CategoryTheory.Functor J RingCat → RingCat
-- Mathlib.Order.BooleanAlgebra.Set
/-- **Alias** of `Set.compl_eq_univ_sdiff`. -/
Set.compl_eq_univ_diff : ∀ {α : Type u_1} (s : Set α), sᶜ = Set.univ \ s
-- Mathlib.RingTheory.MvPolynomial.Ideal
/-- `x` is in a monomial ideal generated by `s` iff every element of its support dominates one of
the generators. Note that `si ≤ xi` is analogous to saying that the monomial corresponding to `si`
divides the monomial corresponding to `xi`.  -/
MvPolynomial.mem_ideal_span_monomial_image : ∀ {σ : Type u_1} {R : Type u_2} [inst : CommSemiring R] {x : MvPolynomial σ R} {s : Set (σ →₀ ℕ)},
  x ∈ Ideal.span ((fun s => (MvPolynomial.monomial s) 1) '' s) ↔ ∀ xi ∈ x.support, ∃ si ∈ s, si ≤ xi
-- Mathlib.Analysis.Normed.Ring.Basic
enorm_pow : ∀ {α : Type u_2} [inst : SeminormedRing α] [NormOneClass α] [NormMulClass α] (a : α) (n : ℕ), ‖a ^ n‖ₑ = ‖a‖ₑ ^ n
-- Mathlib.Analysis.Calculus.Deriv.Add
differentiableOn_neg : ∀ {𝕜 : Type u} [inst : NontriviallyNormedField 𝕜] (s : Set 𝕜), DifferentiableOn 𝕜 Neg.neg s
-- Mathlib.RingTheory.NonUnitalSubring.Basic
NonUnitalSubring.mem_closure_of_mem : ∀ {R : Type u} [inst : NonUnitalNonAssocRing R] {s : Set R} {x : R}, x ∈ s → x ∈ NonUnitalSubring.closure s
-- Mathlib.Order.Filter.Extr
IsMaxOn.inf : ∀ {α : Type u} {β : Type v} [inst : SemilatticeInf β] {f g : α → β} {a : α} {s : Set α},
  IsMaxOn f s a → IsMaxOn g s a → IsMaxOn (fun x => f x ⊓ g x) s a
-- Lean.Meta.Tactic.Grind.EMatchTheorem
Lean.Meta.Grind.EMatchTheoremKind.gen : Lean.Meta.Grind.EMatchTheoremKind → Bool
-- Mathlib.Topology.NhdsWithin
nhdsSet_induced : ∀ {α : Type u_5} {β : Type u_6} {t : TopologicalSpace β} (f : α → β) (s : Set α),
  nhdsSet s = Filter.comap f (nhdsSet (f '' s))
-- Mathlib.Tactic.GCongr.Core
_private.Mathlib.Tactic.GCongr.Core.0.Mathlib.Tactic.GCongr.addGCongrLemma.addImpGCongrLemma.findIdx : (xs : Array Lean.Expr) → Lean.Name → (i : ℕ) → i ≤ xs.size → Lean.MetaM (Fin xs.size)
-- Mathlib.Data.Multiset.AddSub
Multiset.card_add : ∀ {α : Type u_1} (s t : Multiset α), (s + t).card = s.card + t.card
-- Mathlib.Algebra.Group.AddChar
MonoidHom.compAddChar_injective_right : ∀ {B : Type u_2} {M : Type u_3} {N : Type u_4} [inst : AddMonoid B] [inst_1 : Monoid M] [inst_2 : Monoid N]
  (f : M →* N), Function.Injective ⇑f → Function.Injective fun ψ => f.compAddChar ψ
-- Mathlib.CategoryTheory.Limits.Shapes.Products
CategoryTheory.Limits.Pi.isoLimit_inv_π : ∀ {α : Type w₂} {C : Type u} [inst : CategoryTheory.Category.{v, u} C]
  (X : CategoryTheory.Functor (CategoryTheory.Discrete α) C)
  [inst_1 : CategoryTheory.Limits.HasProduct fun j => X.obj { as := j }] [inst_2 : CategoryTheory.Limits.HasLimit X]
  (j : α),
  CategoryTheory.CategoryStruct.comp (CategoryTheory.Limits.Pi.isoLimit X).inv
      (CategoryTheory.Limits.Pi.π (fun j => X.obj { as := j }) j) =
    CategoryTheory.Limits.limit.π X { as := j }
-- Mathlib.CategoryTheory.Localization.Monoidal.Basic
CategoryTheory.Localization.instCategoryLocalizedMonoidal : {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] →
        (L : CategoryTheory.Functor C D) →
          (W : CategoryTheory.MorphismProperty C) →
            [inst_2 : CategoryTheory.MonoidalCategory C] →
              [inst_3 : W.IsMonoidal] →
                [inst_4 : L.IsLocalization W] →
                  {unit : D} →
                    (ε : L.obj (CategoryTheory.MonoidalCategoryStruct.tensorUnit C) ≅ unit) →
                      CategoryTheory.Category.{v_2, u_2} (CategoryTheory.LocalizedMonoidal L W ε)
-- Init.Data.Float.Float32
/-- Subtracts 32-bit floating-point numbers according to IEEE 754. Typically used via the `-` operator.

This function has a logical model in terms of `Float32.Model`. It is compiled to the C subtraction operator.
 -/
Float32.sub : Float32 → Float32 → Float32
-- Lean.Parser.Types
Lean.Parser.ParserState.next : Lean.Parser.ParserState → Lean.Parser.ParserContext → String.Pos.Raw → Lean.Parser.ParserState
-- Mathlib.Topology.Algebra.IsUniformGroup.Basic
TendstoLocallyUniformly.mul : ∀ {α : Type u_1} [inst : UniformSpace α] [inst_1 : Group α] [IsUniformGroup α] {ι : Type u_3} {X : Type u_4}
  [inst_3 : TopologicalSpace X] {F G : ι → X → α} {f g : X → α} {l : Filter ι},
  TendstoLocallyUniformly F f l → TendstoLocallyUniformly G g l → TendstoLocallyUniformly (F * G) (f * g) l
-- Mathlib.Logic.Equiv.Functor
/-- Apply a functor to an `Equiv`.  -/
Functor.mapEquiv : {α β : Type u} → (f : Type u → Type v) → [inst : Functor f] → [LawfulFunctor f] → α ≃ β → f α ≃ f β
-- Mathlib.Algebra.Order.Ring.WithTop
WithBot.instMulZeroClass : {α : Type u_1} → [DecidableEq α] → [MulZeroClass α] → MulZeroClass (WithBot α)
-- Std.Data.DTreeMap.Internal.Queries
_private.Std.Data.DTreeMap.Internal.Queries.0.Std.DTreeMap.Internal.Impl.Const.minEntryD.match_1.splitter : {α : Type u_1} →
  {β : Type u_2} →
    (motive : (Std.DTreeMap.Internal.Impl α fun x => β) → α × β → Sort u_3) →
      (x : Std.DTreeMap.Internal.Impl α fun x => β) →
        (x_1 : α × β) →
          ((fallback : α × β) → motive Std.DTreeMap.Internal.Impl.leaf fallback) →
            ((size : ℕ) →
                (k : α) →
                  (v : β) →
                    (r : Std.DTreeMap.Internal.Impl α fun x => β) →
                      (x : α × β) →
                        motive (Std.DTreeMap.Internal.Impl.inner size k v Std.DTreeMap.Internal.Impl.leaf r) x) →
              ((size : ℕ) →
                  (k : α) →
                    (v : β) →
                      (size_1 : ℕ) →
                        (k_1 : α) →
                          (v_1 : β) →
                            (l r r_1 : Std.DTreeMap.Internal.Impl α fun x => β) →
                              (fallback : α × β) →
                                motive
                                  (Std.DTreeMap.Internal.Impl.inner size k v
                                    (Std.DTreeMap.Internal.Impl.inner size_1 k_1 v_1 l r) r_1)
                                  fallback) →
                motive x x_1
-- Mathlib.Topology.Algebra.Module.Alternating.Basic
ContinuousAlternatingMap.coe_continuous : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_4} {ι : Type u_6} [inst : Semiring R] [inst_1 : AddCommMonoid M]
  [inst_2 : Module R M] [inst_3 : TopologicalSpace M] [inst_4 : AddCommMonoid N] [inst_5 : Module R N]
  [inst_6 : TopologicalSpace N] (f : M [⋀^ι]→L[R] N), Continuous ⇑f
-- Mathlib.CategoryTheory.Triangulated.TStructure.TruncLTGE
CategoryTheory.Triangulated.TStructure.triangleLTLTGELT_map_hom₂ : ∀ {C : Type u} [inst : CategoryTheory.Category.{v, u} C] [inst_1 : CategoryTheory.Preadditive C]
  [inst_2 : CategoryTheory.Limits.HasZeroObject C] [inst_3 : CategoryTheory.HasShift C ℤ]
  [inst_4 : ∀ (n : ℤ), (CategoryTheory.shiftFunctor C n).Additive] [inst_5 : CategoryTheory.Pretriangulated C]
  (t : CategoryTheory.Triangulated.TStructure C) (a b : ℤ) (h : a ≤ b) {X Y : C} (φ : X ⟶ Y),
  ((t.triangleLTLTGELT a b h).map φ).hom₂ = (t.truncLT b).map φ
-- Mathlib.RingTheory.RingHomProperties
RingHom.IsStableUnderBaseChange.pushout_inl : ∀ {P : {R S : Type u} → [inst : CommRing R] → [inst_1 : CommRing S] → (R →+* S) → Prop},
  RingHom.IsStableUnderBaseChange P →
    RingHom.RespectsIso P →
      ∀ {R S T : CommRingCat} (f : R ⟶ S) (g : R ⟶ T),
        P (CommRingCat.Hom.hom g) → P (CommRingCat.Hom.hom (CategoryTheory.Limits.pushout.inl f g))
-- Mathlib.RingTheory.Noetherian.Basic
isNoetherian_prod : ∀ {R : Type u_1} {M : Type u_3} {N : Type u_4} [inst : Ring R] [inst_1 : AddCommGroup M] [inst_2 : AddCommGroup N]
  [inst_3 : Module R M] [inst_4 : Module R N] [IsNoetherian R M] [IsNoetherian R N], IsNoetherian R (M × N)
-- Mathlib.Order.Booleanisation
Booleanisation.comp_bot : ∀ {α : Type u_1} [inst : GeneralizedBooleanAlgebra α], Booleanisation.comp ⊥ = ⊤
-- Init.System.IO
/-- Monotonically increasing time since an unspecified past point in milliseconds. There is no relation
to wall clock time.
 -/
IO.monoMsNow : BaseIO ℕ
-- Mathlib.RingTheory.Ideal.Cotangent
Ideal.instIsScalarTowerQuotientHPowKerRingHomAlgebraMapOfNat : ∀ {R : Type u} [inst : CommRing R] {A : Type u_1} {B : Type u_2} [inst_1 : CommRing A] [inst_2 : CommRing B]
  [inst_3 : Algebra R A] [inst_4 : Algebra R B] [inst_5 : Algebra A B] [IsScalarTower R A B],
  IsScalarTower R (A ⧸ RingHom.ker (algebraMap A B) ^ 2) B
-- Mathlib.Topology.Order.Basic
nhdsLE_basis : ∀ {α : Type u} [inst : TopologicalSpace α] [inst_1 : LinearOrder α] [OrderTopology α] [NoMinOrder α] (a : α),
  (nhdsWithin a (Set.Iic a)).HasBasis (fun u => u < a) fun u => Set.Ioc u a
-- Mathlib.RepresentationTheory.Homological.GroupCohomology.Functoriality
groupCohomology.map_id_comp : ∀ {k G : Type u} [inst : CommRing k] [inst_1 : Group G] {A B C : Rep.{u, u, u} k G} (φ : A ⟶ B) (ψ : B ⟶ C) (n : ℕ),
  groupCohomology.map (MonoidHom.id G) (CategoryTheory.CategoryStruct.comp φ ψ) n =
    CategoryTheory.CategoryStruct.comp (groupCohomology.map (MonoidHom.id G) φ n)
      (groupCohomology.map (MonoidHom.id G) ψ n)
-- Mathlib.GroupTheory.GroupAction.Hom
/-- The identity map as an equivariant map.  -/
AddActionHom.id : (M : Type u_2) → {X : Type u_5} → [inst : VAdd M X] → X →ₑ[id] X
-- Mathlib.CategoryTheory.Idempotents.Karoubi
CategoryTheory.Idempotents.Karoubi.mk.congr_simp : ∀ {C : Type u_1} [inst : CategoryTheory.Category.{v_1, u_1} C] (X : C) (p p_1 : X ⟶ X) (e_p : p = p_1)
  (idem : CategoryTheory.CategoryStruct.comp p p = p),
  { X := X, p := p, idem := idem } = { X := X, p := p_1, idem := ⋯ }
-- Std.Data.ExtDHashMap.Lemmas
Std.ExtDHashMap.getKeyD_filter : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {β : α → Type v} {m : Std.ExtDHashMap α β} [inst : LawfulBEq α]
  {f : (a : α) → β a → Bool} {k fallback : α},
  (Std.ExtDHashMap.filter f m).getKeyD k fallback =
    ((m.getKey? k).pfilter fun x_2 h' => f x_2 (m.get x_2 ⋯)).getD fallback
-- Mathlib.Order.Interval.Finset.Defs
LocallyFiniteOrderTop.ofIci'.eq_1 : ∀ (α : Type u_1) [inst : Preorder α] [inst_1 : DecidableLE α] (finsetIci : α → Finset α)
  (mem_Ici : ∀ (a x : α), x ∈ finsetIci a ↔ a ≤ x),
  LocallyFiniteOrderTop.ofIci' α finsetIci mem_Ici =
    { finsetIoi := fun a => {x ∈ finsetIci a | ¬x ≤ a}, finsetIci := finsetIci, finset_mem_Ici := mem_Ici,
      finset_mem_Ioi := ⋯ }
-- Batteries.Recycling.RBTree.Basic
RBTree.RBNode.Path.right.injEq : ∀ {α : Type u} (c : RBTree.RBColor) (l : RBTree.RBNode α) (v : α) (parent : RBTree.RBNode.Path α) (c_1 : RBTree.RBColor)
  (l_1 : RBTree.RBNode α) (v_1 : α) (parent_1 : RBTree.RBNode.Path α),
  (RBTree.RBNode.Path.right c l v parent = RBTree.RBNode.Path.right c_1 l_1 v_1 parent_1) =
    (c = c_1 ∧ l = l_1 ∧ v = v_1 ∧ parent = parent_1)
-- Mathlib.Topology.Separation.Regular
/-- In a (possibly non-Hausdorff) locally compact regular space, for every containment `K ⊆ U` of
a compact set `K` in an open set `U`, there is a compact closed neighborhood `L`
such that `K ⊆ L ⊆ U`: equivalently, there is a compact closed set `L` such
that `K ⊆ interior L` and `L ⊆ U`.  -/
exists_compact_closed_between : ∀ {X : Type u_1} [inst : TopologicalSpace X] [LocallyCompactSpace X] [RegularSpace X] {K U : Set X},
  IsCompact K → IsOpen U → K ⊆ U → ∃ L, IsCompact L ∧ IsClosed L ∧ K ⊆ interior L ∧ L ⊆ U
-- Mathlib.Algebra.Homology.HomologicalComplex
CochainComplex.of_d_ne : ∀ {V : Type u} [inst : CategoryTheory.Category.{v, u} V] [inst_1 : CategoryTheory.Limits.HasZeroMorphisms V]
  {α : Type u_2} [inst_2 : AddRightCancelSemigroup α] [inst_3 : One α] [inst_4 : DecidableEq α] (X : α → V)
  (d : (n : α) → X n ⟶ X (n + 1)) {i j : α}, i + 1 ≠ j → CochainComplex.of.d X d i j = 0
-- Mathlib.Probability.Kernel.Defs
ProbabilityTheory.Kernel.instSubsingletonOfIsEmpty : ∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} [IsEmpty β],
  Subsingleton (ProbabilityTheory.Kernel α β)
-- Mathlib.Analysis.Complex.UpperHalfPlane.Basic
UpperHalfPlane.norm_ρ : ‖↑UpperHalfPlane.ρ‖ = 1
-- Mathlib.Algebra.Category.MonCat.Basic
AddMonCat.mk.sizeOf_spec : ∀ (carrier : Type u) [str : AddMonoid carrier],
  sizeOf { carrier := carrier, str := str } = 1 + sizeOf carrier + sizeOf str
-- Init.Sym.Lemmas
Lean.Sym.Rat.lt_eq_false : ∀ (a b : ℚ), decide (a < b) = false → (a < b) = False
-- Mathlib.Topology.Covering.Basic
isCoveringMap_iff_isCoveringMapOn_univ : ∀ {E : Type u_1} {X : Type u_2} [inst : TopologicalSpace E] [inst_1 : TopologicalSpace X] {f : E → X},
  IsCoveringMap f ↔ IsCoveringMapOn f Set.univ
-- Mathlib.CategoryTheory.Limits.Shapes.Equalizers
/-- If `C` has all colimits of diagrams `parallelPair f g`, then it has all coequalizers  -/
CategoryTheory.Limits.hasCoequalizers_of_hasColimit_parallelPair : ∀ (C : Type u) [inst : CategoryTheory.Category.{v, u} C]
  [∀ {X Y : C} {f g : X ⟶ Y}, CategoryTheory.Limits.HasColimit (CategoryTheory.Limits.parallelPair f g)],
  CategoryTheory.Limits.HasCoequalizers C
-- Mathlib.RingTheory.ClassGroup.Basic
ClassGroup.mk0_eq_one_iff : ∀ {R : Type u_1} [inst : CommRing R] [inst_1 : IsDomain R] [inst_2 : IsDedekindDomain R] {I : Ideal R}
  (hI : I ∈ nonZeroDivisors (Ideal R)), ClassGroup.mk0 ⟨I, hI⟩ = 1 ↔ Submodule.IsPrincipal I
-- Lean.Meta.Tactic.Simp.BuiltinSimprocs.UInt
UInt32.reduceOfNat : Lean.Meta.Simp.DSimproc
-- Batteries.Data.BinomialHeap.Basic
/-- `O(log n)`. Returns the smallest element in the heap, or panics if the heap is empty.  -/
Batteries.BinomialHeap.head! : {α : Type u} → {le : α → α → Bool} → [Inhabited α] → Batteries.BinomialHeap α le → α
-- Mathlib.LinearAlgebra.PerfectPairing.Basic
Submodule.dualAnnihilator_map_linearEquiv_flip_symm : ∀ {R : Type u_1} {M : Type u_2} {N : Type u_3} [inst : CommRing R] [inst_1 : AddCommGroup M] [inst_2 : Module R M]
  [inst_3 : AddCommGroup N] [inst_4 : Module R N] [inst_5 : Module.IsReflexive R M] (e : N ≃ₗ[R] Module.Dual R M)
  (p : Submodule R (Module.Dual R N)),
  (Submodule.map (↑e.flip.symm) p).dualAnnihilator = Submodule.map (↑e) p.dualCoannihilator
-- Std.Sync.Notify
Std.Notify.Consumer.select : {α : Type} → Std.Async.Waiter α → Std.Notify.Consumer α
-- Std.Data.DTreeMap.Internal.Model
Std.DTreeMap.Internal.Impl.Const.entryAtIdxD.eq_1 : ∀ {α : Type u} {β : Type v} (x : ℕ) (x_1 : α × β),
  Std.DTreeMap.Internal.Impl.Const.entryAtIdxD Std.DTreeMap.Internal.Impl.leaf x x_1 = x_1
-- Mathlib.Tactic.ComputeAsymptotics.Multiseries.Monomial.Basic
Tactic.ComputeAsymptotics.UnitMonomial.toFun_nil : ∀ (basis : Tactic.ComputeAsymptotics.Basis), Tactic.ComputeAsymptotics.UnitMonomial.toFun [] basis = 1
-- Mathlib.Topology.Algebra.Group.Defs
/-- Eta-expanded form of `ContinuousOn.div'` -/
ContinuousOn.fun_div' : ∀ {G : Type u_1} {X : Type u_3} [inst : TopologicalSpace X] [inst_1 : TopologicalSpace G] [inst_2 : Div G]
  [ContinuousDiv G] {f g : X → G} {s : Set X}, ContinuousOn f s → ContinuousOn g s → ContinuousOn (fun i => f i / g i) s
-- Std.Data.ExtHashMap.Basic
/-- Computes the union of the given hash maps. If a key appears in both maps, the entry contained in
the second argument will appear in the result.

This function always merges the smaller map into the larger map, so the expected runtime is
`O(min(m₁.size, m₂.size))`.
 -/
Std.ExtHashMap.union : {α : Type u} →
  {β : Type v} →
    {x : BEq α} →
      {x_1 : Hashable α} →
        [EquivBEq α] → [LawfulHashable α] → Std.ExtHashMap α β → Std.ExtHashMap α β → Std.ExtHashMap α β
-- Mathlib.LinearAlgebra.Alternating.Basic
/-- The space of constant maps is equivalent to the space of maps that are alternating with respect
to an empty family.  -/
AlternatingMap.constLinearEquivOfIsEmpty : {ι : Type u_7} →
  {R' : Type u_10} →
    {M'' : Type u_11} →
      {N'' : Type u_13} →
        [inst : CommSemiring R'] →
          [inst_1 : AddCommMonoid M''] →
            [inst_2 : AddCommMonoid N''] →
              [inst_3 : Module R' M''] → [inst_4 : Module R' N''] → [IsEmpty ι] → N'' ≃ₗ[R'] M'' [⋀^ι]→ₗ[R'] N''
-- Mathlib.Algebra.Lie.Subalgebra
LieSubalgebra.toSubmodule_mk : ∀ {R : Type u} {L : Type v} [inst : CommRing R] [inst_1 : LieRing L] [inst_2 : LieAlgebra R L] (p : Submodule R L)
  (h : ∀ {x y : L}, x ∈ p.carrier → y ∈ p.carrier → ⁅x, y⁆ ∈ p.carrier),
  { toSubmodule := p, lie_mem' := h }.toSubmodule = p
-- Mathlib.Order.Interval.Finset.Basic
Finset.Ioc_subset_Ioi_self : ∀ {α : Type u_2} {a b : α} [inst : Preorder α] [inst_1 : LocallyFiniteOrderTop α] [inst_2 : LocallyFiniteOrder α],
  Finset.Ioc a b ⊆ Finset.Ioi a
-- Mathlib.Topology.Sheaves.AddCommGrpCat
TopCat.Presheaf.sections_exact_of_exact : ∀ {X : TopCat} {U : TopologicalSpace.Opens ↑X} {S : CategoryTheory.ShortComplex (TopCat.Presheaf AddCommGrpCat X)},
  S.Exact →
    ∀ {s : ↑(S.X₂.obj (Opposite.op U))},
      (CategoryTheory.ConcreteCategory.hom (S.g.app (Opposite.op U))) s = 0 →
        ∃ t, (CategoryTheory.ConcreteCategory.hom (S.f.app (Opposite.op U))) t = s
-- Lean.Data.Lsp.Capabilities
Lean.Lsp.LeanServerCapabilities.mk.sizeOf_spec : ∀ (moduleHierarchyProvider? : Option Lean.Lsp.ModuleHierarchyOptions) (rpcProvider? : Option Lean.Lsp.RpcOptions),
  sizeOf { moduleHierarchyProvider? := moduleHierarchyProvider?, rpcProvider? := rpcProvider? } =
    1 + sizeOf moduleHierarchyProvider? + sizeOf rpcProvider?
-- Init.Data.Iterators.Basic
Std.Iterators.ProductivenessRelation.mk.sizeOf_spec : ∀ {α : Type w} {m : Type w → Type w'} {β : Type w} [inst : Std.Iterator α m β] [inst_1 : SizeOf α]
  [inst_2 : (a : Type w) → SizeOf (m a)] [inst_3 : SizeOf β] (Rel : Std.IterM m β → Std.IterM m β → Prop)
  (wf : WellFounded Rel) (subrelation : ∀ {it it' : Std.IterM m β}, it'.IsPlausibleSkipSuccessorOf it → Rel it' it),
  sizeOf { Rel := Rel, wf := wf, subrelation := subrelation } = 1 + sizeOf wf
-- Mathlib.CategoryTheory.Bicategory.NaturalTransformation.Lax
CategoryTheory.Lax.StrongTrans.categoryStruct_comp_app : ∀ {B : Type u₁} [inst : CategoryTheory.Bicategory B] {C : Type u₂} [inst_1 : CategoryTheory.Bicategory C]
  {X Y Z : CategoryTheory.LaxFunctor B C} (η : CategoryTheory.Lax.StrongTrans X Y)
  (θ : CategoryTheory.Lax.StrongTrans Y Z) (a : B),
  (CategoryTheory.CategoryStruct.comp η θ).app a = (η.toLax.vComp θ.toLax).app a
-- Lean.Meta.Tactic.Grind.OrderInsts
Lean.Meta.Grind.mkIsPartialOrderInst? : Lean.Level → Lean.Expr → Option Lean.Expr → Lean.Meta.Grind.GoalM (Option Lean.Expr)
-- Mathlib.CategoryTheory.Monoidal.Opposite
CategoryTheory.MonoidalOpposite.mopMopEquivalence_inverse_map_unmop_unmop : ∀ (C : Type u₁) [inst : CategoryTheory.Category.{v₁, u₁} C] {X Y : C} (f : X ⟶ Y),
  ((CategoryTheory.MonoidalOpposite.mopMopEquivalence C).inverse.map f).unmop.unmop = f
-- Mathlib.NumberTheory.DirichletCharacter.Basic
DirichletCharacter.primitiveCharacter_one : ∀ {R : Type u_1} [inst : CommMonoidWithZero R] {n : ℕ} [NeZero n], DirichletCharacter.primitiveCharacter 1 = 1
-- Mathlib.Algebra.Order.SuccPred.TypeTags
instIsSuccArchimedeanAdditive : ∀ {X : Type u_1} [inst : Preorder X] [inst_1 : SuccOrder X] [h : IsSuccArchimedean X], IsSuccArchimedean (Additive X)
-- Init.Data.UInt.Lemmas
UInt32.zero_div : ∀ {a : UInt32}, 0 / a = 0
-- Mathlib.Combinatorics.SimpleGraph.CycleGraph
_private.Mathlib.Combinatorics.SimpleGraph.CycleGraph.0.SimpleGraph.cycleGraph.cycleCons.eq_2 : ∀ (n m : ℕ) (h : m + 1 < n + 3),
  SimpleGraph.cycleGraph.cycleCons✝ n ⟨m.succ, h⟩ = SimpleGraph.Walk.cons ⋯ (SimpleGraph.cycleGraph.cycleCons✝ n ⟨m, ⋯⟩)
-- Std.Data.HashSet.Lemmas
Std.HashSet.get_eq : ∀ {α : Type u} {x : BEq α} {x_1 : Hashable α} {m : Std.HashSet α} [LawfulBEq α] {k : α} (h : k ∈ m), m.get k h = k
-- Mathlib.Algebra.Ring.Subring.Basic
Subring.coe_equivMapOfInjective_apply : ∀ {R : Type u} {S : Type v} [inst : NonAssocRing R] [inst_1 : NonAssocRing S] (s : Subring R) (f : R →+* S)
  (hf : Function.Injective ⇑f) (x : ↥s), ↑((s.equivMapOfInjective f hf) x) = f ↑x
-- Mathlib.Order.Interval.Set.OrdConnected
Set.ordConnected_of_uIcc_subset_left : ∀ {α : Type u_1} [inst : LinearOrder α] {s : Set α} {x : α}, (∀ y ∈ s, Set.uIcc x y ⊆ s) → s.OrdConnected
-- Mathlib.Topology.Algebra.ConstMulAction
closure_smul : ∀ {α : Type u_2} {G : Type u_4} [inst : TopologicalSpace α] [inst_1 : Group G] [inst_2 : MulAction G α]
  [ContinuousConstSMul G α] (c : G) (s : Set α), closure (c • s) = c • closure s
-- Mathlib.Order.Bounded
Set.unbounded_ge_inter_gt : ∀ {α : Type u_1} {s : Set α} [inst : LinearOrder α] (a : α),
  Set.Unbounded (fun x1 x2 => x1 ≥ x2) (s ∩ {b | b < a}) ↔ Set.Unbounded (fun x1 x2 => x1 ≥ x2) s
-- Mathlib.GroupTheory.FreeGroup.Basic
FreeGroup.IsReduced.of_forall_not_step : ∀ {α : Type u} {L₁ : List (α × Bool)}, (∀ (L₂ : List (α × Bool)), ¬FreeGroup.Red.Step L₁ L₂) → FreeGroup.IsReduced L₁
-- Mathlib.Tactic.Translate.Core
/-- Linter used by translate attributes that checks if the attribute is redundant  -/
Mathlib.Tactic.Translate.linter.translateRedundant : Lean.Option Bool